projects
/
lambda.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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
--------------------
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
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
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
σ, 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:
---------------------------
+
&
Gamma;, 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.
Γ, Δ, etc. are variables over (possibly empty) sequences
Γ |- B
</pre>
`A`, `B`, etc. are variables over formulas.
Γ, Δ, etc. are variables over (possibly empty) sequences
-of formulas.
`Γ
|- A` is a sequent, and is interpreted as
+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.
claiming that if each of the formulas in Γ is true, then `A`
must also be true.
@@
-261,32
+261,36
@@
Axiom: -----------
Structural Rules:
Structural Rules:
-
Exchange:
Γ, x:A, y:B, Δ |- R:C
-
-------
-------------------------------
+
Γ, x:A, y:B, Δ |- R:C
+
Exchange:
-------------------------------
Γ, y:B, x:A, Δ |- R:C
Γ, y:B, x:A, Δ |- R:C
-
Contraction:
Γ, x:A, x:A |- R:B
-
--------------------------
+
Γ, x:A, x:A |- R:B
+
Contraction:
--------------------------
Γ, x:A |- R:B
Γ, x:A |- R:B
-
Weakening:
Γ |- R:B
-
---------------------
+
Γ |- R:B
+
Weakening:
---------------------
Γ, x:A |- R:B [x chosen fresh]
Logical Rules:
Γ, x:A |- R:B [x chosen fresh]
Logical Rules:
-
--> I:
Γ, x:A |- R:B
-
-------------------------
+
Γ, x:A |- R:B
+
--> I:
-------------------------
Γ |- \xM:A --> B
Γ |- \xM:A --> B
-
--> E:
Γ |- f:(A --> B) Γ |- x:A
-
--------
-------------------------------------
+
Γ |- f:(A --> B) Γ |- x:A
+
--> E:
-------------------------------------
Γ |- (fx):B
</pre>
In these labeling rules, if a sequence Γ in a premise contains
labeled formulas, those labels remain unchanged in the conclusion.
Γ |- (fx):B
</pre>
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:
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.