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 <code>x<sub>1</sub>, x<sub>2</sub>, x<sub>3</sub></code>, 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 <code>x<sub>1</sub></code>, 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:
-<pre><code>\x<sub>2</sub>. x (\x<sub>8</sub>. x<sub>8</sub> x<sub>2</sub>)
+<pre><code>\x<sub>2</sub>. x<sub>2</sub> (\x<sub>8</sub>. x<sub>8</sub> x<sub>2</sub>)
</code></pre>
In any event, though, we won't make use of de Bruijn notation because, though it makes the semantic algorithms more elegant, it also adds an extra level of conceptual complexity, which we don't want to do.]
(\x. M) N ~~> M {x <- N}
-we'll instead evaluate them by manipulating their environment. (To intepret `(\x. M) N` in environment `e`, we'll interpret `M` in an environment like `e {x:= N}` where `x` may have been changed to now be assigned to `N`.
+we'll instead evaluate them by manipulating their environment. To intepret `(\x. M) N` in environment `e`, we'll interpret `M` in an environment like `e {x:= N}` where `x` may have been changed to now be assigned to `N`.
A few comments. First, what the environment associates with the variable `x` will be expressions of the lambda calculus we're evaluating. If we understand the evaluation to be call-by-name, these expressions may be complexes of the form `N P`. If on the other hand, we understand the evaluation to be call-by-value, then these expressions will always be fully evaluated before being inserted into the environment. That means they'll never be of the form `N P`; but only of the form `y` or `\y. P`. The latter kinds of expressions are called "values." But "values" here are just certain kinds of expressions. (They *could* be the denotations of lambda expressions, if one thinks of the lambda expressions as all having normal-form lambda terms as their denotations, when possible.)
With these ideas settled, then, we can present an environment-based operational semantics for the untyped lambda calculus. Here is a call-by-value version, which assumes that expressions are always fully evaluated before being inserted into the environment.
-1. When `e` assigns some term `v` to `x`, then `x`fully (that is, terminally) reduces in environment `e` to `v`. We write that as: `(e |- x) ==> v`.
+1. When `e` assigns some term `v` to `x`, then `x` fully (that is, terminally) reduces in environment `e` to `v`. We write that as: `(e |- x) ==> v`.
-2. `(e |- \x. M) ==> closure(e, \x. M)`, where a closure is some data-structure (it might just be a pair of the data-structure `e` and the formula `\x. M`).
+2. `(e |- \x. M) ==> closure(e, \x. M)`, where a closure is some data-structure (it might just be a pair of the environment `e` and the formula `\x. M`).
3. If `(e |- M) ==> closure(e2, \x. M2)` and `(e |- N) ==> v` and `(e2 {x:=v} |- M2) ==> u`, then `(e |- M N) ==> u`. Here `e2 {x:=v}` is the environment which is just like `e2` except it assigns `v` to `x`.
Yes! You can do so with a monad, in much the same way we did with our checks for divide-by-zero failures.
-Here we'll use a different monad. It's called the **reader monad**. We define it like this:
+Here we'll use a different monad. It's called the **Reader monad**. We define it like this:
(* we assume we've settled on some implementation of the environment *)
type env = (char * int) list;;
\[[man who(i): Alice spurned i]]
is the result of combining \[[man]], an `e->t` type predicate value, with the adjective-type value of \[[who(i): Alice spurned i]]. As I said, we'll ignore complexities about their treatment of adjectives. But how is \[[who(i): Alice spurned i]] derived? Heim and Kratzer say this is defined only relative to an
-assignment g, and it's defined to be a function from objects x in the domain to the value \[[Alice spurned i]] has relative to shifted assignment g {i:=x}, which is like g except for assigning object x to variable i. So this is not the result of taking some value \[[who(i)]], and some separate value \[[Alice spurned i]], and supplying one of them to the other as argument to function.
+assignment g, and it's defined to be a function from objects x in the domain to the value that \[[Alice spurned i]] has relative to shifted assignment g {i:=x}, which is like g except for assigning object x to variable i. So this is not the result of taking some value \[[who(i)]], and some separate value \[[Alice spurned i]], and supplying one of them to the other as argument to function.
Getting any ideas?
-Yes! We can in fact implement this as a reader monad. And in doing so, we *will* get a value \[[who(i)]] which is a function, and another value \[[Alice spurned i]], to be its argument. So the semantics in the first place again becomes compositional, and in the second place doesn't need any special rule for how \[[who(i): Alice spurned i]] is derived. It uses the same composition rule as other complex expressions.
+Yes! We can in fact implement this as a Reader monad. And in doing so, we *will* get a value \[[who(i)]] which is a function, and another value \[[Alice spurned i]], to be its argument. So the semantics in the first place again becomes compositional, and in the second place doesn't need any special rule for how \[[who(i): Alice spurned i]] is derived. It uses the same composition rule as other complex expressions.
How does this work?
We set \[[Alice]] = the reader-monad value `unit Alice`.
-We have to lift the semantic values of predicates into the reader-monad. So if before we were taking the semantic value of "spurned" to be a function `S` of type `e -> e -> t`, now we set \[[spurned]] = lift2 S.
+We have to lift the semantic values of predicates into the Reader monad. So if before we were taking the semantic value of "spurned" to be a function `S` of type `e -> e -> t`, now we set \[[spurned]] = `lift2 S`.
Finally, we set \[[who(i)]] to be:
fun (u : bool reader) (v : entity reader) -> shift i v u
-You can trace through what happens then if we apply \[[who(i)]] to (\[[spurned]] applied to \[[Alice]] and \[[i]]):
+You can trace through what happens then if we apply \[[who(i)]] to \[[Alice spurned i]]:
- \[[Alice spurned i]] = \[[spurned]] \[[Alice]] \[[i]]
- = (lift2 S) (unit Alice) (lookup i)
- = bind (unit Alice) (fun x -> bind (lookup i) (fun y -> unit (S x y)))
+ \[[Alice spurned i]] = \[[spurned]] \[[i]] \[[Alice]]
+ = (lift2 S) (lookup i) (unit Alice)
+ = bind (lookup i) (fun x -> bind (unit Alice) (fun y -> unit (S x y)))
because of the left-identity rule for `unit`, this is the same as:
- = bind (lookup i) (fun y -> unit (S Alice y))
+ = bind (lookup i) (fun x -> unit (S x Alice))
Substituting in the definition of `bind` for the reader-monad, this is:
- = fun e -> (fun y -> unit (S Alice y)) (lookup i e) e
- = fun e -> unit (S Alice (lookup i e)) e
+ = fun e -> (fun x -> unit (S x Alice)) (lookup i e) e
+ = fun e -> unit (S (lookup i e) Alice) e
Substituting in the definition of `unit`, this is:
- = fun e -> S Alice (lookup i e)
+ = fun e -> S (lookup i e) Alice
And now supplying \[[Alice spurned i]] as an argument to \[[who(i)]], we get:
\[[who(i): Alice spurned i]] = \[[who(i)]] \[[Alice spurned i]]
- = (fun u v -> shift i v u) (fun e -> S Alice (lookup i e))
- = fun v -> shift i v (fun e -> S Alice (lookup i e))
+ = (fun u v -> shift i v u) (fun e -> S (lookup i e) Alice)
+ = fun v -> shift i v (fun e -> S (lookup i e) Alice)
Substituting in the definition of `shift`, this is:
- = fun v -> (fun c v u e -> u ((c, v e) :: e)) i v (fun e -> S Alice (lookup i e))
- = fun v -> (fun u e -> u ((i, v e) :: e)) (fun e -> S Alice (lookup i e))
- = fun v -> (fun e -> (fun e -> S Alice (lookup i e)) ((i, v e) :: e))
- = fun v -> (fun e -> S Alice (lookup i ((i, v e) :: e)) )
- = fun v -> (fun e -> S Alice (v e) )
+ = fun v -> (fun c v u e -> u ((c, v e) :: e)) i v (fun e -> S (lookup i e) Alice)
+ = fun v -> (fun u e -> u ((i, v e) :: e)) (fun e -> S (lookup i e) Alice)
+ = fun v -> (fun e -> (fun e -> S (lookup i e) Alice) ((i, v e) :: e))
+ = fun v -> (fun e -> S (lookup i ((i, v e) :: e)) Alice)
+ = fun v -> (fun e -> S (v e) Alice)
-In other words, it's a function from entity reader monads to a function from assignment functions to the result of applying S to Alice and the value of that entity reader-monad under that assignment function. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[Alice]] and \[[i]].
+In other words, it's a function from entity reader monads to a function from assignment functions to the result of applying S to the value of that entity reader-monad under that assignment function, and to Alice. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[i]] and \[[Alice]].
What's not to like?