XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_simply_typed_lambda.mdwn;h=047ee8b368a8a6f62c3111031a3b59d4ba06c559;hp=4b1bde564d59148e212b2e3a3b575d0a2b25c460;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=d03fe382641cc8bc266184561d3c484deeb12ca1
diff git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 4b1bde56..047ee8b3 100644
 a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ 266,38 +266,45 @@ that even fairly basic recursive computations are beyond the reach of
a simplytyped system.
## Montague grammar is a simplytyped
+## Montague grammar is based on a simplytyped lambda calculus
Systems based on the simplytyped lambda calculus are the bread and
butter of current linguistic semantic analysis. One of the most
influential modern semantic formalismsMontague's PTQ
fragmentinvolved a simplytyped 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 (worldtime pairs). The set of types was
defined recursively:

 e, t, s are types
+fragmentincluded a simplytyped 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 twosorted
+type theory. *Journal of Symbolic Logic* ***54.1***: 6577 for a
+precise characterization of the correspondence between IL and
+twosorted Ty2.]
+
+We'll need three base types: `e`, for individuals, `t`, for truth
+values, and `s` for evaluation indicies (worldtime pairs). The set
+of types is defined recursively:
+
+ the base types e, t, and s are types
if a and b are types, is a type
 if a is a type, is a type
So `>` and `,t>>` are types, but `` is not a
type. As mentioned, this paper is the source for the convention in
linguistics that a type of the form `` corresponds to a
functional type that we will write `a > b`.
+So `>` and `,t>>` are types. As we have mentioned,
+this paper is the source for the convention in linguistics that a type
+of the form `` corresponds to a functional type that we will
+write here as `a > b`. So the type `` 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 *α* is an expression of type *a*, and *β* is an
expression of type b, then *α(β)* has type *b*.
* If *α* is an expression of type *a*, and *u* is a variable of
type *b*, then *λuα* has type
.
+* If *α* is an expression of type **, and *β* is an
+expression of type b, then *α(β)* has type *b*.
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 simplytyped
lambda calculus the baseline semantic analysis for linguistics.
+* If *α* is an expression of type *a*, and *u* is a variable of type *b*, then *λuα* has type
.
+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 simplytyped lambda calculus the baseline
+semantic analysis for linguistics.