Walking on SR-automata to detect grammar ambiguity

TL;DR

This paper introduces SR-automata, a novel method leveraging LR parsing table nondeterminism to detect grammar ambiguity by analyzing paths that reach and diverge at conflict states.

Contribution

It presents a new approach using SR-automata to identify ambiguity in grammars through conflict-driven analysis of LR parsing tables.

Findings

SR-automata effectively identify ambiguous words in grammars.

The method provides a systematic way to analyze LR parser conflicts.

It enhances understanding of grammar ambiguity detection techniques.

Abstract

We exploit the nondeterminism of LR parsing tables to reason about grammar ambiguity after a conflict-driven strategy. First, from parsing tables we define specialized structures, called SR-automata. Next, we search for ambiguous words along the paths of SR-automata that reach a conflict state and then diverge along the branches corresponding to distinct resolutions of the conflict.

Figures

Equations

$$P_I\frac{\text{buildrel}{w}_1}{\text{Longmapsto}}R{\frac{\text{buildrel}[x]}{⟶}}^{\text{lower}6.0pt\ast }P\frac{\text{buildrel}[x]}{⟶}{Z}_1\frac{\text{buildrel}x}{⟹}{Q}_1\frac{\text{buildrel}{w}_2\$}{\text{Longmapsto}}{P}_F{P}_I\frac{\text{buildrel}{w}_1}{\text{Longmapsto}}R{\frac{\text{buildrel}[x]}{⟶}}^{\text{lower}6.0pt\ast }P\frac{\text{buildrel}[x]}{⟶}{Z}_2\frac{\text{buildrel}x}{⟹}{Q}_2\frac{\text{buildrel}{w}_2^{\prime }\$}{\text{Longmapsto}}{P}_F$$

$$P_I\frac{\text{buildrel}{w}_1}{\text{Longmapsto}}R{\frac{\text{buildrel}[x]}{⟶}}^{\text{lower}6.0pt\ast }P\frac{\text{buildrel}x}{⟶}{Q}_1\frac{\text{buildrel}{w}_2\$}{\text{Longmapsto}}{P}_F{P}_I\frac{\text{buildrel}{w}_1}{\text{Longmapsto}}R{\frac{\text{buildrel}[x]}{⟶}}^{\text{lower}6.0pt\ast }P\frac{\text{buildrel}[x]}{⟶}Z\frac{\text{buildrel}x}{⟹}{Q}_2\frac{\text{buildrel}{w}_2^{\prime }\$}{\text{Longmapsto}}{P}_F$$

Full text

Walking on SR-automata to detect

grammar ambiguity

Paola Quaglia

University of Trento

Abstract

We exploit the nondeterminism of LR parsing tables to reason about grammar ambiguity after a conflict-driven strategy. First, from parsing tables we define specialized structures, called SR-automata. Next, we search for ambiguous words along the paths of SR-automata that reach a conflict state and then diverge along the branches corresponding to distinct resolutions of the conflict.

1998 ACM Subject Classification F.4.2 Grammars and Other Rewriting Systems

Keywords Context-free grammars; LR parsing; Ambiguity

1 Introduction

Grammar ambiguity is undecidable [6, 10], and various, inevitably incomplete, approaches have been investigated to detect ambiguity in some cases (e.g., [11, 17, 15, 3, 5, 16, 4]). Some of these techniques are exploratory, meaning that ambiguous derivations are searched for among those generated by the grammar. Other methods are approximate, in the sense that the decision is taken on some approximation of the given language.

Here we present a strategy for ambiguity detection that is centered around a conflict-driven post-processing of the output of a bottom-up parser. We base our analysis on the widespread availability of LALR(1) [7] parser generators (e.g. [12, 9]). If the parsing table for a given grammar is deterministic, then the grammar is surely unambiguous. On the other hand, if the parsing table is nondeterministic, then the grammar might be ambiguous, or it might belong to a deterministic class bigger than that for which the table was built. Hence, we can let a parser generator do a pre-screening of unambiguity, and perform further checks only on those grammars that lead to the construction of nondeterministic tables. Above we made the case for LALR(1) parsing tables. The technique, however, applies to all the tables constructed as controllers for the shift-reduce algorithm (e.g., SLR(1) [8], LR(1) [2]). So, in what follows, we generically refer to tables for LR parsing in its broadest sense [13], and indeed, the bigger the class analyzable by the table, the higher the probability that its nondeterminism depends on ambiguity.

