Curry-Howard, take 1 -------------------- We will return to the Curry-Howard correspondence a number of times during this course. It expresses a deep connection between logic, types, and computation. Today we'll discuss how the simply-typed lambda calculus corresponds to intuitionistic logic. This naturally give rise to the question of what sort of computation classical logic corresponds to---as we'll see later, the answer involves continuations. So at this point we have the simply-typed lambda calculus: a set of ground types, a set of functional types, and some typing rules, given roughly as follows: If a variable `x` has type σ and term `M` has type τ, then the abstract `\xM` has type σ `-->` τ. If a term `M` has type σ `-->` τ, and a term `N` has type σ, then the application `MN` has type τ. These rules are clearly obverses of one another: the functional types that abstract builds up are taken apart by application. The next step in making sense out of the Curry-Howard corresponence is to present a logic. It will be a part of intuitionistic logic. We'll start with the implicational fragment (that is, the part of intuitionistic logic that only involves axioms and implications):
```Axiom: ---------
A |- A

Structural Rules:

Γ, A, B, Δ |- C
Exchange: ---------------------------
Γ, B, A, Δ |- C

Γ, A, A |- B
Contraction: -------------------
Γ, A |- B

Γ |- B
Weakening: -----------------
Γ, A |- B

Logical Rules:

Γ, A |- B
--> I:   -------------------
Γ |- A --> B

Γ |- A --> B         Γ |- A
--> E:   -----------------------------------
Γ |- B
```
`A`, `B`, etc. are variables over formulas. Γ, Δ, etc. are variables over (possibly empty) sequences of formulas. Γ `|- A` is a sequent, and is interpreted as claiming that if each of the formulas in Γ is true, then `A` must also be true. This logic allows derivations of theorems like the following:
```-------  Id
A |- A
---------- Weak
A, B |- A
------------- --> I
A |- B --> A
----------------- --> I
|- A --> B --> A
```
Should remind you of simple types. (What was `A --> B --> A` the type of again?) The easy way to grasp the Curry-Howard correspondence is to *label* the proofs. Since we wish to establish a correspondence between this logic and the lambda calculus, the labels will all be terms from the simply-typed lambda calculus. Here are the labeling rules:
```Axiom: -----------
x:A |- x:A

Structural Rules:

Γ, x:A, y:B, Δ |- R:C
Exchange: -------------------------------
Γ, y:B, x:A, Δ |- R:C

Γ, x:A, x:A |- R:B
Contraction: --------------------------
Γ, x:A |- R:B

Γ |- R:B
Weakening: ---------------------
Γ, x:A |- R:B     [x chosen fresh]

Logical Rules:

Γ, x:A |- R:B
--> I:   -------------------------
Γ |- \xM:A --> B

Γ |- f:(A --> B)      Γ |- x:A
--> E:   -------------------------------------
Γ |- (fx):B
```
In these labeling rules, if a sequence Γ in a premise contains labeled formulas, those labels remain unchanged in the conclusion. What is means for a variable `x` to be chosen *fresh* is that `x` must be distinct from any other variable in any of the labels used in the proof. Using these labeling rules, we can label the proof just given:
```------------  Id
x:A |- x:A
---------------- Weak
x:A, y:B |- x:A
------------------------- --> I
x:A |- (\y.x):(B --> A)
---------------------------- --> I
|- (\x y. x):A --> B --> A
```
We have derived the *K* combinator, and typed it at the same time! Need a proof that involves application, and a proof with cut that will show beta reduction, so "normal" proof. [To do: add pairs and destructors; unit and negation...] Excercise: construct a proof whose labeling is the combinator S, something like this: --------- Ax --------- Ax ------- Ax !a --> !a !b --> !b c --> c ----------------------- L-> -------- L! !a,!a->!b --> !b !c --> c --------- Ax ---------------------------------- L-> !a --> !a !a,!b->!c,!a->!b --> c ------------------------------------------ L-> !a,!a,!a->!b->!c,!a->!b --> c ----------------------------- C! !a,!a->!b->!c,!a->!b --> c ------------------------------ L! !a,!a->!b->!c,! (!a->!b) --> c ---------------------------------- L! !a,! (!a->!b->!c),! (!a->!b) --> c ----------------------------------- R! !a,! (!a->!b->!c),! (!a->!b) --> !c ------------------------------------ R-> ! (!a->!b->!c),! (!a->!b) --> !a->!c ------------------------------------- R-> ! (!a->!b) --> ! (!a->!b->!c)->!a->!c --------------------------------------- R-> --> ! (!a->!b)->! (!a->!b->!c)->!a->!c