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=4b1bde564d59148e212b2e3a3b575d0a2b25c460;hp=a7917b28f4e0190cc4e326dc425a636e82c22582;hb=d03fe382641cc8bc266184561d3c484deeb12ca1;hpb=a95160473037089ea4deb34eceff948391b0cee4
diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index a7917b28..4b1bde56 100644
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -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.,
-N == (σ -> σ) -> σ -> σ for some
+N ≡ (σ -> σ) -> σ -> σ for some
σ, `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, pair ≡ (N -> N -> N) -> N. 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 `(σ ->
-σ) -> σ -> σ`. This means that the type of
-`collect` has to match `σ -> σ`. But we concluded above
-that the type of `collect` also had to be `pair -> pair`. Putting
-these constraints together, it appears that `σ` 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 `σ`. If `σ` turns out to
-depend on `N`, and `N` depends in turn on `σ`, then `σ` 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 (σ
+-> σ) -> σ -> σ. This means that the type of
+`collect` has to match σ -> σ. But we
+concluded above that the type of `collect` also had to be `pair ->
+pair`. Putting these constraints together, it appears that
+σ 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
+σ. If σ turns out to depend on
+`N`, and `N` depends in turn on σ, then
+σ 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,49 @@ 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 a simply-typed
+
+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
+ 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`.
+
+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