To detect ambiguity, we focus on the conflicts found in nondeterministic tables. First, we define SR-automata. They are built from the characteristic automata underlying parsing tables, and encode all the information needed to mimic the shift-reduce algorithm. There is a main difference, though, between the two sorts of automata. In the case of SR-automata, the accepted words are obtained by a specialized concatenation of the terminals found along an unbroken path from the initial to the final state. This does not apply to characteristic automata, where, due to reductions, the same words are recognized by concatenating the terminals scattered along segmented paths.

Working on SR-automata, we look for ambiguous words among those that can be recognized along paths that traverse a conflict state. This activity is partially abstracted by operating on approximated versions of SR-automata that are forgetful of the details needed to control executions, and hence accept a superset of the language under investigation. Essentially, we guess the ambiguous words by searching paths on the approximated structure. We then go back to the SR-automaton to validate those words against proper executions of the shift-reduce algorithm.

The rest of the paper is organized as follows. Sec. 2 presents basic definitions and conventions. SR-automata and their properties are dealt with in Sec. 3. The proposed detection strategy is the subject of Sec. 4, and Sec. 5 concludes the paper. We assume the reader be familiar with the theory of LR parsing (see, e.g., [1, 18]).

2 Preliminaries

In this section, we will collect basic definitions and the adopted conventions.

A context-free grammar is a tuple $\mathcal{G}=(V,T,S,\mathcal{P})$ where $V$ is the finite set of terminals and nonterminals, $T$ is the set of terminals, $S\in(V\setminus{T})$ is the start symbol, and $\mathcal{P}$ is the finite set of productions. We assume grammars be reduced, and adopt the following notational conventions. The empty string is denoted by $\epsilon$, $V^{*}$ is ranged over by $\alpha,\beta,\ldots$, $(V\setminus T)$ by $A,B,\ldots$, $T$ by $a,b,\ldots$, T\cup\mbox{{$}} by $x,x^{\prime},\ldots$, and $T^{*}$ by $w,w^{\prime},\ldots$. Productions are written $A\rightarrow\beta$, and $\mathop{\mid}\beta\mathop{\mid}$ denotes the length of $\beta$. Moreover, $\mathcal{L}(\mathcal{G})$ stands for the language generated by $\mathcal{G}$.

Given any context-free grammar $\mathcal{G}$, LR parsing is applied to strings followed by the endmarker symbol \\notin V$. The parsing table is constructed for the augmented version of$\mathcal{G}$defined as$(V^{\prime},T^{\prime},S^{\prime},\mathcal{P}^{\prime})$where$S^{\prime}$is a fresh symbol,$V^{\prime}=V\cup\mbox{$\{S^{\prime}\}$}$,$T^{\prime}=T\cup\mbox{\{\}}, and \mathcal{P}^{\prime}=\mathcal{P}\cup\mbox{{S^{\prime}\rightarrow{S}$}}. Parsing is performed by running the shift-reduce algorithm [13] using a parsing table as controller, and reading the next input symbol. Two auxiliary structures are involved: a stack to trace the history of computation by recording the traversed states, and a stack to keep trace of the reductions performed. When the parsing of a given word $w$ is successful, the second stack, named ${\rm{tree}}({w})$, contains, from top to bottom, the sequence of productions for the rightmost derivation of $w$ in $\mathcal{G}$.

Different controllers are adopted for different classes of LR parsing. Nonetheless, in any case the parsing table is mechanically computed from two objects that are finer or coarser depending on which class of grammars the table is supposed to parse [14]. These objects are a characteristic automaton, and a lookahead function. Characteristic automata are deterministic finite state automata. Their states are sets of items, i.e. of productions with a dot at some position of their right-hand side. The initial state is the one containing the item S^{\prime}\rightarrow\cdot{S}\$$, and the final state is the one containing S^{\prime}\rightarrow{S}$\cdot$. The transition function of the characteristic automaton is used to set up the *shift* and the *goto* entries of the parsing table. A directive to *reduce* the production$A\rightarrow{\beta}$is inserted in the table at the entry$(P,x)$iff the state$P$of the automaton contains the item$A\rightarrow{\beta}\cdot$and$x\in\mathcal{L}\mathcal{A}(A\rightarrow\beta,P)$, where$\mathcal{L}\mathcal{A}(_,_)$ is the lookahead function mentioned above.

