added discussion of Montague's PTQ

diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 14e2172..4b1bde5 100644 (file)
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -264,3 +264,40 @@ the structure of the Church numbers (and lists).  Most importantly for
 the discussion of the simply-typed lambda calculus, it demonstrates
 that even fairly basic recursive computations are beyond the reach of
 a simply-typed system.
+
+
+## Montague grammar is a simply-typed
+
+Systems based on the simply-typed lambda calculus are the bread and
+butter of current linguistic semantic analysis.  One of the most
+influential modern semantic formalisms---Montague's PTQ
+fragment---involved a simply-typed version of the Predicate Calculus
+with lambda abstraction.  More specifically, Montague called the
+semantic part of the PTQ fragment `Intensional Logic'.  Montague's IL
+had three base types: `e`, for individuals, `t`, for truth values, and
+`s` for evaluation indicies (world-time pairs).  The set of types was
+defined recursively:
+
+    e, t, s are types
+    if a and b are types, <a,b> is a type
+    if a is a type, <s,a> is a type
+
+So `<e,<e,t>>` and `<s,<<s,e>,t>>` are types, but `<e,s>` is not a
+type.  As mentioned, this paper is the source for the convention in
+linguistics that a type of the form `<a, b>` corresponds to a
+functional type that we will write `a -> b`.  
+
+Montague gave rules for the types of various logical formulas.  Of
+particular interest here, he gave the following typing rules for
+functional application and for lambda abstracts:
+
+*    If *&alpha;* is an expression of type *a*, and *&beta;* is an
+expression of type b, then *&alpha;(&beta;)* has type *b*.
+*    If *&alpha;* is an expression of type *a*, and *u* is a variable of
+type *b*, then *&lambda;u&alpha;* has type <code><b, a></code>.
+
+In future discussions about monads, we will investigate Montague's
+treatment of intensionality in some detail.  In the meantime,
+Montague's PTQ fragment is responsible for making the simply-typed
+lambda calculus the baseline semantic analysis for linguistics.
+

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 684f42b..86f1c75 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -18,10 +18,10 @@ System F is due (independently) to Girard and Reynolds.
 It enhances the simply-typed lambda calculus with quantification over
 types.  In System F, you can say things like
 
-<code>&Gamma; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
+<code>&Lambda; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
 
 This says that the identity function maps arguments of type &alpha; to
-results of type &alpha;, for any choice of &alpha;.  So the &Gamma; is
+results of type &alpha;, for any choice of &alpha;.  So the &Lambda; is
 a universal quantifier over types.