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( , )=
axioms:
And one other rule:
⇓⇓⇓
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
e1 ⇓ v1 e2 ⇓ v2 (Play e1 e2) ⇓ match(v1, v2)
2. Logical Formulae: Imagine we have a simple propositional expression language1:
x Prop y Prop x Prop ⊤ Prop ⊥ Prop x ∧ y Prop ¬x Prop
1Yes, the grammar is ambiguous, but assume it’s just a symbolic representation of abstract syntax.
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.
Solution: The set of evaluable expressions is just L. The set of values is {
CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas CfrroemattehdebNyoCurnisPtiraonjeocZtoucas
}. We have three
1
, ,
(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.
⋆
(b) We shall now prove that the reflexive, transitive closure of →, →, is implied by the big-step semantics ⋆
⋆
Refl∗ x → y y → zTrans∗ ⋆⋆
Transitive
Solution: The set of states Σ is simply the set of all expressions Prop. F = {⊤, ⊥}. I = Σ\F .
Solution:
a → a′
¬a → ¬a′ SOS-Not1 ¬⊤ → ⊥ SOS-Not2 ¬⊥ → ⊤ SOS-Not3
a → a′
a∧b→a′ ∧bSOS-And1 ⊤∧b→bSOS-And2 ⊥∧b→⊥SOS-And3
above. → is defined by the following rules:
x → x x → z i. [⋆⋆] First prove the following transitivity lemma:
⋆⋆
p→q q→r ⋆
p → r
⋆
Solution: We will proceed by rule induction on the first premise, that p → q. Therefore, for each case, we must show:
q → r ⋆
p → r
Base case (where p = q from rule Refl∗). For this case, as p = q, our goal is just
q → r ⋆
⋆
⋆
q → r ∗′′⋆
which is trivial.
Inductive case (from rule Trans ). We know that p → p (∗) and p → q (∗∗). We must show
⋆⋆
that q → r (∗∗∗) implies p → r, given the inductive hypothesis from (∗∗) that: ⋆
q → r IH ′⋆
We can now show our goal:
p →r
(∗∗∗)
q → r IH
⋆
p→p′
(∗)
p′ →r p → r
⋆
Trans∗
Page 2
ii. [⋆⋆] Now prove the following two lemmas about Not: ⋆⋆
x → ⊤ ⋆
Lemma-Not1
x → ⊥
⋆ Lemma-Not2
¬x → ⊤
¬x → ⊥
Solution:
Proof of Lemma-Not1. We proceed by rule induction on the premise, that x → ⊤, with the ⋆
goal of proving that ¬x → ⊥. ∗⋆⋆
¬⊤ → ⊥SOS-Not2 ⋆ Refl∗ ⊥ → ⊥
⋆
Base Case (from Refl ), where ⊤ → ⊤, we must show that ¬⊤ → ⊥:
⋆
Trans∗ ∗′′⋆⋆
¬⊤ → ⊥
Inductive Case (from Trans ), where x → x (∗) and x → ⊤(∗∗), we must show that ¬x → ⊥,
′⋆ with the inductive hypothesis from (∗∗) that ¬x → ⊥.
x → x′ (∗)
¬x → ¬x′ SOS-Not1 ′ ⋆ I.H
¬x →⊥ Proof of Lemma-Not2 is very similar and is omitted.
Trans∗
¬x → ⊥
⋆
iii. [⋆⋆] Now prove the following lemmas about And: ⋆⋆
x → ⊥ ⋆
Lemma-And1
x → ⊤
⋆ Lemma-And2
x ∧ y → y
x ∧ y → ⊥
Solution:
Proof of Lemma-And1. We proceed by rule induction on the premises that x → ⊥, with the ⋆
goal of proving that x ∧ y → ⊥. ∗⋆⋆
BaseCase(from Refl ),where⊥→⊥,wemustshowthat⊥∧y→⊥:
⊥ ∧ y → ⊥ SOS-And3 ⋆ Refl∗ ⊥ → ⊥
⋆
Trans∗ ∗′′⋆
x → x′ (∗)
x ∧ y → x′ ∧ y SOS-And1 ′ ⋆ I .H
⋆
⊥ ∧ y → ⊥
Inductive Case (from Trans ), where x → x (∗) and x → ⊥ (∗∗), we must show that
⋆′⋆
x ∧ y → ⊥, with the inductive hypothesis from (∗∗) that x ∧ y → ⊥.
Trans∗
x ∧y→⊥ Proof of Lemma-And2 is very similar, and is therefore omitted.
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 .
Solution: We define σTrue = ⊤, σFalse = ⊥, and σE = E for all expressions E. We proceed by rule induction on the rules of ⇓.
Base case (from rule True). We must show that ⊤ → σTrue, i.e ⊤ → ⊤ which is true by rule
Refl∗ .
Base case (from rule False) We must show that ⊥ → σFalse, i.e ⊥ → ⊥ which is true by rule Refl∗ .
Not cases:
Inductive case (from rule Not1). We must show, assuming x ⇓ True (∗), that ¬x → ⊥.
⋆⋆
⋆⋆
⋆
Page 3
x ∧ y → σv. We have two inductive hypotheses: ⋆
1. x→⊤from(∗) ⋆
2. y → σv from (∗∗)
We can show our goal as follows:
⋆⋆
We have the I.H. from (∗) that x → σTrue i.e. x → ⊤. By Lemma-Not1, we can conclude ⋆
that ¬x → ⊥ as required.
Inductive case (from rule Not2). We must show, assuming x ⇓ False (∗), that ¬x → ⊤.
⋆⋆
We have the I.H. from (∗) that x → σFalse i.e. x → ⊥. By Lemma-Not2, we can conclude ⋆
⋆
We have the I.H. from (∗) that x → ⊥. Thus, we have our goal from Lemma-And1 with the I.H.
that ¬x → ⊤ as required.
Inductive case (from rule And1). We must show, assuming x ⇓ False (∗), that x ∧ y → ⊥.
Inductive case (from rule And3). We must show, assuming x ⇓ True (∗) and y ⇓ v (∗∗), that ⋆
IH1
⋆
x → ⊤ Lemma-And2 IH2 ⋆⋆
⋆
⋆
x ∧ y → y
Thus, by induction, we have shown that E ⇓ V =⇒ E → σV
y → σv
Transitive
⋆
x ∧ y → σ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
Solution: We begin rule induction on the cases for e → e′.
Base case (from rule SOS-Not2). Where e = ¬⊤ and e′ = ⊥. We must show that ⊥ ⇓ v implies¬⊤⇓v. Theonlywayfor⊥⇓vtoholdisifv=False. Thuswecanshow¬⊤⇓v using rules Not1 and True.
Base case (from rule SOS-Not3) Where e = ¬⊥ and e′ = ⊤. We must show that ⊤ ⇓ v implies¬⊥⇓v. Theonlywayfor⊤⇓vtoholdisifv=True. Thereforewemustshow ¬⊥ ⇓ True, trivial from rules Not2 and False.
Base case (from rule SOS-And2) Where e = ⊤ ∧ e′. We must show that e′ ⇓ v implies ⊤ ∧ e′ ⇓ v. This is trivially shown by rule And2 and True.
Base case (from rule SOS-And3) Where e = ⊥∧y and e′ = ⊥. We must show that, assuming ⊥ ∧ y ⇓ v (∗), that ⊥ ⇓ v. If v were True, the assumption (∗) would indicate that ⊥ ⇓ True, which is impossible. Therefore, v must be False, and our goal can be trivially shown by the rule False.
Inductive case (from rule SOS-Not1) Where e = ¬a and e′ = ¬a′ and a → a′. We get the inductive hypothesis that:
∀v. a′ ⇓v a⇓v
And we must show that, assuming ¬a′ ⇓ v, that ¬a ⇓ v. If ¬a′ ⇓ v, this must indicate that either a′ ⇓ True, in which case v = False or a′ ⇓ False, in which case v = True. Either way,
Page 4
we can use our I.H. to conclude that a ⇓ True or a ⇓ False respectively. Then we may show our goal using either Not1 or Not2.
Inductive case (from rule SOS-And1) Where e = a∧b and e′ = a′ ∧b and a → a′. We get the inductive hypothesis that:
∀v. a′ ⇓v a⇓v
And we must show that, assuming a′ ∧b ⇓ v, that a∧b ⇓ v. If a′ ∧b ⇓ v, this must indicate that either a′ ⇓ True, in which case b ⇓ v, or a′ ⇓ False, in which case v = False. Either way, we can use our I.H. to conclude that a ⇓ True or a ⇓ False respectively. Then we may show our goal using either And1 or And2.
ii. [⋆] Now prove that every completed small step trace has a correspoding big step evaluation: ⋆
e → σv e⇓v
⋆ Solution: We begin rule induction on the cases for e → σv.
Base case (from rule Refl∗). Where e = σv. The term e can either be ⊤ or ⊥, and in either case we have that e ⇓ v.
∗′′⋆
Inductive case (from rule Trans ) Where e → e and e → σv. We get the inductive hypothesis
that e′ ⇓ v. We must show that e ⇓ v, which can be done easily using the lemma proven in the previous part.
(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.
Solution: The context shall be a set of variable names, denoted Γ.
v ∈ Γ Γ⊢vOkLookupEnv
Γ ∪ {v} ⊢ x Ok Γ ∪ {v} ⊢ x Ok Γ⊢∃v.xOk Exists Γ⊢∀v.xOk Forall
Γ⊢xOk Γ⊢yOk
This is more or less analogous to the scope-checking rules presented in lectures.
Γ⊢xOk
Γ ⊢ ¬x Ok Not Γ ⊢ x ∧ y Ok And
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 − + ∗).
i. [⋆⋆] Write some static semantics inference rules for a judgement ⊢ e Ok to ensure that programs are well formed.
Page 5
Solution: We will equip our rules with context that includes the number of values that are available on the stack.
The empty program is only valid if there is exactly one value left on the stack – this means the program will evaluate to one result:
1 ⊢ ε Ok Empty
Prepending a number to a program means that one less value is required on the stack:
x∈N (n+1)⊢xsOk n ⊢ x xs Ok
Prepending a symbol will require two values on the stack, and produce one value. The structure of the rule we write reflects this:
x∈{+,−,∗,/} (n+1)⊢xsOk (n + 2) ⊢ x xs Ok
Num
Op
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. [⋆] 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
ii. [⋆⋆] Define a relation ⇓ ⊆ E × V which evaluates RPN programs.
Solution:
1 ⊢ ε Ok Empty
2 ⊢ − Ok Op 3 ⊢ +− Ok
Op Num
2 ⊢ 2 + − Ok
1 ⊢ 3 2 + − Ok
0 ⊢ 1 3 2 + − Ok
Num
Num.
Solution: The set E is simply the set of all e such that e RPN . V is the set of all stacks.
Solution: The empty program evaluates to the empty stack: ε ⇓ ◦BS-Empty
The non-empty program ending in an operator performs the operation on the stack resulting from the previous symbols:
xs⇓a◃b◃s x∈{+,−,/,∗} xs x ⇓ (a x b) ◃ s
The non-empty program ending in a number simply pushes a number onto the stack from the previous symbols:
xs⇓s x∈N xsx⇓x◃s BS-Num
BS-Op
(c) [⋆⋆] 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 ◃ ◦ ⊢ ε.
Page 6
Define a relation → ⊆ Σ × Σ, which evaluates one step of the calculation.
Solution: Numbers simply push to the stack: x∈N
s ⊢ x xs → x ◃ s ⊢ xs SS-Num Operations simply pop two elements from the stack and operate on them.
x ∈ {+,−,∗,/}
a ◃ b ◃ s ⊢ x xs → a x b ◃ s ⊢ xs SS-Op
(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 x → v ⊢ x
It is worth noting that the lemma Transitive from Question 1 applies here also.
◦ ⊢ xs → v ⊢ ε ⋆
Append
Solution: Weshalldefineσe as◦⊢e,andσv asv⊢ε.
Basecase(fromruleBS-Empty). Wheree=εandv=◦. Wemustshow◦⊢ε→◦⊢ε,trivially
true by rule Refl∗.
Inductive case (from rule BS-Num). Here e = xs x for some x ∈ N, and v = x ◃ v′ for some stack ′′⋆′
v. Weknowthatxs⇓v whichgivesrisetotheI.H.that◦⊢xs→v ⊢ε. UsingAppendwith ⋆′⋆
that I.H., we can conclude that ◦ ⊢ xs x → v ⊢ x (∗). As we know that → is Transitive, we can write a chain of reasoning here rather than a derivation tree.
⋆′
◦⊢xsx → v⊢x (∗)
→ x◃v′ ⊢ ε (SS-Num)
Inductive case (from rule BS-Op). Here e = xs x for some operator x and v = (a x b) ◃ v′ for
some stack v′. We know that xs ⇓ a ◃ b ◃ v′, which gives rise to the inductive hypothesis that ⋆′ ⋆′
◦⊢xs→a◃b◃v ⊢ε,wemustshowthat◦⊢xsx→(axb)◃v ⊢ε. FromAppend,wecan ⋆′
thereforeconcludethat◦⊢xsx→a◃b◃v ⊢x(∗). ⋆′
◦⊢xsx → a◃b◃v ⊢x (∗) → (axb)◃v′ ⊢ε (SS-Op)
⋆
Thus we have shown by induction that the big step semantics map to the small step semantics.
We still need to prove Append. We proceed rule induction on the premise, however we will strengthen our proof goal to the more general rule below:
⋆
s ⊢ xs x → v ⊢ x This trivially implies Append by setting s = ◦.
∗⋆ Basecase(whenxs=εands=v,fromrule Refl ). Wemustshowthatv⊢x→v⊢x,trivial
s ⊢ xs → v ⊢ ε ⋆
Append’
by rule Refl∗.
Inductivecase(whens⊢xs→s ⊢xs (†)forsomes andxs,ands ⊢xs →v⊢ε(∗)). Weget the inductive hypothesis from (∗) that s′ ⊢ xs′ x → v ⊢ x.
Looking at the possible cases for (†), we can always prove that s ⊢ xs x → s′ ⊢ xs′ x (∗∗), as the rules for the small-step semantics only ever examine the left hand side of a non-empty sequence. Therefore, we may now show our goal:
s⊢xsx → s′ ⊢xs′ x (∗∗) → v⊢x (I.H.)
′′′′′′⋆
Page 7
(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.
Solution: We shall start by generalising our goal to the more flexible n ⊢ e Ok =⇒ v1 ◃ v2 ◃ ⋆
· · · ◃ vn ◃ ◦ ⊢ e → s ⊢ ε for some s and all v1 through vn. This trivially implies our first goal by setting n = 0 .
⋆
Base case (where e = ε and n = 1, from rule Empty). We must show that v1 ◃ ◦ ⊢ ε → s ⊢ ε, for
some s. This is trivially true by rule Refl∗, where s = v1 ◃ ◦.
Inductive case (where e = x xs for some x ∈ N, and n + 1 ⊢ xs Ok (∗)) Our inductive hypothesis ′′′⋆′′′′
from(∗)isthatv1◃···◃vn◃vn+1◃◦⊢xs→s ⊢εforsomes andallv0 throughvn+1.
We can show our goal by setting our goal’s s = s′, the IH’s v1′ = x and vi′ = vi−1 for all subsequent i.
v1 ◃···◃vn ◃◦⊢xxs→x◃v1 ◃···◃vn ◃◦⊢xsSS-Num ⋆ ′ IH x◃v1 ◃···◃vn ◃◦⊢xs→s ⊢ε
⋆′
v1 ◃v2 ◃···◃vn ◃◦⊢xxs→s ⊢ε
The case where x is an operator is very similar, just different stacks.
Trans∗2
Page 8