The Curry-Howard Correspondence

References:

• Computer-aided formal reasoning course

Classical vs Intuitionistic Logic

Example

There exist irrational numbers $a$ and $b$ such that $a^b$ is rational.

Proof. ${\sqrt{2}}^{\sqrt{2}}$ is either rational or irrational. If it is rational, we’re done.
Otherwise, take $a={\sqrt{2}}^{\sqrt{2}}$ and $b=\sqrt{2}$. Then $a^b=({\sqrt{2}}^{\sqrt{2}}{)}^{\sqrt{2}}=2$ and we’re done.

We didn’t give $a$ and $b$: the proof is non-constructive.

In intuitionistic logic, the following are forbidden:

• Excluded middle: $A\vee \neg A$
• Double negation elimination: $\neg \neg A\to A$
• Pierce’s Law: $((A\to B)\to A)\to A$

What do we gain? → Constructiveness

Theorem (Disjunction and witness properties)

If ${⊢}_{I}A\vee B$, then either ${⊢}_{I}A$ or ${⊢}_{I}B$.
If ${⊢}_I\exists x.P(x)$, then there is a term $t$ such that ${⊢}_{I}P(t)$.

What do we lose? → Nothing! (almost)

Theorem

There is a map $(\cdot {)}^{\neg }$ from formulas to formulas, such that whenever ${⊢}_{C}A$, then ${⊢}_I{A}^{\neg }$.
Moreover, they are classically equivalent: ${⊢}_{C}A\leftrightarrow A^{\neg }$.

Natural Deduction

There are two important families of deduction systems. The two most important are:

• Natural Deduction: Natural deduction follows the natural style of reasoning in text books. Most of an ND proof consists of forward reasoning. Occassionally additional assumptions are introduced or dropped. Natural deduction treats conclusions and assumptions different. Because of this, it fits better to intuitionistic logic than to classical logic.
• Sequent Calculus: In sequent calculus, conclusions and premisses are treated in exactly the same way. Because of this, sequent calculus naturally fits to classical logic. Automated proof search in sequent calculus is relatively easy. Each time when a rule is applied, most formulas are copied unchanged, and one has to write very much.

Now we introduce the intuitionistic natural deduction system ${\mathrm{NJ}}_0$.

Formulas ($p$ is an atomic proposition):

$$\begin{array}{rl}A,B,C& ::=p\mid \top \mid \perp \mid A\wedge B\mid A\vee B\mid A\to B\end{array}$$

Notation: $\neg A:=A\to \perp$

Sequents of the form $\Gamma ⊢A$, where:

• $A$ is a formula.
• $\Gamma =A_1,\dots ,A_n$ is an unordered finite list of formulas.
• $⊢$ stands for logical consequence.

Proof: finite tree of sequents using deduction rules.

Deduction rules:

$$\frac{}{\Gamma ,A⊢A}(\text{Ax})$$

$$\begin{array}{cc}\frac{}{\Gamma ⊢\top }(\top \text{-I})& \frac{\Gamma ⊢\perp }{\Gamma ⊢A}(\perp \text{-E})\\ \frac{\Gamma ,A⊢B}{\Gamma ⊢A\to B}(\to \text{-I})& \frac{\Gamma ⊢A\to B\Gamma ⊢A}{\Gamma ⊢B}(\to \text{-E})\\ \frac{\Gamma ⊢A_1\Gamma ⊢A_2}{\Gamma ⊢A_1\wedge A_2}(\wedge \text{-I})& \frac{\Gamma ⊢A_1\wedge A_2}{\Gamma ⊢A_i}({\wedge }_i\text{-E})\\ \frac{\Gamma ⊢A_i}{\Gamma ⊢A_i\vee A_2}({\vee }_i\text{-I})& \frac{\Gamma ⊢A_1\vee A_2\Gamma ,A_1⊢B\Gamma ,A_2⊢B}{\Gamma ⊢B}({\vee }_i\text{-E})\end{array}$$

Basic Properties

