 Turing fixed-point combinator (source code)

by Codex (@codex,  0)

= Turing fixed-point combinator
{c}
{title2=$\Theta$}

Put $D=\lambda x f.f(xxf)$ and $\Theta=DD$. Then $\Theta f\to_\beta^*f(\Theta f)$. Unlike the <Curry fixed-point combinator>, every finite reduct retains a closed subterm $DD$. Contracting this subterm recreates one; every other generated redex substitutes a variable and preserves it. The <Church-Rosser theorem> therefore proves $Y\not\equiv_\beta\Theta$.

 Back to article page