@@ -217,7 +217,7 @@ and so on.

#Typed lambda terms#

-Given a set of types `T`, we define the set of typed lambda terms <code>&Lamda;_T</code>,
+Given a set of types `T`, we define the set of typed lambda terms <code>&Lambda;_T</code>,
which is the smallest set such that

*    each type `t` has an infinite set of distinct variables, {x^t}_1,
@@ -227,12 +227,12 @@ which is the smallest set such that
&sigma;, then the application `(M N)` has type &tau;.

*    If a variable `a` has type &sigma;, and term `M` has type &tau;,
-     then the abstract `&lambda; a M` has type `&sigma; --> &tau;`.
+     then the abstract <code>&lambda; a M</code> has type &sigma; --> &tau;.

The definitions of types and of typed terms should be highly familiar
-to semanticists, except that instead of writing `&sigma; --> &tau;`,
-linguists (following Montague, who followed Church) write `<&sigma;,
-&tau;>`.  We will use the arrow notation, since it is more iconic.
+to semanticists, except that instead of writing &sigma; --> &tau;,
+linguists (following Montague, who followed Church) write <&sigma;,
+&tau;>.  We will use the arrow notation, since it is more iconic.

Some examples (assume that `x` has type `o`):

@@ -254,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 &tau; in `&Lambda;_T`, then `M` has a
+If `M` is a term with type &tau; in &Lambda;_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 &Omega; does not have a normal form, it follows that &Omega;
-cannot have a type in `&Lambda;_T`.  We can easily see why:
+cannot have a type in &Lambda;_T.  We can easily see why:

&Omega; = (\x.xx)(\x.xx)

@@ -286,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 &sigma;, and `false`
-has type `&tau; --> &tau; --> &tau;` for some &tau;, and one is
-represented by the function `\x.x false 0`, then one must have type
-`(&tau; --> &tau; --> &tau) --> &sigma --> &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
+different type!  For instance, if zero has type &sigma;, then `false`
+has type &tau; --> &tau; --> &tau, for some &tau;.  Since one is
+represented by the function `\x.x false 0`, one must have type `(&tau;
+--> &tau; --> &tau) --> &sigma --> &sigma;`.  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 `(&sigma; --> &sigma;) -->
-&sigma; --> &sigma;`.
+types.  They can all be given the type (&sigma; --> &sigma;) -->
+&sigma; --> &sigma;.