curry-howard.mdwn

   1 Curry-Howard
   2 ------------
   3
   4 The Curry-Howard correspondence expresses a deep connection between
   5 logic, types, and computation.  Today we'll discuss how the
   6 simply-typed lambda calculus corresponds to intuitionistic logic.
   7 This naturally give rise to the question of what sort of computation
   8 classical logic corresponds to---as we'll see later, the answer
   9 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 &sigma; and term `M` has type &tau;, then
  16 the abstract `\xM` has type &sigma; `-->` &tau;.
  17
  18 If a term `M` has type &sigma; `-->` &tau;, and a term `N` has type
  19 &sigma;, then the application `MN` has type &tau;.
  20
  21 These rules are clearly inverse of one another (in some sense to be
  22 made precise): the functional types that abstract builds up are taken
  23 apart by application.  The intuition that abstraction and application
  24 are dual to each other is the heart of the Curry-Howard
  25 correspondence.
  26
  27 The next step in making sense out of the Curry-Howard corresponence is
  28 to present a logic.  It will be a part of intuitionistic logic.  We'll
  29 start with the implicational fragment, that is, the part of
  30 intuitionistic logic that only involves axioms and implications:
  31
  32 <pre>
  33 Axiom: ---------
  34         A |- A
  35
  36 Structural Rules:
  37
  38           &Gamma;, A, B, &Delta; |- C
  39 Exchange: ---------------------------
  40           &Gamma;, B, A, &Delta; |- C
  41
  42              &Gamma;, A, A |- B
  43 Contraction: -------------------
  44              &Gamma;, A |- B
  45
  46            &Gamma; |- B
  47 Weakening: -----------------
  48            &Gamma;, A |- B
  49
  50 Logical Rules:
  51
  52          &Gamma;, A |- B
  53 --> I:   -------------------
  54          &Gamma; |- A --> B
  55
  56          &Gamma; |- A --> B         &Gamma; |- A
  57 --> E:   -----------------------------------
  58          &Gamma; |- B
  59 </pre>
  60
  61 `A`, `B`, etc. are variables over formulas.
  62 &Gamma;, &Delta;, etc. are variables over (possibly empty) sequences
  63 of formulas.  &Gamma; `|- A` is a sequent, and is interpreted as
  64 claiming that if each of the formulas in &Gamma; is true, then `A`
  65 must also be true.
  66
  67 This logic allows derivations of theorems like the following:
  68
  69 <pre>
  70 -------  Id
  71 A |- A
  72 ---------- Weak
  73 A, B |- A
  74 ------------- --> I
  75 A |- B --> A
  76 ----------------- --> I
  77 |- A --> B --> A
  78 </pre>
  79
  80 Should remind you of simple types.  (What was `A --> B --> A` the type
  81 of again?)
  82
  83 The easy way to grasp the Curry-Howard correspondence is to *label*
  84 the proofs.  Since we wish to establish a correspondence between this
  85 logic and the lambda calculus, the labels will all be terms from the
  86 simply-typed lambda calculus.  Here are the labeling rules:
  87
  88 <pre>
  89 Axiom: -----------
  90        x:A |- x:A
  91
  92 Structural Rules:
  93
  94           &Gamma;, x:A, y:B, &Delta; |- R:C
  95 Exchange: -------------------------------
  96           &Gamma;, y:B, x:A, &Delta; |- R:C
  97
  98              &Gamma;, x:A, x:A |- R:B
  99 Contraction: --------------------------
 100              &Gamma;, x:A |- R:B
 101
 102            &Gamma; |- R:B
 103 Weakening: ---------------------
 104            &Gamma;, x:A |- R:B     [x chosen fresh]
 105
 106 Logical Rules:
 107
 108          &Gamma;, x:A |- R:B
 109 --> I:   -------------------------
 110          &Gamma; |- \xM:A --> B
 111
 112          &Gamma; |- f:(A --> B)      &Gamma; |- x:A
 113 --> E:   -------------------------------------
 114          &Gamma; |- (fx):B
 115 </pre>
 116
 117 In these labeling rules, if a sequence &Gamma; in a premise contains
 118 labeled formulas, those labels remain unchanged in the conclusion.
 119
 120 What is means for a variable `x` to be chosen *fresh* is that
 121 `x` must be distinct from any other variable in any of the labels
 122 used in the (sub)proof up to that point.
 123
 124 Using these labeling rules, we can label the proof
 125 just given:
 126
 127 <pre>
 128 ------------  Id
 129 x:A |- x:A
 130 ---------------- Weak
 131 x:A, y:B |- x:A
 132 ------------------------- --> I
 133 x:A |- (\y.x):(B --> A)
 134 ---------------------------- --> I
 135 |- (\x y. x):A --> B --> A
 136 </pre>
 137
 138 We have derived the *K* combinator, and typed it at the same time!
 139
 140 In order to make use of the dual rule, the one for `-->` elimination,
 141 we need a context that will entail both `A --> B` and `A`.  Here's
 142 one, first without labels:
 143
 144 <pre>
 145 ------------------Axiom
 146 A --> B |- A --> B
 147 ---------------------Weak        ---------Axiom
 148 A --> B, A |- A --> B              A |- A
 149 ---------------------Exch        -----------------Weak
 150 A, A --> B |- A --> B              A, A --> B |- A
 151 -------------------------------------------------- --> E
 152 A, A --> B |- B
 153 </pre>
 154
 155 With labels, we have
 156
 157 <pre>
 158 ------------------------Axiom
 159 f:A --> B |- f:A --> B
 160 ----------------------------Weak        -------------Axiom
 161 f:A --> B, x:A |- f:A --> B              x:A |- x:A
 162 ----------------------------Exch        ------------------------Weak
 163 x:A, f:A --> B |- f:A --> B              x:A, f:A --> B |- x:A
 164 -------------------------------------------------------------- --> E
 165 x:A, f:A --> B |- (fx):B
 166 </pre>
 167
 168 Note that in order for the `--> E` rule to apply, the left context and
 169 the right context (the material to the left of each of the turnstiles)
 170 must match exactly, in this case, `x:A, f:A --> B`.
 171
 172 At this point, an application to natural language will help provide
 173 insight.
 174 Instead of labelling the proof above with the kinds of symbols we
 175 might use in a program, we'll label it with symbols we might use in an
 176 English sentence.  Instead of a term `f` with type `A --> B`, we'll
 177 have the English word `left`; and instead of a term `x` with type `A`,
 178 we'll have the English word `John`.
 179
 180 <pre>
 181 -----------------------------Axiom
 182 left:e --> t |- left:e --> t
 183 --------------------------------------Weak        -------------------Axiom
 184 left:e --> t, John:e |- left:e --> t              John:e |- John:e
 185 --------------------------------------Exch        --------------------------------Weak
 186 John:e, left:e --> t |- left:e --> t              John:e, left:e --> t |- John:e
 187 ---------------------------------------------------------------------------------- --> E
 188 John:e, left:e --> t |- (left John):t
 189 </pre>
 190
 191 This proof illustrates how a logic can
 192 provide three things that a complete grammar of a natural language
 193 needs:
 194
 195 * It characterizes which words and expressions can be combined in
 196 order to form a more complex expression.  For instance, we've
 197 just seen a proof that "left" can combine with "John".
 198
 199 * It characterizes the type (the syntactic category) of the result.
 200 In the example, an intransitive verb phrase of type `e --> t` combines
 201 with a determiner phrase of type `e` to form a sentence of type `t`.
 202
 203 * It characterizes the semantic recipe required to compute the meaning
 204   of the complex expression based on the meanings of the parts: the
 205   way to compute to meaning of the expression "John left" is to take
 206   the function denoted by "left" and apply it to the individual
 207   denoted by "John", viz., "(left John)".
 208
 209 This last point is the truly novel and beautiful part, the part
 210 contributed by the Curry-Howard result.
 211
 212 [Incidentally, note that this proof also suggests that if we have the
 213 expressions "John" followed by "left", we also have a determiner
 214 phrase of type `e`.  If you want to make sure that the contribution of
 215 each word counts (no weakening), you have to use a resource-sensitive
 216 approach like Linear Logic or Type Logical Grammar.
 217
 218 In this trivial example, it may not be obvious that anything
 219 interesting is going on, so let's look at a slightly more complicated
 220 example, one that combines abstraction with application.
 221
 222 Linguistic assumptions (abundently well-motivated, but we won't pause
 223 to review the motivations here):
 224
 225 Assumption 1:
 226 Coordinating conjunctions like *and*, *or*, and *but* require that
 227 their two arguments must have the same sytnactic type.  Thus we can
 228 have
 229
 230 <pre>
 231 1. [John left] or [Mary left]     coordination of t
 232 2. John [left] or [slept]         coordination of e -> t
 233 3. [John] or [Mary] left          coordination of e
 234 etc.
 235
 236 4. *John or left.
 237 5. *left or Mary slept.
 238 etc.
 239 </pre>
 240
 241 If the two disjuncts have the same type, the coordination is perfectly
 242 fine, as (1) through (3) illustrate.  But when the disjuncts don't
 243 match, as in (4) and (5), the result is ungrammatical (though there
 244 are examples that may seem to work; each usually has a linguistic
 245 story that needs to be told).
 246
 247 In general, then, *and* and *or* are polymorphic, and have the type
 248 `and:('a -> 'a -> 'a)`.  In the discussion below, we'll use a more
 249 specific instance to keep the discussion concrete, and to abstract
 250 away from polymorphism.
 251
 252 Assumption 2:
 253 Some determiner phrases do not denote an indivdual of type `e`, and
 254 denote only functions of a higher type, typically `(e -> t) -> t` (the
 255 type of an (extensional) generalized quantifier).  So *John* has type
 256 `e`, but *everyone* has type `(e -> t) -> t`.
 257
 258 [Excercise: prove using the logic above that *Everyone left* can have
 259 `(everyone left)` as its Curry-Howard labeling.]
 260
 261 The puzzle, then, is how it can be possible to coordinate generalized
 262 quantifier determiner phrases with non-generalized quantifier
 263 determiner phrases:
 264
 265 1. John and every girl laughed.
 266 2. Some boy or Mary should leave.
 267
 268 The answer involves reasoning about what it means to be an individual.
 269
 270 Let the type of *or* in this example be `Q -> Q -> Q`, where
 271 `Q` is the type of a generalized quantifier, i.e, `Q = ((e->t)->t`.
 272
 273 <pre>
 274 -----------------Ax  -----------------Ax
 275 John:e |- John:e     P:e->t |- P:e->t
 276 --------------------------------------Modus Ponens (proved above)
 277 John:e, P:e->t |- (P John):t
 278 --------------------------------- --> I
 279 John:e |- (\P.P John):(e->t)->t
 280 </pre>
 281
 282 This proof is very interesting: it says that if *John* has type `e`,
 283 then *John* automatically can be used as if it also has type
 284 `(e->t)->t`, the type of a generalized quantifier.
 285 The Curry-Howard labeling is the term `\P.P John`, which is a function
 286 from verb phrase meanings to truth values, just as we would need.
 287
 288 [John and everyone left]
 289
 290 beta reduction = normal proof.
 291
 292 [To do: add pairs and destructors; unit and negation...]
 293
 294 Excercise: construct a proof whose labeling is the combinator S,
 295 something like this:
 296
 297 <pre>
 298            --------- Ax  --------- Ax   ------- Ax
 299            !a --> !a     !b --> !b      c --> c
 300            ----------------------- L->  -------- L!
 301               !a,!a->!b --> !b          !c --> c
 302 --------- Ax  ---------------------------------- L->
 303 !a --> !a           !a,!b->!c,!a->!b --> c
 304 ------------------------------------------ L->
 305       !a,!a,!a->!b->!c,!a->!b --> c
 306       ----------------------------- C!
 307        !a,!a->!b->!c,!a->!b --> c
 308        ------------------------------ L!
 309        !a,!a->!b->!c,! (!a->!b) --> c
 310        ---------------------------------- L!
 311        !a,! (!a->!b->!c),! (!a->!b) --> c
 312        ----------------------------------- R!
 313        !a,! (!a->!b->!c),! (!a->!b) --> !c
 314        ------------------------------------ R->
 315        ! (!a->!b->!c),! (!a->!b) --> !a->!c
 316        ------------------------------------- R->
 317        ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
 318        --------------------------------------- R->
 319         --> ! (!a->!b)->! (!a->!b->!c)->!a->!c
 320 </pre>
 321
 322 See also
 323 [Wadler's symmetric
 324 calculus](http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf), and
 325 [[http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism]].