Parsing tables can be nondeterministic, meaning that they may have multiply-defined entries containing either a shift and a reduce directive (called s/r conflict) or multiple reduce directives relative to distinct productions (called r/r conflict). Here we are mainly interested in nondeterministic parsing tables. To run the shift-reduce algorithm over them, we assume that, any time control goes to an entry of the table that contains a conflict, a random local choice resolves the conflict in favour of one of the possible alternatives.

In what follows, given a characteristic automaton ${\mathcal{A}}$ for the augmented version of a grammar $\mathcal{G}$ and an associated lookahead function $\mathcal{L}\mathcal{A}$, we will refer to the pair $(\mathcal{A},\mathcal{L}\mathcal{A})$ as to a parsing table of $\mathcal{G}$. Also, we will call parsing of $w$ on $(\mathcal{A},\mathcal{L}\mathcal{A})$ the application to the string $w$ of the shift-reduce algorithm driven by the controller $(\mathcal{A},\mathcal{L}\mathcal{A})$.

3 SR-automata

In this section, we will define SR-automata, and present their main properties.

Below, we will denote automata with a single final state by a tuple whose elements represent, respectively, the set of states, the vocabulary, the transition function, the initial state, and the final state. Also, given a set $L$ of symbols, we let $[L]$ represent the set of all the elements of $L$ surrounded by square brackets. We call prospective symbols the elements of $[L]$. The intuition behind a prospective symbol like $[x]$ is that we go across it pretending that its concrete counterpart $x$ will eventually be found and consumed.

Definition 3.1** (SR-automata: layout).**

Let $(\mathcal{A},\mathcal{L}\mathcal{A})$ be a parsing table of $\mathcal{G}=(V,T,S,\mathcal{P})$. Also, let {\mathcal{A}}=(\mathcal{Q},V\cup\mbox{{$}},\tau_{c},P_{I},P_{F}). Then the SR-automaton for $(\mathcal{A},\mathcal{L}\mathcal{A})$ is the finite state automaton (\mathcal{Q},T\cup\mbox{{$}}\mathrel{\cup}([T\cup\mbox{{$}}]\times{\mathcal{Q}}\times{\mathcal{P}}),\tau_{sr},P_{I},P_{F}) where $\tau_{sr}$ is defined by the following rules

\begin{array}[]{l@{\hspace{7ex}}l}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 1.4418pt\hbox{\displaystyle\penalty 1\tau_{c}(P,x)=Q}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=55.55275pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\tau_{sr}(P,x)=Q}}}}\hfil\hskip 30.1388pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1x\in\mathcal{L}\mathcal{A}(A\rightarrow\beta,P),\quad R\in\mbox{${\rm{opening}}(A\rightarrow\beta,P)$},\quad\tau_{c}(R,A)=Q}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=251.99188pt\hbox{}}}\hbox{\kern 75.58421pt\hbox{\displaystyle\tau_{sr}(P,[x]:{R}:{A\rightarrow\beta})=Q}}}}\\[8.61108pt] \end{array}**

with R\in\mbox{{\rm{opening}}(A\rightarrow\beta,P)} iff there is a path spelling $\beta$ in $\mathcal{A}$ from $R$ to $P$.

For the grammar $\mathcal{G}_{1}$ with production-set given by $\{E\rightarrow{E+E},\,E\rightarrow{a}\}$, Fig. 1 shows the instance of $(\mathcal{A},\mathcal{L}\mathcal{A})$ à la Bison and the corresponding SR-automaton.

The language accepted by an SR-automaton is defined in terms of an execution relation which describes transitions between configurations. Each configuration is a quadruple of the shape $\langle h,\,s,\,z,\,t\rangle$ where $z$ is a string of symbols in T\cup\mbox{{$}}, $s$ (called state-stack) is a stack that contains states, $t$ (called production-stack) is a stack that contains productions, and $h$ is an auxiliary object to trace which prospective symbol, if any, was involved in the past transition. We denote stacks as lists of elements with the top of stack at the rightmost position, so that $[]$ represents the empty stack. Also, we use the usual functions ${\rm{top}}({\_})$, ${\rm{push}}(\_,\_)$, and ${\rm{pop}}(\_)$ on stacks, and let ${\rm{pop}}^{n}(s)$ stand for $n$ consecutive applications of the function ${\rm{pop}}$ to the stack $s$.

Definition 3.2** (SR-automata: execution & language).**

Let $\mathcal{S}$ be an SR-automaton with transition function $\tau_{sr}$, and initial state $P_{I}$. The language accepted by $\mathcal{S}$ is given by

