Semester 2, 2018

# Tute (Week 5)

## 1 Semantics

A robot moves along a grid according to a simple program.

The program consists of a sequence of commands move and turn, separated by semicolons, with the command sequence terminated by the keyword stop:

$\newcommand{\llbracket}{[\![} \newcommand{\rrbracket}{]\!]} \mathcal{R} ::= \texttt{move};\ \mathcal{R}\ |\ \texttt{turn};\ \mathcal{R}\ |\ \texttt{stop}$

Initially, the robot faces east and starts at the grid coordinates (0,0). The command turn causes the robot to turn 90 degrees counter-clockwise, and move to move one unit in the direction it is facing.

### 1.1 Denotational Semantics

First, devise a suitable denotational semantics for this language. For this exercise, we are only interested in the final position of the robot, so the mathematical object which we associate to the sequence of instructions should merely be the final coordinates of the robot as a 2D vector.

$\llbracket \cdot \rrbracket : \mathcal{R} \rightarrow \mathbb{Z}^2$

\begin{array}{lcl} \llbracket \mathtt{turn}; r \rrbracket & = & \begin{pmatrix} 0 & -1 \\ 1 & 0 \end{pmatrix}\llbracket r \rrbracket\\ \llbracket \mathtt{move}; r \rrbracket & = & \llbracket r \rrbracket + \begin{pmatrix} 1 \\ 0 \end{pmatrix} \\ \llbracket \mathtt{stop} \rrbracket & = & \begin{pmatrix} 0 \\ 0 \end{pmatrix} \end{array}

### 1.2 Operational Semantics

#### 1.2.1 Small-Step Semantics

Next, we will devise a set of small-step semantics rules for this language.

This means determining answers to the following questions:

1. What is the set of states?
2. Which of those states are final states, and which are initial states?
3. What transitions exist between those states?

The set of states will be a triple $$\mathbb{Z}^2 \times \mathbb{Z}^2 \times \mathcal{R}$$ containing:

• The robot's current position,
• A unit vector for the robot's facing direction, and
• The current commands being executed

The initial states are all states where the robot faces east – $$\begin{pmatrix}1 \\ 0\end{pmatrix}$$ – at coordinates $$\begin{pmatrix} 0 \\ 0 \end{pmatrix}$$.

$I = \left\{ \left(\begin{pmatrix} 0 \\ 0 \end{pmatrix}, \begin{pmatrix} 1 \\ 0 \end{pmatrix}, r\right)\ \Big\vert\ r\ \mathcal{R} \right\}$

The final states are those where the commands under execution are just stop.

$F = \left\{ (\mathbf{p}, \mathbf{d}, \texttt{stop})\ \vert\ \mathbf{p}, \mathbf{d} \in \mathbb{Z}^2 \right\}$

Lastly, the transition relation is specified by the following rules:

$\dfrac{ }{ (\mathbf{p}, \mathbf{d}, \texttt{move}; r) \mapsto \left(\mathbf{p} + \mathbf{d}, \mathbf{d}, r\right) }$

$\dfrac{ }{ (\mathbf{p}, \mathbf{d}, \texttt{turn}; r) \mapsto \left(\mathbf{p}, \begin{pmatrix}0 & -1 \\ 1 & 0\end{pmatrix}\mathbf{d}, r\right) }$

#### 1.2.2 Big-Step Semantics

Lastly, we will devise a set of big-step evaluation rules for this language.

This means determining answers to the following questions:

1. What is the set of evaluable expressions?
2. What is the set of values?
3. How do evaluable expressions evaluate to those values?

The set of evaluable expressions is once again a triple of position, direction, and commands to execute – the same as the states in the small step semantics.

The set of values is a tuple of both the final position and direction of the robot after executing the program.

There are three rules to describe the evaluation:

$\dfrac{ }{(\mathbf{p}, \mathbf{d}, \texttt{stop} ) \Downarrow (\mathbf{p}, \mathbf{d})}$

$\dfrac{ (\mathbf{p} + \mathbf{d},\mathbf{d}, r) \Downarrow (\mathbf{p'}, \mathbf{d'}) }{ (\mathbf{p}, \mathbf{d}, \texttt{move}; r) \Downarrow (\mathbf{p'}, \mathbf{d'}) }$

$\dfrac{ \left(\mathbf{p},\begin{pmatrix} 0 & -1 \\ 1 & 0 \end{pmatrix} \mathbf{d}, r\right) \Downarrow (\mathbf{p'}, \mathbf{d'}) }{ (\mathbf{p}, \mathbf{d}, \texttt{turn}; r) \Downarrow (\mathbf{p'}, \mathbf{d'}) }$

## 2 Midsession Revision/Postmortem

If your tutorial is before the midsession test, feel free to ask your tutor revision questions. If it is after the midsession test, feel free to comiserate with your tutor or ask questions from the test.

2018-11-16 Fri 19:37