代写代考 COMP3151 (foundations of

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 <> □, ○ | ● ≻ (Num 2)
↦E Apply <> □, ○ | ● ≺ 2
↦E ○ | x=2, f=<>,● ≻ x
↦E ○ | x=2, f=<>,● ≺ 2

Done! Final state:

○ | x=2, f=<>,● ≺ 2

..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 + <> However, because our local binding for x gets left
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