A Crash Course on the Curry-Howard Isomorphism

Reed College ACM

Talk given February 27, 2013

Notes revised March 24, 2013

1 Overview
2 Logic
3 Lambda Calculus
4 The Isomorphism
5 Continuations and Classical Logic

1 Overview

The Curry-Howard Isomorphism is a framework for relating logic and programming languages. So, we need to define what we mean by those terms.

2 Logic

Note that we're only going to be considering propositional logic and its structure, but that the result will be more interesting than you might expect.

2.1 Intuitionism

Think of the logic you're used to, minus double negation elimination. Note that proof by contradiction is still allowed, but there are some surprising consequences.

2.2 Language

2.2.1 Symbols

We have:

Proposition symbols $p_0, p_1, p_2, \ldots$
The special proposition symbol $\bot$, denoting a false proposition.
The material conditional arrow, $\rightarrow$, as well as the connectives $\vee$ and $\wedge$, for disjunction and conjunction, respectively.
Parentheses

2.2.2 Sentences

Defined recursively:

Each proposition symbol is a sentence.
If $S_1$ and $S_2$ are sentences, then so is $(S_1 \rightarrow S_2)$.

2.2.3 Abbreviations

We write $\neg p$ for $(p \rightarrow \bot)$.

2.3 Natural Deduction

2.3.1 Notation

We write $\Gamma \vdash \alpha$, where $\Gamma$ is a set of sentences and $\alpha$ is a single sentence, to mean that $\Gamma$ implies $\alpha$.

2.3.2 Rules

These are how we move from one implication to another.

We can always deduce $\Gamma, \alpha \vdash \alpha$ (Ax).
From $\Gamma \vdash \bot$ we can deduce $\Gamma \vdash \alpha$ for whatever $\alpha$ we please (PC).
From $\Gamma, \alpha \vdash \beta$ we can deduce $\Gamma \vdash \alpha \rightarrow \beta$ (DP).
From $\Gamma \vdash \alpha, \alpha \rightarrow \beta$ we can deduce $\Gamma \vdash \beta$ (MP).
From $\Gamma \vdash \alpha$ we can deduce either $\Gamma \vdash \alpha \vee \beta$ or $\Gamma \vdash \beta \vee \alpha$ ($\vee$ I).
From $\Gamma \vdash \alpha \wedge \beta$, we can deduce either $\Gamma \vdash \alpha$ or $\Gamma \vdash \beta$ ($\wedge$ E).
From $\Gamma \vdash \alpha$ and $\Gamma \vdash \beta$, we can deduce $\Gamma \vdash \alpha \wedge \beta$ ($\wedge$ I).

2.4 The Implicational Fragment

We will concern ourselves primarily with the implicational fragment, which consists of those sentences using only proposition symbols and the $\rightarrow$ connective.

3 Lambda Calculus

3.1 Language

3.1.1 Symbols

We have the following alphabet:

Variable symbols $x_0, x_1, x_2, \ldots$
The $\lambda$ operator
Parentheses

3.1.2 Sentences

Defined recursively, as before:

Each variable symbol on its own,
Anything of the form $(\lambda x_i M)$, where $M$ is another lambda term.
Anything of the form $MN$, where $M$ is a term obtained through lambda abstraction and $N$ is any lambda term.

3.2 Evaluation / reduction

Quickly go over $\beta$-reduction, perhaps with examples. Note important facts and theorems about order of reduction. Make note of the surprising capabilities of this seemingly barebones system. Mention the Y Combinator, just because it's cool.

3.3 Types

For our purposes, the important part.

3.3.1 Notation

We write $\Gamma \vdash M : \tau$ to mean that, in environment $\Gamma$, $M$ has type $\tau$. An environment is just a binding that assigns types to variable symbols, i.e. $\Gamma = \{ x_1 : \tau_1, x_2 : \tau_2, \ldots, x_n : \tau_n\}$. Thinking of this sort of like a function, we write $\mathrm{dom}(\Gamma) = \{ x \ \vert \ x : \tau \in \Gamma \text{ for some } \tau \}$ and $\mathrm{rg}(\Gamma) = \{ \tau \ \vert \ x : \tau \in \Gamma \text{ for some } x \}$. Sort of like in our logical notation, we will use $\bot$ to denote the empty type.

3.3.2 Type Inference Rules

Motivate these by their similarity to Haskell's type system.

We can always deduce $\Gamma, x : \tau \vdash x : \tau$ (Var).
From $\Gamma, x : \alpha \vdash M : \beta$ we can deduce $\Gamma \vdash (\lambda x M) : (\alpha \rightarrow \beta)$ (Abs).
From $\Gamma \vdash N : \alpha, M : (\alpha \rightarrow \beta)$ we can deduce $\Gamma \vdash MN : \beta$ (App).
From $\Gamma \vdash N : \bot$, we can deduce $\Gamma \vdash \ast(\tau) : \tau$ for any type $\tau$, where $\ast(\tau)$ is the miracle of type $τ$.

3.3.3 Other Types

We can also define types that are analogous to conjunction and disjunction, though we won't do that here.

4 The Isomorphism

$\Gamma \vdash M : \phi$ for some lambda term $M$ iff $\mathrm{rg}(\Gamma) \vdash \phi$ in the implicational fragment of intuitionistic logic.

5 Continuations and Classical Logic

Continuations are a way of expressing conventional control flow operators in functional languages (i.e. Scheme). The idea is to call a function with another function as an argument. The argument can then be called from within the original function in order to move to another part of the program.

5.1 Example: Exception Handling with call/cc

A common instance of a control structure in modern languages, like so:

(define (f throw)
  (let ((fst (get-number-from-user))
        (snd (get-number-from-user)))
    (if (= snd 0)
        (throw 'div-by-zero-exception)
        (/ fst snd))))

(call/cc f)

Make a note of applications to web programming.

5.2 Type of call/cc

In Scheme as it is, call/cc isn't quite what we want. There is a typed variant of the Scheme implementation Racket, and it reports the type of call/cc as follows:

Welcome to Racket v5.3.1.
> call/cc
- : (All (a b) (((a -> Nothing) -> b) -> (U a b)))
#<procedure:call-with-current-continuation>

However, on another interpretation, an operator like call/cc can be given type $((\alpha \rightarrow \bot) \rightarrow \bot) \rightarrow \alpha$. This gives us a Curry-Howard Isomorphism for classical logic.

5.3 Kolmogorov Double Negation Embedding

We can relate classical and intuitionistic logic in an interesting way.

5.3.1 Definition

If $\alpha$ is a sentence of just an atomic proposition, then $K(\alpha) = \neg \neg \alpha$. For general sentences $\beta$ and $\gamma$, we define $K(\beta \rightarrow \gamma) = \neg \neg (K(\beta) \rightarrow K(\gamma))$.

5.3.2 Properties

For any sentence $\alpha$, you can classically derive $K(\alpha)$ from it, and vice versa. Also (this is the big part), $K(\alpha)$ is a theorem in intuitionistic logic iff $\alpha$ is a theorem in classical logic.

5.4 Continuation Passing Style

The corresponding translation from the lambda calculus with call/cc to the lambda calculus without it. This is the computational analog of the Kolmogorov embedding just described. Working the details of this out is where much of the work on my thesis lies.