From: Chris Date: Thu, 19 Mar 2015 22:43:59 +0000 (-0400) Subject: added intensionality and binding X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=ea187cef2fbecef2991baeac77e0d79d768ce941 added intensionality and binding --- diff --git a/topics/_week8_binding.mdwn b/topics/_week8_binding.mdwn new file mode 100644 index 00000000..ce4d087c --- /dev/null +++ b/topics/_week8_binding.mdwn @@ -0,0 +1,302 @@ +[[!toc]] + +Substitution versus Environment-based Semantics +----------------------------------------------- + +Let's step back and consider the semantics we've assumed so far for our lambda calculi. We've been doing this: + + (\x. M) N ~~> M {x <- N} + +where `M {x <- N}` is the result of substituting N in for free occurrences of `x` in `M`. + +What do I mean by calling this a "semantics"? Wasn't this instead part of our proof-theory? Haven't we neglected to discuss any model theory for the lambda calculus? + +Well, yes, that's right, we haven't much discussed what computer scientists call *denotational semantics* for the lambda calculus. That's what philosophers and linguists tend to think of as "semantics." + +But computer scientists also recognize what they call *operational semantics* and *axiomatic semantics*. The former consists in the specification of an "abstract machine" for evaluating complex expressions of the language. The latter we won't discuss. + +When it comes down to it, I'm not sure what difference there is between an operational semantics and a proof theory; though it should be noted that the operational semantics generally *don't* confine themselves to only using abstract machines whose transitions are identical to the ones licensed in the formal system being interpreted. Instead, any viable algorithm for reducing expressions to some sort of normal form (when they can be so reduced) would be entertained. + +If we think of the denotations of lambda terms as sets of inter-convertible terms, and let the sets which have normal forms use that normal form as their +representative, then operational semantics can be thought of as algorithms for +deriving what a formula's denotation is. But it's not necessary to think of the denonations of lambda terms in that way; and even if we do, matters are complicated by the presence of non-normalizing terms. + +In any case, the lambda evaluator we use on our website does evaluate expressions using the kind of operational semantics described above. We can call that a "substitution-based" semantics. + +Let's consider a different kind of operational semantics. Instead of substituting `N` in for `x`, why don't we keep some extra data-structure on the side, where we note that `x` should now be understood to evaluate to whatever `N` does? In computer science jargon, such a data-structure is called an **environment**. Philosophers and linguists would tend to call it an **assignment** (though there are some subtleties about whether these are the same thing, which we'll discuss). + +[Often in computer science settings, the lambda expression to be evaluated is first translated into **de Bruijn notation**, which we discussed in the first week of term. That is, instead of: + + \x. x (\y. y x) + +we have: + + \. 1 (\. 1 2) + +where each argument-occurrence records the distance between that occurrence and the `\` which binds it. This has the advantage that the environment can then just be a stack, with the top element of the stack being what goes in for the outermost-bound argument, and so on. + +Some students have asked: why do we need de Bruijn notation to represent environments that way? Can't we just assume our variables are of the form `x1, x2, x3`, and so on? And then the values that get assigned to those variables could just be kept in a stack, with the first value understood to be assigned to `x1`, and so on. Yes, we could do that. But the advantage of the de Bruijn notation is that we don't have to keep track of which variable is associated with which lambda binder. In the de Bruijn framework, the outermost binder always goes with the top-most member of the stack. In the proposed alternative, that's not so: we could have: + +
``````\x2. x2 (\x8. x8 x2)
+``````
```+				VP
+			  /    \
+			 /      \
+			/        \
+		   /          \
+		  /            \
+		 /              NP
+		/              /  \
+	   /              /    \
+	   V             /      \
+	   |            /        \
+\[[interprets]]    AP         N
+				  / \         |
+			  \[[complex]] \[[phrases]]
+```
```+Extensional types              Intensional types       Examples
+-------------------------------------------------------------------
+
+S         t                    s->t                    John left
+DP        e                    s->e                    John
+VP        e->t                 (s->e)->s->t            left
+Vt        e->e->t              (s->e)->(s->e)->s->t    saw
+Vs        t->e->t              (s->t)->(s->e)->s->t    thought
+```
+ +This system is modeled on the way Montague arranged his grammar. +There are significant simplifications: for instance, determiner +phrases are thought of as corresponding to individuals rather than to +generalized quantifiers. + +The main difference between the intensional types and the extensional +types is that in the intensional types, the arguments are functions +from worlds to extensions: intransitive verb phrases like "left" now +take so-called "individual concepts" as arguments (type s->e) rather than plain +individuals (type e), and attitude verbs like "think" now take +propositions (type s->t) rather than truth values (type t). +In addition, the result of each predicate is an intension. +This expresses the fact that the set of people who left in one world +may be different than the set of people who left in a different world. +(Normally, the dependence of the extension of a predicate to the world +of evaluation is hidden inside of an evaluation coordinate, or built +into the the lexical meaning function, but we've made it explicit here +in the way that the intensionality monad makes most natural.) + +The intensional types are more complicated than the extensional +types. Wouldn't it be nice to make the complicated types available +for those expressions like attitude verbs that need to worry about +intensions, and keep the rest of the grammar as extensional as +possible? This desire is parallel to our earlier desire to limit the +concern about division by zero to the division function, and let the +other functions, like addition or multiplication, ignore +division-by-zero problems as much as possible. + +So here's what we do: + +In OCaml, we'll use integers to model possible worlds. Characters (characters in the computational sense, i.e., letters like `'a'` and `'b'`, not Kaplanian characters) will model individuals, and OCaml booleans will serve for truth values: + + type s = int;; + type e = char;; + type t = bool;; + + let ann = 'a';; + let bill = 'b';; + let cam = 'c';; + + let left1 (x:e) = true;; + let saw1 (x:e) (y:e) = y < x;; + + left1 ann;; (* true *) + saw1 bill ann;; (* true *) + saw1 ann bill;; (* false *) + +So here's our extensional system: everyone left, including Ann; +and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word +order we're using is VOS, verb-object-subject.) + +Now we add intensions. Because different people leave in different +worlds, the meaning of *leave* must depend on the world in which it is +being evaluated: + + let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;; + left ann 1;; (* true: Ann left in world 1 *) + left cam 2;; (* false: Cam didn't leave in world 2 *) + +This new definition says that everyone always left, except that +in world 2, Cam didn't leave. + +Note that although this general *left* is sensitive to world of +evaluation, it does not have the fully intensionalized type given in +the chart above, which was `(s->e)->s->t`. This is because +*left* does not exploit the additional resolving power provided by +making the subject an individual concept. In semantics jargon, we say +that *leave* is extensional with respect to its first argument. + +Therefore we will adopt the general strategy of defining predicates +in a way that they take arguments of the lowest type that will allow +us to make all the distinctions the predicate requires. When it comes +time to combine this predicate with monadic arguments, we'll have to +make use of various lifting predicates. + +Likewise, although *see* depends on the world of evaluation, it is +extensional in both of its syntactic arguments: + + let saw x y w = (w < 2) && (y < x);; + saw bill ann 1;; (* true: Ann saw Bill in world 1 *) + saw bill ann 2;; (* false: no one saw anyone in world 2 *) + +This (again, partially) intensionalized version of *see* coincides +with the `saw1` function we defined above for world 1; in world 2, no +one saw anyone. + +Just to keep things straight, let's review the facts: + +
```+     World 1: Everyone left.
+              Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
+     World 2: Ann left, Bill left, Cam didn't leave.
+              No one saw anyone.
+```
```+type 'a intension = s -> 'a;;
```+lift2' saw (unit bill) (unit ann) 1;;  (* true *)