author Chris Barker Sun, 3 Oct 2010 00:57:15 +0000 (20:57 -0400) committer Chris Barker Sun, 3 Oct 2010 00:57:15 +0000 (20:57 -0400)
 week4.mdwn patch | blob | history

index 2fa501c..e01db2e 100644 (file)
@@ -171,3 +171,132 @@ so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation...
*    I hear that `Y` delivers the *least* fixed point.  Least
according to what ordering?  How do you know it's least?
Is leastness important?
+
+
+##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 &Omega; 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, thing of the ground types as the bar-level 0
+categories, 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 &sigma; and &tau; in `T`, the type &sigma; -->
+     &tau; 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 `&Lamda;_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 &sigma; --> &tau;, and a term `N` has type
+     &sigma;, then the application `(M N)` has type &tau;.
+
+*    If a variable `a` has type &sigma;, and term `M` has type &tau;,
+     then the abstract `&lambda; a M` has type `&sigma; --> &tau;`.
+
+The definitions of types and of typed terms should be highly familiar
+to semanticists, except that instead of writing `&sigma; --> &tau;`,
+linguists (following Montague, who followed Church) write `<&sigma;,
+&tau;>`.  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 &tau; in `&Lambda;_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 &Omega; does not have a normal form, it follows that &Omega;
+cannot have a type in `&Lambda;_T`.  We can easily see why:
+
+     &Omega; = (\x.xx)(\x.xx)
+
+Assume &Omega; has type &tau;, and `\x.xx` has type &sigma;.  Then
+because `\x.xx` takes an argument of type &sigma; and returns
+something of type &tau;, `\x.xx` must also have type `&sigma; -->
+&tau;`.  By repeating this reasoning, `\x.xx` must also have type
+`(&sigma; --> &tau;) --> &tau;`; 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 &sigma;, and `false`
+has type `&tau; --> &tau; --> &tau;` for some &tau;, and one is
+represented by the function `\x.x false 0`, then one must have type
+`(&tau; --> &tau; --> &tau) --> &sigma --> &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