Tute - Completed (Week 3)
Table of Contents
1. Parsing Relation
Using the inference rules for the parsing relation of arithmetic expressions
given in the syntax slides, derive the abstract syntax
corresponding to the concrete syntax 3 + let x = 5 in x + 2 end.
Here \(\texttt{Num}\) nodes are shortened to just \(\mathtt{N}\).
\[ \tiny{ \dfrac{ \dfrac{ \dfrac{}{ \texttt{3}\ \mathbf{Atom} \longleftrightarrow (\mathtt{N}\ 3)} }{\texttt{3}\ \mathbf{PExp} \longleftrightarrow (\mathtt{N}\ 3) } \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{}{ \texttt{5}\ \mathbf{Atom} \longleftrightarrow (\mathtt{N}\ 5)} }{\texttt{5}\ \mathbf{PExp} \longleftrightarrow (\mathtt{N}\ 5) } }{\texttt{5}\ \mathbf{SExp} \longleftrightarrow (\mathtt{N}\ 5) } \dfrac{ \dfrac{ \dfrac{}{ \texttt{x}\ \mathbf{Atom} \longleftrightarrow (\mathtt{Var}\ \texttt{"x"})} }{\texttt{x}\ \mathbf{PExp} \longleftrightarrow (\mathtt{Var}\ \texttt{"x"}) } \dfrac{ \dfrac{ \dfrac{}{ \texttt{2}\ \mathbf{Atom} \longleftrightarrow (\mathtt{N}\ 2)} }{\texttt{2}\ \mathbf{PExp} \longleftrightarrow (\mathtt{N}\ 2) } }{\texttt{2}\ \mathbf{SExp} \longleftrightarrow (\mathtt{N}\ 2) } }{\texttt{x + 2}\ \mathbf{SExp} \longleftrightarrow (\mathtt{Plus}\ (\mathtt{Var}\ \texttt{"x"})\ (\mathtt{N}\ 2) ) } }{\texttt{let x = 5 in x + 2 end}\ \mathbf{Atom} \longleftrightarrow (\mathtt{Let}\ \texttt{"x"}\ (\mathtt{N}\ 5)\ (\mathtt{Plus}\ (\mathtt{Var}\ \texttt{"x"})\ (\mathtt{N}\ 2))) } }{\texttt{let x = 5 in x + 2 end}\ \mathbf{PExp} \longleftrightarrow (\mathtt{Let}\ \texttt{"x"}\ (\mathtt{N}\ 5)\ (\mathtt{Plus}\ (\mathtt{Var}\ \texttt{"x"})\ (\mathtt{N}\ 2))) } }{\texttt{let x = 5 in x + 2 end}\ \mathbf{SExp} \longleftrightarrow (\mathtt{Let}\ \texttt{"x"}\ (\mathtt{N}\ 5)\ (\mathtt{Plus}\ (\mathtt{Var}\ \texttt{"x"})\ (\mathtt{N}\ 2))) } } {\texttt{3 + let x = 5 in x + 2 end}\ \mathbf{SExp} \longleftrightarrow (\mathtt{Plus}\ (\mathtt{N}\ 3)\ (\mathtt{Let}\ \texttt{"x"}\ (\mathtt{N}\ 5)\ (\mathtt{Plus}\ (\mathtt{Var}\ \texttt{"x"})\ (\mathtt{N}\ 2))))} } \] Typically this is computed by first doing the concrete syntax derivation, then filling the abstract syntax in from axioms down.
2. Substitution
What is the result of the substitution in the following expressions?
- \((\mathtt{Let}\ x\ (y.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ x)))[x:=y]\)
- \((\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ z))[x:=y]\)
- \((\mathtt{Let}\ x\ (z.\ (\mathtt{Plus}\ x\ z))[x:=y]\)
- \((\mathtt{Let}\ x\ (x.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ x))[x:=y]\)
- Capture is possible. Alpha renaming could be used to make this work: \((\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ y)))\)
- No effect: \((\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ z))\)
- \((\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ y\ z))\)
- Remember that a substitution only applies to the free occurrences of a variable, and only the first \(x\) is free: \((\mathtt{Let}\ y\ (x.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ x))\)
3. Semantics
You may want to look at the W3 Tuesday notes before attempting these questions.
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.
3.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\]
Remember from linear algebra that rotation matrices can be used to rotate a vector anticlockwise in the plane. For our purposes, we want \(\theta = \pi/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}3.2. Operational Semantics
3.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:
- What is the set of states?
- Which of those states are final states, and which are initial states?
- 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) } \]
3.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:
- What is the set of evaluable expressions?
- What is the set of values?
- 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'}) }\]
4. Lambda calculus and binding
4.1. Reduction
Apply \(\beta\) and \(\eta\) reduction as much as possible to this term, until you reach a normal form. Where necessary, use \(\alpha\) renaming to avoid capture.
\[ (\lambda n\ f\ x.\ f\ (n\ x\ x))\ (\lambda f\ x.\ f) \]
\[ \begin{array}{lcl} (\lambda n\ f\ x.\ f\ (n\ x\ x))\ (\lambda f\ x.\ f) & \mapsto_\beta & (\lambda f\ x.\ f\ ((\lambda f\ x.\ f)\ x\ x))\\ & \equiv_\alpha & (\lambda f\ x.\ f\ ((\lambda f\ x'.\ f)\ x\ x))\\ & \mapsto_\beta & (\lambda f\ x.\ f\ ((\lambda x'.\ x)\ x))\\ & \mapsto_\beta & (\lambda f\ x.\ f\ x)\\ & \mapsto_\eta & (\lambda f.\ f)\\ \end{array} \]
4.2. de Bruijn Indices
How would the above \(\lambda\) term be represented in de Bruijn indices? Repeat the same reduction with de Bruijn indices.
\[\begin{array}{lcl} (\lambda.\ \lambda.\ \lambda.\ \mathbf{1}\ (\mathbf{2}\ \mathbf{0}\ \mathbf{0}))\ (\lambda.\ \lambda.\ \mathbf{1}) & \mapsto_\beta & (\lambda.\ \lambda.\ \mathbf{1}\ ((\lambda.\ \lambda.\ \mathbf{1})\ \mathbf{0}\ \mathbf{0}))\\ & \mapsto_\beta & (\lambda.\ \lambda.\ \mathbf{1}\ ((\lambda.\ \mathbf{1})\ \mathbf{0}))\\ & \mapsto_\beta & (\lambda.\ \lambda.\ \mathbf{1}\ \mathbf{0})\\ & \mapsto_\eta & (\lambda.\ \mathbf{0}) \end{array}\]