edits

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index ca6eb4c..d46981e 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -270,9 +270,9 @@ cannot have a type in Λ_T.  We can easily see why:
 
 Assume Ω has type τ, and `\x.xx` has type σ.  Then
 because `\x.xx` takes an argument of type σ and returns
 
 Assume Ω has type τ, and `\x.xx` has type σ.  Then
 because `\x.xx` takes an argument of type σ and returns

-something of type τ, `\x.xx` must also have type `σ -->
-τ`.  By repeating this reasoning, `\x.xx` must also have type
-`(σ --> τ) --> τ`; and so on.  Since variables have
+something of type τ, `\x.xx` must also have type σ -->
+τ.  By repeating this reasoning, `\x.xx` must also have type
+(σ --> τ) --> τ; and so on.  Since variables have

 finite types, there is no way to choose a type for the variable `x`
 that can satisfy all of the requirements imposed on it.
 
 finite types, there is no way to choose a type for the variable `x`
 that can satisfy all of the requirements imposed on it.
 


@@ -287,9 +287,9 @@ 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 σ, then `false`
 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 σ, then `false`

-has type τ --> τ --> &tau, for some τ.  Since one is
+has type τ --> τ --> τ, for some τ.  Since one is

 represented by the function `\x.x false 0`, one must have type (τ
 represented by the function `\x.x false 0`, one must have type (τ

---> τ --> &tau) --> &sigma --> σ.  But this is a different
+--> τ --> τ) --> σ --> σ.  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
 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