COMP3161/COMP9164
Abstract Machines Exercises
Liam O’ 20, 2019
1. Decision Machines: Suppose we have a language of nested brackets N (where ε is the empty string): N eNN eNN eNN
εN 1 (e)N 2 ⟨e⟩N 3 [e]N 4 Note that ()() is not a string in this language.
We developed a simple abstract machine to check if strings are in this language. We set the states for the machine to be simply strings. Initial states are all non-empty strings, and the final state is the empty string. Then, our state transition relation is:
(e) → eM1 [e] → eM2 ⟨e⟩ → eM3
(a) A machine recognises a language if any machine in the state corresponding to a string S will eventually reach a final state if and only if the string S is in the language.
i. [⋆] Show that the string ([⟨⟩]) is in the language N, and show that our machine reaches a final state given the same string.
Solution: The string is in the language, as shown: ε N N1
[⟨⟩] N ([⟨⟩]) N
The machine derivation is simply: ([⟨⟩])
→ [⟨⟩] (M1) → ⟨⟩ (M2) → ε (M3)
ii. [⋆⋆] Show that the string []()[] is not in the language N, and show that our machine reaches a
non-final state with no outgoing transitions given the same string, i.e, there exists some stuck state
s such that []()[] → s
Solution: If we attempt to derive []()[] N :
We get the subgoal ]()[ N, which is false, as all strings in N are either ε or begin with an opening bracket. Hence, as the rules are unambiguous, there is no other way to derive []()[] N and hence it is not in N. Similarly, our machine derivation:
→ ]()[ (M2)
We end up in the state ]()[, which is a stuck state, as there are no transitions from a state that begins with a closing bracket.
iii. Prove that the machine recognises the language N, that is: ⋆⋆
α) [⋆⋆⋆] s N =⇒ s → ε. The relation → of course being the reflexive transitive closure of →,
s1 →s2 s2 →s3 Refl* ⋆
β) [⋆⋆⋆] s→ε =⇒ sN
Base case: Where s = ε, we must show ε → ε. We can show this using the reflexivity rule:
ε → ε ′′′⋆
Inductive cases: Where s = (s ) and s N, with the inductive hypothesis that s → ε, we ′′⋆
must show that, if (s ) N , then (s ) → ε. We simply derive our goal as follows:
(s′) → s′ M1 ′ ⋆ I.H s →ε
′⋆ (s ) → ε
The other inductive cases are extremely similar.
Proof. Here we use induction over the number of steps in the machine’s execution, which ⋆
is the same as induction over the definition of →.
Base case: Where the length of the execution is zero – i.e, we are already in a final state. The only final state is ε, and hence our proof goal is just ε N, which is already known from rule N1.
′′′⋆ Inductive case: Where our state s executes in one step to s (s → s ), and s → ε (∗).
From (∗) we have the inductive hypothesis s′ N . We must show that s N . We proceed by case distinction on s. Seeing as s → s′, s must be one of (s′) (by rule M1), [s′] (by rule M2), or ⟨s′⟩ (by rule M3). All three cases are nearly identical, so we will deal with just the first case, where s = (s′).
s′ N I.H (s′) N N2
(b) Suppose that we were unable to efficiently read from both the beginning and end of the string simul- taneously (For example, if a tape or a linked list is used to represent the string). This makes our original machine highly inefficient, as each state transition must examine the end of a string for a closing bracket.
We develop a new, stack-based machine that attempts to solve this problem. Our stack consists of three symbols, P,A, and B, one for each type of bracket. The states of the machine are of the form s | e, where s is a stack and e is a string. Our initial states are all states with an empty stack and a non-empty string, i.e: ◦ | e, our final state is ◦ | ε, and our state transitions are as follows:
s | (e → P ◃ s | e S1 s | ⟨e → A ◃ s | e S2 s | [e → B ◃ s | e S3 P ◃ s | )e → s | e S4 A ◃ s | ⟩e → s | e S5 B ◃ s | ]e → s | e S6
i. [⋆] Show the execution of the new stack machine given the start state ◦ | [(⟨⟩)].
Solution: The machine execution proceeds as follows: ◦ | [(⟨⟩)]
→ B◃◦|(⟨⟩)]
→ P◃B◃◦|⟨⟩)]
→ A◃P◃B◃◦|⟩)]
→ P◃B◃◦|)]
(S3 ) (S1) (S2) (S5 ) (S4 ) (S6 )
ii. Does the new machine recognise N?
α) [⋆⋆⋆⋆] Prove or disprove that s N =⇒ ◦|s → ◦|ε for all strings s. Hint: You may find it
useful to prove the following lemma:
Also, you may need to generalise your proof goal to a broader claim.
Proof of Lemma. We will prove the lemma provided above first, as it will come in handy. ⋆
We proceed by induction on the size of the execution s1 → s2, and must show that, given s2 → s3 (†), that s1 → s3.
0⋆ Base case: s1 → s2, i.e s1 = s2. We must therefore show that s2 → s3:
s →s (†) ⋆ Refl*
s3 → s3 ⋆
Inductive case: When s1 → s1 (∗), and s1 → s2 (∗∗), and we have the inductive hypothesis
from (∗∗) that:
s1 → s3 Then, we simply derive the proof goal:
s2 → s3 ′′⋆
s2 → s3 I.H ′⋆
s →s (†) (∗) 2 3 I.H
s →s′ ′ ⋆
1 1 s1 → s3 Trans*
Proof of main theorem. Now that we have proven the lemma, we must now prove that ⋆
s N =⇒ ◦ | s → ◦ | ε. We will generalise this proof goal to make the stronger claim that ⋆
s N =⇒ t | sr → t | r for any stack t and remainder string r. Note that this trivially
implies our original proof goal by setting t to ◦ and r to ε.
Base case: Where s = ε, we must therefore show that t | r → t | r, trivially shown by rule
Inductive case: s = (s′), where s′ N(∗). From (∗), we have the inductive hypothesis:
′′′⋆′′′′ ′⋆
t |sr →t |r,foranyt andr. Wemustshowthatt|(s)r→t|rforallt,r.
t | (s′)r → P ◃ t | s′)r S1
⋆ I.H1 S4 P ◃ t | s′)r → P ◃ t | )r P ◃ t | )r → t | r
P ◃ t | s )r → t | r
t | (s )r → t | r
The other inductive cases are extremely similar.
1: The application of the I.H rule here sets t′ to be P◃t and r′ to be )r.
β) [⋆⋆] Prove or disprove that ◦ | s → ◦ | ε =⇒ s N
Counterexample. We will disprove this by way of a counterexample. It is already estab- ⋆
lished that ()() is not in N. We will show that ◦|()() → ◦|ε and thus there is no way ⋆
that ◦ | s → ◦ | ε could imply s N . The machine execution is as follows:
→ P◃◦|)() (S1) → ◦|() (S4) → P◃◦|) (S1) → ◦|ε (S4)
iii. [⋆⋆] If your answer to the previous question was no, amend the structure of the stack machine so that it does recognise N (efficiently). Explain your answer.
Solution: The problem with the existing machine is that it recognises any amount of strings in N placed next to each other. A string in N consists of a sequence of opening brackets, followed by a sequence of closing brackets. Once a closing bracket has been observed by the machine, it should not see any opening brackets. To fix this, we modify the state such that there are two modes, pushing ( ≻ ), and popping ( ≺ ). The machine starts in pushing mode, i.e: ◦ ≻ s for some string s, and now we have two terminating states: ◦ ≻ ε and ◦ ≺ ε. Our transition rules are updated as follows:
s ≻ (e→P◃s ≻ e P◃s ≻ )e→P◃s ≺ )e
P◃s ≺ )e→s ≺ e
s ≻ ⟨e→A◃s ≻ e A◃s ≻⟩e→A◃s ≺⟩e
A◃s ≺⟩e→s ≺ e
s ≻ [e→B◃s ≻ e
B◃s ≻ ]e→B◃s ≺ ]e
B◃s ≺ ]e→s ≺ e
As there are no rules to go from popping to pushing mode, the machine cannot push a symbol after one has been popped, and hence the machine recognises N.
2. Computing Machines: Abstract machines are not just used for decision problems (yes/no answers), they can also be used to compute results. Can you think of a machine to compute binary addition?
(a) [⋆⋆⋆] Formalise such a machine.
Hint: Think about the algorithm you would use when adding up large binary numbers on paper.
Solution: The machine’s states are of the form:
Where s, n1 and n2 are strings of binary digits, and c is a single carry bit. n1 and n2 are also padded with zeros so as to be the same length.
Initial states are all states where s is empty and the carry bit is zero:
Final states are all states where n1 and n2 are empty and the carry bit is zero:
The transition rules work as follows:
n10 n1 B1 n10 n1 B2 n0 s⟨⟨0⟩⟩→n 0s⟨⟨0⟩⟩ n1 s⟨⟨0⟩⟩→n 1s⟨⟨0⟩⟩
n11 n1 B3 n11 n1 B4 n0 s⟨⟨0⟩⟩→n 1s⟨⟨0⟩⟩ n1 s⟨⟨0⟩⟩→n 0s⟨⟨1⟩⟩
n10 n1 B1c n10 n1 B2c n0 s⟨⟨1⟩⟩→n 1s⟨⟨0⟩⟩ n1 s⟨⟨1⟩⟩→n 0s⟨⟨1⟩⟩
n11 n1 B3c n11 n1 B4c n0 s⟨⟨1⟩⟩→n 0s⟨⟨1⟩⟩ n1 s⟨⟨1⟩⟩→n 1s⟨⟨1⟩⟩
ε ε Boverflow ε s ⟨⟨1⟩⟩ → ε 1s ⟨⟨0⟩⟩
(b) [⋆] Compute the result 110 + 1010 with your machine. Show each execution step.
The result is 10000, as shown below:
→ 10 00⟨⟨1⟩⟩ (B4) 0
→ 1 000 ⟨⟨1⟩⟩ (B3c) ε
→ ε 0000 ⟨⟨1⟩⟩ (B2c)
→ ε 10000 ⟨⟨0⟩⟩ (Boverflow)
0110 1010
→ 101 0⟨⟨0⟩⟩ (B1)
3. Evaluation Machines: Because machines can express computation, we can also use them to express the operational semantics of a programming language. Imagine an extremely simple functional language with the following big-step semantics:
lam(x, y) ⇓ ⟨⟨x.y⟩⟩
Lambda e1 ⇓ ⟨⟨x.y⟩⟩ e2 ⇓ e′2 y[x := e′2] ⇓ rApply apply(e1, e2) ⇓ r
(a) [⋆⋆] Develop a structural operational (“small step”) semantics for this language.
i. Include three rules for function application. Assume the function expression is evaluated before
the argument expression. Note that this language does not include explicit recursion.
(b) Now define an abstract machine which eliminates recursion from the meta-level of the semantics to include an explicit stack, a la the C Machine.
i. [⋆] Define a suitable stack formalism.
t1 → t′1 Apply t2 → t′2 Apply apply(t1, t2) → apply(t′1, t2) 1 apply(lam(x.y), t2) → apply(lam(x.y), t′2)
apply(lam(x.y), lam(a.b)) → y[x := lam(a.b)] Apply3
x Frame s Stack ◦ Stack x ◃ s Stack
Where a F rame is simply either apply(, x) or apply(x, ) for some x.
ii. [⋆⋆] Define the set of states Σ, the set of initial states I ⊆ Σ, and the set of final states F ⊆ Σ.
Solution: The set of states consists of an expression, and a stack: s Stack e Expr
s|e∈Σ Initial states are an expression with an empty stack:
e Expr ◦|e∈I
Final states are a function with an empty stack
◦ | lam(x.e) ∈ F
iii. [⋆⋆] Include three rules for function application, using capture-avoiding substitution as a built-in machine operation.
(c) Now suppose that we want to eliminate substitution from our machine. Extend the semantics to include environments, a la the E Machine. Recall than an environment is commonly defined as:
x Ident y Expr Γ Env • Env x ← y; Γ Env
i. [⋆⋆] Revise your definition of the state sets Σ, I and F , and of the stack.
ii. [⋆⋆⋆] Add a transition rule for function literals. Note that these function literals should produce closures which capture the environment at their definition.
iii. [⋆⋆⋆] Revise your rules for function application.
s | apply(e1, e2) → apply(, e2) ◃ s | e1 apply(, e2) ◃ s | lam(x.y) → apply(lam(x.y), ) ◃ s | e2 apply(lam(x.y), ) ◃ s | lam(a.b) → s | y[x := lam(a.b)]
Solution: Our stack can now also include environments: s Stack Γ Env
Γ ◃ s Stack
Our state now also includes a current environment, of the form s | Γ | e, where s is a Stack, Γ is an environment and e is an expression.
I and F are unchanged except that they include the empty environment.
s | Γ | lam(x, y) → s | Γ | ⟨⟨Γ, x.y⟩⟩
s | apply(e1, e2) → apply(, e2) ◃ s | e1
apply(, e2) ◃ s | Γ | ⟨⟨∆, x.y⟩⟩ → apply(⟨⟨∆, x.y⟩⟩, ) ◃ s | ∆ | e2 apply(⟨⟨Γ, x.y⟩⟩, ) ◃ s | ∆ | ⟨⟨E, a.b⟩⟩ → ∆ ◃ s | x ← ⟨⟨E, a.b⟩⟩; Γ | y
iv. [⋆⋆⋆] Include any additional rules necessary to complete the definition, such as variable lookup.
Solution: Variable Lookup:
s | x ← y; Γ | x → s | x ← y; Γ | y
Popping environments from the stack, back into the current environment:
Γ ◃ s | ∆ | ⟨⟨E, x.y⟩⟩ → s | Γ | ⟨⟨E, x.y⟩⟩
v. [⋆⋆] Give an example of an expression in this language which requires closures in order to evaluate correctly. Explain your answer.
Solution: A simple example is:
apply(apply(lam(x, lam(y, apply(x, y))), lam(a, a)), lam(b, b))
Evaluating the outer application will cause the inner application to be evaluated first, where x is bound to ⟨⟨a.a⟩⟩. Without closures, the inner application will return the function ⟨⟨y.apply(x,y)⟩⟩ back beyond the stack frame where x is in scope resulting in a free variable inside the function. When the outer application is finally evaluated, one would end up encoun- tering x free in the program, and be in a stuck state. With closures, however, the environment containing the binding for x is captured in the returned function and x will not be found free.
4. Stack Machines: In this question, we will examine a machine that is quite similar to a type of machine used in virtual machines, such as the JVM, called a stack machine. Imagine an arithmetic expression language with the following big step semantics:
x ∈ Z x ⇓ x′ y ⇓ y′ x ⇓ x′ y ⇓ y′ num(x)⇓xNum plus(x,y)⇓x′ +y′Plus times(x,y)⇓x′ ×y′Times
We have a machine, called the J Machine, that’s capable of performing these operations, however it works by using a stack to store operands and accumulate results. For example, 4 * (2 + 3) would be the following program in the J Machine’s bytecode: val(4); val(2); val(3); add; times. Each val instruction pushes a value to the stack, and each operation instruction pops two values off, and pushes the result of the operation.
Formally, the J Machine is specified as follows: The machine consists of three instructions: x∈Z
val(x) Inst plus Inst times Inst
The state of the machine consists of a list of instructions, called a Program, and a stack of integers:
i Inst p Program halt Program i; p Program
x∈Z sStack ◦ Stack x ◃ s Stack
They are presented in the form s | p where s is a stack and p is program. The initial state consists of the empty stack and any nonempty program p i.e, ◦ | p. The final state consists of a stack with merely one element r (the result of the computation), and the empty program, i.e, r ◃ ◦ | halt.
The state transition rules are as follows:
s | val(x); p → x ◃ s | p J1 y ◃ x ◃ s | add; p → x + y ◃ s | p J2 y ◃ x ◃ s | times; p → x × y ◃ s | p J3
(a) [⋆⋆] Translate the expression plus(times(num(-1), num(7)), num(7)) into a J Machine program, and
write down each step the J Machine would take to execute this program.
Solution: The program is: val(-1); val(7); times; val(7); plus; halt.
Execution is as follows:
◦ | val(-1); val(7); times; val(7); plus; halt
→ -1 ◃ ◦ | val(7); times; val(7); plus; halt
→ 7 ◃ -1 ◃ ◦ | times; val(7); plus; halt
→ -7 ◃ ◦ | val(7); plus; halt
→ 7◃-7◃◦|plus;halt
→ 0◃◦|halt
(J1 ) (J1 ) (J3 ) (J1 ) (J2 )
(b) [⋆⋆⋆] Formalise (using inference rules) a “compilation” relation ⊆ Expr×Program which translates expressions in the arithmetic language to the semantically equivalent J Machine bytecode. You may assume that the semicolon operator in J Machine code is associative.
(c) [⋆⋆⋆⋆] Suppose we wanted to add a let construct to add variables to our arithmetic language, using environments as shown:
num(n) val(n); halt NumJ
n n′;halt m m′;halt Plus n n′;halt m m′;halt Times plus(n, m) n′; m′; plus; halt J times(n, m) n′; m′; times; halt J
x ∈ Z Γ⊢num(x)⇓xNum
Γ ⊢ x ⇓ x′ Γ ⊢ y ⇓ y′ Γ⊢plus(x,y)⇓x′ +y′Plus
Γ ⊢ x ⇓ x′ Γ ⊢ y ⇓ y′ Γ⊢times(x,y)⇓x′ ×y′Times
x←v∈Γ Γ⊢var(x)⇓vVar
Γ∪{x←v1}⊢e2 ⇓v2 122
Γ⊢let(x,e ,e )⇓v Let
Extend the J Machine to support this construct, and expand your relation to include the correct translation. Don’t forget to deal with name shadowing by exploiting stacks.
Solution: We extend the state definition of the states in the machine to include an additional stack of environments, called scopes, notated as z | s | p, where z is the integer stack and s is the scope stack. The initial states now look like this:
That is, they start with the empty environment sitting at the bottom of the scope stack. Similarly, final states also have the empty environment only on their scope stack.
We introduce three new instructions, scope, descope, and var, which have the following semantics: scope(x) pushes a new environment to the scope stack. The new environment is the same as the old environment except it includes a new binding1 from the name x to the value on the top of the value stack. The value stack is also popped.
descope(x) simply pops the scope stack. var(x) pushes the value of a variable to the value stack. The value is determined by looking in the topmost scope environment.
v ◃ s | Γ ◃ ζ | scope(x); p → s | Γ ∪ {x ← v} ◃ ζ | p J4 s | Γ ◃ ζ | descope; p → s | ζ | p J5 s | {x ← v} ∪ Γ ◃ ζ | var(x); p → v ◃ s | {x ← v} ∪ Γ ◃ ζ | p J6
1: Because each environment is a superset of the last, pointer magic could be used here to make this efficient in practice.
As for the compilation relation, we translate let as follows:
e1 e′1; halt e2 e′2; halt LetJ let(x, e1, e2) e′1; scope(x); e′2; descope; halt
And, for variable lookup, it’s quite simple:
var(x) var(x)VarJ
Note: This is basically how the JVM bytecode works (modulo some OO features).