index 4b1bde5..047ee8b 100644 (file)
@@ -266,38 +266,45 @@ that even fairly basic recursive computations are beyond the reach of
a simply-typed system.

a simply-typed system.

-## Montague grammar is a simply-typed
+## 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

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
+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
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`.
+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:

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>.
+* If *&alpha;* is an expression of type *<a, b>*, and *&beta;* is an
+expression of type b, then *&alpha;(&beta;)* has type *b*.