added jsMath files
[lambda.git] / week5.mdwn
index 3eed60e..cfadf7a 100644 (file)
@@ -2,43 +2,73 @@
 
 ##The simply-typed lambda calculus##
 
 
 ##The simply-typed lambda calculus##
 
-The untyped lambda calculus is pure computation.  It is much more
-common, however, for practical programming languages to be typed.
+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
+computation.
+
+But we live in an impure world.  It is much more common for practical
+programming languages to be typed, either implicitly or explicitly.
 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.
 
 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.
 
+From a linguistic perspective, types are generalizations of (parts of)
+programs.  To make this comment more concrete: types are to (e.g.,
+lambda) terms as syntactic categories are to expressions of natural
+language.  If so, if it makes sense to gather a class of expressions
+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.
+
 Soon we will consider polymorphic type systems.  First, however, we
 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 Ω 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.
 
 #Types#
 
 
 #Types#
 
-We will have at least one ground type, `o`.  From a linguistic point
-of view, think of the ground types as the bar-level 0 categories, that
-is, the lexical types, such as Noun, Verb, Preposition (glossing over
-the internal complexity of those categories in modern theories).
+We will have at least one ground type.  For the sake of linguistic
+familiarity, we'll use `e`, the type of individuals, and `t`, the type
+of truth values.
 
 In addition, there will be a recursively-defined class of complex
 types `T`, the smallest set such that
 
 
 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`
+*    ground types, including `e` and `t`, are in `T`
 
 *    for any types σ and τ in `T`, the type σ -->
      τ is in `T`.
 
 For instance, here are some types in `T`:
 
 
 *    for any types σ and τ in `T`, the type σ -->
      τ is in `T`.
 
 For instance, here are some types in `T`:
 
-     o
-     o --> o
-     o --> o --> o
-     (o --> o) --> o
-     (o --> o) --> o --> o
+     e
+     e --> t
+     e --> e --> t
+     (e --> t) --> t
+     (e --> t) --> e --> t
 
 and so on.
 
 
 and so on.
 
@@ -58,8 +88,8 @@ which is the smallest set such that
 
 The definitions of types and of typed terms should be highly familiar
 to semanticists, except that instead of writing σ --> τ,
 
 The definitions of types and of typed terms should be highly familiar
 to semanticists, except that instead of writing σ --> τ,
-linguists (following Montague, who followed Church) write <&sigma;,
-&tau;>.  We will use the arrow notation, since it is more iconic.
+linguists write <&sigma;, &tau;>.  We will use the arrow notation,
+since it is more iconic.
 
 Some examples (assume that `x` has type `o`):
 
 
 Some examples (assume that `x` has type `o`):
 
@@ -77,9 +107,10 @@ Excercise: write down terms that have the following types:
 
 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)`.
 
 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)))`.
+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.
 
 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.
@@ -113,16 +144,15 @@ functions, one for each type.
 
 Version 1 type numerals are not a good choice for the simply-typed
 lambda calculus.  The reason is that each different numberal has a
 
 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;, then `false`
-has type &tau; --> &tau; --> &tau;, for some &tau;.  Since one is
-represented by the function `\x.x false 0`, one must have type (&tau;
---> &tau; --> &tau;) --> &sigma; --> &sigma;.  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
+different type!  For instance, if zero has type &sigma;, then since
+one is represented by the function `\x.x false 0`, it must have type
+`b --> &sigma; --> &sigma;`, 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 (&sigma; --> &sigma;) -->
 &sigma; --> &sigma;.
 
 types.  They can all be given the type (&sigma; --> &sigma;) -->
 &sigma; --> &sigma;.