Institute of Informatics,
University of Warsaw<EMAIL_ADDRESS>Janusz Schmude[100]Theory of
computation Formal languages and automata Supported by ERC Consolidator Grant
LIPA, agreement no. 683080.

###### Acknowledgements.

I would like to thank Mikołaj Bojańczyk for the support in obtaining the
results and writing this paper. I would also like to thank James Worrell,
Mahsa Shirmohammadi, Sandra Kiefer, Sławomir Lasota and Radosław Piórkowski
for helpful discussions.

# On polynomial grammars extended with substitution

Janusz Schmude

###### Abstract

We investigate decidability of equivalence of register transducers, also
called copyful Streaming String Transducers in case of string input, extended
with an operation of substituting a register for all occurrences of a given
letter in another register. We reduce to zeroness of polynomial grammars (over
ring of polynomials) extended with analogous substitution operation by
encoding strings into polynomials; a similar method was used successfully by
Seidl et al. in 2018. We give two restrictions under which register
transducers with substitution have decidable equivalence. They seem to be very
restrictive but on the other hand, they seem to be on the edge of the scope of
this “polynomial” method, as in the third result we give a rather restricted
model of polynomial grammars with substitution that has undecidable
equivalence.

###### keywords:

equivalence problem, register transducers, word substitution, polynomial
grammar

##  1 Introduction

Let us consider the following computation device that computes string-to-
string functions: it has two registers $R,S$ that store strings and reads
input words from left to right. It initializes the registers to empty words
and if the read letter is $a$, it updates the registers by putting
simultaneously

$\begin{cases}R:=a\cdot R,\\\ S:=R\cdot a.\end{cases}$

After input word is read, it outputs $R\cdot S$. For example, a run over input
word $w=abb$ is

$\\!\\!\begin{tabular}[]{c}$R=\varepsilon$\\\
$S=\varepsilon$\end{tabular}\\!\\!\xrightarrow{a}\\!\\!\begin{tabular}[]{c}$R=a$\\\
$S=a$\end{tabular}\\!\\!\xrightarrow{b}\\!\\!\begin{tabular}[]{c}$R=ba$\\\
$S=ab$\end{tabular}\\!\\!\xrightarrow{b}\\!\\!\begin{tabular}[]{c}$R=bba$\\\
$S=abb$\end{tabular}\\!\\!\rightarrow\text{output }bbaabb.$

This device computes function $w\mapsto\operatorname{rev}(w)\cdot w$, where
$\operatorname{rev}$ is the reverse function. Such a device is an instance of
a _register transducer_ [8] (in general, register transducers can compute
tree-to-string functions, however in all the examples we give string-to-string
functions, which are a special case where input trees are monadic). Sometimes
two register transducers defined in two different ways compute the same
function – the _equivalence problem_ asks, given two register transducers, if
this is the case. For example, the register transducers that compute,
respectively, the reverse and identity function are equivalent if and only if
the alphabet is unary.

There are several methods of deciding equivalence of register transducers e.g.
by use of an equivalent model of two-way transducers [11] or by reduction to
non-emptiness of one counter automata in case of _copyless_ register
transducers, which are called _Streaming String Transducers_ [1]. Method that
is close to one we use in this paper is by reduction to _zeroness problem_ for
_polynomial grammars_ [8].

Let us describe a variant of polynomial grammars that uses a free monoid
instead of a ring and explain how it is related to equivalence problem of
register transducers. It is a generalisation of context-free grammar, in which
each nonterminal is associated with some dimension $k$, and therefore outputs
$k$-tuples, and right-hand sides of production rules may use function symbols
to avoid introducing independent copies of a nonterminal. For example,
consider a polynomial grammar over $(\Sigma^{*},\cdot)$ with one nonterminal
$X$ of dimension 2 and production rules

$\displaystyle X\rightarrow\ p_{a}(X),$ $\displaystyle\
a\in\Sigma\mid(\varepsilon,\varepsilon),\text{where}$ $\displaystyle
p_{a}:(\Sigma^{*})^{2}\rightarrow$ $\displaystyle(\Sigma^{*})^{2}$
$\displaystyle p_{a}(w_{1},w_{2})=$ $\displaystyle\ (aw_{1},w_{2}a)\text{ for
}a\in\Sigma,w_{1},w_{2}\in\Sigma^{*}.$

By definition, its language consists of pairs
$p_{a_{n}}(p_{a_{n-1}}(\ldots(p_{a_{2}}(p_{a_{1}}(\varepsilon,\varepsilon)))\ldots))$
for $a_{1},\ldots,a_{n}\in\Sigma$. We define the _grammar equivalence problem_
, in the case the initial nonterminal is 2-dimensional, as follows: is the
first coordinate equal to the second coordinate for every produced pair?
Observe that equivalence holds for the mentioned grammar if and only if the
register transducers that compute, respectively, reverse and identity
function, are equivalent.

