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!