Lambda Calculus Paradigm

Using Church Numerals

See also:

• https://gist.github.com/JayDugger/2438955

• https://rosettacode.org/wiki/Church_numerals

• https://github.com/orsinium-labs/python-lambda-calculus/

Auxiliary Functions

church_to_int = lambda n: n(lambda x: x + 1)(0)

zero = lambda f: lambda x: x

assert church_to_int(zero) == 0

successor_church = lambda n: lambda f: lambda x: f(n(f)(x))

assert church_to_int(successor_church(zero)) == 1


int_to_church = lambda n: zero if n == 0 else successor_church(int_to_church(n - 1))

assert church_to_int(int_to_church(0)) == 0
assert church_to_int(int_to_church(10)) == 10


first_int = 5
second_int = 2

first_church = int_to_church(first_int)
second_church = int_to_church(second_int)

Predecessor and Successor

successor_church = lambda n: lambda f: lambda x: f(n(f)(x))

assert church_to_int(successor_church(zero)) == 1

assert church_to_int(successor_church(int_to_church(0))) == 1
assert church_to_int(successor_church(int_to_church(10))) == 11

Addition

addition_church = lambda m: lambda n: lambda f: lambda x: n(f)(m(f)(x))

assert church_to_int(addition_church(zero)(zero)) == 0
assert church_to_int(addition_church(first_church)(second_church)) == first_int + second_int

Multiplication

multiplication_church = lambda m: lambda f: lambda x: m(f(x))

assert church_to_int(multiplication_church(int_to_church(0))(int_to_church(5))) == 0
assert church_to_int(multiplication_church(int_to_church(5))(int_to_church(0))) == 0
assert church_to_int(multiplication_church(int_to_church(5))(int_to_church(1))) == 5
assert church_to_int(multiplication_church(int_to_church(1))(int_to_church(5))) == 5
assert church_to_int(multiplication_church(first_church)(second_church)) == first_int * second_int

Exponentiation

exponentiation_church = lambda m: lambda n: n(m)

assert church_to_int(exponentiation_church(int_to_church(5))(int_to_church(0))) == 1
assert church_to_int(exponentiation_church(int_to_church(5))(int_to_church(1))) == 5
assert church_to_int(exponentiation_church(first_church)(second_church)) == first_int ** second_int