the topic starts with recursive functions; a typical example is the factorial function F(n); it is easy to implement; for example, we can implement it in python using either def or lambda:

def F(n):
if n == 0:
return 1
else:
return n * F(n-1)

F = lambda n: 1 if n == 0 else n * F(n-1)


but think about this: what if all functions are anonymous? we are not able to use F in its own function body; then how do we express recursion?

## session 0: basic

actually there is a way to express anonymous recursion in lambda calculus; the magic is F = GG; here G is a higher-order function that gives F when applied to itself; we pass G to itself as an argument so that it can emulate recursion; we use the factorial example (notation, use \ for λ):

F   =      \n.(n == 0 ? 1 : n *  F(n-1))        # definition of F
GG  =      \n.(n == 0 ? 1 : n * GG(n-1))        # F=GG
GG  = ( \g.\n.(n == 0 ? 1 : n * gg(n-1)) ) G    # β-reduction
G   =   \g.\n.(n == 0 ? 1 : n * gg(n-1))        # cancel G


now we have G, so we can calculate F as GG:

def exam0():
G = lambda g : (
lambda n : (
1 if n == 0 else n * g(g)(n-1)
))
F = G(G)
assert F(4) == 24


the assert statement passes; this method is working;

before we end this session, we adopt a simplified format when write deductions and proofs; we only write the recursive parts because other parts are verbatim and can be complemented whenever necessary; for example, the above example can be simplified into:

F   =      \n. F(n-1)
GG  =      \n.GG(n-1)
GG  = ( \g.\n.gg(n-1) ) G
G   =   \g.\n.gg(n-1)


## session 1: fancy

this session upgrades the magic F=GG into F=GGGGGGGG; the number of G on the right side can be any integer larger than one (eight in this example); the deductions are similar to the above one, just with more steps:

F          = (                      \n.       F(n-1) )
GGGGGGGG   = (                      \n.GGGGGGGG(n-1) )      # F = GGGGGGGG
GGGGGGGG   = (                   \g.\n.GGGGGGGg(n-1) ) G    # β-reduction
GGGGGGG    = (                   \g.\n.GGGGGGGg(n-1) )      # cancel G
GGGGGGG    = (                \f.\g.\n.GGGGGGfg(n-1) ) G
GGGGGG     = (                \f.\g.\n.GGGGGGfg(n-1) )
GGGGGG     = (             \e.\f.\g.\n.GGGGGefg(n-1) ) G
GGGGG      = (             \e.\f.\g.\n.GGGGGefg(n-1) )
GGGGG      = (          \d.\e.\f.\g.\n.GGGGdefg(n-1) ) G
GGGG       = (          \d.\e.\f.\g.\n.GGGGdefg(n-1) )
GGGG       = (       \c.\d.\e.\f.\g.\n.GGGcdefg(n-1) ) G
GGG        = (       \c.\d.\e.\f.\g.\n.GGGcdefg(n-1) )
GGG        = (    \b.\c.\d.\e.\f.\g.\n.GGbcdefg(n-1) ) G
GG         = (    \b.\c.\d.\e.\f.\g.\n.GGbcdefg(n-1) )
GG         = ( \a.\b.\c.\d.\e.\f.\g.\n.aabcdefg(n-1) ) G
G          = ( \a.\b.\c.\d.\e.\f.\g.\n.aabcdefg(n-1) )

def exam1():
G = lambda a : (
lambda b : (
lambda c : (
lambda d : (
lambda e : (
lambda f : (
lambda g : (
lambda n : (
1 if n == 0 else n * (a)(a)(b)(c)(d)(e)(f)(g)(n-1)
))))))))
F = (G)(G)(G)(G)(G)(G)(G)(G)
assert F(4) == 24


to see F defined this way is correct:

F = (G)(G)(G)(G)(G)(G)(G)(G)
= lambda n : 1 if n == 0 else n * (G)(G)(G)(G)(G)(G)(G)(G)(n-1)   # β-reduction
= lambda n : 1 if n == 0 else n * F(n-1)                          # definition of F


## session 2: fancier

you probably have noticed, in exam1, when we define:

F = (G)(G)(G)(G)(G)(G)(G)(G)


we are setting all of a, …, g to G; so, these variables can be switched between each other; this can also be reasoned from the deductions: β-reductions in the deductions factor out one or more arbitrary G, thus choosing different G to factor out can give a different term as deduction result;

