X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=0dcb0957803ffa0855c51e792a0c0979a4590683;hp=a7b4bb912333577b0afea0cb4f5ec855da96d566;hb=4d9fe4645917a4966694c7c4bf8edde8b243745f;hpb=c98d4e2d9d0c85b16ac707323031114f2a3db1aa

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index a7b4bb91..0dcb0957 100644
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -1,23 +1,13 @@
 [[!toc levels=2]]
 
-# System F and recursive types
-
-In the simply-typed lambda calculus, we write types like <code>&sigma;
--> &tau;</code>.  This looks like logical implication.  We'll take
-that resemblance seriously when we discuss the Curry-Howard
-correspondence.  In the meantime, note that types respect modus
-ponens: 
-
-<pre>
-Expression    Type      Implication
------------------------------------
-fn            &alpha; -> &beta;    &alpha; &sup; &beta;
-arg           &alpha;         &alpha;
-------        ------    --------
-(fn arg)      &beta;         &beta;
-</pre>
-
-The implication in the right-hand column is modus ponens, of course.
+# System F: the polymorphic lambda calculus
+
+The simply-typed lambda calculus is beautifully simple, but it can't
+even express the predecessor function, let alone full recursion.  And
+we'll see shortly that there is good reason to be unsatisfied with the
+simply-typed lambda calculus as a way of expressing natural language
+meaning.  So we will need to get more sophisticated about types.  The
+next step in that journey will be to consider System F.
 
 System F was discovered by Girard (the same guy who invented Linear
 Logic), but it was independently proposed around the same time by