Computability
Computation Models: Lambda Calculus and Combinators
Haskell, Clojure, Scala, Erlang - all functional languages are built on ideas nearly 100 years old. Church's lambda calculus from 1936 is the mathematical foundation of every map, filter, and reduce. To understand λ-calculus is to understand computation itself.
- Haskell, ML, OCaml - direct implementations of λ-calculus
- JavaScript: arrow functions = λ-abstractions
- React hooks are based on closures (λ-abstractions)
- Compilers: GHC Core = extended λ-calculus
Lambda Calculus: Computation Without Data
**Lambda calculus** (λ-calculus) is a minimal formal system for computation, invented by Church in the 1930s. It contains only three constructs: variable, abstraction (λx.M), and application (M N).
**Church-Turing Thesis:** λ-calculus and the Turing Machine are computationally equivalent. Any computation expressible in one is expressible in the other. This is the most fundamental statement in the theory of computation.
What does (λx. λy. y) a b evaluate to?
Church Encoding: Numbers from Functions
**Church numerals** are an encoding of natural numbers in λ-calculus. The number n is represented as applying a function n times. This demonstrates that λ-calculus is Turing-complete without any built-in data types.
**Predecessor is non-trivial:** Computing the predecessor (n-1) in λ-calculus is not obvious. Kleene needed time to find the solution. This shows that despite Turing-completeness, some computations in λ-calculus require ingenuity.
A Church numeral n represents n as:
S, K, I Combinators
**Combinatory logic** is a variable-free system using only combinators. Schönfinkel (1920) and Curry showed that just two combinators, S and K, are sufficient for all computation.
**Unlambda:** There is an esoteric programming language called Unlambda, based entirely on S, K, I. Any algorithm is expressible in it. This is a practical proof of the completeness of combinatory logic.
S, K, I combinators are a mathematical curiosity with no practical use. Real programs are written in assembly, C, Python, not two-letter calculi.
SKI combinators are Turing-complete and sit at the foundation of point-free style in Haskell, lambda lifting in compilers, and supercombinators in the GHC STG machine. Every closure in a functional language is internally translated through combinators.
Surface simplicity of notation is confused with practical irrelevance. In reality SKI is a normal form for an abstract machine: GHC performs lambda lifting during compilation, converting local functions into supercombinators because they optimize better without captured environment. Nobody writes two-letter programs by hand, but the compiler does.
What does K x y equal in combinatory logic?
Key Takeaways
- λ-calculus: three constructs (variable, abstraction, application) - Turing-complete
- β-reduction: computation = substituting the argument
- Church numerals: natural numbers as n-fold function applications
- S, K combinators: sufficient for all computation without variables
- Church-Turing Thesis: λ-calculus ≡ Turing Machine
Related Topics
Lambda calculus is the theoretical foundation of functional languages.
- Turing Machine — Equivalence by the Church-Turing Thesis
- Computability in Practice — Type systems and λ-calculus are intertwined
Вопросы для размышления
- Can you implement recursion in λ-calculus if functions have no names? (Hint: Y-combinator)
- Why do all programs terminate in Simply Typed Lambda Calculus? What is lost when types are added?
- What is the practical significance of functional languages being based on λ-calculus?
Связанные уроки
- comp-01 — Turing machine - the starting point for comparison with lambda calculus
- comp-07 — Automata theory shows weaker models of computation
- comp-15 — Kolmogorov complexity builds on the notion of computable function
- alg-01-big-o — Lambda reduction and Big O: different languages for the same idea of resource consumption
- fl-18-turing-machine