(no commit message)

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 6b80c20..ae0b7e0 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -119,13 +119,13 @@ relevant evaluator is called "fullpoly"):
 
     N = ∀α. (α->α)->α->α;
     Pair = (N->N->N) -> N;
 
     N = ∀α. (α->α)->α->α;
     Pair = (N->N->N) -> N;

-    let zero = α . λs:α->α . λz:α. z in 
-    let fst = λx:N . λy:N . x in
-    let snd = λx:N . λy:N . y in
-    let pair = λx:N . λy:N . λz:N->N->N . z x y in
-    let suc = λn:N . λα . λlambda s:α->α . λz:α . s (n [α] s z) in
-    let shift = λp:Pair . pair (suc (p fst)) (p fst) in
-    let pre = λn:N . n [Pair] shift (pair zero zero) snd in
+    let zero = Î\9bα. λs:α->α . λz:α. z in 
+    let fst = λx:N. λy:N . x in
+    let snd = λx:N. λy:N . y in
+    let pair = λx:N. λy:N . λz:N->N->N . z x y in
+    let suc = λn:N. λα . λlambda s:α->α . λz:α. s (n [α] s z) in
+    let shift = λp:Pair. pair (suc (p fst)) (p fst) in
+    let pre = λn:N. n [Pair] shift (pair zero zero) snd in

 
     pre (suc (suc (suc zero)));
 
 
     pre (suc (suc (suc zero)));
 


@@ -165,19 +165,19 @@ Typing ω
 In fact, unlike in the simply-typed lambda calculus, 
 it is even possible to give a type for ω in System F. 
 
 In fact, unlike in the simply-typed lambda calculus, 
 it is even possible to give a type for ω in System F. 
 

-<code>&omega; = lambda x:(∀ α. α->α) . x [∀ α . α->α] x</code>
+<code>&omega; = λlambda x:(∀ α. α->α) . x [∀ α . α->α] x</code>

 
 In order to see how this works, we'll apply &omega; to the identity
 function.  
 
 <code>&omega; id ==</code>
 
 
 In order to see how this works, we'll apply &omega; to the identity
 function.  
 
 <code>&omega; id ==</code>
 

-    (lambda x:(∀ α . α->α) . x [∀ α . α->α] x) (lambda α . lambda x:α . x)
+    (λx:(∀α. α->α) . x [∀α.α->α] x) (Λα.λx:α. x)

 
 

-Since the type of the identity function is `(∀ α . α->α)`, it's the
+Since the type of the identity function is `∀α.α->α`, it's the

 right type to serve as the argument to &omega;.  The definition of
 &omega; instantiates the identity function by binding the type
 right type to serve as the argument to &omega;.  The definition of
 &omega; instantiates the identity function by binding the type

-variable `α` to the universal type `∀ α . α->α`.  Instantiating the
+variable `α` to the universal type `∀α.α->α`.  Instantiating the

 identity function in this way results in an identity function whose
 type is (in some sense, only accidentally) the same as the original
 fully polymorphic identity function.
 identity function in this way results in an identity function whose
 type is (in some sense, only accidentally) the same as the original
 fully polymorphic identity function.


@@ -228,10 +228,8 @@ uses.  Can we capture this using polymorphic types?
 
 With these basic types, we want to say something like this:
 
 
 With these basic types, we want to say something like this:
 

-    and:t->t->t = lambda l:t . lambda r:t . l r false
-    and = lambda α . lambda β . 
-            lambda l:α->β . lambda r:α->β . 
-              lambda x:α . and:β (l x) (r x)
+    and:t->t->t = λl:t. λr:t. l r false
+    and = Λα.Λβ.λl:α->β.λr:α->β.λx:α. and [β] (l x) (r x)

 
 The idea is that the basic *and* conjoins expressions of type `t`, and
 when *and* conjoins functional types, it builds a function that
 
 The idea is that the basic *and* conjoins expressions of type `t`, and
 when *and* conjoins functional types, it builds a function that