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 &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 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