##The simply-typed lambda calculus##
-The untyped lambda calculus is pure. Pure in many ways: all variables
-and lambdas, with no constants or other special symbols; also, all
-functions without any types. As we'll see eventually, pure also in
-the sense of having no side effects, no mutation, just pure
+The untyped lambda calculus is pure. Pure in many ways: nothing but
+variables and lambdas, with no constants or other special symbols;
+also, all functions without any types. As we'll see eventually, pure
+also in the sense of having no side effects, no mutation, just pure
computation.
But we live in an impure world. It is much more common for practical
together into a set of Nouns, or Verbs, it may also make sense to
gather classes of terms into a set labelled with some computational type.
+To develop this analogy just a bit further, syntactic categories
+determine which expressions can combine with which other expressions.
+If a word is a member of the category of prepositions, it had better
+not try to combine (merge) with an expression in the category of, say,
+an auxilliary verb, since *under has* is not a well-formed constituent
+in English. Likewise, types in formal languages will determine which
+expressions can be sensibly combined.
+
+Now, of course it is common linguistic practice to supply an analysis
+of natural language both with syntactic categories and with semantic
+types. And there is a large degree of overlap between these type
+systems. However, there are mismatches in both directions: there are
+syntactic distinctions that do not correspond to any salient semantic
+difference (why can't adjectives behave syntactically like verb
+phrases, since they both denote properties with (extensional) type
+`<e,t>`?); and in some analyses there are semantic differences that do
+not correspond to any salient syntactic distinctions (as in any
+analysis that involves silent type-shifters, such as Herman Hendriks'
+theory of quantifier scope, in which expressions change their semantic
+type without any effect on the syntactic expressions they can combine
+with syntactically). We will consider again the relationship between
+syntactic types and semantic types later in the course.
+
Soon we will consider polymorphic type systems. First, however, we
will consider the simply-typed lambda calculus.
-[Pedantic on. Why "simply typed"? Well, the type system is
-particularly simple. As mentioned in class by Koji Mineshima, Church
+[Pedantic on. Why "*simply* typed"? Well, the type system is
+particularly simple. As mentioned to us by Koji Mineshima, Church
tells us that "The simple theory of types was suggested as a
modification of Russell's ramified theory of types by Leon Chwistek in
1921 and 1922 and by F. P. Ramsey in 1926." This footnote appears in
`t`. Cool paper! If you ever want to see Church numerals in their
native setting--but I'm getting ahead of my story. Pedantic off.]
-There's good news and bad news: the good news is that the simply-type
+There's good news and bad news: the good news is that the simply-typed
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