From 8e8edc03022be0da1621d6f1b418919c2637856e Mon Sep 17 00:00:00 2001
From: Chris Barker <barker@omega.(none)>
Date: Sun, 24 Oct 2010 22:32:22 -0400
Subject: [PATCH 1/1] added Curry-Howard

---
 week6.mdwn | 37 ++++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

diff --git a/week6.mdwn b/week6.mdwn
index 5f225d36..57158c6b 100644
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -188,7 +188,7 @@ 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
+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
@@ -205,32 +205,32 @@ Axiom: ---------
 
 Structural Rules:
 
-Exchange: &Gamma;, A, B, &Delta; |- C
-          ---------------------------
-          $Gamma;, B, A, &Delta; |- C
+          &Gamma;, A, B, &Delta; |- C
+Exchange: ---------------------------
+          &Gamma;, B, A, &Delta; |- C
 
-Contraction: &Gamma;, A, A |- B
-             -------------------
+             &Gamma;, A, A |- B
+Contraction: -------------------
              &Gamma;, A |- B
 
-Weakening: &Gamma; |- B
-           -----------------
+           &Gamma; |- B
+Weakening: -----------------
            &Gamma;, A |- B 
 
 Logical Rules:
 
---> I:   &Gamma;, A |- B
-         -------------------
+         &Gamma;, A |- B
+--> I:   -------------------
          &Gamma; |- A --> B  
 
---> E:   &Gamma; |- A --> B         &Gamma; |- A
-         -----------------------------------------
+         &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
+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.
 
@@ -262,7 +262,7 @@ Axiom: -----------
 Structural Rules:
 
 Exchange: &Gamma;, x:A, y:B, &Delta; |- R:C
-          --------------------------------------
+          -------------------------------
           &Gamma;, y:B, x:A, &Delta; |- R:C
 
 Contraction: &Gamma;, x:A, x:A |- R:B
@@ -280,13 +280,17 @@ Logical Rules:
          &Gamma; |- \xM:A --> B  
 
 --> E:   &Gamma; |- f:(A --> B)      &Gamma; |- x:A
-         ---------------------------------------------
+         -------------------------------------
          &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.
-- 
2.11.0