Environments
Environments Closures Refinement
Copyright By PowCoder代写 加微信 powcoder
Environments
Johannes Åman Pohjola
Term 3 2021
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 7→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
Environments Closures Refinement
Environments
Definition
An environment is a context containing the values of variables.
It is like the states of TinyImp, except the value of a variable never changes.
x = v , η Env
η(x) denotes the leftmost value bound to to x in η.
Let’s change our machine states to include an environment:
s | η � e s | η ≺ v
Environments Closures Refinement
First Attempt
First, we’ll add a rule for consulting the environment if we encounter a free variable:
s | η � x 7→E s | η ≺ η(x)
Then, we just need to handle function application.
One broken attempt:
(Apply 〈〈f .x . e〉〉 �) . s | η ≺ v 7→E s | (x = v , f = 〈〈f .x . e〉〉, η) � e
We don’t know when to remove the variables again!
Environments Closures Refinement
Second Attempt
We will extend our stacks to allow us to save the old environment to it.
η Env s Stack
η . s Stack
When we call a function, we save the environment to the stack.
(Apply 〈〈f .x . e〉〉 �) . s | η ≺ v 7→E η . s | (x = v , f = 〈〈f .x . e〉〉, η) � e
When the function returns, we restore the old environment, clearing out the new
η . s | η′ ≺ v 7→E s | η ≺ v
This attempt is also broken (we’ll see why soon)
Environments Closures Refinement
Simple Example
◦ | • � (Ap (Fun (f .x . (Plus x (N 1)))) (N 3))
(Ap � (N 3)) . ◦ | • � (Fun (f .x . (Plus x (N 1))))
(Ap � (N 3)) . ◦ | • ≺ 〈〈f .x . (Plus x (N 1))〉〉
(Ap 〈〈· · ·〉〉 �) . ◦ | • � (N 3)
(Ap 〈〈· · ·〉〉 �) . ◦ | • ≺ 3
• . ◦ | x = 3, f = 〈〈· · ·〉〉, • � (Plus x (N 1))
(Plus � (N 1)) . • . ◦ | x = 3, f = 〈〈· · ·〉〉, • � x
(Plus � (N 1)) . • . ◦ | x = 3, f = 〈〈· · ·〉〉, • ≺ 3
(Plus 3 �) . • . ◦ | x = 3, f = 〈〈· · ·〉〉, • � (N 1)
(Plus 3 �) . • . ◦ | x = 3, f = 〈〈· · ·〉〉, • ≺ 1
• . ◦ | x = 3, f = 〈〈· · ·〉〉, • ≺ 4
to work for basic examples, but is there some way to break it?
Environments Closures Refinement
Closure Capture
◦ | • � (Ap (Ap (Fun (f .x . (Fun (g .y . x)))) (N 3)) (N 4))
7→E (Ap � (N 4)) . ◦ | • � (Ap (Fun (f .x . (Fun (g .y . x)))) (N 3))
7→E (Ap � (N 3)) . (Ap � (N 4)) . ◦ | • � (Fun (f .x . (Fun (g .y . x))))
7→E (Ap � (N 3)) . (Ap � (N 4)) . ◦ | • ≺ 〈〈f .x . (Fun (g .y . x))〉〉
7→E (Ap 〈〈f · · ·〉〉 �) . (Ap � (N 4)) . ◦ | • � (N 3)
7→E (Ap 〈〈f · · ·〉〉 �) . (Ap � (N 4)) . ◦ | • ≺ 3
7→E • . (Ap � (N 4)) . ◦ | x = 3, f = 〈〈f · · ·〉〉, • � (Fun (g .y . x))
7→E • . (Ap � (N 4)) . ◦ | x = 3, f = 〈〈f · · ·〉〉, • ≺ 〈〈g .y . x〉〉
7→E (Ap � (N 4)) . ◦ | • ≺ 〈〈g .y . x〉〉
7→E (Ap 〈〈g .y . x〉〉 �) . ◦ | • � (N 4)
7→E (Ap 〈〈g .y . x〉〉 �) . ◦ | • ≺ 4
7→E • . ◦ | y = 4, g = 〈〈g .y . x〉〉, • � x
Oh no! We’re stuck!7
Environments Closures Refinement
Something went wrong!
When we return functions, the function’s body escapes the scope of bound variables
from where it as defined:
(let x = 3 in recfun f y = x + y) 5
The function value 〈〈f .y . x + y〉〉, when it is applied, does not “remember” that x = 3.
Solution: Store the environment inside the function value!
s | η � (Recfun (f .x . e)) 7→E s | η ≺ 〈〈η, f .x . e〉〉
This type of function value is called a closure.
Environments Closures Refinement
(Apply 〈〈η′, f .x . e〉〉 �) . s | η ≺ v 7→E η . s | (x = v , f = 〈〈f .x . e〉〉, η′) � e
old env. in
Retrieve the new
env. from the closure
Environments Closures Refinement
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 � (N 4)) . ◦ | x = 3, f = 〈〈f · · ·〉〉, • � (Fun (g .y . x))
• . (Ap � (N 4)) . ◦ | x = 3, f = 〈〈f · · ·〉〉, • ≺ 〈〈(x = 3, f = · · · , •), g .y . x〉〉
(Ap � (N 4)) . ◦ | • ≺ 〈〈(x = 3, f = · · · , •), g .y . x〉〉
(Ap 〈〈(x = 3, f = · · · , •), g .y . x〉〉 �) . ◦ | • � (N 4)
(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
◦ | • ≺ 310
Environments Closures Refinement
Refinement
We already sketched a proof that each C-machine execution has a corresponding
M-machine execution (refinement).
This means 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 an M-machine execution).
Environments Closures Refinement
Ingredients for Refinement
Once again, we want 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 E-machine transition, either there is a corresponding C-Machine
transition, or the two E-machine 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.
There is one rule which is not 1:1. Which one?
Environments
Refinement
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com