X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=8714eae88f924c42f7ba6560530d3094be741f07;hp=e01db2e857d5550eee64aa84f99860658b2fea47;hb=f4e64dfd73d6935c7636a1f4586b7d5202a74272;hpb=72af25c790aaa979710ffc2b7fab823ffaf94b05
diff --git a/week4.mdwn b/week4.mdwn
index e01db2e8..8714eae8 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -192,11 +192,10 @@ are also forbidden, so recursion is neither simple nor direct.
#Types#
-We will have at least one ground type, `o`. From a linguistic
-point of view, thing of the ground types as the bar-level 0
-categories, the lexical types, such as Noun, Verb, Preposition
-(glossing over the internal complexity of those categories in modern
-theories).
+We will have at least one ground type, `o`. From a linguistic point
+of view, think of the ground types as the bar-level 0 categories, that
+is, the lexical types, such as Noun, Verb, Preposition (glossing over
+the internal complexity of those categories in modern theories).
In addition, there will be a recursively-defined class of complex
types `T`, the smallest set such that
@@ -218,7 +217,7 @@ and so on.
#Typed lambda terms#
-Given a set of types `T`, we define the set of typed lambda terms `&Lamda;_T`,
+Given a set of types `T`, we define the set of typed lambda terms Λ_T
,
which is the smallest set such that
* each type `t` has an infinite set of distinct variables, {x^t}_1,
@@ -228,12 +227,12 @@ which is the smallest set such that
σ, then the application `(M N)` has type τ.
* If a variable `a` has type σ, and term `M` has type τ,
- then the abstract `λ a M` has type `σ --> τ`.
+ then the abstract λ a M
has type σ --> τ.
The definitions of types and of typed terms should be highly familiar
-to semanticists, except that instead of writing `σ --> τ`,
-linguists (following Montague, who followed Church) write `<σ,
-τ>`. We will use the arrow notation, since it is more iconic.
+to semanticists, except that instead of writing σ --> τ,
+linguists (following Montague, who followed Church) write <σ,
+τ>. We will use the arrow notation, since it is more iconic.
Some examples (assume that `x` has type `o`):