Tutorial 4

Exercise 1

Show by structural induction that rules of abstract machine allow us to find a value for any boolean expression $B$ in SIMP.

Boolean expressions in SIMP:

• $\neg B$
• $B\wedge B^{\prime }$

Base case:

• $P(True),P(False)$: valid as there are transition rules to prove this
• $P(E\text{ op }{E}^{\prime })$: there is a situation where bop ends up at the top of the stack; which leads us to a boolean; hence valid as there are transition rules to prove this

Induction case:

• $P(B)$ implies that $P(\neg B)$; there is a transition rule
• $P(B)$ and $P(B^{\prime })$ implies $P(B\wedge B^{\prime })$; holds as base case holds

Exercise 2

If $E$ is an integer expression, $(E,m)\Downarrow n$ holds for a unique value $n$.

Axioms:

• Transition rule is valid.
• $m$ is a function that we assume has location $l$

Rule:

• Break down into cases $(E_1,m)\Downarrow n_1$ and $(E_2,m)\Downarrow n_2$.
• Use the first axiom to prove that they evaluate to $n_1$ and $n_2$.
• Hence $(E_1\text{ op }{E}_2,m)\Downarrow n$ is equivalent to $(n_1\text{ op }{n}_2,m)\Downarrow n$ and evaluates to $n$ as $n=n_1\text{ op }{n}_2$.

Exercise 3

$$\begin{array}{rl}⟨c,m⟩& =⟨z:=!x;(x:=!y;y:=!z),s⟩\\ & =⟨z:=1;[\dots ],s⟩\text{ by }(:{=}_R\text{ and }\text{var})\\ & =⟨\text{skip};[\dots ],s\left[\begin{array}{c}z\to 1\end{array}\right]\text{ by }(\text{:=})⟩\end{array}$$

Exercise 4

The memory doesn’t change in the new rule, this means that the expressions cannot mutate the memory but this isn’t possible anyways with the current rules, to prove this; We prove that if $⟨E,s⟩\Downarrow ⟨n,s^{\prime }⟩$ then $s=s^{\prime }$.

Base cases:

• $⟨n,s⟩\Downarrow ⟨n,s⟩$
• $⟨!l,s⟩\Downarrow ⟨n,s⟩\text{ if }s(l)=n$

Inductive step:

$$\begin{array}{r}\text{IH: }⟨E_1,s⟩\Downarrow ⟨n_1,s⟩\\ ⟨E_2,s⟩\Downarrow ⟨n_2,s⟩\end{array}$$ $$\text{Prove }\underset{E_1,E_2}{\forall }⟨E_1\text{ op }{E}_2,s⟩\Downarrow ⟨n,s⟩$$

We look at the original big step semantics rule and substitute our equations into it to arrive at the second rule.

Exercise 5

We use the rules ${\text{if}}_F$: $\frac{⟨B,s⟩\Downarrow ⟨\text{False},s^{\prime }⟩⟨C_2,s^{\prime }⟩\Downarrow ⟨\text{skip},s^{\prime \prime }⟩}{⟨\text{if }B\text{ then }{C}_{!}\text{ else }{C}_2,s⟩\Downarrow ⟨\text{skip},s^{\prime \prime }⟩}$

We know that $⟨c^{\prime },s⟩\Downarrow \underset{\text{doesn’t terminate}}{⟨\text{skip},s^{\prime }⟩}$ Hence, we apply the command to the rule: $\frac{\overline{⟨\text{False},s⟩\Downarrow ⟨\text{False},s⟩}⟨C^{\prime },s⟩\Downarrow \underset{\text{doesn’t terminate}}{⟨\text{skip},s^{\prime }⟩}}{⟨\text{if }B\text{ then }{C}_{!}\text{ else }{C}_2,s⟩\Downarrow ⟨\text{skip},s^{\prime \prime }⟩}$

Exercise 6

Start with the rule for ${\text{while}}_T$:

$$\frac{⟨B,s⟩\Downarrow ⟨\text{True},s^{\prime }⟩⟨C,s^{\prime }⟩\Downarrow ⟨\text{skip},s^{\prime \prime }⟩⟨\text{while }B\text{ do }C,s^{\prime \prime }⟩\Downarrow ⟨\text{skip},s^{\prime \prime \prime }⟩}{⟨\text{while }B\text{ do }C,s⟩\Downarrow ⟨skip,s^{\prime \prime \prime }⟩}$$

We also have the rule ${\text{while}}_F$:

$$\frac{⟨B,s⟩\Downarrow ⟨\text{False},s^{\prime }⟩}{⟨\text{while }B\text{ do }C,s⟩\Downarrow ⟨\text{skip},s^{\prime }⟩}$$

We want to prove that we can’t use these rules to show $\text{while }2>0\text{ do skip}$. We use proof by contradiction, assume we can use the rules to show this.

$$\frac{\frac{\overline{⟨2,s⟩\Downarrow ⟨2,s⟩}\overline{⟨0,s⟩\Downarrow ⟨0,s⟩}}{⟨2>0,s⟩\Downarrow ⟨\text{True},s⟩}⟨\text{skip},s⟩\Downarrow ⟨\text{skip},s⟩\text{...}}{⟨\text{while }2>0\text{ do skip},s⟩\stackrel{?}{\Downarrow }⟨\text{skip},s^{\prime \prime \prime }⟩}$$

We cannot use the third rule in ${\text{while}}_T$ hence it will never terminate as $2>0$ will never evaluate to false.