X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=7cd8a921dbfebc07558180aa7717a3b83e0cd0d5;hp=8714eae88f924c42f7ba6560530d3094be741f07;hb=5dad3bae051905473c6cc3d01bf261cbcce0968e;hpb=f4e64dfd73d6935c7636a1f4586b7d5202a74272;ds=sidebyside

diff --git a/week4.mdwn b/week4.mdwn
index 8714eae8..7cd8a921 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -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 τ 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)
 
@@ -286,14 +286,14 @@ 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 `(τ
+--> τ --> &tau) --> &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 `(σ --> σ) -->