Register transducers considered in this paper are enriched with a substitution
operation, we call them _register transducers with substitution_. For example,
consider the function
$\operatorname{\texttt{sqrev}}:\Sigma^{*}\rightarrow(\Sigma\cup\\{\\#\\})^{*}$,
called _squared reverse_ (the definition and name are motivated by _iterated
reverse_ [6]), defined as follows:

$\operatorname{\texttt{sqrev}}:w\mapsto(\\#\cdot\operatorname{rev}(w))^{|w|}.$

It can be computed by two following register transducers with substitution
that initialize their registers on empty strings, output register $R$, and
have register updates as follows:

$\begin{cases}R:=\\#\cdot a\cdot S\cdot(R[\\#:=\\#\cdot a]),\\\ S:=a\cdot
S,\end{cases}\text{ for }a\in\Sigma$

and

$\begin{cases}R:=(R[\\#:=\\#\cdot a])\cdot\\#\cdot a\cdot S,\\\ S:=a\cdot
S,\end{cases}\text{ for }a\in\Sigma.$

To decide their equivalence, one may consider a _polynomial grammar with
substitution_ (again, over free monoid instead of a ring) with initial
nonterminal $Y$ of dimension 4: $Y\rightarrow
q_{a}(Y),a\in\Sigma\mid(\varepsilon,\varepsilon,\varepsilon,\varepsilon)$,
where $q_{a}(w_{1},w_{2},w_{3},w_{4})=(\\#\cdot a\cdot
w_{2}\cdot(w_{1}[\\#:=\\#\cdot a]),a\cdot w_{2},(w_{3}[\\#:=\\#\cdot
a])\cdot\\#\cdot a\cdot w_{4},a\cdot w_{4})$ and test for equivalence the
grammar $S_{1}\rightarrow\pi_{[1,3]}(Y)$, where $\pi_{I}$ is projection on
coordinates from $I$.

We are interested in decidability of grammar equivalence for such grammars.

We use the Hilbert Method [8], which relies on encoding objects manipulated by
transducers, like strings or trees, into rings e.g. of integers or of
polynomials; this is done in order to use algebraic geometry machinery. This
method has been used to prove decidability of equivalence for register
transducers without substitution, where strings were encoded into ring of
integers [14] (see also [8] for a slightly different encoding). In this paper
we use an analogous encoding (Definition 2.4), this time into ring of
polynomials, in order to cover substitution, thus reducing problem to
equivalence of _polynomial grammars with substitution_ over a ring of
polynomials. Equivalence is known to be undecidable for this model, even in a
rather restricted special case [5, Theorem 20]. In this paper we prove two
decidability results for other special cases and strengthen this
undecidability result, clarifying the scope of this “polynomial” approach.

Obtained decidability results transfer immediately to corresponding register
transducers. This is stated in Lemma 2.5 for unrestricted polynomial grammars
with substitution, which is a reduction to an undecidable problem, however, as
explained in Remark 2.6, reduction holds also for special cases, which are
decidable (Theorem 3.4 and Lemma 4.3).

Main results. The main problem discussed in this paper is _zeroness_ of
polynomial grammars with substitution over a ring of polynomials (Definition
2.3). First we discuss such grammars with an additional fixed bound on the
number of transitions per derivation that use substitution. We provide a
positive result (Theorem 3.4) and a negative one (Theorem 3.10). The negative
result is a strengthening of [5, Theorem 20], mentioned in the previous
paragraph. Then we move to grammars that use a special case of substitution –
evaluation. For this variant we give a positive result (Lemma 4.3) and
describe how it transfers to register transducers with substitution (Theorem
4.10).

##  2 Preliminaries

Polynomial functions. By a _ring_ we mean a commutative ring with unity. A
ring has _no zero divisors_ if for all non-zero $a,b\in R$, their
multiplication $a\cdot b$ is non-zero. Let $R$ be a ring, for example the ring
of integers. Following [8], it is convenient to define polynomial functions so
that they can return tuples. Tuples inputted by polynomials will be also
called _vectors_. A function

$p:R^{n}\rightarrow R^{k}$

for some $n,k\geq 0$ is a _polynomial function_ if every output coordinate is
represented by a polynomial in $n$ variables. For a set $V\subseteq R^{n}$, by
$p_{|_{V}}$ we denote function $p$ restricted to $V$.

Substitution. In the ring $R[X]$, substitution is a $(|X|+1)$ \- ary operation
defined as

$\displaystyle\operatorname{subs}$ $\displaystyle:R[X]\times
R[X]^{X}\rightarrow R[X]$ $\displaystyle\operatorname{subs}$
$\displaystyle(p,(q_{x})_{x\in X})=p[x:=(q_{x})_{x\in X}].$

We consider a vectorized variant of substitution:

$\displaystyle\operatorname{subs}^{Y}_{X}$ $\displaystyle:R[X]^{Y}\times
R[X]^{X}\rightarrow R[X]^{Y}$ $\displaystyle\operatorname{subs}^{Y}_{X}$
$\displaystyle((p_{y})_{y\in Y},(q_{x})_{x\in X})=(p_{y}(x:=q_{x},x\in
X))_{y\in Y}.$

If the arities are clear from the context, we simply write
$\operatorname{subs}(\overline{p},\overline{q}),$ or even

$\overline{p}(\overline{q}),$

where $\overline{p}=(p_{y})_{y\in Y}$ and $\overline{s}=(q_{x})_{x\in X}$ are
tuples of polynomials in $R[X]$.

Polynomial grammars. We define polynomial grammars following [8, Definition
2.1]. As opposed to the Introduction, we define them only for rings. Most of
the times it will be the ring of polynomials, although in the proof of Theorem
3.4 we also use other rings.

######  Definition 2.1.

A _polynomial grammar_ over ring $R$ consists of

  * •

finite set of _nonterminals_ with a distinguished _initial nonterminal_ , each
nonterminal with an associated _dimension_ $\in\\{0,1,2,\ldots\\}$, and

  * •

finite set of _production rules_ , each of form $X\rightarrow
p(Y_{1},\ldots,Y_{k})$ for $k=0,1,\ldots$ where $p:R^{n}\rightarrow R^{m}$ is
a polynomial function, $Y_{i}$ for $i=1,\ldots,k$ are nonterminals, and input
and output dimensions of expressions “match”, i.e. sum of dimensions of
$Y_{i}$’s, for $i=1\ldots l$, is equal to $n$, and dimension of $X$ is equal
to $m$.

If a nonterminal has dimension $n$, then it generates a subset of $R^{n}$,
which is defined as follows by induction. (The language generated by the
grammar is defined to be the subset generated by its initial nonterminal.)
Suppose that

$X\rightarrow p(Y_{1},...,Y_{k})$

is a production and we already know that vectors $v_{1},\ldots,v_{k}$ are
generated by nonterminals $Y_{1},...,Y_{k}$ respectively. Then the vector
$p(v_{1},\ldots,v_{k})$ is generated by nonterminal $X$. The induction base is
the special case of $k=0$, where the polynomial $p$ is a constant.

######  Example 2.2 (see Fig. 1).

Polynomial grammar

$A\rightarrow p(A)\mid 2$

with $p(a)=a\cdot a$ has language

$\\{2^{2^{n}}:n\in\mathbb{Z}_{+}\\}.$

A similar polynomial grammar,

$A\rightarrow A\cdot A\mid 2$

has language

$\\{2^{n}:n\in\mathbb{Z}_{+}\\}.$

We define the _dimension_ of a grammar to be the dimension of its initial
nonterminal. For simplicity, the language of a grammar $G$ with initial
nonterminal $A$ is sometimes denoted by $A$. For a polynomial function
$f:R^{n}\rightarrow R^{m}$, for a grammar $G$ with initial nonterminal $A$ of
dimension $n$, by $f(G)$ or $f(A)$ we denote a “canonical” grammar with
language $f(A)$, i.e. grammar build from $G$ by adding a fresh initial
nonterminal $S$ and a production $S\rightarrow f(A)$.

$\cdot$2$\cdot$22$A$$A$$A$$A$$A$$p$$p$2$A$$A$$A$ Figure 1: Example derivation
trees for grammars $A\rightarrow p(A)\mid 2$ with $p(a)=a\cdot a$ and
$A\rightarrow A\cdot A\mid 2$. They produce $8=2^{3}$ and, respectively,
$16=2^{2^{2}}$.

Polynomial grammars with substitution. Let $R$ be a ring. A _polynomial
grammar with substitution_ over $R[X]$ is an extension of polynomial grammar
over $R[X]$ where polynomials in production rules may use substitution
(additionally to $+$ and $\cdot$).

######  Definition 2.3.

For a polynomial grammar or a polynomial grammar with substitution $A$ over a
ring of polynomials, that has a non-empty language 111A technical assumption,
does not change the essence of the problem. Notice it can be checked easily -
it is enough to find productive nonterminals e.g. by fixpoint strategy. In
particular, the algorithm does not depend on the output algebra., _zeroness
problem_ asks if $L(A)=\\{0\\}$; we often abbreviate it to $A=0$.

String-to-polynomial encoding. The principal application of zeroness problem
is equivalence of register transducers; the latter can be reduced to the
former by the encoding we describe now.

######  Definition 2.4.

Consider the function $\Phi$ that maps strings over $\Sigma$ into pairs of
polynomials in variables from set $\widetilde{\Sigma}\cup\overline{\Sigma}$,
which are two disjoint copies of $\Sigma$, defined as follows:

$\displaystyle\Phi$ $\displaystyle:a_{1}\ldots
a_{n}\mapsto\left(\sum_{i=1}^{n}\overline{a_{1}}\cdot\ldots\cdot\overline{a_{i-1}}\widetilde{a_{i}},\quad\overline{a_{1}}\cdot\ldots\overline{a_{n}}\right).$
(1)

We denote first and second coordinate of $\Phi(w)$ by $\widetilde{w}$ and
$\overline{w}$, i.e.

$\Phi(w)=(\widetilde{w},\overline{w}).$ (2)

For example,
$\Phi(abbab)=(\widetilde{a}{\overline{b}}^{2}{\overline{a}}+\widetilde{b}{\overline{b}}^{2}{\overline{a}}+\widetilde{b}{\overline{b}}{\overline{a}}+\widetilde{a}{\overline{b}}+\widetilde{b},{\overline{a}}^{2}{\overline{b}}^{3})$.

The function $\Phi$ is a “generalisation222It is a generalisation in a sense,
that natural encoding is an evaluation of $\Phi$ at
$\widetilde{a}=\tau(a),\overline{a}=|\Sigma|$ for a bijection $\tau$ of
$\Sigma$ with $\\{0,1,\ldots,|\Sigma|-1\\}$” of a natural encoding of strings
into numbers they represent in $|\Sigma|$ -ary, i.e.
$w\mapsto(\operatorname{val}_{|\Sigma|}(w),|\Sigma|^{|w|})$ where
$\operatorname{val}_{|\Sigma|}(w)$ is the value of $w$ as a number in
$|\Sigma|$-ary (assuming some bijection of $\Sigma$ with
$\\{0,1,\ldots,|\Sigma|-1\\}$). We use this generalisation to be able to use
substitution.

Notice that $\Phi$ “commutes” with substitution , i.e.

$\Phi(w[a:=v_{a},a\in\Sigma])=\Phi(w)[\widetilde{a}:=\widetilde{v_{a}},\overline{a}:=\overline{v_{a}},a\in\Sigma]\text{
for }w,(v_{a})_{a\in\Sigma}\in\Sigma^{*}.$

We say that the polynomial substitution
$(\widetilde{a}:=\widetilde{v_{a}},\overline{a}:=\overline{v_{a}})_{a\in\Sigma}$
is _induced by_ the word substitution $(a:=v_{a})_{a\in\Sigma}$.

Using the encoding above, we obtain the following lemma.

######  Lemma 2.5.

Equivalence of register transducers with substitution over $\Sigma^{*}$ can be
reduced to zeroness of polynomial grammars with substitution over
$\mathbb{Q}[\widetilde{\Sigma}\cup\overline{\Sigma}]$.

######  Remark 2.6 (Undecidability in Lemma 2.5).

Let us emphasize that even though in Lemma 2.5 we have a reduction to an
undecidable problem, it remains valid for special cases of this problem that
are decidable – Theorem 3.4 and Lemma 4.3. As corollaries we obtain,
respectively, result from beginning of Section 3.3 and Theorem 4.10.

######  Proof 2.7 (Proof sketch of Lemma 2.5).

Suppose that we have two register transducers with substitution that compute
string-to-string functions $f,g:\Sigma^{*}\rightarrow\Sigma^{*}$. We can
convert them into a polynomial grammar $G$ over
$\mathbb{Q}[\widetilde{\Sigma}\cup\overline{\Sigma}]$ that produces pairs of
polynomials $(\widetilde{f(w)},\widetilde{g(w)})$ for input words $w$. It can
be done us using the fact that

$\Phi(w\cdot v)=p(\Phi(w),\Phi(v))$

for some polynomial function $p$ – indeed, for any words $w,v$ we have
$\widetilde{wv}=\widetilde{w}\cdot\overline{v}+\widetilde{v}$ and
$\overline{wv}=\overline{w}\cdot\overline{v}$ or explicitly

$p(x_{1},x_{2},y_{1},y_{2})=(x_{1}y_{2}+y_{1},x_{2}y_{2})$

– and that $\Phi$ “commutes” with substitution (see Definition 2.4). Applying
polynomial function $p(x_{1},x_{2})=x_{1}-x_{2}$ to $G$ results in grammar
$p(G)$ for which zeroness holds if and only if $f,g$ are equivalent.

###  2.1 Fields, algebraic sets

A _field_ is a ring in which every non-zero element has an inverse. Let $K$ be
a field. By $K[X]$ we denote the ring of polynomials over set of variables
$X$. By $K(X)$ we denote the field of rational functions over $X$, i.e.
$K(X)=\\{\frac{p}{q}\ |\ p,q\in K[X],q\neq 0\\}$.

A field is a _computable field_ if its elements can be enumerated such that
operations $+,\cdot$ are computable functions.

A field $K$ is _algebraically closed_ , if every univariate polynomial with
coefficients in $K$ has a root in $K$. An _algebraic closure_ of a field $K$,
denoted by $\overline{K}$, is, roughly speaking, the smallest algebraically
closed field that contains $K$. Typical examples of algebraically closed
fields are (1) the field of complex numbers, which is algebraic closure of
field of real numbers and (2) the field of algebraic numbers, which is
algebraic closure of field $\mathbb{Q}$.

Introducing algebraic closures does not affect effectiveness:

######  Lemma 2.8.

([13, Theorem 7]) Let $K$ be a given computable field. Then one can compute an
embedding $K\subset\overline{K}$, which moreover is a computable function. In
particular, $\overline{K}$ is a computable field and it can be computed, given
$K$.

By an _ideal_ we mean a subset $I$ of $K[X]$ in which $f,g\in I$ implies
$f+g\in I$ and $f\in I,p\in K[X]$ implies $f\cdot p\in I$, for all polynomials
$f,g,p$. For a set of polynomials $F$, by $\langle F\rangle$ we denote set
$\\{r_{1}f_{1}+r_{2}f_{2}+\ldots+r_{k}f_{k}\mid f_{i}\in F,r_{i}\in K[X],k\geq
0\\}$; this is the smallest ideal that contains set $F$ called _ideal
generated by $F$_; elements of $F$ are called _generators_ of $\langle
F\rangle$. Ideals can be represented in a finite way, as shown by Hilbert’s
Basis Theorem.

######  Fact 1.

(Hilbert’s Basis Theorem, [10, Chapter 2, §5, Theorem 5]). Let $K$ be a field.
Every ideal in $K[X]$ can be generated by a finite set of polynomials.

Let $K$ be a field. An _algebraic set_ is a subset of $K^{n}$ which is a set
of zeros of some set of polynomials in $n$ variables, i.e. is of form $\\{v\in
K^{n}\ |\ p(v)=0\text{ for all }p\in F\\}$ for some set of polynomials
$F\subseteq K[X]$. For an algebraic set $V$, by $I(V)$ we denote the set of
all polynomials that are zero on $V$; this is an ideal. For a ideal $I$ in
$K[X]$, by $V(I)$ we denote the set of common zeros of all polynomials of $I$;
this is a variety. We say that $V(I)$ is _represented_ by $I$. Every algebraic
set can be represented by some ideal, for example by $I(V)$; this, together
with Hilbert’s Basis Theorem (Fact 1), provides a way to represent algebraic
sets in a finite way.

From this we conclude the following.

######  Corollary 2.

Let $K$ be a computable field. Then algebraic sets can be enumerated.

A _coordinate ring_ of an algebraic set $V\subseteq K^{n}$ is the ring of
polynomial functions from $V$ to $K$. An algebraic set is called an
(irreducible) _variety_ if it cannot be represented as a finite union of
pairwise distinct algebraic sets.

######  Remark 2.9 (Notation: does algebraic set = variety?).

Different sources introduce different names for algebraic sets. For example,
in [10] they are called varieties, and what we call a variety is called an
irreducible variety. To avoid confusion, we always precede word “variety” with
“(irreducible)”.

######  Lemma 2.10.

([10, Chapter 4, §6, Theorem 2 and remarks at the end of Chapter 4, §6 ]) Let
$K$ be a computable field. Then every algebraic set can be effectively
decomposed into (irreducible) varieties.

######  Lemma 2.11.

([10, Chapter 4, §5, Proposition 3]) An algebraic set is an (irreducible)
variety if and only if its coordinate ring has no zero divisors.

##  3 Polynomial grammars with a bounded number of substitutions

In this section we discuss decidability of zeroness problem for polynomial
grammars with substitution over a ring of polynomials with the following
restriction: substitution operation can be used once per derivation. We call
this model _polynomial grammar with one substitution_. Let us recall that
zeroness is decidable in case of no substitutions.

######  Lemma 3.1 ([7], Theorem 15).

Let $R$ be a computable ring with no zero divisors. Then equivalence is
decidable for polynomial grammars over $R$.

Let us define the main decision problem of this section, which generalises
zeroness of polynomial grammars without substitution.

Zeroness of independent substitution of polynomial grammars
Input:
$R$ \- _a computable ring with no zero divisors_ ,
$X$ \- _finite set of variables_ ,
$A$ \- _polynomial grammar over ring $R[X]$_,
$B$ \- _polynomial grammar over ring $R$_
Question: _Is it the case that for all $a\in A,b\in B$_ $a(b)=0?$
We often abbreviate the statement above to

$A(B)=0.$

This problem can be seen as a special case of zeroness of polynomial grammars
with one substitution, for grammars of the form $\operatorname{subs}(A,B)$,
where $A,B$ are polynomial grammars. We call such substitution _independent_
because tuples of substituted values come from a different nonterminal than
polynomials to which they are substituted, and therefore they are produced
independently; we prove this problem decidable in Theorem 3.4. As we will see
in Section 3.2, in case of _dependent_ substitution, the problem is
undecidable.

######  Example 3.2.

Consider a polynomial grammar $A$ over ring of polynomials in two variables
$\widetilde{x},\overline{x}$ with coefficients in
$\mathbb{Q}(\widetilde{a},\overline{a})$, i.e.
$(\mathbb{Q}(\widetilde{a},\overline{a}))[\widetilde{x},\overline{x}]$ defined
as $A\rightarrow m(S),S\rightarrow p(S)\mid(0,1,0,1)$ where
$m(\widetilde{r},\overline{r},\widetilde{s},\overline{s})=\widetilde{r}-\widetilde{s}$
and
$p(\widetilde{r},\overline{r},\widetilde{s},\overline{s})=(\widetilde{r}\cdot\overline{x}\cdot\overline{a}+\widetilde{x}\cdot\overline{a}+\widetilde{a},\overline{r}\cdot\overline{x}\cdot\overline{a},\widetilde{x}\cdot\overline{s}\cdot\overline{a}+\widetilde{s}\cdot\overline{a}+\widetilde{a},\overline{x}\cdot\overline{s}\cdot\overline{a})$
and a polynomial grammar $B$ over ring of polynomials in two variables
$\widetilde{a},\overline{a}$ and coefficients in $\mathbb{Q}$, i.e.
$\mathbb{Q}[\widetilde{a},\overline{a}]$ defined as $B\rightarrow
q(B)\mid(0,1)$ where
$q(\widetilde{t},\overline{t})=(\widetilde{t}\cdot\overline{a}+\widetilde{a},\widetilde{t}\cdot\overline{a}$).
Then $A(B)=0$.

######  Remark 3.3.

The above Example expresses the fact, under our string-to-polynomial encoding,
that $(xa)^{n}=x^{n}a^{n}$ for all words $x\in\\{a\\}^{*}$, for all $n\geq 0$.

Remark on algebraic closure. Let us discuss a subtlety before we state and
prove Theorem 3.4. Despite the fact that all polynomials arising from our
string-to-polynomial encoding are elements of field
$\mathbb{Q}(\widetilde{\Sigma}\cup\overline{\Sigma})$, we carry out the proof
for algebraically closed fields. It does not affect generality, as every field
can be effectively embedded into algebraically closed field (Lemma 2.8). We do
so because it makes the description of the algorithm more readable, as in such
case one can compute the coordinate ring of a given algebraic set (Lemma
A.12); however, we present a version of the proof that does not use the notion
of algebraic closure in Section A.3.

We conjecture that the algorithm from Theorem 3.4 does _not_ have to use
elements of $\overline{K}$ that are not in $K$ – in consequence, the decision
of introducing algebraic closure would affect only the high-level description
of the algorithm, not the algorithm itself. This might be important when
trying to obtain a feasible complexity for a special case (recall in general
zeroness of polynomial grammars over a ring is Ackermann-hard [3, Theorem 1]).

###  3.1 Zeroness of independent substitution of polynomial grammars:
decidability

In this section we prove Theorem 3.4.

######  Theorem 3.4.

Let $R$ be a computable ring with no zero divisors. Then zeroness of
independent substitution of polynomial grammars over $R[X]$ is decidable.

As stated in Remark 2.6, the reduction from Lemma 2.5, restricted to the
special case from Theorem 3.4, yields decidability of the corresponding
problem for register transducers (Section 3.3).

The proof is based on the proof of [14, Corollary 8.2] in the presentation of
[8].

######  Proof 3.5 (Proof of Theorem 3.4).

Without loss of generality we may assume that grammar $A$ is of dimension 1
(notice we cannot assume it for $B$). In this proof, by abuse of notation, we
identify a polynomial grammar $A$ with its the language. We treat $A$ and $B$
as polynomial grammars over a computable algebraically closed field that
contains $R$, for example algebraic closure of its field of fractions.

There is a clear semi-procedure for non-zeroness – it essentially amounts to
enumerating all derivations. In rest of the proof, we show a semi-procedure
for zeroness.

Observe that $A(B)=0$ if and only if for some algebraic set $V$:

$\begin{cases}B\subseteq V\text{ (i) and}\\\ A_{|_{V}}=0\text{
(ii)},\end{cases}$

where $A_{|_{V}}$ denotes set $\\{f_{|_{V}}\mid f\in A\\}$. Indeed – for
example, as $V$, one may take $V(A)$. The semi-procedure for equivalence is as
follows: guess, by infinite enumeration (see Corollary 2), an algebraic set
$V$ and test conditions (i) and (ii), which can be done the following way.

######  Sublemma 1.

For a given $V$, condition (i) can be tested effectively.

######  Proof 3.6.

Condition (i) reduces to zeroness of polynomial grammars in the following way.
Denote by $I$ the ideal that $V$ is represented by. Observe that $B\subset
V(I)=V$ if and only if $f(B)=0$ for all generators $f$ of $I$.

######  Sublemma 2.

For a given $V$, condition (ii) can be tested effectively.

######  Proof 3.7 (Proof sketch).

Decompose $V$ into (irreducible) varieties $V=V_{1}\cup V_{2}\cup\ldots\cup
V_{k},\ \\!\\!k\geq 1$ (see Lemma 2.10). Then $A_{|_{V}}=0$ holds iff
$A_{|_{V_{i}}}=0\text{ for }i=1,\ldots,k$. Observe that $A_{|_{V_{i}}}=0$ is
equivalent to zeroness of $A$, treated as a polynomial grammar over coordinate
ring of $V_{i}$ (see Lemma A.12 for effectiveness); it has no zero divisors
(Lemma 2.11) and hence decidability follows from Lemma 3.1.

Generalisation. An analogous problem can be defined for arbitrary number of
grammars; for $k$ grammars, we will abbreviated it to
$A_{1}(A_{2}(\ldots(A_{n-1}(A_{k}))))=0$. Let us sketch the proof of its
decidability – it is very similar to the proof of case $n=2$. Observe that
$A_{1}(A_{2}(A_{3}(\ldots(A_{n})\ldots)))=0$ is equivalent to
$A_{2}(A_{3}(\ldots(A_{n})\ldots))\subseteq V$ and ${A_{1}}_{|_{V}}=0$ for
some algebraic set $V$. For a given $V$, first condition is equivalent to
$f(A_{2}(A_{3}(\ldots(A_{n})\ldots)))=0$ for generators $f$ of ideal that $V$
is represented by – this is decidable by induction assumption for $n-1$
polynomial grammars $f(A_{2}),A_{3},\ldots,A_{n}$. Second condition was proven
decidable in Sublemma 2.

######  Remark 3.8.

For any polynomial grammar $A$ there always exists a _finite_ set of
polynomials $F$ such that $A(v)=0$ if and only if $F(v)=0$, for every vector
$v$. In particular $A(B)=0$ if and only if $F(B)=0$. Given a finite set of
polynomials $F$, $F(B)=0$ can be decided (Lemma 3.1). However, it is not clear
how to compute such set $F$ given grammar $A$.

######  Remark 3.9.

Let $A,B$ be polynomial grammars. If the grammar $A$ is linear, i.e. there is
at most one nonterminal on the right-hand side of every production rule, then
grammar $A(B)$ can be seen as a polynomial grammar too – it is enough to
“concatenate” those two grammars by replacing production rules of grammar $A$
of form $nonterminal\rightarrow constant$ with $nonterminal\rightarrow B$.
However in case $A$ is not linear, it is not clear how to convert $A(B)$ to a
polynomial grammar.

###  3.2 Polynomial grammar with one substitution: undecidability

In previous section we saw that restriction to one _independent_ substitution
per derivation yields decidability of zeroness. In this section we show that
in general case of one _dependent_ substitution, this problem is undecidable.
We call such substitution dependent because substituted tuples and polynomials
to which they are substituted may come from the same nonterminal and hence be
generated dependently.

######  Theorem 3.10.

Zeroness of polynomial grammars with one substitution over $\mathbb{Z}[x]$ is
undecidable.

In contrast to Theorem 3.4, the reduction from Lemma 2.5 restricted to special
case from Theorem 3.10 does _not_ yield decidability nor undecidability of
analogous problem for register transducers.

The proof was suggested by Lasota and Piórkowski [12]. It is analogous to
proof of [5, Theorem 17], except two-counter machines are replaced by reset
VASS-es; used encoding of reset VASS into register transducer is similar to
[4, Example 3].

By a _VASS_ we mean a Vector Addition System with States. We call vectors that
describe transitions _step vectors_. By a _reset VASS_ we mean an extension of
VASS where transitions may also reset some of coordinates to 0. By a _unit
step vector_ we mean a step vector of form $(0,0,\ldots,0,1,0,\ldots,0)$. For
a reset VASS, by $\mathbf{0}$ we denote vector of zeros of its dimension.

######  Proof 3.11 (Proof sketch).

We show a reduction from reachability in reset VASS, which is known to be
undecidable [2, Theorem 5]. Without loss of generality assume it is
reachability from $\mathbf{0}$ to $\mathbf{0}$ and step vectors are unit –
this ensures that sum of coordinates is an integer from interval $[0,n]$ after
$n$ steps of a valid run. Given a reset VASS $\mathcal{V}$ we construct a
register transducer with substitution _over ring $\mathbb{Z}[x]$_ that uses
substitution only in the output transition (hence once per run) such that
$\mathcal{V}$ can reach $\mathbf{0}$ from $\mathbf{0}$ if and only if the
register transducer returns a non-zero output on some input (such register
transducers are a different formalism for the same model as polynomial
grammars with one substitution).

We describe the construction. The transducer takes a sequence of transitions
of $\mathcal{V}$ as an input (this is a word over finite alphabet), which may
describing a (valid) run of $\mathcal{V}$ or not. The state of the transducer
is the state of $\mathcal{V}$ and turns to error state if in the input word
the states of some pair of consecutive transitions do not match. The
transducer holds the counter values of $\mathcal{V}$ in registers that we call
_counter registers_. It has an _error register_ which turns 0 when an “error”
occurs, i.e. some coordinate of $\mathcal{V}$ goes below 0 (note that step
vectors are unit so such coordinate equals $-1$) and holds 0 for the rest of
the run – this is achieved by multiplying the error register by the product of
values of counter registers, each value incremented by 1, in each update.
There is a _reachability test register_ that holds a polynomial
$(x-1)(x-2)\ldots(x-n)$ after $n$ steps (formally, to construct it one needs
an _auxiliary register_ that holds number $n$); it has a property that, for an
integer input from interval $[0,n]$, it evaluates to 0 if and only if the
input number is non-zero. Finally, if the state is accepting, in output
transition the transducer returns error register multiplied by reachability
test register evaluated at the sum of counter registers (this involves
substitution of a register into another register); observe this is a non-zero
number if and only if input word is a (valid) run of $\mathcal{V}$ and this
run reaches $\mathbf{0}$ from $\mathbf{0}$. We give details of the
construction in Section A.2.

###  3.3 Interpretation of Theorem 3.4 and Theorem 3.10 as testing infinitely
many equations on a language generated by a register transducer

Consider a register transducer $E$ that returns pairs of words over alphabet
$\Delta\cup X$ and a register transducer $T$ that returns $X$-tuples of words
over $\Delta$. Transducer $E$ can be interpreted as a generator of equations
(constraints) and $T$ as generator of tuples to be tested. Then Theorem 3.4
states that it is decidable if all tuples of words generated by $T$ satisfy
all equations generated by $E$. On the other hand, Theorem 3.10 states that,
in case when polynomials and integers are generated, it is undecidable for a
polynomial grammar that generates “pairs” (equation, tuple of vectors) if the
“second” coordinate is always a solution for the “first” one (formally, the
numbers of mentioned coordinates differ as e.g. an equation alone requires two
coordinates). In such interpretation, words “independent” and “dependent”
describe the relationship between equations and tested tuples. We include a
formal presentation in Section A.1.

##  4 Polynomial grammars with evaluations

In previous section we considered polynomial grammars with restricted number
of uses of substitution per derivation. Another way of restricting
substitution is to consider evaluations – instead of adding general ($1+|X|$)
- ary substitution operation

$\operatorname{subs}:K(X)\times K(X)^{X}\rightarrow K(X)$

we add _evaluations_ , which are substitutions where the argument from
$K(X)^{X}$ is fixed, i.e. unary operations

$\displaystyle\operatorname{eval}_{v}:K(X)\rightarrow K(X),$
$\displaystyle\operatorname{eval}_{v}(p)\mapsto p(v),$

for vectors $v\in K(X)^{X}$. We call this restriction of polynomial grammars
with substitution _polynomial grammars with evaluations_.

In this section we prove Theorem 4.10 that states that polynomial grammars
with evaluations that satisfy simultaneous automorphism condition (Definition
4.2) have decidable zeroness. The core technical ingredient is Lemma 4.3,
which is a result of discussions with Bojańczyk, Worrell, Shirmohammadi and
Kiefer [9], allows to use simultaneous field automorphisms in polynomial
grammars over a field. Lemma 4.8 gives an easy-to-check characterisation of
word substitutions that are mapped to field automorphisms by the string-to-
polynomial encoding from Definition 2.4. Theorem 4.10 concludes those two
lemmas.

###  4.1 Polynomial grammar with simultaneous automorphisms: decidable
equivalence.

######  Definition 4.1.

Let $R$ be a ring. An _automorphism_ of $R$ is a bijective function
$h:R\rightarrow R$ that satisfies $h(\eta(a,b))=\eta(h(a),h(b))$ for $\eta$
being either addition or multiplication for every $a,b\in R$. For example,
evaluation $\operatorname{eval}_{v}$ for $v=x+1$, i.e.

$\mathbb{Q}(x)\ni f\mapsto f[x:=x+1]\in\mathbb{Q}(x)$

is an automorphism of the field $\mathbb{Q}(x)$. An automorphism of product of
fields $K^{n}$ is called _simultaneous_ if it is of form
$\alpha^{n}=\underbrace{(\alpha,\alpha,\ldots,\alpha)}_{n}$ for some
automorphism $\alpha$ of $K$.

######  Definition 4.2.

A _polynomial grammar with simultaneous automorphisms/evaluations_ is an
extension of polynomial grammar over a field where production rules are of
form $Y\rightarrow p(\alpha^{N}(Y_{1},\ldots Y_{n}))$ where $\alpha$ is a
field automorphism/an evaluation and $N=\dim Y_{1}+\ldots+\dim Y_{n}$.

######  Lemma 4.3.

Let $K$ be a computable field. Then polynomial grammars with simultaneous
automorphisms over $K$ have decidable equivalence.

Similarly as for Theorem 3.4, the reduction from Lemma 2.5, restricted to the
special case from Lemma 4.3, yields decidability of equivalence for certain
class of register transducers with substitution (Theorem 4.10).

######  Proof 4.4 (Proof of Lemma 4.3).

A proof analogous to proof of Lemma 3.1 can be performed for polynomial
grammars with simultaneous automorphisms – it is enough to show that preimage
of an algebraic set by simultaneous automorphism of $K$ is effectively an
algebraic set (note that this fact holds for any algebra, with the same proof
as for fields).

Let $\alpha$ be an automorphism of $K$; by abuse of notation, denote the same
way coordinate-wise application of it. Then
$\alpha^{-1}(V({p}_{1},\ldots,{p}_{n}))=V(p_{1}\circ\alpha,\ldots,p_{n}\circ\alpha)$.
Functions $p_{i}\circ\alpha$ might not be polynomial, however for a polynomial
$p({x}_{1},\ldots,{x}_{n})=\sum_{i=0}^{n}a_{i}x^{i}$ equality
$(p\circ\alpha)({x}_{1},\ldots,{x}_{n})=0$ is equivalent to a polynomial
equation $\sum_{i=0}^{n}\alpha^{-1}(a_{i})x^{i}=0$.

######  Definition 4.5.

We call a word substitution $p:\Sigma\rightarrow\Sigma^{*}$ _com-injective_ if
$w\mapsto p(w)$ is injective, when treated as a mapping of commutative words.

By abuse of notation, we also denote as com-injective a polynomial
substitution, which is an image of com-injective word substitution by our
string-to-polynomial encoding.

######  Lemma 4.6.

If $p$ is a substitution for one letter, call it $\sigma$, (in other words,
$p$ is an identity function on all letters except $\sigma$) and it does not
vanish letter $\sigma$, then it is com-injective. Example of such substitution
is $p:a\mapsto bacbaab$. A non-example of such substitution is $p:a\mapsto
bbc$.

######  Proof 4.7.

Straightforward.

In the following lemma we characterise word substitutions that induce field
automorphisms via our string-to-polynomial encoding. Finding such word
substitutions is challenging, as almost no word substitution induces an
automorphism of field $\mathbb{Q}(\widetilde{\Sigma}\cup\overline{\Sigma})$.
However, a reasonably large class of word substitutions induces automorphisms
of the field $\mathbb{Q}(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq
0}},a\in\Sigma)$, an extension of
$\mathbb{Q}(\widetilde{\Sigma}\cup\overline{\Sigma})$ that is defined below.

Notions of a polynomial and a rational function, considered as formal
expressions, can be extended to situation where some of variables have
exponents from an arbitrary infinite monoid, that can be embedded in some
group – “ordinary” polynomials use monoid $(\mathbb{N},+,0)$. We use this
extension with monoid $(\mathbb{Q}_{\geq 0},+,0)$. Let $K$ be a field. By
$K[\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq 0}},a\in\Sigma]$ we denote the
ring of polynomials over variables $\widetilde{\Sigma}\cup\overline{\Sigma}$
where variables $\overline{\Sigma}$ have exponents in $(\mathbb{Q}_{\geq
0},+,0)$ and by $K(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq
0}},a\in\Sigma)=\\{\frac{p}{q}\ |\ p,q\in
K[\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq 0}},a\in\Sigma],q\neq 0\\}$ the
corresponding field of rational functions; let us emphasize that the latter
contains elements with negative exponents as well, e.g.
${\overline{a}}^{-1/2}=\frac{1}{{\overline{a}}^{1/2}}$.

