`Λ_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 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 `x`, `y`, and `z`
+have types `a`, `b`, and `c`, respectively, then `f` has type
+`a --> b --> c --> d == (a --> (b --> (c --> d)))`, where `d` is the
+type of the complete term.
+
+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 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 (σ --> σ) -->
+σ --> σ.
+
+
+
+
+
+