theoremTheorem lemma[theorem]Lemma claim[theorem]Claim

# Equivariant ideals of polynomials

Arka Ghosh  0000-0003-3839-8459 University of WarsawPoland and  Sławomir
Lasota  0000-0001-8674-4470 University of WarsawPoland

###### Abstract.

We study existence and computability of finite bases for ideals of polynomials
over infinitely many variables. In our setting, variables come from a
countable logical structure A, and embeddings from A to A act on polynomials
by renaming variables. First, we give a sufficient and necessary condition for
A to guarantee the following generalisation of Hilbert’s Basis Theorem: every
polynomial ideal which is equivariant, i.e. invariant under renaming of
variables, is finitely generated. Second, we develop an extension of classical
Buchberger’s algorithm to compute a Gröbner basis of a given equivariant
ideal. This implies decidability of the membership problem for equivariant
ideals. Finally, we sketch upon various applications of these results to
register automata, Petri nets with data, orbit-finitely generated vector
spaces, and orbit-finite systems of linear equations.

Hilbert’s Basis Theorem, polynomial ring, ideal, ideal membership problem,
equivariant sets, sets with atoms, orbit-finite sets, register automata, Petri
nets with data

##  1\. Introduction

A ring is _Noetherian_ if each of its ideals is finitely-generated. According
to Hilbert’s Basis Theorem, the ring of polynomials over a finite set of
variables, with coefficients from a given Noetherian ring, is Noetherian. In
particular, every polynomial ideal can be represented by its finite basis, and
hence can be given as input to algorithms. Given such a finite basis,
Buchberger’s algorithm computes a Gröbner basis that can be used to decide the
membership problem for polynomial ideals: determine, whether a given
polynomial belongs to the ideal generated by a given set of polynomials.
Hilbert’s Basis Theorem and Gröbner bases have important algorithmic
applications, for instance to decide zeroness of polynomial automata (weighted
automata with polynomial updates) (Ben17), reachability of reversible Petri
nets (MayrMeyer82), or bisimulation equivalence checking (Stribrna97). Other
applications of Buchberger’s algorithm are overviewed in (Bu-app98).

We generalise the above classical results to the ring of polynomials over an
infinite set of variables. Clearly, Hilbert’s Basis Theorem is not
generalisable literally, since every polynomial belonging to a finitely-
generated ideal may use at least one of variables used by the generators. In
this paper we investigate the following setting:

  * •

Variables are elements of a countable relational structure $\mathcal{A}$
(which we call _domain of variables_).

  * •

The monoid of embeddings $\mathcal{A}\to\mathcal{A}$ acts on polynomials by
renaming variables.

  * •

We restrict to polynomial ideals which are invariant under renaming (such
ideals we call _equivariant_). Accordingly, we adapt the definition of basis,
enforcing equivariance of a generated ideal.

###### Example 1.1.

For illustration, consider _equality_ domain of variables, namely the
structure $\mathcal{A}=(A,=)$ consisting of a countable infinite set $A$ and
the equality relation. Embeddings are injective mappings $A\to A$. Consider
the ring $\mathbb{R}[\mathcal{A}]$ of polynomials with real coefficients over
variables $A$. The subset $\mathcal{I}\subseteq\mathbb{R}[\mathcal{A}]$ of
polynomials whose coefficients sum up to 0, is an equivariant ideal. It is the
least ideal containing all univariate polynomials $p_{a}(a)=a-1$, where $a\in
A$. For instance, the polynomial $p(a,b,c)=ab^{2}-bc$ with variables $a,b,c\in
A$ belongs to $\mathcal{I}$ and decomposes as:

$ab^{2}-bc\ =\ (b-1)(ab+a-c)+(a-1)-(c-1).$

$\mathcal{I}$ is also the least _equivariant_ ideal including
$\left\\{p_{a}\right\\}$, for a fixed $a\in A$, hence finitely-generated
according to our adapted definition. $\triangleleft$

### Contribution.

We investigate equivariant ideals of polynomials over domains of variables
which are _totally ordered_ , namely admit a total order as one of its
relations, and _well structured_ , namely admit a naturally defined _well
quasi order_ (as defined in Section 2). A prototypical example of such a
domain is rational order $\mathcal{Q}=(Q,\leq_{\mathcal{Q}})$. For such
domains $\mathcal{A}$ we prove, in Section 3, the following generalisation of
Hilbert’s Basis Theorem: for every Noetherian ring $\mathbb{K}$, every
equivariant ideal in the polynomial ring $\mathbb{K}[\mathcal{A}]$ has a
finite basis. We transfer this property to lexicographic products of totally
ordered, well structured domains, and to reducts thereof, including the
equality domain. We also show that well structure is necessary for the
generalisation of Hilbert’s Basis Theorem to hold.

For further investigations we restrict to domains of variables which are _well
ordered_ , well structured, and _computable_ (as formalized in Section 5). We
develop a generalisation of Buchberger’s algorithm to compute a Gröbner basis
of an equivariant ideal, given as a finite set of generators. As a corollary,
in Section 7 we obtain decidability of the membership problem for equivariant
ideals. Similarly as our generalisation of Hilbert’s Basis Theorem, we
transfer the decidability result to a wide range of other domains, including
equality domain, rational order, and lexicographic products thereof.

Our results are of fundamental nature, with various potential applications. We
sketch upon some of them. In Section 4 we apply our generalisation of
Hilbert’s Basis Theorem to prove that orbit-finitely generated vector spaces
have finite length, i.e., admit no infinite increasing chains of equivariant
subspaces. This generalises a crucial result of (BKM21) (however, without
explicit upper bound). As a consequence, we derive decidability of the
zeroness problem for weighted register automata, again generalising a result
of (BKM21). We also apply, in Section 8, the ideal membership problem to
decide reachability in reversible Petri nets with data, for a wide range of
data domains. This includes rational order domain, where the problem is known
to be undecidable for general non-reversible Petri nets (LNORW07). Finally, in
Section 9, we apply the ideal membership problem to solving orbit-finite
systems of linear equations. This generalises a core result of (GHL22) to a
wide range of domains (again, without complexity upper bound). All our proofs
of generalisations of (BKM21) and (GHL22) are remarkably simple, compared to
the original ones.

### Structure of the paper.

The paper has two parts: the first part concentrates on _existence_ of finite
bases, while the second one investigates _computability_ thereof. In the first
part, Sections 2–4, we set up preliminaries, prove our generalisation of
Hilbert’s Basis Theorem, and sketch upon its applications. Then, in Sections
5–9 we generalise Buchberger algorithm, use it for decidabillity of the ideal
membership problem, and show applications thereof.

Some proofs are delegated to Appendix.

### Related research.

Our motivations, together with the most fundamental concepts such as
equivariance and orbit-finiteness, come from the theory of sets with atoms
(BKL14; atombook). The concept of well structured domain, crucial for
development of this paper, turns out to be essentially the same as
_preservation of well quasi order_ , introduced in (Lasota16) and conjectured
to characterise data domains rendering decidability of a range of decision
problems for Petri nets. Relationship between the two settings calls for
further investigation.

There have been numerous earlier contributions regarding existence and
computability of finite bases of equivariant ideals. To the best of our
knowledge, all of them considered (using our terminology) either equality or
well order domains. First, (Cohen67) proves finite basis property for domain
$\omega=(\mathbb{N},\leq)$, then (Cohen87) and (Emmott87) extend to larger
ordinals. These two papers also give sufficient condition for computability of
Gröbner bases, which is shown to hold in $\omega$ in (HKL18). Similar results
were independently obtained in (AH07; AH08; BD11). In (HS12) the authors use
the aforementioned results to prove the Independent Set Conjecture in
algebraic statistics.

There are a number of recent results concerning finite generation of vector
spaces: (BKM21) shows that every equivariant subspace of orbit-finitely
generated vector space is finitely generated (this follows from our results in
Section 3, as argued in Section 4); furthermore, (GHL22) shows that dual
vector spaces are finitely generated.

##  2\. Preliminaries

A relational structure $\mathcal{A}=(A,r_{1},\ldots,r_{n})$ is a set $A$
together with finitely many relations $r_{1}\subseteq
A^{s_{1}},\ldots,r_{n}\subseteq A^{s_{n}}$ of finite arities
$s_{1},\ldots,s_{n}\in\mathbb{N}$, respectively. In the sequel we restrict to
countable structures only. Every relation $r\subseteq A^{m}$ which is
expressible as a Boolean combination of relations $r_{1},\ldots,r_{n}$, we
call _definable_. We always assume that equality $=$ is definable. An _induced
substructure_ of $\mathcal{A}$ is the restriction of $\mathcal{A}$ to some
subset of $A$.

An _embedding_ of $\mathcal{A}$ is a map $\iota:A\to A$ that preserves and
reflects all relations, which means that for every relation $r_{i}$ and
$a_{1},\ldots,a_{s_{i}}\in A$, the following equivalence holds:

$r_{i}(a_{1},\ldots,a_{s_{i}})\iff
r_{i}(\iota(a_{1}),\ldots,\iota(a_{s_{i}})).$

In other words, an embedding $\iota$ is an isomorphism of $\mathcal{A}$ and
its substructure induced by $\iota(A)$. Clearly, embeddings preserve and
reflect all definable relations, and hence each such relation can be
considered w.l.o.g. to be among $r_{1},\ldots,r_{n}$. The set of all
embeddings of $\mathcal{A}$ we denote as $\text{\sc Emb}_{\mathcal{A}}$. We
say that $\mathcal{A}$ is _totally ordered_ (resp.  _well ordered_) if a total
order (resp. a well order) is definable in $\mathcal{A}$.

Speaking intuitively, a _reduct_ of $\mathcal{A}$ is a structure obtained by
removing some relations from $\mathcal{A}$. Formally, a structure
$\mathcal{A}^{\prime}=(A,r_{1},\ldots,r_{n})$ is a reduct of
$\mathcal{A}=(A,\ldots)$, with the same carrier set $A$, if all relations
$r_{1},\ldots,r_{n}$ are definable in $\mathcal{A}$.

###### Example 2.1.

For a countable infinite set $A$, embeddings of the equality structure
$\mathcal{A}=(A,=)$, with equality as the only relation, are all injective
maps $A\to A$. Embeddings of the rational order
$\mathcal{Q}=(Q,\leq_{\mathcal{Q}})$ are all strictly monotonic maps
$\iota:Q\to Q$, i.e. functions satisfying

$q<_{\mathcal{Q}}q^{\prime}\implies\iota(q)<_{\mathcal{Q}}\iota(q^{\prime}).$

Note that equality is definable using $\leq$, namely $q=q^{\prime}\iff q\leq
q^{\prime}\wedge q^{\prime}\leq q$. The equality structure is thus a reduct of
$\mathcal{Q}$.

Every ordinal $\alpha$ can be seen as a (well ordered) relational structure,
with just one binary relation – the ordinal order. Again, its embeddings are
strictly monotonic maps $\alpha\to\alpha$. A special case is
$\omega=(\mathbb{N},\leq)=\left\\{0<1<\ldots\right\\}$; or $\langle
d\rangle=\left\\{0<1<\ldots<d{-}1\right\\}$, for $d\in\mathbb{N}$, where the
only embedding is the identity. In the sequel we identify an ordinal with the
corresponding relational structure. $\triangleleft$

### Noetherianity.

Recall that an _ideal_ in a commutative ring $\mathbb{K}$ is any nonempty
subset $\mathcal{I}\subseteq\mathbb{K}$ closed under addition and
multiplication by any element of $\mathbb{K}$:
$a,a^{\prime}\in\mathcal{I}{\implies}a+a^{\prime}\in\mathcal{I}$, and
$a\in\mathcal{I},b\in\mathbb{K}{\implies}a\cdot b\in\mathcal{I}$. A basis of
$\mathcal{I}$ is any subset $\mathcal{B}\subseteq\mathcal{I}$ such that every
$a\in\mathcal{I}$ is obtainable from $\mathcal{B}$ by addition and
multiplication by arbitrary elements of $\mathbb{K}$; equivalently,
$a=a_{1}\cdot b_{1}+\ldots+a_{n}\cdot b_{n}$ for some
$b_{1},\ldots,b_{n}\in\mathcal{B}$ and $a_{1},\ldots,a_{n}\in\mathbb{K}$. A
commutative ring is _Noetherian_ if each of its ideals has a finite basis. In
particular, each field is a Noetherian commutative ring.

### Polynomials.

Let $\mathcal{A}=(A,r_{1},\ldots,r_{n})$ be a relational structure, which we
call a _domain of variables_ , or simply a _domain_. We define, in the
expected way, the commutative multiplicative monoid of monomials over
variables from $A$, denoted $\text{\sc Mon}[\mathcal{A}]$. A _monomial_ is a
formal expression of the form

$\displaystyle f(a_{1}\ldots a_{m})=a_{1}^{n_{1}}\cdot\ \ldots\ \cdot
a_{m}^{n_{m}},$

where $m\geq 0$, $\text{\sc
vars}(f)=\left\\{a_{1},\ldots,a_{m}\right\\}\subseteq A$ are distinct
variables, and $n_{i}=\text{\sc deg}_{f}\,a_{i}>0$ is the _degree_ of variable
$a_{i}$ in $f$. For $a\notin\text{\sc vars}(f)$ we set $\text{\sc
deg}_{f}\,a=0$. The trivial unit monomial, for $m=0$, we denote as
$\mathbf{1}$. Also, given a commutative ring $\mathbb{K}$, we define the
commutative ring of polynomials with coefficients from $\mathbb{K}$ and
variables from $A$, denoted $\mathbb{K}[\mathcal{A}]$. A _term_ is a formal
expression of the form $r\cdot f$, for $r\in\mathbb{K}$ and $f\in\text{\sc
Mon}[\mathcal{A}]$, and a _polynomial_ is a finite sum of terms, i.e., a
formal expression of the form

$f\ =\ r_{1}\cdot f_{1}+\ldots+r_{n}\cdot f_{n},$

$f_{1},\ldots,f_{n}\in\text{\sc Mon}[\mathcal{A}]$ are distinct monomials and
$r_{1},\ldots,r_{n}\in\mathbb{K}$ are their _coefficients_. The zero
polynomial, for $n=0$, we denote by $\mathbf{0}$. We set $\text{\sc
vars}(f)=\text{\sc vars}(f_{1})\cup\ldots\cup\text{\sc vars}(f_{n})$.

### Equivariant Noetherianity.

Embeddings act on polynomials by renaming variables: an embedding
$\iota\in\text{\sc Emb}_{A}$ maps a polynomial $f$ to the polynomial
$\iota(f)$ obtained by renaming all variables in $f$ according to $\iota$,
i.e., by replacing each variable $a$ by $\iota(a)$111 Clearly, $f$ and
$\iota(f)$ define the same functions $\mathbb{K}^{n}\to\mathbb{K}$, where
$n=|\text{\sc vars}(f)|$. . An ideal
$\mathcal{I}\subseteq\mathbb{K}[\mathcal{A}]$ is called _equivariant_ if it is
additionally closed under the action of ${\text{\sc Emb}_{\mathcal{A}}}$:
whenever $f\in\mathcal{I}$ and $\iota\in{\text{\sc Emb}_{\mathcal{A}}}$ then
$\iota(f)\in\mathcal{I}$. We adapt the notion of basis by taking additionally
into account the action of ${\text{\sc Emb}_{\mathcal{A}}}$. By a _basis_ of
an equivariant ideal $\mathcal{I}$ we mean a subset
$\mathcal{B}\subseteq\mathcal{I}$ such that each element of $\mathcal{I}$ is
obtainable from $\mathcal{B}$ by addition, multiplication by arbitrary
polynomials, and action of ${\text{\sc Emb}_{\mathcal{A}}}$. This is
equivalent to saying that

(1) $\displaystyle{\text{\sc Emb}_{\mathcal{A}}}(\mathcal{B})\
\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\
\left\\{\iota(g)\,\middle|\,\iota\in{\text{\sc Emb}_{\mathcal{A}}},\
g\in\mathcal{B}\right\\}$

is a basis of $\mathcal{I}$ in classical sense, or to presentability of every
element $f\in\mathcal{I}$ as

$f\ =\ \sum_{i=1}^{n}h_{i}\cdot\iota_{i}(g_{i}),$

for $g_{1}\ldots g_{n}\in\mathcal{B}$ and $h_{1}\ldots
h_{n}\in\mathbb{K}[\mathcal{A}]$ and $\iota_{1}\ldots\iota_{n}\in{\text{\sc
Emb}_{\mathcal{A}}}$ (since the action of ${\text{\sc Emb}_{\mathcal{A}}}$
commutes with addition and multiplication of polynomials). When $\mathcal{B}$
is a basis of $\mathcal{I}$, we also say that $\mathcal{I}$ is the equivariant
ideal _generated_ by $\mathcal{B}$, and denote it by
$\mathcal{I}=\langle\mathcal{B}\rangle$.

###### Example 2.2.

Consider the rational order $\mathcal{Q}=(Q,\leq_{\mathcal{Q}})$ as a domain
of variables, and a polynomial

$f_{0}(a_{0},b_{0},c_{0})\ =\ b_{0}^{2}-a_{0}c_{0}$

for some arbitrarily chosen, fixed variables $a_{0}<b_{0}<c_{0}$ from $Q$. For
every other variables $a<b<c$, the polynomial $ac^{2}-b^{3}$ belongs to the
equivariant ideal generated by $\left\\{f_{0}\right\\}$, because

$ac^{2}-b^{3}\ =\ a\cdot(c^{2}-bd)\ -\ b\cdot(b^{2}-ad),$

for arbitrary variable $d>c$. $\triangleleft$

The ring $\mathbb{K}[\mathcal{A}]$ we call _equivariantly Noetherian_ if each
equivariant ideal has a finite basis. In Section 3 we demonstrate that a wide
range of domains $\mathcal{A}$ satisfy the following generalisation of
Hilbert’s Basis Theorem:

###### Property 2.3.

For every Noetherian commutative ring $\mathbb{K}$, the polynomial ring
$\mathbb{K}[\mathcal{A}]$ is equivariantly Noetherian.

### Orbit-finite bases.

Equivalently, $\mathbb{K}[\mathcal{A}]$ is equivariantly Noetherian if each
equivariant ideal has a basis, in classical sense, which is _orbit-finite_ ,
i.e., finite up to embeddings. Formally, orbit-finite sets are set of the form
(1) where $\mathcal{B}$ is finite. A finite set $\mathcal{B}$ is called a
_presentation_ of an orbit-finite set (1). The concept of orbit-finiteness
comes from the theory of sets with atoms (atombook; BKL14), where it refers to
sets which are infinite but finite up to automorphisms of an underlying
structure of atoms. We slightly extend this setting here, and consider
embeddings instead of just automorphisms. In case of equality and rational
order domains (and any _homogeneous_ structure), the action of embeddings is
essentially the same as the action of automorphisms, as every automorphism of
finite induced substructures extends to an automorphism of the whole domain.

### Ideal membership.

For $\mathcal{A}$ satisfying Property 2.3, every equivariant ideal in
$\mathbb{K}[\mathcal{A}]$ can be represented by its finite basis, and thus can
be input to algorithms. In Section 7, assuming $\mathbb{K}$ to be a fixed
computable field (e.g. rational222 The set of rationals appears in the sequel
in two roles: as a totally ordered set $\mathcal{Q}$, and as a field
$\mathbb{Q}$. We use different fonts to distinguish these two roles.  field
$\mathbb{Q}$), we study decidability of the following decision problem of
membership of a given polynomial in a given equivariant ideal, for different
domains $\mathcal{A}$:

Ideal-memb in $\mathbb{K}[\mathcal{A}]$::

Input: :

a polynomial $f\in\mathbb{K}[\mathcal{A}]$ and an equivariant ideal

$\mathcal{I}\subseteq\mathbb{K}[\mathcal{A}]$.

Question: :

$f\in\mathcal{I}$?

### Well structured structures.

A quasi order consists of a set $Y$ and a reflexive and transitive relation
$\preceq\,\subseteq Y\times Y$. $(Y,\preceq)$ is a _well quasi order_ (wqo) if
every infinite sequence $y_{1},y_{2},\ldots$ of elements of $Y$ contains a
dominating pair, i.e., two elements $y_{i}$ and $y_{j}$, for $i<j$, such that
$y_{i}\preceq y_{j}$. Clearly, every well order is a wqo.

A subset $X\subseteq Y$ is _upward-closed_ if $x\in X$ and $x\preceq
x^{\prime}$ implies $x^{\prime}\in X$. A _basis_ of an upward-closed set $X$
(not to be confused with a basis of an ideal) is any subset $B\subseteq X$
such that for every $x\in X$ there is $b\in B$ with $b\preceq x$. Every wqo is
well-founded and admits no infinite antichains (diestel, Proposition 12.1.1),
which implies:

