1. (a)
(b)
(c)
COMP3161/COMP9164
Syntax Exercises
Liam O’Connor September 26, 2019
[⋆] Consider the following expressions in Higher Order abstract syntax. Convert them to concrete syntax.
i. (Let (Num 3) (x. (Let (Plus x (Num 1)) (x. (Plus x x)))))
ii. (Plus (Let (Num 3) (x. (Plus x x))) (Let (Num 2) (y. (Plus y (Num 4)))))
iii. (Let (Num 2) (x. (Let (Num 1) (y. (Plus x y)))))
[⋆] Apply the substitution x := (Plus z 1) to the following expressions:
i. (Let (Plus x z) (y. (Plus x y))) ii. (Let (Plus x z) (x. (Plus z z))) iii. (Let (Plus x z) (z. (Plus x z)))
[⋆] Which variables are shadowed in the following expression and where?
(Let (Plus y 1) (x. (Let (Plus x 1) (y. (Let (Plus x y) (x. (Plus x y)))))))
2. Here is a concrete syntax for specifying binary logic gates with convenient if − then − else syntax. Note that the else clause is optional, which means we must be careful to avoid ambiguity – we introduce mandatory parentheses around nested conditionals:
⊤ Output ⊥ Output α Input β Input
c Input t IExpr e Expr if c then t else e Expr
c Input t IExpr x Output if c then t Expr x IExpr
e Expr (e) IExpr
e IExpr e Expr
If an else clause is omitted, the result of the expression if the condition is false is defaulted to ⊥. For example, an AND or OR gate could be specified like so:
Or, a NAND gate:
AND : if α then (if β then ⊤)
OR : if α then ⊤ else (if β then ⊤)
if α then (if β then ⊥ else ⊤) else ⊤
(a) [⋆⋆] Devise a suitable abstract syntax A for this language.
(b) [⋆] Write rules for a parsing relation (←→) for this language.
(c) [⋆] Here’s the parse derivation tree for the NAND gate above:
⊥ Output ←→ β Input ←→ ⊥ IExpr ←→
⊤ Output ←→ ⊤ IExpr ←→ ⊤ Expr ←→
⊤ Output ←→ ⊤ IExpr ←→ ⊤ Expr ←→
if β then ⊥ else ⊤ Expr ←→ (if β then ⊥ else ⊤) IExpr ←→
α Input ←→
if α then (if β then ⊥ else ⊤) else ⊤ Expr ←→
Fill in the right-hand side of this derivation tree with your parsing relation, labelling each step as you progress down the tree.
1
3. Here is a first order abstract syntax for a simple functional language, Lc. In this language, a lambda term defines a function. For example, lambda x (var x) is the identity function, which simply returns its input.
e1 Lc e2 Lc x VarName e Lc x VarName Appe1 e2 Lc LambdaxeLc VarxLc
(a) [⋆] Give an example of name shadowing using an expression in this language, and provide an α- equivalent expression which does not have shadowing.
(b) [⋆⋆] Here is an incorrect substitution algorithm for this language:
(App e1 e2)[v := t] (Var v)[v := t] (Lambda x e)[v := t]
→ App (e1[v := t]) (e2[v := t]) → t
→ Lambda x (e[v := t])
What is wrong with this algorithm? How can you correct it?
(c) [⋆⋆] Aside from the difficulties with substitution, using arbitrary strings for variable names in first- order abstract syntax means that α-equivalent terms can be represented in many different ways, which is very inconvenient for analysis. For example, the following two terms are equivalent, but have different representations:
Lambda x (Lambda y (App (Var x) (Var y)))
Lambda a (Lambda b (App (Var a) (Var b)))
One technique to achieve canonical representations (i.e α-equivalence is the same as equality) is called
higher order abstract syntax (HOAS). Explain what HOAS is and how it solves this problem.
Page 2