Can we determine if two λ-terms are equal?
Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, (Y λr.λt.(t r)) and (Y λr.λt.(t (λt. (t r)))) are equal, despite not having a normal form, because both terms have the same infinite Bohm trees. I believe this problem, in general, is undecidable. Is there any efficient, preferably simple algorithm capable of determining if two λ-terms are equal for some large class of common terms? The main problem, I believe, is finding the right series of reductions that make two terms identical without getting stuck in an infinite loop.
Can we determine if two equi-recursive types are equal?
Suppose we extend CoC with equi-recursive types. Naturally, type checking the application of a f : ∀ (x : A) -> B to a x : A' requires you to check if A == A'. In plain CoC, this can be done by merely reducing both sides to normal form and checking if they are equal. In the presence of equi-recursive types, though, that isn't possible. Is there any algorithm capable of checking if two types are equal in such language?
Note: I'm not sure if those questions are equivalent and I felt that asking another question would be spammy, so I've asked both in this same thread.
