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=1fedd2a3c9843afd4b0721ba26e7be798c75dac3;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=967055fbde4c32649cdf8acf16ac127d43ec3118 diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index 1fedd2a3..047ee8b3 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -54,11 +54,10 @@ tells us that "The simple theory of types was suggested as a modification of Russell's ramified theory of types by Leon Chwistek in 1921 and 1922 and by F. P. Ramsey in 1926." This footnote appears in Church's 1940 paper [A formulation of the simple theory of -types](church-simple-types.pdf). In this paper, as Will Starr -mentioned in class, Church does indeed write types by simple -apposition, without the ugly angle brackets and commas used by -Montague. Furthermore, he omits parentheses under the convention that -types associated to the *left*---the opposite of the modern +types](church-simple-types.pdf). In this paper, Church writes types +by simple apposition, without the ugly angle brackets and commas used +by Montague. Furthermore, he omits parentheses under the convention +that types associated to the *left*---the opposite of the modern convention. This is ok, however, because he also reverses the order, so that `te` is a function from objects of type `e` to objects of type `t`. Cool paper! If you ever want to see Church numerals in their @@ -82,16 +81,16 @@ types `T`, the smallest set such that * ground types, including `e` and `t`, are in `T` -* for any types σ and τ in `T`, the type σ --> +* for any types σ and τ in `T`, the type σ -> τ is in `T`. For instance, here are some types in `T`: e - e --> t - e --> e --> t - (e --> t) --> t - (e --> t) --> e --> t + e -> t + e -> e -> t + (e -> t) -> t + (e -> t) -> e -> t and so on. @@ -103,28 +102,28 @@ which is the smallest set such that * each type `t` has an infinite set of distinct variables, {x^t}_1, {x^t}_2, {x^t}_3, ... -* If a term `M` has type σ --> τ, and a term `N` has type +* If a term `M` has type σ -> τ, and a term `N` has type σ, then the application `(M N)` has type τ. * If a variable `a` has type σ, and term `M` has type τ, - then the abstract λ a M has type σ --> τ. + then the abstract λ a M has type σ -> τ. The definitions of types and of typed terms should be highly familiar -to semanticists, except that instead of writing σ --> τ, +to semanticists, except that instead of writing σ -> τ, linguists write <σ, τ>. We will use the arrow notation, since it is more iconic. Some examples (assume that `x` has type `o`): x o - \x.x o --> o + \x.x o -> o ((\x.x) x) o Excercise: write down terms that have the following types: - o --> o --> o - (o --> o) --> o --> o - (o --> o --> o) --> o + o -> o -> o + (o -> o) -> o -> o + (o -> o -> o) -> o #Associativity of types versus terms# @@ -132,7 +131,7 @@ As we have seen many times, in the lambda calculus, function application is left associative, so that `f x y z == (((f x) y) z)`. Types, *THEREFORE*, are right associative: if `x`, `y`, and `z` have types `a`, `b`, and `c`, respectively, then `f` has type -`a --> b --> c --> d == (a --> (b --> (c --> d)))`, where `d` is the +`a -> b -> c -> d == (a -> (b -> (c -> d)))`, where `d` is the type of the complete term. It is a serious faux pas to associate to the left for types. You may @@ -147,13 +146,13 @@ present it here; see Berendregt or Hankin. Since Ω does not have a normal form, it follows that Ω cannot have a type in Λ_T. We can easily see why: - Ω = (\x.xx)(\x.xx) +Ω = (\x.xx)(\x.xx) Assume Ω has type τ, and `\x.xx` has type σ. Then because `\x.xx` takes an argument of type σ and returns -something of type τ, `\x.xx` must also have type σ --> +something of type τ, `\x.xx` must also have type σ -> τ. By repeating this reasoning, `\x.xx` must also have type -(σ --> τ) --> τ; and so on. Since variables have +(σ -> τ) -> τ; and so on. Since variables have finite types, there is no way to choose a type for the variable `x` that can satisfy all of the requirements imposed on it. @@ -161,51 +160,151 @@ In general, there is no way for a function to have a type that can take itself for an argument. It follows that there is no way to define the identity function in such a way that it can take itself as an argument. Instead, there must be many different identity -functions, one for each type. +functions, one for each type. Some of those types can be functions, +and some of those functions can be (type-restricted) identity +functions; but a simply-types identity function can never apply to itself. #Typing numerals# -Version 1 type numerals are not a good choice for the simply-typed -lambda calculus. The reason is that each different numberal has a -different type! For instance, if zero has type σ, then since -one is represented by the function `\x.x false 0`, it must have type -`b --> σ --> σ`, where `b` is the type of a boolean. But -this is a different type than zero! Because each number has a -different type, it becomes unbearable to write arithmetic operations -that can combine zero with one, since we would need as many different -addition operations as we had pairs of numbers that we wanted to add. - -Fortunately, the Church numerals are well behaved with respect to -types. They can all be given the type (σ --> σ) --> -σ --> σ. - - - - - - +The Church numerals are well behaved with respect to types. +To see this, consider the first three Church numerals (starting with zero): + + \s z . z + \s z . s z + \s z . s (s z) + +Given the internal structure of the term we are using to represent +zero, its type must have the form ρ -> σ -> σ for +some ρ and σ. This type is consistent with term for one, +but the structure of the definition of one is more restrictive: +because the first argument (`s`) must apply to the second argument +(`z`), the type of the first argument must describe a function from +expressions of type σ to some result type. So we can refine +ρ by replacing it with the more specific type σ -> τ. +At this point, the overall type is (σ -> τ) -> σ -> +σ. Note that this refined type remains compatible with the +definition of zero. Finally, by examinining the definition of two, we +see that expressions of type τ must be suitable to serve as +arguments to functions of type σ -> τ, since the result of +applying `s` to `z` serves as the argument of `s`. The most general +way for that to be true is if τ ≡ σ. So at this +point, we have the overall type of (σ -> σ) -> σ +-> σ. + + + +## Predecessor and lists are not representable in simply typed lambda-calculus ## + +As Oleg Kiselyov points out, [[predecessor and lists can't be +represented in the simply-typed lambda +calculus|http://okmij.org/ftp/Computation/lambda-calc.html#predecessor]]. +This is not because there is any difficulty typing what the functions +involved do "from the outside": for instance, the predecessor function +is a function from numbers to numbers, or τ -> τ, where τ +is our type for Church numbers (i.e., (σ -> σ) -> σ +-> σ). (Though this type will only be correct if we decide that +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: + + 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'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. + +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 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 +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.