edits

diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index cee3f91..a2cb3f5 100644 (file)
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -174,23 +174,25 @@ To see this, consider the first three Church numerals (starting with zero):
     \s z . s (s z)
 
 Given the internal structure of the term we are using to represent
     \s z . s (s z)
 
 Given the internal structure of the term we are using to represent

-zero, its type must have the form ρ --> σ --> $sigma; for
+zero, its type must have the form ρ --> σ --> σ for

 some ρ and σ.  This type is consistent with term for one,
 but the structure of the definition of one is more restrictive:
 some ρ and σ.  This type is consistent with term for one,
 but the structure of the definition of one is more restrictive:

-because the first argument `s` must apply to the second argument `z`,
-the type of the first argument must describe a function from
-expressions of type σ to some other type.  So we can refine ρ
-by replacing it with the more specific type σ --> τ.  At
-this point, the overall type is (σ --> τ) --> σ -->
+because the first argument (`s`) must apply to the second argument
+(`z`), the type of the first argument must describe a function from
+expressions of type σ to some result type.  So we can refine
+ρ by replacing it with the more specific type σ --> τ.
+At this point, the overall type is (σ --> τ) --> σ -->

 σ.  Note that this refined type remains compatible with the
 σ.  Note that this refined type remains compatible with the

-definition of zero.  Finally, by examinine the definition of two, we
+definition of zero.  Finally, by examinining the definition of two, we

 see that expressions of type τ must be suitable to serve as
 see that expressions of type τ must be suitable to serve as

-arguments to functions of type σ --> τ.  The most general
+arguments to functions of type σ --> τ, since the result of
+applying `s` to `z` serves as the argument of `s`.  The most general

 way for that to be true is if τ ≡ σ.  So at this
 way for that to be true is if τ ≡ σ.  So at this

-point, we have the overall type of (σ --> σ) --> σ -->
-σ.
-
+point, we have the overall type of (σ --> σ) --> σ
+--> σ.

 
 

+<!-- Make sure there is talk about unification and computation of the
+principle type-->

 
 ## Predecessor and lists are not representable in simply typed lambda-calculus ##
 
 
 ## Predecessor and lists are not representable in simply typed lambda-calculus ##