# Environment Model
Today we will study the semantics given in the most recent lecture notes on
[a core sub-language of OCaml](core-ocaml.html).
## Evaluation
In the small-step substitution model, evaluation of an expression was
rather *list-like*: we could write an evaluation in a linear form
like `e --> e1 --> e2 --> ... --> en --> v`. In the big-step environment
model, evaluation is instead rather *tree-like*: evaluations have a
nested, recursive structure. Here's an example:
```
<[], (3 + 5) * 2> ==> 16 (op rule)
because <[], (3 + 5)> ==> 8 (op rule)
because <[],3> ==> 3 (int const rule)
and <[],5> ==> 5 (int const rule)
and 3+5 is 8
and <[], 2> ==> 2 (int const rule)
and 8*2 is 16
```
We've used indentation here to show the shape of the tree, and we've labeled
each usage of one of the semantic rules. A more textbook-style presentation
of that same information would be the following *proof tree*:
![](infer/infer.png)
(You can see the \\(\LaTeX\\) source for that image here: [infer.tex](infer/infer.tex).
To avoid requiring everyone in the class to learn \\(\LaTeX\\), though, we will
continue to use a plain ASCII representation of proof trees, as in the first
example above.)
##### Exercise: simple expressions [✭]
Evaluate the following expressions using the big-step environment model.
Use the notation for evaluation that we demonstrated in either of the examples
above, in which you provide a hint as to which rule is applied at each
node in the tree.
- `110 + 3*1000` *hint: three uses of the constant rule, two uses of the op rule*
- `if 2 + 3 < 4 then 1 + 1 else 2 + 2` *hint: five uses of constant, three uses of op,
one use of if(else)*
□
##### Exercise: let and match expressions [✭✭]
Evaluate these expressions, continuing to use the tree notation (either
plain text or graphical), and continuing to label each usage of a rule.
- `let x=0 in 1` *hint: one use of let, two uses of constant*
- `let x=2 in x+1` *hint: one use of let, two uses of constant, one use of op, one
use of variable*
- `match Left 2 with Left x -> x+1 | Right x -> x-1` *hint: one use of match(left),
two uses of constant, one use of op, one use of variable*
□
##### Exercise: closures [✭✭]
Evaluate these expressions, continuing to use the tree notation (either
plain text or graphical), and continuing to label each usage of a rule.
- `(fun x -> x+1) 2` *hint: one use of application, one use of anonymous function,
two uses of constant, one use of op, one use of variable*
- `let f = fun x -> x+1 in f 2` *hint: one use of let, one use of anonymous function,
one use of application, two uses of variable, one use of op, two uses of constant*
□
##### Exercise: lexical scope and shadowing [✭✭]
Evaluate these expressions, continuing to use the tree notation (either
plain text or graphical), and continuing to label each usage of a rule.
- `let x=0 in x + (let x=1 in x)` *hint: two uses of let, two uses of variable,
one use of op, two uses of constant*
- `let x=1 in let f=fun y -> x in let x=2 in f 0` *hint: three uses of let, one use
of anonymous function, one use of application, two uses of variable, three uses of constant*
□
## Dynamic scope
Recall that dynamically scoped languages use the following evaluation
rules for anonymous functions and function application:
```
e> ==> fun x -> e
==> v
if ==> fun x -> e
and ==> v2
and v2],e> ==> v
```
##### Exercise: dynamic scope [✭✭✭]
Use dynamic scope to evaluate the following expression. You do not
need to write down all of the evaluation steps unless you find it
helpful. Compare your answer to the answer you would expect from a
language with lexical scope.
```
let x = 5 in
let f y = x + y in
let x = 4 in
f 3
```
## Additional exercises
##### Exercise: more evaluation [✭✭]
- `let x = 2 + 2 in x + x`
- `let x = 1 in let x = x + x in x + x`
- `let f = fun x -> fun y -> x + y in let g = f 3 in g 2`
- `let f = fst (let x = 3 in fun y -> x, 2) in f 0`
□
##### Exercise: more dynamic scope [✭✭✭]
Use dynamic scope to evaluate the following expressions.
Compare your answers to the answers you would expect from a
language with lexical scope.
Expression 1:
```
let x = 5 in
let f y = x + y in
let g x = f x in
let x = 4 in
g 3
```
Expression 2:
```
let f y = x + y in
let x = 3 in
let y = 4 in
f 2
```
□
Okay, that's it for the wacky world of dynamic scope. We now return to lexical scope.
## Challenge exercise: References
Let's add refs to the core language:
```
e ::= ...
| ()
| ref e
| !e
| e1 := e2
v ::= ... | () | loc
loc ::= memory locations
```
Think of *memory locations* as being like addresses in memory. They are another example
of a type of value that cannot be written directly inside of a program, like closures.
The expression `ref e` allocates a new memory location, stores a value at it, and returns
a pointer to that location; `!e` dereferences a pointer and retrieves the value stored
at a location; and `e1 := e2` evaluates `e1` to a pointer, `e2` to a value, and stores
the value at the location pointed to by `e1`.
We extend machine configurations to represent the *state* of memory. We'll write
`st` as a meta-variable to represent states. A state maps locations to values.
We'll write `st(loc)` to mean looking up the value stored at location `loc` in `st`,
and `st[loc->v]` to mean updating the value stored at location `loc` in `st` to be `v`.
This is the same notation we're using for environments. Also, we'll say that
`loc` is *fresh* for `st` if `st` does not currently map `loc` to any value.
Fresh locations are needed to do allocation. As concrete values for locations,
we might write integers. For example, a state might map memory location `1` to
a string value `"bigred"` after the allocation `ref "bigred"`, though there's no
way for the programmer to know that memory location `1` was chosen as opposed
to any other location.
The big-step judgement becomes a quinternary relation:
```
==>
```
Read that as "evaluating `e` in environment `env` and state `st` produces value `v`
and a new state `st'`." The reason that `st'` is needed on the right-hand side
is because evaluation of `e` might change the state, and we need to track such changes.
Here are the evaluation rules for the four new expressions, an updated rule for let,
and rule for semicolon that is a specialization of the let rule (recalling that
semicolon is syntactic sugar for let):
```
<(), env, st> ==> <(), st>
[ ==> v]>
if ==>
and loc is fresh for st'
==>
if ==>
==> <(), st2[loc->v]>
if ==>
and ==>
==>
if ==>
and v1], st1> ==>
==>
if ==>
and ==>
```
##### Exercise: evaluate refs [✭✭✭]
Evaluate these expressions.
- `let x = ref 0 in (x := x + 1; !x)`
- `let x = ref (ref 0) in let y = ref 1 in x := y`
□
##### Exercise: update rules [✭✭✭✭]
Update all the rest of the rules of core OCaml to use states. You'll need to
figure out how to thread the state through the rules. *Hint: closures remain
unchanged; they contain only a function and its environment, not any state.*
□
]