Throughout the twentieth century, mathematical logic, computer science, and category theory developed along seemingly isolated trajectories. Logic studied propositions and deduction; computer science studied algorithms and types; category theory studied abstract structures and morphisms. Then, a profound revelation united them into a single intellectual continent: the Curry-Howard-Lambek Correspondence. A mathematical proposition is literally a data type; a mathematical proof is literally an executable program; and cut elimination is literally program execution.
1. The Propositions-as-Types Principle (Curry-Howard)
In 1934, Haskell Curry observed that the types of combinators in combinatory logic correspond to axiom schemes of intuitionistic propositional logic. In 1969, William Alvin Howard formalized this into an exact isomorphism between Intuitionistic Natural Deduction and the Simply Typed Lambda Calculus ($lambda^to$):
The Curry-Howard Isomorphism Dictionary
| Intuitionistic Logic | Type Theory / Computer Science | Category Theory (CCC) |
|---|---|---|
| Proposition $A$ | Type $A$ | Object $A in text{Ob}(mathcal{C})$ |
| Proof $pi$ of Proposition $A$ | Term / Program $t$ of type $A$ ($t : A$) | Morphism $f: 1 to A$ (Global element) |
| Conjunction $A land B$ | Product Type $A times B$ (Pair / Tuple) | Categorical Product $A times B$ |
| Disjunction $A lor B$ | Sum / Either Type $A + B$ | Coproduct / Pushout $A amalg B$ |
| Implication $A to B$ | Function Type $A to B$ | Exponential Object $B^A$ |
| Tautology $top$ (True) | Unit Type $mathbf{1}$ (`()`) | Terminal Object $1$ |
| Absurdity $bot$ (False) | Void / Empty Type $mathbf{0}$ | Initial Object $0$ |
| Proof Normalization (Cut Elimination) | $beta$-Reduction (Computation / Execution) | Categorical Equality of Arrows |
2. The Mechanics: Implication as Lambda Abstraction
Consider the natural deduction rules for implication ($to$):
- Introduction Rule ($totext{I}$): If assuming $A$ allows us to prove $B$, then $A to B$ holds.
Typed $lambda$-calculus: If variable $x: A$ allows constructing term $e: B$, then the anonymous function $(lambda x: A . e)$ has type $A to B$. - Elimination Rule ($totext{E}$ / Modus Ponens): From $A to B$ and $A$, deduce $B$.
Typed $lambda$-calculus: Given function $f: A to B$ and argument $a: A$, function application $(f , a)$ has type $B$.
What happens when an introduction rule is immediately followed by an elimination rule? In logic, this is a detour (a Cut). In computer science:
[
(lambda x: A . e) , a ;; longrightarrow_beta ;; e[x mapsto a]
]
Beta-reduction is the universal engine of computation! Evaluating a program is literally simplifying a proof. A program that halts without error is a normalized, cut-free proof.
3. Enter Joachim Lambek: Cartesian Closed Categories (CCC)
In 1972, Canadian mathematician Joachim Lambek established the third vertex of the trinity. A category $mathcal{C}$ is a Cartesian Closed Category (CCC) if it has:
- A terminal object $1$.
- Binary products $A times B$ for any objects $A, B$.
- Exponential objects $B^A$ equipped with an evaluation morphism $text{eval}: B^A times A to B$ satisfying the universal property:
[
text{Hom}(X times A, B) cong text{Hom}(X, B^A)
]
Lambek proved that the internal language of any Cartesian closed category is precisely the simply typed lambda calculus, which in turn is isomorphic to intuitionistic propositional logic! The equivalence is not an analogy; it is an exact, bidirectional categorical equivalence of categories:
[
mathbf{IntLogic} ;cong; mathbf{TypedLambda} ;cong; mathbf{CCC}
]
4. Dependent Types: The Modern Frontier
The correspondence extends directly to first-order quantifiers through Dependent Type Theory (Per Martin-Löf, 1972):
- Universal Quantifier ($forall x: A . B(x)$): Corresponds to the Dependent Product Type ($Pi$-type): a function whose return type depends on the specific input value.
- Existential Quantifier ($exists x: A . B(x)$): Corresponds to the Dependent Sum Type ($Sigma$-type): a dependent pair $(a, b)$ where $a: A$ is the witness and $b: B(a)$ is the proof that $a$ satisfies the predicate.
This correspondence is the beating heart of modern software verification. When an interactive proof assistant like Lean 4 or Coq verifies a mathematical theorem, it is simply compiling and type-checking a functional computer program. A compiler error is a logical fallacy; a successfully compiled binary is an infallible mathematical proof.
