X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=61033f5602f114fcbc33eb8ea03e6949733f3907;hp=8fe37ad2be182d92c8cc1298794ced2cc6a99b9d;hb=bfc18dfc2a8f9fee385b4f6f2b31fc99c155c728;hpb=c3998b2b5a85bd4b5a47c1b2518739fe9948807f diff --git a/week4.mdwn b/week4.mdwn index 8fe37ad2..61033f56 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -173,129 +173,3 @@ so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation... Is leastness important? -##The simply-typed lambda calculus## - -The uptyped lambda calculus is pure computation. It is much more -common, however, for practical programming languages to be typed. -Likewise, systems used to investigate philosophical or linguistic -issues are almost always typed. Types will help us reason about our -computations. They will also facilitate a connection between logic -and computation. - -Soon we will consider polymorphic type systems. First, however, we -will consider the simply-typed lambda calculus. There's good news and -bad news: the good news is that the simply-type 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 fixed-point combinators -are also forbidden, so recursion is neither simple nor direct. - -#Types# - -We will have at least one ground type, `o`. From a linguistic point -of view, think of the ground types as the bar-level 0 categories, that -is, the lexical types, such as Noun, Verb, Preposition (glossing over -the internal complexity of those categories in modern theories). - -In addition, there will be a recursively-defined class of complex -types `T`, the smallest set such that - -* ground types, including `o`, are in `T` - -* for any types σ and τ in `T`, the type σ --> - τ is in `T`. - -For instance, here are some types in `T`: - - o - o --> o - o --> o --> o - (o --> o) --> o - (o --> o) --> o --> o - -and so on. - -#Typed lambda terms# - -Given a set of types `T`, we define the set of typed lambda terms &Lamda;_T, -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 - σ, 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 `σ --> τ`. - -The definitions of types and of typed terms should be highly familiar -to semanticists, except that instead of writing `σ --> τ`, -linguists (following Montague, who followed Church) 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) x) o - -Excercise: write down terms that have the following types: - - o --> o --> o - (o --> o) --> o --> o - (o --> o --> o) --> o - -#Associativity of types versus terms# - -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 `f`, `x`, `y`, and `z` -have types `a`, `b`, `c`, and `d`, respectively, then `f` has type `a ---> b --> c --> d == (a --> (b --> (c --> d)))`. - -It is a serious faux pas to associate to the left for types, on a par -with using your salad fork to stir your tea. - -#The simply-typed lambda calculus is strongly normalizing# - -If `M` is a term with type τ in `Λ_T`, then `M` has a -normal form. The proof is not particularly complex, but we will not -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) - -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 `σ --> -τ`. By repeating this reasoning, `\x.xx` must also have type -`(σ --> τ) --> τ`; 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 σ, and `false` -has type `τ --> τ --> τ` for some τ, and one is -represented by the function `\x.x false 0`, then one must have type -`(τ --> τ --> &tau) --> &sigma --> σ`. But this is a -different type than zero! Because numbers have different types, it -becomes impossible to write arithmetic operations that can combine -zero with one. We would need as many different addition operations as -we had pairs of numbers that we wanted to add. - -Fortunately, the Church numberals are well behaved with respect to -types. They can all be given the type `(σ --> σ) --> -σ --> σ`. -