Date: Sun, 24 Oct 2010 22:10:28 -0400
Subject: [PATCH] added Curry-Howard
---
week6.mdwn | 135 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 135 insertions(+)
diff --git a/week6.mdwn b/week6.mdwn
index 221e0207..79b12f71 100644
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -171,3 +171,138 @@ We can use functions that take arguments of type unit to control
execution. In Scheme parlance, functions on the unit type are called
*thunks* (which I've always assumed was a blend of "think" and "chunk").
+Curry-Howard, take 1
+--------------------
+
+We will returnto 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 `σ --> &tau`, 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):
+
++Axiom: ---------
+ A |- A
+
+Structural Rules:
+
+Exchange: Γ, A, B, Δ |- C
+ ---------------------------
+ $Gamma;, B, A, Δ |- C
+
+Contraction: Γ, A, A |- B
+ -------------------
+ Γ, A |- B
+
+Weakening: Γ |- B
+ -----------------
+ Γ, A |- B
+
+Logical Rules:
+
+--> I: Γ, A |- B
+ -------------------
+ Γ |- A --> B
+
+--> E: Γ |- A --> B Γ |- A
+ -----------------------------------------
+ Γ |- B
+

+
+`A`, `B`, etc. are variables over formulas.
+Γ, Δ, etc. are variables over (possibly empty) sequences
+of formulas. `Γ |- A` is a sequent, and is interpreted as
+claiming that if each of the formulas in Γ is true, then `A`
+must also be true.
+
+This logic allows derivations of theorems like the following:
+
++------- Id
+A |- A
+---------- Weak
+A, B |- A
+------------- --> I
+A |- B --> A
+----------------- --> I
+|- A --> B --> A
+

+
+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:
+
++Axiom: -----------
+ x:A |- x:A
+
+Structural Rules:
+
+Exchange: Γ, x:A, y:B, Δ |- R:C
+ --------------------------------------
+ Γ, y:B, x:A, Δ |- R:C
+
+Contraction: Γ, x:A, x:A |- R:B
+ --------------------------
+ Γ, x:A |- R:B
+
+Weakening: Γ |- R:B
+ ---------------------
+ Γ, x:A |- R:B [x chosen fresh]
+
+Logical Rules:
+
+--> I: Γ, x:A |- R:B
+ -------------------------
+ Γ |- \xM:A --> B
+
+--> E: Γ |- f:(A --> B) Γ |- x:A
+ ---------------------------------------------
+ Γ |- (fx):B
+

+
+In these labeling rules, if a sequence Γ in a premise contains
+labeled formulas, those labels remain unchanged in the conclusion.
+
+Using these labeling rules, we can label the proof
+just given:
+
++------------ 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
+

+
+We have derived the *K* combinator, and typed it at the same time!
+
+[To do: add pairs and destructors; unit and negation...]
+
+Excercise: construct a proof whose labeling is the combinator S.
--
2.11.0