Textbook of AI

The lambda calculus is a formal system invented by Alonzo Church in the early 1930s as a foundation for mathematics. It has just three constructs: variables (x, y, z), abstraction (λx. M, an anonymous function whose parameter is x and whose body is M), and application (M N, applying function M to argument N). Computation proceeds by β-reduction: (λx. M) N reduces to M with every free occurrence of x replaced by N.

Despite its minimalism the lambda calculus is Turing-complete. Every computable function can be expressed as a lambda term. Numerals, booleans, lists, recursion (via the Y-combinator) and arbitrarily complex data structures are all definable. The Church–Turing thesis was first established by showing the equivalence of lambda-definable functions with Turing-machine-computable functions and with general recursive functions.

The lambda calculus is the direct ancestor of every functional programming language, LISP (1958), Scheme, ML, Haskell, OCaml, F#, Clojure , and through them of features now ubiquitous in mainstream languages: anonymous functions (lambdas in Python, Java, JavaScript, C++), closures, first-class functions, and let-bindings. Type-theoretic extensions (the simply-typed lambda calculus, System F, the calculus of constructions) underpin modern proof assistants Coq, Lean and Agda.

In AI, the lambda calculus is the substrate of much symbolic reasoning, of program-synthesis approaches to inductive learning, and of the type theories that ground modern formal verification of neural-network properties.