Decidability of DPDA equivalence

Colin Stirling Division of Informatics University of Edinburgh

email: cps@dcs.ed.ac.uk

Abstract

A proof of decidability of equivalence between deterministic pushdown automata is presented using a mixture of methods developed in concurrency and language theory. The technique appeals to a tableau proof system for equivalence of configurations of strict deterministic grammars.

1 The DPDA problem

Ingredients of pushdown automata with ε-transitions are a finite set of states P, a finite set of stack symbols S, a finite alphabet A and a finite family of basic transitions, each of the form pS ⟶^{a} qα where p, q are states, a ∈ A ∪ {ε}, S is a stack symbol and α is a sequence of stack symbols. A configuration of an automaton is any expression pα, p ∈ P and α ∈ S^{∗} whose behaviour is determined by the basic transitions together with the following prefix rule, where β ∈ S^{∗}:

if pS ⟶^{a} qα then pSβ ⟶^{a} qαβ

The language accepted by a configuration pα is {w ∈ A^{∗} : ∃q ∈ P. pα ⟶^{w} qϵ} where the extended transitions for words are defined as expected. Note that ε-transitions are swallowed in the usual fashion. Acceptance is by empty stack (and not by final state, see [5]).

A deterministic pushdown automaton, DPDA, has restrictions on its basic transitions (where pS ⟶^{a} abbreviates pS ⟶^{a} qα for some q and some α)

if pS ⟶^{a} qα and pS ⟶^{a} rβ then q = r and α = β

if pS ⟶^{a} and a ∈ A then not(pS ⟶^{ε})

Moreover one can assume that in a basic transition pS ⟶^{a} qα the length of α is less than 3, and that ε-transitions can only pop the stack: if pS ⟶^{ε} qα then

\begin{matrix}pX ⟶^{a} pX & pX ⟶^{b} pϵ & pX ⟶^{c} pX & rX ⟶^{ϵ} pϵ \\ pY ⟶^{a} pϵ & pY ⟶^{b} rϵ & pY ⟶^{c} pY Y & rY ⟶^{ϵ} rϵ \end{matrix}

Figure 1: A DPDA

α = ϵ. One consequence of the restrictions is that the language accepted by a configuration is prefix-free: if w is accepted then no proper prefix of w is accepted. Thus if ϵ is accepted then no other word is. In the following we assume ϵ-free DPDAs^{1}. Figure 1 depicts a simple DPDA whose basic transitions are listed under the diagram.

The DPDA decidability problem was first posed in 1966 [2]. Is there an effective procedure for deciding whether or not two configurations of a DPDA accept the same language?^{2} Why is the decision question so difficult to answer, despite all the intensive work on the problem over the past 30 years? Because one needs to expose the right structure. It appears that the notation of pushdown configurations, although simple, is not rich enough. Attempts to prove the result (such as Valiant’s technique) examine differences between stack lengths and potentially equivalent configurations. This method showed decidability of equivalence for real-time DPDAs which have no ϵ-transitions [7]. But when there are ϵ-transitions it is possible for configurations of arbitrary size to be equivalent. For example configurations pY^{n}X and pY^{m}X of Figure 1 are equivalent for all m and n. Finally Sénizergues [8] showed decidability. However his proof is formidable and is over 100 pages long [9]. It exposes structure in DPDAs using power series which leads to quite difficult notation.

Instead we provide a proof using a mixture of techniques developed in concurrency theory for showing decidability of bisimulation equivalence and ideas from language theory, especially those developed in [4]. The proof also essentially depends on insights gained from trying to understand Sénizergues’s method. The proof consists of two semi-decision procedures. One half of the proof is easy: if two configurations do not accept the same language then there is a smallest word which distinguishes them. Therefore we just need to establish semi-decidability of accepting the same language. The crux of this part of the proof is that there is a finite tableau proof that two configurations are equivalent. The method employs ideas developed in [6, 1, 10]. It relies upon exposure of structure within DPDA, so that we can “decompose” configurations. We shall build a structured language (almost a process algebra) for describing configurations of a DPDA using strict deterministic grammars.

1Classical DPDAs have final states, but for any language L recognised by a configuration of such a DPDA there is a configuration of an ϵ-free DPDA with empty stack acceptance for the language L$ where $ is an endmarker.

2As the disjoint union of two DPDAs is a DPDA, we can assume the decision question over configurations of a single DPDA instead of between two different DPDAs.

2 Strict deterministic grammars

An ϵ-free context-free grammar in 3-Greibach normal form consists of a finite family N of nonterminals, a finite alphabet A and a finite family of basic transitions, each of the form X ⟶^{a} α where X ∈ N, a ∈ A and α ∈ N^{∗} such that its length, |α|, is less than 3. A simple configuration is a sequence of nonterminals whose behaviour is determined by the basic transitions and the prefix rule: if X ⟶^{a} α then Xβ ⟶^{a} αβ where β ∈ N^{∗}. The language accepted by a simple configuration is the set of words {w ∈ A^{∗} : α ⟶^{w} ϵ}. However we shall also consider composite configurations which are finite families of simple configurations. We use the (process calculus) notation α_{1} + … + α_{n} for such a configuration. The language accepted by a composite configuration is the union of the languages accepted by its components.

We are interested in a restricted family of context-free grammars, the strict deterministic grammars [3, 4]. Assume a context-free grammar (in 3-Greibach normal form). Let ≡ be a partition of its nonterminals N. We extend ≡ to sequences of nonterminals, α ≡ β if α = β or there is a δ such that α = δXα_{1} and β = δY β_{1} and X ≡ Y and X ≠ Y. The partition ≡ on N is strict if the basic transitions obey the following two conditions:

if X ⟶^{a} α and Y ⟶^{a} δ and X ≡ Y then α ≡ δ

if X ⟶^{a} α and Y ⟶^{a} α and X ≡ Y then X = Y

An immediate consequence of these conditions is that if X ⟶^{a} ϵ and X ≡ Y and X ≠ Y then not(Y ⟶^{a}). A context-free grammar is strict deterministic if there exists a strict partition of its nonterminals.

We now examine some properties of strict deterministic grammars. First the strictness conditions generalise to words (see [4] for a proof).

Fact 1 i. If X ⟶^{w} α and Y ⟶^{w} δ and X ≡ Y then α ≡ δ.

ii. If X ⟶^{w} α and Y ⟶^{w} α and X ≡ Y then X = Y.

Therefore if X ≡ Y then the languages accepted by X and Y are prefix-disjoint and if X ≠ Y then they accept disjoint languages (again see [4] for a proof).

Fact 2 If X ≡ Y and X ⟶^{w} ϵ then i. not(Y ⟶^{u} ϵ) for any proper prefix u of w, and ii. not(Y ⟶^{w} ϵ) when X ≠ Y.

Our main concern is with a subset of composite configurations. A composite configuration β_{1} + … + β_{n} is admissible if β_{i} ≡ β_{j} for each pair of components β_{i} and β_{j}. For ease of notation we also assume that the empty sum, ∅, is admissible. In [4] admissible configurations are called “associates”. Notice that if X ≡ Y then for any w the sum ∑{β : X ⟶^{w} β or Y ⟶^{w} β} is admissible. Moreover “reachability” under any word preserves admissibility (yet again see [4] for a proof).

Fact 3 If β_{1} + … + β_{n} is admissible then for any w the following is admissible

∑{β′_{1} : β_{1} ⟶^{w} β′_{1}} + … + ∑{β′_{n} : β_{n} ⟶^{w} β′_{n}}

An ϵ-free DPDA can be transformed into an equivalent 3-Greibach normal form strict deterministic grammar (and vice versa) [3]. For every pair of states p, q and stack symbol S introduce a nonterminal [pSq] (whose language will be {w ∈ A^{∗} : pS ⟶^{w} qϵ}). The basic transitions for a ∈ A are also translated: pS ⟶^{a} qϵ becomes [pSq] ⟶^{a} ϵ, pS ⟶^{a} qT becomes the family for each r, [pSr] ⟶^{a} [qT r], and pS ⟶^{a} qT U becomes the family for each r and p′, [pSr] ⟶^{a} [qT p′][p′Ur]. Erase all ϵ-nonterminals (if pS ⟶^{ε} qϵ then [pSq] is an ϵ-nonterminal) from the right hand side of any transition. Next delete all transitions involving redundant nonterminals (those which accept no words). It is easy to check that the partition ≡ relating pairs [pSq] and [pSr] is strict. A configuration pS_{1}S_{2} … S_{n} of a DPDA becomes the following admissible configuration, where the summation is over all p_{i}, 1 ≤ i ≤ n

∑[pS_{1}p_{1}][p_{1}S_{2}p_{2}] … [p_{n−1}S_{n}p_{n}]

after all ϵ-nonterminals are erased and all components involving redundant nonterminals are removed.

An example is the translation of the DPDA of Figure 1 into a strict deterministic grammar. First the basic transitions are transformed as follows.