Weakening: If $\Gamma ⊢B$, then $\Gamma ,A⊢B$.

Contraction: If $\Gamma ,A,A⊢B$, then $\Gamma ,A⊢B$.

Theorem (admitted)

The excluded middle is not provable in ${\mathrm{NJ}}_0$: there is a formula $A$ such that $/⊢A\vee \neg A$.

Classical Natural Deduction (${\mathrm{NK}}_0$): All the rules of ${\mathrm{NJ}}_0$ + Law of Excluded Middle:

$$\frac{}{\Gamma ⊢A\vee \neg A}(\text{EM})$$

Untyped $\lambda$-calculus

Syntax:

$$t,u::=x\mid \lambda x.t\mid tu\text{where x is a variable}$$

$$\begin{array}{cc}\lambda \text{-calculus}& \text{Haskell}\\ \lambda x.t& \text{x -> t}\\ tu& \text{t u}\end{array}$$

$\beta$-reduction:

$$(\lambda x.t)u{▹}_{\beta }t[u/x]$$

Its reflexive-symmetric-transitive closure is written ${\equiv }_{\beta }$.

⚠ beware of free and bound variables:

$$\lambda x.zx=\lambda y.zy\ne \lambda z.zz$$

Examples:

$$I=\lambda x.xK=\lambda x\lambda y.xS=\lambda x\lambda y\lambda z.xz(yz)$$

$$\Delta =\lambda x.xx\Omega =\Delta \Delta$$

Exercise: reduce the following λ-terms:

$$\Delta IISKK\Omega KI\Omega \Delta (II)$$

Theorem (admitted)

The untyped λ-calculus is Turing-complete.

Simply-typed $\lambda$-calculus

Types ($\kappa$ is a base type):

$$T,U::=\kappa \mid U\to T$$

Context: finite map from variables to types

$$\Gamma =x_1:T_1,\dots ,x_n:T_n\text{such that xi=xj when i=j}$$

Typing judgement: “The term $t$ has type $T$ in context $\Gamma$ ”.

$$\Gamma ⊢t:T$$

Typing rules:

$$\frac{}{\Gamma ,x:T⊢x:T}(\mathrm{Ax})$$

$$\frac{\Gamma ,x:U⊢t:T}{\Gamma ⊢\lambda x.t:U\to T}(\to \text{-I})\frac{\Gamma ⊢t:U\to T\Gamma ⊢u:U}{\Gamma ⊢tu:T}(\to \text{-E})$$

Exercise: derive the following typing judgements

• $⊢\lambda x.x:T\to T$
• $x:T,y:U,z:T\to U\to V⊢zxy:V$

Solution

$$\frac{\frac{}{x:T⊢x:T}(\mathrm{Ax})}{⊢\lambda x.x:T\to T}(\to \text{-I})$$

• Let $\Gamma =x:T,y:U,z:T\to U\to V$.

$$\frac{\frac{\frac{}{\Gamma ⊢z:T\to U\to V}(\mathrm{Ax})\frac{}{\Gamma ⊢x:T}(\mathrm{Ax})}{\Gamma ⊢zx:U\to V}(\to \text{-E})\frac{}{\Gamma ⊢y:U}(\mathrm{Ax})}{\Gamma ⊢zxy:V}(\to \text{-E})$$

Exercise: type the following terms:

• $K=\lambda x\lambda y.x$
• $S=\lambda x\lambda y\lambda z.xz(yz)$

Solution

$$\frac{\frac{\frac{}{x:T,y:U⊢y:U}(\mathrm{Ax})}{x:T⊢\lambda y.x:U\to T}(\to \text{-I})}{\Gamma ⊢\lambda x\lambda y.x:T\to U\to T}(\to \text{-I})$$

• Let $\Gamma =x:T\to U\to V,y:T\to U,z:T$.

$$\frac{\frac{}{\Gamma ⊢x:T\to U\to V}(\mathrm{Ax})\frac{}{\Gamma ⊢z:T}(\mathrm{Ax})}{\Gamma ⊢xz:U\to V}(\to \text{-E})$$

