Code and Notes (Week 5 Thursday)
(x=3,y=3,x=5,●)(x) = 3
(x=3,y=3,x=5,●)(y) = 3
Copyright By PowCoder代写 加微信 powcoder
(x=3,y=3,x=5,●)(z) = undefined
The reason we get the leftmost is that the bindings to right
are shadowed by the leftmost binding.
○ | x=3,y=3,x=5,● ≻ Plus (Var x) (Var y)
↦E Plus □ (Var y) ▷ ○ | x=3,y=3,x=5,● ≻ Var x
↦E Plus □ (Var y) ▷ ○ | x=3,y=3,x=5,● ≺ 3
↦E Plus 3 □ ▷ ○ | x=3,y=3,x=5,● ≻ Var y
↦E Plus 3 □ ▷ ○ | x=3,y=3,x=5,● ≺ 3
↦E ○ | x=3,y=3,x=5,● ≺ 6
Q: Do we need to put the Var constructur explicitly in the rule?
A: We probably should have, but there’s going to enough syntactic noise
anyway later on, so we’ll just leave it implicit most of the time.
With broken attempt 1:
(λx. x) 2 =
(recfun f (Int -> Int) x = x) (f 2)
○ | ● ≻ (recfun f (Int -> Int) x = x) (Num 2)
↦E Apply □ (Num 2), ○ | ● ≻ (recfun f (Int -> Int) x = x)
↦E Apply □ (Num 2), ○ | ● ≺ <
↦E Apply <
↦E Apply <
↦E ○ | x=2, f=<
↦E ○ | x=2, f=<
Done! Final state:
○ | x=2, f=<
..but what we *really* want is:
What does this mean? It means that local bindings for f and x persist
in the environment *after* we leave their scope! This creates all
sorts of problems.
Consider this expression:
((λx. x) 2) + x
This should evaluate to 2 + <
behind after the call to (λx. x) the above expression will always
evaluate to 4! Because the x from within (λx. x) escaped its scope.
The same expression works exactly as expected under the second
attempted semantics.
(λx. x + 1) 3
In slide “simple example”, we’ve abbreviated the constructor names to
save space.
In particular:
Ap is short for Apply
N is short for Num
Closure capture slides is about this program (in λ-notation)
((λx. λy. x) 3) 4
what *should* we return?
((λx. λy. x) 3) 4 ↦β (λy. 3) 4 ↦β 3
Refinement
We say that the concrete thing C is a refinement of the abstract thing
— every possible behaviour of C is also a possible behaviour of A.
We can think of A as
— a specification, and then C is an implementation
— a source-level program, then C is the compiler output.
Q: What’s a behaviour exactly?
A: Wait until later in the course, or take COMP3151 (foundations of
concurrency) or COMP2111 (somethingsomething systems modelling)
What the ingredients prove together is the following:
For all complete E-machine executions
○ | ● ≻ e ↦E* ○ | ● ≺ v
There exists a C-machine execution with the same final result:
○ | ● ≻ e ↦C* ○ | ● ≺ v
Let’s have a language L of arithmetic expression with only Plus and
L ::= Num ℤ | Plus L L
Then two machines for this language
— M-machine:
__________________________
Plus e1 e2 ↦M Plus e1′ e2
_________________________________
Plus (Num n) e ↦M Plus (Num n) e
_________________________________
Plus (Num n) (Num m) ↦M Num(n+m)
— C-machine
______________________________________
s ≻ Plus e1 e2 ↦C Plus □ e2 ▷ s ≻ e1
___________________________________________
Plus □ e2 ▷ s ≺ v ↦C Plus v □ ▷ s ≻ e2
____________________________________
Plus v □ ▷ s ≺ v’ ↦C s ≻ v + v’
_________________
s ≻ Num n ↦C s ≺ n
— Refinement
What do we do if we want to show refinement?
(1) Make an abstraction function
For example, the state
Plus □ (Num 3) ▷ ○ ≻ (Num 2)
that corresponds to the M-machine state (aka expression) Plus (Num 2)
A’ :: stack -> expr -> expr
A’ ○ e = e
A’ (Plus □ e1 ▷ s) e2 = A’ s (Plus e1 e2)
A’ (Plus v □ ▷ s) e2 = A’ s (Plus (Num v) e2)
A :: state -> expr
A (s ≺ v) = A’ s (Num v)
A (s ≻ e) = A’ s e
(2) Each initial C-machine state maps to an initial M-machine
state. (Trivial, because all M-machine states are initial)
(3) Each final C-machine state maps to a final M-machine states (aka a Num v)
Suppose we have a final C-machine state:
A(○ ≺ v) = A’ ○ (Num v) = Num v …which is final, QED.
(4) Suppose we have a C-machine transition
st ↦C st’
show that *either*
A(st) = A(st’)
A(st) ↦C A(st’)
You would prove this by induction.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com