1

As far as I know, two lambda terms are equal if and only if their normal forms can be $\alpha$ converted to each other.

However, for expressions that do not have a normal form (such as expressions involving a Y combinator), are there any rules to let us state two expressions are equal?

I originally thought of this problem when I tried to figure out whether $(Y\ f)$ equals $(Y\ (f\circ f))$ (where $f\circ f=\lambda x.\ f\ (f\ x)$), but I can neither prove it nor find an exception to the formula.

creaple
  • 68
  • When you write $Y f \circ f$ do you mean $(Yf) \circ f$ or $Y(f \circ f)$? – Taroccoesbrocco Aug 31 '22 at 09:47
  • @Taroccoesbrocco $Y (f\circ f)$. – creaple Aug 31 '22 at 11:04
  • To answer your question, do you know what $\beta$-reduction or $\beta$-conversion is? – Taroccoesbrocco Aug 31 '22 at 12:48
  • yes. but I'm not sure about the relationship between $\alpha$ conversion, $\beta$ reduction, and the 'equivalence' of expressions. – creaple Aug 31 '22 at 14:32
  • 1
    α, β and possibly η are the generating rules for equivalence. Equivalence is the closure of those rules. Your statement about normal forms is incorrect; it's not an "if and only if." If the two terms have normal forms, and the normal forms are equal, then the two terms are equivalent. But terms without normal forms can also be equivalent to one another. You just cannot 'easily' check by finding normal forms. (Easy in the sense that it is a rote procedure. It might still require a lot of work.) – Dan Doel Aug 31 '22 at 15:12
  • @DanDoel Thanks for your answer, that's really helpful. But in the case of $(Y\ f)$ and $(Y\ (f\circ\ f))$, is there a way to prove that the two terms are equal or not equal? – creaple Sep 01 '22 at 00:13
  • It depends. The rules for equivalence are usually taken to be inductive. So, two expressions are equal if they are related by finitely many steps. However, the sense in which $Y f$ is equivalent to $Y (f \circ f)$ is coinductive. Two unfoldings of $Y f = f (Y f)$ match one unfolding of $Y (f \circ f) = f (f (Y (f \circ f)))$, reducing to the same underlying question. So, if you consider these sorts of infinite simulations, that is how it is done. However, I don't think they are equivalent in the usual, inductive sense. – Dan Doel Sep 01 '22 at 00:52

0 Answers0