The Environment Model

Step Relation¶

General Rules: don’t step on values; don’t step on variables

• Small/Single Step Relation: e --> e', where e’ can be a value or another expression yet to be evaluated to a value
• Multi-Step Relation: e -->* e' is the reflexive closure of single step. It allows single step to be performed 0 or multiple times
• Big-Step Relation: e ==> v step expressions to values through multi-step and stop when it becomes values.

Introduction¶

For sake of efficiency, it would be better to substitute lazily: only when the value of a variable is needed should the interpreter have to do the substitution. That’s the key idea behind the environment model. In this model, there is a data structure called the dynamic environment, which is a dictionary mapping variable names to values. Whenever the value of a variable is needed, it’s looked up in that dictionary. （空间换时间）

Instead of e ==> v, we now have <env, e> ==> v, where env denotes the environment, and <env, e> is called a machine configuration. That configuration represents the state of the computer as it evaluates a program: env represents a part of the computer’s memory (the binding of variables to values), and e represents the program.

• {} represent the empty environment,
• {x1:v1, x2:v2, ...} represent the environment that binds x1 to v1, etc.
• env[x -> v] represent the environment env with the variable x additionally bound to the value v
• env(x) represent the binding of x in env.

Evaluation¶

Trivially,

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

Problem¶

However, when we try to define the rules of function application, we run into trouble. Intuitively, we would write something like this, where we sort of “substitute” all the occurrences of x in e with v2 and get the result v.

<env, e1 e2> ==> v
  if <env, e1> ==> fun x -> e
  and <env, e2> ==> v2
  and <env[x -> v2], e> ==> v

let x = 1 in
let f = fun y -> x in
let x = 2 in
f 0

According to our semantics thus far, it would evaluate as follows:

• let x = 1 would produce the environment {x:1}.

• let f = fun y -> x would produce the environment {x:1, f:(fun y -> x)}.

• let x = 2 would produce the environment {x:2, f:(fun y -> x)}. Note how the binding of x to 1 is shadowed by the new binding.

• Now we would evaluate <{x:2, f:(fun y -> x)}, f 0>

  <{x:2, f:(fun y -> x)}, f 0> ==> 2
    because <{x:2, f:(fun y -> x)}, f> ==> fun y -> x
    and <{x:2, f:(fun y -> x)}, 0> ==> 0
    and <{x:2, f:(fun y -> x)}[y -> 0], x> ==> 2`
      because <{x:2, f:(fun y -> x), y:0}, x> ==> 2`

• The result is therefore 2.

However, this should evaluate to 1. Notice that we evaluated e1 in the current environment, or more formally, we used a dynamic scope here.

Dynamic vs. Static Scope¶

• Dynamic Scope: the body of a function is evaluated in the current dynamic environment at the time the function is called, i.e. it uses the latest binding
• Lexical Scope: the body of a function is evaluated in the old dynamic environment that existed at the time the function was defined.

Most modern languages use lexical scope.

Implementing Time Travel¶

We have to store the variable binding at the time the function was defined. We define a new data structure called “closure” with two parts: (|exp, env|), where exp is the expression we are concerned about, and env the environment when the expression was defined.

Since we only have to consider scope in function application, the exp in our closure must always be a function, denoted by fun x -> e. Therefore, we can also write our closure as (|x, exp, env|), where x is the argument name, e is the function body, and env is the environment when this function was defined. In fact, that’s how we define it when implementing the Environment Model.

When we use big-step relation in evaluation, we say the result must be a value. Here, we can consider closure to be the value evaluated from a function. <env, fun x -> e> ==> (| fun x -> e, env |)

Using closure, we can now correctly define evaluation of function applications. (defenv represents the environment when e1 was defined)

<env, e1 e2> ==> v
  if <env, e1> ==> (| fun x -> e, defenv |)
  and <env, e2> ==> v2
  and <defenv[x -> v2], e> ==> v