程序代写代做代考 Environments Closures Refinement

Environments Closures Refinement
Environments
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
1

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
5

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
8

Environments Closures Refinement
Simple Example
◦ | • ≻ (Ap(Fun(f.x.(Plusx (N1))))(N3))
10

Environments
Closures Refinement
◦ (Ap 􏰈 (N 3))◃◦
| • | •
Simple Example
≻ (Ap(Fun(f.x.(Plusx (N1))))(N3)) ≻ (Fun (f.x. (Plus x (N 1))))
11

Environments
Closures
Refinement
◦ (Ap 􏰈 (N 3))◃◦ (Ap 􏰈 (N 3))◃◦
| • | • | •
Simple Example
≻ (Ap(Fun(f.x.(Plusx (N1))))(N3)) ≻ (Fun (f.x. (Plus x (N 1))))
≺ ⟨⟨f.x. (Plus x (N 1))⟩⟩
12

Environments
Closures
Refinement
◦ (Ap 􏰈 (N 3))◃◦ (Ap 􏰈 (N 3))◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦
| • | • | • | •
Simple Example
≻ (Ap(Fun(f.x.(Plusx (N1))))(N3)) ≻ (Fun (f.x. (Plus x (N 1))))
≺ ⟨⟨f.x. (Plus x (N 1))⟩⟩
≻ (N 3)
13

Environments
Closures
Refinement
◦ (Ap 􏰈 (N 3))◃◦ (Ap 􏰈 (N 3))◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦
| • | • | • | • | •
Simple Example
≻ (Ap(Fun(f.x.(Plusx(N1))))(N3)) ≻ (Fun (f .x . (Plus x (N 1))))
≺ ⟨⟨f .x. (Plus x (N 1))⟩⟩
≻ (N 3)
≺ 3
14

Environments
Closures
Refinement
◦ (Ap 􏰈 (N 3))◃◦ (Ap 􏰈 (N 3))◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ •◃◦
| • ≻ | • ≻ | • ≺ | • ≻ | • ≺ | 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))
Simple Example
15

Environments
Closures
Refinement
◦ (Ap 􏰈 (N 3))◃◦ (Ap 􏰈 (N 3))◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ •◃◦ (Plus􏰈(N1))◃•◃◦
| • ≻ | • ≻ | • ≺ | • ≻ | • ≺ | 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
Simple Example
16

Environments
Closures
Refinement
◦ (Ap 􏰈 (N 3))◃◦ (Ap 􏰈 (N 3))◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ •◃◦ (Plus􏰈(N1))◃•◃◦ (Plus􏰈(N1))◃•◃◦
| • ≻ | • ≻ | • ≺ | • ≻ | • ≺ | 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
Simple Example
17

Environments
Closures
Refinement
◦ (Ap 􏰈 (N 3))◃◦ (Ap 􏰈 (N 3))◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ (Ap ⟨⟨···⟩⟩ 􏰈)◃◦ •◃◦ (Plus􏰈(N1))◃•◃◦ (Plus􏰈(N1))◃•◃◦ (Plus3􏰈)◃•◃◦
| • ≻ | • ≻ | • ≺ | • ≻ | • ≺ | 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)
Simple Example
18

Environments
Closures
Refinement
◦ (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 =⟨⟨···⟩⟩,•
≻ (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
Simple Example
19

Environments
Closures
Refinement
◦ (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
Simple Example
20

Environments Closures Refinement
Closure Capture
◦ | • ≻ (Ap (Ap (Fun (f .x. (Fun (g.y. x)))) (N 3)) (N 4))
23

Environments Closures Refinement
Closure Capture
◦ | • ≻ (Ap (Ap (Fun (f .x. (Fun (g.y. x)))) (N 3)) (N 4)) 􏰀→E (Ap 􏰈 (N 4)) ◃ ◦ | • ≻ (Ap (Fun (f .x. (Fun (g.y. x)))) (N 3))
24

Environments
Closures
Refinement
􏰀→E 􏰀→E
Closure Capture
◦ | • ≻ (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))))
25

Environments
Closures
Refinement
Closure Capture
◦ | • ≻ (Ap (Ap (Fun (f .x. (Fun (g.y. x)))) (N 3)) (N 4))
􏰀→E (Ap􏰈(N4))◃◦|•≻(Ap(Fun(f.x.(Fun(g.y.x))))(N3)) 􏰀→E (Ap􏰈(N3))◃(Ap􏰈(N4))◃◦|•≻(Fun(f.x.(Fun(g.y.x)))) 􏰀→E (Ap􏰈(N3))◃(Ap􏰈(N4))◃◦|•≺⟨⟨f.x.(Fun(g.y.x))⟩⟩
􏰀→E (Ap⟨⟨f···⟩⟩􏰈)◃(Ap􏰈(N4))◃◦|•≻(N3)
􏰀→E (Ap⟨⟨f···⟩⟩􏰈)◃(Ap􏰈(N4))◃◦|•≺3
􏰀→E •◃(Ap􏰈(N4))◃◦|x=3,f =⟨⟨f···⟩⟩,•≻(Fun(g.y.x))
􏰀→E •◃(Ap􏰈(N4))◃◦|x=3,f =⟨⟨f···⟩⟩,•≺⟨⟨g.y.x⟩⟩
30

Environments
Closures
Refinement
􏰀→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!
34

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.
35

Environments Closures Refinement
(Apply⟨⟨η′,f.x.e⟩⟩􏰈)◃s|η≺v 􏰀→E η◃s|(x=v,f =⟨⟨f.x.e⟩⟩,η′)≻e

Environments Closures Refinement
(Apply⟨⟨η′,f.x.e⟩⟩􏰈)◃s|η≺v 􏰀→E η◃s|(x=v,f =⟨⟨f.x.e⟩⟩,η′)≻e
Store the old env. in the stack

Environments Closures Refinement
(Apply⟨⟨η′,f.x.e⟩⟩􏰈)◃s|η≺v 􏰀→E η◃s|(x=v,f =⟨⟨f.x.e⟩⟩,η′)≻e
Store the old env. in the stack
Retrieve the new env. from the closure
38

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􏰈(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
43

Environments Closures Refinement
46
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
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).
47

Environments Closures Refinement
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.
48

Environments Closures Refinement
How to define A?
49

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.
50

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?
53

Related Posts