Fixed-point combinators

gistfile1.txt

-----------------------------------------------------------------
A = £xy.y(xxy)
T = AA

for any term F:
TF = AAF 
   = (£xy.y(xxy)) (£xy.y(xxy)) F
   = (£y.y( (£xy.y(xxy)) (£xy.y(xxy)) y)) F
   = F( (£xy.y(xxy)) (£xy.y(xxy)) F)
   = F( A A F)
   = F(TF)

TF is a fixed point of F
therefore T is a fixed-point combinator (Turing)
-----------------------------------------------------------------
Y = £f.(£x.f(x x)) (£x.f(x x))

for any term F:
YF = £y.((£x.y(x x)) (£x.y(x x))) F
   = (£x.F(x x)) (£x.F(x x))
   = F((£x.F(x x)) (£x.F(x x)))
   = F(YF)

YF is a fixed point of F
therefore Y is a fixed-point combinator (Haskell-Curry)
-----------------------------------------------------------------
Z = £f.(£x.f(£v.((x x)v))) (£x.f(£v.((x x)v)))
with (£v.((x x)v)) equivalent to (x x)

For call-by-value languages, we need to eta-expand the self-applications (x x) inside the combinator, resulting in the call-by-value Y combinator (also called the Z combinator).