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=4caeb551fb7430abc581726459543baea2d4982f;hp=71856f64773eb77dbcd239dee3e053e76bf46080;hb=2e1217b17ae7e408c89f52c4f6b43ce69284a342;hpb=2306723f0538613e28d2adf8f8e69b744242c554 diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index 71856f64..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,11 +282,11 @@ 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 based on a simply-typed lambda calculus @@ -272,33 +295,39 @@ 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. +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 +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 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 `>` 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 **, 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 . +expression of type b, then *α(β)* has type *b*. -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. +* 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.