COMP3161/COMP9164
Syntax Exercises
Liam O’ 26, 2019
1. (a) [⋆] 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)))))
(b) [⋆] 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)))
(c) [⋆] 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 c Input t IExpr x Output
Solution: letx=3inletx=x+1inx+x
Solution: (letx=3inx+x)+(lety=2iny+4)
Solution: let x = 2+(let y = 1 in x+y)
Solution: (Let (Plus (Plus z 1) z) (y. (Plus (Plus z 1) y)))
Solution: (Let (Plus (Plus z 1) z) (x. (Plus z z)))
Solution: Undefined without applying α-renaming first. Can safely substitute after renaming the bound z to a: (Let (Plus (Plus z 1) z) (a. (Plus (Plus z 1) a)))
Solution: The innermost let shadows the binding of x from the outermost let. The middle let shadows the free y mentioned in the outermost let.
if c then t else e Expr
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.
x∈{a,b} x∈{T,F} cInput tA eA xOutput x Input x Output If c t e A x A
⊤ Output ←→ TTop ⊥ Output ←→ FBot α Input ←→ AInputα β Input ←→ BInputβ
c Input ←→ c′ t IExpr ←→ t′ ifcthentExpr←→Ifc′ t′ F If2
e Expr ←→ e′ e Output ←→ e′
(e) IExpr ←→ e′ Paren e IExpr ←→ e′ Shunt1 e Expr ←→ e′ Shunt2
c Input ←→ c′ t IExpr ←→ t′ e Expr ←→ e′ ifcthentelseeExpr←→Ifc′ t′ e′ If1
e IExpr ←→ e′
(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.
⊤ Output ←→ T ⊥ Output ←→ F ⊤ IExpr ←→ T β Input ←→ B ⊥ IExpr ←→ F ⊤ Expr ←→ T
if β then ⊥ else ⊤ Expr ←→ If B F T (if β then ⊥ else ⊤) IExpr ←→ If B F T
⊤ Output ←→ T ⊤ IExpr ←→ T ⊤ Expr ←→ T
α Input ←→ A
if α then (if β then ⊥ else ⊤) else ⊤ Expr ←→ If A (If B F T) T
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
(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:
Solution: A simple example is Lambda x (Lambda x (Var x)). Here, the name x is shadowed in the inner binding.
An α-equivalent expression without shadowing would use a different variable y, i.e
Lambda x (Lambda y (Var y))
(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.
Solution: The substitution doesn’t deal with name clashes. The rule for lambdas should look like
Lambdax(e[v:=t]) ifx̸=vandx∈/FV(t) (Lambda x e)[v := t] → Lambda x e if x = v
undefined otherwise
Solution: Higher order abstract syntax encodes abstraction in the meta-logic level, or in the language implementation, rather than as a first-order abstract syntax construct.
First order abstract syntax might represent a term like λx.x as something like
Lambda ”x” (Var ”x”), where literal variable name strings are placed in the abstract syntax directly. Higher order abstract syntax, however, would place a function inside the abstract syntax, i.e Lambda (λx. x), where the variable x is a meta-variable (or a variable in the language used to implement our interpreter, rather than the language being implemented). This function is (exten- sionally) equal to any other α-equivalent function, and therefore we can consider two α-equivalent terms to be equal with HOAS, assuming extensionality (that is, a function f equals a function g if and only if, for all x, f(x) = g(x).
For example, a first order Haskell implementation of the above syntax might look like this:
type VarName = String
data AST = App AST AST
| Var VarName
| Lambda VarName AST
test = Lambda “x” (Lambda “y” (App (Var “x”) (Var “y”)))
Whereas a higher order syntax might look like this:
data AST = App AST AST
| Lambda (AST -> AST)
test = Lambda $ \x -> Lambda $ \y -> App x y
There is no way in Haskell, for example, to determine that we used the names x and y for those function arguments. The only way for a Haskell function f to be distinguished from a function g is for f x to be different from g x for some x (i.e extensionality). As α-equivalent Haskell functions cannot be so distinguished, we must judge a term as equal to any other in its α-equivalence class.