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 || v
```

Recall 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 2
```

Here 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 = 4
```

The 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 || v
```

As 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 1
```

How can we handle `if`

? We could desugar `if`

into `match`

:

```
if e1 then e2 else e3
=
match e1 with Left _ -> e2 | Right _ -> e3
```

And 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 || v
```

We 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`

.