Semester 2, 2018

# Tute (Week 4)

## 1 Parsing Relation

Using the inference rules for the parsing relation of arithmetic expressions given in the Tuesday slides, as well as the additional rules for let and variables from the the first Thursday slide, 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.

The module for last week partially implements a lexer and parser for the language of arithmetic expressions without let-bindings. Extend both to handle let-bindings. Use strings to represent variable names. The parsing rule is given in the slides for that lecture.

Add a case to the Token data type for identifiers and our keywords.

data Token = IntLit Int
| Ident String -- new
| Let | Equals | In | Then -- new
| LParen
| RParen
| TimesSign
| PlusSign
| Unknown
deriving (Show)


And the new types of expressions:

data Exp = Plus Exp Exp
| Times Exp Exp
| Num Int
| Let String Exp Exp
| Var String
deriving (Show)


A new case to the lexer:

lexer (c:cs) = ... -- all previous cases except "otherwise"
| c == '='  = Equals : lexer cs
| isAlpha c = let
(letters,rest) = span isAlpha (c:cs)
in toToken letters : lexer rest
| otherwise = Unknown : lexer cs
where
toToken "let" = Let
toToken "in"  = In
toToken "end" = End
toToken s     = Ident s


Then, extending the parser with variables and let expressions, by adding cases to parseAtom:

parseAtom (Ident x:rest) = (Var x, rest)
parseAtom (Let:Ident x:Equals:rest) = case parseSExp rest of
(a, In:rest') -> case parseSExp rest' of
(b, End:rest'') -> (Let x a b, rest'')
_ -> error "expected 'end'"
_ -> error "expected 'in'"


We can now parse let!

## 3 Substitution

What is the result of the substitution in the following expressions?

1. $$(\mathtt{Let}\ x\ (y.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ x)))[x:=y]$$
2. $$(\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ z))[x:=y]$$
3. $$(\mathtt{Let}\ x\ (z.\ (\mathtt{Plus}\ x\ z))[x:=y]$$
4. $$(\mathtt{Let}\ x\ (x.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ x))[x:=y]$$
1. Capture is possible. Alpha renaming could be used to make this work: $$(\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ y)))$$
2. $$(\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ z))$$
3. $$(\mathtt{Let}\ y\ (z.\ (\mathtt{Plus}\ y\ z))$$
4. $$(\mathtt{Let}\ y\ (x.\ (\mathtt{Plus}\ (\mathtt{Num}\ 1)\ x))$$

## 4 λ-calculus

### 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}$

2018-11-16 Fri 19:37