Paths to discovery : the Curry-Howard correspondence, 1930-1970

Abstract

The first lecture traced the three paths leading to Curry and Howard's discovery : the lambda-calculus, intuitionistic logic, and simple type systems.

Around 1930, Church introduced the lambda-notation λx.e to designate the function that associates e with x, and used it to unify various mathematical notations involving related variables (sums, limits, quantifiers, etc.). His first lambda-calculus, published in 1932 and 1933, is a mathematical logic that uses lambda-notation to represent sets. This logic was quickly abandoned as incoherent. By 1936, however, pure lambda-calculus, stripped of its logical connectors, had established itself as a fundamental formalism of computability, in equivalence with Turing machines, and then, starting with the Lisp language (1960), as the core of functional programming languages.

Intuitionistic logic, introduced by Glivenko and Heyting around 1928, formalizes the notion of constructive demonstration, which is an important aspect of intuitionism, the philosophy of mathematics founded by Brouwer. According to the BHK (Brouwer, Heyting, Kolmogorov) interpretation of intuitionism, the only true propositions in intuitionistic logic are those that are justified by a construction, i.e. a mathematical object that attests to their veracity. Thus, a construction of ∃x.P is a pair of a value for x and a construction of P(x). Non-constructive demonstrations of ∃x.P are therefore excluded.

Types are present in many programming languages to detect programming errors and clarify the meaning of programs. In logic, they appeared as early as 1908 in Russell's work to reject absurd terms such as x ∉ x (" x does not belong to itself") and the paradoxes that ensued. Starting with Russell's type theory, several simplifications lead to the simply typed lambda-calculus published by Church in 1940.

The stage was set for the resonance between typed lambda-calculus and intuitionistic logic. A first observation, made by Curry in 1958, is that if we read the types of functions τ → σ as the implication P ⇒ Q of propositions, the typing rule of the application is the modus ponens rule of deduction, and the types of the combinators S, K, I of the lambda-calculus are the axioms defining implication in a Hilbert-style logic. But it wasn't until 1969 that Howard constructed the complete correspondence between typed lambda-calculus and intuitionistic logic. Not only do types correspond to propositions and terms to constructions (in the BHK sense), but the evaluation of terms by betareductions corresponds to the elimination of cuts in demonstrations, at least for the implicative fragment.