# Environment Model The environment model, like the [substitution model][subst], is a way of thinking about how OCaml programs evaluate. It uses a *big-step semantics* that describes how an expression *evaluated* down to a *value*. [subst]: ../17-subst-model/core-ocaml.html ## Notation - `<env,e>` is a *machine configuration*. The machine's environment is `env` and the code remaining to be evaluated is `e`. - `<env,e> ==> v` means "`e` evaluates or big-steps to `v` in environment `env`" - `(|fun x -> e, env|)` denotes a *closure* with environment `env`. - `{x1:v1, x2:v2, ...}` denotes the environment with `x1` bound to `v1`, `x2` bound to `v2` and so on. - `env[x->v]` denotes the environment `env` extended with a binding from `x` to `v`. If `env` already has a binding for `x` then it is replaced. - `env(x)` denotes the value associated with `x` in `env`. ## Syntax ``` e ::= x | e1 e2 | fun x -> e | n | b | e1 + e2 | (e1,e2) | fst e1 | snd e2 | Left e | Right e | match e with Left x1 -> e1 | Right x2 -> e2 | if e1 then e2 else e3 | let x = e1 in e2 ``` Operator `+` may be any primitive binary operator, such as addition, multiplication, equality, or less than. ## Semantics ``` <env, x> ==> v if env(x) = v <env, e1 e2> ==> v' if <env,e1> ==> (|fun x -> e, newenv|) and <env,e2> ==> v and <newenv[x->v],e> ==> v' <env, fun x -> e> ==> (|fun x -> e, env|) <env, n> ==> n <env, b> ==> b <env, e1 + e2> ==> n if <env,e1> ==> n1 and <env,e2> ==> n2 and n is the result of applying the 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 x1 -> e1 | Right x2 -> e2> ==> v1 if <env,e> ==> Left v and <env[x1->v], e1> ==> v1 <env, match e with Left x1 -> e1 | Right x2 -> e2> ==> v2 if <env,e> ==> Right v and <env[x2->v], e2> ==> v2 <env, if e1 then e2 else e3> ==> v2 if <env,e1> ==> true and <env,e2> ==> v2 <env, if e1 then e2 else e3> ==> v3 if <env,e1> ==> false and <env,e3> ==> v3 <env, let x = e1 in e2> ==> v2 if <env,e1> ==> v1 and <env[x->v1],e2> ==> v2 ```