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=1fedd2a3c9843afd4b0721ba26e7be798c75dac3;hpb=967055fbde4c32649cdf8acf16ac127d43ec3118;p=lambda.git
diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 1fedd2a3..4caeb551 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,174 @@ 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 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 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 `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
+`shift` function. Since `n` is a number, its type is (σ
+-> σ) -> σ -> σ
. This means that the type of
+`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)
+-> 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 `shift` operation. And since `shift` 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 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
+
+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.