[pXp] ⟶^{a} [pXp]  [pXr] ⟶^{a} [pXr]  [pXp] ⟶^{b} ϵ
[pXp] ⟶^{c} [pXp]  [pXr] ⟶^{c} [pXr]
[pY p] ⟶^{a} ϵ [pY r] ⟶^{b} ϵ [pY p] ⟶^{c} [pY p][pY p]
[pY p] ⟶^{c} [pY r][rY p] [pY r] ⟶^{c} [pY p][pY r] [pY r] ⟶^{c} [pY r][rY r]

There are also two ϵ-nonterminals, [rXp] and [rY r]. These are erased from the right hand side of any transition: the transition [pY r] ⟶^{c} [pY r][rY r] is changed to [pY r] ⟶^{c} [pY r]. There are also two redundant nonterminals [pXr] and [rY p]. All transitions involving these nonterminals are removed. This reduces the transitions to the following

[pXp] ⟶^{a} [pXp]  [pXp] ⟶^{b} ϵ  [pXp] ⟶^{c} [pXp]
[pY p] ⟶^{a} ϵ  [pY r] ⟶^{b} ϵ  [pY p] ⟶^{c} [pY p][pY p]
[pY r] ⟶^{c} [pY p][pY r] [pY r] ⟶^{c} [pY r]

The set of nonterminals is {[pXp], [pY p], [pY r]} and the partition is into the sets {{[pXp]}, {[pY p], [pY r]}}. An example configuration pY Y X of the DPDA becomes the following admissible configuration

[pY p][pY p][pXp] + [pY p][pY r] + [pY r]

The DPDA problem is equivalent to the question of decidability of (language) equivalence between admissible configurations of a strict deterministic grammar. Therefore we now extend the transition relation to admissible configurations. The idea is as in process calculi that one builds transitions from a composite process out of transitions of its components. First the basic transitions are determinized by coalescing all the basic transitions of a nonterminal with the same label: if X ⟶^{a} α_{1} and … and X ⟶^{a} α_{n} then form the single transition X ⟶^{a} α_{1}+…+α_{n}^{3}. We also assume that if not(X ⟶^{a}) then X ⟶^{a} ∅. Consequently for each nonterminal X and each a ∈ A there is a single transition rule X ⟶^{a} ∑ α_{j}. For instance the rule for [pY r] and c above becomes [pY r] ⟶^{c} [pY p][pY r]+[pY r]. The transition rule for admissible configurations, the prefix rule, is then as follows.

if X_{i} ⟶^{a} ∑ α_{ij} then ∑ X_{i}β_{i} ⟶^{a} ∑ ∑ α_{ij}β_{i}

For example the admissible configuration corresponding to pY Y X above has the following c transition

[pY p][pY p][pXp] + [pY p][pY r] + [pY r]
↓ c
[pY p][pY p][pY p][pXp] + [pY p][pY p][pY r] + [pY p][pY r] + [pY r]

The resulting configuration corresponds to pY Y Y X.

The extended transition relation ⟶^{w}, w ∈ A^{∗}, is defined as usual. Consequently the language accepted by an admissible configuration β_{1} + … + β_{k} is the set of words {w : β_{1} +…+β_{k} ⟶^{w} ϵ}. The rest of the paper is devoted to the proof of decidability of language equivalence between admissible configurations. In the next section we introduce some useful notation. In section 4 we isolate crucial combinatorial properties of admissible configurations which underpin the tableau proof system for showing decidability in section 5.

3By strictness α_{1} + … + α_{n} is admissible.

3 Measures, shapes and recursive nonterminals

Assume a fixed strict deterministic grammar in 3-Greibach normal form without redundant nonterminals. We use α, β, … to range over sequences of nonterminals and E, F, G, … to range over admissible configurations. The size of E, written |E|, is the length of its longest sequence of nonterminals: if E is β_{1} + … + β_{n} then |E| is max{|β_{j}| : 1 ≤ j ≤ n}^{4}. Notice that for each n there are only finitely many admissible configurations of size n.

We assume a fixed total ordering on the alphabet A. From this we define a total ordering on words: u < v if |u| < |v| or when |u| = |v| u is lexicographically less than v. If u < v we say that u is shorter than v. For each nonterminal X there is a unique shortest word u such that X ⟶^{u} ϵ. We let w(X) denote this word and we let the norm of X, written n(X), be its length. An important measure is M which is just larger than the maximum norm.

M = 1 + max {n(X) : X is a nonterminal }

The notion of norm extends to admissible configurations: n(E) is the length of the shortest word u such that E ⟶^{u} ϵ^{5}. Infinitely many different admissible configurations can have the same norm (and this is one reason why the decision problem is difficult).

An admissible configuration has a variety of “shapes” as it can be presented in many different ways using the following (obvious) equalities.

\begin{aligned}E + ∅ & = & E & ∅E & = & ∅ \\ E(F + G) & = & EF + EG & (E + F)G & = & EG + F G \end{aligned}

One basic shape is “head nonterminal form” X_{1}G_{1} + … + X_{k}G_{k} where X_{i} ≠ X_{j}, i ≠ j, and X_{i} ≡ X_{j}: some of the G_{i}s may be ϵ. In this case the X_{i}s are the “heads” and the G_{i}s are the “tails”. Another important head form is β_{1}G_{1}+…+β_{n}G_{n}+E′ where β_{i} ≡ β_{j} (and β_{i} ≠ β_{j}, i ≠ j) and |β_{i}| = |β_{j}| and G_{i} is not ϵ, and |E′| ≤ |β_{i}|. Instead one may focus on “tail” forms. If X_{i} ⟶^{w} E_{i} for each i : 1 ≤ i ≤ k (where some E_{i}s may be ∅) then X_{1}G_{1} + … + X_{k}G_{k} ⟶^{w} E_{1}G_{1} + … + E_{k}G_{k}. The shape E_{1}G_{1} + … + E_{k}G_{k} highlights the tails. Because the grammar is in 3-Greibach normal form |E_{i}| ≤ 1 + |w| for each i. In this example the “head” E_{1} + … + E_{k} is itself admissible. Tail forms E_{1}G_{1} + … + E_{k}G_{k} are only permitted when the “head” is admissible. For instance [pY p][pY p][pXp] + [pY p][pY r] + [pY r] is not permitted to have as tail form [pY p]G_{1} + ([pY p] + ϵ)G_{2}. However it does have the form [pY p]G_{1} + [pY r]G_{2}.

Another useful notation is “the result of E after u”, written E · u. This is the configuration F such that E ⟶^{u} F, which can be ∅. An example is (X_{1}G_{1} + … + X_{n}G_{n}) · w(X_{i}) = G_{i}. If |u| < min{n(E_{i}) : 1 ≤ i ≤ k} then (E_{1}G_{1} + … + E_{k}G_{k}) · u = (E_{1} · u)G_{1} + … + (E_{k} · u)G_{k}.

4We let |∅| = 0.

5We assume n(∅) = ∞.

Although the starting point is a fixed strict deterministic grammar we shall extend it with auxilary nonterminals, ranged over by V, each of which has an associated definition V =^{def} H. We say that (V_{1}, …, V_{n}) is a family of recursive nonterminals if for each i : 1 ≤ i ≤ n either V_{i} =^{def} H_{i1}V_{1} + … + H_{in}V_{n} where H_{i1}+…+H_{in} is admissible and each H_{ij} is distinct and does not contain auxilary nonterminals, or V_{i} =^{def} V_{j} and j ≤ i and V_{j} =^{def} V_{j}. An auxilary nonterminal can only appear as a final element in a sequence of nonterminals. Admissibility is extended to such families of sequences as follows. A configuration which is a singleton V is admissible, and β_{1}V′_{1}+…+β_{k}V′_{k} is admissible if the head β_{1}+…+β_{k} is admissible and each β_{j} is distinct, and there is a family of recursive nonterminals (V_{1}, …, V_{n}) such that each V′_{i} is one of the V_{j}s. An admissible configuration can therefore be presented in tail form E_{1}V_{1} + … + E_{n}V_{n}. We assume that |V | = 1 for each recursive nonterminal V.

The transition rules are extended to the wider class of admissible configurations with the following rule

if E ⟶^{w} V_{i} and V_{i} =^{def} H then E ⟶^{w} H

The definition of E · u is refined so that it is always unique: if E ⟶^{u} V_{i} and V_{i} =^{def} H then E · u = H. Consequently if E · u = V_{i} then V_{i} =^{def} V_{i}. The language accepted by an extended configuration E is the set {w : (E · w) = V_{i}}. We view a recursive nonterminal V_{i} such that V_{i} =^{def} V_{i} as a terminating nonterminal. The norm of E, n(E), is again the length of the smallest word accepted by E. In the sequel we are only interested in normed configurations. This implies that in a recursive family (V_{1}, …, V_{n}) there is at least one terminating nonterminal.

Two configurations E and F are equivalent, written E ∼ F, if they accept the same language and, when applicable, agree on terminating recursive nonterminals. If E and F are normed then E and F accept the same language iff they “reject” the same words, and because the language accepted by a configuration is prefix-free it follows that E ∼ F iff for all words w

