X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week6.mdwn;h=5f225d3628da01602119b189c9a9476c4dbf3c67;hp=1839455a6542b7df4b9339222295d6f871b14358;hb=4cc40e4c5ca2646b579213ee40f2caa794a3a474;hpb=80ad862c64373ac07b6e33236a47a50e98583d62 diff --git a/week6.mdwn b/week6.mdwn index 1839455a..5f225d36 100644 --- a/week6.mdwn +++ b/week6.mdwn @@ -44,9 +44,10 @@ Oh well. Booleans in OCAML, and simple pattern matching ---------------------------------------------- -Where we would write `true 1 2` and expect it to evaluate to `1`, in -OCAML boolean types are not functions (equivalently, are functions -that take zero arguments). Choices are made as follows: +Where we would write `true 1 2` in our pure lambda calculus and expect +it to evaluate to `1`, in OCAML boolean types are not functions +(equivalently, are functions that take zero arguments). Selection is +accomplished as follows: # if true then 1 else 2;; - : int = 1 @@ -69,8 +70,8 @@ Compare with # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;; - : int = 9 -Unit ----- +Unit and thunks +--------------- All functions in OCAML take exactly one argument. Even this one: @@ -135,7 +136,7 @@ Oh, one more thing: lambda expressions look like this: # (fun x -> x);; - : 'a -> 'a = # (fun x -> x) true;; - - : book = true + - : bool = true (But `(fun x -> x x)` still won't work.) @@ -152,7 +153,7 @@ reverse the order of the arguments: Infinite loop. -Now consider the following differences: +Now consider the following variations in behavior: # let test = omega omega;; [Infinite loop, need to control c out] @@ -170,3 +171,138 @@ We can use functions that take arguments of type unit to control execution. In Scheme parlance, functions on the unit type are called *thunks* (which I've always assumed was a blend of "think" and "chunk"). +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 σ `-->` &tau, 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:
+
+Exchange: Γ, A, B, Δ |- C
+          ---------------------------
+          $Gamma;, B, A, Δ |- C
+
+Contraction: Γ, A, A |- B
+             -------------------
+             Γ, A |- B
+
+Weakening: Γ |- B
+           -----------------
+           Γ, A |- B 
+
+Logical Rules:
+
+--> I:   Γ, A |- B
+         -------------------
+         Γ |- A --> B  
+
+--> E:   Γ |- A --> B         Γ |- A
+         -----------------------------------------
+         Γ |- 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:
+
+Exchange: Γ, x:A, y:B, Δ |- R:C
+          --------------------------------------
+          Γ, y:B, x:A, Δ |- R:C
+
+Contraction: Γ, x:A, x:A |- R:B
+             --------------------------
+             Γ, x:A |- R:B
+
+Weakening: Γ |- R:B
+           --------------------- 
+           Γ, x:A |- R:B     [x chosen fresh]
+
+Logical Rules:
+
+--> I:   Γ, x:A |- R:B
+         -------------------------
+         Γ |- \xM:A --> B  
+
+--> E:   Γ |- f:(A --> B)      Γ |- x:A
+         ---------------------------------------------
+         Γ |- (fx):B
+
+ +In these labeling rules, if a sequence Γ in a premise contains +labeled formulas, those labels remain unchanged in the conclusion. + +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! + +[To do: add pairs and destructors; unit and negation...] + +Excercise: construct a proof whose labeling is the combinator S.