Church numerals in Python

church.py

#! /usr/bin/python
#
# Church numerals in Python.
# See http://en.wikipedia.org/wiki/Church_encoding
#
# Vivek Haldar <[email protected]>

zero = lambda f: lambda x: x

# Compute the successor of a Church numeral, n.
# Apply function one more time.
succ = lambda n: lambda f: lambda x: f(n(f)(x))

one = succ(zero)

# Add two Church numerals, n, m.
add = lambda m: lambda n: lambda f: lambda x: n(f)(m(f)(x))

# Multiply two Church numerals, n, m.
mult = lambda m: lambda n: lambda f: lambda x: n(m(f))(x)

# Exponentiation: n^m
exp = lambda m: lambda n: n(m)

# Convert a Church numeral into a concrete integer.
# n = 0, f = (add 1 to a number)
plus1 = lambda x: x + 1
church2int = lambda n: n(plus1)(0)

# Convert a concrete integer into a church numeral.
def int2church(i):
    if i == 0:
        return zero
    else:
        return succ(int2church(i - 1))


print 'church2int(zero) = ', church2int(zero)
print 'church2int(succ(zero)) = ', church2int(succ(zero))
print 'church2int(one) = ', church2int(one)
print 'church2int(succ(one)) = ', church2int(succ(one))
print 'church2int(succ(succ(one))) = ', church2int(succ(succ(one)))
print 'church2int(succ(succ(succ(one)))) = ', church2int(succ(succ(succ(one))))
print 'church2int(add(one)(succ(one))) = ', church2int(add(one)(succ(one)))
print 'church2int(add(succ(one))(succ(one))) = ', church2int(add(succ(one))(succ(one)))
print 'church2int(mult(succ(one))(succ(one))) = ', church2int(mult(succ(one))(succ(one)))
print 'church2int(exp(succ(one))(succ(one))) = ', church2int(exp(succ(one))(succ(one)))
print '-----'
print 'church2int(int2church(0)) = ', church2int(int2church(0))
print 'church2int(int2church(1)) = ', church2int(int2church(1))
print 'church2int(int2church(111)) = ', church2int(int2church(111))

c232 = int2church(232)
c421 = int2church(421)
print 'church2int(mult(c232)(c421)) = ', church2int(mult(c232)(c421))
print '232 * 421 = ', 232 * 421


c2 = int2church(2)
c10 = int2church(10)
print 'church2int(exp(c2)(c10) = ', church2int(exp(c2)(c10))
print '2 ** 10 = ', 2 ** 10

subtraction?

# Kleene's predecessor
pred = lambda n: lambda f: lambda x: n (lambda g: lambda h: h (g (f))) (lambda y: x) (lambda x: x)

# Subtraction of Church numerals
minus = lambda n: lambda m: m (pred) (n)