X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=5870a6a3ff8cca5e4ef453ca53c5bc312245c410;hp=1f52cf3ba6a655701148c9d78530b53f93c476b6;hb=cb31839ef2a0cea9b6138fa84d487ab7107328c2;hpb=3af15277e1a4116c0eb3025f371e0a9a9417ebc9 diff --git a/week4.mdwn b/week4.mdwn index 1f52cf3b..5870a6a3 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -217,7 +217,7 @@ and so on. #Typed lambda terms# -Given a set of types `T`, we define the set of typed lambda terms Λ~T~, +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, @@ -227,12 +227,12 @@ which is the smallest set such that σ, 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 `σ --> τ`. + 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. +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`): @@ -254,25 +254,25 @@ 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. +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 +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: +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 +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. @@ -286,16 +286,46 @@ functions, one for each type. 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. +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 `(σ --> σ) --> -σ --> σ`. +types. They can all be given the type (σ --> σ) --> +σ --> σ. + + + + +