X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=week4.mdwn;h=b7ff879082a8bb7f11fe2907df3a59ed908977e1;hb=6dffa91feff41dc4736d907bf59c3a76a3c8d50f;hp=e01db2e857d5550eee64aa84f99860658b2fea47;hpb=72af25c790aaa979710ffc2b7fab823ffaf94b05;p=lambda.git
diff --git a/week4.mdwn b/week4.mdwn
index e01db2e8..b7ff8790 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`):
@@ -255,17 +254,17 @@ Types, *THEREFORE*, are right associative: if `f`, `x`, `y`, and `z`
have types `a`, `b`, `c`, and `d`, respectively, then `f` has type `a
--> b --> c --> d == (a --> (b --> (c --> d)))`.
-It is a serious faux pas to associate to the left for types, on a par
-with using your salad fork to stir your tea.
+It is a serious faux pas to associate to the left for types. You may
+as well use your salad fork to stir your tea.
#The simply-typed lambda calculus is strongly normalizing#
-If `M` is a term with type τ in `Λ_T`, then `M` has a
+If `M` is a term with type τ in Λ_T, then `M` has a
normal form. The proof is not particularly complex, but we will not
present it here; see Berendregt or Hankin.
Since Ω does not have a normal form, it follows that Ω
-cannot have a type in `Λ_T`. We can easily see why:
+cannot have a type in Λ_T. We can easily see why:
Ω = (\x.xx)(\x.xx)
@@ -287,16 +286,16 @@ functions, one for each type.
Version 1 type numerals are not a good choice for the simply-typed
lambda calculus. The reason is that each different numberal has a
-different type! For instance, if zero has type σ, and `false`
-has type `τ --> τ --> τ` for some τ, and one is
-represented by the function `\x.x false 0`, then one must have type
-`(τ --> τ --> &tau) --> &sigma --> σ`. But this is a
-different type than zero! Because numbers have different types, it
-becomes impossible to write arithmetic operations that can combine
-zero with one. We would need as many different addition operations as
-we had pairs of numbers that we wanted to add.
+different type! For instance, if zero has type σ, then `false`
+has type τ --> τ --> &tau, for some τ. Since one is
+represented by the function `\x.x false 0`, one must have type (τ
+--> τ --> τ) --> σ --> σ. But this is a different
+type than zero! Because each number has a different type, it becomes
+impossible to write arithmetic operations that can combine zero with
+one. We would need as many different addition operations as we had
+pairs of numbers that we wanted to add.
Fortunately, the Church numberals are well behaved with respect to
-types. They can all be given the type `(σ --> σ) -->
-σ --> σ`.
+types. They can all be given the type (σ --> σ) -->
+σ --> σ.