$$\frac{\frac{}{\Gamma ⊢y:T\to U}(\mathrm{Ax})\frac{}{\Gamma ⊢z:T}(\mathrm{Ax})}{\Gamma ⊢yz:V}(\to \text{-E})$$

$$\frac{\Gamma ⊢xz:U\to V\Gamma ⊢yz:V}{\Gamma ⊢xz(yz):V}(\to \text{-E})$$

$$\frac{\frac{\frac{x:T\to U\to V,y:T\to U,z:T⊢xz(yz):V}{x:T\to U\to V,y:T\to U⊢\lambda z.xz(yz):T\to V}(\to \text{-I})}{x:T\to U\to V⊢\lambda y\lambda z.xz(yz):(T\to U)\to T\to V}(\to \text{-I})}{⊢\lambda x\lambda y\lambda z.xz(yz):(T\to U\to V)\to (T\to U)\to T\to V}(\to \text{-I})$$

Exercise: is $\Delta =\lambda x.xx$ typable?

Full Type System

We extend the simply-typed $\lambda$-calculus with Sum Types, Product Types, Unit Type, and Void Type.

$$\begin{array}{cc}\lambda \text{-calculus}& \text{Haskell}\\ \lambda x.t& \text{x -> t}\\ tu& \text{t u}\\ T\times U& \text{(T, U)}\\ ⟨t,u⟩& \text{(t, u)}\\ {\pi }_{1}t& \text{fst t}\\ {\pi }_{2}t& \text{snd t}\\ T+U& \text{Either T U}\\ {\mathrm{in}}_{1}t& \text{Left t}\\ {\mathrm{in}}_{2}t& \text{Right t}\\ \text{case}\dots & \text{pattern matching}\\ \text{Unit}& \text{()}\\ ⟨⟩& \text{()}\\ \text{Void}& \text{Void}\\ \text{case t of {}}& \text{absurd t}\end{array}$$

Types:

$$\begin{array}{rl}T,U& ::=\kappa \mid U\to T\mid T\times U\mid T+U\mid \text{Unit}\mid \text{Void}\end{array}$$

Terms:

$$\begin{array}{rl}t,u::=& x\mid \lambda x.t\mid tu\mid ⟨t,u⟩\mid {\pi }_{1}t\mid {\pi }_{2}t\mid ⟨⟩\mid \text{case t of {}}\mid \\ & {\mathrm{in}}_{1}t\mid {\mathrm{in}}_{2}t\mid \text{case }t\text{ of }\left\{{\mathrm{in}}_{1}x\mapsto u\mid {\mathrm{in}}_{2}y\mapsto v\right\}\end{array}$$

$\beta$-reduction:

$$\begin{array}{c}(\lambda x.t)u{▹}_{\beta }t[u/x]\\ {\pi }_1⟨t,u⟩{▹}_{\beta }t{\pi }_2⟨t,u⟩{▹}_{\beta }u\\ \text{case }({\mathrm{in}}_{i}t)\text{ of }\{{\mathrm{in}}_1{x}_1\mapsto u_1,{\mathrm{in}}_2{x}_2\mapsto u_2\}{▹}_{\beta }{u}_i[t/x_i]\end{array}$$

Typing rules:

$$\frac{}{\Gamma ,x:T⊢x:T}(\text{Ax})\frac{}{\Gamma ⊢⟨⟩:\text{Unit}}(\text{Unit-I) }\frac{\Gamma ⊢t:\text{Void}}{\Gamma ⊢\text{case }t\text{ of }\{\}:T}(\text{Void-E})$$

$$\frac{\Gamma ,x:U⊢t:T}{\Gamma ⊢\lambda x.t:U\to T}(\to \text{-I})\frac{\Gamma ⊢t:U\to T\Gamma ⊢u:U}{\Gamma ⊢tu:T}(\to \text{-E})$$