(E · w) = ∅ iff (F · w) = ∅ and (E · w) = V_{i} iff (F · w) = V_{i}

Later we use this consequence as the criterion for equivalence of configurations. Below are some obvious properties of equivalence, including congruence.

Fact 1

i. If E ∼ F then for all u ∈ A^{∗}, E · u ∼ F · u. ii. If E ∼ E′ and F ∼ F′ then E + F ∼ E′ + F′. iii. If EF ∼ G and F ∼ F′ then EF′ ∼ G. iv. If EF ∼ G and E ∼ E′ then E′F ∼ G. v. If E ∼ F then n(E) = n(F).

The family (V′_{1}, …, V′_{n}) of recursive nonterminals refines the family (V_{1}, …, V_{n}) when the following two conditions hold.

if V_{i} =^{def} H_{1}V_{1} + … + H_{n}V_{n} then V′_{i} =^{def} H_{1}V′_{1} + … + H_{n}V′_{n}

if V_{i} =^{def} V_{j} and V′_{i} =^{def} H then V′_{j} =^{def} H

A refined family agrees on the definitions of nonterminating nonterminals and preserves equality of definitions, but may contain fewer terminating nonterminals. Because equivalence of configurations includes agreement of terminating recursive nonterminals, equivalence is preserved by refinement.

Fact 2 If E_{1}V_{1} + … + E_{n}V_{n} ∼ F_{1}V_{1} + … + F_{n}V_{n} and (V′_{1}, …, V′_{n}) refines (V_{1}, …, V_{n}) then E_{1}V′_{1} + … + E_{n}V′_{n} ∼ F_{1}V′_{1} + … + F_{n}V′_{n}.

Equivalence can be “approximated”. For n ≥ 0 we say that E and F are n-equivalent, written E ∼_{n} F, if for all words w whose length |w| ≤ n

(E · w) = ∅ iff (F · w) = ∅ and (E · w) = V_{i} iff (F · w) = V_{i}

Note that for each n it is decidable whether E ∼_{n} F. Moreover E ∼ F iff E ∼_{n} F for all n ≥ 0. Below are some routine properties of the approximants ∼_{n}.

Fact 3 i. If E ∼_{n} F then for all u ∈ A^{∗} where |u| ≤ n, E · u ∼_{n−|u|} F · u. ii. If E ∼_{n} F and 0 ≤ m < n then E ∼_{m} F. iii. If E ∼_{n} F and F ≁_{n} G then E ≁_{n} G. iv. If E ∼_{n} E′ and F ∼_{n} F′ then E + F ∼_{n} E′ + F′. v. If EF ∼_{n} G and E ∼_{n} E′ then E′F ∼_{n} G.

4 Imbalance and size

Consider trying to show that E ∼ F. One approach is goal directed. Start with the goal E = F (to be understood as, “is E ∼ F?”) and then reduce it to subgoals. Keep reducing to further subgoals until one reaches either obviously true subgoals (such as G = G) or obviously false subgoals (such as G = H when n(G) ≠ n(H)). This naive technique which is described more formally in terms of tableaux in the next section is the approach adopted.

Assume that E has shape E_{1}G_{1} + … + E_{n}G_{n} and that F has similar shape F_{1}G_{1} + … + F_{n}G_{n}. The measure of “imbalance” between E and F with these shapes is max { |E_{i}|, |F_{i}| : 1 ≤ i ≤ n}. An important step in the proof is that one can bound imbalance by reducing goals to balanced subgoals.

Proposition 1 If X_{1}H_{1} + … + X_{k}H_{k} ∼ F and E_{1}H_{1} + … + E_{k}H_{k} ∼ F′ then E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})) ∼ F′. Proof: Let E be X_{1}H_{1} + … + X_{k}H_{k}. Assume E ∼ F and E_{1}H_{1} + … + E_{k}H_{k} ∼ F′. Since (E · w(X_{i})) = H_{i} it follows that H_{i} ∼ (F · w(X_{i})). By congruence E_{1}H_{1} + … + E_{k}H_{k} ∼ E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})), see Fact 1 of the previous section. □

Proposition 1 will be used to reduce imbalance. Let X_{1}H_{1} + … + X_{k}H_{k} = F

and E_{1}H_{1} + … + E_{k}H_{k} = F′ be two goals where X_{1} + … + X_{k} ⟶^{w} E_{1} + … + E_{k},

F ⟶^{w} F′, |w| = M and n(F′) > 0. Therefore |E_{i}| ≤ M + 1 for each i. If F contains recursive nonterminals then it has head form β_{1}G_{1} + … + β_{n}G_{n} where |β_{i}| = M + 1 and G_{i} ≠ ϵ or |β_{i}| < M + 1 and G_{i} is a recursive nonterminal V_{j}. If F does not contain recursive nonterminals then it has a similar head form β_{1}G_{1} + … + β_{n−1}G_{n−1} + JG_{n} where |β_{i}| = M + 1 and |J| < M + 1 and G_{n} = ϵ. Assume that F does not contain recursive nonterminals (the other case is almost similar). Let (β_{i} ·w) be F′_{i} and (J ·w) be F′_{n} and therefore |F′_{i}| ≤ 2M +1 for each i. Because F′ = F ·w the second goal is E_{1}H_{1} +…+E_{k}H_{n} = F′_{1}G_{1} +…+F′_{n}G_{n}. If the two starting goals are true then Proposition 1 justifies reduction to the subgoal

E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})) = F′_{1}G_{1} + … + F′_{n}G_{n}

Because |w(X_{i})| < M for each i, the left hand side configuration has the following matrix form

E_{1}(β_{1} · w(X_{1}))G_{1} + … + E_{1}(J · w(X_{1}))G_{n} +
⋮  ⋮
E_{k}(β_{1} · w(X_{k}))G_{1} + … + E_{k}(J · w(X_{k}))G_{n}

where |E_{i}(β_{j} · w(X_{i}))| ≤ 3M + 2, and |E_{i}(J · w(X_{i}))| < 3M + 2. Collecting terms together the subgoal therefore has the tail form E′_{1}G_{1} + … + E′_{n}G_{n} = F′_{1}G_{1} + … + F′_{n}G_{n} where the maximum imbalance is 3M + 2.

Next we need to show that introducing balanced subgoals is “sound” (there is a fuller discussion of soundness in the next section). The next Proposition shows that if the starting goals are not true then falsity is preserved when introducing a balanced subgoal.

Proposition 2 If n ≥ m and m ≥ M − 1 and E_{1}H_{1} + … + E_{k}H_{k} ≁_{n−m} F′ and X_{1}H_{1} + … + X_{k}H_{k} ∼_{n} F then E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})) ≁_{n−m} F′.

Proof: Assume n ≥ m ≥ M − 1 and X_{1}H_{1} + … + X_{k}H_{k} ∼_{n} F. Therefore H_{i} ∼_{n−|w(X_{i})|} (F · w(X_{i})). Because |w(X_{i})| ≤ M − 1, H_{i} ∼_{n−m} (F · w(X_{i})). Therefore E_{1}H_{1} + … + E_{k}H_{k} ∼_{n−m} E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})). Assume E_{1}H_{1} + … + E_{k}H_{k} ≁_{n−m} F′. By Fact 3 iii of the previous section the result follows. □

Bounding imbalance between configurations is not enough for showing decidability. The sizes of subgoals may keep growing. The next and crucial step in the argument is a mechanism for controlling size. It is at this point that we appeal to recursive nonterminals. The balanced goal,

(1) E_{1}G_{1} + … + E_{n}G_{n} = F_{1}G_{1} + … + F_{n}G_{n}

where the E_{i}s and F_{i}s do not contain recursive nonterminals, can be reduced to a subgoal of the form

(2) E_{1}V_{1} + … + E_{n}V_{n} = F_{1}V_{1} + … + F_{n}V_{n}

where (V_{1}, …, V_{n}) is a family of recursive nonterminals. The mechanism for reducing goal (1) to goal (2) involves constructing the recursive family (V_{1}, …, V_{n}) from a subsidary family of goals, E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} = F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} where i ≥ 1, with the same tails as (1).

Proposition 3 If k ≥ 1 and E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼ F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} for each i : 1 ≤ i ≤ k and every E_{j}^{i} and F_{j}^{i} does not contain recursive nonterminals then there is a family of recursive nonterminals (V_{1}, …, V_{n}) such that

1. E_{1}^{i}V_{1} + … + E_{n}^{i}V_{n} ∼ F_{1}^{i}V_{1} + … + F_{n}^{i}V_{n} for each i : 1 ≤ i ≤ k,

2. if V_{i} =^{def} H_{1}V_{1} + … + H_{n}V_{n} then G_{i} ∼ H_{1}G_{1} + … + H_{n}G_{n}.

3. if V_{i} =^{def} V_{j} then G_{i} ∼ G_{j}.

