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.
By extending the λ-calculus to allow for infinite λ-terms and infinite reductions. Then you may assert that both $Y f$ and $Θ f$ have $f(f(f(⋯)))$ as their normal form and, thus, that $$Y = λf·Yf = λf·f(f(f(⋯))) = λf·Θf = Θ.$$ Going further, in fact, defining $U = λxλy·y(xy)$, we also have $$UY = λf·UYf = λf·f(Yf) = λf·Yf = Y.$$ Similarly, $UΘ = Θ$.
Therefore, allowing for infinite λ-terms, you have $Y = U(U(U(⋯)))) = Θ$. Thus, it also follows that $Y U = Y$ and $Θ U = Θ$.
Lots of references exist, now, on the infinitary λ-calculus. Here are a few, in the field: Infinitary lambda calculus, A New Coinductive Confluence Proof For Infinitary Lambda Calculus [PDF], Infinitary Rewriting Coinductively, All the λ-Terms are Meaningful for the Infinitary Relational Model, just for starters. I'm getting close to implementing it in the combinator cruncher Combo I put up on GitHub, now that I have a better understanding of how to convert them to (likewise infinitary) combinators. With the syntax that I've been using (by hand) the normal forms would just be $$Yf = x:f x = f(f(f(⋯))),\quad Y = x: U x = U(U(U(⋯)))),$$ to express the respective infinite terms in finite form.
