X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_simply_typed_lambda.mdwn;fp=topics%2F_week5_simply_typed_lambda.mdwn;h=cfadf7a0510c6e842dde993407f2ce9043e9dae4;hp=0000000000000000000000000000000000000000;hb=da8c71643ef408b942d125d17b6b746bace93ee5;hpb=f223b9dc134769fb9c6558980911594efb82d648
diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
new file mode 100644
index 00000000..cfadf7a0
--- /dev/null
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -0,0 +1,188 @@
+[[!toc]]
+
+##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
+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.
+
+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
+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#
+
+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
+
+* 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`:
+
+ e
+ e --> t
+ e --> e --> t
+ (e --> t) --> t
+ (e --> t) --> e --> t
+
+and so on.
+
+#Typed lambda terms#
+
+Given a set of types `T`, we define the set of typed lambda terms Λ_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 σ --> τ, and a term `N` has type
+ σ, then the application `(M N)` has type τ.
+
+* If a variable `a` has type σ, and term `M` has type τ,
+ then the abstract λ a M
has type σ --> τ.
+
+The definitions of types and of typed terms should be highly familiar
+to semanticists, except that instead of writing σ --> τ,
+linguists write <σ, τ>. 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 `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.
+
+#The simply-typed lambda calculus is strongly normalizing#
+
+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:
+
+ Ω = (\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
+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 σ, then since
+one is represented by the function `\x.x false 0`, it must have type
+`b --> σ --> σ`, 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 (σ --> σ) -->
+σ --> σ.
+
+
+
+
+
+