Tutorial - 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. Operational Semantics
3.1.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.1.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'}) }\]
3.2. 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}4. Abstract syntax and binding
Consider this arithmetic expression involving let-expressions:
\[ \mathtt{let} ~ x ~ = ~ 4 ~ \mathtt{in} ~ (\mathtt{let} ~ z ~ = ~ (\mathtt{let} ~ y ~ = ~ x + 1 ~ \mathtt{in} ~ x + y) ~ \mathtt{in} ~ x + z) \]
- What does it evaluate to?
- What would this term look like as first-order abstract syntax with (string) names?
- What would this term look like using de-Bruijn indices?
One evaluation strategy for a let-expression is to substitute the variable definition in the body, like this:
\[ \mathtt{let} ~ x ~ = ~ e_1 ~ \mathtt{in} ~ e_2 ~ \longrightarrow ~ e_2[x := e_1] \]
- Evaluate this expression using this strategy, and de-Bruijn indices.
4.0.1. Part 1:
There is no variable shadowing, so we can just observe that:
- x is 4
- y is x + 1, which is 5
- z is x + y, which is 9
- the final result is x + z, which is 13
4.0.2. Part 2:
The key construct is "Let nm e1 e2" for "let nm = e1 in e2".
Let "x" (Num 4) (Let "z" (Let "y" (Plus (Var "x") (Num 1)) (Plus (Var "x") (Var "y"))) (Plus (Var "x") (Var "z")))
Apologies, here and below, we would like to indent the above expression for clarity, but we can't get that to work in the markup format we are using.
4.0.3. Part 3:
To convert from name-carrying syntax to de-Bruijn syntax, we compute for each Var how many let bindings we are in between this Var and the let binding that introduced that variable. Once we have done that we can drop the names from the Let constructs.
Stepping through our expression tracking what is in scope:
| In scope | |
| Let "x" (Num 4) ( | |
| ["x"] | Let "z" (Let "y" (Plus (Var "x") (Num 1)) ( |
| ["x", "y"] | Plus (Var "x") (Var "y") |
| ["x]" | )) ( |
| ["x", "z"] | Plus (Var "x") (Var "z") |
| ["x"] | ) |
| ) |
Replacing named with indexed Var elements:
| In scope | |
| Let "x" (Num 4) ( | |
| ["x"] | Let "z" (Let "y" (Plus (Var 0) (Num 1)) ( |
| ["x", "y"] | Plus (Var 1) (Var 0) |
| ["x"] | )) ( |
| ["x", "z"] | Plus (Var 1) (Var 0) |
| ["x"] | ) |
| ) |
The final result is:
Let (Num 4) (Let (Let (Plus (Var 0) (Num 1)) (Plus (Var 1) (Var 0))) (Plus (Var 1) (Var 0)))
4.0.4. Part 4:
In de-Bruijn style, substitution into a let works like this:
(Let e1 e2)[i := e3] \(\equiv\) Let (e1[i := e3]) (e2[i + 1 := e3])
The above assumes e3 does not contain any Vars needing adjusting.
Using this approach:
Let (Num 4) (Let (Let (Plus (Var 0) (Num 1)) (Plus (Var 1) (Var 0))) (Plus (Var 1) (Var 0)))
\(\mapsto\) (Let (Let (Plus (Var 0) (Num 1)) (Plus (Var 1) (Var 0))) (Plus (Var 1) (Var 0)) )[0 := Num 4]
\(\equiv\) Let ((Let (Plus (Var 0) (Num 1)) (Plus (Var 1) (Var 0)))[0 := Num 4]) ((Plus (Var 1) (Var 0))[1 := Num 4])
\(\equiv\) Let (Let ((Plus (Var 0) (Num 1))[0 := Num 4]) ((Plus (Var 1) (Var 0))[1 := Num 4])) (Plus (Num 4) (Var 0))
\(\equiv\) Let (Let (Plus (Num 4) (Num 1)) (Plus (Num 4) (Var 0))) (Plus (Num 4) (Var 0))
\(\mapsto\) Let (Let (Num 5) (Plus (Num 4) (Var 0))) (Plus (Num 4) (Var 0))
\(\mapsto\) Let ((Plus (Num 4) (Var 0))[0 := Num 5]) (Plus (Num 4) (Var 0))
\(\equiv\) Let (Plus (Num 4) (Num 5)) (Plus (Num 4) (Var 0))
\(\mapsto\) Let (Num 9) (Plus (Num 4) (Var 0))
\(\mapsto\) (Plus (Num 4) (Var 0))[0 := Num 9]
\(\equiv\) Plus (Num 4) (Num 9)
\(\mapsto\) Num 13