the example below gives another arbitrary combination of a to g; because it has seven variables and eight positions, at least one variable will show in two positions; it is not quite obvious how to remove this duplication; anyway, this method works;

def exam2():
G = lambda a : (
lambda b : (
lambda c : (
lambda d : (
lambda e : (
lambda f : (
lambda g : (
lambda n : (
1 if n == 0 else n * (f)(c)(a)(d)(e)(e)(a)(g)(n-1)  # any combination
))))))))
F = (G)(G)(G)(G)(G)(G)(G)(G)
assert F(4) == 24


## session 3: y combinator

the solutions given in the above sessions do work, but they require we rewrite the function definition by duplicating some variables; for example, in session 0 we have G as:

G = \g.\n.gg(n-1)   # gg, not g


this looks ugly; we wish we can get F from this beautiful G that keeps the original function definition:

G = \g.\n.g(n-1)    # g, not gg


to do so, we introduce the concept of fixed point: a fixed point of a function is a value that is mapped to itself by the function; in other words, if fix f is a fixed point of f, then:

fix f = f(fix f)


to see why fixed points are useful to our problem at hand, we currently have:

F = \n.F(n-1)       # definition of F
G = \g.\n.g(n-1)    # definition of G


we have observations in both directions:

• we know F is a fixed point of G, because:

GF = (\g.\n.g(n-1)) F   # definition of G
= \n.F(n-1)          # β-reduction
= F                  # definition of F

• for any fixed point F' of G, we have:

F' = GF'                # F' is fixed point
= (\g.\n.g(n-1)) F'  # definition of G
= \n.F'(n-1))        # β-reduction


but this means F' = F because F' and F have the same definition (assuming they have the same initial value);

put these together, F and fix G are exactly the same thing; to get F, we just need to get fix G; imagine we have a function Y such that Y G gives fix G, then we can use Y to get F; we do not know this Y yet, but will soon see how to make it;

because F is the fixed point of G, we know F=GF (from definition of fixed point) and F=YG (from definition of Y);

now, recall our magic F=GG; but G already has a different meaning here, so we rename our magic into F=HH; we assume there is a higher-order function H that gives F when applied to itself; then we have these deductions:

F=GF
HH=G(HH)
HH=(\x.G(xx)) H
H =(\x.G(xx))

F=HH
=(\x.G(xx))(\x.G(xx))
=(\g.(\x.g(xx))(\x.g(xx))) G

F=YG

YG=(\g.(\x.g(xx))(\x.g(xx))) G
Y = \g.(\x.g(xx))(\x.g(xx))     # bingo!


this is the famous y combinator;

to see it works correctly, we verify YG=G(YG):

YG=(\g.(\x.g(xx))(\x.g(xx))) G
=    (\x.G(xx))(\x.G(xx))
=  G((\x.G(xx))(\x.G(xx)))
=  G(YG)


this means YG indeed gives a fixed point of G;

cool, let us use this Y to define F:

def exam3():
Y = lambda g : (
(lambda x : g(x(x)))
(lambda x : g(x(x)))
)
G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
F = Y(G)


wait, it does not work; python outputs:

RecursionError: maximum recursion depth exceeded


## session 4: y combinator expanded

we did not expect the failure in the previous session; in fact the y combinator we got in that session is good; the problem is with evaluation order;

there are two types of evaluation orders:

• strict (aka: eager) evaluation requires all function arguments to be evaluated before the function is applied;

• non-strict (aka: lazy) evaluation allows a function to return a result before all arguments are evaluated;

the y combinator only works in a lazy evaluation environment, but python is an eager evaluation environment; the python evaluation of some function arguments lead to infinite loop and exhaust the stack; to find the exact error spot, we have turned the y combinator into a def implementation:

def exam4():
def Y(g):
def A(x):
return g(x(x))
def B(x):
return g(x(x))  # boom!
return A(B)

G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
F = Y(G)


this code is pretty easy to follow, so no explanation here; do some prints to track the control flow if they are helpful;

## session 5: z combinator

the rescue to an eager evaluation environment is the z combinator;

the z combinator is very similar to the y combinator; the difference is some η -reductions:

Y=(\g.(\x.g(   xx ))(\x.g(   xx )))
Z=(\g.(\x.g(\v.xxv))(\x.g(\v.xxv)))


η-reductions do not change function return value, but delay the evaluation of function arguments (because they are now provided in an evaluated form); code below now works correctly:

