index a7917b2..047ee8b 100644 (file)
@@ -220,7 +220,7 @@ ways to suit present purposes:

Let's see how far we can get typing these terms.  `zero` is the Church
encoding of zero.  Using `N` as the type for Church numbers (i.e.,
-<code>N == (&sigma; -> &sigma;) -> &sigma; -> &sigma;</code> for some
+<code>N &equiv; (&sigma; -> &sigma;) -> &sigma; -> &sigma;</code> for some
&sigma;, `zero` has type `N`.  `snd` takes two numbers, and returns
the second, so `snd` has type `N -> N -> N`.  Then the type of `pair`
is `N -> N -> (type(snd)) -> N`, that is, `N -> N -> (N -> N -> N) ->
@@ -230,24 +230,24 @@ namely, <code>pair &equiv; (N -> N -> N) -> N</code>.  So far so good.

The problem is the way in which `pred` puts these parts together.  In
particular, `pred` applies its argument, the number `n`, to the
-`collect` function.  Since `n` is a number, its type is `(&sigma; ->
-&sigma;) -> &sigma; -> &sigma;`.  This means that the type of
-`collect` has to match `&sigma; -> &sigma;`. But we concluded above
-that the type of `collect` also had to be `pair -> pair`.  Putting
-these constraints together, it appears that `&sigma;` must be the type
-of a pair of numbers.  But we already decided that the type of a pair
-of numbers is `(N -> N -> N) -> N`.  Here's the difficulty: `N` is
-shorthand for a type involving `&sigma;`.  If `&sigma;` turns out to
-depend on `N`, and `N` depends in turn on `&sigma;`, then `&sigma;` is a proper
-subtype of itself, which is not allowed in the simply-typed lambda
-calculus.
-
-The way we got here is that the pred function relies on the right-fold
-structure of the Church numbers to recursively walk down the spine of
-its argument.  In order to do that, the argument number had to take
-the operation in question as its first argument.  And the operation
-required in order to build up the predecessor must be the sort of
-operation that manipulates numbers, and the infinite regress is
+`collect` function.  Since `n` is a number, its type is <code>(&sigma;
+-> &sigma;) -> &sigma; -> &sigma;</code>.  This means that the type of
+`collect` has to match <code>&sigma; -> &sigma;</code>. But we
+concluded above that the type of `collect` also had to be `pair ->
+pair`.  Putting these constraints together, it appears that
+<code>&sigma;</code> must be the type of a pair of numbers.  But we
+already decided that the type of a pair of numbers is `(N -> N -> N)
+-> N`.  Here's the difficulty: `N` is shorthand for a type involving
+<code>&sigma;</code>.  If <code>&sigma;</code> turns out to depend on
+`N`, and `N` depends in turn on <code>&sigma;</code>, then
+<code>&sigma;</code> is a proper subtype of itself, which is not
+allowed in the simply-typed lambda calculus.
+
+The way we got here is that the `pred` function relies on the built-in
+right-fold structure of the Church numbers to recursively walk down
+the spine of its argument.  In order to do that, the argument had to
+apply to the `collect` operation.  And since `collect` had to be the
+sort of operation that manipulates numbers, the infinite regress is
established.

Now, of course, this is only one of myriad possible implementations of
@@ -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>.
+