Proof: The proof proceeds by iteratively refining families of recursive nonterminals for each E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼ F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} in order starting with i = 1. Let E be E_{1}^{1}G_{1} + … + E_{n}^{1}G_{n} and let F be F_{1}^{1}G_{1} + … + F_{n}^{1}G_{n}. For the base case V_{i}^{0} =^{def} V_{i}^{0}, 1 ≤ i ≤ n. Clearly 2 and 3 hold for each V_{i}^{0}. Assume that the jth family (V_{1}^{j}, …, V_{n}^{j}), j ≥ 0, is given and that 2 and 3 hold for each V_{i}^{j}. Let E′ be E_{1}^{1}V_{1}^{j} + … + E_{n}^{1}V_{n}^{j} and let F′ be F_{1}^{1}V_{1}^{j} + … + F_{n}^{1}V_{n}^{j}. If E′ ∼ F′ then we have dealt with the first equation. Now let E be E_{1}^{2}G_{1} + … + E_{n}^{2}G_{n} and F be F_{1}^{2}G_{1}+…+F_{n}^{2}G_{n} and let E′ be E_{1}^{2}V_{1}^{j}+…+E_{n}^{2}V_{n}^{j} and let F′ be F_{1}^{2}V_{1}^{j}+…+F_{n}^{2}V_{n}^{j}. If E′ ∼ F′ then we have dealt with the second equation too. We keep repeating this until either all the equations are exhausted (and then (V_{1}^{j}, …, V_{n}^{j}) is the required family of recursive nonterminals) or E is E_{1}^{l}G_{1} + … + E_{n}^{l}G_{n} and F is F_{1}^{l}G_{1} + … + F_{n}^{l}G_{n} and E′ is E_{1}^{l}V_{1}^{j} + … + E_{n}^{l}V_{n}^{j} and and F′ is F_{1}^{l}V_{1}^{j} + … + F_{n}^{l}V_{n}^{j} and E′ ≁_{k} F′ for a least k. Let u be the smallest distinguishing word for E′ and F′. There are two possibilities. First that one and only one of (E′ · u) and (F′ · u) is ∅. Second is that just one of this pair is a particular terminating nonterminal V_{i}^{j}. We show below that the first possibility is impossible because E ∼ F. In the case of the second possibility we refine the family of recursive nonterminals to (V_{1}^{j+1}, …, V_{n}^{j+1}) where each V_{i}^{j+1} obeys conditions 2 and 3. By Fact 2 of section 3, E_{1}^{i}V_{1}^{j+1} +…+E_{n}^{i}V_{n}^{j+1} ∼ F_{1}^{i}V_{1}^{j+1} +…+F_{n}^{i}V_{n}^{j+1} for all i < l. Hence we continue the construction for E is E_{1}^{l}G_{1} +…+E_{n}^{l}G_{n} and F be F_{1}^{l}G_{1} +…+F_{n}^{l}G_{n} and E′ is E_{1}^{l}V_{1}^{j+1} + … + E_{n}^{l}V_{n}^{j+1} and F′ is F_{1}^{l}V_{1}^{j+1} + … + F_{n}^{l}V_{n}^{j+1}.

We now examine the case when E′ ≁_{k} F′ and u = a_{1} … a_{k} is the smallest distinguishing word. Consider the following four sequences when Z is E′, F′, E and F respectively

(Z · a_{1}), …, (Z · a_{1} … a_{i}), …, (Z · a_{1} … a_{k})

Consider the initial part of the sequence in the case Z is E′ up to the first prefix, if there is one, u_{1} = a_{1} … a_{m} such that Z ·u_{1} = E′′ where E′′ = H_{1}V_{1}^{j} +…+H_{n}V_{n}^{j}

and (E′ · a_{1} … a_{m−1}) ⟶^{a_{m}} V_{i}^{j}. From 2 we know that G_{i} ∼ H_{1}G_{1} + … + H_{n}G_{n}

because V_{i}^{j} =^{def} E′′. The initial part of the sequence when Z is E up to E · a_{1} … a_{m−1} is similar to the initial part for Z is E′ in that they have the same “heads”. Consequently E ·u_{1} = G_{i}. Therefore the sequence for Z is E is updated from position m to k. Let E · a_{1} … a_{s}, for s ≥ m, be (H_{1}G_{1} + … + H_{n}G_{n}) · a_{m+1} … a_{s}. This updating restores the same heads in the two sequences Z is E and Z is E′ until the next occurrence of a G_{i′} in the updated sequence for Z is E. We repeatedly update the new sequence for Z is E whenever there is a

later position E′ · a_{1} … a_{t} = H′_{1}V_{1}^{j} + … + H′_{n}V_{n}^{j} and V_{i′}^{j} =^{def} H′_{1}V_{1}^{j} + … + H′_{n}V_{n}^{j}

and E · a_{1} … a_{t} in the (updated) sequence is G_{i′} for t < k. The same updating construction is applied to the sequences when Z is F′ and Z is F. Note that repeated updating of the sequences for E and F does not affect the property that their corresponding positions are equivalent.

The final positions of the sequences for E′ and F′ are the elements E′ · u and F′ · u. If one of them is ∅ then one of the final positions of the updated sequences for E and F is also ∅, which would contradict that E ∼ F. Therefore one of them is a terminating recursive nonterminal V_{i}^{j}. Without loss of generality assume that E′ · u = V_{i}^{j}. Consider the final element of the updated sequence for E. It is either G_{i} or G_{t} when V_{t}^{j} =^{def} V_{i}^{j} (and i ≤ t). In the second case by 2, G_{t} ∼ G_{i}. Consider now the final element F′ · u.

The first case is that F′ · u is H′_{1}V_{1}^{j} + … + H′_{n}V_{n}^{j} and in the updated sequence F · u is H′_{1}G_{1} + … + H′_{n}G_{n} (where no H_{i} is ϵ). Because E ∼ F it follows that G_{i} ∼ H′_{1}G_{1} + … + H′_{n}G_{n}. The family (V_{1}^{j}, …, V_{n}^{j}) is refined to (V_{1}^{j+1}, …, V_{n}^{j+1}) as follows. First V_{i}^{j+1} =^{def} H′_{1}V_{1}^{j+1} + … + H′_{n}V_{n}^{j+1}. Next for any index t such that V_{t}^{j} =^{def} V_{i}^{j} let V_{t}^{j+1} =^{def} H′_{1}V_{1}^{j+1} + … + H′_{n}V_{n}^{j+1}. For the other entries we merely update the index j to j + 1 on the V_{i}^{j}s on both sides of =^{def}. By construction properties 2 and 3 both hold for the new family (V_{1}^{j+1}, …, V_{n}^{j+1}).

The second case is that F′ · u = V_{i′}^{j}. Therefore the final element F · u in the updated sequence is either G_{i′} or G_{t′} such that G_{t′} ∼ G_{i′} where V_{t′}^{j} =^{def} V_{i′}^{j} and i′ ≤ t′. Because E′ · u = V_{i}^{j} we know that i ≠ i′ since u distinguishes E′ and F′. However G_{i} ∼ G_{i′} because E ∼ F. Consider min{i, i′}. Without loss of generality assume it is i′. The refined family of recursive nonterminals (V_{1}^{j+1}, …, V_{n}^{j+1}) is defined as follows. First V_{i}^{j+1} =^{def} V_{i′}^{j+1}. Secondly for any index t such that V_{t}^{j} =^{def} V_{i}^{j} let V_{t}^{j+1} =^{def} V_{i′}^{j+1}. For the rest of the entries we just update the index j to j + 1 as in the first case. By construction, properties 2 and 3 hold for the new family of recursive nonterminals.

The stages of the construction produce a sequence of families of recursive nonterminals (V_{1}^{0}, …, V_{n}^{0}), …, (V_{1}^{j}, …, V_{n}^{j}), … where each family refines the previous family. The final step in the proof is that the iteration must terminate by stage n − 1. At each stage j exactly one terminating nonterminal V_{i}^{j} is directly refined. Other elements V_{t}^{j} when V_{t}^{j} =^{def} V_{i}^{j} and t > i may also be refined. No element V_{i}^{k} with index i is directly refined more than once. Therefore by stage n − 1 the iteration must terminate with the family (V_{1}^{n−1}, …, V_{n}^{n−1}). Now it is a simple argument that if property 1 does not hold by stage n − 1 then afterall E ≁ F for the then current E and F. □

The recursive family (V_{1}, …, V_{n}) as constructed in the proof of Proposition 3 is said to be “canonical” for the family E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} = F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} of true goals. The construction of canonical nonterminals is independent of the tails G_{i}.

Fact 1 If (V_{1}, …, V_{n}) is canonical for E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼ F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} then it is also canonical for the family E_{1}^{i}J_{1} + … + E_{n}^{i}J_{n} ∼ F_{1}^{i}J_{1} + … + F_{n}^{i}J_{n}, where i : 1 ≤ i ≤ k.