\mathcal{L}(\mathcal{S})=\{w\mid\exists\,s,t\mbox{ such that }\langle\epsilon,\,[{P_{I}}],\,\epsilon,\,[{}]\rangle\rightsquigarrow^{*}\langle\epsilon,\,s,\,w\,,t\rangle}$**

where the execution relation $\rightsquigarrow$ is defined by the following rules

\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\mbox{${\rm{top}}({s})$}=P,\quad\tau_{sr}(P,x)=Q,\quad h\in\mbox{$\{\epsilon,[x]\}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=173.58513pt\hbox{\kern 3.00003pt(S)}}}\hbox{\kern 11.81737pt\hbox{\displaystyle\langle h,,s,,w,,t\rangle\rightsquigarrow\langle\epsilon,,\mbox{${\rm{push}}(Q,s)$},,wx,,t\rangle}}}}\\[17.22217pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\mbox{${\rm{top}}({s})$}=P,\quad\tau_{sr}(P,[x]:{R}:{A\rightarrow\beta})=Q,\quad s^{\prime}={\mbox{${\rm{pop}}^{\mathop{\mid}\beta\mathop{\mid}}(s)$}},\quad\mbox{${\rm{top}}({s^{\prime}})$}=R,\quad h\in\mbox{$\{\epsilon,[x]\}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=342.93608pt\hbox{\kern 3.00003pt(R)}}}\hbox{\kern 66.70204pt\hbox{\displaystyle\langle h,,s,,w,,t\rangle\rightsquigarrow\langle[x],,\mbox{${\rm{push}}(Q,s^{\prime})$},,w,,\mbox{${\rm{push}}(A\rightarrow\beta,t)$}\rangle}}}}\end{array}**

Rule (S) in the definition of $\rightsquigarrow$ mimics the execution of a shift move of the shift-reduce algorithm. Here we just observe two facts. First, $h$ is required to be either empty or the prospective version of the symbol which triggers the execution step. Second, when $h$ actually equals $[x]$, the application of rule (S) obliterates the tracing of $[x]$ in the reached configuration. Hence, an execution step involving a prospective symbol $[x]$ can never be followed by a step depending on some $\tau_{sr}(P_{n},x^{\prime})$ with ${x^{\prime}}\neq{x}$. Also, the tracing of a prospective symbol stops once its concrete version is met. Rule (R) simulates the execution of a reduce move, with the prospective symbol $[x]$ playing the lookahead $x$ that calls for the reduction. Notice that the application of the (R) rule traces $[x]$ in the first component of the new configuration. Moreover, by the premiss h\in\mbox{{\epsilon,[x]}}, an execution step depending on the prospective symbol $[x]$ can never be followed by a step depending on $[x^{\prime}]$ if ${x^{\prime}}\neq{x}$. Overall, the intuition behind the use of prospective symbols in SR-automata is that once a symbol $[x]$ starts playing as lookahead for a reduction, it keeps doing so until an application of the (S) rule actually consumes $[x]$ in the first component of the configuration, and appends $x$ to the word under construction.

Next, we present a result on the correspondence between the execution of the shift-reduce algorithm and the execution of SR-automata.

Theorem 3.3**.**

Let $\mathcal{S}$ be the SR-automaton for the parsing table $(\mathcal{A},\mathcal{L}\mathcal{A})$ of $\mathcal{G}$. Also, let $P_{I}$ be the initial state of $\mathcal{S}$. Then the following holds.

• •

If, for some local resolution of possible conflicts, the parsing of $w$ on $(\mathcal{A},\mathcal{L}\mathcal{A})$ is successful and returns ${\rm{tree}}({w})$ then, for some $s$, \langle\epsilon,\,[{P_{I}}],\,\epsilon,\,[{}]\rangle\rightsquigarrow^{*}\langle\epsilon,\,s,\,w\,,\mbox{${\rm{tree}}({w})$}\rangle$.

• •

If, for some $s$ and some $t$, \langle\epsilon,\,[{P_{I}}],\,\epsilon,\,[{}]\rangle\rightsquigarrow^{*}\langle\epsilon,\,s,\,w\,,t\rangle$* then, for some local resolution of possible conflicts, the parsing of *$w$* on *$(\mathcal{A},\mathcal{L}\mathcal{A})$* is successful and *$\mbox{${\rm{tree}}({w})$}=t$.

Proof**.**

