Source file for "Lambda Calculus from the Ground Up"

lambda-calculus.py

# Source file for my blog "Lambda Calculus from the Ground Up"
# https://blog.ruo-chen.wang/r/10 (zh_CN)

# Bool
def TRUE(x):
    return lambda y: x

def FALSE(x):
    return lambda y: y

def NOT(x):
    return x(FALSE)(TRUE)

def AND(x):
    return lambda y: x(y)(x)

def OR(x):
    return lambda y: x(x)(y)

# Numbers
ZERO = lambda f: lambda x: x
ONE = lambda f: lambda x: f(x)
TWO = lambda f: lambda x: f(f(x))
THREE = lambda f: lambda x: f(f(f(x)))
FOUR = lambda f: lambda x: f(f(f(f(x))))
def toint(n):
    return n(lambda x: x + 1)(0)

# Add and multiply
SUCC = lambda n: lambda f: lambda x: f(n(f)(x))
ADD = lambda x: lambda y: y(SUCC)(x)
MUL = lambda x: lambda y: lambda f: y(x(f))

# Pairs
CONS = lambda a: lambda b: (lambda s: s(a)(b))
CAR = lambda p: p(TRUE)
CDR = lambda p: p(FALSE)

# Subtraction
T = lambda p: CONS(SUCC(CAR(p)))(CAR(p))
PRED = lambda n: CDR(n(T)(CONS(ZERO)(ZERO)))
SUB = lambda x: lambda y: y(PRED)(x)

# Is zero
ISZERO = lambda n: n(lambda _: FALSE)(TRUE)

# Lazy evaluation
L_TRUE = lambda x: lambda y: x()
L_FALSE = lambda x: lambda y: y()
L_ISZERO = lambda n: n(lambda _: L_FALSE)(L_TRUE)

# Y combinator
Y = lambda f: (lambda x: f(lambda z: x(x)(z)))(lambda x: f(lambda z: x(x)(z)))
FACT = Y(lambda f: lambda n: L_ISZERO(n)(lambda: ONE)(lambda: MUL(n)(f(PRED(n)))))