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=1a0425feef46b5802638cde9bc20e89f57b77490;hp=1fedd2a3c9843afd4b0721ba26e7be798c75dac3;hb=6a0ec687459f0862571cccde6bb2529ca06dd568;hpb=967055fbde4c32649cdf8acf16ac127d43ec3118
diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 1fedd2a3..1a0425fe 100644
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -26,7 +26,7 @@ To develop this analogy just a bit further, syntactic categories
determine which expressions can combine with which other expressions.
If a word is a member of the category of prepositions, it had better
not try to combine (merge) with an expression in the category of, say,
-an auxilliary verb, since *under has* is not a well-formed constituent
+an auxilliary verb, since \**under has* is not a well-formed constituent
in English. Likewise, types in formal languages will determine which
expressions can be sensibly combined.
@@ -41,7 +41,7 @@ phrases, since they both denote properties with (extensional) type
not correspond to any salient syntactic distinctions (as in any
analysis that involves silent type-shifters, such as Herman Hendriks'
theory of quantifier scope, in which expressions change their semantic
-type without any effect on the syntactic expressions they can combine
+type without any effect on the expressions they can combine
with syntactically). We will consider again the relationship between
syntactic types and semantic types later in the course.
@@ -54,15 +54,14 @@ 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
-native setting--but I'm getting ahead of my story. Pedantic off.]
+native setting--but we're getting ahead of our story. Pedantic off.]
There's good news and bad news: the good news is that the simply-typed
lambda calculus is strongly normalizing: every term has a normal form.
@@ -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,48 @@ 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
+
+#A first glipse of the connection between types and logic
+
+In the simply-typed lambda calculus, we write types like σ
+-> τ. This looks like logical implication. We'll take
+that resemblance seriously when we discuss the Curry-Howard
+correspondence. In the meantime, note that types respect modus
+ponens:
+
+
+Expression Type Implication
+-----------------------------------
+fn α -> β α ⊃ β
+arg α α
+------ ------ --------
+(fn arg) β β
+
+
+The implication in the right-hand column is modus ponens, of course.
+
#Associativity of types versus terms#
@@ -132,7 +151,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,65 +166,196 @@ 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.
-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.
-
-#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 (σ --> σ) -->
-σ --> σ.
-
-
-
-
+In fact, we can't even type the parts of Ω, that is, `ω
+\equiv \x.xx`. In general, there is no way for a function to have a
+type that can take itself for an argument.
-
+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 ##
+
+
+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 fst = \x y. x in
+ let snd = \x y. y in
+ let pair = \x y . \f . f x y in
+ let succ = \n s z. s (n s z) in
+ let shift = \p. pair (succ (p fst)) (p fst) in
+ let pred = \n. n shift (pair zero zero) snd in
+
+Note that `shift` takes a pair `p` as argument, but makes use of only
+the first element of the pair. 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 3
+ 3 shift (pair zero zero) snd
+ (\s z.s(s(s z))) shift (pair zero zero) snd
+ shift (shift (shift (\f.f 0 0))) snd
+ shift (shift (pair (succ ((\f.f 0 0) fst)) ((\f.f 0 0) fst))) snd
+ shift (shift (\f.f 1 0)) snd
+ shift (\f. f 2 1) snd
+ (\f. f 3 2) snd
+ snd 3 2
+ 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 Oleg Kiselyov's discussion and works cited there for details:
+[[predecessor and lists can't be represented in the simply-typed
+lambda
+calculus|http://okmij.org/ftp/Computation/lambda-calc.html#predecessor]].
+
+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,
+Montague's 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, which match the rules
+for the simply-typed lambda calculus exactly:
+
+* 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