# Programming in pure lambda calculus, or at least as pure as lambda terms
# are included in python

# Pure combinators in python:

I = lambda x:x
K = lambda x:lambda y:x
S = lambda x:lambda y:lambda z: x(z)(y(z))

# In terms of notation, application (M N) in python is M(N).
# Note that K is not the same as lambda x,y:x  which expects both parameters
# together as a pair.  So the (K A B) is written K(A)(B) in python, not
# K(A,B)!   This is called Currying.

# does SKI reduce to I?

SKI = S(K)(I)
print SKI(4)  # should print 4, same as I(4)

### BOOLEANS ARE ALIVE!  (cheat by using pairs for convenience)
T = K  # true
F = K(I)  # false
IFA = lambda x,y,z: x(y)(z)
IFN = lambda x,y,z: x(y)(z)()
And = lambda x,y: IFA(x)(y)(F)
Or = lambda x,y: IFA(x)(T)(y)
Not = lambda x: IFA(x)(F)(T)

# applicative order Y (fixed point) combinator:

Fix = lambda P:(lambda x:P(lambda y:y(x(x))))(lambda x:P(lambda y:y(x(x))))

# linked lists
CONS = lambda a,b:(lambda c:IFA(c)(a)(b))
CAR = lambda m:m(T)
CDR = lambda m:m(F)
NIL = I   # anything

M = CONS(2,CONS(4,CONS(6,NIL)))
print CAR(CDR(M))