# 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 [&#10029;] 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)* &square; ##### Exercise: let and match expressions [&#10029;&#10029;] 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* &square; ##### Exercise: closures [&#10029;&#10029;] 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* &square; ##### Exercise: lexical scope and shadowing [&#10029;&#10029;] 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* &square; ## Dynamic scope Recall that dynamically scoped languages use the following evaluation rules for anonymous functions and function application: ``` <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 ``` ##### Exercise: dynamic scope [&#10029;&#10029;&#10029;] 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 ``` <!-- answer: 7 --> ## Additional exercises ##### Exercise: more evaluation [&#10029;&#10029;] - `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` &square; ##### Exercise: more dynamic scope [&#10029;&#10029;&#10029;] 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 ``` &square; <!-- answers: 6, 5 --> 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: ``` <e, env, st> ==> <v, st'> ``` 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> <ref e, env, st> ==> <loc, st'[loc->v]> if <e, env, st> ==> <v, st'> and loc is fresh for st' <!e, env, st> ==> <st(loc), st'> if <e, env, st> ==> <loc, st'> <e1 := e2, env, st> ==> <(), st2[loc->v]> if <e1, env, st> ==> <loc, st1> and <e2, env, st1> ==> <v, st2> <let x = e1 in e2, env, st> ==> <v2, st2> if <e1, env, st> ==> <v1, st1> and <e2, env[x->v1], st1> ==> <v2, st2> <e1; e2, env, st> ==> <v2, st2> if <e1, env, st> ==> <v1, st1> and <e2, env, st1> ==> <v2, st2> ``` ##### Exercise: evaluate refs [&#10029;&#10029;&#10029;] 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` &square; ##### Exercise: update rules [&#10029;&#10029;&#10029;&#10029;] 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.* &square;