[[!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]]
```