The assembly of a canonical family proceeds in stages. Each recursive family (V_{1}^{j+1}, …, V_{n}^{j+1}) refines (V_{1}^{j}, …, V_{n}^{j}). As the construction must terminate by stage j = n − 1, at most n of the goals E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} = F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} are used in the refinement process. The other goals play no role. The building of the V_{i}^{j+1}s from the V_{i}^{j}s appeals to the smallest distinguishing word u_{j+1} for E′ ≁ F′ (when E′ is E_{1}^{l}V_{1}^{j} +…+E_{n}^{l}V_{n}^{j} and F′ is F_{1}^{l}V_{1}^{j} +…+F_{n}^{l}V_{n}^{j}). We have no insight as to the upper bound on |u_{j+1}|. For instance it is not determined by the maximum norm of the heads E_{i}^{l} and F_{i}^{l}. Indeed this turns out to be the reason why the procedure for equivalence of the next section is only semi-decidable.

Next we wish to show that introducing canonical recursive nonterminals is “sound” for a family of goals (see the next section for a fuller discussion of soundness). We need to consider how to introduce recursive nonterminals when the family of goals need not all be true. The idea is to approximate canonicity by defining when a recursive family (V_{1}, …, V_{n}) is “canonical to depth d” where d ≥ 0, for a family of goals E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} = F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} when E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼_{m} F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} for m > d for each i. The construction is the same as in Proposition 3, except that we stop at the first stage j ≥ 0 with (V_{1}^{j}, …, V_{n}^{j}) as the required family of recursive nonterminals if the sum of the distinguishing words s_{j} = |u_{1}| + … + |u_{j}| is no larger than d, and E′ ∼_{d−s_{j}} F′ for the current E′ and F′. A goal E = F is “m-true” if E ∼_{m} F. Given m it is decidable whether a finite family of goals are m-true. Furthermore given d < m it is decidable whether family (V_{1}, …, V_{n}) is canonical to depth d for a finite family E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼_{m} F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n}. If (V_{1}, …, V_{n}) is canonical to depth d for a family of goals which are m-true then it is also canonical to depth d for that family for any k > m, provided they are k-true. Being canonical to depth d is independent of the tails: if (V_{1}, …, V_{n}) is canonical to depth d for E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼_{m} F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} then it is also canonical to depth d for the family E_{1}^{i}J_{1} + … + E_{n}^{i}J_{n} ∼_{m} F_{1}^{i}J_{1} + … + F_{n}^{i}J_{n} with the same heads but different tails. Moreover if (V_{1}, …, V_{n}) is canonical for a family of (true) goals then there is a smallest d for which it is canonical to depth d. This motivates the next result, which guarantees that introduction of recursive nonterminals is “sound”.

Proposition 4 If 0 < k < n and 0 < d < m and (V_{1}, …, V_{n}) is canonical to depth d for the family of goals E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} = F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} where E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼_{m} F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} for each i : 1 ≤ i ≤ k, and E_{1}G_{1} + … + E_{n}G_{n} ≁_{m−d} F_{1}G_{1} + … + F_{n}G_{n} then E_{1}V_{1} + … + E_{n}V_{n} ≁_{m−d} F_{1}V_{1} + … + F_{n}V_{n}.

Proof: Assume (V_{1}, …, V_{n}) is canonical to depth d where d < m for the family of goals E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} = F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n}, and that E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼_{m} F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n} for each i : 1 ≤ i ≤ k. By construction of the canonical nonterminals to depth d, it follows that if V_{i} =^{def} H_{1}V_{1} + … + H_{n}V_{n} then G_{i} ∼_{m−d}

H_{1}G_{1}+…+H_{n}G_{n} and if V_{i} =^{def} V_{j} then G_{i} ∼_{m−d} G_{j}. Next assume that E ≁_{m−d} F

when E is E_{1}G_{1} + … + E_{n}G_{n} and F is F_{1}G_{1} + … + F_{n}G_{n}, but E′ ∼_{m−d} F′ when E′ is E_{1}V_{1} + … + E_{n}V_{n} and F′ is F_{1}V_{1} + … + F_{n}V_{n}. Consider the smallest word u = a_{1} … a_{k} which distinguishes E and F. Note that E · a_{1} … a_{i} ≁_{m−(d+i)} F · a_{1} … a_{i} and E′ · a_{1} … a_{i} ∼_{m−(d+i)} F′ · a_{1} … a_{i}. Consider the following four sequences when Z is E, F, E′ and F′: (Z · a_{1}), … (Z · a_{1} … a_{k′}) where either k′ = k or k′ < k and the final elements for the sequences for Z is E′ and F′ is a terminating nonterminal V_{i}. The idea is as in the proof of Proposition 3 to update the sequences for Z is E and Z is F so that they have the same heads as as those for Z is E′ and Z is F′. Consider the initial prefix u_{1} = a_{1} … a_{i} of Z is E′, if there is one, such that Z · u_{1} = E′′ and E′′ = H_{1}V_{1} + … + H_{n}V_{n} and (E′ · a_{1} … a_{i−1}) ⟶^{a_{i}} V_{j}. Hence E · u_{1} = G_{j}. Because V_{j} =^{def} E′′ the following hold: G_{j} ∼_{m−d} H_{1}G_{1} + … + H_{n}G_{n} and E · u_{1} = G_{j} ≁_{m−(d+i)} F · u_{1}. Therefore by Fact 3 iii of section 3, H_{1}G_{1} + … + H_{n}G_{n} ≠_{m−(d+i)} F · u_{1}. Therefore the sequence for Z is E is updated from position i to k′: E · a_{1} … a_{s}, s > i, becomes (H_{1}G_{1} + … + H_{n}G_{n}) · a_{i+1} … a_{s}. This updating restores the same heads in the two sequences for Z is E and Z is E′ until the next occurrence of a G_{i′} in the first sequence in which case we then again update it. The same updating construction is applied to the sequence Z is F using Z is F′. The repeated updating of the sequences for E and F does not affect the property that their corresponding positions j are inequivalent at m − (d + j). Consider now the final elements in the updated sequences for E and F. The first case is that one and only one of the elements is ∅, but then one and only one of the corresponding elements in the sequences for E′ and F′ is also ∅ which is a contradiction. The second case is that one of the elements, say in the sequence for E, is a terminating recursive nonterminal U_{j}, which means that some G_{i} is U_{j}. But then the corresponding element in the sequence for E′ is also a terminating nonterminal V_{i} (because G_{i} ∼_{m−d} H iff H is G_{i}). Therefore the corresponding element in the sequence for F′ is also V_{i} and so the final element in the sequence for F is U_{j} as well. □

5 Tableaux

The proof of decidability is completed by presenting a tableau proof system for demonstrating equivalence of admissible configurations. The proof system is goal directed and consists of two kinds of rules, “simple” and “conditional”. Simple rules have the form

\frac{Goal}{Subgoal_{1} … Subgoal_{n}} C

where Goal is what currently is to be proved and the subgoals are what it reduces to, provided the side condition C holds. A conditional rule has the form

Goal_{1}

⋮ Goal_{k}

⋮  C

Goal Subgoal

where Goal is the current goal to be shown and there is a single subgoal to which it reduces provided that the goals Goal_{1},…,Goal_{k} occur above Goal on the path between it and the root (starting goal) and provided that the side condition C holds. Goals and subgoals are all of the form E = F where E and F are (normed) admissible configurations which may contain recursive nonterminals.

There is also the important notion of when a current goal counts as final. Final goals are classified as either successful or unsuccessful. A tableau proof for a starting Goal is a finite proof tree, whose root is Goal and all of whose leaves are successful final goals, and all of whose inner subgoals are the result of an application of one of the rules. It is our intention to show that E ∼ F iff there is a tableau proof for E = F.

There is one simple rule UNF presented in Figure 2. A goal E = F reduces UNF

\frac{E = F}{E · a_{1} = F · a_{1} … E · a_{k} = F · a_{k}} A = \{a_{1}, …, a_{k}\}

Figure 2: Simple tableau rule

to the subgoals E ·a_{i} = F ·a_{i} for each a_{i} ∈ A. UNF obeys local completeness and soundness. Completeness is that if the goal is true then so are all the subgoals. This is clear from Fact 1 i of section 3. Soundness is that if all the subgoals are true then so is the goal, or equivalently if the goal is false then so is at least one of the subgoals. A finer version uses approximants, which provide a measure of how false a goal E = F is. Consider the smallest n such that E ≁_{n} F. For UNF if the goal is false at n + 1, E ≁_{n+1} F, then at least one of the subgoals is false at n, E · a ≁_{n} F · a, see Fact 3 i of section 3.

The conditional rules are given in Figure 3. The BAL rules introduce “balance” between goals, and CUT introduces recursive nonterminals. Completeness for BAL is that if the premise goals (those above the subgoal) are true then so is the subgoal which follows from Proposition 1 of the previous section. The statement of completeness for CUT is that there are correct applications of it. If (V_{1}, …, V_{n}) is canonical for the first k premises then there is a depth d for which it is canonical. Moreover (V_{1}, …, V_{n}) needs to be a recursive family for the true goal E_{1}G_{1} + … + E_{n}G_{n} = F_{1}G_{1} + … + F_{n}G_{n}, in which case the subgoal follows^{6}.

