cat theory ready
[lambda.git] / curry-howard.mdwn
1 Curry-Howard, take 1
2 --------------------
3
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.
10
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:
14
15 If a variable `x` has type σ and term `M` has type τ, then 
16 the abstract `\xM` has type σ `-->` τ.
17
18 If a term `M` has type σ `-->` τ, and a term `N` has type
19 σ, then the application `MN` has type τ.
20
21 These rules are clearly obverses of one another: the functional types
22 that abstract builds up are taken apart by application.
23
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):
28
29 <pre>
30 Axiom: ---------
31         A |- A
32
33 Structural Rules:
34
35           &Gamma;, A, B, &Delta; |- C
36 Exchange: ---------------------------
37           &Gamma;, B, A, &Delta; |- C
38
39              &Gamma;, A, A |- B
40 Contraction: -------------------
41              &Gamma;, A |- B
42
43            &Gamma; |- B
44 Weakening: -----------------
45            &Gamma;, A |- B 
46
47 Logical Rules:
48
49          &Gamma;, A |- B
50 --> I:   -------------------
51          &Gamma; |- A --> B  
52
53          &Gamma; |- A --> B         &Gamma; |- A
54 --> E:   -----------------------------------
55          &Gamma; |- B
56 </pre>
57
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.
63
64 This logic allows derivations of theorems like the following:
65
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>
76
77 Should remind you of simple types.  (What was `A --> B --> A` the type
78 of again?)
79
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:
84
85 <pre>
86 Axiom: -----------
87        x:A |- x:A
88
89 Structural Rules:
90
91           &Gamma;, x:A, y:B, &Delta; |- R:C
92 Exchange: -------------------------------
93           &Gamma;, y:B, x:A, &Delta; |- R:C
94
95              &Gamma;, x:A, x:A |- R:B
96 Contraction: --------------------------
97              &Gamma;, x:A |- R:B
98
99            &Gamma; |- R:B
100 Weakening: --------------------- 
101            &Gamma;, x:A |- R:B     [x chosen fresh]
102
103 Logical Rules:
104
105          &Gamma;, x:A |- R:B
106 --> I:   -------------------------
107          &Gamma; |- \xM:A --> B  
108
109          &Gamma; |- f:(A --> B)      &Gamma; |- x:A
110 --> E:   -------------------------------------
111          &Gamma; |- (fx):B
112 </pre>
113
114 In these labeling rules, if a sequence &Gamma; in a premise contains
115 labeled formulas, those labels remain unchanged in the conclusion.
116
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.
120
121 Using these labeling rules, we can label the proof
122 just given:
123
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>
134
135 We have derived the *K* combinator, and typed it at the same time!
136
137 Need a proof that involves application, and a proof with cut that will
138 show beta reduction, so "normal" proof.
139
140 [To do: add pairs and destructors; unit and negation...]
141
142 Excercise: construct a proof whose labeling is the combinator S,
143 something like this:
144
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