Equality on Recursive λ-Terms

equality_on_recursive_lambda_terms.md

A tricky problem in Type Theory has a short satisfactory solution. To check if two potentially recursive expressions are equal, first we take the weak head normal form of both sides, without unrolling fixed points. Then, we do:

(F . G) == (G . F)
------------------- Fix=Fix case: apply T6's Theorem
μk(F k) == μk(G k)

(F Y) == Y
------------- Fix=Val case: apply T6's Theorem
μk(F k) == Y

X == (G μk(G k))
---------------- Val=Fix case: unroll the right side
X == μk(G k)

-- Otherwise: just do case analysis and recurse, as usual. 

This might give false negatives (we believe?) but never false positives. It is elegant, efficient and covers most practical cases. You can use it to check equality on arbitrary type-level recursive expressions, which aren't allowed in conventional proof assistants. The first 2 cases use the theorem discovered by T6. Explanation and proofs in our Discord:

https://discord.com/channels/912426566838013994/1007033260662071306/1328426881111953420

For completion, below is the full algorithm in Agda pseudocode (unchecked):

data Term : Set where
  Var : Nat → Term
  Lam : (Term → Term) → Term
  App : Term → Term → Term
  Fix : (Term → Term) → Term

equal : Term → Term → Nat → Bool
equal a b d with whnf a | whnf b
... | Fix f   | Fix g   = equal (f (g (Var d))) (g (f (Var d))) d
... | Fix f   | b       = equal (f b) b d
... | a       | Fix g   = equal a (g (Fix bf)) d
... | Var i   | Var j   = i == j
... | Lam f   | Lam g   = equal (f (Var d)) (g (Var d)) (suc d)
... | App f x | App g y = equal f g d ∧ equal x y d
... | _       | _       = false

Here's the actual HVM3 code we're using:

// Equality
// ========

!@equal(a b &dep) =
  @equal_a(@whnf(a) b &dep)

!@equal_a(!a b &dep) =
  ~ a !b {
    #Fix{a_bod} : @equal_a_rec_b(a_bod @whnf(b) &dep)
    a_val       : @equal_a_val_b(a_val @whnf(b) &dep)
  }

!@equal_a_rec_b(a_bod !b &dep) = 
  ~ b !a_bod {
    #Fix{b_bod} : @equal_a_rec_b_rec(a_bod b_bod &dep)
    b_val       : @equal_a_rec_b_val(a_bod b_val &dep)
  }

!@equal_a_val_b(a_val !b &dep) =
  ~ b !a_val {
    #Fix{b_bod} : @equal_a_val_b_rec(a_val b_bod &dep)
    b_val       : @equal_a_val_b_val(a_val b_val &dep)
  }

// Fixed-Point Equality
// ===============