For soundness of the conditional rules consider global soundness of the proof system. The overall idea is that if there is a successful tableau whose root is false then there is a path through the tableau within which each subgoal is false. The idea is refined using approximants. If the root is false then there is an offending path (of false goals) through the tableau within which the approximant indices decrease whenever rule UNF has been applied, and hence this would mean that a successful final goal is false (which, as we shall show, is impossible). Soundness of the conditional rules is that if the premises are on an offending path then the subgoal preserves the falsity index of the goal immediately above it. In the case of BAL(R) assume that the offending path passes through the premise goals. There is a least n such that for the initial premise F ∼_{n} X_{1}H_{1} + … + X_{k}H_{k} and F ≁_{n+1} X_{1}H_{1} + … + X_{k}H_{k}. As there are exactly M applications of UNF between the initial and final premise it follows that F′ ∼_{n−M} E_{1}H_{1} + … + E_{k}H_{k}. However, as this is the offending path F′ ≁_{(n−M)+1} E_{1}H_{1} +…+E_{k}H_{k}. Therefore by Proposition 2 of the previous section F′ ≁_{(n−M)+1} E_{1}(F ·w(X_{1}))+…+E_{k}(F · w(X_{k})). The same argument proves soundness of BAL(L). There is a similar BAL(R)

6If (V_{1}, …, V_{n}) is canonical for the first k premises and E_{1}V_{1}+…+E_{n}V_{n} ≁ F_{1}V_{1}+…+F_{n}V_{n} then (V_{1}, …, V_{n}) can be refined to (V′_{1}, …, V′_{n}) so it is canonical for all the premises. Because there can only be at most n − 1 refinements, eventually CUT will be applicable if goals with the common tails G_{i} persist: see the later discussion.

F = X_{1}H_{1} + … + X_{k}H_{k}
⋮  C_{1}
F′ = E_{1}H_{1} + … + E_{k}H_{k}
F′ = E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k}))

BAL(L)

X_{1}H_{1} + … + X_{k}H_{k} = F
⋮  C_{1}
E_{1}H_{1} + … + E_{k}H_{k} = F′
E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})) = F′

where C_{1} is the condition

1. There are precisely M applications of UNF between the top goal and the bottom goal, and no application of any other rule.

CUT

E_{1}^{1}G_{1} + … + E_{n}^{1}G_{n} = F_{1}^{1}G_{1} + … + F_{n}^{1}G_{n}
⋮
E_{1}^{k}G_{1} + … + E_{n}^{k}G_{n} = F_{1}^{k}G_{1} + … + F_{n}^{k}G_{n}
⋮  C_{2}
E_{1}G_{1} + … + E_{n}G_{n} = F_{1}G_{1} + … + F_{n}G_{n}
E_{1}V_{1} + … + E_{n}V_{n} = F_{1}V_{1} + … + F_{n}V_{n}

where C_{2} is the condition

1. No E_{j}^{i} or F_{j}^{i} contains recursive nonterminals.

2. (V_{1}, …, V_{n}) is canonical to depth d for the goals E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} = F_{1}^{i}G_{1} + … + F_{n}^{i}G_{n}, 1 ≤ i ≤ k and k ≤ n.

3. There are at least d + 1 applications of UNF between the goal E_{1}^{k}G_{1} + … + E_{n}^{k}G_{n} = F_{1}^{k}G_{1} + … + F_{n}^{k}G_{n} and E_{1}G_{1} + … + E_{n}G_{n} = F_{1}G_{1} + … + F_{n}G_{n} (as well as possibly other rules).

Figure 3: Conditional tableau rules Successful final goals

E = F
⋮  UNF
⋮  at least once
1. E = E  2. E = F

Unsuccessful final goals

1. E = F when n(E) ≠ n(F)

2. V_{i} = V_{j} when i ≠ j and V_{i} =^{def} V_{i}, and V_{j} =^{def} V_{j}

Figure 4: Final goals

argument for CUT. Consider m > d such that E_{1}^{i}G_{1} + … + E_{n}^{i}G_{n} ∼_{m} F_{1}^{i}G_{1} + …+F_{n}^{i}G_{n} for each i : 1 ≤ i ≤ k and E_{1}^{k}G_{1}+…+E_{n}^{k}G_{n} ≁_{m+1} F_{1}^{k}G_{1}+…+F_{n}^{k}G_{n}. There are at least d+1 applications of UNF between the kth premise and the final premise of the rule, and so as this is an offending path E_{1}G_{1} + … + E_{n}G_{n} ≁_{m−d} F_{1}G_{1} + … + F_{n}G_{n}. Therefore by Proposition 4, E_{1}V_{1} + … + E_{n}V_{n} ≁_{m−d} F_{1}V_{1} + … + F_{n}V_{n}.

Final goals are presented in Figure 4. Unsuccessful goals are clearly false. A final goal is successful if it is either an identity or a repeat. An offending path of false goals with decreasing falsity indices cannot include either kind of successful goal. Clearly it is not possible for E ≁_{m} E. For the other case, suppose the offending path passes through E = F twice. At the first instance there is an m, E ∼_{m} F and E ≁_{m+1} F, but as there is at least one application of UNF between the two occurrences this would imply that E ≁_{m} F, which is a contradiction.

The first main result is that a successful tableau for E = F indeed constitutes a proof that E ∼ F.

Theorem 1 If there is a successful tableau for E = F then E ∼ F.

Proof: Suppose there is a successful tableau for E = F but E ≁ F. Then there is a least n such that E ≁_{n} F. We now construct an offending path of false goals through the tableau within which the approximant indices decrease whenever UNF is applied. But this is impossible, for we must reach a successful final goal as the tableau is finite. □

More intricate is the proof of the converse of Theorem 1, that if E ∼ F then there is a successful tableau for E = F. Given a true goal one applies the rules, preserving truth, according to the strategy described below. It is therefore not possible to reach an unsuccessful final goal. Thus the main issue is how to guarantee that the tableau construction is finite. We show that on any infinite path of goals developed using the strategy there must be infinitely many successful final goals.

We start with a simple observation.

(1) For any m ≥ 0, there are only finitely many different goals E = F (whose recursive nonterminals belong to (V_{1}, …, V_{n})) with |E| ≤ m and |F | ≤ m.

If F has recursive nonterminals in the family (V_{1}, …, V_{n}) then we let rec(F) be the size of the largest definition in the family, max{|H| : V_{i} =^{def} H}. The next observation tells us how much a configuration can increase in size through an application of UNF.

(2) For any a, |E · a| ≤ max{rec(E), |E| + 1}.

The size of an application of BAL is the size of the configuration F in the initial goal of the rule (see Figure 3), and the application is said to use the configuration F. The resulting subgoal contains the configuration E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})). E_{i} is a “head” of an application and (F · w(X_{i})) is a “tail”. The size of a head is bounded, |E_{i}| ≤ M + 1 (using (2)). Moreover because E_{1} + … + E_{k} is itself admissible if E_{i}(F · w(X_{i})) ⟶^{u} (F · w(X_{i})) then (E_{j}(F · w(X_{j})) · u) = ∅ for j ≠ i. A further observation about BAL (which uses (2)) is as follows.

(3) If E′ = F′ is the result of an application of BAL of size m then configurations |E′|, |F′| ≤ k + 2M, where k = max{m, rec(E′)}.

A configuration F without recursive nonterminals is “small” if |F | ≤ M^{2} + 4M +1, and F with recursive nonterminals is small if |F | ≤ rec(F)+M^{2}+4M +1. The strategy is to apply the BAL rules wherever possible when the sizes of their applications are small, and otherwise to apply UNF. The rule CUT is not applied. Any infinite path of goals containing infinitely many small applications of BAL, and no application of CUT, must therefore contain infinitely many final goals (“repeats”) by properties (3) and (1).

Next suppose there is an application of BAL which uses a large F of size m. The strategy is to build a “block”. Assume that it is an application of BAL(L).

F
⋮ BAL(L)
(∗) E_{1}(F · w(X_{1})) + … + E_{k}(F · w(X_{k})) = F′

F is the “root configuration” of the block and (∗) is its “root goal” (which will also be a potential root, the initial premise, of an application of CUT). Once a block is initiated with BAL(L), the strategy is to repeatedly apply BAL(L) wherever possible, and UNF otherwise^{7}. However BAL(R) is permitted, once

F′′
⋮ BAL(L)
E′_{1}(F′′ · w(X′_{1})) + … + E′_{k′}(F′′ · w(X′_{k′})) = H
⋮ ⋮ UNFs
(F′′ · w(X′_{i})) = G_{1} = H_{1}
⋮ ⋮
G_{k} = H_{k}

Figure 5: A potential switch from BAL(L) to BAL(R)