The first statement is proved by induction on the number of steps performed by the shift-reduce algorithm. The inductive handle is based on the following facts. Each move of the shift-reduce algorithm is matched by an execution step of the SR-automaton, and the state-stack of the automaton evolves exactly as the parsing auxiliary stack. Also, at each move, the word-component of the configuration reached by the automaton equals the portion of input already processed by the shift-reduce algorithm, and the production-stacks of the two executions grow in lockstep fashion.

In proving the second statement, care has to be taken to ensure that, if the SR-automaton performs a step which involves either $x$ or $[x]$, then the symbol $x$ is actually what the shift-reduce algorithm gets from its input buffer. To get the required guarantees, the statement is proven by induction on the length of SR-automata executions whose latest step is obtained by an application of rule (S), which is the case, indeed, for executions leading to \langle\epsilon,\,s,\,w\,,t\rangle$. By the definition of$\rightsquigarrow$, if the execution step is inferred by rule (S) and depends on an$x$-transition of the automaton, then$x$shows as suffix of the word-component of the reached configuration. Suppose now that the execution step is deduced by rule (R), that it involves$[x]$, and that the word-component of the current configuration is$w$. If this is the case, then by the properties of$\rightsquigarrow^{}$described above,$x$is the symbol that is appended to$w$ at the first (S)-step along the execution. As for the rest, the inductive handle is dual to that used in the proof of the first statement. It keeps track of the correspondence between pairs of stacks, and between the word-component of configurations and the word consumed by the shift-reduce algorithm.*

Cor. 3.4 below is an immediate consequence of Th. 3.3.

Corollary 3.4**.**

Let $\mathcal{S}$ be the SR-automaton for the parsing table $(\mathcal{A},\mathcal{L}\mathcal{A})$ of $\mathcal{G}$. Then $\mathcal{L}(\mathcal{S})=\mathcal{L}(\mathcal{G})$.

We conclude this section by a comment on nondeterminism. As the proof of Th. 3.3 hints, the nondeterminism of parsing tables is reflected in SR-automata in a precise sense. Suppose that the state $P$ contains a conflict on $x$. If, during an execution of the SR-automaton, $P$ is on top of the state-stack when the current word is $w$, then there are two distinct ways to reach a configuration for the word $wx$ by going along the distinct branches outgoing $P$.

4 Ambiguity detection

In this section, we will present the proposed strategy for ambiguity detection.

The activity is carried on alternating two sorts of phases: guessing and validation. In the guessing phase, relying upon an approximation of SR-automata, we identify words – if any – that might show the ambiguity of the grammar. In the subsequent phase, we validate the paths associated with these words against proper executions of SR-automata.

A grammar $\mathcal{G}$ is ambiguous iff there exists a word in $\mathcal{L}(\mathcal{G})$ that has two distinct rightmost derivations, or, equivalently, two distinct leftmost derivations. The next result, that underpins the proposed detection strategy, characterizes ambiguity in terms of executions of SR-automata.

Below, given any configuration $\mathcal{C}=\langle h,\,s,\,w,\,t\rangle$, we say that two execution steps from $\mathcal{C}$ are in conflict on $x$ to mean that P=\mbox{{\rm{top}}({s})} has a conflict on $x$ and one of the following scenarios apply: (i) both the execution steps are inferred by rule (R) and depend, respectively, on some $\tau_{sr}(P,[x]:{R^{\prime}}:{p^{\prime}})$ and on some $\tau_{sr}(P,[x]:{R^{\prime\prime}}:{p^{\prime\prime}})$ such that $p^{\prime}\neq{p^{\prime\prime}}$; (ii) one of the execution steps is inferred by rule (S) and depends on $\tau_{sr}(P,x)$, and the other is inferred by rule (R) and depends on some $\tau_{sr}(P,[x]:{R}:{p})$.

Theorem 4.1**.**

Let $\mathcal{S}$ be the SR-automaton for the parsing table $(\mathcal{A},\mathcal{L}\mathcal{A})$ of $\mathcal{G}$. Also, let $P_{I}$ be the initial state of $\mathcal{S}$, and $\tau_{sr}$ be its transition function. Then $\mathcal{G}$ is ambiguous iff $w$ exists such that $\langle\epsilon,\,[{P_{I}}],\,\epsilon,\,[{}]\rangle\rightsquigarrow^{*}\mathcal{C}$ and \mathcal{C}\rightsquigarrow\mathcal{C}^{\prime}\rightsquigarrow^{*}\langle\epsilon,\,s_{1},\,w\,,t_{1}\rangle$and$\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime\prime}\rightsquigarrow^{}\langle\epsilon,,s_{2},,w$,,t_{2}\rangle$for some$s_{1},t_{1}$,$s_{2},t_{2}$,$\mathcal{C},\mathcal{C}^{\prime},\mathcal{C}^{\prime\prime}$such that$\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime}$and$\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime}$are in conflict on$x$.*

