projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
f9bc566
)
added Curry-Howard
author
Chris Barker
<barker@omega.(none)>
Mon, 25 Oct 2010 02:12:16 +0000
(22:12 -0400)
committer
Chris Barker
<barker@omega.(none)>
Mon, 25 Oct 2010 02:12:16 +0000
(22:12 -0400)
week6.mdwn
patch
|
blob
|
history
diff --git
a/week6.mdwn
b/week6.mdwn
index
79b12f7
..
5f225d3
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
σ `-->` &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