the “tail” of an application of BAL(L) is exposed, see Figure 5. Assume an application of BAL(L) using F′′. Between its result and the goal G_{1} = H_{1} there are no further applications of BAL(L), and G_{1} is a tail of the BAL application. BAL(R) is now permitted provided it uses configuration G_{i}, i ≥ 1. BAL(R) is not permitted using a configuration from a goal above G_{1} = H_{1}. BAL(R) is not enforced, for one can still apply BAL(L). The strategy is always to apply a BAL rule whenever it is permitted. If BAL(R) is applied then the strategy is to repeatedly apply BAL(R), and to use UNF otherwise. BAL(L) is only permitted once a tail (F′′·w(X′_{i})) of an application of BAL(R) is the right hand configuration of a goal. Thus a block consists of alternating sub-blocks of BAL(L)s and UNFs and BAL(R)s and UNFs. If a later application of BAL is smaller than m then either a new block with a smaller root configuration is initiated or the size of the application is small and the earlier strategy applies.

Assume a root configuration F of size m with block root E_{1} = F_{1}. Let π be a path of goals E_{1} = F_{1}, …, E_{l} = F_{l}, … belonging to the block developed from E_{1} = F_{1} using the strategy. All applications of BAL have at least size m in this path. We show the following crucial property.

(4) For every G which is used in an application of BAL in π there is a word u such that G is (F · u) and |(F · v)| > m − (M^{2} + 3M) for all prefixes v of u.

Property (4) holds for initial root configuration F because F is F ·ϵ and |F | = m. Assume the block is initiated with a BAL(L). Consider a later application of BAL(L) using F′ (where there are no intervening applications of BAL(R)) as depicted in the left derivation of Figure 6. F′ arises from F via applications of UNF (and possibly BAL(L)). Consequently there is a word u, constructed from the applications of UNF, with F′ = (F · u), and by assumption |F′| ≥ m. For every prefix v of u, (F · v) is a configuration on the path between F and F′.

7If BAL(R) initiates the block then the strategy is to repeatedly apply BAL(R) and UNF.

F  F′
⋮ BAL(L)  ⋮ BAL(L)
E_{1} = F_{1}  E_{j} = F_{j}
⋮  ⋮
F′  (F′ · w(X_{i}))
⋮ BAL(L)  ⋮
E_{n} = F_{n}  E′
⋮  ⋮  BAL(R)
E_{l} = F_{l}
⋮

Figure 6: Showing property (4)

Assume that for one of these configurations F′′, |F′′| ≤ m − (M^{2} + 3M). There are two cases to examine.

The first case is that F′′ occurs between a configuration used for a BAL and its application (between, for example, F and F_{1} in Figure 6). The second case is that F′′ occurs at or after an application of BAL(L), between F_{1} and F′ in Figure 6. Consider the first case. There are at most M − 1 applications of UNF between F′′ and the application of BAL (because F′′ cannot be the configuration used in this application). Assume that E_{1} = F_{1} is the result of this BAL(L) which uses F and that F′ is the next configuration used in an application of BAL(L). Because |F′′| ≤ m−(M^{2} +3M) and there are at most M −1 applications of UNF between it and F_{1}, by (2) it follows that |F_{1}| ≤ m − (M^{2} + 2M + 1). Because |F′| ≥ m, there must be at least (M^{2} + 2M + 1) applications of UNF between F_{1} and F′ which are size increasing: for F_{1} must increase its size and become F′. The second case is also covered by these observations: if F′′ occurs between F_{1} and F′ then there must be at least (M^{2} + 3M) applications of UNF between F_{1} and F′ which are size increasing. However within at most M^{2} + M applications of UNF from F_{1} a tail (F · w(X_{i})) of the application of BAL(L) must occur as the left hand configuration of a goal. E_{1} has the form E′_{1}(F ·w(X_{1}))+…+E′_{k}(F ·w(X_{k})) where |E′_{i}| ≤ M + 1. Because BAL(L) does not apply between F_{1} and F′, each E′_{i}’s size must be declining. If E_{1} in head nonterminal form is Y_{1}H_{1} + … + Y_{l}H_{l} then within M applications of UNF the left hand configuration must be H_{j} for some j, and within another M applications of UNF H_{j} must lose its “head” nonterminals, and so on. Consequently within M^{2} + M applications of UNF between F_{1} and F′ a goal (F · w(X_{i})) = F_{k} has to occur. F_{1} may have increased in size in becoming F_{k} but only by M^{2} + M, and so |F_{k}| ≤ m − (M + 1). So there are still at least M + 1 applications of UNF between F_{k} and F′ which are size increasing. However BAL(R) is now permitted, and clearly it must apply between F_{k} and F′ because there must be a sequence of M UNFs where the right hand configurations are not decreasing in size. But this is a contradiction.

Next we show that property (4) continues to hold when there is a switch from BAL(L) using F′ to an application of BAL(R) using E′, pictured on the right in Figure 6. BAL(R) is only permitted when a tail (F′ · w(X_{i})) of the application of BAL(L) occurs as a left hand configuration. By assumption there is a word u such that F′ is (F · u). Therefore the tail (F′ · w(X_{i})) is (F · u w(X_{i})). There are no applications of BAL between this tail and E′, and therefore there is a word v such that E′ is (F · u w(X_{i}) v). Moreover both F′ and E′ have size at least m. Assume that for some prefix v′ of w(X_{i}) v, |F′ · v′| ≤ m − (M^{2} + 3M). There are two cases to consider. First is that v′ is a prefix of w(X_{i}), and secondly that it is a prefix of the form w(X_{i}) v′′. Because |w(X_{i})| ≤ M − 1 for the first case this means that |(F′ ·w(X_{i}))| ≤ m−(M^{2} +2M +2). Therefore there has to be at least (M^{2} + 2M + 2) applications of UNF between (F′ · w(X_{i})) and E′ which increase size, and for the second case there has to be at least M^{2} + 3M applications. However BAL(L) is still permitted between (F′ · w(X_{i})) and E′. Clearly BAL(L) must therefore apply to a configuration belonging to a goal strictly above E′ because there must be a sequence of M UNFs where the left hand configurations are not decreasing in size. But this is a contradiction.

The argument for (4) is now repeated for all further applications of BAL within π.

Using (4) we now establish a final property which shows that CUT eventually applies in a block. Assume a root configuration F of size m with block root E_{1} = F_{1}, and assume π is a path of goals belonging to this block developed using the strategy. If F does not contain recursive nonterminals then it can be written in head form β_{1}G_{1}+…+β_{n}G_{n} where |β_{i}| = (M^{2}+4M +1) or |β_{i}| < (M^{2}+4M +1) and G_{i} = ϵ. Notice that there is an upper bound on the “width” n (as it can be no more than the number of sequences of nonterminals whose length is at most M^{2} + 4M + 1). In fact we can reduce the number of tails by amalgamating them when they are the same: for instance, if G_{i} = G_{j} then we can have the expression … + (β_{i} + β_{j})G_{i} + . . .. The final property for this case of F is

(5A) The result of every application of BAL within π has the form E_{1}G_{1} + … + E_{n}G_{n} = F_{1}G_{1} + … + F_{n}G_{n} where the G_{i}s are the tails of the root configuration F.

If F does contain recursive nonterminals drawn from (U_{1}, …, U_{l}) then it has a similar head form β_{1}G_{1} + … + β_{n}G_{n} where |β_{i}| = (M^{2} + 4M + 1) and G_{i} ≠ ϵ, or |β_{i}| < (M^{2} + 4M + 1) and G_{i} is a recursive nonterminal U_{j}. This is not quite enough for stating the property, for besides the tails G_{i} we need a (bounded) number of “supplementary” tails. Consider any β_{i} with |β_{i}| < (M^{2} + 4M + 1) and let x_{1} be min{M, (M^{2} + 4M + 1) − |β_{i}|}. G_{i} is a recursive nonterminal U_{j}. If U_{j} =^{def} U_{k} then we include U_{k} as an extra tail. Otherwise U_{j} =^{def} H_{j1}U_{1}+…+H_{jl}U_{l}. We now put the right hand side definition of U_{j} into head form β_{j1}G_{j1}+…+β_{jk}G_{jk} where |β_{ji}| = x_{1} and G_{ji} ≠ ϵ or |β_{ji}| < x_{1} and G_{ji} is a recursive nonterminal. We include the G_{ji}s as extra tails. Next we iterate the construction, but for a smaller size. Consider any |β_{ji}| < x_{1} and let x_{2} = x_{1} − |β_{ji}|. Assume G_{ji} is U_{j′}. If U_{j′} =^{def} U_{k′} then include U_{k′} as an extra tail. Otherwise U_{j′} =^{def} H. Put H into head form, β′_{1}G′_{1} + … + β′_{k′}G′_{k′} where |β′_{i′}| = x_{2} and G′_{i′} ≠ ϵ or |β′_{i′}| < x_{2} and G′_{i′} is a recursive nonterminal. Include these G′_{i′}s as supplementary tails. For each β′_{i′} such that |β′_{i′}| < x_{2} repeat this construction for size x_{3} = x_{2} − |β′_{i′}|. And so on. Note that the sizes of the heads are decreasing M ≥ x_{1} > x_{2} > . . .. Let G_{1}, …, G_{n} be the primary tails of F. Here n is bounded by the number of sequences of nonterminals (excluding the recursive nonterminals) whose length is less than or equal to M^{2} + 4M + 1. Let G_{n+1}, …, G_{n+k′} be the supplementary tails. Here k′ is also bounded^{8}. Thus the “width” n + k′ is bounded. As with the earlier case we can amalgamate equivalent tails. Notice that F has head form β_{1}G_{1} + … + β_{n}G_{n} + E_{n+1}G_{n+1} + … + E_{n+k′}G_{n+k′} (where each E_{n+i} is ∅). The property corresponding to (5A) is as follows.