$$\frac{\Gamma ⊢t:T\Gamma ⊢u:U}{\Gamma ⊢⟨t,u⟩:T\times U}(\times \text{-I})\frac{\Gamma ⊢t:T_1\times T_2}{\Gamma ⊢{\pi }_{i}t:T_i}({\times }_i\text{-E})$$

$$\frac{\Gamma ⊢t:T_i}{\Gamma ⊢{\mathrm{in}}_{i}t:T_1+T_2}(+{}_i\text{-I})$$

$$\frac{\Gamma ⊢t:T_1+T_2\Gamma ,x:T_1⊢u_1:U\Gamma ,y:T_2⊢u_2:U}{\Gamma ⊢\text{case }t\text{ of }\left\{{\mathrm{in}}_{1}x\mapsto u_1\mid {\mathrm{in}}_{2}y\mapsto u_2\right\}:U}(+\text{-E})$$

Properties

Inversion:

• If $\Gamma ⊢\lambda x.t:T$ then $T=U\to V$ and $\Gamma ,x:U⊢t:V$
• If $\Gamma ⊢⟨t_1,t_2⟩:T$ then $T=T_1\times T_2$ and $\Gamma ⊢t_i:T_i$
• If $\Gamma ⊢{\mathrm{in}}_{i}t:T$ then $T=T_1+T_2$ and $\Gamma ⊢t:T_i$
• ...

Substitution: If $\Gamma ,x:U⊢t:T$ and $\Gamma ⊢u:U$ then $\Gamma ⊢t[u/x]:T$

Theorem (Subject Reduction)

If $\Gamma ⊢t:T$ and $t{▹}_{\beta }u$ then $\Gamma ⊢u:T$.

Theorem (Strong Normalization)

If $\Gamma ⊢t:T$ then $t$ is strongly normalizing.

Curry-Howard Correspondence

• Propositions $\leftrightarrow$ Types
• Proofs $\leftrightarrow$ Programs
• Computation $\leftrightarrow$ Proof Simplification

Propositions:

$$A,B::=p\mid A\to B\mid A\wedge B\mid A\vee B\mid \top \mid \perp$$

Types:

$$T,U::=\kappa \mid U\to T\mid T\times U\mid T+U\mid \text{Unit}\mid \text{Void}$$

$$\begin{array}{cc}\text{Propositions}& \text{Types}\\ p& T\\ A\to B& T\to U\\ A\wedge B& T\times U\\ A\vee B& T+U\\ \top & \text{Unit}\\ \perp & \text{Void}\end{array}$$

Theorem (Curry-Howard Correspondence for ${\mathrm{NJ}}_0$)

$A_1,\dots ,A_n⊢A$ is derivable in ${\mathrm{NJ}}_0$ iff there is a term $t$ with $\mathrm{FV}(t)\subseteq \left\{x_1,\dots ,x_n\right\}$ such that $x_1:A_1,\dots ,x_n:A_n⊢t:A$.

Reminder: some properties of ${▹}_{\beta }$ :

• Subject reduction: if $\Gamma ⊢t:T$ and $t{▹}_{\beta }u$ then $\Gamma ⊢u:T$.
• If $t$ is typable, then it is strongly normalizing.

Lemma (Closed normal forms)

If $t$ is typed, closed, and in ${▹}_{\beta }$-normal form, then $t$ is of the form: $⟨⟩$ or $\lambda x.u$ or $⟨u,v⟩$ or ${\mathrm{in}}_{i}u$.

Corollary: in intuitionistic propositional logic $({\mathrm{NJ}}_0)$,

• $⊢\perp$ is not provable.
• if $⊢A\vee B$, then either $⊢A$ or $⊢B$.

Beyond ${\mathrm{NJ}}_0$ and simple types

The correspondence can be extended in many ways:

• System F → second-order logic
• Martin-Löf Type Theory → dependent types (quantifiers)
• Calculus of Constructions
• Calculus of Inductive Constructions → Coq
• Homotopy Type Theory
• ...

Other approaches to the “Proofs as Programs” paradigm:

• Realizability
• Classical Realizability