Proof**.**

(If) If $\mathcal{G}$ is ambiguous then there exists $w\in\mathcal{L}(\mathcal{G})$ that has two distinct rightmost derivations. Hence by Th. 3.3, letting $P_{I}$ be the initial state of $\mathcal{S}$, \langle\epsilon,\,[{P_{I}}],\,\epsilon,\,[{}]\rangle\rightsquigarrow^{*}\langle\epsilon,\,s_{1},\,w\,,t_{1}\rangle$and$\langle\epsilon,,[{P_{I}}],,\epsilon,,[{}]\rangle\rightsquigarrow^{}\langle\epsilon,,s_{2},,w$,,t_{2}\rangle$for some$s_{1},s_{2},t_{1},t_{2}$with$t_{1}\neq t_{2}$. By$t_{1}\neq t_{2}$, the two executions above must differ at least for one step inferred by the$(R)$-rule. Since both executions lead to configurations with the same word-component, the steps of the two executions are inferred from transitions of the SR-automaton involving the same sequence of symbols in$T\cup\mbox{\{\}}. Hence, the two executions must be made of zero or more equal steps up to a configuration with a state $P$ at the top of the state-stack that contains a conflict on some $x$. From that configuration, the two executions must continue with distinct steps that are in conflict on $x$.

(Only if) By Cor. 3.4, $w\in\mathcal{L}(\mathcal{G})$, and by Th. 3.3 both $t_{1}$ and $t_{2}$ represent derivation trees for $w$. It remains to show that $t_{1}\neq t_{2}$. Assume $\mathcal{C}=\langle h,\,s,\,w_{1},\,t\rangle$. If both $\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime}$ and $\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime\prime}$ are inferred by the (R) rule, then the production-stacks of $\mathcal{C}^{\prime}$ and of $\mathcal{C}^{\prime\prime}$ are obtained by pushing distinct productions on $t$. Nothing is popped out of production-stacks during execution, hence the thesis. Suppose now that $\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime}$ is inferred by the (S) rule, and $\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime\prime}$ by the (R) rule, and let $A\rightarrow\beta$ be the production involved in the inference of $\mathcal{C}\rightsquigarrow\mathcal{C}^{\prime\prime}$. Then, $w$ has the form $w^{\prime}_{1}w^{\prime\prime}_{1}$ for some $w^{\prime\prime}_{1}$ that is the frontier of the subtree rooted at $A$ in the tree described by $t_{2}$. This is not the case for $w^{\prime\prime}_{1}$ in the tree represented by $t_{1}$. Hence $t_{1}\neq t_{2}$.*

The labelled transition relations defined below are used to get approximations of the language recognized by SR-automata.

Definition 4.2**.**

Let $\mathcal{S}$ be the SR-automaton for the parsing table $(\mathcal{A},\mathcal{L}\mathcal{A})$ of $\mathcal{G}$. Also, let $\tau_{sr}$ be the transition function of $\mathcal{S}$. For every pair of states $P$ and $Q$ of $\mathcal{S}$, $P\mathrel{\buildrel x\over{\longrightarrow}}Q$ iff $\tau_{sr}(P,x)=Q$, and $P\mathrel{\buildrel[x]\over{\longrightarrow}}Q$ iff $\tau_{sr}(P,[x]:{R}:{p})=Q$ for some $R$ and some $p$. Also, $\mathrel{\buildrel x\over{\Longrightarrow}}$ stands for \mathrel{{\buildrel[x]\over{\longrightarrow}}^{\lower 6.0pt\hbox{\scriptstyle{}}}}\mathrel{\buildrel x\over{\longrightarrow}}, and $\mathrel{\buildrel w\over{\Longmapsto}}$ stands for $\mathrel{\buildrel x_{1}\over{\Longrightarrow}}\ldots\mathrel{\buildrel x_{j}\over{\Longrightarrow}}$ for $w=x_{1}\ldots{x_{j}}$.*

