added Curry-Howard

[lambda.git] / week6.mdwn

diff --git a/week6.mdwn b/week6.mdwn
index 79b12f7..f26285f 100644 (file)
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -174,7 +174,7 @@ execution.  In Scheme parlance, functions on the unit type are called
 Curry-Howard, take 1
 --------------------
 
-We will returnto the Curry-Howard correspondence a number of times
+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
@@ -186,9 +186,9 @@ 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 `σ --> τ`.
+the abstract `\xM` has type σ `-->` τ.
 
-If a term `M` has type `σ --> &tau`, and a term `N` 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
@@ -205,32 +205,32 @@ Axiom: ---------
 
 Structural Rules:
 
-Exchange: Γ, A, B, Δ |- C
-          ---------------------------
-          $Gamma;, B, A, Δ |- C
+          Γ, A, B, Δ |- C
+Exchange: ---------------------------
+          Γ, B, A, Δ |- C
 
-Contraction: Γ, A, A |- B
-             -------------------
+             Γ, A, A |- B
+Contraction: -------------------
              Γ, A |- B
 
-Weakening: Γ |- B
-           -----------------
+           Γ |- B
+Weakening: -----------------
            Γ, A |- B 
 
 Logical Rules:
 
---> I:   Γ, A |- B
-         -------------------
+         Γ, A |- B
+--> I:   -------------------
          Γ |- A --> B  
 
---> E:   Γ |- A --> B         Γ |- A
-         -----------------------------------------
+         Γ |- A --> B         Γ |- A
+--> E:   -----------------------------------
          Γ |- 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
+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.
 
@@ -261,32 +261,36 @@ Axiom: -----------
 
 Structural Rules:
 
-Exchange: &Gamma;, x:A, y:B, &Delta; |- R:C
-          --------------------------------------
+          &Gamma;, x:A, y:B, &Delta; |- R:C
+Exchange: -------------------------------
           &Gamma;, y:B, x:A, &Delta; |- R:C
 
-Contraction: &Gamma;, x:A, x:A |- R:B
-             --------------------------
+             &Gamma;, x:A, x:A |- R:B
+Contraction: --------------------------
              &Gamma;, x:A |- R:B
 
-Weakening: &Gamma; |- R:B
-           --------------------- 
+           &Gamma; |- R:B
+Weakening: --------------------- 
            &Gamma;, x:A |- R:B     [x chosen fresh]
 
 Logical Rules:
 
---> I:   &Gamma;, x:A |- R:B
-         -------------------------
+         &Gamma;, x:A |- R:B
+--> I:   -------------------------
          &Gamma; |- \xM:A --> B  
 
---> E:   &Gamma; |- f:(A --> B)      &Gamma; |- x:A
-         ---------------------------------------------
+         &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:
 
@@ -303,6 +307,9 @@ x:A |- (\y.x):(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.