Lambda calculus

Lambda calculus is a simple system of computation introduced by Alonzo Church. in which functions, and the operations of abstraction and application, act as primitive operations and objects. Natural numbers can be encoded in the lambda calculus using a system known as Church numerals. It's been proven that lambda calculus and Turing machines are able to compute the same processes, which led to the independently formulated Church-Turing thesis that all Turing-complete methods of computation are equivalent.

John Tromp has invented the system of binary lambda calculus, an extremely compact and efficient encoding of lambda calculus, which he used to define a variant of Kleene's O, and used it to calculate the fundamental sequence of \(\omega_1^{\mathrm{CK}}\).