A subtlety. There is a subtlety regarding defining evaluations. In field
$K(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq 0}},a\in\Sigma)$, as opposed
to $K(\widetilde{\Sigma}\cup\overline{\Sigma})$, evaluation is _not_ defined
for every vector: for it to do so, it must evaluate variables from
$\overline{\Sigma}$ on monomials in variables from $\overline{\Sigma}$;
however polynomial substitutions induced by word substitutions via our word-
to-polynomial encoding have that property.

######  Lemma 4.8.

Com-injective word substitutions induce automorphisms of field
$\mathbb{Q}(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq 0}},a\in\Sigma)$.
Non-com-injective word substitutions do not induce automorphisms of any field
that contains $\mathbb{Q}(\widetilde{\Sigma}\cup\overline{\Sigma})$.

######  Corollary 3.

Grammar $Y$ from Introduction is a polynomial grammar with simultaneous
automorphisms via our string-to-polynomial encoding.

######  Proof 4.9.

Substitutions in the grammar are simultaneous – both register transducers
apply the same word substitutions at the same steps on all of their registers
(notice that update of register $S$ does not use substitution explicitly, but
it could with no difference, as strings stored in $S$ do not contain symbol
$\\#$, for which the substitution is performed). They are com-injective 4.6
and hence induce automorphisms (Lemma 4.8).

From Lemma 4.8 one can conclude Theorem 4.10.

######  Theorem 4.10.

Register transducers with simultaneous evaluations of com-injective
substitutions have decidable equivalence.

######  Proof 4.11.

Due to Lemma 4.8, the corresponding polynomial grammar with evaluations is a
polynomial grammar with simultaneous automorphisms, when considered over the
field $\mathbb{Q}(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq
0}},a\in\Sigma)$. Its zeroness is decidable due to Lemma 4.3.

