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=047ee8b368a8a6f62c3111031a3b59d4ba06c559;hp=a7917b28f4e0190cc4e326dc425a636e82c22582;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=63650e00ceddb514ac97085572d078699b797980 diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index a7917b28..047ee8b3 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,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, is a type + +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 . + +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.