X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=curry-howard.mdwn;h=183b54ebb463fb1cae33283053dc6703c15860dc;hb=HEAD;hp=f3c1be7590eb348711cee3bd4d25e993f1272749;hpb=ac6c32595e75ae0d3aa0631be7df6ca758626d56;p=lambda.git
diff --git a/curry-howard.mdwn b/curry-howard.mdwn
deleted file mode 100644
index f3c1be75..00000000
--- a/curry-howard.mdwn
+++ /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):
-
-
-Axiom: ---------
- A |- A
-
-Structural Rules:
-
- Γ, A, B, Δ |- C
-Exchange: ---------------------------
- Γ, B, A, Δ |- C
-
- Γ, A, A |- B
-Contraction: -------------------
- Γ, A |- B
-
- Γ |- B
-Weakening: -----------------
- Γ, A |- B
-
-Logical Rules:
-
- Γ, A |- B
---> I: -------------------
- Γ |- A --> B
-
- Γ |- A --> B Γ |- A
---> E: -----------------------------------
- Γ |- 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:
-
- Γ, x:A, y:B, Δ |- R:C
-Exchange: -------------------------------
- Γ, y:B, x:A, Δ |- R:C
-
- Γ, x:A, x:A |- R:B
-Contraction: --------------------------
- Γ, x:A |- R:B
-
- Γ |- R:B
-Weakening: ---------------------
- Γ, x:A |- R:B [x chosen fresh]
-
-Logical Rules:
-
- Γ, x:A |- R:B
---> I: -------------------------
- Γ |- \xM:A --> B
-
- Γ |- f:(A --> B) Γ |- x:A
---> E: -------------------------------------
- Γ |- (fx):B
-
-
-In these labeling rules, if a sequence Γ 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:
-
-
------------- 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!
-
-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