From 967055fbde4c32649cdf8acf16ac127d43ec3118 Mon Sep 17 00:00:00 2001 From: Chris Date: Sat, 21 Feb 2015 17:56:18 -0500 Subject: [PATCH] edits --- topics/_week5_simply_typed_lambda.mdwn | 37 +++++++++++++++++++++++++++------- 1 file changed, 30 insertions(+), 7 deletions(-) diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index cfadf7a0..1fedd2a3 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -2,10 +2,10 @@ ##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 @@ -22,11 +22,34 @@ 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. +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 +``?); 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 @@ -41,7 +64,7 @@ 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 +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 -- 2.11.0