Tute (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.
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]\)
3. 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.
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\]
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?
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?
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.