How to show beta equivalence of property of Y combinator

Question

How to show that $\underline{Y}f =_{\beta} f(\underline{Y}f)$ where $\underline{Y}$ is the usual Y combinator?

Thanks.

Answer 1

I'm assuming that by "the usual $Y$ combinator" you mean Curry's fixed point combinator:

$$ Y = \lambda f . (\lambda x . f (x x)) (\lambda x. f(x x)) $$

The property $Y F \equiv_\beta F(Y F)$ can be proven as follows:

$$\begin{aligned} YF &\equiv_\beta^\star (\lambda x . F (x x)) (\lambda x. F(x x)) & (1)\\ &\equiv_\beta^\star F ((\lambda x . F (x x)) (\lambda x. F(x x)))& (2)\\ &\equiv F(YF)& (3) \end{aligned}$$

Where $\equiv_\beta^\star$ is the transitive and reflexive closure of the beta-reduction.

1. The $Y$ combinator is applied to $F$
2. The recursion happens; the first $(\lambda x. F(x x))$ is applied to the second, obtaining exactly the expression from (1), but "wrapped" inside an $F$.
3. Since what we had before was equivalent to $YF$, the result is $F(YF)$.