Now we give a proof of Lemma 4.8 for an example substitution, in order to to
avoid unnecessary formalism; the proof idea is the same in the general case,
for which we give a proof in Section A.4.

######  Proof 4.12 (Proof of Lemma 4.8 for an example substitution).

Let $\Sigma=\\{a,b\\}$. Consider a substitution of words $p:a^{*}\rightarrow
a^{*}$ defined as $p:a\mapsto aa$. Then induced substitution of polynomials is
$p^{\prime}:\widetilde{a}\mapsto\widetilde{a}\overline{a}+\widetilde{a},\overline{a}\mapsto\overline{a}^{2}.$
This substitution is not invertible when considered in the field
$\mathbb{Q}(\widetilde{\Sigma}\cup\overline{\Sigma})$, however we show it is
invertible when considered in the field
$\mathbb{Q}(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq 0}},a\in\Sigma)$. To
find the inverse substitution, we consider a system of equations:

$\displaystyle\begin{cases}\widetilde{a}^{\prime}=\widetilde{a}\cdot(\overline{a}+1),\\\
\overline{a}^{\prime}=\overline{a}^{2}.\end{cases}$ (3)

Second equation is purely in variable $\overline{a}$, hence we solve it first;
it is a linear equation, where the exponents play the role of coefficients
from the field $\mathbb{Q}$. We get
$\overline{a}={\overline{a}^{\prime}}^{1/2}.$ We substitute this into the
first equation and get
$\widetilde{a}^{\prime}=\widetilde{a}\cdot({\overline{a}^{\prime}}^{1/2}+1),$
This is a linear equation in variable $\widetilde{a}$ with coefficients in the
field
$\mathbb{Q}(\widetilde{a}^{\prime},{\overline{a}^{\prime}}^{\mathbb{Q}_{\geq
0}})$. Solving it, we obtain
$\widetilde{a}=\frac{\widetilde{a}^{\prime}}{1+{\overline{a}^{\prime}}^{1/2}}.$
This shows that substitution
$\widetilde{a}\mapsto\frac{\widetilde{a^{\prime}}}{1+{\overline{a}^{\prime}}^{1/2}},\overline{a}\mapsto{\overline{a^{\prime}}}^{1/2}$
is the right-inverse of $p$. It is a two-sided inverse because the equations
are linear (in the mentioned sense). This finishes the proof for this example.