def exam5():
Z = lambda g : (
(lambda x : g(lambda v : x(x)(v)))
(lambda x : g(lambda v : x(x)(v)))
)
G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
F = Z(G)
assert F(4) == 24


## session 6: z combinator expanded

this session turns the z combinator into a def implementation:

def exam6():
def Z(g):
def A(x):
def C(v):
return x(x)(v)
return g(C)         # lazy
def B(x):
def D(v):
return x(x)(v)
return g(D)         # lazy
return A(B)
G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
F = Z(G)
assert F(4) == 24


here is a stepping trace of the evaluation of F(n) | n = 4:

F(n)                = Z(G)(n)
= A(B)(n)
= G(C)(n) | (C.x=B)
= 1 if n == 0 else n * C(n-1) | (C.x=B)

C(n-1) | (C.x=B)    = B(B)(n-1)
= G(D)(n-1) | (D.x=B)
= 1 if (n-1) == 0 else (n-1) * D(n-2) | (D.x=B)

D(n-2) | (D.x=B)    = B(B)(n-2)
= G(D)(n-2) | (D.x=B)
= 1 if (n-2) == 0 else (n-2) * D(n-3) | (D.x=B)

D(n-3) | (D.x=B)    = B(B)(n-3)
= G(D)(n-3) | (D.x=B)
= 1 if (n-3) == 0 else (n-3) * D(n-4) | (D.x=B)

D(n-4) | (D.x=B)    = B(B)(n-4)
= G(D)(n-4) | (D.x=B)
= 1 if (n-4) == 0 else (n-4) * D(n-5) | (D.x=B)
= 1


## session 7: hybrid combinator (y and z)

those who have step-traced the y combinator failure may realize that only the second part needs a patch in an eager evaluation environment; this produces a hybrid combinator that looks like both y and z:

def exam7():
YZ = lambda g : (
(lambda x : g(x(x)))                # like y combinator
(lambda x : g(lambda v : x(x)(v)))  # like z combinator
)
G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
F = YZ(G)
assert F(4) == 24


## session 8: y8 combinator

in this session we introduce a method to construct an infinite-sized group of fixed-point combinators; the simplest in this group is the y combinator which has been introduced above, others are more complicated; because the combinator can be quite long, we use a non-standard notation ^ for repetitive patterns;

we can construct a combinator for any size greater than 1; the example below constructs a combinator with size 8;

we have:

F = \n.F(n-1)
G = \g.\n.g(n-1)

F=GF
F=YG


we want Y such that:

YG=G(YG)


assume F=HHHHHHHH, then we have HHHHHHHH=G(HHHHHHHH); then we can make the following deductions; we can freely choose any H to factor out in each step, so there are many results other than aabcdefg here:

HHHHHHHH=(                        G(HHHHHHHH))
HHHHHHHH=(                     \g.G(HHHHHHHg)) H
HHHHHHH =(                     \g.G(HHHHHHHg))
HHHHHHH =(                  \f.\g.G(HHHHHHfg)) H
HHHHHH  =(                  \f.\g.G(HHHHHHfg))
HHHHHH  =(               \e.\f.\g.G(HHHHHefg)) H
HHHHH   =(               \e.\f.\g.G(HHHHHefg))
HHHHH   =(            \d.\e.\f.\g.G(HHHHdefg)) H
HHHH    =(            \d.\e.\f.\g.G(HHHHdefg))
HHHH    =(         \c.\d.\e.\f.\g.G(HHHcdefg)) H
HHH     =(         \c.\d.\e.\f.\g.G(HHHcdefg))
HHH     =(      \b.\c.\d.\e.\f.\g.G(HHbcdefg)) H
HH      =(      \b.\c.\d.\e.\f.\g.G(HHbcdefg))
HH      =(   \a.\b.\c.\d.\e.\f.\g.G(aabcdefg)) H
H       =(   \a.\b.\c.\d.\e.\f.\g.G(aabcdefg))

H=(\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))
F=HHHHHHHH
=H^8
=     (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^8
=(\x.((\a.\b.\c.\d.\e.\f.\g.x(aabcdefg))^8)) G

F=YG

Y=(\x.((\a.\b.\c.\d.\e.\f.\g.x(aabcdefg))^8))


now we have got Y; we then verify YG=G(YG);

let _ = (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg)); this _ is actually H, but we use _ to mean it does not need for the proof special properties H may have;

