X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=inline;f=topics%2F_week5_simply_typed_lambda.mdwn;h=1a0425feef46b5802638cde9bc20e89f57b77490;hb=be11c9fb4e8f436be20b5ccd5fb5a03794815440;hp=4caeb551fb7430abc581726459543baea2d4982f;hpb=de74e6bac683afd7a0d6c64716814ac6c4942c6b;p=lambda.git
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 `