Environments Closures Refinement
1
Environments
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
Environments
Closures
Refinement
Where we’re at
We refined the abstract M-Machine to a C-Machine, with explicit stacks: s≻e s≺v
Function application is still executed via substitution:
(Apply⟨⟨f.x.e⟩⟩)◃s≺v →C s≻e[x:=v,f :=(Fun(f.x.e))]
We’re going to extend our C-Machine to replace substitutions with an environment, giving us a new E-Machine
2
Environments Closures Refinement
Environments
Definition
An environment is a context containing equality assumptions about variables. It can be viewed like a state that maps variables to their values, except that a variable’s value does not change over time.
η Env •Env x=v,ηEnv
We write η(x) to indicate the leftmost value corresponding to x in η. Let’s change our machine states to include an environment:
s|η≻e s|η≺v
3
Environments Closures Refinement
First Attempt
First, we’ll add a rule for consulting the environment if we encounter a free variable:
s | η ≻ x →E s | η ≺ η(x) Then, we just need to handle function application.
One broken attempt:
(Apply⟨⟨f.x.e⟩⟩)◃s|η≺v →E s|(x=v,f =⟨⟨f.x.e⟩⟩,η)≻e We don’t know when to remove the variables again!
4
Environments Closures Refinement
Second Attempt
We will extend our stacks to allow us to save the old environment to it. s Stack η Env
η ◃ s Stack
Calling a function, we save the environment to the stack.
(Apply⟨⟨f.x.e⟩⟩)◃s|η≺v →E η◃s|(x=v,f =⟨⟨f.x.e⟩⟩,η)≻e When the function returns, we restore the old environment, clearing out the new
bindings:
5
η◃s|η′≺v →E s|η≺v
Environments
Closures
Refinement
6
◦ (Ap (N 3))◃◦ (Ap (N 3))◃◦ (Ap ⟨⟨···⟩⟩ )◃◦ (Ap ⟨⟨···⟩⟩ )◃◦ •◃◦ (Plus(N1))◃•◃◦ (Plus(N1))◃•◃◦ (Plus3)◃•◃◦ (Plus3)◃•◃◦ •◃◦
| •
| •
| •
| •
| •
| x=3,f=⟨⟨···⟩⟩,• | x=3,f =⟨⟨···⟩⟩,• | x=3,f =⟨⟨···⟩⟩,• | x=3,f =⟨⟨···⟩⟩,• | x=3,f =⟨⟨···⟩⟩,• | x=3,f=⟨⟨···⟩⟩,•
≻ (Ap(Fun(f.x.(Plusx(N1))))(N3)) ≻ (Fun (f .x . (Plus x (N 1))))
≺ ⟨⟨f .x. (Plus x (N 1))⟩⟩
≻ (N 3)
≺ 3
≻ (Plusx(N1)) ≻ x
≺ 3
≻ (N1)
≺ 1
≺ 4
Seems
◦|• ≺4
to work for basic examples, but is there some way to break it?
Simple Example
Environments
Closures
Refinement
7
→E →E →E →E →E →E →E →E →E →E →E
Closure Capture
◦ | • ≻ (Ap (Ap (Fun (f .x. (Fun (g.y. x)))) (N 3)) (N 4)) (Ap(N4))◃◦|•≻(Ap(Fun(f.x.(Fun(g.y.x))))(N3)) (Ap(N3))◃(Ap(N4))◃◦|•≻(Fun(f.x.(Fun(g.y.x)))) (Ap(N3))◃(Ap(N4))◃◦|•≺⟨⟨f.x.(Fun(g.y.x))⟩⟩ (Ap⟨⟨f···⟩⟩)◃(Ap(N4))◃◦|•≻(N3) (Ap⟨⟨f···⟩⟩)◃(Ap(N4))◃◦|•≺3 •◃(Ap(N4))◃◦|x=3,f =⟨⟨f···⟩⟩,•≻(Fun(g.y.x)) •◃(Ap(N4))◃◦|x=3,f =⟨⟨f···⟩⟩,•≺⟨⟨g.y.x⟩⟩ (Ap(N4))◃◦|•≺⟨⟨g.y.x⟩⟩
(Ap⟨⟨g.y.x⟩⟩)◃◦|•≻(N4) (Ap⟨⟨g.y.x⟩⟩)◃◦|•≺4 •◃◦|y=4,g=⟨⟨g.y.x⟩⟩,•≻x Oh no! We’re stuck!
Environments Closures Refinement
Something went wrong!
Returning functions as a result means that the function’s body expression escapes the scope of bound variables that existed where it is defined:
(letx=3inrecfunf y=x+y)5
The function value ⟨⟨f .y . x + y ⟩⟩, when it is applied, does not “remember” that x = 3
when the function was defined.
Solution: Store the environment inside the function value!
s |η≻(Recfun(f.x.e)) →E s |η≺⟨⟨η, f.x.e⟩⟩ This type of function value is called a closure.
8
Environments Closures Refinement
(Apply⟨⟨η′,f.x.e⟩⟩)◃s|η≺v →E η◃s|(x=v,f =⟨⟨f.x.e⟩⟩,η′)≻e
9
Store the old env. in the stack
Retrieve the new env. from the closure
Environments Closures Refinement
10
Our Example
◦ | • ≻ (Ap (Ap (Fun (f .x. (Fun (g.y. x)))) (N 3)) (N 4))
(Ap (N 4)) ◃ ◦ | • ≻ (Ap (Fun (f .x. (Fun (g.y. x)))) (N 3))
(Ap (N 3)) ◃ (Ap (N 4)) ◃ ◦ | • ≻ (Fun (f .x. (Fun (g.y. x))))
(Ap (N 3)) ◃ (Ap (N 4)) ◃ ◦ | • ≺ ⟨⟨•, f .x . (Fun (g .y . x ))⟩⟩
(Ap ⟨⟨•, f · · ·⟩⟩ ) ◃ (Ap (N 4)) ◃ ◦ | • ≻ (N 3)
(Ap ⟨⟨•, f · · ·⟩⟩ ) ◃ (Ap (N 4)) ◃ ◦ | • ≺ 3
•◃(Ap(N4))◃◦|x=3,f =⟨⟨f···⟩⟩,•≻(Fun(g.y.x)) •◃(Ap(N4))◃◦|x=3,f =⟨⟨f···⟩⟩,•≺⟨⟨(x=3,f =···,•),g.y.x⟩⟩ (Ap(N4))◃◦|•≺⟨⟨(x=3,f =···,•),g.y.x⟩⟩
(Ap⟨⟨(x=3,f =···,•),g.y.x⟩⟩)◃◦|•≻(N4)
(Ap⟨⟨(x=3,f =···,•),g.y.x⟩⟩)◃◦|•≺4 •◃◦|y=4,g=⟨⟨g.y.x⟩⟩,x=3,f =···,•≻x •◃◦|y=4,g=⟨⟨g.y.x⟩⟩,x=3,f =···,•≺3
◦|•≺3
Environments
Closures Refinement
11
Refinement
We already sketched the proof that shows that each C-machine execution has a corresponding M-machine execution (refinement).
This means that any functional correctness (not security or cost) property we prove about all M-machine executions of a program apply just as well to any C-machine executions of the same program.
Now we want to prove that each E-machine execution has a corresponding C-machine execution (and therefore a M-machine execution).
Environments Closures Refinement
12
Ingredients for Refinement
Once again, we want the same ingredients to prove a simulation proof that we did in the previous refinement. That is, we must define an abstraction function A that converts E-machine states to C-machine states, such that:
Each initial state in the E-machine is mapped to an initial state in the C-Machine. Each final state in the E-machine is mapped to a final state in the C-Machine.
For each transition from one state to another in the E-machine, either there exists a corresponding transition in the C-Machine, or the two states map to the same C-machine state.
Environments
Closures
Refinement
How to define A?
Our abstraction function A applies the environment η as a substitution to the
current expression, and to the stack, starting at the left.
If any environment is encountered in the stack, switch to substituting with that environment instead.
E-Machine values are converted to C-Machine values merely by applying the environment inside closures as a substitution to the expression inside the closure.
With such a function definition, it is trivial to prove that each E-Machine transition has a corresponding transition in the C-Machine, as it is 1:1.
Except!
There is one rule which is not 1:1. Which one?
13