# 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)```

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