1 Curry-Howard, take 1
2 --------------------
4 We will return to the Curry-Howard correspondence a number of times
5 during this course.  It expresses a deep connection between logic,
6 types, and computation.  Today we'll discuss how the simply-typed
7 lambda calculus corresponds to intuitionistic logic.  This naturally
8 give rise to the question of what sort of computation classical logic
9 corresponds to---as we'll see later, the answer involves continuations.
11 So at this point we have the simply-typed lambda calculus: a set of
12 ground types, a set of functional types, and some typing rules, given
13 roughly as follows:
15 If a variable `x` has type &sigma; and term `M` has type &tau;, then
16 the abstract `\xM` has type &sigma; `-->` &tau;.
18 If a term `M` has type &sigma; `-->` &tau;, and a term `N` has type
19 &sigma;, then the application `MN` has type &tau;.
21 These rules are clearly obverses of one another: the functional types
22 that abstract builds up are taken apart by application.
24 The next step in making sense out of the Curry-Howard corresponence is
25 to present a logic.  It will be a part of intuitionistic logic.  We'll
26 start with the implicational fragment (that is, the part of
27 intuitionistic logic that only involves axioms and implications):
29 <pre>
30 Axiom: ---------
31         A |- A
33 Structural Rules:
35           &Gamma;, A, B, &Delta; |- C
36 Exchange: ---------------------------
37           &Gamma;, B, A, &Delta; |- C
39              &Gamma;, A, A |- B
40 Contraction: -------------------
41              &Gamma;, A |- B
43            &Gamma; |- B
44 Weakening: -----------------
45            &Gamma;, A |- B
47 Logical Rules:
49          &Gamma;, A |- B
50 --> I:   -------------------
51          &Gamma; |- A --> B
53          &Gamma; |- A --> B         &Gamma; |- A
54 --> E:   -----------------------------------
55          &Gamma; |- B
56 </pre>
58 `A`, `B`, etc. are variables over formulas.
59 &Gamma;, &Delta;, etc. are variables over (possibly empty) sequences
60 of formulas.  &Gamma; `|- A` is a sequent, and is interpreted as
61 claiming that if each of the formulas in &Gamma; is true, then `A`
62 must also be true.
64 This logic allows derivations of theorems like the following:
66 <pre>
67 -------  Id
68 A |- A
69 ---------- Weak
70 A, B |- A
71 ------------- --> I
72 A |- B --> A
73 ----------------- --> I
74 |- A --> B --> A
75 </pre>
77 Should remind you of simple types.  (What was `A --> B --> A` the type
78 of again?)
80 The easy way to grasp the Curry-Howard correspondence is to *label*
81 the proofs.  Since we wish to establish a correspondence between this
82 logic and the lambda calculus, the labels will all be terms from the
83 simply-typed lambda calculus.  Here are the labeling rules:
85 <pre>
86 Axiom: -----------
87        x:A |- x:A
89 Structural Rules:
91           &Gamma;, x:A, y:B, &Delta; |- R:C
92 Exchange: -------------------------------
93           &Gamma;, y:B, x:A, &Delta; |- R:C
95              &Gamma;, x:A, x:A |- R:B
96 Contraction: --------------------------
97              &Gamma;, x:A |- R:B
99            &Gamma; |- R:B
100 Weakening: ---------------------
101            &Gamma;, x:A |- R:B     [x chosen fresh]
103 Logical Rules:
105          &Gamma;, x:A |- R:B
106 --> I:   -------------------------
107          &Gamma; |- \xM:A --> B
109          &Gamma; |- f:(A --> B)      &Gamma; |- x:A
110 --> E:   -------------------------------------
111          &Gamma; |- (fx):B
112 </pre>
114 In these labeling rules, if a sequence &Gamma; in a premise contains
115 labeled formulas, those labels remain unchanged in the conclusion.
117 What is means for a variable `x` to be chosen *fresh* is that
118 `x` must be distinct from any other variable in any of the labels
119 used in the proof.
121 Using these labeling rules, we can label the proof
122 just given:
124 <pre>
125 ------------  Id
126 x:A |- x:A
127 ---------------- Weak
128 x:A, y:B |- x:A
129 ------------------------- --> I
130 x:A |- (\y.x):(B --> A)
131 ---------------------------- --> I
132 |- (\x y. x):A --> B --> A
133 </pre>
135 We have derived the *K* combinator, and typed it at the same time!
137 Need a proof that involves application, and a proof with cut that will
138 show beta reduction, so "normal" proof.
140 [To do: add pairs and destructors; unit and negation...]
142 Excercise: construct a proof whose labeling is the combinator S,
143 something like this:
145            --------- Ax  --------- Ax   ------- Ax
146            !a --> !a     !b --> !b      c --> c
147            ----------------------- L->  -------- L!
148               !a,!a->!b --> !b          !c --> c
149 --------- Ax  ---------------------------------- L->
150 !a --> !a           !a,!b->!c,!a->!b --> c
151 ------------------------------------------ L->
152       !a,!a,!a->!b->!c,!a->!b --> c
153       ----------------------------- C!
154        !a,!a->!b->!c,!a->!b --> c
155        ------------------------------ L!
156        !a,!a->!b->!c,! (!a->!b) --> c
157        ---------------------------------- L!
158        !a,! (!a->!b->!c),! (!a->!b) --> c
159        ----------------------------------- R!
160        !a,! (!a->!b->!c),! (!a->!b) --> !c
161        ------------------------------------ R->
162        ! (!a->!b->!c),! (!a->!b) --> !a->!c
163        ------------------------------------- R->
164        ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
165        --------------------------------------- R->
166         --> ! (!a->!b)->! (!a->!b->!c)->!a->!c