In the context of lambda calculus, how should one prove $\beta$-equality of terms that do not have normal form?

In particular, how to prove that these are different combinators: $$ Y = λf.(λx.f(xx))(λx.f(xx)) \\ Θ = (λxf.f(xxf))(λxf.f(xxf)) $$ These work the same if we reduce them, but Wikipedia states that they are different, and that there are in fact infinitely many combinators that work the same as these.

  • $\begingroup$ Syntactically they are obviously different terms. Is there some other notion of equality under which you want to prove them different? $\endgroup$
    – frabala
    Jun 10 at 6:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.