renamed curry-howard

[lambda.git] / curry-howard

diff --git a/curry-howard b/curry-howard
deleted file mode 100644 (file)
index f3c1be7..0000000
--- a/curry-howard
+++ /dev/null
@@ -1,166 +0,0 @@
-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):
-
-<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,
-something like this:
-
-           --------- Ax  --------- Ax   ------- Ax
-           !a --> !a     !b --> !b      c --> c
-           ----------------------- L->  -------- L!
-              !a,!a->!b --> !b          !c --> c
---------- Ax  ---------------------------------- L->
-!a --> !a           !a,!b->!c,!a->!b --> c
------------------------------------------- L->
-      !a,!a,!a->!b->!c,!a->!b --> c
-      ----------------------------- C!
-       !a,!a->!b->!c,!a->!b --> c
-       ------------------------------ L!
-       !a,!a->!b->!c,! (!a->!b) --> c
-       ---------------------------------- L!
-       !a,! (!a->!b->!c),! (!a->!b) --> c
-       ----------------------------------- R!
-       !a,! (!a->!b->!c),! (!a->!b) --> !c
-       ------------------------------------ R->
-       ! (!a->!b->!c),! (!a->!b) --> !a->!c
-       ------------------------------------- R->
-       ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
-       --------------------------------------- R->
-        --> ! (!a->!b)->! (!a->!b->!c)->!a->!c