COMP3161/COMP9164
Abstract Machines Exercises
Liam O’Connor October 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.
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
iii. Prove that the machine recognises the language N, that is: ⋆⋆
α) [⋆⋆⋆] s N =⇒ s → ε. The relation → of course being the reflexive transitive closure of →,
that is:
⋆
β) [⋆⋆⋆] s→ε =⇒ sN
⋆
⋆
s1 →s2 s2 →s3 Refl* ⋆
s1 → s3
Trans*
s → s
(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 ◦ | [(⟨⟩)]. ii. Does the new machine recognise N?
1
α)
β) iii. [⋆⋆]
⋆
[⋆⋆⋆⋆] Prove or disprove that s N =⇒ ◦|s → ◦|ε for all strings s. Hint: You may find it useful to prove the following lemma:
⋆
s2 →s3
Also, you may need to generalise your proof goal to a broader claim.
⋆
[⋆⋆] Prove or disprove that ◦ | s → ◦ | ε =⇒ s N
If your answer to the previous question was no, amend the structure of the stack machine so
s1 →s2
s1 → s3
Lemma
that it does recognise N (efficiently). Explain your answer.
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.
(b) [⋆] Compute the result 110 + 1010 with your machine. Show each execution step.
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.
ii. [⋆⋆] Define the set of states Σ, the set of initial states I ⊆ Σ, and the set of final states 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.
iv. [⋆⋆⋆] Include any additional rules necessary to complete the definition, such as variable lookup.
v. [⋆⋆] Give an example of an expression in this language which requires closures in order to evaluate correctly. Explain your answer.
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.
Page 2
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.
(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:
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
Γ⊢e1 ⇓v1
Γ⊢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.
Page 3