// μk(F k) == μk(G k)
// ---------------------- Fix-Fix case: T6 Theorem
// (F (G K)) == (G (F K))
@equal_a_rec_b_rec(F G &dep) =
  ! &{F0 F1} = F
  ! &{G0 G1} = G
  @equal((F0 (G0 #Var{&dep})) (G1 (F1 #Var{&dep})) &dep)

// μk(F k) == Y
// ------------- Fix-Val case: T6 Theorem
// (F Y) == Y
@equal_a_rec_b_val(F Y &dep) =
  ! &{Y0 Y1} = Y
  @equal((F Y0) Y1 &dep)

// X == μk(G k)
// ---------------- Val-Fix case: just unroll
// X == (G μk(G k))
@equal_a_val_b_rec(X G &dep) =
  ! &{G0 G1} = G
  @equal(X (G0 #Fix{G1}) &dep)

// Value Equality
// ==============

!@equal_a_val_b_val(!a !b &dep) = ~ a !b {
  #Var{ai}: ~ b !ai {
    #Var{bi}: (== ai bi)
    b: 0
  }
  #Lam{ab}: ~ b !ab {
    #Lam{bb}: @equal((ab #Var{&dep}) (bb #Var{&dep}) (+ &dep 1))
    b: 0
  }
  #App{af aa}: ~ b !af !aa {
    #App{bf ba}: @and(@equal(af bf &dep) @equal(aa ba &dep))
    b: 0
  }
}

Note ~ stands for match.

Taelin — Yesterday at 15:14
can someone help me quickly find/link where T6 proposed his fixed point equality formula?
@Team /\
enricozb — Yesterday at 15:14
for ITT or the WHY combinator?
Taelin — Yesterday at 15:14
the μx f x == μy g y thing
I think it was this:
// μx (F x) == μy (G y)
// ----------------------
// (F (G X)) == (G (F X))
but i want to double check
(here I'm making X a rigid variable)
enricozb — Yesterday at 15:17
not sure what's being referred to here... don't think i'll be much better than searching "fixed point" from:@T6
Taelin — Yesterday at 15:19
I tried
nicolas. — Yesterday at 15:21
⁠kind⁠
this i think
i searched for µ (not μ that's a different character) 
enricozb — Yesterday at 15:24
wow
Taelin — Yesterday at 15:35
lol
thanks
if you now can also find a post where I show a counter-example where T6's algorithm will diverge that'd be appreciated 😅
T6 — Yesterday at 15:39
this was where I originally came up with it: ⁠unknown
T6 — Yesterday at 15:41
hmm I don't recall this
T6 — Yesterday at 15:42
yeah I have a bad habit of using the 'micro' character in place of the 'mu' character because I can type micro with option+m
Taelin — Yesterday at 15:49
@T6 how do you handle μx. (F x) == G when G doesn't reduce to a fixed point? do you just unroll the left side?
T6 — Yesterday at 15:49
just check (F G) == G 
Taelin — Yesterday at 15:50
so you never unroll at all?
during equality
T6 — Yesterday at 15:50
no
Taelin — Yesterday at 15:50
will that be capable of checking recursive functions though? like not types, but say, double 7 etc.
T6 — Yesterday at 15:52
not sure what exactly you mean but probably not
if you mean checking equality on recursive functions
though that's undecidable, so...
Taelin — Yesterday at 15:53
say you use μ to define recursive functions (like double = μF. λx. ...)...
hmm my understanding is that your algorithm wouldn't diverge, either halt or give you a false negative
T6 — Yesterday at 15:54
my algorithm won't give false positives
not sure what false negatives it may have in that context
maybe few enough for it to be useful, maybe not
I don't think it would diverge either
though I don't have a proof of that
T6 — Yesterday at 15:57
(proof: ⁠unknown)
Taelin — Yesterday at 15:58
I see
cool, thanks
I think I could use it for recursive types at the very least
Taelin — Yesterday at 17:09
I can't find my message, but I think I recall the example:

μx(1 : x) == (1 : μx(1 : x))
----------------------------
(1 : (1 : μx(1 : x))) == (1 : μx(1 : x))
----------------------------------------
(1 : μx(1 : x)) == μx(1 : x)
----------------------------
(1 : μx(1 : x)) == (1 : (1 : μx(1 : x)))
----------------------------------------
μx(1 : x) == (1 : μx(1 : x))


in this case, it will just diverge, right?
T6 — Yesterday at 17:23
ah yes, the simplest possible test case (µ F = F (µ F)) fails 🤦
Taelin — Yesterday at 17:24
I think the core of the issue is that your original equation works when both sides are fixed points, but, when only one side is, then, there are two things we could do: we could unroll the side that is, or we could apply your theorem. our goal should be to have both sides become a fixed point, but the right choice to do so depends 
T6 — Yesterday at 17:24
yeah that makes sense
Taelin — Yesterday at 17:25
note that the equation above works if you just unroll the left side
T6 — Yesterday at 17:25
I think just unrolling in those cases should do the trick?
er no
Taelin — Yesterday at 17:25
but if you always unroll, I think we can come up with other counter examples
T6 — Yesterday at 17:25
yeah it does depend
yeah like µ (F . F) = F (µ (F . F))
Taelin — Yesterday at 17:26
my hypothesis is that there is always a sequence of decisions (i.e., either unroll or apply your theorem) that results in both sides being a fixed point, which can then be resolved by your theorem
T6 — Yesterday at 17:27
I wonder if when one does T = µ F  -->  T = F T if there's some way to 'entangle' any copied µs in T that would avoid the issue
Taelin — Yesterday at 17:27
you mean manipulating the labels? that would be a powerful result
T6 — Yesterday at 17:36
goal:
F (µ F) = µ F

rewrite as:
x = F x
y = F y
F x = y
------------- subst
x = F x
F x = F (F x)
------------- simplify
x = F x
x = F x
------------- subst
F x = F x
------------- simplify
x = x
------------- tauto
success
goal:
F (µ (F . F)) = (µ (F . F))

rewrite as:
x = F (F x)
y = F (F y)
F x = y
----------- subst
x = F (F x)
F x = F (F (F x))
----------- simplify
x = F (F x)
x = F (F x)
----------- subst
F (F x) = F (F x)
----------- simplify
F x = F x
----------- simplify
x = x
----------- tauto
success
T6 — Yesterday at 17:37
the issue with this process is that the µ term keeps getting duplicated, and so no progress is made
but this is fixed if, whenever we have two copies of one original µ term, and we substitute into one of them, we also substitute into the other
though I don't know how to express that non-equationally like the above
Taelin — Yesterday at 17:50
just an example on how a sequence of unroll and T6-Theo will result in both sides being identical on this case:

(F μx(F (F x))) == μx(F (F x))
------------------------------
| Unroll:
  (F μx(F (F x))) == (F (F μ(F (F x))))
  -------------------------------------
  μx(F (F x)) == (F μ(F (F x)))
  ------
  (loop)
| T6-Theo:
  (F μx(F (F x))) == (F (F (F μx(F (F x)))))
  ------------------------------------------
  μx(F (F x)) == (F (F μx(F (F x))))
  | Unroll:
    (F (F μx(F (F x)))) == (F (F μx(F (F x))))
    ------------------------------------------
    (F μx(F (F x))) == (F μx(F (F x)))
    ----------------------------------
    μx(F (F x)) == μx(F (F x))
    --------------------------
    | T6-Theo:
      (F (F (F (F x)))) == (F (F (F (F x))))
      refl
  | T6-Theo:
    (F (F (F (F μx(F (F x)))))) == (F (F μx(F (F x))))
    --------------------------------------------------
    (F (F (F μx(F (F x))))) == (F μx(F (F x)))
    ------------------------------------------
    (F (F μx(F (F x)))) == μx(F (F x))
    | Unroll:
      (F (F μx(F (F x)))) == (F (F μx(F (F x))))
      refl


so the conjecture is this is always the case

and the question is whether there is a way to tell which action to perform rather than having to make choices. perhaps if we do the theorem when the left side is fix, and unroll when the right side is fix? i.e., choosing one side to substitute on
yeah at least on this example, this strategy works:

(F μx(F (F x))) == μx(F (F x))
-------------------------------------------- unroll (right side is μ)
(F μx(F (F x))) == (F (F μx(F (F x))))
-------------------------------------------- simplify
μx(F (F x)) == (F μx(F (F x)))
-------------------------------------------- T6-Theo (left side is μ)
(F (F (F μx(F (F x))))) == (F μx(F (F x)))
-------------------------------------------- simplify
(F (F μx(F (F x)))) == μx(F (F x))
-------------------------------------------- unroll (right side is μ)
(F (F μx(F (F x)))) == (F (F μx(F (F x))))
-------------------------------------------- simplify
(F μx(F (F x))) == (F μx(F (F x)))
-------------------------------------------- simplify
μx(F (F x)) == μx(F (F x))
-------------------------------------------- T6-Theo
(F (F (F (F x)))) == (F (F (F (F x))))
-------------------------------------------- refl
ok
is this always the case though? would be very neat and useful if yes 
Taelin — Yesterday at 18:02
so, to recap, the problem is: how to handle the fix==val equality case? the strategy of always applying T6's theorem doesn't work (counter-example: μx(1:x)==1:μx(1:x)), and the strategy "always unroll" also doesn't work (counter-example: (1:μx(1:1:x)))==μx(1:1:x)). yet, in both examples, the strategy of "unroll when the left side is fix, apply t6's theorem when the right side is fix" works. the question is: does it always work? if yes, what's the proof? if not, another question: is there always a sequence of t6-theorem | unroll's that unifies both sides? 
Taelin — Yesterday at 18:18
promising news: I just updated the superposed program enumerator to use the mixed strategy above as a drop-in replacement for the old equality (which used ugly hardcoded ids to check recursive type equality) and it works! all other strategies failed (i.e., T6-theo only, unroll only, etc.)
including super complex recursive cases. obviously not a proof but encouraging
T6 — Yesterday at 18:24
yeah I believe that works
F(x, y, a, b) = number of steps to eliminate all µs from equation `F^a (µ F^x) = F^b (µ F^y)`

F(x, y, 0, 0) = 0                     (theorem; µ on both sides)
F(x, y, 0, b) = 1 + F(y, y, x+b, b)   (theorem; µ on left)
F(x, y, a, 0) = 1 + F(x, y, a, y)     (unroll;  µ on right)
F(x, y, a, b) = 1 + F(x, y, a-1, b-1) (simplify)
Taelin — Yesterday at 18:26
that's so smart
T6 — Yesterday at 18:27
(x, y, a, b) will eventually become (y, y, p, q) which will eventually become (y, y, y+t, t) which will eventually become (y, y, y, 0) which eventually goes to (y, y, 0, 0)
Taelin — Yesterday at 18:27
T6 you literally solved the fundamental problem of Kind, congratulations
no for real, you have no idea how many hours were poured on equality and how much we had to sacrifice in the past to achieve half decent results
and as far as I can tell this is the solution
can't believe all tests worked and there isn't a single ugly hack on the equality algorithm
it just works
T6 — Yesterday at 18:28
deciding theorem vs. unroll via which side of the equation it is on is very slick
Taelin — Yesterday at 18:29
thanks but like it was literally the only bit of information that could be used to make this decision
which sadly is how I solve things I guess
T6 — Yesterday at 18:30
bahaha
Taelin — Yesterday at 18:42
for some reason the MIPS on the program synthesizer increased from 90 to 180 after this change, but interaction count also doubled. I've never seen anything like that
that wasn't the goal, just an interesting side effect















T6 — 21/12/22, 15:52
You're trying to check equality, right?
Franchu
OP
 — 21/12/22, 15:56
yes
T6 — 21/12/22, 15:58
def rec_eq_rec(a: RecursiveTerm, b: RecursiveTerm):
  var = NamedTerm("_temp")
  return eq(a.body(b.body(var)), b.body(a.body(var)))
I think that'll work
Franchu
OP
 — 21/12/22, 15:59
what i mean is, what about lam_eq_rec?
oh wait
all lambdas can be expressed as closed recursive terms of lambdas 
x = μ_ x
T6 — 21/12/22, 16:00
Yeah
So if you replace a with RecursiveTerm(lambda _: a) that becomes eq(a, b.body(a))
Which seems reasonable?
If a = b then a = b.body(a)
Not sure about the other direction
But I think it's true
Franchu
OP
 — 21/12/22, 16:03
a = b.body(a) is a true if b is a recursive term
wait no
T6 — 21/12/22, 16:04
Yeah I'm pretty sure a = b iff a = b.body(a)
T6 — 21/12/22, 16:04
So this works in general for recursive equality
Oh, a = b.body(a) is the definition of b
Franchu
OP
 — 21/12/22, 16:05
so * -> * -> ! = ! given the definition ! = * -> !
oh wow your function seems to work
you always come up with these brilliant if and only if statements
Franchu
OP
 — 21/12/22, 16:11
this works because f . g = g . f if f = g
. being composition
T6 — 21/12/22, 16:12
Yes but there's more to it
Say you have recursive terms µx f (f (f x)) and µx f (f x)
They are both f (f (f (f (f ...))))
But if you check them naively you won't find them to be equivalent
Since f . f . f != f . f
But if a = f . f . f and b = f . f then a . b = f . f . f . f . f = b . a
Franchu
OP
 — 21/12/22, 16:14
magic
T6 — 21/12/22, 16:14
Btw I believe lam_eq_rec should be
def lam_eq_rec(a: LambdaTerm, b: RecursiveTerm):
  return eq(a, b.body(b))
Franchu
OP
 — 21/12/22, 16:14
yes
it's unrolling the rec
T6 — 21/12/22, 16:14
Pretty sure using x = μ_ x, though technically correct, results in an infinite loop
Right
That definition of rec_eq_rec even works for something like µa µb f b = µc f c:
µa µb f b = µc f c
(µb f b)[a/(f c)[c/x]] = (f c)[c/(µb f b)[a/x]]
µb f b = f (µb f b)
f (µb f b) = f (µb f b)
µb f b = µb f b
f (f x) = f (f x)
Franchu
OP
 — 21/12/22, 16:24
wow
T6 — 21/12/22, 16:30
Here's one direction of the proof that this is valid:
definition of µ:
  a = µx f x iff (a = f a)

µx f x = µx g x
 iff µx f x = g (µx f x)
 iff g (µx f x) = µx f x
 iff g (µx f x) = f (g (µx f x))
 iff g (f (µx f x)) = f (g (µx f x))
  if g . f = f . g
 
Franchu
OP
 — 21/12/22, 16:31
neat
T6 — 21/12/22, 16:34
For a µ term to be valid it has to have only one fixed point
Not sure exactly how we check that
Maybe µx f x is valid only if f x != x?
So µx x would be invalid
As would be µx µ_ x
Franchu
OP
 — 21/12/22, 16:35
i guess if it prevents those cases then its enough
T6 — 21/12/22, 16:36
I think that combined with our typing of x having no upper bound other than * is enough
T6 — 21/12/22, 16:43
Oh this last if can be an iff because x has no bound
So it does work in both directions
Essentially since x: * there’s no way to discriminate on it
So either f.g and g.f are equal for all inputs or they are unequal for all inputs
Franchu
OP
 — 21/12/22, 16:46
right
Franchu
OP
 — 21/12/22, 18:01
µ x a <= µ y b
  iff x <= y -> a <= b

Can't this rule be used for equality checking too?
µ x a <= µ y b and µ x b <= µ y a, then they represent equal types
oh right, but not equal terms
T6 — 21/12/22, 19:07
This is quite possibly wrong, it was largely a guess 
T6 — 21/12/22, 19:25
I think all equal types are equal terms, but I don't have a proof
Franchu
OP
 — 21/12/22, 20:29
do you mean "equal types are definitionally equal terms"?
i'm fairly sure there's, for example, many different empty types.
Franchu
OP
 — 21/12/22, 20:42
an additional rule needs to be added at the beginning, where a <= a always
because we can check a b <= c in some cases
T6 — 21/12/22, 20:55
I think if a <= b and b <= a then a = b using our rules for each
Franchu
OP
 — 21/12/22, 20:57
eta equivalent?
T6 — 21/12/22, 20:57
Sure
Franchu
OP
 — 21/12/22, 21:04
Yay
I've finished a HVM typechecker, almost fully implementing the axioms
T6 — 21/12/22, 21:05
Nice
Franchu
OP
 — 21/12/22, 21:06
I was about to point out another error with your axioms, but it was actually an error with my implementation, where I didn't follow the axioms exactly. Your axioms are really complete.
T6 — 21/12/22, 21:07
A couple of them were wild guesses lol
They may be wrong
Is it in the gist?
Or the repo?
Franchu
OP
 — 21/12/22, 21:09
i'll upload it
the only problem is that tom avoid putting state in the typechecker, i forked HVM to allow creating unique IDs without state
in Python i used object()
this is the fork https://github.com/FranchuFranchu/HVM/tree/nodeid

here's the checker https://github.com/tjjfvi/exile/tree/hvm-checker
GitHub
[GitHub - tjjfvi/exile at hvm-checker](https://github.com/tjjfvi/exile/tree/hvm-checker)
Contribute to tjjfvi/exile development by creating an account on GitHub.
GitHub - tjjfvi/exile at hvm-checker
the way it works it's a bit complicated
T6 — 21/12/22, 21:16
You work quickly haha
Franchu
OP
 — 21/12/22, 21:17
checker.py generates a data.hvm file with some terms since I haven't bothered to implement a parser in Kind2, and then you concatenate the data.hvm file to the file produced by kind2 to-hvm, and then you'll have to run the file with the fork of HVM
run.sh does that automatically so if you're in a UNIX environment you should be fine
Franchu
OP
 — 21/12/22, 21:17
coding these sorts of things in Kind2 and HVM is extremely easy
it's a one-to-one mapping between the code and the axioms
T6 — 21/12/22, 21:17
True
T6 — 21/12/22, 21:40
Well I started on a TS impl but I should probably look at your HVM impl instead
All I got done was the parser lol
Ooh I could use the TS parser as a frontend for the HVM
Like you do with the python
But the TS parser supports full programs 
Franchu
OP
 — 21/12/22, 21:44
awesome
if we do lazy evaluation for type checking, then the type annotations are just instructions for the typechecker to check something, right?
T6 — 21/12/22, 21:46
Yea
Franchu
OP
 — 21/12/22, 21:47
so the ts file outputs a hvm file that contains the terms to check, and the main function
T6 — 21/12/22, 22:14
Pushed to a branch for ts
Have to run
But I have an initial write thing
Probably very broken
Franchu
OP
 — 21/12/22, 22:46
we've talked a lot
Image
T6 — 21/12/22, 22:48
Wow yeah








Taelin — 22/02/23, 11:12
@Franchu yes the problem isn't self types, but recursive types. once we can handle these, adding self (and thus the things you mention) would be easy
it is true that HVM's speed comes from the checker implementation, but I think we could come up with an equality function that is capable of handling recursive types, without compromising performance of non-recursive stuff
Franchu — 22/02/23, 12:42
for any two recursive terms μx (f x), μx (g x):
μx (f x) = μx (g x) 
   if and only if (f (g x)) = (g (f x)) for all x

that's one of the things we figured out in ⁠forum which I didn't know before. 
if the equality function is the only problem then that should do it, i think
Taelin — 22/02/23, 17:01
what why would that be the case
T6 — 22/02/23, 17:26
Here's one direction of it:
definition of µ:
  a = µx f x iff (a = f a)

µx f x = µx g x
 iff µx f x = g (µx f x)
 iff g (µx f x) = µx f x
 iff g (µx f x) = f (g (µx f x))
 iff g (f (µx f x)) = f (g (µx f x))
  if g . f = f . g
An example of why it works well is μx (f (f x)) = μx (f (f (f x))) 
If you naively check it you'll never find that they're equivalent
But they're both (f (f (f (f (f (f ...))))))
But if you set a = f . f and b = f . f . f, then
a . b = f . f . f . f . f = b . a
Franchu — 22/02/23, 20:51
as @T6 said, it's essentially because f ∘ g = g ∘ f iff f = g
wait no
T6 — 22/02/23, 20:52
* iff for some h exists n, m in N such that f = h^n and g = h^m
Franchu — 22/02/23, 20:52
what I said is inaccurate
the correct term is "f commutes with g", which matches with the definition of µ
Franchu — 22/02/23, 20:53
right
Taelin — 23/02/23, 13:05
oh I see
interesting
seems obvious now, thanks
but not sure how we could apply that to checking recursive types for equality
T6 — 23/02/23, 13:06
g . f = f . g is sufficient for equality, although I'm not sure if it's necessary
Taelin — 23/02/23, 13:06
wouldn't that blow up easily?
T6 — 23/02/23, 13:07
When checking μx (f x) = μx (g x), instead check if (f (g x)) = (g (f x))
It completely eliminates the recursive type
Taelin — 23/02/23, 13:07
yep I know, I mean, that will blow up
T6 — 23/02/23, 13:07
How so? It's bounded
Taelin — 23/02/23, 13:07
the normal form will get exponentially bigger
T6 — 23/02/23, 13:09
I suppose if you have n nested recursive types it could grow to a size of 2^n
But most of that would likely be cached?
It's at minimum a lot better than rolling/unrolling to to check it
Franchu — 23/02/23, 13:16
i'd bet it's the optimal way


Taelin — 23/02/23, 14:06
yep you're right, it would require an additional pass though, but fair
also look how much bigger it gets hmm
Franchu — 23/02/23, 14:10
i'm not sure what the alternatives are
Franchu — 23/02/23, 14:13
let Unit_i be the self-contained version of Unit, and Unit the rolled-up version of Unit
Let cost(x, y) the cost of checking x == y
cost(Unit_i, Unit_i) == cost(Unit, Unit) + cost(Unit.new, Unit.new)
this is because Unit_i contains only one copy of Unit.new and one copy of Unit. It is not actually that big. 
Taelin — 23/02/23, 14:20
why the need to encode it with mu? why not just leave it as is?
Franchu — 23/02/23, 14:21
but then how would we check for equality?
We would have to unroll and roll until the two terms were equal, which is definitely less performant 
Franchu — 23/02/23, 14:23
this method only works if you can easily replace the recursive variable by anything you want, which is what mu lets you do.
Taelin — 23/02/23, 14:33
why unrolling would be less performant?
Franchu — 23/02/23, 14:34
imagine you want to check unroll(unroll(Unit)) against Unit
Taelin — 23/02/23, 14:36
why unroll (unroll Unit)? there would be no unroll
Franchu — 23/02/23, 14:36
do you mean that unrolling is idempotent?
by "unrolling" i mean replacing every reference by its value once
Taelin — 23/02/23, 14:38
why would you do it though?
for example the checking for self-encoded Empty == Empty (simpler than Unit, for the sake of this example) goes like this

Empty == Empty
(%s. ∀(P: Empty -> Type) -> P s) == (%s. ∀(P: Empty -> Type) -> P s)
(∀(P: Empty -> Type) -> P s) == (∀(P: Empty -> Type) -> P s)
(Empty -> Type) == (Empty -> Type)
Empty == Empty


which returns true, since it occurred before
Franchu — 23/02/23, 14:47
that returns false negatives in some cases.
what that's implementing is 
µx f x = µx g x
 if for all x, (f x) = (g x)

In this case x = Empty.

I'm not sure if that algorithm operates with the "knowledge" that Empty = (%s. ∀(P: Empty -> Type) -> P s) and attempts to unroll it whenever you end up with something like Empty == (%s. ∀(P: Empty -> Type) -> P s), or just treats it as an opaque variable. In the first case I think that it will end up with infinite recursion in some cases. In the second cases it features false negatives.
(%s. ∀(P: (%s. ∀(P: Empty -> Type) -> P s) -> Type) -> P s) == (%s. ∀(P: Empty -> Type) -> P s) will give a false negative in the second case.
Franchu — 23/02/23, 14:59
Z = Z
Empty = (%s. ∀(P: Empty -> Type) -> P s)

Empty == Z

this check would loop infinitely in the first case, because Z would get unrolled infinitely 
i'll admit it's a degenerate case
T6 — 23/02/23, 15:03
In that case, you can change it to μx (f x) = μx (g x) --> (g (μx (f x))) = (f (μx (g x))) – it works just as well for the case where f = g = x, and is better for things like f = x . x, g = x . x . x
T6 — 23/02/23, 15:15
If approaching this in terms of recursive definitions, instead of µ terms, and you have a cache, then I think you can just swap the definitions every time you check equality between two definitions 
Foo := f (f Foo)
Bar := f (f (f Bar))
Foo == Bar
------------------------
Bar := f (f Foo)
Foo := f (f (f Bar))
f (f Foo) == f (f (f Bar))
f Foo == f (f Bar)
Foo == f Bar
f (f (f Bar)) == f Bar
f (f Bar) == Bar
f (f Bar) == f (f Foo)
f Bar == f Foo
Bar == Foo
 
That should support mutual recursion, too
T6 — 23/02/23, 15:22
Note that f was only unwrapped 2 + 3 = 5 times, not 2 * 3 = 6 times
Taelin — 24/02/23, 11:53
hmm cool stuff
will think about it