YG=(\x.((\a.\b.\c.\d.\e.\f.\g.x(aabcdefg))^8)) G
=     (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^8 = ________
=     (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))(\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))(\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^6
=     (   \b.\c.\d.\e.\f.\g.G(__bcdefg))                                  (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^6
=     (      \c.\d.\e.\f.\g.G(___cdefg))                                  (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^5
=     (         \d.\e.\f.\g.G(____defg))                                  (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^4
=     (            \e.\f.\g.G(_____efg))                                  (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^3
=     (               \f.\g.G(______fg))                                  (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^2
=     (                  \g.G(_______g))                                  (\a.\b.\c.\d.\e.\f.\g.G(aabcdefg))^1
=     (                     G(________))
=                           G(________)
=                           G(YG)


the simplest one in the group (ie: y combinator) can be called Y2, while this big one with eight variables can be called Y8; compare Y2 and Y8:

Y2=(\x.(  (\a.                  x(aa      ))^2  ))
Y8=(\x.(  (\a.\b.\c.\d.\e.\f.\g.x(aabcdefg))^8  ))

def exam8():
Y8 = lambda x : (
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: ( x((a)(a)(b)(c)(d)(e)(f)(g))))
)
G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
F = Y8(G)   # boom!


as you might have expected, this y8 combinator does not work in python, for the same reason (ie: evaluation order) the y combinator does not work in python;

## session 9: y8 combinator expanded

this session gives def implementation of y8 combinator, and shows where it fails; ok, that was the plan, but when i started writing this session i felt explaining y8 would need too much effort, so i had to downgrade y8 to y4 and explained y4 instead… the explanation is pretty much the code itself;

this session also shows how to patch this y4 combinator into z4 combinator, which works with eager evaluation;

def exam9():

def Y4(x):
def A(a):
def B(b):
def C(c):
return x((a)(a)(b)(c))      # boom!
return C
return B
return (A)(A)(A)(A)

def Z4(x):
def A(a):
def B(b):
def C(c):
def V(v):
return (a)(a)(b)(c)(v)
return x(V)                 # lazy
return C
return B
return (A)(A)(A)(A)

G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
F = Y4(G)   # boom!
F = Z4(G)
assert F(4) == 24


## session 10: z8 combinator

this session patches y8 combinator into z8 combinator, using the same technique as in the previous session (for z4 combinator); in contrast to the previous session, combinators in this session are implemented with lambda not def;

there are three combinators in this session in addition to Y8:

• Z8BRUTAL: a patch abusing η-reductions without much thought;

• Z8: a patch making good (and fewer) use of η-reductions;

• Z8UNROLL: Z8 unrolled;

def exam10():

#Y8=(\x.(  (\a.\b.\c.\d.\e.\f.\g.x(aabcdefg))^8  ))
def Y8(x):
A = (
lambda a : (
lambda b : (
lambda c : (
lambda d : (
lambda e : (
lambda f : (
lambda g : (
x((a)(a)(b)(c)(d)(e)(f)(g))
))))))))
return (A)(A)(A)(A)(A)(A)(A)(A)

def Z8BRUTAL(x):
A = (
lambda a : (
lambda b : (
lambda c : (
lambda d : (
lambda e : (
lambda f : (
lambda g : (
x(
lambda vg: (
lambda vf: (
lambda ve: (
lambda vd: (
lambda vc: (
lambda vb: (
lambda va: (a)(a)(va)
)(b)(vb)
)(c)(vc)
)(d)(vd)
)(e)(ve)
)(f)(vf)
)(g)(vg)
)
))))))))
return (A)(A)(A)(A)(A)(A)(A)(A)

def Z8(x):
A = (
lambda a : (
lambda b : (
lambda c : (
lambda d : (
lambda e : (
lambda f : (
lambda g : (
x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v))
))))))))
return (A)(A)(A)(A)(A)(A)(A)(A)

def Z8UNROLL(x):
return (
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
(lambda a: lambda b: lambda c: lambda d: lambda e: lambda f: lambda g: x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v)))
)

G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
#    F = Y8(G)   # boom!
#    F = Z8BRUTAL(G)
F = Z8(G)
#    F = Z8UNROLL(G)
assert F(4) == 24


## session 11: turing combinator

in addition to the y combinator, there is another important combinator called turing combinator (here denoted by T); as its name implies, it is discovered by alan turing;

deductions (recall our magic T=SS):

Tf=f(Tf)
T=\f.f(Tf)
T=SS
SS=\f.f(SSf)
SS=(\z.\f.f(zzf)) S
S =(\z.\f.f(zzf))
T =(\z.\f.f(zzf))(\z.\f.f(zzf))
=(\x.\y.y(xxy))(\x.\y.y(xxy)) # α-conversion


verify:

TG = (\x.\y.y(xxy))(\x.\y.y(xxy)) G
= (   \y.y(SSy))               G # β-reduction
=        G(SSG)                  # β-reduction
=        G( TG)


as an exercise, we can do fancy turing combinator too if we assume T=SSSSSSSS instead of T=SS; again, the number of S can be any integer larger than one and the choice of variable to factor out in each step is arbitrary:

Tf=f(Tf)
T=\f.f(Tf)
T=SSSSSSSS
SSSSSSSS=(                     \f.f(SSSSSSSSf))
SSSSSSSS=(                  \h.\f.f(SSSSSSShf)) S
SSSSSSS =(                  \h.\f.f(SSSSSSShf))
SSSSSSS =(               \g.\h.\f.f(SSSSSSghf)) S
SSSSSS  =(               \g.\h.\f.f(SSSSSSghf))
SSSSSS  =(            \e.\g.\h.\f.f(SSSSSeghf)) S
SSSSS   =(            \e.\g.\h.\f.f(SSSSSeghf))
SSSSS   =(         \d.\e.\g.\h.\f.f(SSSSdeghf)) S
SSSS    =(         \d.\e.\g.\h.\f.f(SSSSdeghf))
SSSS    =(      \c.\d.\e.\g.\h.\f.f(SSScdeghf)) S
SSS     =(      \c.\d.\e.\g.\h.\f.f(SSScdeghf))
SSS     =(   \b.\c.\d.\e.\g.\h.\f.f(SSbcdeghf)) S
SS      =(   \b.\c.\d.\e.\g.\h.\f.f(SSbcdeghf))
SS      =(\a.\b.\c.\d.\e.\g.\h.\f.f(aabcdeghf)) S
S       =(\a.\b.\c.\d.\e.\g.\h.\f.f(aabcdeghf))
T=SSSSSSSS
=(\a.\b.\c.\d.\e.\g.\h.\f.f(aabcdeghf))^8


the same technique applied to 26 variables gives:

T=SSSSSSSSSSSSSSSSSSSSSSSSSS
S=\a.\b.\c.\d.\e.\f.\g.\h.\i.\j.\k.\l.\m.\n.\o.\p.\q.\s.\t.\u.\v.\w.\x.\y.\z.\r.r(thisisafixedpointcombinator)


as with all turing-like combinators, the last variable (r in this example) is special; all the other 25 variables have equal status;

for similar reason why we patch y combinator into z combinator, turing-like combinators also need patch for eager evaluation:

def exam11():

TY = (
(lambda x : (lambda y : (y(x(x)(y)))))
(lambda x : (lambda y : (y(x(x)(y)))))
)

TZ = (
(lambda x : (lambda y : (y(lambda v: x(x)(y)(v)))))
(lambda x : (lambda y : (y(lambda v: x(x)(y)(v)))))
)

G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
#    F = TY(G)   # boom!
F = TZ(G)
assert F(4) == 24


## session 12: summary

this session gives a summary of y combinators and z combinators;

def exam12():

def Y2(x):
A = (
lambda a : (
x((a)(a))
))
return (A)(A)

def Z2(x):
A = (
lambda a : (
x(lambda v: (a)(a)(v))
))
return (A)(A)

def Y4(x):
A = (
lambda a : (
lambda b : (
lambda c : (
x((a)(a)(b)(c))
))))
return (A)(A)(A)(A)

def Z4(x):
A = (
lambda a : (
lambda b : (
lambda c : (
x(lambda v: (a)(a)(b)(c)(v))
))))
return (A)(A)(A)(A)

def Y8(x):
A = (
lambda a : (
lambda b : (
lambda c : (
lambda d : (
lambda e : (
lambda f : (
lambda g : (
x((a)(a)(b)(c)(d)(e)(f)(g))
))))))))
return (A)(A)(A)(A)(A)(A)(A)(A)

def Z8(x):
A = (
lambda a : (
lambda b : (
lambda c : (
lambda d : (
lambda e : (
lambda f : (
lambda g : (
x(lambda v: (a)(a)(b)(c)(d)(e)(f)(g)(v))
))))))))
return (A)(A)(A)(A)(A)(A)(A)(A)

G = lambda g : (
lambda n : (
1 if n == 0 else n * g(n-1)
))
#    F = Y2(G)   # boom!
#    F = Z2(G)
#    F = Y4(G)   # boom!
#    F = Z4(G)
#    F = Y8(G)   # boom!
F = Z8(G)
assert F(4) == 24


## session 13: racket implementation

the racket language allows lazy evaluation; so we can build some examples to test y combinators that do not work in python; in addition, we test z combinators work with lazy evaluation too;

#lang lazy

;Y2=\x.(  (\a.x(aa))^2  )
(define Y2 (
λ(x)
(
(λ(a) (x (a a)))
(λ(a) (x (a a)))
)
))

;Z2=\x.(  (\a.x(\v.aav))^2  )
(define Z2 (
λ(x)
(
(λ(a) (x (λ(v) ((a a) v))))
(λ(a) (x (λ(v) ((a a) v))))
)
))

;Y4=\x.(  (\a.\b.\c.x(aabc))^4  )
(define Y4 (
λ(x)
(((
(λ(a) (λ(b) (λ(c) (x (((a a) b) c) ))))
(λ(a) (λ(b) (λ(c) (x (((a a) b) c) )))))
(λ(a) (λ(b) (λ(c) (x (((a a) b) c) )))))
(λ(a) (λ(b) (λ(c) (x (((a a) b) c) )))))
))

;Z4=\x.(  (\a.\b.\c.x(\v.aabcv))^4  )
(define Z4 (
λ(x)
(((
(λ(a) (λ(b) (λ(c) (x (λ(v) ((((a a) b) c) v))))))
(λ(a) (λ(b) (λ(c) (x (λ(v) ((((a a) b) c) v)))))))
(λ(a) (λ(b) (λ(c) (x (λ(v) ((((a a) b) c) v)))))))
(λ(a) (λ(b) (λ(c) (x (λ(v) ((((a a) b) c) v)))))))
))

;Y8=\x.(  (\a.\b.\c.\d.\e.\f.\g.x(aabcdefg))^8  )
(define Y8 (
λ(x)
(((((((
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g)))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (((((((a a) b) c) d) e) f) g))))))))))
))

