X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=inline;f=topics%2F_week5_simply_typed_lambda.mdwn;h=4caeb551fb7430abc581726459543baea2d4982f;hb=c55a7320fe75884e8fda7f7785b68194ac9554b5;hp=4b1bde564d59148e212b2e3a3b575d0a2b25c460;hpb=d03fe382641cc8bc266184561d3c484deeb12ca1;p=lambda.git
diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 4b1bde56..4caeb551 100644
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -208,32 +208,55 @@ the predecessor of zero should be a number, perhaps zero.)
Rather, the problem is that the definition of the function requires
subterms that can't be simply-typed. We'll illustrate with our
-implementation of the predecessor, sightly modified in inessential
-ways to suit present purposes:
+implementation of the predecessor function, based on the discussion in
+Pierce 2002:547:
let zero = \s z. z in
let snd = \a b. b in
let pair = \a b. \v. v a b in
let succ = \n s z. s (n s z) in
- let collect = \p. p (\a b. pair (succ a) a)
- let pred = \n. n collect (pair zero zero) snd in
+ let shift = \p. p (\a b. pair (succ a) a)
+ let pred = \n. n shift (pair zero zero) snd in
+
+Note that `shift` applies its argument p ("p" for "pair") to a
+function that ignores its second argument---why does it do that? In
+order to understand what this code is doing, it is helpful to go
+through a sample computation, the predecessor of 3:
+
+ pred (\s z.s(s(s z)))
+ (\s z.s(s(s z))) (\n.n shift (\f.f 0 0) snd)
+ shift (shift (shift (\f.f 0 0))) snd
+ shift (shift ((\f.f 0 0) (\a b.pair(succ a) a))) snd
+ shift (shift (\f.f 1 0)) snd
+ shift (\f. f 2 1) snd
+ (\f. f 3 2) snd
+ 2
+
+At each stage, `shift` sees an ordered pair that contains two numbers
+related by the successor function. It can safely discard the second
+element without losing any information. The reason we carry around
+the second element at all is that when it comes time to complete the
+computation---that is, when we finally apply the top-level ordered
+pair to `snd`---it's the second element of the pair that will serve as
+the final result.
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
-σ, `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) ->
-N`. Likewise, `succ` has type `N -> N`, and `collect` has type `pair
--> pair`, where `pair` is the type of an ordered pair of numbers,
-namely, pair ≡ (N -> N -> N) -> N
. So far so good.
+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) -> N`. Likewise, `succ` has type `N -> N`, and `shift` has type
+`pair -> pair`, where `pair` is the type of an ordered pair of
+numbers, 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 (σ
+`shift` 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 ->
+`shift` has to match σ -> σ
. But we
+concluded above that the type of `shift` 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)
@@ -246,7 +269,7 @@ 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
+apply to the `shift` operation. And since `shift` had to be the
sort of operation that manipulates numbers, the infinite regress is
established.
@@ -259,45 +282,52 @@ 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.
+This result is not obvious, to say the least. 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
+## 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*. 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, 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 simply-typed
-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 simply-typed lambda calculus the baseline
+semantic analysis for linguistics.