To detect ambiguity, we analyze one conflict at a time, and look for words that are accepted along paths taking either branch out of the conflict state. The analysis is applied to all the conflicts of the SR-automaton and searching for longer and longer words, up to the point that either we can conclude that the grammar is ambiguous or unambiguous, or a fixed bound on the length of the searched words is reached. When analyzing a certain conflict of state $P$, we assume that all the conflicts of the states other than $P$ are switched off by applying a combination of resolutions for them. If the analysis of the conflict of $P$ is inconclusive, the analysis is retried for a different combination of resolutions for the other conflicts.

The search for words that might have distinct derivations is carried on alternating guessing and validation phases as described below. In the guessing phase, we make use of the function ${\rm{guess}}({P},{Q},{l})$ that returns the set of words $w$ shorter than $l$ and such that $P\mathrel{\buildrel w\over{\Longmapsto}}Q$. The validation phase checks whether an execution meeting specified requirements exists. If an execution from $\mathcal{C}$ to $\mathcal{C}^{\prime}$ exists, where $\mathcal{C}^{\prime}$ is a configuration with $P$ at the top of its state-stack and with $w$ as word-component, then the invocation of ${\rm{validate}}({\mathcal{C}},{w},{P})$ returns $\mathcal{C}^{\prime}$, otherwise it returns failure.

For clarity, we first describe the main principles of the analysis of a single conflict. Then we comment on how inconclusive searches are handled. We assume that the SR-automaton at hand has initial state $P_{I}$, and final state $P_{F}$. Also, we let $\mathcal{C}_{0}=\langle\epsilon,\,[{P_{I}}],\,\epsilon,\,[{}]\rangle$, and let $l_{1},l_{2}$ be integers. We first consider the case that the state $P$ has an r/r conflict for $x$. By Th. 4.1, we focus on pairs of paths with the following shape

[TABLE]

where $Z_{1}$ and $Z_{2}$ are inferred by transitions of the automaton involving $[x]$ and two distinct productions $p_{1}$ and $p_{2}$. We notice here that there are as many plausible instances of $Z_{i}$ meeting the above requirements as the size of ${\rm{opening}}(p_{i},P)$. To save on validation failures, we operate as follows.

For each $R$ such that R\mathrel{{\buildrel[x]\over{\longrightarrow}}^{\lower 6.0pt\hbox{\scriptstyle{*}}}}P, we invoke ${\rm{guess}}({P_{I}},{R},{l_{1}})$. So, we can collect a set of triples $(P_{I},w_{1},R)$ such that $P_{I}\mathrel{\buildrel w_{1}\over{\Longmapsto}}R$. Call GR such set. 2. 2.

For each triple $(P_{I},w_{1},R)$ in GR, we invoke ${\rm{validate}}({\mathcal{C}_{0}},{w_{1}},{R})$. Call VR the set of configurations obtained in this way. We use VR to decide which are the most appropriate targets to consider among the $[x]$-transitions outgoing $P$ in (1). To do that, we select the configurations in VR that can undergo the following manipulation. We attempt to prolong the execution from each configuration in VR by performing zero or more steps driven by the (R) rule under $[x]$ so to reach a configuration with $P$ on top of the state-stack. Then, by executing steps driven by the (R) rule for $p_{1}$ and, resp., by the (R) rule for $p_{2}$, we get configurations with $Z_{i}$ on top of the state-stack, with $i=1,2$. Next, we extend these executions further by means of zero or more steps driven by the (R) rule under $[x]$, and then by a step driven by the (S) rule for $x$. So, from those configurations in VR which can be extended as described above, we obtain pairs of configurations reachable from $\mathcal{C}_{0}$ that have $w_{1}{x}$ as word-component and $Q_{i}$ at the top of their state-stacks. Call VQs the set of these pairs. 3. 3.

For each pair $(\mathcal{C}_{1},\mathcal{C}_{2})$ in VQs we do the following. Suppose $Q_{i}$ is on top of the state-stack of $\mathcal{C}_{i}$. For each w^{\prime}\in\mbox{{\rm{guess}}({Q_{1}},{P_{F}},{l_{2}})}, we check whether $Q_{2}\mathrel{\buildrel w^{\prime}\over{\Longmapsto}}P_{F}$. If so, we run both ${\rm{validate}}({\mathcal{C}_{1}},{w^{\prime}},{P_{F}})$ and ${\rm{validate}}({\mathcal{C}_{2}},{w^{\prime}},{P_{F}})$. If both validations are successful, then the returned configurations have word-components $w_{1}{x}w^{\prime}$ with w^{\prime}=w_{2}\$$ for some w_{2}$. Also, their production-stacks represent two distinct derivation trees for$w_{1}{x}w_{2}$. Hence the grammar is ambiguous.

