projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
4cc40e4
)
added Curry-Howard
author
Chris Barker
<barker@omega.(none)>
Mon, 25 Oct 2010 02:32:22 +0000
(22:32 -0400)
committer
Chris Barker
<barker@omega.(none)>
Mon, 25 Oct 2010 02:32:22 +0000
(22:32 -0400)
week6.mdwn
patch
|
blob
|
history
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 σ `-->` &tau
;
, 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.
@@
-262,7
+262,7
@@
Axiom: -----------
Structural Rules:
Exchange: Γ, x:A, y:B, Δ |- R:C
Structural Rules:
Exchange: Γ, x:A, y:B, Δ |- R:C
- -------------------------------
-------
+ -------------------------------
Γ, y:B, x:A, Δ |- R:C
Contraction: Γ, x:A, x:A |- R:B
Γ, y:B, x:A, Δ |- R:C
Contraction: Γ, x:A, x:A |- R:B
@@
-280,13
+280,17
@@
Logical Rules:
Γ |- \xM:A --> B
--> E: Γ |- f:(A --> B) Γ |- x:A
Γ |- \xM:A --> B
--> E: Γ |- f:(A --> B) Γ |- x:A
- -------------------------------------
--------
+ -------------------------------------
Γ |- (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.