# Lambda calculus

The lambda calculus is a formal system invented by [Alonzo Church](https://www.edgepedia.org/alonzo-church) in which computation is expressed entirely through the definition and application of functions, using three kinds of terms: variables, function abstraction, and function application. Church developed it in the 1930s and used it in 1936 to prove that Hilbert's Entscheidungsproblem, the decision problem, has no algorithmic solution.<sup>[1](https://github.com/akardapolov/software-atlas/blob/main/docs/works/papers/church-1936-lambda.md)</sup> Despite its minimal vocabulary, it computes exactly the same functions as Turing machines, and it remains a foundation of programming language theory and functional programming.<sup>[2](https://www.cs.tau.ac.il/~nachumd/papers/Church-Turing-Theorem.pdf)</sup>

| Key fact | Detail |
|---|---|
| Origin | Alonzo Church, "An Unsolvable Problem of Elementary Number Theory," *American Journal of Mathematics* 58(2), 345–363 (1936)<sup>[1](https://github.com/akardapolov/software-atlas/blob/main/docs/works/papers/church-1936-lambda.md)</sup><sup> • </sup><sup>[3](https://phil415.pbworks.com/f/Church.pdf)</sup> |
| Terms | Variables, abstractions \( \lambda x.M \), and applications \( M\,N \); the pure calculus excludes constants, types, and primitive operators such as + and ×<sup>[4](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html)</sup> |
| Central rule | β-reduction: \( (\lambda x.M)\,N \rhd M[x := N] \), substituting \( N \) for occurrences of \( x \) in \( M \)<sup>[5](https://plato.stanford.edu/archives/spr2022/entries/lambda-calculus/)</sup> |
| Church–Rosser theorem | If a term reduces to two terms, both reduce to a common term; if a normal form exists, it is unique<sup>[6](https://plato.stanford.edu/entries/logic-combinatory/)</sup> |
| Computational power | Turing proved his machines compute exactly the same numeric functions as the lambda calculus; both are equivalent to recursive functions, Markov algorithms, and other universal models<sup>[2](https://www.cs.tau.ac.il/~nachumd/papers/Church-Turing-Theorem.pdf)</sup> |
| Nontermination | The term \( \omega = (\lambda x.x\,x)(\lambda x.x\,x) \) has no normal form; reduction can loop forever<sup>[7](https://theory.stanford.edu/~blynn/lambda/)</sup> |
| Descendants | LISP (John McCarthy), Peter Landin's work, Corrado Böhm's treatment of λ-calculus as a programming language, and typed calculi underlying proof assistants<sup>[8](https://citeseerx.ist.psu.edu/document?doi=959d32cfa6df9299312ba51e2102045e1f25bc18&repid=rep1&type=pdf)</sup><sup> • </sup><sup>[9](https://arxiv.org/abs/0804.3434)</sup> |

## Syntax and terms

A λ-term is built from variables, abstraction \( \lambda x.M \), which binds the variable \( x \) in the body \( M \), and application \( M\,N \), which supplies \( N \) as the argument to the function \( M \). By convention application is left-associative, so \( A\,B\,C \) means \( (A\,B)\,C \), and application binds more tightly than abstraction, so \( \lambda x.A\,B \) means \( \lambda x.(A\,B) \).<sup>[4](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html)</sup> The pure calculus contains nothing else: no numbers, no data structures, no primitive operations. Everything, including booleans, pairs, and natural numbers (encoded as Church numerals), must be constructed from functions alone.<sup>[4](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html)</sup>

## β-reduction and normal forms

Computation in the calculus proceeds by rewriting. The principal rule is β-reduction: an application \( (\lambda x.M)\,N \) contracts to \( M[x := N] \), the body \( M \) with \( N \) plugged in for the occurrences of \( x \).<sup>[5](https://plato.stanford.edu/archives/spr2022/entries/lambda-calculus/)</sup> For example, \( (\lambda x[x])\,a \rhd a \), and if \( x \) and \( y \) are distinct variables, \( (\lambda x[y])\,a \rhd y \).<sup>[5](https://plato.stanford.edu/archives/spr2022/entries/lambda-calculus/)</sup> A term that admits no further β-reduction is in normal form, and this form plays the role of a computed answer.<sup>[7](https://theory.stanford.edu/~blynn/lambda/)</sup>

A second rule, η-reduction, contracts \( \lambda x[M\,x] \) to \( M \) when the variable does not interfere; it identifies a function with the function that applies its argument and does nothing else.<sup>[5](https://plato.stanford.edu/archives/spr2022/entries/lambda-calculus/)</sup>

Not every term reaches a normal form. The self-application \( \omega = (\lambda x.x\,x)(\lambda x.x\,x) \) reduces to itself, so any attempt to normalize it loops forever.<sup>[7](https://theory.stanford.edu/~blynn/lambda/)</sup> This behavior is not a defect: it is what gives the untyped calculus the full power of universal computation, and it is the λ-calculus face of the halting problem.<sup>[10](https://arxiv.org/abs/0801.0882)</sup>

## The Church–Rosser theorem

A single term can contain several redexes, so different reduction orders can lead along different paths. The Church–Rosser theorem, an early result due to Church and [J. Barkley Rosser](https://www.edgepedia.org/j-barkley-rosser) (1936), states that if \( M \) reduces to both \( N \) and \( P \), then there is a term \( Q \) to which both \( N \) and \( P \) reduce.<sup>[6](https://plato.stanford.edu/entries/logic-combinatory/)</sup> Viewed computationally, the theorem means that when a term is reduced through a sequence of steps, the outcome reached at the end does not depend on which order those steps are performed in, provided a normal form is reached at all; uniqueness holds only in that case.<sup>[6](https://plato.stanford.edu/entries/logic-combinatory/)</sup>

The theorem has two further consequences. First, it implies the consistency of the plain λ-calculus, the theory \( \lambda \) of equations between λ-terms, in the sense that not all equations are derivable.<sup>[11](https://plato.sydney.edu.au/entries////////////////////////////////////////////////////////////////////////lambda-calculus/)</sup> Second, it underlies parallelism in functional languages: because any two evaluation orders converge, independent redexes can be reduced concurrently without changing the result.<sup>[12](https://arxiv.org/abs/2601.13040)</sup>

## Evaluation strategies

Choosing which redex to reduce first matters in practice. Normal-order reduction always reduces the leftmost outermost redex first; the normalization theorem guarantees that if a normal form exists, repeatedly reducing the leftmost redex eventually reaches it.<sup>[7](https://theory.stanford.edu/~blynn/lambda/)</sup> Applicative-order reduction instead reduces the leftmost innermost redex, evaluating arguments before the function is applied; this corresponds to call-by-value parameter passing.<sup>[4](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html)</sup>

Each strategy has a weakness. Normal order can be inefficient, because an argument used many times in a function body is re-evaluated at each use. Applicative order is efficient but may fail to terminate on an expression that does have a normal form.<sup>[4](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html)</sup> Call-by-need parameter passing combines the two: the argument is evaluated only when first used, as in call-by-name, but the result is saved and reused afterward, so in the absence of side effects it computes the same values as call-by-name, usually faster.<sup>[4](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html)</sup> This is the strategy of lazy functional languages such as Haskell.<sup>[7](https://theory.stanford.edu/~blynn/lambda/)</sup>

## Computability and the Church–Turing thesis

Church proposed his thesis in 1935 and 1936: real-world calculation can be done using the lambda calculus, which is equivalent to using general recursive functions.<sup>[13](https://mathworld.wolfram.com/Church-TuringThesis.html)</sup> Turing then proved that his machines compute exactly the same numeric functions as the lambda calculus, and Stephen Kleene combined the two claims into what is now called the [Church–Turing thesis](https://www.edgepedia.org/church-turing-thesis).<sup>[2](https://www.cs.tau.ac.il/~nachumd/papers/Church-Turing-Theorem.pdf)</sup> Turing machines, the lambda calculus, Gödel's recursive functions, Markov algorithms, Post's string systems, Minsky's counter machines, random access machines, and [term rewriting systems](https://www.edgepedia.org/term-rewriting-system) all compute the same total and partial functions.<sup>[2](https://www.cs.tau.ac.il/~nachumd/papers/Church-Turing-Theorem.pdf)</sup>

Church's 1936 paper used this machinery to settle Hilbert's Entscheidungsproblem negatively: there is no general algorithmic procedure that determines whether an arbitrary mathematical statement is true or false. He showed that certain problems expressible in the λ-calculus have no algorithmic solution, publishing shortly before Turing's independent proof.<sup>[1](https://github.com/akardapolov/software-atlas/blob/main/docs/works/papers/church-1936-lambda.md)</sup> His proof exploited the equivalence of recursiveness and λ-definability, which he established himself.<sup>[14](https://plato.stanford.edu/archives/spr2023/entries/church/supplementA.html)</sup>

## Types and logic

The untyped calculus can encode paradoxical self-application, so a natural refinement is to assign types. The simply-typed lambda calculus, and its extensions with polymorphism and type inference, form a core subject of courses and research on programming language theory, together with the Curry–Howard isomorphism, which reads programs as proofs and types as propositions.<sup>[9](https://arxiv.org/abs/0804.3434)</sup> In dependently typed λ-calculi, proofs themselves are terms, and this representation underlies interactive theorem provers.<sup>[15](https://arxiv.org/abs/2607.12654)</sup> Typed calculi also connect to denotational semantics and to weak and strong normalization, the study of which reduction sequences terminate.<sup>[9](https://arxiv.org/abs/0804.3434)</sup>

A closely related system is combinatory logic, which removes variables altogether by rewriting with constant combinators such as \( \mathbf{S} \) and \( \mathbf{K} \); the two systems were developed in parallel through the 1920s and 1930s and share the Church–Rosser property.<sup>[6](https://plato.stanford.edu/entries/logic-combinatory/)</sup><sup> • </sup><sup>[8](https://citeseerx.ist.psu.edu/document?doi=959d32cfa6df9299312ba51e2102045e1f25bc18&repid=rep1&type=pdf)</sup>

## Influence on programming languages

The path from Church's formalism to real languages runs through several landmarks documented in the history by Felice Cardone, a researcher in lambda-calculus history and formal methods, and J. Roger Hindley, emeritus professor of mathematics at Swansea University: John McCarthy's LISP, Peter Landin's analysis of programming languages in λ-calculus terms, and [Corrado Böhm](https://www.edgepedia.org/corrado-bohm)'s demonstration of the λ-calculus as a programming language in its own right.<sup>[8](https://citeseerx.ist.psu.edu/document?doi=959d32cfa6df9299312ba51e2102045e1f25bc18&repid=rep1&type=pdf)</sup> Modern compilers continue to work with λ-shaped intermediate forms; the [Glasgow Haskell Compiler](https://www.edgepedia.org/glasgow-haskell-compiler), for example, performs late lambda lifting, transforming locally defined functions into top-level functions whose free variables become extra parameters.<sup>[16](https://downloads.haskell.org/ghc/9.12.4.20260713/docs/libraries/ghc-9.12.4.20260713/GHC-Stg-Lift.html)</sup> Research has also compiled λ-calculus directly to parallel digital logic, exploiting the Church–Rosser theorem to abandon serial imperative execution.<sup>[12](https://arxiv.org/abs/2601.13040)</sup>

## References

1. [Alonzo Church (1936). An Unsolvable Problem of Elementary Number Theory, summary, software-atlas](https://github.com/akardapolov/software-atlas/blob/main/docs/works/papers/church-1936-lambda.md)
2. [Nachum Dershowitz and Yuri Gurevich. A Proof of the Church-Turing Thesis](https://www.cs.tau.ac.il/~nachumd/papers/Church-Turing-Theorem.pdf)
3. [Alonzo Church (1936). An Unsolvable Problem of Elementary Number Theory, American Journal of Mathematics 58(2), 345–363](https://phil415.pbworks.com/f/Church.pdf)
4. [Lambda Calculus, CS 704 lecture notes, University of Wisconsin–Madison](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/1.LAMBDA-CALCULUS.html)
5. [The Lambda Calculus, Stanford Encyclopedia of Philosophy (Spring 2022 edition)](https://plato.stanford.edu/archives/spr2022/entries/lambda-calculus/)
6. [Combinatory Logic, Stanford Encyclopedia of Philosophy](https://plato.stanford.edu/entries/logic-combinatory/)
7. [Lambda Calculus, Brett Blynn, Stanford theory group](https://theory.stanford.edu/~blynn/lambda/)
8. [Felice Cardone and J. Roger Hindley (2006). History of Lambda-calculus and Combinatory Logic, Swansea University MRRS-05-06](https://citeseerx.ist.psu.edu/document?doi=959d32cfa6df9299312ba51e2102045e1f25bc18&repid=rep1&type=pdf)
9. [Lecture notes on the lambda calculus, arXiv:0804.3434](https://arxiv.org/abs/0804.3434)
10. [Call-by-value Termination in the Untyped lambda-calculus, arXiv:0801.0882](https://arxiv.org/abs/0801.0882)
11. [The Lambda Calculus, Stanford Encyclopedia of Philosophy (mirror copy)](https://plato.sydney.edu.au/entries////////////////////////////////////////////////////////////////////////lambda-calculus/)
12. [CPU-less parallel execution of lambda calculus in digital logic, arXiv:2601.13040](https://arxiv.org/abs/2601.13040)
13. [Church-Turing Thesis, Wolfram MathWorld](https://mathworld.wolfram.com/Church-TuringThesis.html)
14. [Alonzo Church: A. Church on Computability, Stanford Encyclopedia of Philosophy (Spring 2023 supplement)](https://plato.stanford.edu/archives/spr2023/entries/church/supplementA.html)
15. [Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants, arXiv:2607.12654](https://arxiv.org/abs/2607.12654)
16. [GHC.Stg.Lift: Late lambda lifting in STG, GHC 9.12 documentation](https://downloads.haskell.org/ghc/9.12.4.20260713/docs/libraries/ghc-9.12.4.20260713/GHC-Stg-Lift.html)

---
*Topic: Encyclopedia › Physical world and mathematics › Mathematics and statistics › Logic and discrete mathematics › Formal logic and foundations › Logical calculi and logical syntax › Lambda calculus and type theory › Untyped lambda calculus*

*Initially written Sep 17, 2026 · Reviewed: Oct 15, 2026 · Edited: Oct 15, 2026 · Last review: Oct 15, 2026*

*Copyright 2026 EdgeChat AI, a subsidiary of Biostate AI.*

License: Edgepedia Community License 1.0, https://www.edgepedia.org/edgepedia/license