Recitation 7: Examples of evaluation

We started off this course using the substitution model to understand how OCaml programs evaluate. The basic idea is simple: evaluate subexpressions to values, and when you have a function call, substitute the argument value for the formal parameter within the body of the function, and then evaluate the resulting expression.

But the substitution model is not without its shortcomings.  It's not a very efficient or realistic model of OCaml programs are really evaluated. It's also difficult to extend the substitution model to support side effects, which we will soon be covering. So last week we introduced a more realistic semantics called the environment model that is much closer to how OCaml is really implemented.

The environment model

Let's review the environment model. We start with a core sublanguage of OCaml:

e ::= c | (op) | x | (e1, ..., en) | C e | e1 e2
    | fun x -> e | let x = e1 in e2 
    | match e0 with p1 -> e1 | ... | pn -> en
    | let rec f x = e1 in e2

where e represents an expression, c a constant, (op) a built-in operator, x and f an identifier, C a constructor, and p a pattern. Expressions are evaluated with respect to an environment, which is a mapping from identifiers to values. We can think of an environment as a set of substitutions that we have delayed making.

Values are, except for closures, a syntactic subset of expressions:

v ::= c | (op) | x | (v1, ..., vn) | C v
    | << f, fun x -> e, env >>

where env is an environment and << f, fun x -> e, env >> is a recursive closure. The closure records the name f of a recursive function, its implementation fun x -> e, and the dynamic environment env that was current at the time the function was defined. If the function is anonymous, rather then recursive, then we just leave the name out of the closure, so that it looks like << fun x -> e, env >>

We write env :: e --> v to mean that e evaluates to v in environment env. We write env(x) to look up the value of x in env. We write {} to mean the empty environment (which is never truly empty, because OCaml opens Pervasives automatically). We write env+{x=v} to mean the same environment as env, except that x is now bound to v instead of whatever value (if any) it had before.

Evaluation rules in the environment model

Constants and operators:

env :: c --> c
env :: (op) --> (op)


if env(x) = v 
then env :: x --> v


if env :: e --> v
then env :: C e --> C v


if env :: en --> vn
and ...
and env :: e2 --> v2
and env :: e1 --> v1
then env :: (e1,...,en) --> (v1,...,vn)

Let expressions:

if env :: e1 --> v1
and env + {x=v1} :: e2 --> v2
then env :: (let x = e1 in e2) --> v2

Let rec expressions:

If env + {f=<< f, fun x -> e1, env >>} :: e2 --> v2
then env :: (let rec f x = e1 in e2) --> v2

Match expressions:

if env :: e0 --> v0
and pi is the first pattern to match v0
and that match produces bindings b
and env+b :: ei --> vi
then env :: (match e0 with p1 -> e1 | ... | pn -> en) --> vi

Function expressions:

env :: (fun x -> e) --> << fun x -> e, env >>

Anonymous function application:

if env :: e2 --> v2
and env :: e1 --> << fun x-> e, env' >>
and env' + {x=v2} :: e --> v
then env :: (e1 e2) --> v

Recursive function application:

if env :: e2 --> v2
and env :: e1 --> << f, fun x-> e, env' >>
and env' + {x=v2, f=<< f, fun x-> e, env' >>} :: e --> v
then env :: (e1 e2) --> v

Primitive operator application:

and env :: e1 --> v1
and env :: e --> (op)
then env :: ((op) e1) --> "op" e1
(* where "op" means the primitive operator built-in to OCaml *)

The evaluation rules above use lexical scope, in which the meaning of a variable name is determined by where the name appears lexically in the source code, rather than when the variable name is dynamically evaluated. The latter would be dynamic scope. We saw rules for dynamic scope in lecture. OCaml (and nearly all modern languages) use lexical scope.

You should practice evaluating some expressions using the environment model to see how it works.

Example 1.

let d = 2 in
let f = fun x -> x + d in
let d = 1 in
f 2


Example 2.

let rec fact n = if n = 0 then 1 else n * (fact (n-1)) 
in fact 1


Example 3.

let rec filter = fun f -> fun xs ->
  (match xs with
     [] -> []
   | x::xs' -> if f x then x::(filter f xs') else filter f xs') in
let all_gt = fun n -> fun xs -> filter (fun x -> x > n) xs in
all_gt 1 [1;2]


Those examples get tedious. It's no wonder we have computers to compute them for us!