Above, we streamlined the search strategy. It remains to comment on the scenarios that induce us either to retry the analysis with longer words, or to give up, or to conclude that the grammar is unambiguous. They are identified as follows. If either $GR$ or $VR$ or $VQs$ is empty, and if $l_{1}$ can be increased further, then we try again from the beginning searching longer guesses for $w_{1}$. Analogously, if either ${\rm{guess}}({Q_{1}},{P_{F}},{l_{2}})$ is empty, or no w^{\prime}\in\mbox{{\rm{guess}}({Q_{1}},{P_{F}},{l_{2}})} is such that $Q_{2}\mathrel{\buildrel w^{\prime}\over{\Longmapsto}}P_{F}$, or no w^{\prime}\in\mbox{{\rm{guess}}({Q_{1}},{P_{F}},{l_{2}})} can be validated from both $\mathcal{C}_{1}$ and $\mathcal{C}_{2}$, then we can reuse $VQs$ and retry with longer guesses for $w_{2}$. This is reasonable, however, only under some circumstances. Indeed, if all the possible guesses for $w_{1}$ and for $w_{2}$ have been computed (and hence all the possible instances of $R$, $Z_{1}$ and $Z_{2}$ have been considered), and if either the analyzed conflict is the single conflict of the grammar, or analogous circumstances apply to all the conflicts of the grammar, then we conclude that the grammar is unambiguous.

In case the state $P$ has an s/r conflict for $x$, the relevant pairs of paths have the following shape

[TABLE]

and the analysis is carried on analogously to the case of an r/r conflict. Shortly, we compute guesses for $w_{1}$ from $P_{I}$ to $R$, then we validate the guesses against proper executions from $P_{I}$ to $R$, and get extensions to $Q_{1}$ and to $Q_{2}$. Next, we compute guesses for $w_{2}$ from $Q_{1}$ to $P_{F}$, then check whether they could, at least approximately, be matched from $Q_{2}$. If so, we run the validations for $w_{2}$ from configurations whose state-stacks have $Q_{1}$ and $Q_{2}$ at their top.

We conclude the section by playing the proposed strategy for the s/r conflict on $\mathop{+}$ in state $5$ of the SR-automaton for $\mathcal{G}_{1}$ (Fig. 1). Using the naming in (2), $R$ ranges over $\{1,5\}$. For $l_{1}=4$, we get

GR=\mbox{{a,a\mathop{+}a}}

and, by validation,

$VR=\{\langle{\epsilon},{[{0,1}]},{a},{[{}]}\rangle,\langle{\epsilon},{[{0,2,4,1}]},{a\mathop{+}a},{[{p_{2}}]}\rangle\}$.

The manipulation of $\langle\epsilon,\,[{0,1}],\,a,\,[{}]\rangle$ fails, and we are left with

$VQs=\{(\langle\epsilon,\,[{0,2,4,5,4}],\,a\mathop{+}a\mathop{+},\,[{p_{2},p_{2}}]\rangle,\langle\epsilon,\,[{0,2,4}],\,a\mathop{+}a\mathop{+},\,[{p_{2},p_{2},p_{1}}]\rangle)\}$.

Next, we compute guesses for $l_{2}=l_{1}$ from state $4$ to state $3$. We obtain a\$$ and run its validations from the configurations paired in VQs$. By that, we get

\langle{\epsilon},{[{0,2,3}]},{a\mathop{+}a\mathop{+}a\},{[{p_{2},p_{2},p_{2},p_{1},p_{1}}]}\rangle$, and$\langle{\epsilon},{[{0,2,3}]},{a\mathop{+}a\mathop{+}a$},$${[{p_{2},p_{2},p_{1},p_{2},p_{1}}]}\rangle$

that show the ambiguity of $\mathcal{G}_{1}$.

5 Conclusions

Starting from LR parsing tables, we defined SR-automata, and used them to describe a conflict-driven strategy to detect grammar ambiguity. Through prospective symbols, lookaheads are accommodated on the edges of SR-automata. This feature was crucial to mine words in the language as paths on labelled graphs.

The reported strategy showed to be a quite handy way of reasoning about the ambiguity of small grammars of scholarly size. The assessment of its effectiveness for large grammars, as well as comparisons with other detection methods, is subject to further investigation. Other directions for future work are relative to possible applications of SR-automata in testing the adequacy of the heuristics used by parser generators to handle nondeterministic grammars.