added Curry-Howard

[lambda.git] / week6.mdwn

diff --git a/week6.mdwn b/week6.mdwn
index 5f225d3..57158c6 100644 (file)
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -188,7 +188,7 @@ roughly as follows:
 If a variable `x` has type σ and term `M` has type τ, then 
 the abstract `\xM` has type σ `-->` τ.
 
 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
+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
 σ, then the application `MN` has type τ.
 
 These rules are clearly obverses of one another: the functional types


@@ -205,32 +205,32 @@ Axiom: ---------
 
 Structural Rules:
 
 
 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
 
              Γ, A |- B
 

-Weakening: Γ |- B
-           -----------------
+           Γ |- B
+Weakening: -----------------

            Γ, A |- B 
 
 Logical Rules:
 
            Γ, A |- B 
 
 Logical Rules:
 

---> I:   Γ, A |- B
-         -------------------
+         Γ, A |- B
+--> I:   -------------------

          Γ |- A --> B  
 
          Γ |- 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
          &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.
 
 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
 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
           &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; |- \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.
 
          &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:
 
 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!
 
 
 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.
 [To do: add pairs and destructors; unit and negation...]
 
 Excercise: construct a proof whose labeling is the combinator S.