Safety and Completeness of Disambiguation corresponds toTermination and Confluence of ReorderingLuı́s Eduardo de Souza Amorim1 and Eelco Visser2
1

Australian National University, Australia
LuisEduardo.deSouzaAmorim@anu.edu.au2
Delft University of Technology, The Netherlands
e.visser@tudelft.nl
Abstract
Associativity and priority are well known techniques to disambiguate expression grammars. In recent work we develop a direct semantics for disambiguation by associativity
and priority rules and prove that a safe and complete disambiguation relation producesa safe and complete disambiguation. The proof approach relies on a correspondence between disambiguation and term rewriting such that safety of disambiguation corresponds
to termination of the rewrite system and completeness of disambiguation correspond toconfluence of the rewrite system. In this extended abstract we illustrate that approach
using diagrams.

1

Introduction

Associativity and priority are well known techniques to lexical syntax
disambiguate expression grammars. Figure 1 illustrates
ID = [a-zA-Z][a-zA-Z0-9]*
the approach. An expression grammar defines the infix context-free syntaxoperators of an expression language using left- and rightExp.Var = IDrecursive productions such as Exp.Add = Exp "+" Exp.
Exp.Add = Exp "+" Exp {left}
Exp.Min = Exp "-" Exp {left}
Such a grammar is ambiguous; an expression such as a +Exp.Mul = Exp "*" Exp {left}
b + c can be read as (a + b) + c or as a + (b + c).
Exp.Div = Exp "/" Exp {left}
One way to disambiguate an expression grammar is toExp.Pow = Exp "^" Exp {right}
transform it to a grammar that uses extra non-terminals
context-freeprioritiesto represent priority levels. However such grammars areExp.Pow
harder to read and the direct correspondence to the un> {left: Exp.Mul Exp.Div}
derlying abstract syntax trees is lost. An alternative ap> {left: Exp.Add Exp.Min}
proach is to augment an ambiguous expression grammar
Figure 1: SDF3 definition.
with associativity and priority rules. The semantics ofsuch disambiguation rules is typically defined indirectlyin the implementation of parser generators or by means of grammar transformations. In recentwork, we have developed a direct semantics for associativity and priority in terms of subtree
exclusion that extends to expression grammars with prefix and postifix operators, mixfix operators, indirect recursion, and overlap. We are currently revising a paper about this work for
the TOPLAS journal [2]. A previous version of the semantics of disambiguation rules appearedin [1], but did not feature the proof technique based on rewriting. We refer to those papers fora discussion of related work.
To verify the approach we developed a technique based on term rewriting that shows thatsoundness and completeness of disambiguation corresponds to termination and confluence reordering parse trees. In this extended abstract we illustrate the proof technique for the case ofinfix expression grammars. We omit formal definitions and mostly explain the approach usingdiagrams.

Safety and Completeness of Disambiguation

Amorim and Visser

a+b*c-d

Adda

Add+ Mulba-+ Min
Mul -* Minc

Muldb

*da

Min

Add

*Min+b c-

Add adMind

Mul Add *+ Mulcb*ca+dcbmatches

Ematchesmatches

Mul

Add* MinE-EEMulE+ MinE

M ul > M inmatches-Mul* MinEE

Add left M in-Add *EEM ul > M in+EE

M ul > AddFigure 2: Parse trees for an ambiguous expression, and its disambiguation using subtree exclusion rules

2Disambiguation by Subtree Exclusion

An ambiguous sentence has multiple parse trees. The diagram in figure 2 shows the parse trees
for the expression a + b * c - d according the underlying grammar of figure 1. Disambiguation by subtree exclusion defines conflict patterns that should not occur in selected parse trees.
The safe subtree exclusion rules (for infix expressions) of SDF3 [2] are defined as follows:
A.C1 > A.C2
C1A.C1 > A.C2C1C2αβα

A

A.C1 left A.C2C1C2AAβαC2A

βA.C1 right A.C2C1AAC2βαA

A

Instantiating these rules to some of the disambiguation rules in figure 1 leads to the following
subtree exclusion patterns (aka conflict patterns):
E.M ul > E.Add
Mul

