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.
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 (σ --> σ) -->
+σ --> σ.