edits

[lambda.git] / topics / _week5_simply_typed_lambda.mdwn

diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 4b1bde5..71856f6 100644 (file)
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -266,38 +266,39 @@ that even fairly basic recursive computations are beyond the reach of
 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
-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*.  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 base 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`.  
+type.  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`.
 
 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*.  * 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.
+When we talk 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.