Integer arithmetic in lambda calculus

Integers are represented in lambda calculus by the Church numerals. Zero is represented by the lambda expression λfx.x, and other integers are generated by the applying successor function λnfx.f(nfx) to an existing integer n. In other words, n is represented by λfx.f(f(...f(fx)..)) where there are n fs on the right.

Addition can be performed using the lambda expression λmnfx.(mf)(nfx). This applies f to x n times, and then another m times.

Multiplication is also easy, using the lambda expression λmnf.m(nf). This applies fn m times to x.

Even exponentiation is easy, using the lambda expression λmn.nm. This is more difficult to understand than the previous two expressions. Remember that nmfx means ((nm)f)x. This is equivalent to f^m^...^mx, which is f^(m^n)x.

The predecessor function is defined to return the integer before n, unless n is zero in which case it returns zero. This can be accomplished with the lambda expression n(λag.(a(λbc.c))(successor(a(λbc.c))))(λg.00)(λab.a), where ‘successor’ is the successor function, and 0 represents the zero expression. This is not as complicated as it looks. It applies n times a function that maps (x,y) to (y,y+1), to the pair (0,0), resulting in a pair (n-1,n), from which we take the left number, n-1.

Subtraction of n from m is accomplished using the lambda expression λmn.n predecessor m, where ‘predecessor’ is the predecessor function.

Where now?

Found this useful? Share it:

Also in Lambda calculus: