Recall that, in the environment model semantics, an expression e reduces to a value v in an environment env, and we denote that as env :: e || v.
Here's the environment model semantics for the entire core sublanguage from the previous recitation:
env :: n || n
env :: e1 + e2 || n
if env :: e1 || n1 and env :: e2 || n2
and n is the result of applying primitive operation +
to n1 and n2
env :: (e1, e2) || (v1, v2)
if env :: e1 || v1 and env :: e2 || v2
env :: fst e || v1
if env :: e || (v1,v2)
env :: snd e || v2
if env :: e || (v1,v2)
env :: Left e || Left v
if env :: e || v
env :: Right e || Right v
if env :: e || v
env :: match e with Left x -> e1 | Right y -> e2 || v1
if env :: e || Left v
and env+{x=v} :: e1 || v1
env :: match e with Left x -> e1 | Right y -> e2 || v2
if env :: e || Right v
and env+{y=v} :: e2 || v2
env :: let x = e1 in e2 || v2
if env :: e1 || v1
and env+{x=v1} :: e2 || v2
env :: x || v
if env(x) = v
env :: (fun x -> e) || <<fun x -> e, env>>
env :: e1 e2 || v
if env :: e1 || <<fun x -> e, env'>>
and env :: e2 || v2
and env' + {x=v2} :: e || v
env :: let rec f x = e1 in e2 || v
if env + {f = <<f, fun x -> e1, env>>} :: e2 || v
env :: e1 e2 || v
if env :: e1 || <<f, fun x -> e, env'>>
and env :: e2 || v2
and env' + {x=v2,f=<<f, fun x -> e, env'>>} :: e || vRecall that <<fun x -> e, env>> is a closure, which is used by lexical scoping to record the values of all free variables of a function at the time the function is defined. And <<f, fun x-> e, env>> is a recursive closure that records the function's name.
Here's an example we did in the previous recitation with the substitution model, but we omitted it then in the environment model, because we didn't have the rules for functions and application. We can now do the example:
{} :: (fun x -> x+1) 2 || 3
{} :: fun x -> x+1 || <<fun x -> x+1, {}>>
{} :: 2 || 2
{} + {x=2} :: x+1 || 3
{x=2} :: x || 2
{x=2} :: 1 || 1
2+1 = 3
We're now omitting the English words like "because", simply for brevity, seeing as you now know how to read these proof trees.
Consider this program:
let d = 2 in
let f = fun x -> x + d in
let d = 1 in
f 2Here is how it evaluates in the environment model:
{} :: let d = 2 in (let f = fun x -> x+d in (let d = 1 in f 2)) || 4
{} :: 2 || 2
{} + {d=2} :: let f = fun x -> x+d in (let d = 1 in f 2) || 4
{d=2} :: fun x -> x+d || <<fun x -> x+d, {d=2}>>
{d=2, f=<<fun x -> x+d, {d=2}>>} :: let d = 1 in f 2 || 4
{d=2, f=<<fun x -> x+d, {d=2}>>} :: 1 || 1
*{d=1, f=<<fun x -> x+d, {d=2}>>} :: f 2 || 4
{d=1, f=<<fun x -> x+d, {d=2}>>} :: f || <<fun x -> x+d, {d=2}>>
{d=1, f=<<fun x -> x+d, {d=2}>>} :: 2 || 2
**{d=2}+{x=2} :: x+d || 4
{d=2,x=2} :: x || 2
{d=2,x=2} :: d || 2
2+2 = 4The key steps to observe are those labeled * and **. In *, the function closure still binds d to 2, even though the outer environment changes to bind d to 1. In **, the environment is extracted from the function closure, causing d to be bound to 2.
With dynamic scoping, the function evaluation rules would change to the following:
DYNAMIC SCOPING
env :: (fun x -> e) || (fun x -> e)
env :: e1 e2 || v
if env :: e1 || (fun x -> e)
and env :: e2 || v2
and env + {x=v2} :: e || vAs an additional exercise, try redoing the example above with dynamic scoping. Note that you won't use any closures.
Consider this program:
let rec fact n =
if n = 0 then 1 else n * (fact (n-1))
in fact 1How can we handle if? We could desugar if into match:
if e1 then e2 else e3
=
match e1 with Left _ -> e2 | Right _ -> e3And now our Boolean operators, such as n=0, would need to return Left c for true and Right c for false; any constant c would suffice.
Or we could simply introduce new rules for if:
env :: if e1 then e2 else e3 || v
if env :: e1 || true
and env :: e2 || v
env :: if e1 then e2 else e3 || v
if env :: e1 || false
and env :: e3 || vWe now would have two new constant values, true and false, which evaluate to themselves.
Using those new rules and values, we can evaluate the program. For brevity, let F denote the expression if n = 0 then 1 else n * (fact (n-1)), and let cl denote the closure <<fact, fun n -> F, {}>>:
{} :: let rec fact n = F in fact 1 || 1
{fact=cl} :: fact 1 || 1
{fact=cl} :: fact || cl
{fact=cl} :: 1 || 1
{n=1,fact=cl} :: F || 1
{n=1,fact=cl} :: n = 0 || false
{n=1,fact=cl} :: n || 1
{n=1,fact=cl} :: 0 || 0
the result of applying primitive operator = to 1 and 0 is false
{n=1,fact=cl} :: n * (fact (n-1)) || 1
{n=1,fact=cl} :: n || 1
{n=1,fact=cl} :: fact (n-1) || 1
{n=1,fact=cl} :: fact || cl
{n=1,fact=cl} :: n-1 || 0
{n=1,fact=cl} :: n || 1
{n=1,fact=cl} :: 1 || 1
1-1 is 0
{n=0,fact=cl} :: F || 1
{n=0,fact=cl} :: n = 0 || true
{n=0,fact=cl} :: n || 0
{n=0,fact=cl} :: 0 || 0
the result of applying primitive operator = to 0
and 0 is true
{n=0,fact=cl} :: 1 || 1
1 * 1 is 1
let rec filter f xs =
(match xs with
| [] -> []
| x::xs' -> if f x then x::(filter f xs') else filter f xs') in
let all_gt n xs = filter (fun x -> x > n) xs in
all_gt 1 [1;2]The entire proof tree here would be tediously long to construct, so let's instead consider one key detail: how does n evaluate to 1 inside the anonymous function in the penultimate line?
The final line starts with a function application all_gt 1. In the dynamic environment at the time of that application, all_gt would be bound to a closure <<fun n -> fun xs -> filter (fun x -> x > n) xs, {filter=F}>>. (We omit the closure to which filter is bound for brevity, and simply write F.) So the application would evaluate to a new closure, <<fun xs -> filter (fun x -> x > n) xs, {filter=F, n=1}>>. That closure would then be applied to [1;2], yielding the expression filter (fun x -> x > n) xs, which would be evaluated in the environment {filter=F, n=1, xs=[1;2]}. That expression begins with a function application, filter (fun x -> x > n). The filter part of that evaluates to a closure F. The argument, fun x -> x > n, evaluates to a new closure. The code part of that new closure is fun x -> x > n, and the environment part is {filter=F, n=1, xs=[1;2]}. That environment binds n to 1.
So whenever the filtering function f is evaluated inside of filter, it evaluates to the closure <<fun x -> x > n, {filter=F, n=1, xs=[1;2]}>>. Since neither filter nor xs appear in the code part of the closure, their values don't really matter. But n does appear, and it will evaluate to 1.