From bcc92bf29fae7f7c1423a3903dfce5ac07b97147 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 12:23:49 -0400 Subject: [PATCH] move type stuff to 'week5' page (without prejudice against covering it in week4) Signed-off-by: Jim Pryor --- week4.mdwn | 156 ------------------------------------------------------------ week5.mdwn | 158 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 158 insertions(+), 156 deletions(-) create mode 100644 week5.mdwn diff --git a/week4.mdwn b/week4.mdwn index 5870a6a3..61033f56 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -173,159 +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 Λ_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. You may -as well use 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 σ, then `false` -has type τ --> τ --> τ, for some τ. Since one is -represented by the function `\x.x false 0`, one must have type (τ ---> τ --> τ) --> σ --> σ. But this is a different -type than zero! Because each number has a different type, 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 (σ --> σ) --> -σ --> σ. - - - - - - diff --git a/week5.mdwn b/week5.mdwn new file mode 100644 index 00000000..a13c55ed --- /dev/null +++ b/week5.mdwn @@ -0,0 +1,158 @@ +[[!toc]] + +##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 Λ_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. You may +as well use 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 σ, then `false` +has type τ --> τ --> τ, for some τ. Since one is +represented by the function `\x.x false 0`, one must have type (τ +--> τ --> τ) --> σ --> σ. But this is a different +type than zero! Because each number has a different type, 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 (σ --> σ) --> +σ --> σ. + + + + + + -- 2.11.0