-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.
+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
+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
+Church's 1940 paper [A formulation of the simple theory of
+types](church-simple-types.pdf). In this paper, as Will Starr
+mentioned in class, Church does indeed write types by simple
+apposition, without the ugly angle brackets and commas used by
+Montague. Furthermore, he omits parentheses under the convention that
+types associated to the *left*---the opposite of the modern
+convention. This is ok, however, because he also reverses the order,
+so that `te` is a function from objects of type `e` to objects of type
+`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
+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.