author Chris Barker Mon, 25 Oct 2010 13:32:42 +0000 (09:32 -0400) committer Chris Barker Mon, 25 Oct 2010 13:32:42 +0000 (09:32 -0400)
 curry-howard [new file with mode: 0644] patch | blob wadler-monads.pdf [new file with mode: 0644] patch | blob

diff --git a/curry-howard b/curry-howard
new file mode 100644 (file)
index 0000000..7840e37
--- /dev/null
@@ -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 &sigma; and term `M` has type &tau;, then
+the abstract `\xM` has type &sigma; `-->` &tau;.
+
+If a term `M` has type &sigma; `-->` &tau;, and a term `N` has type
+&sigma;, then the application `MN` has type &tau;.
+
+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):
+
+<pre>
+Axiom: ---------
+        A |- A
+
+Structural Rules:
+
+          &Gamma;, A, B, &Delta; |- C
+Exchange: ---------------------------
+          &Gamma;, B, A, &Delta; |- C
+
+             &Gamma;, A, A |- B
+Contraction: -------------------
+             &Gamma;, A |- B
+
+           &Gamma; |- B
+Weakening: -----------------
+           &Gamma;, A |- B
+
+Logical Rules:
+
+         &Gamma;, A |- B
+--> I:   -------------------
+         &Gamma; |- A --> B
+
+         &Gamma; |- A --> B         &Gamma; |- A
+--> E:   -----------------------------------
+         &Gamma; |- B
+</pre>
+
+`A`, `B`, etc. are variables over formulas.
+&Gamma;, &Delta;, etc. are variables over (possibly empty) sequences
+of formulas.  &Gamma; `|- A` is a sequent, and is interpreted as
+claiming that if each of the formulas in &Gamma; is true, then `A`
+must also be true.
+
+This logic allows derivations of theorems like the following:
+
+<pre>
+-------  Id
+A |- A
+---------- Weak
+A, B |- A
+------------- --> I
+A |- B --> A
+----------------- --> I
+|- A --> B --> A
+</pre>
+
+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:
+
+<pre>
+Axiom: -----------
+       x:A |- x:A
+
+Structural Rules:
+
+          &Gamma;, x:A, y:B, &Delta; |- R:C
+Exchange: -------------------------------
+          &Gamma;, y:B, x:A, &Delta; |- R:C
+
+             &Gamma;, x:A, x:A |- R:B
+Contraction: --------------------------
+             &Gamma;, x:A |- R:B
+
+           &Gamma; |- R:B
+Weakening: ---------------------
+           &Gamma;, x:A |- R:B     [x chosen fresh]
+
+Logical Rules:
+
+         &Gamma;, x:A |- R:B
+--> I:   -------------------------
+         &Gamma; |- \xM:A --> B
+
+         &Gamma; |- f:(A --> B)      &Gamma; |- x:A
+--> E:   -------------------------------------
+         &Gamma; |- (fx):B
+</pre>
+
+In these labeling rules, if a sequence &Gamma; 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:
+
+<pre>
+------------  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
+</pre>
+
+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.