(no commit message)

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index a80cc58..f7c38eb 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -117,13 +117,13 @@ however.  Here is one way, coded in
 System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
 relevant evaluator is called "fullpoly"):
 
 System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
 relevant evaluator is called "fullpoly"):
 

-    N = All X . (X->X)->X->X;
+    N = ∀ α . (α->α)->α->α;

     Pair = (N -> N -> N) -> N;
     Pair = (N -> N -> N) -> N;

-    let zero = lambda X . lambda s:X->X . lambda z:X. z in 
+    let zero = lambda α . lambda s:α->α . lambda z:α. z in 

     let fst = lambda x:N . lambda y:N . x in
     let snd = lambda x:N . lambda y:N . y in
     let pair = lambda x:N . lambda y:N . lambda z:N->N->N . z x y in
     let fst = lambda x:N . lambda y:N . x in
     let snd = lambda x:N . lambda y:N . y in
     let pair = lambda x:N . lambda y:N . lambda z:N->N->N . z x y in

-    let suc = lambda n:N . lambda X . lambda s:X->X . lambda z:X . s (n [X] s z) in
+    let suc = lambda n:N . lambda α . lambda s:α->α . lambda z:α . s (n [α] s z) in

     let shift = lambda p:Pair . pair (suc (p fst)) (p fst) in
     let pre = lambda n:N . n [Pair] shift (pair zero zero) snd in
 
     let shift = lambda p:Pair . pair (suc (p fst)) (p fst) in
     let pre = lambda n:N . n [Pair] shift (pair zero zero) snd in
 


@@ -138,7 +138,7 @@ lambda).
 
 The key to the extra expressive power provided by System F is evident
 in the typing imposed by the definition of `pre`.  The variable `n` is
 
 The key to the extra expressive power provided by System F is evident
 in the typing imposed by the definition of `pre`.  The variable `n` is

-typed as a Church number, i.e., as `All X . (X->X)->X->X`.  The type
+typed as a Church number, i.e., as `∀ α . (α->α)->α->α`.  The type

 application `n [Pair]` instantiates `n` in a way that allows it to
 manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`.  In
 other words, the instantiation turns a Church number into a
 application `n [Pair]` instantiates `n` in a way that allows it to
 manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`.  In
 other words, the instantiation turns a Church number into a


@@ -151,8 +151,8 @@ that the ordered pairs we need here are pairs of numbers.  If we tried
 to replace the type for Church numbers with a concrete (simple) type,
 we would have to replace each `X` with the type for Pairs, `(N -> N ->
 N) -> N`.  But then we'd have to replace each of these `N`'s with the
 to replace the type for Church numbers with a concrete (simple) type,
 we would have to replace each `X` with the type for Pairs, `(N -> N ->
 N) -> N`.  But then we'd have to replace each of these `N`'s with the

-type for Church numbers, `(X -> X) -> X -> X`.  And then we'd have to
-replace each of these `X`'s with... ad infinitum.  If we had to choose
+type for Church numbers, `(α -> α) -> α -> α`.  And then we'd have to
+replace each of these `α`'s with... ad infinitum.  If we had to choose

 a concrete type built entirely from explicit base types, we'd be
 unable to proceed.
  
 a concrete type built entirely from explicit base types, we'd be
 unable to proceed.
  


@@ -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:(All X. X->X) . x [All X . 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:(All X . X->X) . x [All X . X->X] x) (lambda X . lambda x:X . x)
+    (lambda x:(∀ α . α->α) . x [∀ α . α->α] x) (lambda α . lambda x:α . x)

 
 

-Since the type of the identity function is `(All X . X->X)`, 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 `X` to the universal type `All X . X->X`.  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.


@@ -229,9 +229,9 @@ uses.  Can we capture this using polymorphic types?
 With these basic types, we want to say something like this:
 
     and:t->t->t = lambda l:t . lambda r:t . l r false
 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 'a . lambda 'b . 
-            lambda l:'a->'b . lambda r:'a->'b . 
-              lambda x:'a . and:'b (l x) (r x)
+    and = lambda α . lambda β . 
+            lambda l:α->β . lambda r:α->β . 
+              lambda 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


@@ -258,7 +258,7 @@ argument of that type.  We would like to instantiate the recursive use
 of *and* in the definition by using the result type.  But fully
 instantiating the definition as given requires type application to a
 pair of types, not to just a single type.  We want to somehow
 of *and* in the definition by using the result type.  But fully
 instantiating the definition as given requires type application to a
 pair of types, not to just a single type.  We want to somehow

-guarantee that 'b will always itself be a complex type.
+guarantee that β will always itself be a complex type.

 
 So conjunction and disjunction provide a compelling motivation for
 polymorphism in natural language, but we don't yet have the ability to
 
 So conjunction and disjunction provide a compelling motivation for
 polymorphism in natural language, but we don't yet have the ability to