###### Lemma 2.4.

Every upward-closed subset of a wqo has a finite basis.

Given a relational structure $\mathcal{A}$ and a quasi order $(Y,\preceq)$, by
$\text{\sc Age}(\mathcal{A})$ we denote the set of all its finite induced
substructures. We do not distinguish between a finite subset
$B\subseteq_{\text{fin}}A$ and the substructure $\mathcal{B}$ of $\mathcal{A}$
induced by $B$, i.e., we equate $\text{\sc Age}(\mathcal{A})$ with
$\mathcal{P}_{\text{\tiny fin}}(\mathcal{A})$. By $\text{\sc
Age}(\mathcal{A},Y)$ we denote the set of all finite induced substructures
labeled by $Y$, i.e., functions $\ell:B\to Y$ where $B\in\text{\sc
Age}(\mathcal{A}){}$. The quasi order $(Y,\preceq)$ _determines_ a natural
quasi order $\rightsquigarrow$ on $\text{\sc Age}(\mathcal{A},Y)$, where
$(\ell:B\to Y)\rightsquigarrow(\ell^{\prime}:B^{\prime}\to Y)$ if there is an
embedding $\iota\in{\text{\sc Emb}_{\mathcal{A}}}$ such that
$\iota(B)\subseteq B^{\prime}$ and $\ell(b)\preceq\ell^{\prime}(\iota(b))$ for
all $b\in B$. In most cases we will focus on $(Y,\preceq)=(\mathbb{N},\leq)$.

###### Definition 2.5.

$\mathcal{A}$ is _$\omega$ -well structured_ if $\omega=(\mathbb{N},\leq)$
determines a wqo on $\text{\sc Age}(\mathcal{A},\mathbb{N})$. Moreover,
$\mathcal{A}$ is _well structured_ if every wqo $(Y,\preceq)$ determines a wqo
on $\text{\sc Age}(\mathcal{A},Y)$.333 It is possible that the two conditions
are equivalent. See e.g. (KS91) for related results.  $\triangleleft$

For instance, the rational order $\mathcal{Q}=(Q,\leq_{\mathcal{Q}})$ is well
structured. Indeed, finite induced substructures of $\mathcal{Q}$ are finite
total orders, and $\text{\sc Age}(\mathcal{Q},Y)$ is a wqo by Higman’s Lemma
(Hig52). The equality structure is also well structured, as a reduct of
$\mathcal{Q}$. _Universal tree_ arising as Frai̇ssé limit of finite trees
(atombook, Section 7), similarly as $\mathcal{Q}$ arises as Frai̇ssé limit of
finite total orders, is well structured. By Nash-Williams’s Theorem (nash-
williams, Theorem 2) (cf. also (Hig52) in the restricted case of $\omega$)
ordinals are well structured too: Every ordinal (seen as a relational
structure) is well structured.

###### Proof.

Let $\alpha$ be a fixed ordinal and $(Y,\preceq)$ a fixed wqo. We add to $Y$
the least element $*$, namely put $*\prec y$ for all $y\in Y$, and observe
that $(Y\cup\left\\{*\right\\},\preceq)$ is still a wqo. According to Theorem
2 in (nash-williams), the wqo $(Y\cup\left\\{*\right\\},\preceq)$ determines a
wqo on the set $F(Y)$ of image-finite functions $\ell:\alpha\to
Y\cup\left\\{*\right\\}$. Elements of $\text{\sc Age}(\alpha,Y)$ may be
identified with those functions $\ell:\alpha\to Y$ which map almost all
elements to 0, a subset $F_{0}(Y)\subseteq F(Y)$. Furthermore, the quasi
orders determined by $(Y\cup\left\\{*\right\\},\preceq)$ on $\text{\sc
Age}(\alpha,Y)$ and $F_{0}(Y)$ agree. Therefore
$(Y\cup\left\\{*\right\\},\preceq)$ determines a wqo on $\text{\sc
Age}(\alpha,Y)$, as required. ∎

### Lexicographic product of structures.

We will build larger domains from smaller ones, using _lexicographic product_
defined below. The operation, in contrast to Cartesian product (as illustrated
in Example 2.6), preserves well structure.

Given two relational structures $\mathcal{A}=(A,\ldots)$ and
$\mathcal{A}^{\prime}=(A^{\prime},\ldots)$, their lexicographic product
$\mathcal{A}\otimes\mathcal{A}^{\prime}$ is defined as follows. The carrier
set of $\mathcal{A}\otimes\mathcal{A}^{\prime}$ is the Cartesian product
$A\times A^{\prime}$, and the set of relation symbols is the disjoint union of
sets of relation symbols of $\mathcal{A}$ and $\mathcal{A}^{\prime}$. For each
$k$-ary relation $r$ of $\mathcal{A}$, the relation $r$ in
$\mathcal{A}\otimes\mathcal{A}^{\prime}$ relates those $k$-tuples

(2) $\displaystyle((a_{1},a^{\prime}_{1}),\ldots,(a_{k},a^{\prime}_{k}))$

where $r(a_{1},\ldots,a_{k})$ in $\mathcal{A}$ (the second coordinate comming
from $\mathcal{A}^{\prime}$ is ignored). Furthermore, for each $k$-ary
relation $r^{\prime}$ of $\mathcal{A}^{\prime}$, the relation $r^{\prime}$ in
$\mathcal{A}\otimes\mathcal{A}^{\prime}$ relates those tuples (2) where
$a_{1}=\ldots=a_{k}$ and $r^{\prime}(a^{\prime}_{1},\ldots,a^{\prime}_{k})$ in
$\mathcal{A}^{\prime}$ (the first coordinate comming from $\mathcal{A}$ is
required to be equal). The product is associative.

Embeddings of $\mathcal{A}\otimes\mathcal{A}^{\prime}$ are exactly maps of the
form

(3) $\displaystyle(a,a^{\prime})\ \longmapsto\
(\iota(a),\iota^{\prime}_{a}(a^{\prime})),$

determined by some $\iota\in{\text{\sc Emb}_{\mathcal{A}}}$ and a family
$\left\\{\iota^{\prime}_{a}\in\text{\sc
Emb}_{\mathcal{A}^{\prime}}\,\middle|\,a\in A\right\\}$.

###### Proof.

In one direction, every mapping $A\times A^{\prime}\to A\times A^{\prime}$ of
the form (3) preserves and reflects all relations of
$\mathcal{A}\otimes\mathcal{A}^{\prime}$, since each relation of $\mathcal{A}$
is preserved and reflected by $\iota\in\text{\sc Emb}_{\mathcal{A}}$, and each
relation of $\mathcal{A}^{\prime}$ is preserved and reflected by every
$\iota^{\prime}_{a}$, for $a\in A$.

In the reverse direction, consider any embedding $\kappa\in\text{\sc
Emb}_{A\otimes A^{\prime}}$. As equality is definable in $\mathcal{A}$, the
mapping $\kappa$ preserves and reflects equality of the first coordinate,
which determines an injection $\iota:A\to A$ such that the first component of
$\kappa(a,a^{\prime})$ equals $\iota(a)$. As $\kappa$ preserves and reflects
all relations of $\mathcal{A}$, the injection is an embedding,
$\iota\in{\text{\sc Emb}_{\mathcal{A}}}$. Furthermore, for each $a\in A$ the
mapping $\kappa$ restricted to pairs $(a,\\_)$, preserves and reflects all
relations of $\mathcal{A}^{\prime}$ on the second coordinate. Therefore, for
each $a\in\mathcal{A}$ there is some $\iota^{\prime}_{a}\in\text{\sc
Emb}_{\mathcal{A}^{\prime}}$ such that $\kappa$ is equal to (3). ∎

Lexicographic product of two totally ordered (well ordered, well structured,
resp.) relational structures is totally ordered (well ordered, well
structured, resp.).

###### Proof.

Consider two relational structures $\mathcal{A}=(A,\ldots)$ and
$\mathcal{A}^{\prime}=(A^{\prime},\ldots)$. Let $\preceq$ and
$\preceq^{\prime}$ be definable total orders on $\mathcal{A}$ and
$\mathcal{A}^{\prime}$, respectively. The lexicographic product of $\preceq$
and $\preceq^{\prime}$ is definable in
$\mathcal{A}\otimes\mathcal{A}^{\prime}$, and is well when $\preceq$ and
$\preceq^{\prime}$ are well, and therefore if both $\mathcal{A}$ and
$\mathcal{A}^{\prime}$ are totally ordered (resp. well ordered), so is
$\mathcal{A}\otimes\mathcal{A}^{\prime}$.

It thus remains to show that $\mathcal{A}\otimes\mathcal{A}^{\prime}$ is well
structured. This follows immediately, once we prove:

Let $(Y,\prec)$ is a wqo. Then $\text{\sc
Age}(\mathcal{A}\otimes\mathcal{A}^{\prime},Y)$ is isomorphic, as a quasi
order, to $\text{\sc Age}(\mathcal{A},\text{\sc
Age}(\mathcal{A}^{\prime},Y))$. For proving the claim, consider any
$B\in\text{\sc Age}(\mathcal{A}\otimes\mathcal{A}^{\prime})$ and its labelling
$(\ell:B\to Y)\in\text{\sc Age}(\mathcal{A}\otimes\mathcal{A}^{\prime},Y)$.
Let $\overline{B}\in\text{\sc Age}(\mathcal{A})$ be its projection on the
first coordinate. Furthermore, for $a\in\overline{B}$ let
$B_{a}\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\left\\{a^{\prime}\,\middle|\,(a,a^{\prime})\in
B\right\\}\in\text{\sc Age}(\mathcal{A}^{\prime})$, and let $\ell_{a}:B_{a}\to
Y$ be the corresponding restriction of $\ell$, namely
$\ell_{a}(a^{\prime})=\ell(a,a^{\prime})$. This defines a function

$\overline{\ell}:a\mapsto\ell_{a},\qquad\text{ for }a\in\overline{B},$

i.e., $(\overline{\ell}:\overline{B}\to\text{\sc
Age}(\mathcal{A}^{\prime},Y))\in\text{\sc Age}(\mathcal{A},\text{\sc
Age}(\mathcal{A}^{\prime},Y))$. We have thus defined a mapping
$\ell\mapsto\overline{\ell}$. One easily defines its inverse, and hence it is
a bijection between $\text{\sc Age}(\mathcal{A}\otimes\mathcal{A}^{\prime},Y)$
and $\text{\sc Age}(\mathcal{A},\text{\sc Age}(\mathcal{A}^{\prime},Y))$.

Given two induced substructures $B_{i}\in\text{\sc
Age}(\mathcal{A}\otimes\mathcal{A}^{\prime})$ and its labellings
$(\ell_{i}:B_{i}\to Y)\in\text{\sc
Age}(\mathcal{A}\otimes\mathcal{A}^{\prime},Y)$, for $i=1,2$, using Lemma 2 we
notice equivalence of the following two conditions:

  * •

$\ell_{1}\rightsquigarrow\ell_{2}$ are related by the quasi order determined
by $(Y,\preceq)$ on $\text{\sc
Age}(\mathcal{A}\otimes\mathcal{A}^{\prime},Y)$;

  * •

there is some $\iota\in{\text{\sc Emb}_{\mathcal{A}}}$ such that for every
$a\in\overline{B}$, $(\ell_{1})_{a}\rightsquigarrow(\ell_{2})_{\iota(a)}$ are
related by the quasi order determined by $(Y,\preceq)$ on $\text{\sc
Age}(\mathcal{A}^{\prime},Y)$.

The latter condition says exactly that
$\overline{\ell}_{1}\rightsquigarrow\overline{\ell}_{2}$ are related by the
quasi order determined by $(Y,\preceq)$ on $\text{\sc
Age}(\mathcal{A},\text{\sc Age}(\mathcal{A}^{\prime},Y))$. The claim is thus
shown. ∎

###### Example 2.6.

Since the rational order $\mathcal{Q}$ is well structured, the lexicographic
product $\mathcal{Q}\otimes\mathcal{Q}$ is also so, while the Cartesian
product $\mathcal{Q}\times\mathcal{Q}$ is not. We claim that the quasi order
$\rightsquigarrow$ determined by an arbitrary wqo on $\text{\sc
Age}(\mathcal{Q}\times\mathcal{Q})$ (the choice of wqo is irrelevant) is not a
wqo. Indeed, consider the family of ’cycle’ subsets $C=(C_{n}\in\text{\sc
Age}(\mathcal{Q}\times\mathcal{Q}))_{n\in\mathbb{N}}$, where (cf. Figure 1)

$\displaystyle C_{n}=\left\\{(x_{i},y_{i}),(x_{i},y_{i+1\\!\\!\\!\mod
n})\,\middle|\,i\in\left\\{0\ldots n-1\right\\}\right\\}$

for arbitrary rationals $x_{0}<\ldots<x_{n-1}$ and $y_{0}<\ldots<y_{n-1}$. As
embeddings of $\mathcal{Q}\times\mathcal{Q}$ are induced by pairs of
embeddings of $\mathcal{Q}$,

$\text{\sc Emb}_{\mathcal{Q}\times\mathcal{Q}}=\text{\sc
Emb}_{\mathcal{Q}}\times\text{\sc Emb}_{\mathcal{Q}},$

a smaller cycle can not embed into a larger one. Therefore
$C_{n}\rightsquigarrow C_{m}$ implies $n=m$, i.e., $C$ is an antichain, and
hence $\rightsquigarrow$ is not a wqo.

$y_{0}$$x_{0}$$y_{1}$$x_{1}$$y_{2}$$x_{2}$$y_{3}$$x_{3}$$y_{4}$$x_{4}$

Figure 1. $C_{5}\in\text{\sc Age}(\mathcal{Q}\times\mathcal{Q})$. Its elements
are depicted by edges.

$\triangleleft$

##  3\. Equivariant Noetherianity

We prove that every totally ordered and $\omega$-well structured domain of
variables satisfies Property 2.3. Moreover, almost conversely, Property 2.3
implies that domain of variables is $\omega$-well structured.

###### Theorem 3.1.

If the polynomial ring $\mathbb{K}[\mathcal{A}]$ is equivariantly Noetherian
for some commutative ring $\mathbb{K}$ then $\mathcal{A}$ is $\omega$-well
structured.

For every $\omega$-well structured and totally ordered domain of variables
$\mathcal{A}$ and a Noetherian commutative ring $\mathbb{K}$, the polynomial
ring $\mathbb{K}[\mathcal{A}]$ is equivariantly Noetherian.

###### Proof.

Suppose, towards contradiction, that an equivariant ideal
$\mathcal{I}\subseteq\mathbb{K}[\mathcal{A}]$ is not finitely generated. Then
there exists an infinite sequence $f_{0},f_{1},f_{2},\dots$ of polynomials in
$\mathcal{I}$ such that
$f_{n}\in\mathcal{I}\setminus\langle\left\\{f_{0},\dots,f_{n-1}\right\\}\rangle$
for all $n\in\mathbb{N}$. Since $\preceq_{\text{\tiny lex}}$ is well-founded
we can furthermore assume that $\text{\sc cp}(f_{n})$ is $\preceq_{\text{\tiny
lex}}$-minimal for all $n$, i.e. there is no
$g\in\mathcal{I}\setminus\langle\left\\{f_{1},\dots,f_{n-1}\right\\}\rangle$
such that $\text{\sc cp}(g)\prec_{\text{\tiny lex}}\text{\sc cp}(f_{n})$. As
$\sqsubseteq$ is a well partial order, the sequence $(\text{\sc
cp}(f_{n}))_{n\in\mathbb{N}}$ contains an infinite non-decreasing subsequence:

$\text{\sc cp}(f_{n_{1}})\ \sqsubseteq\ \text{\sc cp}(f_{n_{2}})\ \sqsubseteq\
\dots$

Let $\mathcal{J}_{k}\subseteq\mathbb{K}$ be the ideal generated by
$\\{\text{\sc lc}(f_{n_{1}}),\dots,\text{\sc lc}(f_{n_{k}})\\}$. We have thus
an increasing chain of ideals in $\mathbb{K}$,

$\mathcal{J}_{1}\ \subseteq\ \mathcal{J}_{2}\ \subseteq\ \dots,$

which necessarily stabilises as $\mathbb{K}$ is Noetherian. Let
$K\in\mathbb{N}$ be such that $\mathcal{J}_{n}=\mathcal{J}_{K}$ for all $n\geq
K$. As $\mathcal{J}_{K+1}=\mathcal{J}_{K}$, there are
$r_{1},\dots,r_{K}\in\mathbb{K}$ such that

(4) $\displaystyle\text{\sc lc}(f_{n_{K+1}})=\sum_{i=1}^{K}r_{i}\cdot\text{\sc
lc}(f_{n_{i}}).$

Moreover, since $\text{\sc cp}(f_{n_{i}})\sqsubseteq\text{\sc
cp}(f_{n_{K+1}})$ for $i=1\ldots K$, there are some monomials
$g_{1},\dots,g_{K}\in\text{\sc Mon}[\mathcal{A}]$ and embeddings
$\iota_{1},\dots,\iota_{K}\in{\text{\sc Emb}_{\mathcal{A}}}$ such that

$\displaystyle g_{i}\cdot\iota_{i}(\text{\sc lm}(f_{n_{i}}))$
$\displaystyle=\text{\sc lm}(f_{n_{K+1}})$ $\displaystyle\iota_{i}(\text{\sc
vars}(f_{n_{i}}))$ $\displaystyle\subseteq\text{\sc vars}(f_{n_{i+1}})$

for $i=1\ldots K$. Using the fact that $\text{\sc lm}(\\_)$ and $\text{\sc
vars}(\\_)$ both commute with the action of embeddings, and Lemma 3, the left-
hand side can be rewritten to:

(5) $\displaystyle\text{\sc lm}(g_{i}\cdot\iota_{i}(f_{n_{i}}))$
$\displaystyle=\text{\sc lm}(f_{n_{K+1}})$ (6) $\displaystyle\text{\sc
vars}(\iota_{i}(f_{n_{i}}))$ $\displaystyle\subseteq\text{\sc
vars}(f_{n_{i+1}})$

Since $\text{\sc lt}(f_{n_{i}})=\text{\sc lc}(f_{n_{i}})\cdot\text{\sc
lm}(f_{n_{i}})$, by the equalities (4) and (5) we get:

$\text{\sc lt}(f_{n_{K+1}})\ =\ \sum_{i=1}^{K}r_{i}\cdot\text{\sc
lt}(g_{i}\cdot\iota_{i}(f_{n_{i}})).$

Using the equality $r\cdot\text{\sc lt}(f)=\text{\sc lt}(r\cdot f)$, we
rewrite further to:

$\displaystyle\text{\sc lt}(f_{n_{K+1}})\ =\ \sum_{i=1}^{K}\text{\sc
lt}(r_{i}\cdot g_{i}\cdot\iota_{i}(f_{n_{i}})).$

The left-hand side of the above equality contains just one term, therefore
$\text{\sc lm}(f_{n_{K+1}})=\text{\sc lm}(r_{i}\cdot
g_{i}\cdot\iota_{i}(f_{n_{i}}))$ for some $i\in\left\\{1\ldots K\right\\}$,
and leading monomials different that $\text{\sc lm}(f_{n_{K+1}})$ cancel out
in the right-hand side sum. Dropping summands with leading monomials different
that $\text{\sc lm}(f_{n_{K+1}})$ yields:

(7) $\displaystyle\text{\sc lt}(f_{n_{K+1}})\ =\ \text{\sc
lt}\big{(}\sum_{i=1}^{K}r_{i}\cdot g_{i}\cdot\iota_{i}(f_{n_{i}})\big{)}.$

Let $f^{\prime}$ be the polynomial appearing on the right-hand side:

$f^{\prime}\ :=\ \sum_{i=1}^{K}r_{i}\cdot g_{i}\cdot\iota_{i}(f_{n_{i}}).$

As $f^{\prime}\in\mathcal{I}_{n_{K}}$ and
$f_{n_{K+1}}\in\mathcal{I}_{n_{K+1}}\setminus\mathcal{I}_{n_{K}}$, the
difference of polynomials
$(f_{n_{K+1}}-f^{\prime})\in\mathcal{I}_{n_{K+1}}\setminus\mathcal{I}_{n_{K}}$.
All the leading terms appearing on both sides of (7) cancel out in
$f_{n_{K+1}}-f^{\prime}$. We thus deduce

$\text{\sc lm}(f_{n_{K+1}}-f^{\prime})\prec_{\text{\tiny lex}}\text{\sc
lm}(f_{n_{K+1}}).$

Moreover, by (5) and (6) we deduce

$\text{\sc vars}(f_{n_{K+1}}-f^{\prime})\subseteq\text{\sc vars}(f_{n_{K+1}})\
.$

Combining the last two statements we obtain

$\text{\sc cp}(f_{n_{K+1}}-f^{\prime})\prec_{\text{\tiny lex}}\text{\sc
cp}(f_{n_{K+1}}),$

a contradiction with $\preceq_{\text{\tiny lex}}$-minimality of $\text{\sc
cp}(f_{n_{K+1}})$, which completes the proof. ∎

###### Lemma 3.2.

If $\mathbb{K}[\mathcal{A}]$ is equivariantly Noetherian and $\mathcal{B}$ is
a reduct of $\mathcal{A}$ then $\mathbb{K}[\mathcal{B}]$ is also equivariantly
Noetherian.

###### Proof.

Since ${\text{\sc Emb}_{\mathcal{A}}}\subseteq\text{\sc Emb}_{\mathcal{B}}$,
every equivariant ideal $\mathcal{I}$ in $\mathbb{K}[\mathcal{B}]$ is
automatically an equivariant ideal in $\mathbb{K}[\mathcal{A}]$, and therefore
$\mathcal{I}$ is finitely generated in there. Furthermore, again due to
${\text{\sc Emb}_{\mathcal{A}}}\subseteq\text{\sc Emb}_{\mathcal{B}}$, a
finite basis of $\mathcal{I}$ in $\mathbb{K}[\mathcal{A}]$ is also its basis
in $\mathbb{K}[\mathcal{B}]$. ∎

###### Remark 3.3.

Theorem 3 applies in particular to: every ordinal (by Lemma 2.5); rational
order $\mathcal{Q}$; equality domain (by Lemma 3.2); lexicographic products
thereof (by Lemma 2). All subsequent results in this paper apply to all the
above-listed domains too.

According to Pouzet’s conjecture (Pouzet20), necessary and sufficient
conditions of Theorems 3.1 and 3 coincide, namely every $\omega$-well
structured structure may be equipped with a total order while preserving
$\omega$-well structure:

###### Conjecture 3.4 ((Pouzet20)).

Every $\omega$-well structured relational structure $\mathcal{A}$ is a reduct
of an $\omega$-well structured, totally ordered structure.

The conjecture, together with Theorems 3.1 and 3, and Lemma 3.2, would imply
that Property 2.3 is satisfied exactly by reducts of $\omega$-well structured
and totally ordered domains of variables.

### Quasi orders on monomials.

We need some definitions before proving Theorems 3.1 and 3. In the sequel let
$\mathbb{K}$ be a fixed Noetherian commutative ring, and let
$\mathcal{A}=(A,\preceq,\ldots)$ be a fixed domain of variables, totally
ordered by $\preceq$. We define three quasi orders on monomials, related by
the following refinements:

$\textstyle{f\preceq_{\text{\tiny lex}}f^{\prime}\ }$$\textstyle{\ f\mid
f^{\prime}\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\
f\sqsubseteq f^{\prime}.}$

The two left ones are standard orders. Given two monomials $f$ and
$f^{\prime}$, _division order_ is defined by $f\mid f^{\prime}$ if $f\cdot
g=f^{\prime}$ for some $g\in\text{\sc Mon}[\mathcal{A}]$. In order to define
_lexicographic order_ , we consider the $\preceq$-largest variable $a\in A$
such that $\text{\sc deg}_{f}\,a\neq\text{\sc deg}_{f^{\prime}}\,a$, and set
$f\prec_{\text{\tiny lex}}f^{\prime}$ if $\text{\sc deg}_{f}\,a<\text{\sc
deg}_{f^{\prime}}\,a$. Lexicographic order is a _term order_ :

###### Lemma 3.5.

For every monomials $f,f^{\prime},g\in\text{\sc Mon}[\mathcal{A}]$,

$f\mid f^{\prime}\implies f\preceq_{\text{\tiny lex}}f^{\prime}\implies f\cdot
g\preceq_{\text{\tiny lex}}f^{\prime}\cdot g.$

The quasi order $\sqsubseteq$ is defined as relaxation of division order
modulo renamings of variables:

(8) $\displaystyle\begin{aligned} f\sqsubseteq
f^{\prime}&\iff\exists\iota\in{\text{\sc Emb}_{\mathcal{A}}}:\iota(f)\mid
f^{\prime}.\end{aligned}$

We argue that (8) defines a quasi order, i.e., a transitive relation. Indeed,
as action of embeddings preserves the division order, namely

$\displaystyle f\mid f^{\prime}$
$\displaystyle\implies\kappa(f)\mid\kappa(f^{\prime})$

for every $\kappa\in{\text{\sc Emb}_{\mathcal{A}}}$, we may deduce
transitivity of $\sqsubseteq$:

$\iota(f)\mid f^{\prime}\ \wedge\ \kappa(f^{\prime})\mid f^{\prime\prime}\
\implies\ (\kappa\circ\iota)(f)\mid\kappa(f^{\prime})\mid f^{\prime\prime}.$

$\text{\sc Mon}[\mathcal{A}]$ may be identified with $\text{\sc
Age}(\mathcal{A},\mathbb{N}\setminus 0)$, and $\sqsubseteq$ with the quasi
order determined by $\omega$ on $\text{\sc
Age}(\mathcal{A},\mathbb{N}\setminus 0)$. Thus $\sqsubseteq$ is a wqo, if
$\mathcal{A}$ is $\omega$-well structured.

###### Definition 3.6.

Given a non-zero polynomial $f\in\mathbb{K}[\mathcal{A}]$, $f\neq\mathbf{0}$,
the _leading monomial_ $\text{\sc lm}(f)\in\text{\sc Mon}[\mathcal{A}]$ of $f$
is the $\preceq_{\text{\tiny lex}}$-largest monomial appearing in $f$; the
_leading coefficient_ $\text{\sc lc}(f)\in\mathbb{K}$ of $f$ is the coeffcient
of $\text{\sc lm}(f)$ in $f$; and the _leading term_ of $f$ is $\text{\sc
lt}(f)=\text{\sc lc}(f)\cdot\text{\sc lm}(f)$.

For every $f\in\mathbb{K}[\mathcal{A}]$ and $g\in\text{\sc Mon}[\mathbb{K}]$
it holds $\text{\sc lm}(g\cdot f)\ =g\cdot\text{\sc lm}(f)$ and $\text{\sc
lt}(g\cdot f)\ =g\cdot\text{\sc lt}(f)$.

###### Proof.

Due to Lemma 3.5, the $\preceq_{\text{\tiny lex}}$-largest monomial $\text{\sc
lm}(f)$ in $f$, after mutliplying $f$ by a monomial $g$, is still the
$\preceq_{\text{\tiny lex}}$-largest monomial in $g\cdot f$, namely $\text{\sc
lm}(g\cdot f)=g\cdot\text{\sc lm}(f)$. As $g$ is a monomial, we have
$\text{\sc lc}(g\cdot f)=\text{\sc lc}(f)$, which implies $\text{\sc
lt}(g\cdot f)=g\cdot\text{\sc lt}(f)$. ∎

### Characteristic pairs.

Instead of just monomials, we consider monomial-set pairs:

$\text{\sc C}[\mathcal{A}]\ =\ \left\\{(f,v)\in\text{\sc
Mon}[\mathcal{A}]\times\mathcal{P}_{\text{\tiny fin}}(A)\,\middle|\,\text{\sc
vars}(f)\subseteq v\right\\}.$

###### Definition 3.7.

The _characteristic pair_ of $f$ is defined as $\text{\sc cp}(f)=(\text{\sc
lm}(f),\text{\sc vars}(f))\in\text{\sc C}[\mathcal{A}]$.

We extend division and lexicographic orders to $\text{\sc C}[\mathcal{A}]$ by
combining them with inclusion (we overload symbols $\mid$ and
$\preceq_{\text{\tiny lex}}$):

$\displaystyle(f,v)\ \mid\ (f^{\prime},v^{\prime})$ $\displaystyle\iff f\mid
f^{\prime}\ \wedge\ v\subseteq v^{\prime}$
$\displaystyle(f,v)\prec_{\text{\tiny lex}}(f^{\prime},v^{\prime})$
$\displaystyle\iff f\prec_{\text{\tiny lex}}f^{\prime}\ \wedge\ v\subseteq
v^{\prime}.$

While lexicographic order on monomials does not need to be well founded, its
extension to $\text{\sc C}[\mathcal{A}]$ does. This is crucial in the sequel.
The extended $\preceq_{\text{\tiny lex}}$ is well founded.

###### Proof.

We need to show that every decreasing chain

$(f_{1},v_{1})\succeq_{\text{\tiny lex}}(f_{2},v_{2})\succeq_{\text{\tiny
lex}}\ldots$

eventually stabilises. The second component eventually stabilises, i.e., there
is $n\in\mathbb{N}$ and $v\subseteq_{\text{fin}}A$ such that for all $i\geq n$
we have $v_{i}=v$. Since $v$ is finite, lexicographic order is well founded on
$\left\\{f\in\text{\sc Mon}[\mathcal{A}]\,\middle|\,\text{\sc
vars}(f)\subseteq v\right\\}$, and therefore $f_{n}\succeq_{\text{\tiny
lex}}f_{n+1}\succeq_{\text{\tiny lex}}\ldots$ eventually stabilises too. ∎

Similarly we extend $\sqsubseteq$ to $\text{\sc C}[\mathcal{A}]$, by combining
relaxation of division order (8) with inclusion:

(9) $\displaystyle(m,v)\ \sqsubseteq\
(m^{\prime},v^{\prime})\iff\exists\iota\in{\text{\sc
Emb}_{\mathcal{A}}}:\iota(m)\mid m^{\prime}\wedge\iota(v)\subseteq
v^{\prime}.$

###### Lemma 3.8.

The extended $\sqsubseteq$ is a wqo, if $\mathcal{A}$ is $\omega$-well
structured.

###### Proof.

Given a pair $(f,v)\in\text{\sc C}[\mathcal{A}]$, define
$(\ell_{(f,v)}:v\to\mathbb{N})\in\text{\sc Age}(\mathcal{A},\mathbb{N})$ as
follows:

$\ell_{(f,v)}(a)\ =\ \begin{cases}\text{\sc deg}_{f}\,a&\text{ if
}a\in\text{\sc vars}(f)\\\ 0&\text{ if }a\in v\setminus\text{\sc
vars}(f).\end{cases}$

We observe that $(f,v)\sqsubseteq(f^{\prime},v^{\prime})$ exactly when
$\ell_{(f,v)}\rightsquigarrow\ell_{(f^{\prime},v^{\prime})}$ are related by
the quasi order determined by $\omega=(\mathbb{N},\leq)$. Therefore
$\sqsubseteq$ is a wqo, since $\mathcal{A}$ is $\omega$-well structured. ∎

### Proof of Theorem 3.

Fix a totally ordered and $\omega$-well structured domain
$\mathcal{A}=(A,\preceq,\ldots)$. For simplicity, we restrict to the case when
$\mathbb{K}$ is a _field_ – the general proof for an arbitrary Noetherian
commutative ring is in Appendix. We proceed by a careful adaptation of the
classical proof, see e.g. (Cox15, Section 2.5) using $\sqsubseteq$ in place of
division order, and characteristic pairs in place of just leading monomials.

Consider an arbitrary ideal $\mathcal{I}\subseteq\mathbb{K}[\mathcal{A}]$, and
the set of characteristic pairs of all polynomials in $\mathcal{I}$:

$\text{\sc cp}(\mathcal{I})=\left\\{\text{\sc
cp}(f)\,\middle|\,f\in\mathcal{I}\right\\}.$

Let $J\subseteq\text{\sc C}[\mathcal{A}]$ be the upward closure of $\text{\sc
cp}(\mathcal{I})$ with respect to $\sqsubseteq$:

$J=\left\\{(f,v)\in\text{\sc
C}[\mathcal{A}]\,\middle|\,(f^{\prime},v^{\prime})\sqsubseteq(f,v)\text{ for
some }(f^{\prime},v^{\prime})\in\text{\sc cp}(\mathcal{I})\right\\}.$

The set $J$ is thus upward-closed and therefore has a finite basis
$B\subseteq_{\text{fin}}J$ (relying on Lemmas 2.4 and 3.8). W.l.o.g.
$B\subseteq\text{\sc cp}(\mathcal{I})$, as $J$ is the upward closure of
$\text{\sc cp}(\mathcal{I})$. Therefore: For every $(f,v)\in B$, there is a
polynomial $g_{f,v}\in\mathcal{I}$ such that $\text{\sc cp}(g_{f,v})=(f,v)$.
Let $\mathcal{B}=\left\\{g_{f,v}\,\middle|\,(f,v)\in B\right\\}$. We prove
that $\mathcal{B}$ is a basis of $\mathcal{I}$, i.e.,
$\mathcal{I}=\langle\mathcal{B}\rangle$.

One inclusion is obvious, $\langle\mathcal{B}\rangle\subseteq\mathcal{I}$. In
order to prove the opposite inclusion suppose, towards contradiction, that
$\mathcal{I}\setminus\langle\mathcal{B}\rangle$ is nonempty. Take any
polynomial $g\in\mathcal{I}\setminus\langle\mathcal{B}\rangle$ whose
characteristic pair $(f,v)=\text{\sc cp}(g)$ is $\preceq_{\text{\tiny
lex}}$-minimal, i.e., there is no
$g^{\prime}\in\mathcal{I}\setminus\langle\mathcal{B}\rangle$ with $\text{\sc
cp}(g^{\prime})\prec_{\text{\tiny lex}}\text{\sc cp}(g)$ (cf. Lemma3). Choose
any $(f^{\prime},v^{\prime})\in B$ such that
$(f^{\prime},v^{\prime})\sqsubseteq(f,v)$, i.e., there is some $h\in\text{\sc
Mon}[\mathcal{A}]$ and $\iota\in{\text{\sc Emb}_{\mathcal{A}}}$ such that

$h\cdot\iota(f^{\prime})=f\qquad\iota(v^{\prime})\subseteq v.$

Equivalently, using Claim 3 and taking
$g^{\prime}=g_{f^{\prime},v^{\prime}}\in\mathcal{B}$, we have:

$h\cdot\iota(\text{\sc lm}(g^{\prime}))=\text{\sc lm}(g)\qquad\iota(\text{\sc
vars}(g^{\prime}))\subseteq\text{\sc vars}(g).$

As $\text{\sc lm}(\\_)$ and $\text{\sc vars}(\\_)$ both commute with the
action of embeddings, the two equalities rewrite first to

(10) $\displaystyle h\cdot\text{\sc lm}(\iota(g^{\prime}))\ =\ \text{\sc
lm}(g)\qquad\text{\sc vars}(\iota(g^{\prime}))\ \subseteq\ \text{\sc
vars}(g),$

and then, by Lemma 3, the first one rewrites further to

(11) $\displaystyle\text{\sc lm}(h\cdot\iota(g^{\prime}))\ $ $\displaystyle=\
\text{\sc lm}(g).$

Let $g^{\prime\prime}$ be the polynomial appearing on the left-hand side:
$g^{\prime\prime}\ :=h\cdot\iota(g^{\prime}).$ By (11), the leading terms
appearing on both sides of (11) cancel out in $g-g^{\prime\prime}$. We thus
have

(12) $\displaystyle\text{\sc lm}(g-g^{\prime\prime})\prec_{\text{\tiny
lex}}\text{\sc lm}(g).$

Furthermore, by the first equality in (10) we get $\text{\sc
vars}(h)\subseteq\text{\sc vars}(g)$, and then by the second one we get
$\text{\sc vars}(g^{\prime\prime})\subseteq\text{\sc vars}(g)$, and hence

(13) $\displaystyle\text{\sc vars}(g-g^{\prime\prime})\subseteq\text{\sc
vars}(g).$

By (12) and (13) we thus derive:

(14) $\displaystyle\text{\sc cp}(g-g^{\prime\prime})\prec_{\text{\tiny
lex}}\text{\sc cp}(g).$

Finally, as both $\langle\mathcal{B}\rangle$ and $\mathcal{I}$ are ideals,
knowing that
$g^{\prime\prime}\in\langle\mathcal{B}\rangle\subseteq\mathcal{I}$ and
$g\in\mathcal{I}\setminus\langle\mathcal{B}\rangle$, we deduce:

(15)
$\displaystyle(g-g^{\prime\prime})\in\mathcal{I}\setminus\langle\mathcal{B}\rangle.$

Conditions (14) and (15) are in contradiction with $\preceq_{\text{\tiny
lex}}$-minimality of $\text{\sc cp}(g)$, which completes the proof of Theorem
3. ∎

### Proof of Theorem 3.1.

Let $\mathcal{A}=(A,\ldots)$ be a relational structure and $\mathbb{K}$ a
commutative ring such that $\mathbb{K}[\mathcal{A}]$ is equivariantly
Noetherian. It is sufficient to prove that $(\text{\sc
Mon}[\mathcal{A}],\sqsubseteq)$ is a wqo, as it is isomorphic to the quasi
order determined by $\omega=(\mathbb{N},\leq)$ on $\text{\sc
Age}(\mathcal{A},\mathbb{N}\setminus 0)$, and hence also on $\text{\sc
Age}(\mathcal{A},\mathbb{N})$.

Given any infinite sequence of monomials $f_{1},f_{2},\ldots$, we prove that
it contains a dominating pair. Let
$\mathcal{I}_{i}\subseteq\mathbb{K}[\mathcal{A}]$ be the equivariant ideal
generated by the set $\left\\{f_{1},\ldots,f_{i-1}\right\\}$. Clearly,
$\mathcal{I}_{1}\subseteq\mathcal{I}_{2}\subseteq\ldots$.
$\mathcal{I}_{i}=\mathcal{I}_{i+1}$ for some $i\in\mathbb{N}$. To prove the
claim, let $\mathcal{I}\subseteq\mathbb{K}[\mathcal{A}]$ be the equivariant
ideal of polynomials generated by the infinite set
$\left\\{f_{1},f_{2},\ldots\right\\}$. By assumption, it has a finite basis
$\mathcal{B}$, $\mathcal{I}=\langle\mathcal{B}\rangle$. Choose
$i\in\mathbb{N}$ such that $\mathcal{B}\subseteq\mathcal{I}_{i}$. Then
$\mathcal{I}_{i}=\langle\mathcal{B}\rangle=\mathcal{I}$ and hence
$\mathcal{I}_{i}=\mathcal{I}_{i+1}=\ldots=\mathcal{I}$.

By the claim we have $f_{i+1}\in\mathcal{I}_{i}$, i.e., for some
$r_{1},\ldots,r_{i}\in\mathbb{K}$, embeddings
$\iota_{1},\ldots,\iota_{i}\in{\text{\sc Emb}_{\mathcal{A}}}$, and monomials
$h_{1},\ldots,h_{i}\in\text{\sc Mon}[\mathbb{K}]$,

$f_{i+1}\ =\ r_{1}\cdot h_{1}\cdot\iota_{1}(f_{1})+\ldots+r_{i}\cdot
h_{i}\cdot\iota_{i}(f_{i}).$

Since $f_{i+1}$ is a monomial, all monomials $h_{k}\cdot\iota_{k}(f_{k})$
different than $f_{i+1}$ necessarily cancel out, and moreover $f_{i+1}$ has to
be equal to $h_{k}\cdot\iota_{k}(f_{k})$ for some $k\leq i$. In other words,
we get a dominating pair $f_{k}\sqsubseteq f_{i+1}$, as required. ∎

##  4\. Application: Orbit-finitely generated vector spaces

We use Theorem 3 to give a simple proof of a generalisation of the key result
of (BKM21): orbit-finitely generated vector spaces have finite chains of
equivariant subspaces. In the following, $\mathbb{K}$ is a field and
$\mathcal{A}=(A,\ldots)$ an $\omega$-well structured relational structure.

### Orbit-finitely generated vector spaces.

For $d\in\mathbb{N}$, consider the vector space $\text{\sc Lin}(A^{d})$ freely
generated by the set $A^{d}$ of $d$-tuples of elements of $A$. Thus $\text{\sc
Lin}(A^{d})$ consists of finite formal sums

(16) $\displaystyle r_{1}\cdot t_{1}+\ldots+r_{m}\cdot t_{m},$

where $r_{1},\ldots,r_{m}\in\mathbb{K}$ and $t_{1},\ldots,t_{m}\in A^{d}$.
Equivalently, $\text{\sc Lin}(A^{d})$ may be defined as the set of all
functions $v:A^{d}\to\mathbb{K}$ such that $v(t)\neq 0$ for finitely many
$t\in A^{d}$. Addition of vectors (16) and multiplication by a scalar
$r\in\mathbb{K}$ are then defined pointwise, as expected. Embeddings
$\iota\in{\text{\sc Emb}_{\mathcal{A}}}$ act pointwise on tuples
$t=(a_{1},\ldots,a_{d})$, namely $\iota(t)=(\iota(a_{1}),\ldots$,
$\iota(a_{d}))$, and also pointwise on vectors:

$\iota(r_{1}\cdot t_{1}+\ldots+r_{m}\cdot t_{m})\ =\
r_{1}\cdot\iota(t_{1})+\ldots+r_{m}\cdot\iota(t_{m}).$

A subset of $\text{\sc Lin}(A^{d})$ is called _equivariant_ if it is invariant
under action of ${\text{\sc Emb}_{\mathcal{A}}}$.

###### Example 4.1.

When $d=2$, generators are ordered pairs $(a,a^{\prime})\in A^{2}$. A vector
in $\text{\sc Lin}(A^{2})$ can be presented as a finite directed graph,
possibly containing self-loops, whose nodes are elements $a\in A$ and edges
are labelled by elements of the field $\mathbb{K}$. Addition of vectors
amounts to merging two such graphs, and adding labels of common edges.
Multiplication by a scalar $r\in\mathbb{K}$ amount to multiplying labels of
all edges by $r$. The set of those graphs where the sum of labels is 0 is an
equivariant subspace of $\text{\sc Lin}(A^{2})$. $\triangleleft$

We encode vectors as polynomials as follows. A single generator
$t=(a_{1},a_{2},\ldots,a_{d})\in A^{d}$ is encoded as the monomial

$\text{\sc enc}(t)\ =\
{a_{1}}^{1}\cdot{a_{2}}^{2}\cdot\ldots\cdot{a_{d}}^{2^{d}}.$

As repetitions $a_{i}=a_{j}$ are allowed, the degree of a variable $a$ is thus
equal to the sum of powers $2^{i}$, ranging over positions $i$ such that
$a_{i}=a$. This guarantees injectivity of $\text{\sc enc}(\\_)$, namely
different tuples $t$ have different encodings. Then a vector $v=r_{1}\cdot
t_{1}+\ldots+r_{m}\cdot t_{m}$ is encoded as the polynomial

$\text{\sc enc}(v)\ =\ r_{1}\cdot\text{\sc
enc}(t_{1})+\ldots+r_{m}\cdot\text{\sc enc}(t_{m}),$

which yields a linear map $\text{\sc enc}(\\_):\text{\sc
Lin}(A^{d})\to\mathbb{K}[\mathcal{A}]$.

Vector space $\text{\sc Lin}(A^{d})$ is indeed _orbit-finitely generated_ once
$\mathcal{A}$ is assumed to be $\omega$-well structured, due to the following
lemma:

###### Lemma 4.2 (oligomorphicity444 If we restrict to automorphisms, instead
of all embeddings, this is a characterisation of oligomorphic automophism
groups (Cameron), and $\omega$-categorical structures (H97). Furthermore, as
mentioned in Section 2, when $\mathcal{A}$ is homogeneous, action of
embeddings is essentially the same as action of automorphisms. ).

$A^{d}$ is orbit-finite, namely $A^{d}={\text{\sc
Emb}_{\mathcal{A}}}(B)\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\left\\{\iota(t)\,\middle|\,\iota\in{\text{\sc
Emb}_{\mathcal{A}}},t\in B\right\\}$ for some $B\subseteq_{\text{fin}}A^{d}$.

Any such finite set $B$ we call a _presentation_ of $A^{d}$.

###### Proof.

Suppose $A^{d}$ is orbit-infinite. In such case there is an infinite sequence
$t_{1},t_{2},\ldots\in A^{d}$ such that $A^{d}={\text{\sc
Emb}_{\mathcal{A}}}(\left\\{t_{1},t_{2},\ldots\right\\})$ and $(*)$ there is
no $i,j\in\mathbb{N}$ and embedding $\iota\in{\text{\sc Emb}_{\mathcal{A}}}$
such that $\iota(t_{i})=t_{j}$. We know that $(\text{\sc
Mon}[\mathbb{K}],\sqsubseteq)$ is a wqo and hence the infinite sequence of
monomials

$\text{\sc enc}(t_{1}),\ \text{\sc enc}(t_{2}),\ \ldots$

in $\text{\sc Mon}[\mathbb{K}]$ admits a domination, namely $\iota(\text{\sc
enc}(t_{i}))\mid\text{\sc enc}(t_{j})$ for some $i<j$ and $\iota\in{\text{\sc
Emb}_{\mathcal{A}}}$. A crucial fact is that all monomials used in encodings
have the same degree $D=1+2+\ldots+2^{d}=2^{d+1}-1$, understood as the sum of
degrees of all variables. Therefore $\iota(\text{\sc enc}(t_{i}))\mid\text{\sc
enc}(t_{j})$ implies $\iota(\text{\sc enc}(t_{i}))=\text{\sc enc}(t_{j})$. The
encoding commutes with action of embeddings: $\iota(\text{\sc
enc}(t))=\text{\sc enc}(\iota(t))$. This implies $\text{\sc
enc}(\iota(t_{i}))=\text{\sc enc}(t_{j})$, and by injectivity of $\text{\sc
enc}(\\_)$ also $\iota(t_{i})=t_{j}$, thus contradicting $(*)$. ∎

### Finite length.

Theorem 4.3 generalises (BKM21, Lemma IV.8) which only considers
$\mathcal{A}=\mathcal{Q}=(Q,\leq_{\mathcal{Q}})$. On the other hand, (BKM21)
provides explicite upper bound on the length.

###### Theorem 4.3 (Finite length).

Let $\mathbb{K}$ be any field. If $\mathcal{A}$ is a reduct of an
$\omega$-well structured and totally ordered structure then strictly
increasing chains of equivariant subspaces of $\text{\sc
Lin}(\mathcal{A}^{d})$ are finite.

###### Proof.

Consider any increasing chain of equivariant subspaces

$\mathcal{V}_{1}\subseteq\mathcal{V}_{2}\subseteq\ldots$

and let $\mathcal{I}_{i}$ be the ideal in $\mathbb{K}[\mathcal{A}]$ generated
(in the classical sense) by $\text{\sc enc}(\mathcal{V}_{i})$, the encodings
of vectors from $\mathcal{V}_{i}$. As action of embeddings commutes with
encoding, equivariance of subspaces $\mathcal{V}_{i}$ implies equivariance of
the sets $\text{\sc enc}(\mathcal{V}_{i})$. As action of embeddings commutes
with addition and multiplication of polynomials, ideals $\mathcal{I}_{i}$ are
equivariant. By Theorem 3 and Lemma 3.2, the chain
$\mathcal{I}_{1}\subseteq\mathcal{I}_{2}\subseteq\ldots$ stabilises, namely,
$\mathcal{I}_{i}=\mathcal{I}_{j}$ for all sufficiently large $i,j$. We claim:
$\mathcal{I}_{i}=\mathcal{I}_{j}$ implies $\text{\sc
enc}(\mathcal{V}_{i})=\text{\sc enc}(\mathcal{V}_{j})$. Having the claim we
immediately complete the proof, as $\text{\sc enc}(\mathcal{V}_{i})=\text{\sc
enc}(\mathcal{V}_{j})$ implies $\mathcal{V}_{i}=\mathcal{V}_{j}$, by
injectivity of $\text{\sc enc}(\\_)$.

For demonstrating the claim it is sufficient to prove the inclusion $\text{\sc
enc}(\mathcal{V}_{i})\supseteq\text{\sc enc}(\mathcal{V}_{j})$. Given an
arbitrary polynomial $f\in\text{\sc enc}(\mathcal{V}_{j})$, we thus prove
$f\in\text{\sc enc}(\mathcal{V}_{i})$. As $\mathcal{I}_{i}=\mathcal{I}_{j}$,
we have $f\in\mathcal{I}_{i}$, i.e.,

(17) $\displaystyle f\ =\ r_{1}\cdot h_{1}\cdot\text{\sc
enc}(v_{1})+\ldots+r_{n}\cdot h_{n}\cdot\text{\sc enc}(v_{n})$

for some vectors $v_{1},\ldots,v_{n}\in\mathcal{V}_{i}$, monomials
$h_{1},\ldots,h_{n}\in\text{\sc Mon}[\mathbb{K}]$ and ring elements
$r_{1},\ldots,r_{n}\in\mathbb{K}$. As all monomials used in encodings have the
same degree $D$, all monomials $g$ appearing in $\text{\sc
enc}(v_{1}),\ldots,\text{\sc enc}(v_{n})$ have degree $\text{\sc deg}\,g=D$,
as well as all monomials appearing in $f$. This means that all the monomials
of degree larger than $D$, obtained as a multiplication $h_{i}\cdot g$,
forcedly cancel out in the final sum (17). Formally ($\mathbf{0}$ is the zero
polynomial):

$\sum_{i\in I}r_{i}\cdot h_{i}\cdot\text{\sc enc}(v_{i})\ =\ \mathbf{0},$

where the sum ranges over those $i$ where $h_{i}$ has positive degree:
$I=\left\\{i\in\left\\{1\ldots n\right\\}\,\middle|\,\text{\sc
deg}\,h_{i}>0\right\\}.$ All polynomials $r_{i}\cdot h_{i}\cdot\text{\sc
enc}(v_{i})$, for $i\in I$, can be thus safely removed. As $\text{\sc
deg}\,h_{i}=0$ exactly when $h_{i}$ is a unit monomial, we end up with

$f\ =\ \sum_{i\notin I}r_{i}\cdot\text{\sc enc}(v_{i})\ =\ \text{\sc
enc}(\sum_{i\notin I}r_{i}\cdot v_{i}),$

the latter equality following from linearity of $\text{\sc enc}(\\_)$.
Therefore $f\in\text{\sc enc}(\mathcal{V}_{i})$, as required. ∎

### Weighted Register Automata.

Using Theorem 4.3 we obtain a generalisation of another result of (BKM21):
decidability of zeroness of weighted register automata.

For $d\in\mathbb{N}$, let $Q_{d}=A^{d}\cup\\{\bot\\}$. The auxiliary element
$\bot$ is assumed to be equivariant, namely $\iota(\bot)=\bot$ for all
$\iota\in{\text{\sc Emb}_{\mathcal{A}}}$. The vector space $\text{\sc
Lin}(Q_{d})$ is defined like $\text{\sc Lin}(A^{d})$, as the set of finite
formal sums of elements of $Q_{d}$.

Classically, transition function of a weighted automaton with finite state-
space $Q$ maps every input symbol and state to a vector over states:
$\Sigma\times Q\to\text{\sc Lin}(Q)$. Our definition of weighted $d$-register
automaton (equivalent to the definition of (BKM21)) is along the same lines,
except that input alphabet is $\Sigma=A$, state-space is orbit-finite
$Q=Q_{d}$, and transition function is equivariant.

A weighted $d$-register automaton consists of a _transition_ function
$\delta:A\times Q_{d}\to\text{\sc Lin}(Q_{d})$ and a _final_ function
$F:Q_{d}\to\mathbb{K}$, both equivariant, namely for every $a\in A$, $q\in
Q_{d}$, and $\iota\in{\text{\sc Emb}_{\mathcal{A}}}$:

$\delta(\iota(a),\iota(q))\ =\ \iota(\delta(a,q))\qquad F(\iota(a))\ =\ F(a).$

$F$ extends uniquely to a linear map $F:\text{\sc Lin}(Q_{d})\to\mathbb{K}$.
Likewise, for every $a\in A$, the function $\delta(a,\\_):Q_{d}\to\text{\sc
Lin}(Q_{d})$ extends uniquely to a linear map $\widetilde{\delta}(a):\text{\sc
Lin}(Q_{d})\to\text{\sc Lin}(Q_{d})$. We overload $\bot$ and use it for vector
defined by the singleton formal sum $\bot\in\text{\sc Lin}(Q_{d})$, the
_initial_ vector. The semantics of a weighted register automaton
$(d,\delta,F)$ maps every word $w=a_{1}\ldots a_{\ell}\in A^{*}$ to the
_final_ vector

$\widetilde{\delta}(w)\ =\
\widetilde{\delta}(a_{\ell})\circ\ldots\circ\widetilde{\delta}(a_{1})(\bot)\
\in\ \text{\sc Lin}(Q_{d}),$

on which $F$ is evaluated to get the _value_
$F(\widetilde{\delta}(w))\in\mathbb{K}$ assigned by the automaton to $w$. By
equivariance of $\bot$, $\delta$ and $F$, the function $\widetilde{\delta}$ is
equivariant and the value is stable under the pointwise action of ${\text{\sc
Emb}_{\mathcal{A}}}$ on words, $\iota(a_{1}\ldots
a_{\ell})=\iota(a_{1})\ldots\iota(a_{\ell})$.

###### Lemma 4.4.

$F(\widetilde{\delta}(\iota(w)))=F(\widetilde{\delta}(w))$ for every
$\iota\in{\text{\sc Emb}_{\mathcal{A}}}$.

The _zeroness_ problem asks, given a weighted register automaton
$(d,\delta,F)$, whether it is _zeroing_ , i.e., whether it assigns value 0 to
all input words. When an automaton is input to an algorithm, each of the
functions $\delta$, $F$ is given by its values on a (naturally defined)
presentation of its domain. We prove that zeroness is characterised by a
finite testing set:

###### Theorem 4.5.

Let $\mathbb{K}$ be any field and $\mathcal{A}$ be a reduct of an
$\omega$-well structured and totally ordered structure. For every weighted
register automaton there is a finite set $T\subseteq A^{*}$ such that the
automaton is zeroing if and only if it assigs value 0 to all words in $T$.

###### Proof.

Consider a weighted register automaton $(d,\delta,F)$. For $i\in\mathbb{N}$,
let $A^{\leq i}=A^{0}\cup\ldots\cup A^{i}$, and
$\mathcal{V}_{i}\subseteq\text{\sc Lin}(Q_{d})$ be the vector space spanned by
$V_{i}=\widetilde{\delta}(A^{\leq i})\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\left\\{\widetilde{\delta}(w)\,\middle|\,w\in A^{\leq i}\right\\}$.
Let $B_{i}$ be a presentation of $A^{i}$, and let $B_{\leq
i}=B_{0}\cup\ldots\cup B_{i}$. Therefore

(18) $\displaystyle A^{\leq i}={\text{\sc Emb}_{\mathcal{A}}}(B_{\leq i}),$

and by equivariance of $\widetilde{\delta}$ we have:

(19) $\displaystyle V_{i}={\text{\sc
Emb}_{\mathcal{A}}}(\widetilde{\delta}(B_{\leq i})).$

Thus the sets $V_{i}$ are equivariant, and so are the subspaces
$\mathcal{V}_{i}$. As an immediate consequence of Theorem 4.3 we obtain:
Strictly increasing chains of equivariant subspaces of $\text{\sc Lin}(Q_{d})$
are finite.

###### Proof.

We claim that subspaces of $\text{\sc Lin}(Q_{d})$ split into two types
defined below. Consider an equivariant subspace $\mathcal{V}\subseteq\text{\sc
Lin}(Q_{d})$ and its projection $\mathcal{V}^{\prime}\subseteq\text{\sc
Lin}(A^{d})$ to $\text{\sc Lin}(A^{d})$. If $\mathcal{V}$ contains a vector
$r\cdot\bot$ for some $r\neq 0$ then $\mathcal{V}$ contains vectors
$r\cdot\bot$ for all $r\in\mathbb{K}$ and therefore
$\mathcal{V}=\mathcal{V}^{\prime}\times\mathbb{K}$. Otherwise, every vector
$v^{\prime}\in\mathcal{V}^{\prime}$ extends uniquely to a vector in
$\mathcal{V}$. In both cases, whenever two subspaces
$\mathcal{V}_{1},\mathcal{V}_{2}\subseteq\text{\sc Lin}(Q_{d})$ are related by
strict inclusion, their projections
$\mathcal{V}^{\prime}_{1},\mathcal{V}^{\prime}_{2}$ to $\text{\sc Lin}(A^{d})$
also are:

(20)
$\displaystyle\mathcal{V}_{1}\subset\mathcal{V}_{2}\implies\mathcal{V}^{\prime}_{1}\subset\mathcal{V}^{\prime}_{2}.$

Furthermore, a subspace of the first type is never included in a subspace of
the second type. Therefore every strictly increasing chain
$\mathcal{V}_{1}\subset\mathcal{V}_{2}\subset\ldots$ of equivariant subspaces
of $\text{\sc Lin}(Q_{d})$ splits into two subchains: a chain of subspaces of
the second type, followed by chain of subspaces of the first type. By (20)
each of the subchains corresponds to a strictly increasing chain of subspaces
of $\text{\sc Lin}(A^{d})$, and hence is finite by Theorem 4.3. In
consequence, the whole chain is necessarily finite. ∎

By the claim, the chain
$\mathcal{V}_{0}\subseteq\mathcal{V}_{1}\subseteq\ldots,$ stabilises at some
$n$:

(21) $\displaystyle\mathcal{V}_{n}=\mathcal{V}_{n+1}=\ldots.$

Since the transformation $\mathcal{V}_{i}\mapsto\mathcal{V}_{i+1}$ does not
depend on $i$, the stabilisation (21) is guaranteed once
$\mathcal{V}_{n}=\mathcal{V}_{n+1}$. Zeroness of $(d,\delta,F)$ is then
equivalent to $F(\widetilde{\delta}(w))=0$ for all $w\in A^{\leq n}$. Using
(18) and Lemma 4.4 we refine the characterisation: Zeroness of $(d,\delta,F)$
is equivalent to $F(\widetilde{\delta}(w))=0$ for all $w\in B_{\leq n}$. Hence
$T=B_{\leq n}$ satisfies Theorem 4.5, which is thus proved. ∎

###### Remark 4.6.

Under mild computability assumptions on $\mathbb{K}$ and $\mathcal{A}$
(omitted here for simplicity, but satisfied by all $\omega$-well structured
domains mentioned so far), this characterisation yields decidability of the
zeroness problem. This generalises (BKM21, Lemma VIII.1), but without
providing complexity upper bound. Indeed, a stabilisation point $n$ (21) can
be computed as follows: enumerate in parallel, for all $n\in\mathbb{N}$,
linear combinations of vectors from $V_{n}$, and stop when

$\widetilde{\delta}(B_{\leq n+1})\ \subseteq\ V_{n}.$

Indeed, by (19), this implies $V_{n+1}\subseteq V_{n}$, and hence
$\mathcal{V}_{n+1}\subseteq\mathcal{V}_{n}$. Once a stabilisation point $n$ is
computed, zeroness of an automaton is decided by computing the value assigned
to all words in $B_{\leq n}$.

##  5\. Computability assumptions

We now formulate computability assumptions on a field $\mathbb{K}$ and
structure $\mathcal{A}$ which are necessary in subsequent sections.

A field $\mathbb{K}$ is _computable_ , i.e., its elements are finitely
represented, and field operations can be computed using this representation.
So is, for instance, the rational field $\mathbb{Q}$, as well as every finite
field.

The rest of this section is devoted to spelling out computability assumptions
on an $\omega$-well structured structure $\mathcal{A}=(A,\ldots)$, in
Definition 5.4 below. Given $B\in\text{\sc Age}(\mathcal{A})$, any restriction
${\iota}{|B}$ of an embedding to $B$ we call _local embedding_ of $B$. It is
legitimate to use local embeddings instead of embeddings, as their action on a
polynomial depends only on restriction to its variables:

###### Lemma 5.1.

${\iota}{|\text{\sc vars}(f)}={\iota^{\prime}}{|\text{\sc
vars}(f)}\implies\iota(f)=\iota^{\prime}(f)$.

By ${{\text{\sc Emb}_{\mathcal{A}}}}{|B}$ we denote the set of all local
embeddings of $B$:

${{\text{\sc Emb}_{\mathcal{A}}}}{|B}\ =\
\left\\{{\iota}{|B}\,\middle|\,\iota\in{\text{\sc
Emb}_{\mathcal{A}}}\right\\}.$

For $B,B^{\prime}\in\text{\sc Age}(\mathcal{A})$, we consider the Cartesian
product

$B\boxtimes B^{\prime}\ \stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\
({{\text{\sc Emb}_{\mathcal{A}}}}{|B})\times({{\text{\sc
Emb}_{\mathcal{A}}}}{|B}^{\prime}).$

We extend to this set the action of embeddings: for $\kappa\in{\text{\sc
Emb}_{\mathcal{A}}}$ and $(\pi,\pi^{\prime})\in B\boxtimes B^{\prime}$, we put
$\kappa(\pi,\pi^{\prime})=(\kappa\circ\pi,\kappa\circ\pi^{\prime})$. Clearly,
$B\boxtimes B^{\prime}$ is closed under this action, i.e., it is equivariant.

###### Lemma 5.2.

For $B,B^{\prime}\in\text{\sc Age}(\mathcal{A})$, $B\boxtimes B^{\prime}$ is
orbit-finite, namely $B\boxtimes B^{\prime}={\text{\sc
Emb}_{\mathcal{A}}}(F)\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\left\\{(\kappa\circ\pi,\kappa\circ\pi^{\prime})\,\middle|\,\kappa\in{\text{\sc
Emb}_{\mathcal{A}}},(\pi,\pi^{\prime})\in F\right\\}$ for some finite
$F\subseteq B\boxtimes B^{\prime}$.

Any such finite set $F$ we call a _presentation_ of $B\boxtimes B^{\prime}$.

###### Proof.

Let $n=|B|$ and $n^{\prime}=|B^{\prime}|$. The set $B\boxtimes B^{\prime}$ is
essentially a subset of $\mathcal{A}^{n+n^{\prime}}$. Formally, having fixed
enumerations $B=\left\\{b_{1},\ldots,b_{n}\right\\}$,
$B^{\prime}=\left\\{b^{\prime}_{1},\ldots,b^{\prime}_{n^{\prime}}\right\\}$,
we define an injective mapping $m:B\boxtimes
B^{\prime}\to\mathcal{A}^{n+n^{\prime}}$ as expected:

$(\pi,\pi^{\prime})\ \mapsto\
(\pi(b_{1}),\ldots,\pi(b_{n}),\pi^{\prime}(b^{\prime}_{1}),\ldots,\pi^{\prime}(b^{\prime}_{n^{\prime}})).$

The mapping is equivariant, namely commutes with the action of embeddings:
$m(\iota(\pi,\pi^{\prime}))\ =\ \iota(m(\pi,\pi^{\prime}))$ for every
$\iota\in{\text{\sc Emb}_{\mathcal{A}}}$. Therefore, equivariance of
$B\boxtimes B^{\prime}$ implies equivariance of $m(B\boxtimes B^{\prime})$. By
Lemma 4.2, the set $\mathcal{A}^{n+n^{\prime}}$ is orbit-finite. Importantly,
the same proof shows that _every_ equivariant subset of
$\mathcal{A}^{n+n^{\prime}}$ is orbit-finite. Therefore, $m(B\boxtimes
B^{\prime})={\text{\sc Emb}_{\mathcal{A}}}(F)$ for some finite set $F$. We use
injectivity and equivariance of $m$ to deduce that $m^{-1}(F)$ is a finite
presentation of $B\boxtimes B^{\prime}$. ∎

###### Example 5.3.

For illustration, consider the structure ${\omega=(\mathbb{N},\leq)}$, whose
embeddings are strictly monotonic maps $\omega\to\omega$, and
$B=\left\\{2\right\\}$ and $B^{\prime}=\left\\{1,3\right\\}$. A presentation
of $B\boxtimes B^{\prime}$ is given by $F$ containing five pairs
$(\pi,\pi^{\prime})$ of local embeddings, corresponding to five cases:
$\pi(2)$ is smaller than $\pi^{\prime}(1)$, or equal to $\pi^{\prime}(1)$, or
between $\pi^{\prime}(1)$ and $\pi^{\prime}(3)$, or equal to
$\pi^{\prime}(3)$, or larger than $\pi^{\prime}(3)$:

$\displaystyle\pi_{1}:2{\mapsto}2$
$\displaystyle\quad\pi^{\prime}_{1}:(1,3){\mapsto}(3,5)$
$\displaystyle\quad\pi_{4}:2{\mapsto}3$
$\displaystyle\quad\pi^{\prime}_{4}:(1,3){\mapsto}(1,3)$
$\displaystyle\pi_{2}:2{\mapsto}2$
$\displaystyle\quad\pi^{\prime}_{2}:(1,3){\mapsto}(2,4)$
$\displaystyle\quad\pi_{5}:2{\mapsto}4$
$\displaystyle\quad\pi^{\prime}_{5}:(1,3){\mapsto}(1,3)$
$\displaystyle\pi_{3}:2{\mapsto}2$
$\displaystyle\quad\pi^{\prime}_{3}:(1,3){\mapsto}(1,3)$

The following two pairs are not in $F$, for different reasons:

$\sigma_{1}:2{\mapsto}4\quad\sigma^{\prime}_{1}:(1,3){\mapsto}(1,4)\qquad\sigma_{2}:2{\mapsto}3\quad\sigma^{\prime}_{2}:(1,3){\mapsto}(2,3).$

The left pair $(\sigma_{1},\sigma^{\prime}_{1})$ belongs to $B\boxtimes
B^{\prime}$ but factorizes through $(\pi_{4},\pi^{\prime}_{4})$, namely
$(\sigma_{1},\sigma^{\prime}_{1})=\kappa(\pi_{4},\pi^{\prime}_{4})$ where
$\kappa(0)=0,\kappa(1)=1$, $\kappa(2)=2$, and $\kappa(n)=n+1$ for $n\geq 3$.
The right pair does not even belong to $B\boxtimes B^{\prime}$, as
$\sigma^{\prime}_{2}$ does not extend to an embedding. $\triangleleft$

###### Definition 5.4.

We say that an $\omega$-well structured domain $\mathcal{A}$ is _computable_
if its elements can be finitely represented, and the following tasks are
computable using this representation:

  1. $(\textsc{c}_{1})$

Given $B\in\text{\sc Age}(\mathcal{A})$ and $\pi:B\to A$, decide if
$\pi\in{{\text{\sc Emb}_{\mathcal{A}}}}{|B}$.

  2. $(\textsc{c}_{2})$

Given $B,B^{\prime}\in\text{\sc Age}(\mathcal{A})$, compute a presentation of
$B\boxtimes B^{\prime}$.

In particular, every finite $\mathcal{A}$ is computable. $\triangleleft$

(Our condition $(\textsc{c}_{2})$ is similar to EGB4 in (BD11).) By reusing
the proof of (HKL18, Proposition 3.4) we can show that the ordinal $\omega$,
seen as a relational structure, is computable. In fact the proof can be easily
extended to ordinals $\alpha$ which are _effective_ , by which we mean that
elements of $\alpha$ (i.e., ordinals smaller than $\alpha$) are finitely
represented, and ordinal order $<$ and addition $+$ are computable using this
representation. For example, the ordinals $\omega$, $\omega^{k}$,
$\omega^{\omega}$ and $\varepsilon_{0}$ are effective, using Cantor Normal
Form. Any effective ordinal $\alpha$, seen as a relational structure, is
computable.

###### Proof.

We start by considering $\omega$; later we explain how to extend the proof to
any effective ordinal. Let $B\subseteq_{\text{fin}}\omega$ be a nonempty
subset of $\omega$. A function $\pi:B\to\omega$ extends to an embedding
$\omega\to\omega$ if and only if the following conditions hold:

(22) $\displaystyle\begin{aligned} &b\leq\pi(b)&&\text{ where }b=\min B\\\
&b_{2}-b_{1}\leq\pi(b_{2})-\pi(b_{1})&&\text{ for every }b_{1}\leq
b_{2}.\end{aligned}$

This implies $(\textsc{c}_{1})$.

Concering $(\textsc{c}_{2})$, given $B,B^{\prime}\in\text{\sc
Age}(\mathcal{A})$, we compute $B\boxtimes B^{\prime}$ by a dynamic algorithm
with respect to the orders on $B$ and $B^{\prime}$: for every two initial
segments $C\subseteq B$ and $C^{\prime}\subseteq B^{\prime}$, we compute
$C\boxtimes C^{\prime}$, as follows (the algorithm is similar to (HKL18,
Proposition 3.4)).

The trivial set
$\emptyset\boxtimes\emptyset=\left\\{(\emptyset,\emptyset)\right\\}$ contains
just one pair of empty functions. Consider two initial segments $C\subseteq B$
and $C^{\prime}\subseteq B^{\prime}$. Assume
$\overline{C}\boxtimes\overline{C}^{\prime}$ is already computed for all pairs
of initial segments smaller than $C,C^{\prime}$, i.e. for all pairs
$(\overline{C},\overline{C}^{\prime})\neq(C,C^{\prime})$ of initial segments
$\overline{C}\subseteq C$ and $\overline{C}^{\prime}\subseteq C^{\prime}$. For
computing $C\boxtimes C^{\prime}$ we use $\overline{C}\subseteq C$ obtained
from $C$ by removing the largest element $b$ (assuming $C$ is nonempty), and
$\overline{C}^{\prime}\subseteq C^{\prime}$ obtained from $C^{\prime}$ by
removing the largest element $b^{\prime}$ (assuming $C^{\prime}$ is nonempty).
We compute $C\boxtimes C^{\prime}$ by applying the following three procedures
(note that their pre-conditions are not disjoint):

  * •

Suppose both $C$ and $C^{\prime}$ are nonempty. For every
$(\bar{\pi},\bar{\pi}^{\prime})\in\overline{C}\boxtimes\overline{C}^{\prime}$
we extend $\bar{\pi}$ and $\bar{\pi}^{\prime}$ to $\pi:C\to\omega$ and
$\pi^{\prime}:C^{\prime}\to\omega$ by mapping both $b$ and $b^{\prime}$ to the
minimal value $\pi(b)=\pi^{\prime}(b^{\prime})\in\omega$ satisfying the
condition (22) for both $\pi$ and $\pi^{\prime}$. We add all so obtained pairs
$(\pi,\pi^{\prime})$ to $C\boxtimes C^{\prime}$.

  * •

Suppose $C$ is nonempty (while $C^{\prime}$ is either empty or not). For every
$(\bar{\pi},\pi^{\prime})\in\overline{C}\boxtimes C^{\prime}$ we extend
$\bar{\pi}:\overline{C}\to\omega$ to $\pi:C\to\omega$ by mapping $b$ to the
minimal value $\pi(b)$ outside of the range $\pi^{\prime}(C^{\prime})$ that
satisfies the condition (22). We add all so obtained pairs
$(\pi,\pi^{\prime})$ to $C\boxtimes C^{\prime}$.

  * •

Supposing $C^{\prime}$ is nonempty (while $C$ is either empty or not), we
proceed symmetrically to the previous case.

This completes the procedure to compute $B\boxtimes B^{\prime}$. We have thus
completed the proof for $\omega$.

The proof extends to any ordinal $\alpha$, as long as ordinal subtraction is
computable in $\alpha$, where subtraction of ordinals $\beta-\gamma$, for
$\gamma<\beta<\alpha$, is defined as the unique ordinal $\eta$ such that
$\beta=\gamma+\eta$ (the order of addition is important since addition of
ordinals is not commutative). For any effective ordinal $\alpha$ and
$\gamma<\beta<\alpha$, subtraction $\beta-\gamma$ is computable by enumerating
ordinals $\eta<\alpha$ and testing whether $\beta=\gamma+\eta$. ∎

Lexicographic product of two computable domains is computable.

###### Proof.

Let $\mathcal{A}=(A,\ldots)$ and $\mathcal{B}=(B,\ldots)$ be two computable,
$\omega$-well structured domains. We will show that
$\mathcal{A}\otimes{\mathcal{B}}$ is also computable.

First, assuming that $\mathcal{A}$ and $\mathcal{B}$ satisfy
$(\textsc{c}_{1})$, we show that $\mathcal{A}\otimes{\mathcal{B}}$ satisfies
$(\textsc{c}_{1})$ as well. For $B\in\text{\sc
Age}(\mathcal{A}\otimes{\mathcal{B}})$ let $\overline{B}\in\text{\sc
Age}(\mathcal{A})$ be its projection on the first coordinate. Moreover, for
$a\in\overline{B}$, let $B_{a}=\left\\{a^{\prime}\in
A^{\prime}\,\middle|\,(a,a^{\prime})\in B\right\\}\in\text{\sc
Age}(\mathcal{B})$. Given $B\in\text{\sc Age}(\mathcal{A})$ and $\pi:B\to
A\times A^{\prime}$, we need to check if $\pi$ extend to an embedding of
$\mathcal{A}\otimes{\mathcal{B}}$. W.l.o.g. assume that $\pi$ preserves
equality in first coordinate since (this necessary condition can be easily
checked). Then, $\pi$ induces a map $\overline{\pi}:\overline{B}\to A$ and
maps $\pi_{a}:B_{a}\to A^{\prime}$ for $a\in\overline{B}$. By Lemma 2, $\pi$
extends to an embedding of $\mathcal{A}\otimes{\mathcal{B}}$ only if
$\overline{\pi}$ extends to an embedding $\overline{\iota}$ of $\mathcal{A}$
and for every $a\in\overline{B}$, the map $\pi_{a}$ extend to an embedding
$\iota_{a}$ of $\mathcal{B}$. Moreover if both these conditions are satisfied,
then $\pi$ does extend to the embedding of $\mathcal{A}\otimes{\mathcal{B}}$
determined by $\overline{\iota}$ and the family of embeddings
$(\iota_{a}\in\text{\sc Emb}_{\mathcal{B}})_{a\in A}$, where $\iota_{a}$ is
arbitrary for $a\notin\overline{B}$. Since $\mathcal{A}$ and $\mathcal{B}$
satisfy $(\textsc{c}_{1})$, the conditions can be checked and hence
$\mathcal{A}\otimes\mathcal{B}$ satisfies $(\textsc{c}_{1})$.

Now, assuming further that $\mathcal{A}$ and $\mathcal{B}$ satisfy
$(\textsc{c}_{2})$, we show that $\mathcal{A}\otimes{\mathcal{B}}$ satisfies
$(\textsc{c}_{2})$ as well, i.e., given $V,W\in\text{\sc
Age}(\mathcal{A}\otimes{\mathcal{B}})$, we show how to compute a presentation
$E$ of $V\boxtimes W$. Let $X\in\text{\sc Age}(\mathcal{A})$ be the union of
projections of $V$ and $W$ to the first coordinate:

$X=\overline{V}\cup\overline{W}=\left\\{a\in A\,\middle|\,(a,b)\in V\cup
W\text{ for some }b\in B\right\\}.$

Likewise, let $Y\in\text{\sc Age}(\mathcal{B})$ be the union of projections of
$V$ and $W$ to the second coordinate:

$Y=\bigcup_{a\in X}(V_{a}\cup W_{a})=\left\\{b\in B\,\middle|\,(a,b)\in V\cup
W\text{ for some }a\in A\right\\}.$

Above we assume $V_{a}=\emptyset$ when $a\notin\overline{V}$, and likewise for
$W_{a}$. Let $Z=X\times Y\in\text{\sc Age}(\mathcal{A}\otimes{\mathcal{B}})$.
If $F$ is a presentation of $Z\boxtimes Z$, then

$E:=\left\\{({f}{|V},{g}{|W})\,\middle|\,(f,g)\in F\right\\}$

is a presentation of $V\boxtimes W$.

### Proof:

Consider $(p,q)\in V\boxtimes W$. There exists $(p^{\prime},q^{\prime})\in
Z\boxtimes Z$ such that ${p^{\prime}}{|V}=p$ and ${q^{\prime}}{|W}=q$. There
exists $(f,g)\in F$ and $\iota\in\text{\sc
Emb}_{\mathcal{A}\otimes{\mathcal{B}}}$ such that

$\iota\circ f=p^{\prime}\qquad\text{ and }\qquad\iota\circ g=q^{\prime}\ .$

Which implies

$\iota\circ{f}{|V}=p\qquad\text{ and }\qquad\iota\circ{g}{|W}=q\ .$

As $(p,q)\in V\boxtimes W$ is arbitrary, the claim is proved. $\triangleleft$

It remains to show how to compute a presentation $F$ of $Z\boxtimes Z$. As
$\mathcal{A}$ and $\mathcal{B}$ satisfy $(\textsc{c}_{2})$, we can compute
presentations $S$ and $T$ of $X\boxtimes X$ and $Y\boxtimes Y$ respectively.
Before progressing further we notice that for any set $U$ we have
$U\boxtimes\emptyset=\left\\{(\textrm{Id}_{U},\textrm{Id}_{\emptyset})\right\\}$
and $\emptyset\boxtimes
U=\left\\{(\textrm{Id}_{\emptyset},\textrm{Id}_{U})\right\\}$. Let
$s=(s_{1},s_{2})$ be an arbitrary element in $S$. Let $s(X):=s_{1}(X)\cup
s_{2}(X)$. We define a family of finite subsets $I_{s}$ indexed by $s(X)$ as
follows:

$I_{s}(a)=\begin{cases}T&\text{when }a\in s_{1}(X)\cap s_{2}(X)\\\
\left\\{(\textrm{Id}_{Y},\textrm{Id}_{\emptyset})\right\\}&\text{when }a\in
s_{1}(X)\setminus s_{2}(X)\\\
\left\\{(\textrm{Id}_{\emptyset},\textrm{Id}_{Y})\right\\}&\text{when }a\in
s_{2}(X)\setminus s_{1}(X).\end{cases}$

We put:

$I_{s}:=\prod_{a\in s(X)}I_{s}(a).$

For every $t=(t^{a}_{1},t^{a}_{2})_{a\in s(X)}\in I_{s}$ we define
$f^{s,t}=(f^{s,t}_{1},f^{s,t}_{2})\in Z\boxtimes Z$ as:

$f^{s,t}_{i}(a,b)=(s_{i}(a),t^{s_{i}(a)}_{i}(b)).$

We now prove that

$F:=\left\\{f^{s,t}\,\middle|\,s\in S,\ t\in I_{s}\right\\}$

is a presentation of $Z\boxtimes Z$. Towards this aim, consider an arbitrary
$u=(u_{1},u_{2})\in Z\boxtimes Z$. The two local embeddings $u_{1},u_{2}$
induce maps $\overline{u}_{1},\overline{u}_{2}\in{\text{\sc
Emb}_{\mathcal{A}}}{|X}$ and hence $(\overline{u}_{1},\overline{u}_{2})\in
X\boxtimes X$. Since $S$ is a presentation of $X\boxtimes X$, there exists
$\overline{j}\in\text{\sc Emb}_{\mathcal{A}}$ and $s=(s_{1},s_{2})\in S$ such
that

$\overline{j}\circ
s_{1}=\overline{u}_{1}\qquad\text{and}\qquad\overline{j}\circ
s_{2}=\overline{u}_{2}\ .$

This implies the following equalities:

$\displaystyle\overline{j}(s_{1}(X)\cap s_{2}(X))$
$\displaystyle=\overline{u}_{1}(X)\cap\overline{u}_{2}(X)$
$\displaystyle\overline{j}(s_{1}(X)\setminus s_{2}(X))$
$\displaystyle=\overline{u}_{1}(X)\setminus\overline{u}_{2}(X)$
$\displaystyle\overline{j}(s_{2}(X)\setminus s_{1}(X))$
$\displaystyle=\overline{u}_{2}(X)\setminus\overline{u}_{1}(X).$

For every $a\in s(X)$, the local embeddings $u_{1}$ and $u_{2}$ induce local
embeddings $u^{a}_{1}$ and $u^{a}_{2}$ in ${\text{\sc Emb}_{\mathcal{B}}}{|Y}$
and ${\text{\sc Emb}_{\mathcal{B}}}{|Y}$, respectively. Since $T$ is a
presentation of $Y\boxtimes Y$, there exists $(p^{a}_{1},p^{a}_{2})\in T$ and
$j_{a}\in\text{\sc Emb}_{\mathcal{B}}$ such that

$j_{a}\circ p^{a}_{1}=u^{a}_{1}\qquad\text{and}\qquad j_{a}\circ
p^{a}_{2}=u^{a}_{2}\ .$

Define $t\in I_{s}$ as

$(t^{a}_{1},t^{a}_{2})=\begin{cases}(p^{a}_{1},p^{a}_{2})&\text{when }a\in
s_{1}(X)\cap s_{2}(X)\\\ (\textrm{Id}_{Y},\textrm{Id}_{\emptyset})&\text{when
}a\in s_{1}(X)\setminus s_{2}(X)\\\
(\textrm{Id}_{\emptyset},\textrm{Id}_{Y})&\text{when }a\in s_{2}(X)\setminus
s_{1}(X)\ .\\\ \end{cases}$

We finish the proof by showing that there exists $\iota\in\text{\sc
Emb}_{{\mathcal{A}}\otimes{\mathcal{B}}}$ such that

(23) $\iota\circ f^{s,t}_{1}=u_{1}\qquad\text{and}\qquad\iota\circ
f^{s,t}_{2}=u_{2}\ .$

For $a\in s(X)$ there exists $v^{a}_{1},v^{a}_{2}\in\text{\sc
Emb}_{\mathcal{B}}$ such that

${v^{a}_{1}}{|X}=u^{a}_{1}\qquad\text{and}\qquad{v^{a}_{2}}{|X}=u^{a}_{2}\ .$

Define a family of embeddings $\iota_{a}$ indexed by $a\in\mathcal{A}$ as

$\iota_{a}=\begin{cases}j_{a}&\text{when }a\in s_{1}(X)\cap s_{2}(X)\\\
v^{a}_{1}&\text{when }a\in s_{1}(X)\setminus s_{2}(X)\\\ v^{a}_{2}&\text{when
}a\in s_{2}(X)\setminus s_{1}(X)\\\
\textrm{Id}_{Y}&\text{otherwise.}\end{cases}$

Using Lemma 2 we can determine $\iota\in\text{\sc
Emb}_{{\mathcal{A}}\otimes{\mathcal{B}}}$ by $\overline{j}$ and the family of
embeddings $\iota_{a}$. It is routine to verify that $\iota$ satisfies (23). ∎

##  6\. Gröbner bases

In this section we set up the background for deciding the ideal membership
problem in Section 7. Let $\mathbb{K}$ be a computable field. Let
$\mathcal{A}=(A,\preceq,\ldots)$ be a computable, $\omega$-well structured and
_well ordered_ domain (we thus strengthen the total order assumption).
Therefore, the lexicographic order on monomials is well founded.

### Division step.

Let $\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]\setminus\\{\mathbf{0}\\}$ be
a set of nonzero polynomials. Given polynomials
$f,f^{\prime}\in\mathbb{K}[\mathcal{A}]$, we write

(24) $\displaystyle f\longrightarrow_{\mathcal{G}}f^{\prime}$

if $f^{\prime}$ is the remainder of _division_ of $f$ by some polynomial
$\iota(g)$ from ${\text{\sc Emb}_{\mathcal{A}}}(\mathcal{G})$. Formally, we
define (24) to mean that

(25) $\displaystyle f=r\cdot h\cdot\iota(g)+f^{\prime}$

for some $r\in\mathbb{K},h\in\text{\sc Mon}[\mathcal{A}]$, $\iota\in{\text{\sc
Emb}_{\mathcal{A}}}$ and $g\in\mathcal{G}$ such that the leading monomial
$\text{\sc lm}(r\cdot h\cdot\iota(g))$ (equal to $h\cdot\iota(\text{\sc
lm}(g))$) appears in $f$ with the same coefficient as in $r\cdot
h\cdot\iota(g)$ (namely $r\cdot\text{\sc lc}(g)$). The monomial $\text{\sc
lm}(r\cdot h\cdot\iota(g))$ is called the _head_ of the division step (24).
The head is the largest monomial that disappears from $f$, i.e., does not
appear any more in $f^{\prime}=f-r\cdot h\cdot\iota(g)$. All monomials in $f$
lexicographically larger than the head appear also in $f^{\prime}$ with the
same coefficients, while some monomials lexicographically smaller than the
head may be added or removed by a division step.

Recall that $\langle\mathcal{G}\rangle$ denotes the equivariant ideal
generated by $\mathcal{G}$. Using equality (25) we deduce:

###### Lemma 6.1.

Division step preserves membeship in $\langle\mathcal{G}\rangle$: if
$f\longrightarrow_{\mathcal{G}}f^{\prime}$ then
$f\in\langle\mathcal{G}\rangle\iff f^{\prime}\in\langle\mathcal{G}\rangle$.

A polynomial $f$ is said to be _reduced_ with respect to $\mathcal{G}$ if
there is no $f^{\prime}\in\mathbb{K}[\mathcal{A}]$ such that
$f\longrightarrow_{\mathcal{G}}f^{\prime}$.

###### Lemma 6.2.

Let $\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$ be a finite set of nonzero
polynomials. Every sequence of division steps

(26) $\displaystyle
f_{1}\longrightarrow_{\mathcal{G}}f_{2}\longrightarrow_{\mathcal{G}}f_{3}\longrightarrow_{\mathcal{G}}\ldots$

terminates, i.e., ends in a reduced polynomial.

###### Proof.

By _reduction ab absurdum_ : assuming an infinite sequence of division steps
(26), we deduce that the lexicographic order $\preceq_{\text{\tiny lex}}$ on
monomials $\text{\sc Mon}[\mathcal{A}]$ is not well founded.

Given an infinite sequence of division steps (26), we construct an infinite
forest $\mathcal{F}$, whose nodes are labelled by monomials, as the limit of
an increasing sequence of finite forests
${\mathcal{F}}_{1},{\mathcal{F}}_{2},\ldots$. The construction will maintain
the invariant that all monomials appearing in $f_{i}$ are among labels of
leaves in ${\mathcal{F}}_{i}$ (we _mark_ these leaves, for distinguishing them
from other leaves). The forest ${\mathcal{F}}_{1}$ consists just of (finitely
many) roots, labeled by monomials appearing in $f_{1}$, all of them marked.
Given ${\mathcal{F}}_{i}$, we define ${\mathcal{F}}_{i+1}$ by adding new
children to the marked leaf $v$ labelled by the head monomial $m$ of the
division step $f_{1}\longrightarrow_{\mathcal{G}}f_{i+1}$. The leaves are
labelled by monomials that are added by the division step, and all are marked.
The node $v$ itself becomes unmarked (even if it remains a leaf), and likewise
do all other leaves labelled by monomials of $f_{i}$ that do not appear in
$f_{i+1}$.

By the construction of $\mathcal{F}$, every two monomials $m$, $m^{\prime}$
related by an edge are in strict lexicographic order: $m\succ_{\text{\tiny
lex}}m^{\prime}$. As the sequence (26) is infinite, the forest is also
infinite and, by König’s lemma, forcedly contains an infinite branch. This
implies existence of an infinite strictly decreasing chain of monomials with
respect to lexicographic order, which is a contradiction. ∎

We write $f\longrightarrow^{*}_{\mathcal{G}}f^{\prime}$ if there is some
finite sequence of division steps from $f$ to $f^{\prime}$ and $f^{\prime}$ is
reduced.

### Gröbner basis.

A set $\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$ is said to be a _Gröbner
basis_ if for every $f\in\langle\mathcal{G}\rangle$ there exists
$g\in\mathcal{G}$ such that $\text{\sc lm}(g)\sqsubseteq\text{\sc lm}(f)$.

###### Lemma 6.3.

If $\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$ is a Gröbner basis then for
every polynomial $f\in\mathbb{K}[\mathcal{A}]$, the following conditions are
equivalent: (1) $f\in\langle\mathcal{G}\rangle$; (2)
$f\longrightarrow^{*}_{\mathcal{G}}\mathbf{0}$; (3) every sequence
$f\longrightarrow^{*}_{\mathcal{G}}f^{\prime}$ ends in
$f^{\prime}=\mathbf{0}$.

###### Proof.

The implication (2)$\implies$(1) holds for any $\mathcal{G}$. Indeed, a
sequence $f\longrightarrow^{*}_{\mathcal{G}}\mathbf{0}$ of division steps
yields a decomposition of $f$ into a sum:

$f\ =\ r_{1}\cdot h_{1}\cdot\iota_{1}(g_{1})\ +\ \ldots\ +\ r_{n}\cdot
h_{n}\cdot\iota_{n}(g_{n}),$

where $r_{1},\ldots,r_{n}\in\mathbb{K}$, $g_{1},\ldots,g_{n}\in\mathcal{G}$,
$h_{1},\ldots,h_{n}\in\mathbb{K}[\mathcal{A}]$ and
$\iota_{1},\ldots,\iota_{n}\in{\text{\sc Emb}_{\mathcal{A}}}$, which proves
membership of $f$ in $\langle\mathcal{G}\rangle$.

For (1)$\implies$(3), suppose $f\in\langle\mathcal{G}\rangle$, and consider
any sequence of division steps starting in $f$. By Lemma 6.2 the sequence is
necessarily finite, and hence ends in some reduced polynomial $f^{\prime}$. By
Lemma 6.1, $f^{\prime}\in\langle\mathcal{G}\rangle$. However, as $\mathcal{G}$
is a Gröbner basis, no nonzero polynomial in $\langle\mathcal{G}\rangle$ is
reduced, and hence $f^{\prime}=\mathbf{0}$.

The last implication (3)$\implies$(2) holds vacuously, as every polynomial $f$
admits some sequence of division steps
$f\longrightarrow^{*}_{\mathcal{G}}f^{\prime}$. ∎

###### Remark 6.4.

Note that the proof of Theorem 3 shows that every equivariant ideal has a
finite Gröbner basis. In the sequel we provide a way to _compute_ such a
basis.

### Buchberger’s algorithm.

By the least common multiple of two monomials $f,f^{\prime}\in\text{\sc
Mon}[\mathcal{A}]$, denoted as $\text{\sc lcm}(f,f^{\prime})$, we mean the
least (with respect to divisibility) monomial $g$ divisible by both $f$ and
$f^{\prime}$, i.e. satisfying $f\mid g$ and $f^{\prime}\mid g$.

###### Definition 6.5 ($S$-polynomials).

Given two distinct polynomials $f,g\in\mathbb{K}[\mathcal{A}]$, $f\neq g$, we
define their _S-polynomial_ $\mathcal{S}(f,g)$ as

$\mathcal{S}(f,g)\ :=\ \left(\frac{h}{\text{\sc lt}(f)}\cdot
f\right)-\left(\frac{h}{\text{\sc lt}(g)}\cdot g\right),$

where $h=\text{\sc lcm}(\text{\sc lm}(f),\text{\sc lm}(g))$. We say that
monomial $h$ is _cancelled out_ in $\mathcal{S}(f,g)$. For a subset
$\mathcal{G}\subseteq{\mathbb{K}[\mathcal{A}]}$ of polynomials, we put:

$\displaystyle\mathcal{S}_{\mathcal{G}}\ =\ \bigcup_{(f,g)\in{\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{G}),f\neq
g}\\!\\!\\!\\!\\!\\!\\!\mathcal{S}(f,g).$

Expanding ${\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{G})=\left\\{\iota(g)\,\middle|\,\iota\in{\text{\sc
Emb}_{\mathcal{A}}},\ g\in\mathcal{G}\right\\}$, we get:

$\displaystyle\mathcal{S}_{\mathcal{G}}\ =\
\left\\{\mathcal{S}(\iota(f),\kappa(g))\,\middle|\,\iota,\kappa\in{\text{\sc
Emb}_{\mathcal{A}}},\ f,g\in\mathcal{G},\ \iota(f)\neq\kappa(g)\right\\}.$

As action of embeddings commutes with S-polynomials, namely
$\mathcal{S}(\kappa(f),\kappa(g))\ =\ \kappa(\mathcal{S}(f,g))$ for every
$\kappa\in{\text{\sc Emb}_{\mathcal{A}}}$ and $f,g\in\mathbb{K}[\mathcal{A}]$,
the set $\mathcal{S}_{\mathcal{G}}$ is closed under the action of ${\text{\sc
Emb}_{\mathcal{A}}}$, i.e. is equivariant: $\mathcal{S}_{\mathcal{G}}\ =\
{\text{\sc Emb}_{\mathcal{A}}}(\mathcal{S}_{\mathcal{G}})$. Using assumption
$(\textsc{c}_{2})$ we derive the following key fact:

###### Lemma 6.6 (Computable presentation).

For every finite set of polynomials
$\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$, the set
$\mathcal{S}_{\mathcal{G}}$ is orbit-finite, namely

$\mathcal{S}_{\mathcal{G}}\ =\ {\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{P}_{\mathcal{G}})\
\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\
\left\\{\iota(f)\,\middle|\,\iota\in{\text{\sc
Emb}_{\mathcal{A}}},f\in\mathcal{P}_{\mathcal{G}}\right\\}$

for some presentation
$\mathcal{P}_{\mathcal{G}}\subseteq_{\text{fin}}\mathcal{S}_{\mathcal{G}}$,
which is moreover computable.

###### Proof.

We start by showing orbit-finiteness of $\mathcal{S}_{\mathcal{G}}$. As
$\mathcal{G}$ is finite and
$\mathcal{S}_{\mathcal{G}}=\bigcup_{g,g^{\prime}\in\mathcal{G}}\mathcal{S}_{g,g^{\prime}}$,
where

$\mathcal{S}_{g,g^{\prime}}\ =\
\left\\{\mathcal{S}(\iota(g),\iota^{\prime}(g^{\prime}))\,\middle|\,\iota,\iota^{\prime}\in{\text{\sc
Emb}_{\mathcal{A}}},\ \iota(g)\neq\iota^{\prime}(g^{\prime})\right\\},$

it is enough to prove that $\mathcal{S}_{g,g^{\prime}}$ is orbit-finite for
every two fixed polynomials $g,g^{\prime}\in\mathcal{G}$. Let $B=\text{\sc
vars}(g)$ and $B^{\prime}=\text{\sc vars}(g^{\prime})$, and let
$F_{g,g^{\prime}}$ be a finite presentation of $B\boxtimes B^{\prime}$ (recall
Lemma 5.2). Relying on Lemma 5.1, for a local embedding $\pi\in{{\text{\sc
Emb}_{\mathcal{A}}}}{|B}$ we write $\pi(g)$ to mean the renaming of $g$ by
_any_ extension of $\pi$ to an embedding of $\mathcal{A}$. Likewise we write
$\pi^{\prime}(g^{\prime})$, for $\pi^{\prime}\in{{\text{\sc
Emb}_{\mathcal{A}}}}{|B}^{\prime}$:

$\mathcal{S}_{g,g^{\prime}}\ =\
\left\\{\mathcal{S}(\pi(g),\pi^{\prime}(g^{\prime}))\,\middle|\,(\pi,\pi^{\prime})\in
B\boxtimes B^{\prime},\ \pi(g)\neq\pi^{\prime}(g^{\prime})\right\\}.$

Finally, we define
$\mathcal{P}_{g,g^{\prime}}\subseteq\mathcal{S}_{g,g^{\prime}}$ as the subset
of $\mathcal{S}_{g,g^{\prime}}$ obtained by restricting to local pairs of
embeddings $(\pi,\pi^{\prime})$ belonging to $F_{g,g^{\prime}}$:

$\mathcal{P}_{g,g^{\prime}}\ =\
\left\\{\mathcal{S}(\pi(g),\pi^{\prime}(g^{\prime}))\,\middle|\,(\pi,\pi^{\prime})\in
F_{g,g^{\prime}},\ \pi(g)\neq\pi^{\prime}(g^{\prime})\right\\}.$

As $F$ is finite, $\mathcal{P}_{g,g^{\prime}}$ is finite as well, and orbit-
finiteness of $\mathcal{S}_{g,g^{\prime}}$ follows once we prove that
$\mathcal{P}_{g,g^{\prime}}$ is a presentation of
$\mathcal{S}_{g,g^{\prime}}$: $\mathcal{S}_{g,g^{\prime}}={\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{P}_{g,g^{\prime}})$.

### Proof:

For proving the inclusion ${\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{P}_{g,g^{\prime}})\subseteq\mathcal{S}_{g,g^{\prime}}$,
we take any polynomial $\kappa(f)\in{\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{P}_{g,g^{\prime}})$, where $\kappa\in{\text{\sc
Emb}_{\mathcal{A}}}$ and
$f=\mathcal{S}(\pi(g),\pi^{\prime}(g^{\prime}))\in\mathcal{P}_{g,g^{\prime}}$,
and argue that $\kappa(f)\in\mathcal{S}_{g,g^{\prime}}$. As action of
embeddings commutes with S-polynomials, we have

$\kappa(\mathcal{S}(\pi(g),\pi^{\prime}(g^{\prime})))\ =\
\mathcal{S}(\kappa(\pi(g)),\kappa(\pi^{\prime}(g^{\prime}))).$

As $\kappa$ is injective, knowing $\pi(g)\neq\pi^{\prime}(g^{\prime})$, we
also know $\kappa(\pi(g))\neq\kappa(\pi^{\prime}(g^{\prime}))$, and therefore
$\kappa(f)\in\mathcal{S}_{g,g^{\prime}}$.

The opposite inclusion $\mathcal{S}_{g,g^{\prime}}\subseteq{\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{P}_{g,g^{\prime}})$ is shown similarly. We take
any polynomial
$\mathcal{S}(\pi(g),\pi^{\prime}(g^{\prime}))\in\mathcal{S}_{g,g^{\prime}}$.
As $F_{g,g^{\prime}}$ is a presentation of $B\boxtimes B^{\prime}$, there is
some $(\overline{\pi},\overline{\pi}^{\prime})\in F_{g,g^{\prime}}$ and
$\kappa\in{\text{\sc Emb}_{\mathcal{A}}}$ such that
$(\pi,\pi^{\prime})=(\kappa\circ\overline{\pi},\kappa\circ\overline{\pi}^{\prime})$.
Knowing $\kappa(\pi(g))\neq\kappa(\pi^{\prime}(g^{\prime}))$, we also know
$\pi(g)\neq\pi^{\prime}(g^{\prime})$, and therefore
$\mathcal{S}(\overline{\pi}(g),\overline{\pi}^{\prime}(g^{\prime}))\in\mathcal{P}_{g,g^{\prime}}$.
As action of embeddings commutes with S-polynomials, we get

$\mathcal{S}(\pi(g),\pi^{\prime}(g^{\prime}))\ =\
\kappa(\mathcal{S}(\overline{\pi}(g),\overline{\pi}^{\prime}(g^{\prime}))),$

and in consequence $\mathcal{S}(\pi(g),\pi^{\prime}(g^{\prime}))\in{\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{P}_{g,g^{\prime}})$. $\triangleleft$

Union of all the sets $\mathcal{P}_{g,g^{\prime}}$ yields therefore a
presentation of $\mathcal{S}_{\mathcal{G}}$:

$\mathcal{P}_{\mathcal{G}}\ \stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\
\bigcup_{g,g^{\prime}\in\mathcal{G}}\mathcal{P}_{g,g^{\prime}}.$

It is moreover computable: for every $g,g^{\prime}\in\mathcal{G}$ the finite
set $F_{g,g^{\prime}}$ is computable, by assumption $(\textsc{c}_{2})$, and
therefore the set $\mathcal{P}_{g,g^{\prime}}$ is computable as well. ∎

###### Lemma 6.7 (Orbit-finite Buchberger criterion).

A finite set $\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$ is a Gröbner basis
if and only if for all $h\in\mathcal{S}_{\mathcal{G}}$,

$h\longrightarrow^{*}_{\mathcal{G}}\mathbf{0}.$

###### Proof.

According to our definition, a finite set
$\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$ of polynomials is a Gröbner
basis if and only if the _orbit-finite_ set ${\text{\sc
Emb}_{\mathcal{A}}}(\mathcal{G})$ is a Gröbner basis in the classical sense.
As the set $\mathcal{S}_{\mathcal{G}}$ contains exactly $S$-polynomials of
pairs of polynomials from ${\text{\sc Emb}_{\mathcal{A}}}(\mathcal{G})$, we
reuse the proof of classical Buchberger criterion (which is still valid for
infinite sets, see e.g. (Cox15, Chapter 2)) to deduce the lemma. (This is
actually the only step which requires the stengthening of assumptions, i.e.,
well ordered $\mathcal{A}$.) ∎

###### Lemma 6.8 (Finite Buchberger criterion).

A finite set $\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$ is a Gröbner basis
if and only if for all $h\in\mathcal{P}_{\mathcal{G}}$,

$h\longrightarrow^{*}_{\mathcal{G}}\mathbf{0}.$

###### Proof.

The ’only if’ direction follows immediately by Lemma 6.7. For the ’if’
direction, suppose that $h\longrightarrow_{\mathcal{G}}\mathbf{0}$ for all
$h\in\mathcal{P}_{\mathcal{G}}$. Consider any
$h^{\prime}\in\mathcal{S}_{\mathcal{G}}$, i.e. $h^{\prime}=\iota(h)$ for some
$\iota\in{\text{\sc Emb}_{\mathcal{A}}}$ and $h\in\mathcal{P}_{\mathcal{G}}$.
By assumption, $h\longrightarrow^{*}_{\mathcal{G}}\mathbf{0}$. We observe that
the action of ${\text{\sc Emb}_{\mathcal{A}}}$ (i.e., renaming of variables)
preserves division steps, namely

$f\longrightarrow_{\mathcal{G}}f^{\prime}\implies\iota(f)\longrightarrow_{\mathcal{G}}\iota(f^{\prime}),$

and therefore
$\iota(h)\longrightarrow^{*}_{\mathcal{G}}\iota(\mathbf{0})=\mathbf{0}$. As
$h^{\prime}\in\mathcal{S}_{\mathcal{G}}$ is arbitrary, using Lemma 6.7 we
conclude that $\mathcal{G}$ is a Gröbner basis. ∎

Algorithm 1 is an adaptation of the classical Buchberger algorithm to our
setting. The adaptation amounts to using only polynomials from
$\mathcal{P}_{\mathcal{G}}$ instead of all S-polynomials.

Algorithm 1 Equivariant Buchberger algorithm

Input: A finite set of polynomials
$\mathcal{G}\subseteq_{\text{fin}}\mathbb{K}[\mathcal{A}]$.

repeat

for $f\in\mathcal{P}_{\mathcal{G}}$ do

compute some reduced $h\in\mathbb{K}[\mathcal{A}]$ such that
$f\longrightarrow^{*}_{\mathcal{G}}h$

if $h\neq\mathbf{0}$ then
$\mathcal{G}\leftarrow\mathcal{G}\cup\left\\{h\right\\}$

until $\mathcal{G}$ stabilizes

Output: $\mathcal{G}$

The above description is indeed an algorithm as, relying on our computability
assumption $(\textsc{c}_{1})$, we prove that one can compute some division
step from a given polynomial $f$:

###### Lemma 6.9 (Computability).

Given $f\in\mathbb{K}[\mathcal{A}]$ and
$\mathcal{G}\subseteq_{\text{fin}}\mathbb{K}[\mathcal{A}]$, one can check if
$f$ is reduced wrt. $\mathcal{G}$ and, if $f$ is not, compute some
$f^{\prime}\in\mathbb{K}[\mathcal{A}]$ such that
$f\longrightarrow_{\mathcal{G}}f^{\prime}$.

###### Proof.

For every polynomial $g\in\mathcal{G}$ and monomial $m$ of $f$, we compute the
set $D_{g,m}$ of those functions $\pi:\text{\sc vars}(\text{\sc
lm}(g))\to\text{\sc vars}(m)$ that extend to an embedding in ${\text{\sc
Emb}_{\mathcal{A}}}$ (which is checked using assumption $(\textsc{c}_{1})$)
and satisfy $\pi(\text{\sc lm}(g))\mid m$. If $D_{g,m}=\emptyset$ for all $g$
and $m$, the polynomial $f$ is reduced wrt. $\mathcal{G}$. Otherwise we pick
up arbitrary function $\pi\in D_{g,m}$, and compute some its extension
$\pi^{\prime}:\text{\sc vars}(g)\to A$ to $\text{\sc vars}(g)$ that still
extends to an embedding in ${\text{\sc Emb}_{\mathcal{A}}}$. This is doable by
enumerating all (countably many) candidates $\pi^{\prime}:\text{\sc
vars}(g)\to A$ and checking them (again relying on assumption
$(\textsc{c}_{1})$). Termination is guaranteed as $\pi$ does extend to an
embedding. Finally, we divide $m$ by $\pi^{\prime}(\text{\sc lm}(g))$ which
yields a monomial $h$ satisfying $m\ =\ h\cdot\pi^{\prime}(\text{\sc lm}(g)),$
and compute the remainder $f^{\prime}=f-r\cdot{\text{\sc lc}(g)}^{-1}\cdot
h\cdot\pi^{\prime}(g)$, where $r\in\mathbb{K}$ is the coefficient of $m$ in
$f$. ∎

The algorithm is nondeterministic, namely it may choose different sequences of
division steps $f\longrightarrow^{*}_{\mathcal{G}}h$ and hence different
reduced polynomials $h$, and therefore it may have many different runs for the
same input $\mathcal{G}$. Nevertheless, we prove termination of its every run,
and correctness of output.

###### Lemma 6.10 (Termination).

Every run of Algorithm 1 terminates on every input
$\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$.

###### Proof.

Towards contradiction, suppose some run of the algorithm is infinite. Let
$\mathcal{G}_{n}\subseteq\mathbb{K}[\mathcal{A}]$ be the value of
$\mathcal{G}$ after $n$ iterations of the while loop. Let
$\mathcal{M}_{n}=\left\\{\text{\sc
lm}(g)\,\middle|\,g\in\mathcal{G}_{n}\right\\}\subseteq\text{\sc
Mon}[\mathcal{A}]$. For every $n$ we have
$\mathcal{M}_{n}\subseteq\mathcal{M}_{n+1}$. As every polynomial $h$ added in
$(n+1)$th iteration is reduced with respect to $\mathcal{G}_{n}$, we have
$\text{\sc lm}(h)\notin\mathcal{M}_{n}$, and hence
$\mathcal{M}_{n}\subsetneq\mathcal{M}_{n+1}$ for every $n$. Therefore we can
form an infinite sequence by picking up, for every $n$, a monomial
$m_{n}\in\mathcal{M}_{n+1}\setminus\mathcal{M}_{n}$. This sequence is _bad_ ,
i.e. $m_{i}\not\sqsubseteq m_{j}$ for every $i<j$, which is in contradiction
with $\sqsubseteq$ being a wqo. ∎

###### Lemma 6.11 (Correctness).

Every run of Algorithm 1 computes, given an input
$\mathcal{G}\subseteq\mathbb{K}[\mathcal{A}]$, a Gröbner basis of
$\langle\mathcal{G}\rangle$.

###### Proof.

Each polynomial $h$ added to $\mathcal{G}$ in the algorithm is obtained from
some element of $\mathcal{G}$ by a sequence of division steps
$\longrightarrow_{\mathcal{G}}$, and hence belongs to
$\langle\mathcal{G}\rangle$. Therefore $\langle\mathcal{G}\rangle$ stays
invariant during the algorithm. Once the algorithm terminates, the set
$\mathcal{G}$ satisfies the finite Buchberger criterion and hence is a Gröbner
basis, due to Lemma 6.8. ∎

###### Remark 6.12.

In this section we strengthen the total order assumption, and assume
$\mathcal{A}$ to be well ordered, so that lexicographic order is well founded.
To this effect, in Section 3 we replaced leading monomials with characteristic
pairs. In this section this is not possible, as the proof of Lemma 6.7 does
not adapt.

##  7\. Decidability of ideal membership

As an immediate consequence of Section 6 we get:

###### Theorem 7.1.

Ideal-memb in $\mathbb{K}[\mathcal{A}]$ is decidable, for every computable
field $\mathbb{K}$ and $\omega$-well structured, well ordered and computable
domain of variables $\mathcal{A}$.

###### Proof.

Given an instance $f\in\mathbb{K}[\mathcal{A}]$ and
$\mathcal{B}\subseteq_{\text{fin}}\mathbb{K}[\mathcal{A}]$ we compute, using
Algorithm 1, a Gröbner basis $\mathcal{G}$ of $\langle\mathcal{B}\rangle$.
Then, relying on Lemmas 6.9 and 6.2, we compute some reduced polynomial
$f^{\prime}$ obtainable by a sequence of division steps
$f\longrightarrow^{*}_{\mathcal{G}}f^{\prime}$. Relying on Lemma 6.3, we
answer positively if $f^{\prime}=\mathbf{0}$. ∎

In the rest of this section we develop a method of transfering decidability of
the ideal membership problem to other structures $\mathcal{A}$. The method is
applied to the rational order $\mathcal{Q}=(Q,\leq_{\mathcal{Q}})$, which is
$\omega$-well structured and computable, but not well ordered.

### Reduction game.

Given a relational structure $\mathcal{A}=(A,\ldots)$ and $S,T\in\text{\sc
Age}(\mathcal{A})$ (source and target), by an _$(S,T)$ -local embedding_ we
mean any partial bijection $S\to T$ (i.e., a bijection from a subset of $S$ to
a subset of $T$) that extends to an embedding in ${\text{\sc
Emb}_{\mathcal{A}}}$. The set of all $(S,T)$-local embeddings we call _$(S,T)$
-profile_ of $\mathcal{A}$.

We define a game $\mathcal{G}(\mathcal{A},\mathcal{A}^{\prime})$ induced by
two relational structures $\mathcal{A}=(A,\ldots)$ and
$\mathcal{A}^{\prime}=(A^{\prime},\ldots)$. The game is played by two players,
Spoiler and Reducer, and consists of two rounds.

In the first round, Spoiler chooses $S,T\in\text{\sc Age}(\mathcal{A})$, and
Reducer responds by $S^{\prime},T^{\prime}\in\text{\sc
Age}(\mathcal{A}^{\prime})$. We call $S,S^{\prime}$ _sources_ , and
$T,T^{\prime}$ _targets_. Source and target may intersect. Reducer wins the
first round if there are bijections $\sigma:S^{\prime}\to S$, $\tau:T\to
T^{\prime}$ such that $(S^{\prime},T^{\prime})$-profile of
$\mathcal{A}^{\prime}$ is equal to $(S,T)$-profile of $\mathcal{A}$, modulo
$\sigma$ and $\tau$:

(27)
$\displaystyle(S^{\prime},T^{\prime})\textsc{-prof}(\mathcal{A}^{\prime})\ =\
\left\\{\tau\circ\pi\circ\sigma\,\middle|\,\pi\in(S,T)\textsc{-prof}(\mathcal{A})\right\\}.$

Otherwise Spoiler wins and the play ends.

In the second round, Spoiler chooses one of the structures $\mathcal{A}$,
$\mathcal{A}^{\prime}$, and a finite superset of target in this structure.
Reducer responds similarly in the other structure. This step thus yields two
_extended targets_ $\overline{T}\in\text{\sc Age}(\mathcal{A})$ and
$\overline{T^{\prime}}\in\text{\sc Age}(\mathcal{A}^{\prime})$ such that
$T\subseteq\overline{T}$ and $T^{\prime}\subseteq\overline{T^{\prime}}$.
Reducer wins the second round (and thus the whole play) if $\tau$ extends to a
bijection $\overline{\tau}:\overline{T}\to\overline{T^{\prime}}$ such that:

(28)
$\displaystyle(S^{\prime},\overline{T^{\prime}})\textsc{-prof}(\mathcal{A}^{\prime})\
=\
\left\\{\overline{\tau}\circ\pi\circ\sigma\,\middle|\,\pi\in(S,\overline{T})\textsc{-prof}(\mathcal{A})\right\\}.$

We write $\mathcal{A}\ll\mathcal{A}^{\prime}$ if Reducer has a computable
winning strategy in $\mathcal{G}(\mathcal{A},\mathcal{A}^{\prime})$.

$\mathcal{Q}\ll\omega^{2}$.

###### Proof.

A subset $X\subseteq\omega^{2}$ we call _$k$ -separated_, for
$k\in\mathbb{N}$, if each two consecutive elements of $X$ are separated by at
least $k$ elements of $\omega^{2}$, and likewise there are at least $k$
elements smaller than $\min(X)$.

Let $S,T\in\text{\sc Age}(\mathcal{Q})$ be Spoiler’s choice in the first
round. Then Reducer’s response is the following:

  * •

as source $S^{\prime}$, choose the initial fragment of $\omega$, of the same
size as $S$ (therefore $S^{\prime}\subseteq\omega$);

  * •

as target $T^{\prime}$, choose an arbitrary subset of non-zero multiplicities
of $\omega$, namely $T^{\prime}\subseteq\left\\{\omega\cdot
b\,\middle|\,b\in\omega,b>0\right\\}$, of the same size as $T$.

The unique monotonic bijections $\sigma:S^{\prime}\to S$ and $\tau:T\to
T^{\prime}$ satisfy (27), namely (a proof below):

(29) $\displaystyle(S^{\prime},T^{\prime})\textsc{-prof}(\omega^{2})\ =\
\left\\{\tau\circ\pi\circ\sigma\,\middle|\,\pi\in(S,T)\textsc{-prof}(\mathcal{Q})\right\\}.$

In the second round, if Spoiler chooses the structure $\omega^{2}$ and plays
extended target $\overline{T^{\prime}}\subseteq\omega^{2}$, Reducer responds
by arbitrary $\overline{T}\in\text{\sc Age}(\mathcal{Q})$ so that $\tau$
extends to a monotonic bijection
$\overline{\tau}:\overline{T}\to\overline{T^{\prime}}$. This is always
possible by denseness of $\leq_{\mathcal{Q}}$. Symmetrically, if Spoiler
chooses the structure $\mathcal{Q}$ and plays $\overline{T}\in\text{\sc
Age}(\mathcal{Q})$, Reducer responds by arbitrary
$\overline{T^{\prime}}\subseteq\mathbb{N}^{2}$ so that $\tau$ again extends to
a monotonic bijection $\overline{\tau}:\overline{T}\to\overline{T^{\prime}}$.
This is always possible as $T^{\prime}$ is $k$-separated for every
$k\in\mathbb{N}$. Furthermore, Reducer chooses $\overline{T^{\prime}}$ to be
$|S^{\prime}|$-separated. In both cases we get (28), namely

(30)
$\displaystyle(S^{\prime},\overline{T^{\prime}})\textsc{-prof}(\omega^{2})\ =\
\left\\{\overline{\tau}\circ\pi\circ\sigma\,\middle|\,\pi\in(S,\overline{T})\textsc{-prof}(\mathcal{Q})\right\\}.$

Conditions (29) and (30) hold indeed, since $\tau$ is a monotonic bijection,
and due to the following two observations: Every monotonic partial bijection
$S\to\overline{T}$ extends to an embedding in $\text{\sc Emb}_{\mathcal{Q}}$.
Every monotonic partial bijection $S^{\prime}\to\overline{T^{\prime}}$ extends
to an embedding in $\text{\sc Emb}_{\omega^{2}}$. The former claim follows by
homogeneity of $\mathcal{Q}$. For the latter claim, we first extend the
mapping to $S^{\prime}$, which is possible as $\overline{T^{\prime}}$ is
$|S^{\prime}|$-separated, and then define an extension on remaining arguments
$\alpha\in\mathbb{N}^{2}\setminus S^{\prime}$ by $\alpha\mapsto\alpha+\beta$,
for a sufficiently large ordinal $\beta$. ∎

Corollary 7.2 below may be shown in the same way as Lemma 7, but it also
follows from the general fact that the product of domains preserves the winner
in the reduction game: If $\mathcal{A}_{1}\,{\ll}\,\mathcal{A}^{\prime}_{1}$
and $\mathcal{A}_{2}\ll\mathcal{A}^{\prime}_{2}$ then
$\mathcal{A}_{1}{\otimes}\mathcal{A}_{2}\ll\mathcal{A}^{\prime}_{1}{\otimes}\mathcal{A}^{\prime}_{2}$.

###### Proof.

Assuming Reducer’s strategies in games
$\mathcal{G}(\mathcal{A}_{1},\mathcal{A}^{\prime}_{1})$ and
$\mathcal{G}(\mathcal{A}_{2},\mathcal{A}^{\prime}_{2})$, we need to provide
his strategy in
$\mathcal{G}(\mathcal{A}_{1}\otimes\mathcal{A}_{2},\mathcal{A}^{\prime}_{1}\otimes\mathcal{A}^{\prime}_{2})$.
Suppose Spoiler plays in the first round a source and target

$S,T\in\text{\sc Age}(\mathcal{A}_{1}\otimes\mathcal{A}_{2}).$

Let $S_{1},T_{1}\in\text{\sc Age}(\mathcal{A}_{1})$ and
$S_{2},T_{2}\in\text{\sc Age}(\mathcal{A}_{2})$ be the projections. From
Reducer’s responses in $\mathcal{G}(\mathcal{A}_{1},\mathcal{A}^{\prime}_{1})$
and $\mathcal{G}(\mathcal{A}_{2},\mathcal{A}^{\prime}_{2})$, we get
$S^{\prime}_{1},T^{\prime}_{1}\in\text{\sc Age}(\mathcal{A}^{\prime}_{1})$,
$S^{\prime}_{2},T^{\prime}_{2}\in\text{\sc Age}(\mathcal{A}^{\prime}_{2})$ and
bijections

$\displaystyle\sigma_{1}:S^{\prime}_{1}\to S_{1}$
$\displaystyle\qquad\tau_{1}:T_{1}\to T^{\prime}_{1}$
$\displaystyle\sigma_{2}:S^{\prime}_{2}\to S_{2}$
$\displaystyle\qquad\tau_{2}:T_{2}\to T^{\prime}_{2}.$

The products of these bijections,

$\displaystyle(\sigma_{1},\sigma_{2}):S^{\prime}_{1}\times S^{\prime}_{2}\to
S_{1}\times S_{2}\qquad(\tau_{1},\tau_{2}):T_{1}\times T_{2}\to
T^{\prime}_{1}\times T^{\prime}_{2},$

are used in Reducer’s response $S^{\prime},T^{\prime}\in\text{\sc
Age}(\mathcal{A}^{\prime}_{1}\otimes\mathcal{A}^{\prime}_{2})$:

$S^{\prime}\ :=\ (\sigma_{1},\sigma_{2})^{-1}(S)\qquad T^{\prime}\ :=\
(\tau_{1},\tau_{2})(T).$

The restrictions of $(\sigma_{1},\sigma_{2})$ and $(\tau_{1},\tau_{2})$ to
$S^{\prime}$ and $T$, respectively,

$\sigma={(\sigma_{1},\sigma_{2})}{|S^{\prime}}\qquad\tau={(\tau_{1},\tau_{2})}{|T},$

satisfy (27). Indeed, condition (27) follows directly by Lemma 2, and by the
same condition for games
$\mathcal{G}(\mathcal{A}_{1},\mathcal{A}^{\prime}_{1})$ and
$\mathcal{G}(\mathcal{A}_{2},\mathcal{A}^{\prime}_{2})$.

Similarly we define Reducer’s strategy in the second round of
$\mathcal{G}(\mathcal{A}_{1}\otimes\mathcal{A}_{2},\mathcal{A}^{\prime}_{1}\otimes\mathcal{A}^{\prime}_{2})$.
∎

###### Corollary 7.2.

$\mathcal{Q}\otimes\langle d\rangle\ll\omega^{2}\otimes\langle d\rangle$.

###### Theorem 7.3.

Let $\mathbb{K}$ be a computable field and $\mathcal{A},\mathcal{A}^{\prime}$
two relational structures. If $\mathcal{A}\ll\mathcal{A}^{\prime}$ then Ideal-
memb in $\mathbb{K}[\mathcal{A}]$ reduces to Ideal-memb in
$\mathbb{K}[\mathcal{A}^{\prime}]$.

###### Proof.

Given an instance of Ideal-memb in $\mathbb{K}[\mathcal{A}]$, i.e., a
polynomial $f$ and a finite basis $\mathcal{B}$, we compute an instance
$f^{\prime}$, $\mathcal{B}^{\prime}$ of Ideal-memb in
$\mathbb{K}[\mathcal{A}^{\prime}]$ relying on Reducer’s strategy in the first
round of $\mathcal{G}(\mathcal{A},\mathcal{A}^{\prime})$. We let Spoiler play
$S:=\text{\sc vars}(\mathcal{B})$, the set of variables appearing in
$\mathcal{B}$, and $T:=\text{\sc vars}(f)$. From the Reducer’s answer we get
two subsets $S^{\prime},T^{\prime}\subseteq A^{\prime}$ and bijections
$\sigma:S^{\prime}\to S$ and $\tau:T\to T^{\prime}$. We use this bijections to
rename variables in $f$ and $\mathcal{B}$, thus obtaining $f^{\prime}$ and
$\mathcal{B}^{\prime}$.

Correctness of the reduction is shown using Reducer’s strategy in the second
round. In one direction, suppose $f$ belongs to the ideal generated by
$\mathcal{B}$ in $\mathbb{K}[\mathcal{A}]$, i.e.,

(31) $\displaystyle f\ =\ h_{1}\cdot\iota_{1}(g_{1})\ +\ \ldots\ +\
h_{m}\cdot\iota_{m}(g_{m}),$

for polynomials $g_{1},\ldots,g_{m}\in\mathcal{B}$, polynomials
$h_{1},\ldots,h_{m}\in\mathbb{K}[\mathcal{A}]$ and embeddings
$\iota_{1},\ldots,\iota_{m}\in E$. We let Spoiler play $\overline{T}$
containing all variables appearing on the right in equality (31). Hence
$T\subseteq\overline{T}$. From Reducer’s response we get
$\overline{T^{\prime}}$ and a bijection
$\overline{\tau}:\overline{T}\to\overline{T^{\prime}}$ that extends $\tau$. We
use $\sigma$ and $\overline{\tau}$ to rename all variables in polynomials
$h_{1},\ldots,h_{m}$ and $g_{1},\ldots,g_{m}$ appearing in the decomposition
(31), which results in polynomials
$h^{\prime}_{1},\ldots,h^{\prime}_{m}\in\mathbb{K}[\mathcal{A}^{\prime}]$ and
$g^{\prime}_{1},\ldots,g^{\prime}_{m}\in\mathcal{B}^{\prime}$. Furthermore,
for every $i\in\left\\{1\ldots m\right\\}$, we apply the equalities (27), (28)
to the restriction $\pi_{i}={\iota_{i}}{|S}$ to deduce that
$\overline{\tau}\circ\pi_{i}\circ\sigma$ extends to some embedding
$\iota^{\prime}_{i}\in E^{\prime}$. Therefore, we get:

(32) $\displaystyle f^{\prime}\ =\
h^{\prime}_{1}\cdot\iota^{\prime}_{1}(g^{\prime}_{1})\ +\ \ldots\ +\
h^{\prime}_{m}\cdot\iota^{\prime}_{m}(g^{\prime}_{m}).$

The reverse direction is shown similarly: assuming a decomposition (32), we
let Spoiler choose $\mathcal{A}^{\prime}$ in the second round, and use the
bijections $\sigma$ and $\tau$ obtained from Reducer’s response to get a
decomposition (31). ∎

Using Lemmas 2, 5, and 7, Theorems 7.1, 7.3, and Corollary 7.2 we get
reduction of Ideal-memb in $\mathbb{K}[\mathcal{Q}\otimes\langle d\rangle]$ to
Ideal-memb in $\mathbb{K}[\omega^{2}\otimes\langle d\rangle]$. We easily
generalize this reduction by invoking Lemma 7 several times. For conciseness,
we write ${\mathcal{A}}^{(\ell)}$ for the $\ell$-fold product:
${\mathcal{A}}^{(\ell)}\ :=\
\underbrace{\mathcal{A}\otimes\ldots\otimes\mathcal{A}}_{\ell}.$

###### Corollary 7.4.

For every $d,\ell\geq 1$, Ideal-memb in
$\mathbb{K}[{\mathcal{Q}}^{(\ell)}\otimes\langle d\rangle]$ reduces to Ideal-
memb in $\mathbb{K}[{(\omega^{2})}^{(\ell)}\otimes\langle d\rangle]$ and is
therefore decidable.

##  8\. Application: reversible Petri nets with data

In this section we show that Theorem 7.1 is useful for showing decidability of
the reachability problem for _reversible_ Petri nets whose tokens carry data
from a given domain (Theorem 8.3).

### Petri nets with data.

Among many presentations of Petri nets, we choose multiset rewriting, except
that in place of finite multisets over $\mathcal{A}$ we conveniently take
monomials $\text{\sc Mon}[\mathcal{A}]$.

Let $\mathcal{A}=(A,\ldots)$ be a fixed relational structure. Any set of
rewriting rules of the form

${\mathcal{T}}\subseteq\text{\sc Mon}[\mathcal{A}]\times\text{\sc
Mon}[\mathcal{A}]$

we call _monomial rewriting over $\mathcal{A}$_. Rewriting rules extend to
_transitions_ $\longrightarrow_{{\mathcal{T}}}\ \subseteq\text{\sc
Mon}[\mathcal{A}]\times\text{\sc Mon}[\mathcal{A}]$ as follows: for every
$g\in\text{\sc Mon}[\mathcal{A}]$ and $(h,h^{\prime})\in{\mathcal{T}}$, we
have a transition

$g\cdot h\longrightarrow_{{\mathcal{T}}}g\cdot h^{\prime}.$

The _reachability_ relation is the transitive closure
$\longrightarrow_{{\mathcal{T}}}^{*}$. In the sequel we always assume that
${\mathcal{T}}$ is orbit-finite, namely

${\mathcal{T}}\ =\ {\text{\sc Emb}_{\mathcal{A}}}(T)\
\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}\
\left\\{(\iota(h),\iota(h^{\prime}))\,\middle|\,\iota\in{\text{\sc
Emb}_{\mathcal{A}}},\ (h,h^{\prime})\in T\right\\}$

for some finite set $T\subseteq_{\text{fin}}\text{\sc
Mon}[\mathcal{A}]\times\text{\sc Mon}[\mathcal{A}]$. The set $T$ serves as a
_presentation_ of ${\mathcal{T}}$ when it is input to algorithms. A _Petri net
with data $\mathcal{A}$_ is just a monomial rewriting over
$\mathcal{A}\otimes\langle d\rangle$ for some $d\in\mathbb{N}$:

###### Definition 8.1.

A Petri net with data $\mathcal{A}$, with $d$ places, is an orbit-finite
monomial rewriting ${\mathcal{T}}$ over $\mathcal{A}\otimes\langle d\rangle$.

###### Example 8.2.

In particular, monomial rewriting over $\langle d\rangle$ defines a plain
(data-less) Petri net with $d$ places $\left\\{0\ldots d-1\right\\}$. The only
embedding is identity, and hence ${\mathcal{T}}$ is finite. Monomial rewriting
over $\mathcal{Q}\otimes\langle d\rangle$, where
$\mathcal{Q}=(Q,\leq_{\mathcal{Q}})$ is the rational order, defines a Petri
net with ordered data. According to Lemma 2, embeddings of
$\mathcal{Q}\otimes\langle d\rangle$ are induced by some embedding $\iota$ of
$\mathcal{Q}$ (i.e., a strictly increasing function $Q\to Q$), and preserve
the second component, i.e., preserve places (for conciseness, instead of
$(a,i)$ we write $ai$):

$ai\mapsto\iota(a)i.$

Classical graphical presentation of Petri nets is extendable to Petri nets
with data. For instance, consider a Petri net ${\mathcal{T}}=\text{\sc
Emb}_{\mathcal{Q}}(T)$ with $d=2$ places, and with 2 transition rules
$T=\left\\{t_{1},t_{2}\right\\}$, where

$t_{1}=(\mathbf{1},\ a0\cdot b0)\qquad t_{2}=(b0\cdot b1,\ a0\cdot c1)$

for some $a<b<c\in Q$ ($\mathbf{1}$ is the unit monomial). Petri net
${\mathcal{T}}$ is presented symbolically, using _variables_
$a,b,b^{\prime},c$ ranging over $Q$:

01$t_{1}$$a,b$$t_{2}$$b$$b^{\prime}$$a$$c$$a<b$$a<b=b^{\prime}<c$

Transition rule $t_{1}$ outputs two tokens with arbitrary but distinct
rational values onto place $0$. Transition $t_{2}$ inputs two tokens with the
same value, say $b$, one from $0$ and one from $1$, and outputs two tokens:
one token $a<b$ onto $0$ and the other $c>b$ onto $1$. $\triangleleft$

${\mathcal{T}}$ is _reversible_ if it is closed under inverse:
$c\longrightarrow_{{\mathcal{T}}}^{*}c^{\prime}$ implies
$c^{\prime}\longrightarrow_{{\mathcal{T}}}^{*}c$ for every
$c,c^{\prime}\in\text{\sc Mon}[\mathcal{A}]$. In such case we can assume,
w.l.o.g., that $T$ is closed under inverse: $(h,h^{\prime})\in
T\implies(h^{\prime},h)\in T$.

### Reachability problem.

The _reachability problem_ asks, given a Petri net ${\mathcal{T}}$ and two
monomials, source and target $s,t\in\text{\sc Mon}[\mathcal{A}\otimes\langle
d\rangle]$, whether $s\longrightarrow_{{\mathcal{T}}}^{*}t$.

###### Theorem 8.3.

For every $d\geq 1$, the reachability problem in reversible Petri nets with
$d$ places, with data $\mathcal{A}$, reduces to Ideal-memb in
$\mathbb{Q}[\mathcal{A}\otimes\langle d\rangle]$ (and also to Ideal-memb in
$\mathbb{Z}[\mathcal{A}\otimes\langle d\rangle]$).

###### Proof.

The fundamental idea of the proof comes from (MayrMeyer82). Let
${\mathcal{T}}=\text{\sc Emb}_{\mathcal{A}}(T)$ be a Petri net with data
$\mathcal{A}$, with $d$ places, where
$T=\left\\{(c_{1},c^{\prime}_{1}),\ldots,(c_{n},c^{\prime}_{n})\right\\}$. Let
$s,t\in\text{\sc Mon}[\mathcal{A}\otimes\langle d\rangle]$ be source and
target monomial. The reduction transformes $s,t$ and $T$ to the binomial
$(t-s)\in\mathbb{Z}[\mathcal{A}\otimes\langle d\rangle]$ and the finite set of
binomials
$\mathcal{B}=\left\\{(c^{\prime}_{1}-c_{1}),\ldots,(c^{\prime}_{n}-c_{n})\right\\}\subseteq\mathbb{Z}[\mathcal{A}\otimes\langle
d\rangle]$. Correctness follows due to equivalence of the following three
conditions:

  1. (1)

$c\longrightarrow_{{\mathcal{T}}}^{*}c^{\prime}$;

  2. (2)

$(c^{\prime}-c)$ belongs to the equivariant ideal generated by $\mathcal{B}$
in $\mathbb{Z}[\mathcal{A}\otimes\langle d\rangle]$;

  3. (3)

$(c^{\prime}-c)$ belongs to the equivariant ideal generated by $\mathcal{B}$
in $\mathbb{Q}[\mathcal{A}\otimes\langle d\rangle]$;

The implications $(1){\implies}(2)$ and $(3){\implies}(1)$ are shown by
reusing the proofs of Lemmas 1 and 2 in (MayrMeyer82). The remaining
implication $(2){\implies}(3)$ is trivial. ∎

Reduction of Theorem 8.3 is uniform in the number $d$ of places. So is also
the construction of Gröbner basis underlying the proof of Theorem 7.1, when
instantiated to domains of the form $\mathcal{A}\otimes\langle d\rangle$. We
thus deduce decidability of the reachability problem for reversible Petri nets
for a wide range of domains $\mathcal{A}$, including $\mathcal{Q}$, equality
data (a sub-case of $\mathcal{Q}$), and lexicographic products thereof (on the
basis of Corollary 7.4):

###### Theorem 8.4.

For every $\ell\geq 1$, the reachability problem is decidable in reversible
Petri nets with $\ell$-fold nested ordered data ${\mathcal{Q}}^{(\ell)}$.

###### Remark 8.5.

Without reversiblity restriction, the reachability problem for Petri nets with
ordered data is undecidable, while for Petri nets with equality data its
status is still unknown.

##  9\. Application: Orbit-finite systems of linear equations

We demonstrate that Theorem 7.1 is applicable to solving orbit-finite systems
of linear equations, thus providing a simple proof of a generalisation of the
main result of (GHL22). In the following, $\mathbb{K}$ is a field and
$\mathcal{A}=(A,\ldots)$ an $\omega$-well structured relational structure.

Solving a system of linear equations amount to checking if a given target
vector $b$ is a linear combination of a given set $M$ of vectors. We
generalise this setting to orbit-finite sets, by assuming that $b\in\text{\sc
Lin}(A^{d})$ and that $M$ is an equivariant orbit-finite family of vectors
$M\subseteq\text{\sc Lin}(A^{d})$. For convenience we assume that the family
$M$ is _indexed_ by a set $A^{n}$ for some $n\in\mathbb{N}$, namely

$M=(M_{t}\in\text{\sc Lin}(A^{d}))_{t\in A^{n}}$

(this is w.l.o.g. for equality and rational order domain (GHL22, Sect.6)).
Such a family $M$ is equivariant if for every $\iota\in{\text{\sc
Emb}_{\mathcal{A}}}$ and $t\in A^{n}$,

$\iota(M_{t})=M_{\iota(t)},$

i.e., $M_{\\_}$ commutes with the action of embeddings, as the function
$A^{n}\to\text{\sc Lin}(A^{d})$. Alternatively, $M$ is an infinite
$A^{d}\times A^{n}$ matrix over $\mathbb{K}$, whose every column $M_{t}$,
being a vector in $\text{\sc Lin}(A^{d})$, has finitely many non-zero entries.
A linear combination of $M$ is of the form

(33) $\displaystyle r_{1}\cdot M_{t_{1}}+\ldots+r_{k}\cdot M_{t_{k}},$

where $k\in\mathbb{N}$, $t_{1},\ldots,t_{k}\in A^{n}$, and
$r_{1},\ldots,r_{k}\in\mathbb{K}$. We investigate the following problem:

Lin-solv($\mathbb{K},\mathcal{A}$)::

Input: :

a vector $b\in\text{\sc Lin}(A^{d})$ and an equivariant family

$M=(M_{t}\in\text{\sc Lin}(A^{d}))_{t\in A^{n}}$ of vectors.

Question: :

Is $b$ a linear combination of $M$?

###### Example 9.1.

Let $\mathbb{K}=\mathbb{R}$, $\mathcal{A}=(A,=)$ the equality domain, $d=1$
and $n=2$, and consider an equivariant family of vectors
$M=(M_{(a,b)}\in\text{\sc Lin}(A))_{(a,b)\in A^{2}}$ defined as the following
formal sums:

$M_{(a,b)}=\begin{cases}a+2\cdot b&\text{ when }a\neq b\\\ 0&\text{ when }a=b\
.\end{cases}$

For every $a\in A$, the singleton formal sum $a\in\text{\sc Lin}(A)$ is a
linear combination of $M$:

$a\ =\ \frac{1}{2}\cdot M_{(a,b)}\ +\ \frac{1}{2}\cdot M_{(a,c)}\ -\
\frac{1}{3}\cdot M_{(b,c)}\ -\ \frac{1}{3}\cdot M_{(c,b)},$

for any distinct $b,c\in A$ different than $a$. $\triangleleft$

###### Theorem 9.2.

Lin-solv($\mathbb{K},\mathcal{A}$) reduces to Ideal-memb in
$\mathbb{K}[\mathcal{A}]$, for every computable field $\mathbb{K}$ and
relational structure $\mathcal{A}$.

Theorem 9.2 yields decidability of Lin-solv($\mathbb{K},\mathcal{A}$), thus
generalising (GHL22, Theorem 4.4) which only considers equality structure. On
the other hand, (GHL22) provides an upper complexity bound.

###### Proof of Theorem 9.2.

The reduction uses the same encoding $\text{\sc enc}(\\_):\text{\sc
Lin}(A^{d})\to\mathbb{K}[\mathcal{A}]$ as in Section 4. Consider an instance
of Lin-solv($\mathbb{K},\mathcal{A}$), namely $M=(M_{t})_{t\in A^{n}}$ and
$b$. Relying on Lemma 4.2 we assume that $A^{n}$ is represented by a finite
set $B\subseteq_{\text{fin}}A^{n}$ such that $A^{n}={\text{\sc
Emb}_{\mathcal{A}}}(B)\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\left\\{\iota(t)\,\middle|\,\iota\in{\text{\sc
Emb}_{\mathcal{A}}},t\in B\right\\}$.

We construct an instance of Ideal-memb in $\mathbb{K}[\mathcal{A}]$ by taking
the polynomial $f=\text{\sc enc}(b)\in\mathbb{K}[\mathcal{A}]$, and the
equivariant $\mathcal{I}$ ideal generated by the finite set

$\left\\{\text{\sc enc}(M_{t})\,\middle|\,t\in B\right\\}\ \subseteq\
\mathbb{K}[\mathcal{A}].$

As encoding commutes with the action of embeddings, $\mathcal{I}$ is generated
classically by the orbit-finite set $\left\\{\text{\sc
enc}(M_{t})\,\middle|\,t\in A^{n}\right\\}$. We need to prove: $b$ is a linear
combination of $M$ if and only if $f\in\mathcal{I}$. The ’only if’ direction
is immediate: $\text{\sc enc}(\\_)$, as a linear function, maps a linear
combination of vectors to a linear combination of their encoding polynomials.
For the converse implication, suppose $f=\text{\sc enc}(b)$ belongs to
$\mathcal{I}$, i.e.,

$\text{\sc enc}(b)\ =\ r_{1}\cdot h_{1}\cdot\iota_{1}(\text{\sc
enc}(M_{t_{1}}))+\ldots+r_{1}\cdot h_{k}\cdot\iota_{k}(\text{\sc
enc}(M_{t_{k}}))$

for some $r_{1},\ldots,r_{k}\in\mathbb{K}$, $h_{1},\ldots,h_{k}\in\text{\sc
Mon}[\mathcal{A}]$, $\iota_{1},\ldots,\iota_{k}\in{\text{\sc
Emb}_{\mathcal{A}}}$ and $t_{1},\ldots,t_{k}\in B$. As all monomials appearing
in polynomials $\text{\sc enc}(M_{t_{i}})$ and $\text{\sc enc}(b)$ have the
same degree, similarly as in the proof of Theorem 4.3 we can assume, w.l.o.g.,
that all monomials $h_{i}$ are unit monomials, i.e.,

$\text{\sc enc}(b)\ =\ r_{1}\cdot\iota_{1}(\text{\sc
enc}(M_{t_{1}}))+\ldots+r_{1}\cdot\iota_{k}(\text{\sc enc}(M_{t_{k}})).$

As encoding commutes with the action of embeddings and with scalar
multiplication, we get

$\text{\sc enc}(b)\ =\ \text{\sc
enc}(r_{1}\cdot\iota_{1}(M_{t_{1}}))+\ldots+\text{\sc
enc}(r_{1}\cdot\iota_{k}(M_{t_{k}})),$

and by injectivity of encoding and equivariance of $M$ we obtain

$b\ =\ r_{1}\cdot M_{\iota_{1}(t_{1})}+\ldots+r_{1}\cdot
M_{\iota_{k}(t_{k})},$

i.e. $b$ is a linear combination of $M$, as required. ∎

###### Acknowledgements.

We thank Lorenzo Clemente for posing the questions about equivariant
Noetherianity for equality domain.

## References

  * (1)
  * Aschenbrenner and Hillar (2007) Matthias Aschenbrenner and Christopher Hillar. 2007.  Finite generation of symmetric ideals.  _Trans. Amer. Math. Soc._ 359.11 (2007), 5171–5192.
  * Aschenbrenner and Hillar (2008) Matthias Aschenbrenner and Christopher J. Hillar. 2008.  An algorithm for finding symmetric Grobner bases in infinite dimensional rings. In _Proc. ISSAC_. ACM, 117–124.
  * Benedikt et al. (2017) Michael Benedikt, Timothy Duff, Aditya Sharad, and James Worrell. 2017.  Polynomial automata: Zeroness and applications. In _Proc. LICS 2017_. IEEE Computer Society, 1–12.
  * Bojańczyk ([n.d.]) Mikołaj Bojańczyk. [n.d.].  Slightly Infinite Sets. ([n. d.]).  https://www.mimuw.edu.pl/~bojan/paper/atom-book A draft of a book available at https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  * Bojanczyk et al. (2014) Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. 2014\.  Automata theory in nominal sets.  _Log. Methods Comput. Sci._ 10, 3 (2014).
  * Bojańczyk et al. (2021) Mikołaj Bojańczyk, Bartek Klin, and Joshua Moerman. 2021\.  Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata. In _Proc. LICS_. IEEE, 1–13.
  * Brouwer and Draisma (2011) Andries E. Brouwer and Jan Draisma. 2011.  Equivariant Gröbner Bases and The Gaussian Two-factor Model.  _Math. Comp._ 80, 274 (2011), 1123–1133.
  * Buchberger and Winkler (1998) B. Buchberger and F. Winkler (Eds.). 1998.  _Gröbner Bases and Applications_. Cambridge University.
  * Cameron (1990) Peter J. Cameron. 1990\.  _Oligomorphic Permutation Groups_.  Cambridge University Press.
  * Cohen (1967) Daniel E. Cohen. 1967\.  On the Laws of a Metabelian Variety.  _Journal of Algebra_ 5 (1967), 267–273.
  * Cohen (1987) Daniel E. Cohen. 1987\.  Closure Relations, Buchberger’s Algorithm, and Polynomials in Infinitely Many Variables. In _Computation Theory and Logic_ _(Lecture Notes in Computer Science, Vol. 270)_. Springer, 78–87.
  * Cox et al. (2015) David A. Cox, John Little, and Donal O’Shea. 2015\.  _Ideals, Varieties, and Algorithm_.  Springer.
  * Diestel (2017) Reinhard Diestel. 2017\.  _Graph Theory_.
  * Emmott (1987) Phillip Emmott. 1987\.  _Some decision problems in group theory and ring theory_.  Ph.D. Dissertation. Queen Mary College, University of London.
  * Ghosh et al. (2022) Arka Ghosh, Piotr Hofman, and Slawomir Lasota. 2022.  Solvability of orbit-finite systems of linear equations. In _Proc. LICS’22_. ACM, 11:1–11:13.
  * Higman (1952) G. Higman. 1952\.  Ordering by divisibility in abstract algebras.  _Proc. London Math. Soc._ 3 (1952), 326–336.  Issue 2.
  * Hillar et al. (2018) Christopher J. Hillar, Robert Krone, and Anton Leykin. 2018\.  Equivariant Gröbner bases.  _Advanced Studies in Pure Mathematics_ 77 (2018), 129–154.