Curry fixed-point combinator (source code)

= Curry fixed-point combinator
{c}
{title2=$Y$}

With $A_f=\lambda x.f(xx)$, the <combinator> $Y=\lambda f.A_fA_f$ satisfies $Yf\equiv_\beta f(Yf)$. Every finite reduct of $Y$ is, up to <alpha equivalence>, $\lambda f.f^n(A_fA_f)$: the remaining copy of $A_fA_f$ is its only <beta-redex>.