######  Remark 4.13.

Let us notice that for some grammars, Theorem 4.10 can be reduced to zeroness
of polynomial grammars _without_ substitution by simply removing the
automorphisms from production rules – for example this is the case when
polynomial functions used in productions have integer coefficients. However
this is not true in general when “new” occurrences of substitutable constants
are introduced in the productions. For example, consider polynomial grammar
with substitution over $\mathbb{Q}[a,b]$ with production rules

$S\rightarrow p(X),X\rightarrow q(Y),Y\rightarrow a-b,$

where $p,q:\mathbb{Q}[a,b]\rightarrow\mathbb{Q}[a,b]$ are defined as
$p(f)=f+b,q(f)=f[b:=a+b]$. Then $S=0$, but if automorphisms were removed, we
would have $S=a$.

##  5 Summary, future work

Theorem 3.10 draws a rather pessimistic view on polynomial grammars with
substitution over ring of polynomials – even almost the simplest model has
undecidable zeroness. In this paper we show positive results when the model is
restricted either to independent substitution (Theorem 3.4) or to evaluations
(Theorem 4.10). Theorem 3.4 can be interpreted as decidability of testing
infinite systems of equations on languages, where both the system and the
language can be generated by register transducers (Section 3.3). Theorem 4.10
seems to have large limitations: first, every evaluation must be
“simultaneous” i.e. in each production the same evaluation has to be applied
to all coordinates of all nonterminals at once, second, this evaluations needs
to induce a field automorphism, which excludes evaluations that vanish letters
as they are not an injective. Having said that, in Introduction we define
grammar $Y$ that satisfies both these conditions and can be used to decide
equivalence of two register transducers (also defined in Introduction) that
compute function $\operatorname{\texttt{sqrev}}$ .

Finally, we ask open questions. First one is about expressiveness of register
transducers with evaluations (no automorphism condition).

  1. 1.

What are other interesting string-to-string functions computed by register
transducers with evaluations whose evaluations are not allowed to vanish
letters?

Function similar to $\operatorname{\texttt{sqrev}}$, that maps each word $w$
to $\operatorname{rev}(w)^{|w|}$ seems not to be an example, as it seems to
require introducing symbol $\\#$ in a way analogous to
$\operatorname{\texttt{sqrev}}$ and then vanishing it.

Also, it is interesting what problems about register transducers are
decidable, in particular:

  1. 2.

Is equivalence undecidable?

  2. 3.

Is equivalence decidable if we restrict to register transducers with
evaluations (this question could be asked also for polynomial grammars)?

## References

  * [1] Rajeev Alur.  Streaming string transducers.  In Lev D. Beklemishev and Ruy de Queiroz, editors, Logic, Language, Information and Computation, pages 1–1, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.
  * [2] Toshiro Araki and Tadao Kasami.  Some decision problems related to the reachability problem for petri nets.  Theoretical Computer Science, 3(1):85–104, 1976.  URL: https://www.sciencedirect.com/science/article/pii/0304397576900670, doi:https://doi.org/10.1016/0304-3975(76)90067-0.
  * [3] M. Benedikt, T. Duff, A. Sharad, and J. Worrell.  Polynomial automata: Zeroness and applications.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, 2017.  doi:10.1109/LICS.2017.8005101.
  * [4] M. Benedikt, T. Duff, A. Sharad, and J. Worrell.  Polynomial automata: Zeroness and applications.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, 2017.  doi:10.1109/LICS.2017.8005101.
  * [5] Adrien Boiret, Radoslaw Piórkowski, and Janusz Schmude.  Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method".  In Sumit Ganguly and Paritosh Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), volume 122 of Leibniz International Proceedings in Informatics (LIPIcs), pages 48:1–48:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  URL: http://drops.dagstuhl.de/opus/volltexte/2018/9947, doi:10.4230/LIPIcs.FSTTCS.2018.48.
  * [6] Mikołaj Bojańczyk.  Polyregular functions, 2018.  arXiv:1810.08760.
  * [7] Mikołaj Bojańczyk and Janusz Schmude.  Some Remarks on Deciding Equivalence for Graph-To-Graph Transducers.  In Javier Esparza and Daniel Kráľ, editors, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), volume 170 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1–19:14, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2020/12752, doi:10.4230/LIPIcs.MFCS.2020.19.
  * [8] Mikołaj Bojańczyk.  The hilbert method for transducer equivalence.  ACM SIGLOG News, 6(1):5–17, February 2019.  URL: https://doi.org/10.1145/3313909.3313911, doi:10.1145/3313909.3313911.
  * [9] Mikołaj Bojańczyk, James Worrell, Mahsa Shirmohammadi, and Sandra Kiefer.  Personal communication.
  * [10] David Cox, John Little, and Donal O’Shea.  Ideals, Varieties, and Algorithms. An Introduction to Computational Algebraic Geometry and Commutative Algebra.  Fourth edition edition, 2015.  doi:10.1007/978-3-319-16721-3.
  * [11] Eitan M. Gurari.  The Equivalence Problem for Deterministic Two-Way Sequential Transducers is Decidable.  SIAM J. Comput., 11(3):448–452, 1982.
  * [12] S. Lasota and R. Piórkowski.  Personal communication.
  * [13] Michael O. Rabin.  Computable algebra, general theory and theory of computable fields.  Transactions of the American Mathematical Society, 95(2):341–360, 1960.  URL: http://www.jstor.org/stable/1993295.
  * [14] Helmut Seidl, Sebastian Maneth, and Gregor Kemper.  Equivalence of deterministic top-down tree-to-string transducers is decidable.  J. ACM, 65(4), April 2018.  doi:10.1145/3182653.

##  Appendix A Appendix

###  A.1 Formal presentation of Section 3.3

In this section we give a formal presentation of the problem presented in
Section 3.3. For a polynomial grammar $A$, by abuse of notation we identify it
with its language. We represent equations as a pair of polynomials, denoted as
$e=(e_{1},e_{2})$; a potential solution $v$ is a vector of polynomials; $v$ is
a solution of $e$ iff $e_{1}(v)=e_{2}(v)$.

Independent equation satisfiability
Input:
$\Delta$ \- _finite alphabet_ ,
$X$ \- _finite set of variables_ ,
$E\subseteq((\mathbb{Q}[\Delta])[X])^{2}$ \- _set of equations in variables
$X$_, given by polynomial grammar $E$ of dimension 2.
$T\subseteq(\mathbb{Q}[\Delta])^{|X|}$ \- _tested language_ , given by
polynomial grammar $T$ of dimension $|X|$,
Question: Is it the case that for all inputs $(e_{1},e_{2})\in E,v\in T$:

$e_{1}(v)=e_{2}(v)?$

Dependent equation satisfiability
Input:
$\Delta$ \- _finite alphabet_ ,
$X$ \- _finite set of variables_ ,
$G$ \- polynomial grammar over $(\mathbb{Q}[\Delta])[X]$ of dimension
$(|X|+2)$
Question: Is it the case that for all inputs $((e_{1},e_{2}),v)\in G$:

$e_{1}(v)=e_{2}(v)?$

###  A.2 Detailed proof of Theorem 3.10

In this section we give a details of the construction of register transducer
from proof of Theorem 3.10. See 3.10

######  Proof A.1 (Details of construction from 3.10).

Given a reset VASS $\mathcal{V}$ we construct a register transducer with
substitution over ring $\mathbb{Z}[x]$ that uses substitution once per run
such that $\mathcal{V}$ can reach $\mathbf{0}$ from $\mathbf{0}$ if and only
if the register transducer returns a non-zero output on some input. We omit
description of the states as it is clear.

Description of register transducer:
_Registers:_
$R_{1}$: will store $\mathbb{Z}[x]$ (_reachability test register_),
$R_{1}^{(aux)}$: will store $\mathbb{Z}$ (_auxiliary register_),
$R_{2}$: will store $\mathbb{Z}$ (_error register_),
$S_{1},S_{2},\ldots,S_{dim}$: will store $\mathbb{Z}$ _(counter registers)_ .
_Input alphabet:_
$\Sigma=$ set of transitions of $\mathcal{V}$.
_Output function:_
$\operatorname{output}=\begin{cases}0,&\text{if state is rejecting},\\\
R_{1}[x:=S_{1}+\ldots+S_{dim}]\cdot R_{2},&\text{else}.\end{cases}$

Invariants. Observe, that run of reset VASS can be identified with a word over
an alphabet consisting of its transitions. Registers after reading a run of
$\mathcal{V}$ of length $n$ satisfy the following:

  1. 1.

$S_{1},\ldots,S_{dim}\in\mathbb{Z}$ are current coordinates of $\mathcal{V}$,
viewed as $\mathbb{Z}$ \- VASS (i.e. can go below 0),

  2. 2.

$R_{2}=0$ iff some coordinate of $\mathcal{V}$ went below 0 (hence $R_{2}$
checks correctness of the run),

  3. 3.

$R_{1}[x:=S_{1}+\ldots+S_{dim}]\neq 0$ iff current point is $\mathbf{0}$,

    1. (a)

$R_{1}[x:=i]=0$ iff $i!=0$ for integer $i$ from range $[0,n]$,

    2. (b)

$R_{1}^{(aux)}=n$.

Construction of polynomial grammar with one substitution:
Initial values of registers:

  1. 1.

$S_{1},\ldots,S_{dim}=0$

  2. 2.

$R_{2}=1$:

  3. 3.

$R_{1}$ :

    1. (a)

$R_{1}=1$,

    2. (b)

$R_{1}^{(aux)}=0$.

Update of registers:

  1. 1.

$S_{1},\ldots,S_{dim}$ are incremented, decremented or reset to 0, according
to read transition,

  2. 2.

$R_{2}$:

    1. (a)

$R_{2}=R_{2}\cdot(S_{1}^{\prime}+1)\cdot\ldots\cdot(S_{dim}^{\prime}+1)$,
where $S_{i}^{\prime}$ is the value of $S_{i}$ after the update.

  3. 3.

$R_{1}$ :

    1. (a)

$R_{1}=R_{1}\cdot(x-R_{1}^{(aux)})$ (recall $x$ is a constant in
$\mathbb{Z}[x]$),

    2. (b)

$R_{1}^{(aux)}=R_{1}^{(aux)}+1$.

###  A.3 Proof of Theorem 3.4 without algebraic closure

In this section we present the proof of Theorem 3.4 without introducing the
notion of algebraic closure of a field.

######  Observation A.2 (Representing algebraic sets – not unique).

There is a subtlety regarding representing algebraic sets. Algebraic sets are
_not_ represented by ideals of polynomials that zero on them ($I(V)$) but by
ideals that they are zeros of ($I\text{ such that }V=V(I)$) – these two
notions coincide in case field is algebraically closed and radical of $I$ is
taken (taking radical of $I$ does not change $V(I)$) due to Fact 5. The former
is a unique representation, but we do not choose it because of computability
issues. It is not clear how to decide for a given ideal, even for a radical
one, if it is of form $I(V)$ (it might be merely contained in $I(V)$ for
$V=V(I)$). Therefore, it is not clear how to enumerate such ideals and, if we
chose it as the representation , algebraic sets.

This subtlety is relevant to Sublemma 2. Assume that $V$ was given by an ideal
that is smaller than $I(V)$. Then there are two options:

  * •

test for condition (2) is passed, which gives a true positive (we show that in
a moment), or

  * •

test for condition (2) is failed, potentially giving false negative. Such
event fortunately will be covered either by a true positive when enumerating
$V$ (again) by $I(V)$ or by some previously enumerated true positive.

######  Observation A.3.

Let algebraic set $V$ be given by ideal $I$, i.e. $V=V(I)$. Then coordinate
ring of $V$ is a quotient of $K[X]/I$.

######  Proof A.4.

Straightforward from $I\subseteq I(V)$, which follows from definition of
$I(V)$.

Before we prove the main result of this section, let us state the following
lemma.

######  Lemma A.5.

([10, Chapter 4, §8, Corollary 10 and remarks at the end of Chapter 4, §8])
Let $K$ be a computable field. Then every radical ideal $I$ effectively admits
a _prime decomposition_.

Now we are ready to present the main proof.

######  Proof A.6 (Proof of first bullet point).

Let us go through the algorithm for Sublemma 2 and see if indeed positives are
true, even for $V$ being represented by radical ideal $I$ contained in $I(V)$.
If $A$ is zero, treated as a polynomial grammar over $K[X]/I$, the more it is
when zero treated as a polynomial grammar over coordinate ring (Observation
A.3). Is crucial that when decomposing $V$ into irreducibles, we use algorithm
for prime decomposition (Lemma A.5) of the ideal – then this ring has no zero
divisors (Lemma 2.11) and hence decidability follows from Lemma 3.1.

###  A.4 Proof of Lemma 4.8

In this section we give the proof of Lemma 4.8 used in the proof of Theorem
4.10. See 4.8

######  Lemma A.7.

Let $p:\Sigma\rightarrow\Sigma^{*}$ be a com-injective word substitution. The
following two linear mappings of $|\Sigma|$-dimensional linear spaces are
invertible:

  1. (i)

$\widetilde{w}\mapsto\widetilde{p(w)}$ of linear space of formal linear
combinations of variables $\widetilde{\Sigma}$ with coefficients in the field
$\mathbb{Q}(\overline{\Sigma})$,

  2. (ii)

$w\mapsto p(w)$ treated as a mapping of commutative words, extended to
$\mathbb{Q}$-linear space $\mathbb{Q}^{\Sigma}$

We illustrate the statement of above lemma with the following example.

######  Example A.8.

Let $\Sigma=\\{a,b\\}$ and $p:a\mapsto ab,b\mapsto babb$.
Values of $\mathbb{Q}(\widetilde{\Sigma}\cup\overline{\Sigma})$-linear mapping
$p$ in basis $\widetilde{\Sigma}$ are:

$\displaystyle p(\widetilde{a})$
$\displaystyle=\widetilde{ab}=\widetilde{a}\overline{b}+\widetilde{b},$
$\displaystyle p(\widetilde{b})$
$\displaystyle=\widetilde{babb}=\widetilde{b}\overline{a}{\overline{b}}^{2}+\widetilde{a}{\overline{b}}^{2}+\widetilde{b}\overline{b}+\widetilde{b}.$

Values of $\mathbb{Q}$-linear mapping $p$ on basis $\Sigma$ (coefficients are
in exponents) are:

$\displaystyle p(a)$ $\displaystyle=ab=a^{1}b^{1},$ $\displaystyle p(b)$
$\displaystyle=babb=a^{1}b^{3},$

(recall in (ii) outputted words are considered commutative) hence the
corresponding matrices are $\begin{bmatrix}\overline{b}&{\overline{b}}^{2}\\\
1&\overline{a}{\overline{b}}^{2}+\overline{b}+1\end{bmatrix}$ and
$\begin{bmatrix}1&1\\\ 1&3\end{bmatrix}.$ They are invertible: determinants
are equal to, respectively, $\overline{a}{\overline{b}}^{3}+\overline{b}$ and
2.

######  Proof A.9 (Proof of Lemma A.7).

(ii) is straightforward from definition of com-injectivity. Observe that
mapping from (ii) is the same as mapping from (i) when 1 is substituted for
variables from $\overline{\Sigma}$; the same holds for their determinants, and
hence if determinant for (ii) is a non-zero number, determinant for (i) is a
non-zero polynomial.

No we proceed towards the proof of Lemma 4.8. By _explicit form_ of a
homomorphism we mean a substitution that defines it; a homomorphism given in
this form is said to be _given explicitly_. We write systems of equations as
(name of equation: equation); we define subsystems by giving equation names.

######  Proof A.10 (Proof of Lemma 4.8).

Assume substitution $p$ is com-injective. To find the inverse substitution (if
exists) we consider system of equations
$S=\\{\widetilde{\sigma}:\widetilde{\sigma}^{\prime}=\widetilde{p(\sigma)}\\}\cup\\{\overline{\sigma}:\overline{\sigma}^{\prime}=\overline{p(\sigma)}\\}$.
$\overline{\Sigma}$-subsystem of $S$ is purely in variables
$\overline{\Sigma}$ hence we solve it first. Right hand sides are monomials
and it can be seen as system of linear equations, where exponents play the
role of coefficients from field $\mathbb{Q}$; we solve it (solution exists –
its existence is equivalent to (ii) of Lemma A.7). This solution gives
explicitly an automorphism of $K(\overline{a}^{\mathbb{Q}},a\in\Sigma)$ which
naturally is also an automorphism of
$K(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq 0}},a\in\Sigma)$. We
substitute this to $\widetilde{\Sigma}$-subsystem and obtain a system of
linear equations in variables $\widetilde{\Sigma}$’ and coefficients in
$K(\widetilde{a},\overline{a}^{\mathbb{Q}_{\geq 0}},a\in\Sigma)$; this system
is automorphic to $\widetilde{\Sigma}$-subsystem of $S$ and hence has a
solution (due to (i) of Lemma A.7). Its solution, together with solution of
$\overline{\Sigma}$-subsystem, gives the right-inverse substitution
explicitly. It is a two-sided inverse because both systems of equations were
linear (in the mentioned sense).

The proof of the converse is analogous, which finishes the proof.

###  A.5 Proof of Lemma A.12

In this section we prove Lemma A.12 used in the proof of Theorem 3.4. It is a
well known result (e.g. implicit in [10, Chapter 5, §2 and §3 and §4]), but we
did not find an explicit reference.

Preliminaries. By $K[X]$ we denote over some field $K$ and a finite set of
variables $X$.

Every ideal $I$ in ring $K[X]$ induces a congruence $\sim_{I}$ defied as
$f\sim_{I}g$ iff $f-g\in I$, for $f,g\in K[X]$. By $K[X]/I$ we denote
_quotient ring_ $K[X]/\\!\\!\sim_{I}$. For $f\in K[X]$. A _radical of an
ideal_ $I$ is the set $\sqrt{I}=\\{f\in K[X]\mid f^{n}\in I\text{ for some
}n\geq 0\\}$; it is an ideal. An ideal $I$ is _radical_ if $f^{n}\in I$
implies $f\in I$ for all polynomials $f$ and $n\geq 0$, or in other word, $I$
is equal to its radical. Let $V$ be an algebraic set. A _coordinate ring_ of
$V$ is the ring of polynomial functions from $V$ to $K$. A ring is called a
_computable ring_ if its elements can be enumerated in a way that ring
operations are computable functions.

######  Fact 4.

([10, Remarks at the end of §2 of Chapter 4] ) Given ideal $I$ in $K[X]$, one
can compute its radical.

######  Fact 5 ([10], Chapter 4, §2, Theorem 7 (iii)).

Let $K$ be an algebraically closed field. Then mappings $V\mapsto
I(V),I\mapsto V(I)$ form a bijective correspondence between algebraic sets and
radical ideals.

Representation. For effectiveness of results, we assume that $K$ is a
_computable field_ , i.e. its elements can be enumerated such that field
operations are computable functions. Then we represent objects used by
algorithms as follows:

  * •

ideals are represented by finite sets of generators; every ideal admits such a
representation due to Hilbert’s Basis Theorem (Fact 1), and

  * •

_algebraic sets_ are represented by ideals that they are zeroes of, i.e. an
algebraic set $V$ is represented by $I$ such that $V=V(I)$.

Proof of Lemma A.12.

######  Fact 6.

Let $K$ be a computable, algebraically closed field. Given algebraic set $V$,
one can compute $I(V)$.

######  Proof A.11.

Let $V$ be represented by ideal $I$. Then $I(V)$ is the radical of $I$ (Fact
5); it can be computed (Fact 4).

######  Fact 7.

([10, Chapter 5, §3, Proposition 5]) Quotient rings are computable rings. More
precisely, given ideal $I$, ring $K[X]/I$ is a computable ring.

######  Fact 8.

([10, Chapter 5, §2, remark about Theorem 7 after Definition 8])] For an
algebraic set $V$, its coordinate ring is isomorphic to $K[X]/I(V)$.

######  Lemma A.12.

Let $K$ be an algebraically closed field. Then, given algebraic set $V$, one
can compute its coordinate ring and it is a computable ring.

######  Proof A.13.

Coordinate ring is isomorphic to $K[X]/I(V)$ (Fact 8). It can be computed from
$V$, as we can compute $I(V)$ (Fact 6). It is a computable ring (Fact 7).