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=cee3f916d991985d7b7d07aaec537a0fd137086d;hp=cfadf7a0510c6e842dde993407f2ce9043e9dae4;hb=5e9e42542f2f56e0236af240519eda4cdde09a52;hpb=da8c71643ef408b942d125d17b6b746bace93ee5 diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index cfadf7a0..cee3f916 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -2,10 +2,10 @@ ##The simply-typed lambda calculus## -The untyped lambda calculus is pure. Pure in many ways: all variables -and lambdas, with no constants or other special symbols; also, all -functions without any types. As we'll see eventually, pure also in -the sense of having no side effects, no mutation, just pure +The untyped lambda calculus is pure. Pure in many ways: nothing but +variables and lambdas, with no constants or other special symbols; +also, all functions without any types. As we'll see eventually, pure +also in the sense of having no side effects, no mutation, just pure computation. But we live in an impure world. It is much more common for practical @@ -22,26 +22,48 @@ language. If so, if it makes sense to gather a class of expressions together into a set of Nouns, or Verbs, it may also make sense to gather classes of terms into a set labelled with some computational type. +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 +in English. Likewise, types in formal languages will determine which +expressions can be sensibly combined. + +Now, of course it is common linguistic practice to supply an analysis +of natural language both with syntactic categories and with semantic +types. And there is a large degree of overlap between these type +systems. However, there are mismatches in both directions: there are +syntactic distinctions that do not correspond to any salient semantic +difference (why can't adjectives behave syntactically like verb +phrases, since they both denote properties with (extensional) type +``?); and in some analyses there are semantic differences that do +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 +with syntactically). We will consider again the relationship between +syntactic types and semantic types later in the course. + Soon we will consider polymorphic type systems. First, however, we will consider the simply-typed lambda calculus. -[Pedantic on. Why "simply typed"? Well, the type system is -particularly simple. As mentioned in class by Koji Mineshima, Church +[Pedantic on. Why "*simply* typed"? Well, the type system is +particularly simple. As mentioned to us by Koji Mineshima, Church 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.] -There's good news and bad news: the good news is that the simply-type +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. We shall see that self-application is outlawed, so Ω can't even be written, let alone undergo reduction. The bad news is that @@ -124,7 +146,7 @@ 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 @@ -138,51 +160,61 @@ 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 ρ --> σ --> $sigma; 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 other 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 examinine the definition of two, we +see that expressions of type τ must be suitable to serve as +arguments to functions of type σ --> τ. The most general +way for that to be true is if τ ≡ σ. So at this +point, we have the overall type of (σ --> σ) --> σ --> +σ. -