+
+
+##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 <code>&Lamda;_T</code>,
+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 `(σ --> σ) -->
+σ --> σ`.
+