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
15 If a variable `x` has type σ and term `M` has type τ, then
16 the abstract `\xM` has type σ `-->` τ.
18 If a term `M` has type σ `-->` τ, and a term `N` has type
19 σ, then the application `MN` has type τ.
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):
35 Γ, A, B, Δ |- C
36 Exchange: ---------------------------
37 Γ, B, A, Δ |- C
40 Contraction: -------------------
44 Weakening: -----------------
50 --> I: -------------------
53 Γ |- A --> B Γ |- A
54 --> E: -----------------------------------
58 `A`, `B`, etc. are variables over formulas.
59 Γ, Δ, etc. are variables over (possibly empty) sequences
60 of formulas. Γ `|- A` is a sequent, and is interpreted as
61 claiming that if each of the formulas in Γ is true, then `A`
64 This logic allows derivations of theorems like the following:
73 ----------------- --> I
77 Should remind you of simple types. (What was `A --> B --> A` the type
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:
91 Γ, x:A, y:B, Δ |- R:C
92 Exchange: -------------------------------
93 Γ, y:B, x:A, Δ |- R:C
95 Γ, x:A, x:A |- R:B
96 Contraction: --------------------------
100 Weakening: ---------------------
101 Γ, x:A |- R:B [x chosen fresh]
106 --> I: -------------------------
107 Γ |- \xM:A --> B
109 Γ |- f:(A --> B) Γ |- x:A
110 --> E: -------------------------------------
114 In these labeling rules, if a sequence Γ 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
121 Using these labeling rules, we can label the proof
127 ---------------- Weak
129 ------------------------- --> I
130 x:A |- (\y.x):(B --> A)
131 ---------------------------- --> I
132 |- (\x y. x):A --> B --> A
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,
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