Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time

TL;DR

This paper introduces a new polynomial-time decision procedure for equivalence of separated non-nested attribute systems, extending previous results to partial transducers and string-parameterized transducers.

Contribution

It presents an alternative polynomial-time algorithm for deciding equivalence, improving upon previous methods and extending applicability to more general transducer models.

Findings

New polynomial-time decision procedure for transducer equivalence

Extension to partial transducers and string-parameterized transducers

Improved efficiency over previous methods

Abstract

In 1982, Courcelle and Franchi-Zannettacci showed that the equivalence problem of separated non-nested attribute systems can be reduced to the equivalence problem of total deterministic separated basic macro tree transducers. They also gave a procedure for deciding equivalence of transducer in the latter class. Here, we reconsider this equivalence problem. We present a new alternative decision procedure and prove that it runs in polynomial time. We also consider extensions of this result to partial transducers and to the case where parameters of transducers accumulate strings instead of trees.

Equations

$$\begin{array}[]{lcl}q_{0}(g(x_{1},x_{2}))&\ \to&+(q(x_{1},z),q^{\prime}(x_{2},p(z)))\\ q(f(x_{1},x_{2}),y)&\ \to&+(r(x_{2},y),q(x_{1},s(y)))\\ q^{\prime}(f(x_{1},x_{2}),y)&\ \to&+(r(x_{1},y),q^{\prime}(x_{2},p(y)))\\ \phi(i,y)&\ \to&*(i,\text{EXP}(3,y))\quad\text{for }i\in\{0,1,2\},\phi\in\{q,q^{\prime},r\}\end{array}$$

$$q(f(x_1,\dots ,x_k),y_1,\dots ,y_l)\to T$$

$$\begin{array}[]{lll}T&{::=}&a(T_{1},\ldots,T_{m})\mid q^{\prime}(x_{i},T_{1},\ldots,T_{n})\mid y_{j}\end{array}$$

$$[[q]]:{\mathcal{T}}_{\Sigma }\times {\mathcal{T}}_{\Delta }^l\to {\mathcal{T}}_{\Delta }$$

$$[[q]](f(t_1,\dots ,t_k),\underline{S})$$

$$[[a(T_1,\dots ,T_m)]]\underline{t}\underline{S}$$

$$[[y_j]]\underline{t}\underline{S}$$

$$[[q^{\prime }(x_i,T_1,\dots ,T_l)]]\underline{t}\underline{S}$$

$$\begin{array}[]{lll}T&{::=}&a(T_{1},\ldots,T_{m})\mid y_{j}\mid q^{\prime}(x_{i},T^{\prime}_{1},\ldots,T^{\prime}_{n})\\ T^{\prime}&{::=}&b(T^{\prime}_{1},\ldots,T^{\prime}_{m^{\prime}})\mid y_{j}\end{array}$$

$$q(g(x_1,x_2),y)\to +(q(x_1,y),q^{\prime }(x_2,p(y))).$$

$$q^{\prime }(g(x_1,x_2),y)\to +(\ast (0,\text{EXP}(3,y)),\ast (0,\text{EXP}(3,y))).$$

