X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=curry-howard;fp=curry-howard;h=7840e37716f9307fe64d6bb005007bf7cd4f57a1;hp=0000000000000000000000000000000000000000;hb=37309e8fca0040224958bf089c024d301e39de09;hpb=e735d4bc20d0d6147ca24de3ce4bf0843bd2ab17 diff --git a/curry-howard b/curry-howard new file mode 100644 index 00000000..7840e377 --- /dev/null +++ b/curry-howard @@ -0,0 +1,142 @@ +Curry-Howard, take 1 +-------------------- + +We will return to the Curry-Howard correspondence a number of times +during this course. It expresses a deep connection between logic, +types, and computation. Today we'll discuss how the simply-typed +lambda calculus corresponds to intuitionistic logic. This naturally +give rise to the question of what sort of computation classical logic +corresponds to---as we'll see later, the answer involves continuations. + +So at this point we have the simply-typed lambda calculus: a set of +ground types, a set of functional types, and some typing rules, given +roughly as follows: + +If a variable `x` has type σ and term `M` has type τ, then +the abstract `\xM` has type σ `-->` τ. + +If a term `M` has type σ `-->` τ, and a term `N` has type +σ, then the application `MN` has type τ. + +These rules are clearly obverses of one another: the functional types +that abstract builds up are taken apart by application. + +The next step in making sense out of the Curry-Howard corresponence is +to present a logic. It will be a part of intuitionistic logic. We'll +start with the implicational fragment (that is, the part of +intuitionistic logic that only involves axioms and implications): + +
+Axiom: --------- + A |- A + +Structural Rules: + + Γ, A, B, Δ |- C +Exchange: --------------------------- + Γ, B, A, Δ |- C + + Γ, A, A |- B +Contraction: ------------------- + Γ, A |- B + + Γ |- B +Weakening: ----------------- + Γ, A |- B + +Logical Rules: + + Γ, A |- B +--> I: ------------------- + Γ |- A --> B + + Γ |- A --> B Γ |- A +--> E: ----------------------------------- + Γ |- B ++ +`A`, `B`, etc. are variables over formulas. +Γ, Δ, etc. are variables over (possibly empty) sequences +of formulas. Γ `|- A` is a sequent, and is interpreted as +claiming that if each of the formulas in Γ is true, then `A` +must also be true. + +This logic allows derivations of theorems like the following: + +
+------- Id +A |- A +---------- Weak +A, B |- A +------------- --> I +A |- B --> A +----------------- --> I +|- A --> B --> A ++ +Should remind you of simple types. (What was `A --> B --> A` the type +of again?) + +The easy way to grasp the Curry-Howard correspondence is to *label* +the proofs. Since we wish to establish a correspondence between this +logic and the lambda calculus, the labels will all be terms from the +simply-typed lambda calculus. Here are the labeling rules: + +
+Axiom: ----------- + x:A |- x:A + +Structural Rules: + + Γ, x:A, y:B, Δ |- R:C +Exchange: ------------------------------- + Γ, y:B, x:A, Δ |- R:C + + Γ, x:A, x:A |- R:B +Contraction: -------------------------- + Γ, x:A |- R:B + + Γ |- R:B +Weakening: --------------------- + Γ, x:A |- R:B [x chosen fresh] + +Logical Rules: + + Γ, x:A |- R:B +--> I: ------------------------- + Γ |- \xM:A --> B + + Γ |- f:(A --> B) Γ |- x:A +--> E: ------------------------------------- + Γ |- (fx):B ++ +In these labeling rules, if a sequence Γ in a premise contains +labeled formulas, those labels remain unchanged in the conclusion. + +What is means for a variable `x` to be chosen *fresh* is that +`x` must be distinct from any other variable in any of the labels +used in the proof. + +Using these labeling rules, we can label the proof +just given: + +
+------------ Id +x:A |- x:A +---------------- Weak +x:A, y:B |- x:A +------------------------- --> I +x:A |- (\y.x):(B --> A) +---------------------------- --> I +|- (\x y. x):A --> B --> A ++ +We have derived the *K* combinator, and typed it at the same time! + +Need a proof that involves application, and a proof with cut that will +show beta reduction, so "normal" proof. + +[To do: add pairs and destructors; unit and negation...] + +Excercise: construct a proof whose labeling is the combinator S.