COMP3161/COMP9164
Semantics Exercises
Liam O’Connor September 29, 2019
1. [⋆⋆] Jankenbon:
Below is a language specified to compute the results of rock paper scissors tournaments:
L ::= | | | (Play L L) CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
We assume the existence of an operation match which computes the result of an individual game. match( , )=
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
match( , )= CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
Here are some small step semantics to compute the tournament result:
e 1 → e ′1
(Play e1 e2) → (Play e′1 e2)
v1∈{,,} e2→e′2 CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
(Play v1 e2) → (Play v1 e′2) v1∈{ , , } v2∈{ , , }
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
(Play v1 v2) → match(v1, v2)
Determine a suitable big-step equivalent semantics for this language.
2. Logical Formulae: Imagine we have a simple propositional expression language1:
x Prop y Prop x Prop ⊤ Prop ⊥ Prop x ∧ y Prop ¬x Prop
(a) Here are the big-step evaluation semantics for this language:
⊤ ⇓ TrueTrue ⊥ ⇓ FalseFalse
x⇓True x⇓False x⇓False x⇓True y⇓v
¬x ⇓ False Not1 ¬x ⇓ True Not2 x ∧ y ⇓ False And1 x ∧ y ⇓ v And2
Determine a small step (SOS) semantics for the language Prop.
i. [⋆] Identify the set of states Σ, the set of initial states I, and the set of final states F.
ii. [⋆⋆] Provide inference rules for a relation → ⊆ Σ×Σ, which performs one step only of the expression evaluation.
1Yes, the grammar is ambiguous, but assume it’s just a symbolic representation of abstract syntax. 1
⋆
(b) We shall now prove that the reflexive, transitive closure of →, →, is implied by the big-step semantics ⋆
⋆
Refl∗ x → y y → zTrans∗ ⋆⋆
Transitive
ii. [⋆⋆] Now prove the following two lemmas about Not: ⋆⋆
above. → is defined by the following rules:
x → x x → z i. [⋆⋆] First prove the following transitivity lemma:
⋆⋆
p→q q→r ⋆
x → ⊤ ⋆
Lemma-Not1
x → ⊥
⋆ Lemma-Not2
¬x → ⊤
p → r
¬x → ⊥
iii. [⋆⋆] Now prove the following lemmas about And: ⋆⋆
x → ⊥ ⋆
Lemma-And1
x → ⊤
⋆ Lemma-And2
x ∧ y → ⊥
iv. [⋆⋆⋆] Using these lemmas or otherwise, show that E ⇓ V implies σE → σV , where σE is the state
⋆
corresponding to the expression E and σV is the final state corresponding to the value V .
(c) Now we will prove the other direction of the equivalence.
i. [⋆⋆⋆⋆] Prove the following lemma by rule induction on the small-step premise:
e → e′ e′ ⇓ v e⇓v
Hint: It might help to keep v arbitrary in the induction, and thus prove for each case: ∀v. e′ ⇓v
e⇓v
ii. [⋆] Now prove that every completed small step trace has a correspoding big step evaluation:
⋆
e → σv
e⇓v
(d) [⋆⋆] Suppose we wanted to add quantifiers and variables to our logic language:
x Prop x Prop v is a variable name ∃v. x Prop ∀v. x Prop v Prop
Write a static semantics judgement for this language, written ⊢ e Ok (with whatever context you like before the ⊢), that ensures that there are no free variables in a given logical formula. Remember that a free variable is a variable that is not bound by a quantifier or lambda.
3. Bizarro-Poland: Imagine we have a reverse Polish notation calculator language. Reverse Polish notation is an old calculator format that does not require the use of parenthetical expressions. To achieve this, it moves all operators to post-fix, rather than in-fix order. E.g 1 + 2 becomes 1 2 +, or 1 − (3 + 2) becomes 1 3 2 + −. These calculators evaluated these expressions by pushing symbols onto a stack until an operator was encountered, when two symbols would be popped off and the result of the operation pushed on. The grammar is easily defined:
x ∈ N x ∈ {+,−,/,∗} x Symbol x Symbol
x Symbol xs RPN ε RPN x xs RPN
(a) The issue is that this grammar allows for invalid programs (such as 1 + 2 or − + ∗).
x ∧ y → y
Page 2
i. [⋆⋆] Write some static semantics inference rules for a judgement ⊢ e Ok to ensure that programs are well formed.
ii. [⋆] Showthat⊢132+−Ok.
(b) We will now define some big-step evaluation semantics for this calculator. It may be helpful to read the program from right-to-left rather than left-to-right.
i.
ii. (c) [⋆⋆]
[⋆] Identify the set of evaluable expressions E, and the set of result values V . It may be helpful to use a stack, defined as follows:
x∈N xsStack ◦ Stack x ◃ xs Stack
[⋆⋆] Define a relation ⇓ ⊆ E × V which evaluates RPN programs. Now we will try small-step semantics.
Our states Σ will be of the form s ⊢ p where s is a stack of natural numbers and p is an RPN program. Initial states are all states of the form ◦ ⊢ p.
Final states are all states of the form n ◃ ◦ ⊢ ε.
Define a relation → ⊆ Σ × Σ, which evaluates one step of the calculation.
(d) [⋆⋆⋆⋆] Now we will prove the easier direction of the equivalence proof. Show using rule induction ⋆
on ⇓ that, for all expressions e, if e ⇓ v then σe → σv (where σe and σv are initial and final states respectively corresponding to e and v).
Hint: You may find it helpful to assume the following lemma (A proof of it is provided in the solutions):
⋆
◦ ⊢ xs → v ⊢ ε ⋆
Append
◦ ⊢ xs x → v ⊢ x
It is worth noting that the lemma Transitive from Question 1 applies here also.
(e) [⋆⋆⋆⋆] Show that your static semantics defined in (a) ensure that the program will not reach a stuck ⋆
state. Thatis,showthat⊢eOk =⇒ ◦⊢e→s⊢ε,forsomes. Youmayfindithelpfultogeneralise your proof goal before beginning induction.
Page 3