matthew arcus

My Favourite Combinator

A fixpoint operator F is such that:

Ff = f(Ff)

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)

M is my favourite combinator.

[As an aside, let’s do that constructive type theory thing and prove it as a theorem:

x: (A->B)->A
y: A->B
xy: A
y(xy): B
M: ((A->B)->A)->((A->B)->B) (MP applied twice)

Phew, glad that checks out]

Church’s Y operator is:

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]]

Apply Y to M:

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

T is the Turing fixpoint combinator. Now isn’t that weird? No doubt there is some deep reason behind this, but what it might be I have no idea. Perhaps it’s down to the well-known 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]

One up for Turing there!