(5B) The result of every application of BAL within π has the form E_{1}G_{1} + … + E_{n+k′}G_{n+k′} = F_{1}G_{1} + … + F_{n+k′}G_{n+k′} where the G_{i}s are the primary and supplementary tails of the root configuration F.

Condition (5) in its two versions essentially follows from (4) and admissibility. Assume F does contain recursive nonterminals (the other case is similar but easier). The head of F, β_{1} + … + β_{n} is admissible. Each β_{i} has the form X_{1}^{i} … X_{t}^{i}. Let β_{i}^{j} be the jth suffix X_{j}^{i} … X_{t}^{i} of β_{i}. By admissibility if β_{i} ⟶^{w} β_{i}^{j} then either β_{k} ⟶^{w} β_{k}^{j} (and X_{1}^{i} … X_{j−1}^{i} is the same sequence as X_{1}^{k} … X_{j−1}^{k}) or (β_{k} · w) = ∅. Let G be used in an application of BAL in π. By property (4) G must have the form E_{1}β_{1}^{b_{1}}G_{1} + … + E_{n}β_{n}^{b_{n}}G_{n} where the head E_{1}β_{1}^{b_{1}} + … + E_{n}β_{n}^{b_{n}} is admissible, and if |β_{i}| ≥ (M^{2} +3M) then b_{i} = M^{2} +3M and if |β_{i}| < M^{2} +3M then β_{i}^{b_{i}} is ϵ. Note that for at least one |β_{i}| = (M^{2} + 4M + 1), E_{i} ≠ ∅. The result of BAL using G (assume it is BAL(L)) has the following form where |u| = M and |E′_{i}| ≤ M + 1.

(∗∗) E′_{1}(G · w(X_{1})) + … + E′_{k}(G · w(X_{k})) = (G · u)

It is at this point that we may need the supplementary tails to account for (G·u) and (G · w(X_{i})). The first case is that they only contain primary tails and have the form E′′_{1}β_{1}^{b′_{1}}G_{1} + … E′′_{n}β_{n}^{b′_{n}}G_{n} where if |β_{i}| ≥ (M^{2} + 4M) then b′_{i} is (M^{2} + 4M) and if |β_{i}| < (M^{2} + 4M) then β_{i}^{b′_{i}} is ϵ. The second case is that they “enter” a tail G_{i} when it is a recursive nonterminal and β_{i}^{b′_{i}} is ϵ: for instance, (G · u) is (U_{j} · u′) for some suffix u′ of u (and so, |u′| < M). In which case (U_{j} · u′) has the form E′′_{1}G_{n+1} + … + E′′_{k′}G_{n+k′} (where the G_{n+i}s are supplementary tails and the heads are very small, |E′′_{i}| ≤ 2M + 1). This concludes the proof of (5).

8k′ is at most the maximum of n and 2M times the number of sequences of nonterminals (not including recursive ones) whose length is less than or equal to M.

Property (5) ensures that eventually in a block CUT is applicable, and that in any infinite path containing infinitely many CUTs there are infinitely many final goals. Assume that E′_{1} = F′_{1} is the root goal of a block which is the result of BAL(L) using F. This root goal is (* *) when G is F. Assume F has recursive nonterminals (the other case is similar). Therefore from (5B) the left hand configuration has the form E_{1}G_{1} + … + E_{n+k′}G_{n+k′} where |E_{i}| ≤ M^{2} + 6M for 1 ≤ i ≤ n and |E_{i}| ≤ 3M + 2 for n < i ≤ n + k′, and the right hand configuration (F · u) has the similar form F_{1}G_{1} + … + F_{n+k′}G_{n+k′} where |F_{i}| ≤ M^{2} + 5M + 1 for 1 ≤ i ≤ n and |F_{i}| ≤ M + 1 for n < i ≤ n + k′. Many of the E_{i}s and F_{i}s may be ∅. Because both the width, n + k′, and the sizes of the “heads” are bounded, there can only be finitely many root goals (of a block) with different heads. Let (V_{1}, …, V_{n+k′}) be the canonical family of recursive nonterminals for the root goal with depth d. Consider the first application of a BAL after d + 1 applications of UNF. Assume the result is E′_{2} = F′_{2} which has the form of (5B). The size of the heads are bounded^{9}. If (V_{1}, …, V_{n+k′}) is a recursive family for this goal then CUT can be applied. Otherwise the family is refined to give a recursive family for E′_{1} = F′_{1} and E′_{2} = F′_{2} with depth d′. The argument is repeated. There can only be at most n + k′ − 1 refinements to the recursive family of nonterminals, and therefore CUT must eventually apply in a block. Moreover because there can only be finitely many roots of a block with different heads, in any infinite path with infinitely many applications of CUT there must be infinitely many final goals.

Theorem 2 If E ∼ F then there is a successful tableau for E = F.

Proof: Assume that E ∼ F. Now we keep applying the rules preserving truth using the strategy described above. If goals are small then one keeps applying BAL(L), BAL(R) and UNF. Otherwise one tries to build a block and apply CUT. By preserving truth it is not possible to reach an unsuccessful final goal. Also it is not possible to become stuck, as UNF is always applicable unless a goal is final. Hence the only issue is that the tableau construction goes on forever. Assume that there is a an infinite path through the tableau. If CUT is only applied finitely often on this path then consider the subsequence after its final application. All attempts to build a block are thwarted, and therefore infinitely often there are small goals and so infinitely often there are final goals. Consequently CUT must be applied infinitely often. However by the analysis above any application of CUT is bounded independently of the tails and therefore we must introduce the same family of recursive nonterminals infinitely often to goals with the same heads, and therefore there must be infinitely many final goals. □

9The largest head in the root goal has size M^{2} + 6M. Let G be the resulting goal after d + 1 applications of UNF. There can be at most d + 1/M applications of BAL between the root and G. From the argument for (4) if BAL does not apply within M^{2} + M applications of UNF after G then both BAL rules are permitted, and if it still does not apply then the size of the configurations in the goals must be diminishing. Thus, as a crude measure, there is an upper bound of 2M^{2} + (d + k)M where k is a constant in the size of the heads in E′_{2} = F′_{2} when it has the form in (5B).

6 Conclusion

We have provided a manageable proof of decidability of equivalence between DPDAs. However because the procedure consists of two semi-decision procedures we are unable to provide a complexity bound. More work is needed to see if we can find a useful bound on the depth d for a canonical family of recursive nonterminals.

An intriguing open question is whether there is a more general class of contextfree grammars than the strict deterministic for which language equivalence is decidable.

The proof technique developed in this paper can also be applied to decision problems for bisimulation equivalence. Language equivalence and bisimulation equivalence coincide in the deterministic case (provided there is no redundancy). In particular the technique developed here can be used to extend the result in [10] to all pushdown processes.

Acknowledgement: I am deeply indebted to Olaf Burkart and Didier Caucal for numerous discussions about DPDA, and to Geraud Sénizergues for explanations of his result.

References

[1] Christensen, S., Hüttel, H., and Stirling, C. (1995). Bisimulation equivalence is decidable for all context-free processes. Information and Computation, 121, 143-148.

[2] Ginsberg, S., and Greibach, S. (1966). Deterministic context-free languages. Information and Control, 620-648.

[3] Harrison, M. (1978). Introduction to Formal Language Theory, Addison-Wesley.

[4] Harrison, M., Havel, I., and Yehudai, A. (1979). On equivalence of grammars through transformation trees. Theoretical Computer Science, 9, 173-205.

[5] Hopcroft, J., and Ullman, J. (1979). Introduction to Automata Theory, Languages, and Computation, Addison-Wesley.

[6] Hüttel, H., and Stirling, C. (1991). Actions speak louder than words: proving bisimilarity for context free processes. Proceedings 6th Annual Symposium on Logic in Computer Science, IEEE Computer Science Press, 376-386.

[7] Oyamaguchi, M., Honda, N., and Inagaki, Y. (1980). The equivalence problem for real-time strict deterministic languages. Information and Control, 45, 90-115.

[8] Sénizergues, G. (1997). The equivalence problem for deterministic pushdown automata is decidable. Lecture Notes in Computer Science, 1256, 671-681.

[9] Sénizergues, G. (1998). L(A) = L(B)? Tech. Report LaBRI, Université Bordeaux I, pp. 1-166. (Submitted to Theoretical Computer Science.)

[10] Stirling, C. (1998). Decidability of bisimulation equivalence for normed pushdown processes. Theoretical Computer Science, 195, 113-131.