$$\begin{array}[]{rclr}q(f(x_{1},x_{2}),y)&\to&+(*(r(x_{2},y),\text{EXP}(3,y)),q(x1,s(y)))&\text{ and}\\ q^{\prime}(f(x_{1},x_{2}),y)&\to&+(*(r(x_{1},y),\text{EXP}(3,y),q^{\prime}(x_{2},p(y))).\end{array}$$

$$\begin{array}[]{lll}\llbracket(M,A)\rrbracket(t)&=&p[\llbracket q_{1}\rrbracket(t,\underline{T_{1}}),\ldots,\llbracket q_{m}\rrbracket(t,\underline{T_{m}})]\\ &=&p[\llbracket q^{\prime}_{1}\rrbracket(t,\underline{T^{\prime}_{1}}),\ldots,\llbracket q^{\prime}_{m}\rrbracket(t,\underline{T^{\prime}_{m}})]\\ &=&\llbracket(M^{\prime},A^{\prime})\rrbracket(t).\end{array}$$

$$\begin{array}[]{lll@{\qquad}lll}q(a,y_{1},y_{2})&\to&g(y_{1})&q^{\prime}(a,y^{\prime}_{1},y^{\prime}_{2})&\to&g(y^{\prime}_{2})\end{array}$$

$$\begin{array}[]{lclr}\displaystyle\Psi_{b,q}^{(h)}(z)=\bigwedge_{b(f\underline{x})\to(b_{1},\ldots,b_{k})}&\displaystyle\bigwedge_{q(f\underline{x},\underline{y})\rightarrow y_{j}}&\displaystyle(z\doteq y_{j})&\wedge\\ &\displaystyle\bigwedge_{q(f\underline{x},\underline{y})\rightarrow\hat{q}(x_{i},\underline{T})}&\displaystyle\Psi_{b_{i},\hat{q}}^{(h-1)}(z)[\underline{T}/\underline{y}]&\wedge\\ &\displaystyle\bigwedge_{q(f\underline{x},\underline{y})\rightarrow p[\ldots]\atop p\neq\top}&\displaystyle\bot\end{array}$$

$${\Psi }_{b,q}^{(0)}(z)$$

$${\Psi }_{b,q}^{(1)}(z)$$

$${\Psi }_{b,q}^{(2)}(z)$$

$${\Psi }_{b,q}^{(3)}(z)$$

$$\begin{array}[]{llclr}&\displaystyle\bigwedge_{b(f\underline{x})\to(b_{1},\ldots,b_{k})\atop{q(f\underline{x},\underline{y})\rightarrow p[\underline{t}]\atop q^{\prime}(f\underline{x},\underline{y^{\prime}})\rightarrow p[\underline{t^{\prime}}]}}\Big{(}&\displaystyle\bigwedge_{t_{i}=y_{j_{i}},\atop t^{\prime}_{i}=y^{\prime}_{j^{\prime}_{i}}}&\displaystyle(y_{j_{i}}\doteq y^{\prime}_{j^{\prime}_{i}})&\wedge\\ &&\displaystyle\bigwedge_{t_{i}=y_{j_{i}},\atop t^{\prime}_{i}=q^{\prime}_{i}(x_{j^{\prime}_{i}},\underline{T^{\prime}})}&\displaystyle\Psi_{b_{j^{\prime}_{i}},q^{\prime}_{i}}^{\prime(h-1)}(y_{j_{i}})[\underline{T^{\prime}}/\underline{y^{\prime}}]&\wedge\\ &&\displaystyle\bigwedge_{t^{\prime}_{i}=y^{\prime}_{j^{\prime}_{i}},\atop t_{i}=q_{i}(x_{j_{i}},\underline{T})}&\displaystyle\Psi_{b_{j_{i}},q_{i}}^{(h-1)}(y^{\prime}_{j^{\prime}_{i}})[\underline{T}/\underline{y}]&\wedge\\ &&\displaystyle\bigwedge_{t_{i}=q_{i}(x_{j_{i}},\underline{T}),\atop{t^{\prime}_{i}=q^{\prime}_{i}(x_{j^{\prime}_{i}},\underline{T^{\prime}})\atop j_{i}=j^{\prime}_{i}}}&\displaystyle\Phi_{b_{j_{i}},(q_{i},q^{\prime}_{i})}^{(h-1)}[\underline{T}/\underline{y},\underline{T^{\prime}}/\underline{y^{\prime}}]&\wedge\\ &&\displaystyle\bigwedge_{t_{i}=q_{i}(x_{j_{i}},\underline{T}),\atop{t^{\prime}_{i}=q^{\prime}_{i}(x_{j^{\prime}_{i}},\underline{T^{\prime}})\atop j_{i}\neq j^{\prime}_{i}}}&\displaystyle(\Psi_{b_{j_{i}},q_{i}}^{(h-1)}(s_{b,q_{i}})[\underline{T}/\underline{y}]\wedge\Psi_{b_{j^{\prime}_{i}},q^{\prime}_{i}}^{\prime(h-1)}(s_{b,q_{i}}[\underline{T}/\underline{y}])[\underline{T^{\prime}}/\underline{y^{\prime}}])\ \Big{)}&\wedge\\ &\displaystyle\bigwedge_{b(f)\to(b_{1},\ldots,b_{k})\atop{p\neq p^{\prime},q(f\underline{x},\underline{y})\rightarrow p[\underline{t}]\atop q^{\prime}(f\underline{x},\underline{q})\rightarrow p^{\prime}[\underline{t^{\prime}}]}}&\displaystyle\bot\end{array}$$

$$(q,\underline{T}){\cong }_b^{(h)}(q^{\prime },\underline{T^{\prime }})\iff {\Phi }_{b,(q,q^{\prime })}^{(h)}[\underline{T}/\underline{y},\underline{T^{\prime }}/\underline{y^{\prime }}]\equiv \mathrm{true}$$

$$s{\cong }_b^{(h)}(q^{\prime },\underline{T^{\prime }})\iff {\Psi }_{b,q^{\prime }}^{(h)}(t)[\underline{T^{\prime }}/\underline{y}]\equiv \mathrm{true}$$

$${\Psi }_{b,q}^{(h)}(z)$$

$${\Phi }_{b,(q,q^{\prime })}^{(h)}$$

$$(q,\underline{T}){\cong }_b(q^{\prime },\underline{T^{\prime }})\iff {\Phi }_{b,(q,q^{\prime })}[\underline{T}/\underline{y}][\underline{T^{\prime }}/\underline{y^{\prime }}]\equiv \mathrm{true}$$

$$\begin{array}[]{rcl}q(f(x),y_{1},y_{2})&\rightarrow&a(q(x,b(y_{1},y_{1}),c(y_{2}),d))\\ q(g,y_{1},y_{2})&\rightarrow&y_{1}\\ q(h,y_{1},y_{2})&\rightarrow&y_{2}\par\end{array}$$

$$\begin{array}[]{rcl}q^{\prime}(f(x),y^{\prime}_{1},y^{\prime}_{2})&\rightarrow&a(q^{\prime}(x,c(y^{\prime}_{1}),b(y^{\prime}_{2},y^{\prime}_{2}),d))\\ q^{\prime}(g,y^{\prime}_{1},y^{\prime}_{2})&\rightarrow&y^{\prime}_{2}\\ q^{\prime}(h,y^{\prime}_{1},y^{\prime}_{2})&\rightarrow&y^{\prime}_{1}\par\end{array}$$

$${\Phi }_{r,(q,q^{\prime })}^{(0)}$$

$${\Phi }_{r,(q,q^{\prime })}^{(1)}$$

$$q(f(t_1,\dots ,t_k),y_1,\dots ,y_k)\to t⟨p_1,\dots ,p_k⟩$$

$$\hat{q}(⟨f(x_1,\dots ,x_k),r_1,\dots ,r_k,r_1^{\prime },\dots ,r_k^{\prime }⟩,\underline{y})\to p[{\hat{T}}_1,\dots ,{\hat{T}}_m]$$

$$Y_q$$

$$Z_i$$

$${\mathsf{pref}}_o(q)$$

Full text

1 Introduction

Attribute grammars are a well-established formalism for realizing computations on syntax trees [21, 22], and implementations are available for various programming languages, see, e.g. [30, 29, 13]. A fundamental question for any such specification formalism is whether two specifications are semantically equivalent. As a particular case, attribute grammars have been considered which compute uninterpreted trees. Such devices that translate input trees (viz. the parse trees of a context-free grammar) into output trees, have also been studied under the name “attributed tree transducer” [15] (see also [16]). In 1982, Courcelle and Franchi-Zannettacci showed that the equivalence problem for (strongly noncircular) attribute systems reduces to the equivalence problem for primitive recursive schemes with parameters [3, 4]; the latter model is also known under the name macro tree transducer [10]. Whether or not equivalence of attributed tree transducers (ATTs) or of (deterministic) macro tree transducers (MTTs) is decidable remain two intriguing (and very difficult) open problems.

For several subclasses of ATTs it has been proven that equivalence is decidable. The most general and very recent result that covers almost all other known ones about deterministic tree transducers is that “deterministic top-down tree-to-string transducers” have decidable equivalence [28]. Notice that the complexity of this problem remains unknown (the decidability is proved via two semi-decision procedures). The only result concerning deterministic tree transducers that we are aware of and that is not covered by this general result, is the one by Courcelle and Franchi-Zannettacci about decidability of equivalence of “separated non-nested” ATTs (which they reduce to the same problem for “separated non-nested” MTTs). However, in their paper no statement is given concerning the complexity of the problem. In this paper we close this gap and study the complexity of deciding equivalence of separated non-nested MTTs. To do so we propose a new approach that we feel is simpler and easier to understand than the one of [3, 4]. Using our approach we can prove that the problem can be solved in polynomial time.

In a separated non-nested attribute system, distinct sets of operators are used for the construction of inherited and synthesized attributes, respectively, and inherited attributes may depend on inherited attributes only. Courcelle and Franchi-Zannettacci’s algorithm first translates separated non-nested attribute grammars into separated total deterministic non-nested macro tree transducers. In the sequel we will use the more established term basic macro-tree transducers instead of non-nested MTTs. Here, a macro tree transducer is called separated if the alphabets used for the construction of parameter values and outside of parameter positions are disjoint. And the MTT is basic if there is no nesting of state calls, i.e., there are no state calls inside of parameter positions. Let us consider an example. We want to translate ternary numbers into expressions over $+$, $*$, EXP, plus the constants [math], $1$, and $2$. Additionally, operators $s$, $p$, and $z$ are used to represent integers in unary. The ternary numbers are parsed into particular binary trees; e.g., the left of Figure 1 shows the binary tree for the number $2101.02$. This tree is translated by our MTT into the tree in the right of Figure 1 (which indeed evaluates to $64.\overline{2}$ in decimal). The rules of our transducer $M_{\text{tern}}$ are shown in Figure 2.

The example is similar to the one used by Knuth [21] in order to introduce attribute grammars. The transducer is indeed basic and separated: the operators $p$, $s$, and $z$ are only used in parameter positions.

Our polynomial time decision procedure works in two phases: first, the transducer is converted into an “earliest” normal form. In this form, output symbols that are not produced within parameter positions are produced as early as possible. In particular it means that the root output symbols of the right-hand sides of rules for one state must differ. For instance, our transducer $M_{\text{tern}}$ is not earliest, because all three $r$-rules produce the same output root symbol ($*$). Intuitively, this symbol should be produced earlier, e.g., at the place when the state $r$ is called. The earliest form is a common technique used for normal forms and equivalence testing of different kinds of tree transducers [9, 14, 23]. We show that equivalent states of a transducer in this earliest form produce their state-output exactly in the same way. This means especially that the output of parameters is produced in the same places. It is therefore left to check, in the second phase, that also these parameter outputs are equivalent. To this end, we build an equivalence relation on states of earliest transducers that combines the two equivalence tests described before. Technically speaking, the equivalence relation is tested by constructing sets of Herbrand equalities. From these equalities, a fixed point algorithm can, after polynomially many iterations, produce a stable set of equalities.

An abridged version of this paper will be published within FoSSaCS 2019.

2 Separated Basic Macro Tree Transducers

Let $\Sigma$ be a ranked alphabet, i.e., every symbol of the finite set $\Sigma$ has associated with it a fixed rank $k\in\mathbb{N}$. Generally, we assume that the input alphabet $\Sigma$ is non-trivial, i.e., $\Sigma$ has cardinality at least 2, and contains at least one symbol of rank [math] and at least one symbol of rank $>0$. The set $\mathcal{T}_{\Sigma}$ is the set of all (finite, ordered, rooted) trees over the alphabet $\Sigma$. We denote a tree as a string over $\Sigma$ and parenthesis and commas, i.e., $f(a,f(a,b))$ is a tree over $\Sigma$, where $f$ is of rank $2$ and $a,b$ are of rank zero. We use Dewey dotted decimal notation to refer to a node of a tree: The root node is denoted $\varepsilon$, and for a node $u$, its $i$-th child is denoted by $u.i$. For instance, in the tree $f(a,f(a,b))$ the $b$-node is at position $2.2$. A pattern (or $k$-pattern) (over $\Delta$) is a tree $p\in\mathcal{T}_{\Delta\cup\{\top\}}$ over a ranked alphabet $\Delta$ and a disjoint symbol $\top$ (with exactly $k$ occurrences of the symbol $\top$). The occurrences of the dedicated symbol $\top$ serve as place holders for other patterns. Assume that $p$ is a $k$-pattern and that $p_{1},\dots,p_{k}$ are patterns; then $p[p_{1},\ldots,p_{k}]$ denotes the pattern obtained from $p$ by replacing, for $i=1,\ldots,k$, the $i$-th occurrence (from left-to-right) of $\top$ by the pattern $p_{i}$.

A macro tree transducer (MTT) $M$ is a tuple $(Q,\Sigma,\Delta,\delta)$ where $Q$ is a ranked alphabet of states, $\Sigma$ and $\Delta$ are the ranked input and output alphabets, respectively, and $\delta$ is a finite set of rules of the form:

[TABLE]

where $q\in Q$ is a state of rank $l+1$, $l\geq 0$, $f\in\Sigma$ is an input symbol of rank $k\geq 0$, $x_{1},\ldots,x_{k}$ and $y_{1},\ldots,y_{l}$ are the formal input and output parameters, respectively, and $T$ is a tree built up according to the following grammar:

[TABLE]

for output symbols $a\in\Delta$ of rank $m\geq 0$ and states $q^{\prime}\in Q$ of rank $n+1$, input parameter $x_{i}$ with $1\leq i\leq k$, and output parameter $y_{j}$ with $1\leq j\leq l$. For simplicity, we assume that all states $q$ have the same number $l$ of parameters. Our definition of an MTT does not contain an initial state. We therefore consider an MTT always together with an axiom $A=p[q_{1}(x_{1},\underline{T_{1}}),\ldots,q_{m}(x_{1},\underline{T_{m}})]$ where $\underline{T_{1}},\ldots,\underline{T_{m}}\in\mathcal{T}_{\Delta}^{l}$ are vectors of output trees (of length $l$ each). Sometimes we only use an MTT $M$ without explicitly mentioning an axiom $A$, then some $A$ is assumed implicitly. Intuitively, the state $q$ of an MTT corresponds to a function in a functional language which is defined through pattern matching over its first argument, and which constructs tree output using tree top-concatenation only; the second to $(l+1)$-th arguments of state $q$ are its accumulating output parameters. The output produced by a state for a given input tree is determined by the right-hand side $T$ of a rule of the transducer which matches the root symbol $f$ of the current input tree. This right-hand side is built up from accumulating output parameters and calls to states for subtrees of the input and applications of output symbols from $\Delta$. In general MTTs are nondeterministic and only partially defined. Here, however, we concentrate on total deterministic transducers. The MTT $M$ is deterministic, if for every $(q,f)\in Q\times\Sigma$ there is at most one rule of the form (1). The MTT $M$ is total, if for every $(q,f)\in Q\times\Sigma$ there is at least one rule of the form (1). For total deterministic transducers, the semantics of a state $q\in Q$ with the rule $q(f(x_{1},\ldots,x_{k}),y_{1},\ldots,y_{l})\to T$ can be considered as a function

[TABLE]

which inductively is defined by:

[TABLE]

where $\underline{S}=(S_{1},\ldots,S_{l})\in\mathcal{T}_{\Delta}^{l}$ is a vector of output trees. The semantics of a pair $(M,A)$ with MTT $M$ and axiom $A=p[q_{1}(x_{1},\underline{T_{1}}),\ldots,q_{m}(x_{1},\underline{T_{m}})]$ is defined by $\llbracket(M,A)\rrbracket(t)=p[\llbracket q_{1}\rrbracket(t,\underline{T_{1}}),\ldots,\llbracket q_{m}\rrbracket(t,\underline{T_{m}})]$. Two pairs $(M_{1},A_{1})$, $(M_{2},A_{2})$ consisting of MTTs $M_{1}$, $M_{2}$ and corresponding axioms $A_{1}$, $A_{2}$ are equivalent, $(M_{1},A_{1})\equiv(M_{2},A_{2})$, iff for all input trees $t\in\mathcal{T}_{\Sigma}$, and parameter values $\underline{T}\in\mathcal{T}_{\Delta_{in}}^{l}$, $\llbracket(M_{1},A_{1})\rrbracket(t,\underline{T})=\llbracket(M_{2},A_{2})\rrbracket(t,\underline{T})$.

The MTT $M$ is basic, if each argument tree $T_{j}$ of a subtree $q^{\prime}(x_{i},T_{1},\ldots,T_{n})$ of right-hand sides $T$ of rules (1) may not contain further occurrences of states, i.e., is in $\mathcal{T}_{\Delta\cup Y}$. The MTT $M$ is separated basic, if $M$ is basic, and $\Delta$ is the disjoint union of ranked alphabets $\Delta_{out}$ and $\Delta_{in}$ so that the argument trees $T_{j}$ of subtrees $q^{\prime}(x_{i},T_{1},\ldots,T_{n})$ are in $\mathcal{T}_{\Delta_{in}\cup Y}$, while the output symbols $a$ outside of such subtrees are from $\Delta_{out}$. The same must hold for the axiom. Thus, letters directly produced by a state call are in $\Delta_{out}$ while letters produced in the parameters are in $\Delta_{in}$. The MTT $M_{\text{tern}}$ from the Introduction is separated basic with $\Delta_{out}=\{0,1,2,3,*,+,\text{EXP}\}$ and $\Delta_{in}=\{p,s,z\}$.

As separated basic MTTs are in the focus of our interests, we make the grammar for their right-hand side trees $T$ explicit:

[TABLE]

where $a\in\Delta_{out}$, $q^{\prime}\in Q$, $b\in\Delta_{in}$ of ranks $m,n+1$ and $m^{\prime}$, respectively, and $p$ is an $n$-pattern over $\Delta$. For separated basic MTTs only axioms $A=p[q_{1}(x_{1},\underline{T_{1}}),\ldots,q_{m}(x_{1},\underline{T_{m}})]$ with $T_{1},\ldots,T_{m}\in\mathcal{T}_{\Delta_{in}}^{l}$ are considered.

Note that equivalence of nondeterministic transducers is undecidable (even already for very small subclasses of transductions [19]). Therefore, we assume for the rest of the paper that all MTTs are deterministic and separated basic. We will also assume that all MTTs are total, with the exception of Section 5 where we also consider partial MTTs.

Example 1

We reconsider the example from the Introduction and adjust it to our formal definition. The transducer was given without an axiom (but with a tacitly assumed “start state” $q_{0}$). Let us now remove the state $q_{0}$ and add the axiom $A=q(x_{1},z)$. The new $q$ rule for $g$ is:

[TABLE]

To make the transducer total, we add for state $q^{\prime}$ the rule

[TABLE]

For state $r$ we add rules $q(\alpha(x_{1},x_{2}),y)\to*(0,\text{EXP}(3,y))$ with $\alpha=f,g$. The MTT is separated basic with $\Delta_{out}=\{0,1,2,3,*,+,\text{EXP}\}$ and $\Delta_{in}=\{p,s,z\}$. ∎

We restricted ourselves to total separated basic MTTs. However, we would like to be able to decide equivalence for partial transducers as well. For this reason we define now top-down tree automata, and will then decide equivalence of MTTs relative to some given DTA $D$. A deterministic top-down tree automaton (DTA) $D$ is a tuple $(B,\Sigma,b_{0},\delta_{D})$ where $B$ is a finite set of states, $\Sigma$ is a ranked alphabet of input symbols, $b_{0}\in B$ is the initial state, and $\delta_{D}$ is the partial transition function with rules of the form $b(f(x_{1},\ldots,x_{k}))\to(b_{1}(x_{1}),\ldots,b_{k}(x_{k}))$, where $b,b_{1},\dots,b_{k}\in B$ and $f\in\Sigma$ of rank $k$. W.l.o.g. we always assume that all states $b$ of a DTA are productive, i.e., ${\sf dom}(b)\neq\emptyset$. If we consider a MTT $M$ relative to a DTA $D$ we implicitly assume a mapping $\pi:Q\to B$, that maps each state of $M$ to a state of $D$, then we consider for $q$ only input trees in ${\sf dom}(\pi(q))$.

3 Top-Down Normalization of Transducers

In this section we show that each total deterministic basic separated MTT can be put into an “earliest” normal form relative to a fixed DTA $D$. Intuitively, state output (in $\Delta_{out}$) is produced as early as possible for a transducer in the normal form. It can then be shown that two equivalent transducers in normal form produce their state output in exactly the same way.

Recall the definition of patterns as trees over $\mathcal{T}_{\Delta\cup\{\top\}}$. Substitution of $\top$-symbols by other patterns induces a partial ordering $\sqsubseteq$ over patterns by $p\sqsubseteq p^{\prime}$ if and only if $p=p^{\prime}[p_{1},\ldots,p_{m}]$ for some patterns $p_{1},\ldots,p_{m}$. W.r.t. this ordering, $\top$ is the largest element, while all patterns without occurrences of $\top$ are minimal. By adding an artificial least element $\bot$, the resulting partial ordering is in fact a complete lattice. Let us denote this complete lattice by $\mathcal{P}_{\Delta}$.

Let $\Delta=\Delta_{in}\cup\Delta_{out}$. For $T\in\mathcal{T}_{\Delta\cup Y}$, we define the $\Delta_{out}$-prefix as the pattern $p\in\mathcal{T}_{\Delta_{out}\cup\{\top\}}$ as follows. Assume that $T=a(T_{1},\ldots,T_{m})$.

• •

If $a\in\Delta_{out}$, then $p=a(p_{1},\ldots,p_{m})$ where for $j=1,\ldots,m$, $p_{j}$ is the $\Delta_{out}$-prefix of $T_{j}$.

• •

If $a\in\Delta_{in}\cup Y$, then $p=\top$.

By this definition, each tree $t\in\mathcal{T}_{\Delta\cup Y}$ can be uniquely decomposed into a $\Delta_{out}$-prefix $p$ and subtrees $t_{1},\ldots,t_{m}$ whose root symbols all are contained in $\Delta_{in}\cup Y$ such that $t=p[t_{1},\ldots,t_{m}]$.

Let $M$ be a total separated basic MTT $M$, $D$ be a given DTA. We define the $\Delta_{out}$-prefix of a state $q$ of $M$ relative to $D$ as the minimal pattern $p\in\mathcal{T}_{\Delta_{out}\cup\{\top\}}$ so that each tree $\llbracket q\rrbracket(t,\underline{T})$, $t\in{\sf dom}(\pi(q)),\underline{T}\in\mathcal{T}_{\Delta}^{l},$ is of the form $p[T_{1},\ldots,T_{m}]$ for some sequence of subtrees $T_{1},\ldots,T_{m}\in\mathcal{T}_{\Delta}$. Let us denote this unique pattern $p$ by ${\sf pref}_{o}(q)$. If $q(f,y_{1},\ldots,y_{l})\rightarrow T$ is a rule of a separated basic MTT and there is an input tree $f(t_{1},\ldots,t_{k})\in{\sf dom}(\pi(q))$ then $|{\sf pref}_{o}(q)|\leq|T|$.

Lemma 1

Let $M$ be a total separated basic MTT and $D$ a given DTA. Let $t\in{\sf dom}(\pi(q))$ be a smallest input tree of a state $q$ of $M$. The $\Delta_{out}$-prefix of every state $q$ of $M$ relative to $D$ can be computed in time $\mathcal{O}(|t|\cdot|M|)$.

The proof is similar to the one of [9, Theorem 8] for top-down tree transducers. This construction can be carried over as, for the computation of $\Delta_{out}$-prefixes, the precise contents of the output parameters $y_{j}$ can be ignored. The complete proof can be found in the Appendix.

Example 2

We compute the $\Delta_{out}$-prefix of the MTT $M$ from Example 1. We consider $M$ relative to the trivial DTA $D$ that consists only of one state $b$ with $dom(b)=\mathcal{T}_{\Sigma}$. We therefore omit $D$ in our example. We get the following system of in-equations: from the rules of state $r$ we obtain $Y_{r}\sqsubseteq*(i,\text{EXP}(3,\top))$ with $i\in\{0,1,2\}$. From the rules of state $q$ we obtain $Y_{q}\sqsubseteq+(Y_{q},Y_{q^{\prime}})$, $Y_{q}\sqsubseteq+(Y_{r},Y_{q})$ and $Y_{q}\sqsubseteq*(i,\text{EXP}(3,\top))$ with $i\in\{0,1,2\}$. From the rules of state $q^{\prime}$ we obtain $Y_{q^{\prime}}\sqsubseteq+(*(0,\text{EXP}(3,\top)),*(0,\text{EXP}(3,\top)))$, $Y_{q^{\prime}}\sqsubseteq+(Y_{r},Y_{q^{\prime}})$ and $Y_{q^{\prime}}\sqsubseteq*(i,\text{EXP}(3,\top))$ with $i\in\{0,1,2\}$. For the fixpoint iteration we initialize $Y_{r}^{(0)}$, $Y_{q}^{(0)}$, $Y_{q^{\prime}}^{(0)}$ with $\bot$ each. Then $Y_{r}^{(1)}=*(\top,\text{EXP}(3,\top))=Y_{r}^{(2)}$ and $Y_{q}^{(1)}=\top$, $Y_{q^{\prime}}^{(1)}=\top$. Thus, the fixpoint iteration ends after two rounds with the solution ${\sf pref}_{o}(q)=\top$. ∎

Let $M$ be a separated basic MTT $M$ and $D$ be a given DTA $D$. $M$ is called $D$-earliest if for every state $q\in Q$ the $\Delta_{out}$-prefix with respect to $\pi(q)$ is $\top$.

Lemma 2

For every pair $(M,A)$ consisting of a total separated basic MTT $M$ and axiom $A$ and a given DTA $D$, an equivalent pair $(M^{\prime},A^{\prime})$ can be constructed so that $M^{\prime}$ is a total separated basic MTT that is $D$-earliest. Let $t$ be an output tree of $(M,A)$ for a smallest input tree $t^{\prime}\in{\sf dom}(\pi(q))$ where $q$ is the state occurring in $A$. Then the construction runs in time $\mathcal{O}(|t|\cdot|(M,A)|)$.

The construction follows the same line as the one for the earliest form of top-down tree transducer, cf. [9, Theorem 11]. The proof can be found in the appendix. Note that for partial separated basic MTTs the size of the $\Delta_{out}$-prefixes is at most exponential in the size of the transducer. However for total transducer that we consider here the $\Delta_{out}$-prefixes are linear in the size of the transducer and can be computed in quadratic time, cf. [9].

Corollary 1

For $(M,A)$ consisting of a total deterministic separated basic MTT $M$ and axiom $A$ and the trivial DTA $D$ accepting $\mathcal{T}_{\Sigma}$ an equivalent pair $(M^{\prime},A^{\prime})$ can be constructed in quadratic time such that $M^{\prime}$ is an $D$-earliest total deterministic separated basic MTT.

Example 3

We construct an equivalent earliest MTT $M^{\prime}$ for the transducer from Example 1. In Example 2 we already computed the $\Delta_{out}$-prefixes of states $q,q^{\prime},r$; ${\sf pref}_{o}(q)=\top$, ${\sf pref}_{o}(q^{\prime})=\top$ and ${\sf pref}_{o}(r)=*(\top,\text{EXP}(3,\top))$. As there is only one occurrence of symbol $\top$ in the $\Delta_{out}$-prefixes of $q$ and $q^{\prime}$ we call states ${\langle q,1\rangle}$ and ${\langle q^{\prime},1\rangle}$ by $q$ and $q^{\prime}$, respectively. Hence, a corresponding earliest transducer has axiom $A=q(x_{1},z)$. The rules of $q$ and $q^{\prime}$ for input symbol $g$ do not change. For input symbol $f$ we obtain

[TABLE]

As there is only one occurrence of symbol $\top$ related to a recursive call in ${\sf pref}_{o}(r)$ we call ${\langle r,1\rangle}$ by $r$. For state $r$ we obtain new rules $r(\alpha(x_{1},x_{2}),y)\to 0$ with $\alpha\in\{f,g\}$ and $r(i,y)\to i$ with $i\in\{0,1,2\}$. ∎

We define a family of equivalence relation by induction, $\cong_{b}\ \subseteq((Q,\mathcal{T}_{\Delta_{in}}^{k})\cup\mathcal{T}_{\Delta_{in}})\times((Q,\mathcal{T}_{\Delta_{in}}^{k})\cup\mathcal{T}_{\Delta_{in}})$ with $b$ a state of a given DTA is the intersection of the equivalence relations $\cong^{(h)}_{b}$, i.e., $X\cong_{b}Z$ if and only if for all $h\geq 0$, $X\cong^{(h)}_{b}Z$. We let $(q,\underline{T})\cong^{(h+1)}_{b}(q^{\prime},\underline{T^{\prime}})$ if for all $f\in{\sf dom}(b)$ with $b(f(x_{1},\ldots,x_{k})\to(b_{1},\ldots,b_{k})$, there is a pattern $p$ such that $q(f(x_{1},\ldots,x_{k}),\underline{y})\rightarrow p[t_{1},\ldots,t_{m}]$ and $q^{\prime}(f(x_{1},\ldots,x_{k}),\underline{y^{\prime}})\rightarrow p[t^{\prime}_{1},\ldots,t^{\prime}_{m}]$ with

• •

if $t_{i}$ and $t^{\prime}_{i}$ are both recursive calls to the same subtree, i.e., $t_{i}=q_{i}(x_{j_{i}},\underline{T_{i}})$, $t^{\prime}_{i}=q^{\prime}_{i}(x_{j^{\prime}_{i}},\underline{T^{\prime}_{i}})$ and $j_{i}=j^{\prime}_{i}$, then $(q_{i},\underline{T_{i}})[\underline{T}/\underline{y}]\cong^{h}_{b_{j_{i}}}(q^{\prime}_{i},\underline{T^{\prime}_{i}})[\underline{T^{\prime}}/\underline{y^{\prime}}]$

• •

if $t_{i}$ and $t^{\prime}_{i}$ are both recursive calls but on different subtrees, i.e., $t_{i}=q_{i}(x_{j_{i}},\underline{T_{i}})$, $t^{\prime}_{i}=q^{\prime}_{i}(x_{j^{\prime}_{i}},\underline{T^{\prime}_{i}})$ and $j_{i}\neq j^{\prime}_{i}$, then $\hat{t}:=\llbracket q_{i}\rrbracket(s,\underline{T_{i}})[\underline{T}/\underline{y}]=\llbracket q^{\prime}_{i}\rrbracket(s,\underline{T^{\prime}_{i}})[\underline{T}/\underline{y}]$ for some $s\in\Sigma^{(0)}$ and $(q_{i},\underline{T_{i}})[\underline{T}/\underline{y}]\cong^{(h)}_{b_{j_{i}}}\hat{t}\cong^{(h)}_{b_{j^{\prime}_{i}}}(q^{\prime}_{i},\underline{T^{\prime}_{i}})[\underline{T}/\underline{y}]$

• •

if $t_{i}$ and $t^{\prime}_{i}$ are both parameter calls, i.e., $t_{i}=y_{j_{i}}$ and $t^{\prime}_{i}=y^{\prime}_{j^{\prime}_{i}}$, then $T_{j_{i}}=T^{\prime}_{j^{\prime}_{i}}$

• •

if $t_{i}$ is a parameter call and $t^{\prime}_{i}$ a recursive call, i.e., $t_{i}=y_{j_{i}}$ and $t^{\prime}_{i}=q^{\prime}_{i}(x_{j^{\prime}_{i}},\underline{T^{\prime}_{i}})$, then $T_{j_{i}}\cong^{(h)}_{b_{j^{\prime}_{i}}}(q^{\prime}_{i},\underline{T^{\prime}_{i}})[\underline{T^{\prime}}/\underline{y^{\prime}}]$

• •

(symmetric to the latter case) if $t_{i}$ is a recursive call and $t^{\prime}_{i}$ a parameter call, i.e., $t_{i}=q_{i}(x_{j_{i}},\underline{T_{i}})$ and $t^{\prime}_{i}=y^{\prime}_{j^{\prime}_{i}}$, then $(q_{i},\underline{T_{i}})[\underline{T}/\underline{y}]\cong^{(h)}_{b_{j_{i}}}T^{\prime}_{j^{\prime}_{i}}$.

We let $T\cong^{(h+1)}_{b}(q^{\prime},\underline{T^{\prime}})$ if for all $f\in{\sf dom}(b)$ with $r(f(x_{1},\ldots,x_{k}))\to(b_{1},\ldots,b_{k})$, $q^{\prime}(f(\underline{x}),\underline{y})\rightarrow t^{\prime}$,

• •

if $t^{\prime}=y_{j}$ then $T=T^{\prime}_{j}$

• •

if $t^{\prime}=q^{\prime}_{1}(x_{i},\underline{T^{\prime}_{1}})$ then $T\cong^{(h)}_{b_{i}}(q^{\prime}_{1},\underline{T^{\prime}_{1}})[\underline{T^{\prime}}/\underline{y^{\prime}}]$.

Intuitively, $(q,\underline{T})\cong^{h}_{b}(q^{\prime},\underline{T^{\prime}})$ if for all input trees $t\in{\sf dom}(b)$ of height $h$, $\llbracket q\rrbracket(t,\underline{T})=\llbracket q^{\prime}\rrbracket(t,\underline{T^{\prime}})$. Then $(q,\underline{T})\cong_{b}(q^{\prime},\underline{T^{\prime}})$ if for all input trees $t\in{\sf dom}(b)$ (independent of the height), $\llbracket q\rrbracket(t,\underline{T})=\llbracket q^{\prime}\rrbracket(t,\underline{T^{\prime}})$.

Theorem 3.1

For a given DTA $D$ with initial state $b$, let $M,M^{\prime}$ be $D$-earliest total deterministic separated basic MTTs with axioms $A$ and $A^{\prime}$, respectively. Then $(M,A)$ is equivalent to $(M^{\prime},A^{\prime})$ relative to $D$, iff there is a pattern $p$ such that $A=p[q_{1}(x_{1},\underline{T_{1}}),\ldots,q_{m}(x_{1},\underline{T_{m}})]$, and $A^{\prime}=p[q^{\prime}_{1}(x_{1},\underline{T^{\prime}_{1}}),\ldots,q^{\prime}_{m}(x_{1},\underline{T^{\prime}_{m}})]$ and for $j=1,\ldots,m$, $(q_{j},\underline{T_{j}})\cong_{b}(q^{\prime}_{j},\underline{T^{\prime}_{j}})$, i.e., $q_{j}$ and $q^{\prime}_{j}$ are equivalent on the values of output parameters $\underline{T}_{j}$ and $\underline{T}^{\prime}_{j}$.

Proof

Let $\Delta$ be the output alphabet of $M$ and $M^{\prime}$. Assume that $(M,A)\cong_{b}(M^{\prime},A^{\prime})$. As $M$ and $M^{\prime}$ are earliest, the $\Delta_{out}$-prefix of $\llbracket(M,A)\rrbracket(t)$ and $\llbracket(M^{\prime},A^{\prime})\rrbracket(t)$, for $t\in{\sf dom}(b)$ is the same pattern $p$ and therefore $A=p[q_{1}(x_{1},\underline{T_{1}}),\ldots,q_{m}(x_{1},\underline{T_{m}})]$ and $A^{\prime}=p[q^{\prime}_{1}(x_{1},\underline{T^{\prime}_{1}}),\ldots,q^{\prime}_{m}(x_{1},\underline{T^{\prime}_{m}})]$. To show that $(q_{i},\underline{T_{i}})\cong_{b}(q^{\prime}_{i},\underline{T^{\prime}_{i}})$ let $u_{i}$ be the position of the $i$-th $\top$-node in the pattern $p$. For some $t\in{\sf dom}(b)$ and $\underline{T}\in\mathcal{T}_{\Delta_{in}}$ let $t_{i}$ and $t^{\prime}_{i}$ be the subtree of $\llbracket(M,A)\rrbracket(t,\underline{T})$ and $\llbracket(M^{\prime},A^{\prime})\rrbracket(t,\underline{T})$, respectively. Then $t_{i}=t^{\prime}_{i}$ and therefore $(q_{i},\underline{T_{i}})\cong_{b}(q^{\prime}_{i},\underline{T^{\prime}_{i}})$.

Now, assume that the axioms $A=p[q_{1}(x_{1},\underline{T_{1}}),\ldots,q_{m}(x_{1},\underline{T_{m}})]$ and $A^{\prime}=p[q^{\prime}_{1}(x_{1},\underline{T^{\prime}_{1}}),\ldots,q^{\prime}_{m}(x_{1},\underline{T^{\prime}_{m}})]$ consist of the same pattern $p$ and for $i=1,\ldots,m$, $(q_{i},\underline{T_{i}})\cong_{b}(q^{\prime}_{i},\underline{T^{\prime}_{i}})$. Let $t\in{\sf dom}(b)$ be an input tree then

[TABLE]

4 Polynomial Time

In this section we prove the main result of this paper, namely, that for each fixed DTA $D$, equivalence of total deterministic basic separated MTTs (relative to $D$) can be decided in polynomial time. This is achieved by taking as input two $D$-earliest such transducers, and then collecting conditions on the parameters of pairs of states of the respective transducers for their produced outputs to be equal.

Example 4

Consider a DTA $D$ with a single state only which accepts all inputs, and states $q,q^{\prime}$ with

[TABLE]

Then $q$ and $q^{\prime}$ can only produce identical outputs for the input $a$ (in ${\sf dom}(b)$) if parameter $y_{2}^{\prime}$ of $q^{\prime}$ contains the same output tree as parameter $y_{1}$ of $q$. This precondition can be formalized by the equality $y_{2}^{\prime}\doteq y_{1}$. Note that in order to distinguish the output parameters of $q^{\prime}$ from those of $q$ we have used primed copies $y^{\prime}_{i}$ for $q^{\prime}$. ∎

It turns out that conjunctions of equalities such as in example 4 are sufficient for proving equivalence of states. For states $q,q^{\prime}$ of total separated basic MTTs $M,M^{\prime}$, respectively, that are both $D$-earliest for some fixed DTA $D$, $h\geq 0$ and some fresh variable $z$, we define

[TABLE]

where $\bot$ is the boolean value false. We denote the output parameters in $\Psi_{b,q}^{(h)}(z)$ by $\underline{y}$, we define $\Psi_{b,q^{\prime}}^{\prime(h)}(z)$ in the same lines as $\Psi_{b,q}^{(h)}(z)$ but using $\underline{y^{\prime}}$ for the output parameters. To substitute the output parameters with trees $\underline{T}$, $\underline{T^{\prime}}$, we therefore use $\Psi_{b,q}^{(h)}(z)[\underline{T}/\underline{y}]$ and $\Psi_{b,q^{\prime}}^{\prime(h)}(z)[\underline{T^{\prime}}/\underline{y^{\prime}}]$. Assuming that $q$ is a state of the $D$-earliest separated basic MTT $M$ then $\Psi_{b,q}^{(h)}(z)$ is true for all ground parameter values $\underline{s}$ and some $T\in\mathcal{T}_{\Delta\cup Y}$ if $\llbracket q\rrbracket(t,\underline{s})=T[\underline{s}/\underline{y}]$ for all input trees $t\in{\sf dom}(b)$ of height at most $h$. Note that, since $M$ is $D$-earliest, $T$ is necessarily in $\mathcal{T}_{\Delta_{in}\cup Y}$. W.l.o.g., we assume that every state $b$ of $D$ is productive, i.e., ${\sf dom}(b)\neq\emptyset$. For each state $b$ of $D$, we therefore may choose some input tree $t_{b}\in{\sf dom}(b)$ of minimal depth. We define $s_{b,q}$ to be the output of $q$ for a minimal input tree $t_{r}\in{\sf dom}(b)$ and parameter values $\underline{y}$ — when considering formal output parameters as output symbols in $\Delta_{in}$, i.e., $s_{b,q}=\llbracket q\rrbracket(t_{r},\underline{y})$.

Example 5

We consider again the trivial DTA $D$ with only one state $b$ that accepts all $t\in\mathcal{T}_{\Sigma}$. Thus, we may choose $t_{b}=a$. For a state $q$ with the following two rules $q(a,y_{1},y_{2})\rightarrow y_{1}$ and $q(f(x),y_{1},y_{2})\rightarrow q(x,h(y_{2}),b)$, we have $s_{b,q}=y_{1}$. Moreover, we obtain

[TABLE]

We observe that $\Psi_{b,q}^{(2)}(z)=\Psi_{b,q}^{(3)}(z)$ and therefore for every $h\geq 2$, $\Psi_{b,q}^{(h)}(z)=\Psi_{b,q}^{(3)}(z)$. ∎

According to our equivalence relation $\cong_{b}$, $b$ state of the DTA $D$, we define for states $q,q^{\prime}$ of $D$-earliest total deterministic separated basic MTTs $M,M^{\prime}$, and $h\geq 0$, the conjunction $\Phi_{b,(q,q^{\prime})}^{(h)}$ by

[TABLE]

$\Phi_{b,(q,q^{\prime})}^{(h)}$ is defined in the same lines as the equivalence relation $\cong^{(h)}_{b}$. $\Phi_{b,(q,q^{\prime})}^{(h)}$ is true for all values of output parameters $\underline{T}$, $\underline{T^{\prime}}$ such that $\llbracket q\rrbracket(t,\underline{T})=\llbracket q^{\prime}\rrbracket(t,\underline{T^{\prime}})$ for $t\in{\sf dom}(b)$ of height at most $h$. By induction on $h\geq 0$, we obtain:

Lemma 3

For a given DTA $D$, states $q,q^{\prime}$ of $D$-earliest total separated basic MTTs, vectors of trees $\underline{T},\underline{T^{\prime}}$ over $\Delta_{in}$, $b$ a state of $D$. $s\in{\sf dom}(b)$, and $h\geq 0$ the following two statements hold:

[TABLE]

[TABLE]

∎

$\Phi_{b,(q,q^{\prime})}^{(h)}$ is a conjunction of equations of the form $y_{i}\doteq y_{j}$, $y_{i}\doteq t$ with $t\in\Delta_{in}$. Every satisfiable conjunction of equalities is equivalent to a (possible empty) finite conjunction of equations of the form $y_{i}\doteq t_{i}$, $t_{i}\in\mathcal{T}_{\Delta_{in}\cup Y}$ where the $y_{i}$ are distinct and no equation is of the form $y_{j}\doteq y_{j}$. We call such conjunctions reduced. If we have two inequivalent reduced conjunctions $\phi_{1}$ and $\phi_{2}$ with $\phi_{1}\Rightarrow\phi_{2}$ then $\phi_{1}$ contains strictly more equations. From that follows that for every sequence $\phi_{0}\Rightarrow\ldots\phi_{m}$ of pairwise inequivalent reduced conjunctions $\phi_{j}$ with $k$ variables, $m\leq k+1$ holds. This observation is crucial for the termination of the fixpoint iteration we will use to compute $\Phi_{b,(q,q^{\prime})}^{(h)}$.

For $h\geq 0$ we have:

[TABLE]

As we fixed the number of output parameters to the number $l$, for each pair $(q,q^{\prime})$ the conjunction $\Phi_{b,(q,q^{\prime})}^{(h)}$ contains at most $2l$ variables $y_{i},y^{\prime}_{i}$. Assuming that the MTTs to which state $q$ and $q^{\prime}$ belong have $n$ states each, we conclude that $\Phi_{b,(q,q^{\prime})}^{(n^{2}(2l+1))}\equiv\Phi_{b,(q,q^{\prime})}^{(n^{2}(2l+1)+i)}$ and $\Psi_{b,q}^{(n(l+1))}\equiv\Psi_{b,q}^{(n(l+1)+i)}$ for all $i\geq 0$. Thus, we can define $\Phi_{b,(q,q^{\prime})}:=\Phi_{b,(q,q^{\prime})}^{(n^{2}(2l+1))}$ and $\Psi_{b,q}:=\Psi_{b,q}^{(n(l+1))}$. As $(q,\underline{T})\cong_{b}(q^{\prime},\underline{T^{\prime}})$ iff for all $h\geq 0$, $(q,\underline{T})\cong_{b}^{(h)}(q^{\prime},\underline{T^{\prime}})$ holds, observation (3) implies that

[TABLE]

Therefore, we have:

Lemma 4

For a DTA $D$, states $q,q^{\prime}$ of $D$-earliest separated basic MTTs $M,M^{\prime}$ and states $b$ of $D$, the formula $\Phi_{b,(q,q^{\prime})}$ can be computed in time polynomial in the sizes of $M$ and $M^{\prime}$.

Proof

We successively compute the conjunctions $\Psi_{b,q}^{(h)}(z),\Psi_{b,q^{\prime}}^{(h)}(z),\Phi_{b,(q,q^{\prime})}^{(h)},h\geq 0$, for all states $b,q,q^{\prime}$. As discussed before, some $h\leq n^{2}(2l+1)$ exists such that the conjunctions for $h+1$ are equivalent to the corresponding conjunctions for $h$ — in which case, we terminate. It remains to prove that the conjunctions for $h$ can be computed from the conjunctions for $h-1$ in polynomial time. For that, it is crucial that we maintain reduced conjunctions. Nonetheless, the sizes of occurring right-hand sides of equalities may be quite large. Consider for example the conjunction $x_{1}\doteq a\wedge x_{2}\doteq f(x_{1},x_{1})\wedge\ldots\wedge x_{n}\doteq f(x_{n-1},x_{n-1})$. The corresponding reduced conjunction is then given by $x_{1}\doteq a\wedge x_{2}\doteq f(a,a)\wedge\ldots\wedge x_{n}\doteq f(f(f(\ldots(f(a,a))\ldots)$ where the sizes of right-hand sides grow exponentially. In order to arrive at a polynomial-size representation, we therefore rely on compact representations where isomorphic subtrees are represented only once. W.r.t. this representation, reduction of a non-reduced conjunction, implications between reduced conjunctions as well as substitution of variables in conjunctions can all be realized in polynomial time. From that, the assertion of the lemma follows.

Example 6

Let $D$ be a DTA with the following rules $b(f(x))\to(b)$, $b(g)\to()$ and $b(h)\to()$. Let $q$ and $q^{\prime}$ be states of separated basic MTTs $M$, $M^{\prime}$, respectively, that are $D$-earliest and $\pi$, $\pi^{\prime}$ be the mappings from the states of $D$ to the states of $M$, $M^{\prime}$ with $(b,q)\in\pi$ and $(b,q^{\prime})\in\pi^{\prime}$.

[TABLE]

[TABLE]

[TABLE]

∎

In summary, we obtain the main theorem of our paper.

Theorem 4.1

Let $(M,A)$ and $(M^{\prime},A^{\prime})$ be pairs consisting of total deterministic separated basic MTTs $M$, $M^{\prime}$ and corresponding axioms $A$, $A^{\prime}$ and $D$ a DTA. Then the equivalence of $(M,A)$ and $(M^{\prime},A^{\prime})$ relative to $D$ is decidable. If $D$ accepts all input trees, equivalence can be decided in polynomial time.

Proof

By Lemma 2 we build pairs $(M_{1},A_{1})$ and $(M^{\prime}_{1},A^{\prime}_{1})$ that are equivalent to $(M,A)$ and $(M^{\prime},A^{\prime})$ where $M_{1}$, $M^{\prime}_{1}$ are $D$-earliest separated basic MTTs. If $D$ is trivial the construction is in polynomial time, cf. Corollary 1. Let the axioms be $A_{1}=p[q_{1}(x_{i_{1}},\underline{T_{1}}),\ldots,q_{k}(x_{i_{k}},\underline{T_{k}})]$ and $A^{\prime}_{1}=p^{\prime}[q^{\prime}_{1}(x_{i^{\prime}_{1}},\underline{T_{1}}),\ldots,q^{\prime}_{k}(x_{i^{\prime}_{k^{\prime}}},\underline{T_{k^{\prime}}})]$. According to Lemma 3 $(M_{1},A_{1})$ and $(M^{\prime}_{1},A^{\prime}_{1})$ are equivalent iff

• •

$p=p^{\prime}$, $k=k^{\prime}$ and

• •

for all $j=1,\ldots,k$, $\Phi_{b,(q_{j},q^{\prime}_{j})}[\underline{T_{j}}/\underline{y},\underline{T_{j}}/\underline{y^{\prime}}]$ is equivalent to ${\sf true}$.

By Lemma 4 we can decide the second statements in time polynomial in the sizes of $M_{1}$ and $M^{\prime}_{1}$.

5 Applications

In this section we show several applications of our equivalence result. First, we consider partial transductions of separated basic MTTs. To decide the equivalence of partial transductions we need to decide $a)$ whether the domain of two given MTTs is the same and if so, $b)$ whether the transductions on this domain are the same. How the second part of the decision procedure is done was shown in detail in this paper if the domain is given by a DTA. It therefore remains to discuss how this DTA can be obtained. It was shown in [5, Theorem 3.1] that the domain of every top-down tree transducer $T$ can be accepted by some DTA $B_{T}$ and this automaton can be constructed from $T$ in exponential time. This construction can easily be extended to basic MTTs. The decidability of equivalence of DTAs is well-known and can be done in polynomial time [17, 18]. To obtain a total transducer we add for each pair $(q,f)$, $q\in Q$ and $f\in\Sigma$ that has no rule a new rule $q(f(\underline{x}),\underline{y})\to\bot$, where $\bot$ is an arbitrary symbol in $\Delta_{out}$ of rank zero.

Example 7

In Example 1 we discussed how to adjust the transducer from the introduction to our formal definition. We therefore had to introduce additional rules to obtain a total transducer. Now we still add rules for the same pairs $(q,f)$ but only with right-hand sides $\bot$. Therefore the original domain of the transducer is given by a DTA $D=(R,\Sigma,r_{0},\delta_{D})$ with the rules $r_{0}(g(x_{1},x_{2}))\to(r(x_{1}),r(x_{2}))$, $r(f(x_{1},x_{2}))\to(r(x_{1}),r(x_{2}))$ and $r(i)\to(\ )$ for $i=1,2,3$. ∎

Corollary 2

The equivalence of deterministic separated basic MTTs with a partial transition function is decidable.

Next, we show that our result can be used to decide the equivalence of total separated basic MTTs with look-ahead. A total macro tree transducer with regular look-ahead ($\text{MTT}^{\text{R}}$) is a tuple $(Q,\Sigma,\Delta,\delta,R,\delta_{R})$ where $R$ is a finite set of look-ahead states and $\delta_{R}$ is a total function from $R^{k}\to R$ for every $f\in\Sigma^{(k)}$. Additionally we have a deterministic bottom-up tree automaton $(P,\Sigma,\delta,-)$ (without final states). A rule of the MTT is of the form

[TABLE]

and is applicable to an input tree $f(t_{1},\ldots,t_{k})$ if the look-ahead automaton accepts $t_{i}$ in state $p_{i}$ for all $i=1,\ldots,k$. For every $q,f,p_{1},\ldots,p_{k}$ there is exactly one such rule. Let $N_{1}=(Q_{1},\Sigma_{1},\Delta_{1},\delta_{1},R_{1},\delta_{R1}),N_{2}=(Q_{2},\Sigma_{2},\Delta_{2},\delta_{2},R_{2},\delta_{R2})$ be two total separated basic MTTs with look-ahead. We construct total separated basic MTTs $M_{1},M_{2}$ without look-ahead as follows. The input alphabet contains for every $f\in\Sigma$ and $r_{1},\ldots,r_{k}\in R_{1}$, $r^{\prime}_{1},\ldots,r^{\prime}_{k}\in R_{2}$ the symbols ${\langle f,r_{1},\ldots,r_{k},r^{\prime}_{1},\ldots,r^{\prime}_{k}\rangle}$. For $q(f(x_{1},\ldots,x_{k}),\underline{y})\to p[T_{1},\ldots,T_{m}]\ {\langle r_{1},\ldots,r_{k}\rangle}$ and $q^{\prime}(f(x_{1},\ldots,x_{k}),\underline{y^{\prime}})\to p^{\prime}[T^{\prime}_{1},\ldots,T^{\prime}_{m}]\ {\langle r^{\prime}_{1},\ldots,r^{\prime}_{k}\rangle}$ we obtain for $M_{1}$ the rules

[TABLE]

with $\hat{T}_{i}=\hat{q}_{i}({\langle x_{j_{i}},\hat{r_{1}},\ldots,\hat{r_{l}},\hat{r^{\prime}_{1}},\ldots,\hat{r^{\prime}_{l}}\rangle},Z_{i})$ if $T_{i}=q_{i}(x_{j_{i}},Z_{i})$ and $q_{i}(x_{j_{i}},\underline{y})\to\hat{T_{i}}\ \ {\langle\hat{r_{1}},\ldots,\hat{r_{l}}\rangle}$ and $q^{\prime}_{i}(x_{j_{i}},\underline{y^{\prime}})\to\hat{T^{\prime}_{i}}\ \ {\langle\hat{r^{\prime}_{1}},\ldots,\hat{r^{\prime}_{l}}\rangle}$. If $T_{i}=y_{j_{i}}$ then $\hat{T}_{i}=y_{j_{i}}$. The total separated basic MTT $M_{2}$ is constructed in the same lines. Thus, $N_{i}$, $i=1,2$ can be simulated by $M_{i}$, $i=1,2$, respectively, if the input is restricted to the regular tree language of new input trees that represent correct runs of the look-ahead automata.

Corollary 3

The equivalence of total separated basic MTTs with regular look-ahead is decidable in polynomial time.

Last, we consider separated basic MTTs that concatenate strings instead of trees in the parameters. We abbreviate this class of transducers by $\text{MTT}^{\text{yp}}$. Thus, the alphabet $\Delta_{in}$ is not longer a ranked alphabet but a unranked alphabet which elements/letters can be concatenated to words. The procedure to decide equivalence of $\text{MTT}^{\text{yp}}$ is essentially the same as we discussed in this paper but instead of conjunctions of equations of trees over $\Delta_{in}\cup Y$ we obtain conjunctions equations of words. Equations of words is a well studied problem  [25, 27, 24]. In particular, the confirmed Ehrenfeucht conjecture states that each conjunction of a set of word equations over a finite alphabet and using a finite number of variables, is equivalent to the conjunction of a finite subset of word equations [20]. Accordingly, by a similar argument as in section 4, the sequences of conjunctions $\Psi_{b,q}^{(h)}(z),{\Psi^{\prime}}_{b,q^{\prime}}^{(h)}(z),\Phi_{b,(q,q^{\prime})}^{(h)},h\geq 0$, are ultimately stable.

Theorem 5.1

The equivalence of total separated basic MTTs that concatenate words instead of trees in the parameters ($\Delta_{in}$ is unranked) is decidable.

6 Related Work

For several subclasses of attribute systems equivalence is known to be decidable. For instance, attributed grammars without inherited attributes are equivalent to deterministic top-down tree transducers (DT) [6, 4]. For this class equivalence was shown to be decidable by Esik [11]. Later, a simplified algorithm was provided in [9]. If the tree translation of an attribute grammar is of linear size increase, then equivalence is decidable, because it is decidable for deterministic macro tree transducers (DMTT) of linear size increase. This follows from the fact that the latter class coincides with the class of (deterministic) MSO definable tree translations (DMSOTT) [7] for which equivalence is decidable [8].

Figure 3 shows a Hasse diagram of classes of translations realized by certain deterministic tree transducers. The prefixes “l”, “sn”, “b” and “sb” mean “linear size increase”, “separated non-nested”, “basic” and “separated basic”, respectively. A minimal class where it is still open whether equivalence is decidable is the class of non-nested attribute systems (nATT) which, on the macro tree transducer side, is included in the class of basic deterministic macro tree transducers (bDMTT).

For deterministic top-down tree transducers, equivalence can be decided in EXPSPACE, and in NLOGSPACE if the transducers are total [26]. For the latter class of transducers, one can decide equivalence in polynomial time by transforming the transducer into a canonical normal form and then checking isomorphism of the resulting transducers [9]. In terms of hardness, we know that equivalence of deterministic top-down tree transducers is EXPTIME-hard. For linear size increase deterministic macro tree transducers the precise complexity is not known (but is at least NP-hard). More compexity results are known for other models of tree transducers such as streaming tree transducers [1], see [26] for a summary.

7 Conclusion

We have proved that the equivalence problem for separated non-nested attribute systems can be decided in polynomial time. In fact, we have shown a stronger statement, namely that in polynomial time equivalence of separated basic total deterministic macro tree transducers can be decided. To see that the latter is a strict superclass of the former, consider the translation that takes a binary tree as input, and outputs the same tree, but under each leaf a new monadic tree is output which represents the inverse Dewey path of that node. For instance, the tree $f(f(a,a),a)$ is translated into the tree $f(f(a(1(1(e))),a(2(1(e)))),a(2(e)))$. A macro tree transducer of the desired class can easily realize this translation using a rule of the form $q(f(x_{1},_{2}),y)\to f(q(x_{1},1(y)),q(x_{2},2(y)))$. In contrast, no attribute system can realize this translation. The reason is that for every attribute system, the number of distinct output subtrees is linearly bounded by the size of the input tree. For the given translation there is no linear such bound (it is bounded by $|s|\log(|s|)$).

The idea of “separated” to use different output alphabets, is related to the idea of transducers “with origin” [2, 12]. In future work we would like to define adequate notions of origin for macro tree transducer, and prove that equivalence of such (deterministic) transducers with origin is decidable.

Appendix 0.A Proof of Lemma 1

Let $M$ be a total separated basic MTT $M$, $D$ a given DTA. Let $t\in{\sf dom}(\pi(q))$ be a smallest input tree of a state $q$ of $M$. The $\Delta_{out}$-prefix of every state $q$ of $M$ relative to $D$ can be computed in $\mathcal{O}(|t|\cdot|M|)$.

Proof

The proof is similar to the one of [9, Theorem 8] for top-down tree transducers. This construction can be carried over as, for the computation of $\Delta_{out}$-prefixes, the precise contents of the output parameters $y_{j}$ can be ignored.

The $\Delta_{out}$-prefixes can be computed with the following system of in-equations over the complete lattice $\mathcal{P}_{\Delta_{out}}$ with unknowns $Y_{q}$, $q\in Q$:

For each rule $q(f(x_{1},\ldots,x_{k}),y_{1},\ldots,y_{l})\to T$ such that there is a tree $f(x_{1},\ldots,x_{k})\in{\sf dom}(\pi(q))$ we have the in-equation

[TABLE]

if $T=p[T_{1},\ldots,T_{m}]$ for some pattern $p\in\mathcal{T}_{\Delta_{out}\cup\{\top\}}$ and terms $T_{1},\ldots,T_{m}$ which are either variables $y_{j}$ or of the form $q^{\prime}(x_{i},t^{\prime}_{1},\ldots,t^{\prime}_{l})$, $1\leq i\leq k$ for some $q^{\prime}\in Q$ where

[TABLE]

Since all right-hand sides of in-equations (4) are monotonic in their arguments, the system has a unique least solution. Moreover, we observe that the right-hand sides are distributive w.r.t. the least upper bound of patterns in the arguments. I.e., for sets of patterns $S_{i}$ with $\bar{p_{i}}=\bigsqcup S_{i}$, $p[\bar{p}_{1},\ldots,\bar{p}_{m}]=\bigsqcup\{p[p_{1},\ldots,p_{m}]\mid p_{i}\in S_{i}\}$.

First, we show that the $\Delta_{out}$-prefixes ${\sf pref}_{o}(q)$, $q\in Q$ build a solution for the system of in-equations (4). Let $q(f(x_{1},\ldots,x_{k}),y_{1},\ldots,y_{l})\rightarrow p[T_{1},\ldots T_{m}]$ with $T_{i}=y_{j_{i}}$ or $T_{i}=q_{i}(x_{j_{i}},\underline{T_{i}})$ then

[TABLE]

By distributivity of pattern substitution, the latter pattern equals $p[\bar{p}_{1},\ldots,\bar{p}_{m}]$ where

[TABLE]

Therefore, ${\sf pref}_{o}(q),q\in Q$, satisfies all constraints.

Now consider any solution $p^{\prime}_{q},q\in Q$ of the given constraint system. We claim that then ${\sf pref}_{o}(q)\sqsubseteq p^{\prime}_{q}$ holds for all $q$. Accordingly, ${\sf pref}_{o}(q)$ is the least solution to the given constraint system. In order to prove the claim, we proceed by induction on the input trees $t\in{\sf dom}(\pi(q))$. Assume that $\pi(q)(f(x_{1},\ldots,x_{k}))\to(r_{1}(x_{1}),\ldots,r_{k}(x_{k}))$ and $q(f(t_{1},\ldots,t_{k}),\underline{y})\rightarrow p[T_{1},\ldots,T_{m}]$ is the rule of the MTT for $q$ and $f$ where $T_{i}$ either equals some parameter $y_{j_{i}}$ or an expression $q_{i}(x_{j_{i}},\underline{S_{i}})$. In that latter case, we have by inductive hypothesis for the $t_{i}\in{\sf dom}(\pi(q_{i}))$, that $p^{\prime}_{q_{i}}$ is a prefix of $\llbracket q_{i}\rrbracket(t_{i},\underline{S})$ for every tuple $\underline{S}\in\mathcal{T}_{\Delta_{in}}^{l}$, i.e., $p^{\prime}_{q_{i}}\sqsupseteq\llbracket q_{i}\rrbracket(t_{i},\underline{S})$ holds. For each $i$ with $T_{i}=y_{j_{i}}$, define $p^{\prime}_{i}$ as the pattern $\top$. Then, $p[p^{\prime}_{1},\ldots,p^{\prime}_{m}]$ is a prefix of $\llbracket q\rrbracket(t,\underline{S})$, i.e., $p[p^{\prime}_{1},\ldots,p^{\prime}_{m}]\sqsupseteq\llbracket q\rrbracket(t,\underline{S})$ holds. Since $p^{\prime}_{q}$ is a solution of the system of in-equations, we also have that $p^{\prime}_{q}\sqsupseteq p[p^{\prime}_{1},\ldots,p^{\prime}_{m}]$. Thus, the claim follows by transitivity of $\sqsupseteq$.

To compute the $\Delta_{out}$-prefixes for every $q\in Q$ we first compute some output tree $t_{q}=q(t,\underline{Y})$ where $t$ is a minimal input tree in ${\sf dom}(\pi(q))$ and $\underline{Y}$ a minimal vector of terms over $\Delta_{in}$. These $t_{q}$ can be computed in polynomial time and serve as lower bound for ${\sf pref}_{o}(q)$, i.e., $t_{q}\sqsubseteq{\sf pref}_{o}(q)$. We therefore take $t_{q}$ as inital values for $Y_{q}$ in the fixpoint iteration of the constraint system. Since in each iteration at least one subtree of the current value of $Y_{q}$ has to be replaced the fixpoint iteration ends after a polynomial time of iterations. ∎

Appendix 0.B Proof of Lemma 2

For every pair $(M,A)$ consisting of a total deterministic separated basic MTT $M$ and axiom $A$ and a given DTA $D$, an equivalent pair $(M^{\prime},A^{\prime})$ can be constructed so that $M^{\prime}$ is a total deterministic separated basic MTT that is $D$-earliest. Let $t$ be an output tree of $(M,A)$ for a smallest input tree $t\in{\sf dom}(\pi(q))$ where $q$ is the state occuring in $A$. Then the construction runs in $\mathcal{O}(|t|\cdot|(M,A)|)$.

Proof

Let $M=(Q,\Sigma,\Delta,\delta)$ and $A$ be an axiom. The new transducer $M^{\prime}=(Q^{\prime},\Sigma,\Delta,\delta^{\prime})$ is defined as follows: The set $Q^{\prime}$ of states of $M^{\prime}$ are pairs ${\langle q,v\rangle}$ where $q\in Q$ is a state of $M$, and $v$ the position of a $\top$ leaf in the pattern ${\sf pref}_{o}(q)$, while the new axiom $A^{\prime}$ and the new transition relation $\delta^{\prime}$ are obtained as follows. Let the axiom $A$ of $M$ be of the form $A=p[q_{1}(x_{1},\underline{T_{1}}),\ldots,q_{m}(x_{1},\underline{T_{m}})]$ with $\underline{T_{1}},\ldots,\underline{T_{m}}$ vectors of output parameters and for $j=1,\ldots,m$, let $t_{j}={\sf pref}_{o}(q_{j})[{\langle q_{j},v_{j1}\rangle}(x_{1},\underline{T_{j}}),\ldots,{\langle q_{j},v_{jr_{j}}\rangle}(x_{1},\underline{T_{j}})]$. Here $v_{j1},\ldots,v_{jr_{j}}$ is the sequence of positions of $\top$-leaves in ${\sf pref}_{o}(q_{j})$. Then the new axiom is given by $A^{\prime}=p[t_{1},\ldots,t_{m}]$. Now assume that $q(f(x_{1},\ldots,x_{k}),\underline{y})\to p[u_{1},\ldots,u_{m}]$ where for $i=1,\ldots,m$, $u_{i}$ either equals a parameter $y_{j_{i}}$ or a call $q_{i}(x_{j_{i}},\underline{T_{i}})$. Let $I$ denote the set of indices where the latter is the case. Let $\bar{u}_{i}$ denote the term ${\sf pref}_{o}(q_{i})$ if $i\in I$ and $u_{i}$ otherwise. By construction, $p[\bar{u}_{1},\ldots,\bar{u}_{m}]$ is a prefix of ${\sf pref}_{o}(q)$. Let $t^{\prime}_{i}={\sf pref}_{o}(q_{i})[{\langle q_{i},v_{i1}\rangle}(x_{j_{i}},\underline{T_{i}}),\ldots,{\langle q_{i},v_{ir_{i}}\rangle}(x_{j_{i}},\underline{T_{i}})]$ if $i\in I$ ($v_{i1},\ldots,v_{ir_{i}}$ is the sequence of positions of $\top$ leaves in ${\sf pref}_{o}(q_{j})$) and $y_{j_{i}}$ otherwise. Then ${\sf pref}_{o}(q)[s_{1},\ldots,s_{r}]=p[t^{\prime}_{1},\ldots,t^{\prime}_{m}]$ for some $s_{1},\ldots,s_{r}$. Assuming that $v_{1},\ldots,v_{r}$ are the positions of $\top$-leaves in ${\sf pref}_{o}(q)$, we set

[TABLE]

for $j=1,\ldots,r$. This ends the construction of the new transducer $M^{\prime}$ with the corresponding axiom $A^{\prime}$. Note, that the mapping $\pi^{\prime}$ from states of $M^{\prime}$ to states of $D$ is given by $\pi^{\prime}({\langle q,v\rangle})=b$ if and only if $\pi(q)=b$ with ${\langle q,v\rangle}\in Q^{\prime},q\in Q,b\in B$.

From the construction follows that $M^{\prime}$ is an earliest total deterministic separated basic MTT. We show that $(M,A)$ is equivalent to $(M^{\prime},A^{\prime})$ by induction over the structure of the input trees. The semantics of the pairs $(M,A)$ and $(M^{\prime},A^{\prime})$ is defined as $\llbracket(M,A)\rrbracket(t,\underline{T})=p[\llbracket q_{1}\rrbracket(t,\underline{T_{1}}),\ldots,\llbracket q_{m}\rrbracket(t,\underline{T_{m}})]$ and $\llbracket(M^{\prime},A^{\prime})\rrbracket(t,\underline{T})=p[\llbracket t_{1}\rrbracket,\ldots,\llbracket t_{m}\rrbracket]$ with $\llbracket t_{j}\rrbracket={\sf pref}_{o}(q_{j})[\llbracket{\langle q_{j},v_{j1}\rangle}\rrbracket(t,\underline{T_{j}}),\ldots,\llbracket{\langle q_{j},v_{jr_{j}}\rangle}\rrbracket(t,\underline{T_{j}})]$ for $j=1,\ldots,m$. Therefore, it suffices to show for every state $q\in Q$, every input tree $t\in{\sf dom}(\pi(q))={\sf dom}(\pi^{\prime}(q^{\prime}))$ and every vector of output parameters $\underline{T}\in\mathcal{T}_{\Delta_{in}}^{l}$, that

[TABLE]

holds if the subtrees $\top$ of ${\sf pref}_{o}(q)$ occur at positions $v_{1},\ldots,v_{r}$, respectively.

For $j=1,\ldots,m$, there are thus nodes $v_{j1},\ldots,v_{jr_{j}}$ in ${\sf pref}_{o}(q_{j})$ such that for each input tree $t\in{\sf dom}(\pi(q_{j}))$ and vector of output parameters $\underline{T}\in\mathcal{T}_{\Delta_{in}}^{l}$, $\llbracket q_{j}\rrbracket(t,\underline{T})={\sf pref}_{o}(q_{j})[\llbracket{\langle q_{j},v_{j1}\rangle}\rrbracket(t,\underline{T}),\ldots,\llbracket{\langle q_{j},v_{jr_{j}}\rangle}\rrbracket(t,\underline{T})]$. Note, that in the base case when $t=g$ and $g\in\Sigma$ has rank [math] ($m=1$), the right-hand side of a rule of $q$ is a term $t\in\mathcal{T}_{\Delta_{out}\cup Y}$, i.e., $q(t,\underline{y})\rightarrow p[y_{i1},\ldots,y_{ik}]$. Then for $i=1,\ldots,r$, ${\langle q,v_{i}\rangle}(t,\underline{y})\rightarrow s_{i}$ where ${\sf pref}_{o}(q)[s_{q},\ldots,s_{r}]=p[y_{i1},\ldots,y_{im}]$. Therefore,

[TABLE]

with $t\in{\sf dom}(\pi(q))={\sf dom}(\pi^{\prime}(q^{\prime}))$. Accordingly, for all input trees $t\in{\sf dom}(\pi(q))$ and parameter vectors $\underline{T}\in\mathcal{T}_{\Delta_{in}}^{l}$, $\llbracket M,A\rrbracket(t,\underline{T})=\llbracket M^{\prime},A^{\prime}\rrbracket(t,\underline{T})$.

Assume that $n$ is the number of states of $M$, and $D$ is the maximal size of a common $\Delta_{out}$-prefix. Thus $D$ is at most of the size of a right-hand side of a rule for a symbol of rank [math]. Then each state $q$ of $M$ gives rise to at most $n\cdot D$ states ${\langle q,v\rangle}$ of $M^{\prime}$ where each right-hand side of ${\langle q,v\rangle}$ is at most $D+1$ times the size of the corresponding right-hand side of $q$. Thus, the size of $M^{\prime}$ is polynomial in the size of $M$. Likewise, the axiom $A^{\prime}$ is only a factor of $D+1$ larger than the axiom $A$. Since the $\Delta_{out}$-prefixes of states of $M$ can be computed in polynomial time, the overall algorithm runs in polynomial time. ∎