An Interesting Combinator

A fixpoint operator F is such that:

ie. F = λf.f(Ff)

ie. F is a fixpoint of λF.λf.f(Ff)

ie. fixpoints are fixpoints of M = λx.λy.y(xy)

Church’s Y operator is a fixpoint operator:

Y = λf.(λx.f(xx))(λx.f(xx))
[Yf = (λx.f(xx))(λx.f(xx)) [beta]
= f((λx.f(xx))(λx.f(xx))) [beta]
= f(Yf) [subst of equals]]

Let’s apply Y to M and call the result T:

T = YM = (λx.M(xx))(λx.M(xx))
= (λx.λy.y(xxy))(λx.λy.y(xxy)) [since λx.M(xx) = λx.λy.y(xxy)]

T is the Turing fixpoint combinator. Isn’t that strange? No doubt there is some deep reason behind this, but what it might be I have no idea. Perhaps it’s related to the fact that Yf needs substitution of equals to show equivalence with f(Yf), whereas T(f) directly reduces to f(Tf):

Tf = (λx.λy.y(xxy))Bf [def]
= f(BBf) [beta]
= f(Tf) [def]


---