From: Chris Date: Thu, 26 Feb 2015 18:13:09 +0000 (-0500) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=447c097435042d6895c2cf7e861ec119a2f20b63 edits --- diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index 4caeb551..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. @@ -61,7 +61,7 @@ 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. @@ -125,6 +125,26 @@ Excercise: write down terms that have the following types: (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# As we have seen many times, in the lambda calculus, function @@ -156,13 +176,16 @@ something of type τ, `\x.xx` must also have type σ -> 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. 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. +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. + +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. 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# @@ -196,9 +219,7 @@ principle type--> ## 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 τ @@ -212,24 +233,27 @@ 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 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. p (\a b. pair (succ a) a) + let shift = \p. pair (succ (p fst)) (p fst) in 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: +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 (\s z.s(s(s z))) - (\s z.s(s(s z))) (\n.n shift (\f.f 0 0) snd) + 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 ((\f.f 0 0) (\a b.pair(succ a) a))) 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 @@ -276,7 +300,10 @@ 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. +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 @@ -313,14 +340,15 @@ of types is defined recursively: 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'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: +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*. diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index a7b4bb91..4bde11e0 100644 --- a/topics/_week5_system_F.mdwn +++ b/topics/_week5_system_F.mdwn @@ -1,6 +1,13 @@ [[!toc levels=2]] -# System F and recursive types +# System F: the polymorphic lambda calculus + +The simply-typed lambda calculus is beautifully simple, but it can't +even express the predecessor function, let alone full recursion. And +we'll see shortly that there is good reason to be unsatisfied with the +simply-typed lambda calculus as a way of expressing natural language +meaning. So we will need to get more sophisticated about types. The +next step in that journey will be to consider System F. In the simply-typed lambda calculus, we write types like σ -> τ. This looks like logical implication. We'll take