Church encoding

Summary

Church encoding represents data such as natural numbers and truth values by terms of the pure lambda calculus. The number $n$ becomes the function that applies its first argument $n$ times to its second argument. Arithmetic operations then become lambda terms, and computation becomes beta reduction. It shows that the lambda calculus, which has only functions, can express all computable functions on the natural numbers.