# Pure Lambda Calculus in Python (works in both Python2.2+ and Python3)

## The syntax of Python differs slightly from traditional lambdas calculus
# in that application is written f(x) instead of (f x), and a : is used
# instead of . in lambda bindings.

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

# note: it would not be correct to define K as lambda x,y:x, because that's
# using python's built-in pairs.  Every lambda-abstraction takes exactly
# one argument, although that argument can be a tuple.  To be faithful to
# the build-from-scratch approach, we should use Curried functions.

true = K
false = K(I)
ifelse = lambda c:lambda a:lambda b:c(a)(b)
if_else = lambda c:lambda a:lambda b:c(a)(b)(I) # simulates call-by-name
NOT = lambda a:a(false)(true)

print(ifelse(NOT(true))(1)(2)) ### prints 2

# Church numerals 
ZERO = false
ONE = lambda f:lambda x:f(x)
PLUS = lambda m:lambda n:lambda f:lambda x:m(f)(n(f)(x))
TIMES = lambda m:lambda n:lambda f:lambda x:m(n(f))(x)

# linked lists
CONS = lambda a:lambda b:lambda c:c(a)(b)
CAR = lambda p:p(true)
CDR = lambda p:p(false)
NIL = ZERO
ISNIL = lambda p:p(lambda x:lambda y:lambda z:false)(true)

# applicative order FIX combinator for recursive definitions
FIX = lambda m:(lambda x:m(lambda y:x(x)(y)))(lambda x:(m(lambda y:x(x)(y))))

Primes = CONS(2)(CONS(3)(CONS(5)(CONS(7)(CONS(11)(NIL)))))
print(CAR(CDR(Primes)))  ### prints 3, the second prime

### functions to convert Python numerals to Church numerals:

def Church(n):  # converts non-neg integer n to Church numeral
    if (n==0): return ZERO
    elif n>0: return PLUS(ONE)(Church(n-1))
#
def Unchurch(c):  # converts Church numeral c to Python integer:
    return c(lambda y:1+y)(0)
#
## for example, Unchurch(TWO) beta-reduces to
# (lambda f:lambda x:f(f(x)))(lambda y:1+y)(0), which reduces to 1+1+0=2

# Unfortunately, Python cannot print intermediate lambda terms: it does
# does not support "higher order abstract syntax".

C25 = Church(25)  # pure lambda representation of 25
print(Unchurch(C25))  #### prints 25

## pure lambda function to add all numbers in a linked list

SUM = FIX(lambda f:lambda n:if_else(ISNIL(n))(lambda y:ZERO)(
    lambda y:PLUS(CAR(n))(f(CDR(n)))))

L = CONS(Church(1))(CONS(Church(2))(CONS(Church(4))(CONS(Church(8))(NIL))))

ANSWER = SUM(L)
print(Unchurch(ANSWER))  ### prints 15