;Z8=\x.(  (\a.\b.\c.\d.\e.\f.\g.x(\v.aabcdefgv))^8  )
(define Z8 (
λ(x)
(((((((
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v)))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v)))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v)))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v)))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v)))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v)))))))))))
(λ(a) (λ(b) (λ(c) (λ(d) (λ(e) (λ(f) (λ(g) (x (λ(v) ((((((((a a) b) c) d) e) f) g) v)))))))))))
))

;main
(define Fact (
;    Y2 (λ(fact) (λ(n) (if (zero? n) 1 (* n (fact (- n 1))))))
;    Y4 (λ(fact) (λ(n) (if (zero? n) 1 (* n (fact (- n 1))))))
Y8 (λ(fact) (λ(n) (if (zero? n) 1 (* n (fact (- n 1))))))
;    Z2 (λ(fact) (λ(n) (if (zero? n) 1 (* n (fact (- n 1))))))
;    Z4 (λ(fact) (λ(n) (if (zero? n) 1 (* n (fact (- n 1))))))
;    Z8 (λ(fact) (λ(n) (if (zero? n) 1 (* n (fact (- n 1))))))
))

(Fact 4)
(Fact 40)


## session 14: build a jet

this session shows how to build a jet with fixed-point combinators; well, it actually builds a fixed-point combinator with jets; the code explains itself (on a wide screen);

(define JET
(lambda(a)
(lambda(b)
(lambda(c)
(lambda(d)
(lambda(e)
(lambda(f)
(lambda(g)
(lambda(h)
(lambda(i)
(lambda(j)
(lambda(k)
(lambda(l)
(lambda(m)
(lambda(n)
(lambda(o)
(lambda(p)
(lambda(q)
(lambda(s)
(lambda(t)
(lambda(u)
(lambda(v)
(lambda(w)
(lambda(x)
(lambda(y)
(lambda(z)
(lambda(r)
(r ((((((((((((((((((((((((((t h) i) s) i) s) a) f) i) x) e) d) p) o) i) n) t) c) o) m) b) i) n) a) t) o) r)))))))))))))))))))))))))))))

(define RUNWAY (((((((((((((((((((((((((JET JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET) JET))


i am not lying: RUNWAY is a fixed-point combinator built with racket jets;