X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_simply_typed_lambda.mdwn;h=047ee8b368a8a6f62c3111031a3b59d4ba06c559;hp=6c97df3ca82b684700e293e05abf0d6bc1a5d7f7;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=6417e111947a187f839267b3e6ca8d4e81cfcf4f

diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 6c97df3c..047ee8b3 100644
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -255,3 +255,56 @@ the predecessor function in the lambda calculus.  Could one of them
 possibly be simply-typeable?  It turns out that this can't be done.
 See the works cited by Oleg for details.
 
+Because lists are (in effect) a generalization of the Church numbers,
+computing the tail of a list is likewise beyond the reach of the
+simply-typed lambda calculus.
+
+This result is surprising.  It illustrates how recursion is built into
+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 based on a simply-typed lambda calculus
+
+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---included a simply-typed version of the Predicate Calculus
+with lambda abstraction.
+
+Montague called the semantic part of his PTQ fragment *Intensional
+Logic*.  Without getting too fussy about details, we'll present the
+popular Ty2 version of the PTQ types, roughly as proposed by Gallin
+(1975).  [See Zimmermann, Ede. 1989. Intensional logic and two-sorted
+type theory.  *Journal of Symbolic Logic* ***54.1***: 65--77 for a
+precise characterization of the correspondence between IL and
+two-sorted Ty2.]
+
+We'll need three base types: `e`, for individuals, `t`, for truth
+values, and `s` for evaluation indicies (world-time pairs).  The set
+of types is defined recursively:
+
+    the base types e, t, and s are types
+    if a and b are types, <a,b> is a type
+
+So `<e,<e,t>>` and `<s,<<s,e>,t>>` are types.  As we have 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 here as `a -> b`.  So the type `<a,b>` is the type of a function
+that maps objects of type `a` onto objects of type `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, b>*, 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>.
+
+When we talk about monads, we will consider Montague's treatment of
+intensionality in some detail.  In the meantime, Montague's PTQ is
+responsible for making the simply-typed lambda calculus the baseline
+semantic analysis for linguistics.