Skip to content

Instantly share code, notes, and snippets.

@weirane
Last active Apr 20, 2021
Embed
What would you like to do?
Source file for "Lambda Calculus from the Ground Up"
# 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)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment