Hilbert and Ackermann's Entscheidungsproblem asked whether there is a mechanical procedure that, given any sentence of first-order logic, always determines whether that sentence is logically valid. But it immediately raises a foundational question:
What exactly counts as a mechanical procedure?
In the 1930s, several researchers proposed mathematically precise answers. Alan Turing described computation using what are now called Turing machines. Alonzo Church used lambda-definable functions and general recursive functions. Church and Turing independently proved that the Entscheidungsproblem has no such decision procedure (Church 1936a, 1936b; Turing 1936).
The formalisms look very different. A Turing machine manipulates symbols on a tape according to a finite table of instructions. The lambda calculus treats computation as the rewriting of symbolic expressions. Nevertheless, they determine the same class of computable functions. This agreement is important evidence for the Church–Turing thesis:
Every effectively calculable function is computable by a Turing machine or, equivalently, lambda-definable.
This is a thesis connecting the informal idea of “effective calculability” to a mathematical definition. It is not an ordinary theorem because one side of the proposed identification is informal. What can be proved is that the precise models simulate one another (Church 1936a; Turing 1936; Kleene 1936).
The lambda calculus begins with an extremely small grammar. Terms are generated by three rules:
- Variable: if $x$ is a variable, then $x$ is a term.
- Abstraction: if $t$ is a term, then $\lambda x.t$ is a term representing a function with parameter $x$ and body $t$.
- Application: if $t$ and $s$ are terms, then $t\;s$ is a term representing application of $t$ to $s$.
Application associates to the left, so $f\;x\;y$ means $(f\;x)\;y$. An abstraction's body extends as far right as possible, so $\lambda x.\lambda y.x$ means $\lambda x.(\lambda y.x)$.
For example, $\lambda x.\lambda y.x$ takes $x$ and returns a function that ignores $y$ and returns $x$:
$$(\lambda x.\lambda y.x)\;a\longrightarrow_\beta\lambda y.a.$$The reduction step is beta-reduction:
$$(\lambda x.t)\;s\longrightarrow_\beta t[x:=s],$$where $t[x:=s]$ means capture-avoiding substitution of $s$ for the free occurrences of $x$ in $t$.
Despite its tiny grammar, the untyped lambda calculus can encode Booleans, natural numbers, pairs, recursion, and arbitrary computable functions. Computation is expressed entirely through term construction, application, and substitution (Church 1932, 1936a).
The pure untyped lambda calculus is a system of computation. A term may reduce to a value or run forever; nontermination is not itself a logical contradiction. The trouble appears when unrestricted lambda abstraction and self-application are used as a foundation for logic with implication and modus ponens.
In that setting, Curry's paradox constructs a self-referential proposition that allows any proposition $Q$—even $1=2$—to be derived. Historically, Kleene and Rosser proved Church's original untyped logical system inconsistent in 1935; Curry later isolated the simpler route presented here (Kleene and Rosser 1935; Curry 1942).
The key construction is
$$F=\lambda x.(x\,x\rightarrow Q),\qquad C=F\,F.$$Because the calculus is untyped, $x$ may be applied to itself. Beta-reduction then gives
$$C\longrightarrow_\beta(C\rightarrow Q).$$Thus $C$ has the logical force of “If this very proposition is true, then $Q$.” Combined with ordinary implication rules, that equivalence collapses the logic.
Show the complete Curry-paradox derivation
Step 1: choose an arbitrary proposition
Let $Q$ be any proposition. Nothing in the construction will depend on its content.
Step 2: construct and apply the self-referential function
$$F=\lambda x.(x\,x\rightarrow Q),\qquad C=F\,F.$$ $$\begin{aligned}C&=F\,F\\&=(\lambda x.(x\,x\rightarrow Q))\,F\\&\longrightarrow_\beta F\,F\rightarrow Q.\end{aligned}$$Since $F\,F$ is $C$, we have $C=_\beta(C\rightarrow Q)$.
Step 3: first derive $C\rightarrow Q$
Temporarily assume $C$. By beta-conversion, obtain $C\rightarrow Q$. Modus ponens gives $Q$, so implication introduction discharges the assumption and yields $C\rightarrow Q$.
$$\begin{array}{lll}1.&C&\text{assumption}\\2.&C\rightarrow Q&\text{beta-conversion of line 1}\\3.&Q&\text{modus ponens on 1 and 2}\\4.&C\rightarrow Q&\text{implication introduction.}\end{array}$$Step 4: convert back and conclude $Q$
Because beta-convertibility works in either direction, convert the theorem $C\rightarrow Q$ into $C$. A final use of modus ponens gives $Q$:
$$\frac{C\qquad C\rightarrow Q}{Q}.$$Since $Q$ was arbitrary, choose $Q\equiv(1=2)$. Every proposition becomes provable, so the logic is inconsistent.
Precisely where simple types stop the paradox
The construction depends on $x\,x$. If the argument occurrence of $x$ has type $A$, then the function occurrence must have type $A\to\mathsf{Prop}$. Both occurrences are the same variable, so typing the expression would require
$$A=A\rightarrow\mathsf{Prop}.$$No finite simple type satisfies this equation. Equivalently, the application rule would require both $\Gamma\vdash x:A\to\mathsf{Prop}$ and $\Gamma\vdash x:A$ from a context that assigns one type to $x$:
$$\frac{\Gamma\vdash e_1:A\rightarrow B\qquad\Gamma\vdash e_2:A}{\Gamma\vdash e_1\,e_2:B}.$$The application derivation cannot be constructed. Consequently $F$ cannot be defined, $C$ cannot be formed, and the derivation of arbitrary $Q$ never begins. Types prevent the paradoxical proposition from being constructed(Church 1940).
This restriction makes the language less expressive: ordinary STLC cannot define unrestricted general recursion. In return, every well-typed STLC term terminates.
We study an STLC extended with unit, Booleans, and products. Its expressions are:
$$\begin{aligned}e ::= {}&x &&\text{variable}\\ \mid{}&\langle\rangle &&\text{unit value}\\ \mid{}&\mathbf{false}\mid\mathbf{true} &&\text{Booleans}\\ \mid{}&\mathbf{if}\;e_1\;\mathbf{then}\;e_2\;\mathbf{else}\;e_3 &&\text{case analysis}\\ \mid{}&\langle e_1,e_2\rangle &&\text{pair}\\ \mid{}&\mathbf{fst}(e)\mid\mathbf{snd}(e) &&\text{projections}\\ \mid{}&\lambda x:\tau.e &&\text{abstraction}\\ \mid{}&e_1\;e_2 &&\text{application.}\end{aligned}$$The types are
$$\tau::=\mathbf{unit}\mid\mathbf{bool}\mid\tau_1\times\tau_2\mid\tau_1\to\tau_2.$$unithas one canonical value, $\langle\rangle$.boolhas the canonical valuestrueandfalse.- $\tau_1\times\tau_2$ contains pairs with component types $\tau_1$ and $\tau_2$.
- $\tau_1\to\tau_2$ contains functions from $\tau_1$ inputs to $\tau_2$ outputs.
The arrow associates to the right: $\tau_1\to\tau_2\to\tau_3$ means $\tau_1\to(\tau_2\to\tau_3)$.
A typing judgment has the form $\Gamma\vdash e:\tau$. It reads:
Assuming the variables have the types recorded in $\Gamma$, expression $e$ has type $\tau$.
The context $\Gamma$ is a finite collection of assumptions such as $x:\mathbf{bool},\;f:\mathbf{bool}\to\mathbf{unit}$. A typing rule has premises above a line and a conclusion below it. A term type-checks when we can build a finite derivation tree whose leaves are rules with no premises and whose root is the desired judgment.
Variables and constants
$$\frac{x:\tau\in\Gamma}{\Gamma\vdash x:\tau}\;\text{T-Var}$$If the context assigns type $\tau$ to $x$, then under that context $x$ has type $\tau$. For example, because $x:\mathbf{bool}\in x:\mathbf{bool}$, we have $x:\mathbf{bool}\vdash x:\mathbf{bool}$. The rule does not claim that every variable has one fixed type; its type comes from the current context.
Unit and Boolean constants have their types under any context:
$$\frac{}{\Gamma\vdash\langle\rangle:\mathbf{unit}}\;\text{T-Unit}\qquad \frac{}{\Gamma\vdash\mathbf{true}:\mathbf{bool}}\;\text{T-True}\qquad \frac{}{\Gamma\vdash\mathbf{false}:\mathbf{bool}}\;\text{T-False}$$These rules have no premises, so they form leaves of typing derivations. Unit is useful even though it contains no information: it represents a computation with no interesting result and, under propositions-as-types, corresponds to truth.
Conditional expressions
$$\frac{\Gamma\vdash e_1:\mathbf{bool}\qquad\Gamma\vdash e_2:\tau\qquad\Gamma\vdash e_3:\tau}{\Gamma\vdash\mathbf{if}\;e_1\;\mathbf{then}\;e_2\;\mathbf{else}\;e_3:\tau}\;\text{T-If}$$The condition must be Boolean and both branches must have the same type, because static checking does not generally know which branch will run.
All premises use the same $\Gamma$. This is an ordinary, non-linear type system: variables may appear in several subexpressions or not at all.
Products
$$\frac{\Gamma\vdash e_1:\tau_1\qquad\Gamma\vdash e_2:\tau_2}{\Gamma\vdash\langle e_1,e_2\rangle:\tau_1\times\tau_2}\;\text{T-Pair}$$ $$\frac{\Gamma\vdash e:\tau_1\times\tau_2}{\Gamma\vdash\mathbf{fst}(e):\tau_1}\;\text{T-Fst}\qquad \frac{\Gamma\vdash e:\tau_1\times\tau_2}{\Gamma\vdash\mathbf{snd}(e):\tau_2}\;\text{T-Snd}$$For example, $\langle\mathbf{true},\langle\rangle\rangle:\mathbf{bool}\times\mathbf{unit}$. Its first projection has type $\mathbf{bool}$ and its second has type $\mathbf{unit}$. Operationally, $\mathbf{fst}(\langle v_1,v_2\rangle)\longrightarrow v_1$ and $\mathbf{snd}(\langle v_1,v_2\rangle)\longrightarrow v_2$.
Function abstraction
$$\frac{\Gamma,x:\tau_1\vdash e:\tau_2}{\Gamma\vdash(\lambda x:\tau_1.e):\tau_1\to\tau_2}\;\text{T-Abs}$$Temporarily assume that the parameter $x$ has input type $\tau_1$. If the body has type $\tau_2$, the abstraction has type $\tau_1\to\tau_2$. Thus $\lambda x:\mathbf{bool}.x$ has type $\mathbf{bool}\to\mathbf{bool}$. The assumption about $x$ is local to the body.
The constant function $\lambda x:\mathbf{bool}.\langle\rangle$ has type $\mathbf{bool}\to\mathbf{unit}$. STLC permits the body to ignore $x$.
Function application
$$\frac{\Gamma\vdash e_1:\tau_1\to\tau_2\qquad\Gamma\vdash e_2:\tau_1}{\Gamma\vdash e_1\;e_2:\tau_2}\;\text{T-App}$$The function must accept the argument's type. Here is a complete derivation:
$$\frac{\dfrac{\dfrac{x:\mathbf{bool}\in x:\mathbf{bool}}{x:\mathbf{bool}\vdash x:\mathbf{bool}}\;\text{T-Var}}{\varnothing\vdash\lambda x:\mathbf{bool}.x:\mathbf{bool}\to\mathbf{bool}}\;\text{T-Abs}\qquad\dfrac{}{\varnothing\vdash\mathbf{false}:\mathbf{bool}}\;\text{T-False}}{\varnothing\vdash(\lambda x:\mathbf{bool}.x)\;\mathbf{false}:\mathbf{bool}}\;\text{T-App}$$Evaluation agrees with the assigned type: $(\lambda x:\mathbf{bool}.x)\;\mathbf{false}\longrightarrow_\beta\mathbf{false}$.
The typing rules mirror the grammar of terms:
T-Var,T-Unit,T-True, andT-Falseprovide derivation leaves.T-Pairconstructs products;T-FstandT-Sndeliminate them.T-Absconstructs functions;T-Appeliminates them.T-Ifeliminates a Boolean by selecting between branches.
This constructor/eliminator pattern is fundamental. To understand a type, ask: How are its values introduced? and How can they be eliminated? Later systems—sums, polymorphism, dependent types, and linear types—follow the same organizing idea.
A typing derivation is a static claim about a program. Type safety is conventionally divided into two theorems (Wright and Felleisen 1994).
Preservation
If a well-typed term takes a computation step, its type does not change:
$$\text{If }\Gamma\vdash e:\tau\text{ and }e\longrightarrow e',\text{ then }\Gamma\vdash e':\tau.$$Progress
A closed, well-typed term is either a value or can take another step:
$$\text{If }\varnothing\vdash e:\tau,\text{ then }e\text{ is a value or }e\longrightarrow e'\text{ for some }e'.$$Together, progress and preservation imply that a closed well-typed program does not get stuck by applying true as a function or projecting fst from a Boolean. Type safety does not prove that a program implements its author's intended function; it rules out specific classes of misuse.
Normalization
Every well-typed term in this STLC eventually reaches a normal form. In fact, the calculus is strongly normalizing: no infinite reduction sequence begins from a well-typed term (Tait 1967). This is valuable for logic but restrictive for programming. Real languages regain recursion and infinite computation through recursive types, fixed points, general recursion, or effects—and give up unconditional termination.
Under the Curry–Howard correspondence, types can be read as propositions and terms as proofs:
| Type-theoretic form | Logical reading |
|---|---|
| $\tau_1\to\tau_2$ | implication $A\Rightarrow B$ |
| $\tau_1\times\tau_2$ | conjunction $A\wedge B$ |
unit | truth $\top$ |
| $e:\tau$ | a proof of proposition $\tau$ |
Abstraction is implication introduction: if assuming $A$ lets us prove $B$, then we have a proof of $A\Rightarrow B$. Application is modus ponens. Pair formation supplies proofs of both conjuncts, and projections extract either proof. Beta-reduction simplifies a proof by removing a detour between introducing a connective and immediately eliminating it (Howard 1980).
bool. Our primitive Boolean is a programming datatype and should not automatically be identified with a logical proposition. The cleanest logical presentation uses proposition-indexed base types and often an empty type for falsehood.Foundations
The path from Hilbert's decision problem through Church and Turing revealed that computation can be studied mathematically—and that some precisely stated problems have no algorithmic solution. Types showed how restricting term formation can recover consistency and normalization.
Programming languages
STLC is the small core inside many functional languages and typed intermediate representations. Variables, functions, application, products, and case analysis reappear in ML, Haskell, Scala, Rust, and TypeScript, though real languages add much more. Designers specify syntax, static semantics, and operational semantics, then prove properties such as progress and preservation.
Mechanized reasoning
Through Curry–Howard, constructing a well-typed program can amount to constructing a proof. Proof assistants and dependently typed languages extend this idea so that types express detailed propositions and specifications while type checking verifies proof objects mechanically.
Restricting what programs may be written can make stronger facts about every accepted program mechanically provable.
STLC gives up unrestricted self-application and general recursion. In exchange it gives compositional typing, type safety, normalization, and a precise bridge between computation and deduction. That is why this tiny calculus remains a starting point for programming-language theory, proof theory, compiler design, and more advanced type systems.
- Church, Alonzo. 1932. “A Set of Postulates for the Foundation of Logic.” Annals of Mathematics 33: 346–366. doi:10.2307/1968337.
- Church, Alonzo. 1936a. “An Unsolvable Problem of Elementary Number Theory.” American Journal of Mathematics 58: 345–363. doi:10.2307/2371045.
- Church, Alonzo. 1936b. “A Note on the Entscheidungsproblem.” Journal of Symbolic Logic 1: 40–41. doi:10.2307/2269326.
- Church, Alonzo. 1940. “A Formulation of the Simple Theory of Types.” Journal of Symbolic Logic 5: 56–68. doi:10.2307/2266170.
- Curry, Haskell B. 1942. “The Inconsistency of Certain Formal Logics.” Journal of Symbolic Logic 7: 115–117. doi:10.2307/2269292.
- Howard, William A. 1980. “The Formulae-as-Types Notion of Construction.” In To H. B. Curry, 479–490.
- Kleene, Stephen C. 1936. “General Recursive Functions of Natural Numbers.” Mathematische Annalen 112: 727–742. doi:10.1007/BF01565439.
- Kleene, Stephen C., and J. Barkley Rosser. 1935. “The Inconsistency of Certain Formal Logics.” Annals of Mathematics 36: 630–636. doi:10.2307/1968646.
- Pierce, Benjamin C. 2002. Types and Programming Languages. MIT Press.
- Tait, William W. 1967. “Intensional Interpretations of Functionals of Finite Type I.” Journal of Symbolic Logic 32: 198–212. doi:10.2307/2271658.
- Turing, Alan M. 1936. “On Computable Numbers, with an Application to the Entscheidungsproblem.” Proceedings of the London Mathematical Society 42: 230–265. doi:10.1112/plms/s2-42.1.230.
- Wright, Andrew K., and Matthias Felleisen. 1994. “A Syntactic Approach to Type Soundness.” Information and Computation 115: 38–94. doi:10.1006/inco.1994.1093.