E2Add

*+E

E

E.M ul > E.Add
Mul

E.Add left E.Add
AddEE*Add

E+E+Add

E+E

Safety and Completeness of Disambiguation

Amorim and Visser

Applying these rules to the expression in figure 2 shows that the sentence is completely disambiguated as all but one parse tree for the expression are rejected.
A set of disambiguation rules is safe when each sentence in the underlying grammar isalso a sentence in the disambiguated grammar. That is, no sentences are excluded. A set ofdisambiguation rules is complete when each sentence in the underlying grammar has at most one
parse tree in the disambiguated grammar. That is, each sentence is completely disambiguated.
How can we prove that set of disambiguation rules safe and complete? That is a central questionin our work on the semantics disambiguation rules [2].

3Proving Safety and CompletenessThe central insight in our approach to proving safety and completeness of disambiguation is thatdisambiguation by means of associativity and priority rules corresponds to reordering of parsetrees. For infix expression grammars we define a rewrite system generated by instiantiating thefollowing rewrite rule schemas for each pair of productions in a grammar:
RI

C1

t21

C2

op1

op2

t22

t12

t21

op2

C1

t22

op1

RI

C1
t11

C2

op1

C2

t21

op2

t22

t12

C2

t11

C1

op2

op1

t21

t22

When we apply these rules to the expression in figure 2, we see that all trees can be converted
into each other using these rewrite rules:
AddaAdd

RI+ Mulba* Minc-Mul -yieldba+b*c-daAdd*Min+b c-

MinMul Add *da+bcyieldyield
RI*RIyield

Muldyield

dRI+ MincMin

RId

Add ad+ Mulb*c3

Safety and Completeness of Disambiguation

Amorim and Visser

In general, we have a theorem that states that all ambiguities in an infix expression grammar
are related by reordering, expressed diagrammatically as follows:

w

yield

yield

yield

t1

RI...

RI

ti

RI...

RI

tn

The reordering rewrite system is non-terminating. Each tree can be converted in each othertree. Using the subtree exclusion patterns generated from the associativity and priority rulesof a grammar, we direct the rules of the rewrite system, leading to the following rule schemas:
DI

C1

t21

C2

op1

op2

t22

t12

t21

op1

C2t21

op2

t22

if

op2

C1

t22

op1

RI

C1t11

C2

C2t11

A

t12
if

C1

op2

op1

t21

t22

∈Q

C1
C2

op1

op2

AA

∈Q

C1
A

op1

C2

A

op2

A

In our paper [2] we show that safety of disambiguation corresponds to termatination of thisrewrite system and that completeness of disambiguation corresponds to confluence of the rewritesystem. We illustrate that here using the diagrams in figures 3, 4, and 5.

AddaAddM ul>M in+ MulbaMul -* Minc-db

Mul

MinM ul>M in

Add*Min+b c-

Mul Add *dac+cMin

M ul>Addd

Add abFigure 3: Unsafety corresponds to non-termination
4*d

Add right M inAdd left M in

M ul>Adda+ Mind+ Mulb*c

Safety and Completeness of Disambiguation

Amorim and Visser

Adda

Add+ MulbaMul -* Minc-db*dc

Add left M inM ul>AddMula+ MinMinAdd*Min+b c-

Mul Add *da+MinM ul>AddAdd -dcabd+ Mulb

*cFigure 4: Incompleteness corresponds to non-confluence (non-Church Rosser)
Adda

Add

M ul>M in+ Mulba

Mul -* Minc-db*dc

Add left M in

M ul>AddMula+ Min

Min

M ul>M in

Add*Min+b c-

Mul Add *da+bc

Min

M ul>Addd

Add ad+ Mulb

*cFigure 5: Safety and completeness correspond to termination and confluence.

References[1] Luı́s Eduardo de Souza Amorim. Declarative Syntax Definition for Modern Language Workbenches.
PhD thesis, Delft University of Technology, 2019.
[2] Luı́s Eduardo de Souza Amorim and Eelco Visser. A direct semantics for declarative disambiguationof expression grammars. ACM Transactions on Programming Languages, 2020. under revision.

5