# Orbit-Finite-Dimensional Vector Spaces
and Weighted Register Automata

Mikołaj Bojańczyk  University of Warsaw
Email<EMAIL_ADDRESS>Bartek Klin  University of Warsaw
Email<EMAIL_ADDRESS>Joshua Moerman  RWTH Aachen
Email<EMAIL_ADDRESS>
###### Abstract

We develop a theory of vector spaces spanned by orbit-finite sets. Using this
theory, we give a decision procedure for equivalence of weighted register
automata, which are the common generalization of weighted automata and
register automata for infinite alphabets. The algorithm runs in exponential
time, and in polynomial time for a fixed number of registers. As a special
case, we can decide, with the same complexity, language equivalence for
unambiguous register automata, which improves previous results in three ways:
(a) we allow for order comparisons on atoms, and not just equality; (b) the
complexity is exponentially better; and (c) we allow automata with guessing.

##  I Introduction

Weighted automata over a field were introduced in [17] by Schützenberger. Such
an automaton is defined in the same way as a nondeterministic automaton, with
a set $Q$ of states and an input alphabet $\Sigma$, except that instead of
having subsets for transitions, initial and final states, the automaton has
weight functions into the underlying field:

$\displaystyle\underbrace{I\colon Q\to\mathbb{F}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
initial}\crcr}}}}}}\quad\underbrace{\delta\colon Q\times\Sigma\times
Q\to\mathbb{F}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.33751pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
transition}\crcr}}}}}}\quad\underbrace{F\colon
Q\to\mathbb{F}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
final}\crcr}}}}}}.}}}$

The weight of a run is obtained by multiplying the weights along all
transitions, the initial weight of the first state, and the final weight of
the last state. The automaton recognizes a weighted language, which is the
function $L\colon\Sigma^{*}\to\mathbb{F}$ that maps a word to the sum of
weights of all runs on that word.

Schützenberger proved that weighted automata can be minimized [17, Sec. B],
which provides a polynomial time algorithm for equivalence. In contrast, it is
undecidable whether some field element $a\in\mathbb{F}$ is achieved as the
weight of some word, already in the special case of weighted automata that are
probabilistic [15, Thm. 22]. Equivalence is undecidable for weighted automata
over semirings that are not fields, e.g. for the min-plus semiring [12, Cor.
4.3].

One application of weighted automata (see [1] for other ones) is a polynomial
time algorithm for language equivalence of unambiguous automata, i.e.
nondeterministic finite automata that have at most one accepting run for every
word. The algorithm is a simple reduction to equivalence of weighted automata:
a nondeterministic automaton can be viewed as a weighted automaton over the
field of rational numbers, such that the weight of a word is the number of
accepting runs. For unambiguous automata, the number of accepting runs is
either zero or one, and hence two unambiguous automata accept the same words
if and only if the corresponding weighted automata are equivalent.

In this paper, we generalize weighted automata to infinite alphabets,
motivated by the study of register automata, in particular the equivalence
problem for unambiguous register automata [7, 8, 13]. The kinds of infinite
alphabets that we study are constructed using an infinite set $\mathbb{A}$ of
atoms (also called data values) which can only be accessed in very limited
ways; in the simplest case, they can only be compared for equality. Register
automata are like finite automata, except that they additionally use finitely
many registers to store atoms that occurred in the word. This model was
introduced by Kaminski and Francez [10, Def. 1], under the name of _finite
memory automata_. This model has attracted much attention, and is now one of
the most widely studied infinite state systems. The decidability landscape for
register automata is rather complex: for example, emptiness is decidable for
nondeterministic register automata [10, Thm. 1], but universality is not [16,
Thm 5.1]. More robust results can be achieved for deterministic register
automata, but at a considerable loss of expressive power.

One of the numerous (unfortunately non-equivalent) variants of register
automata are unambiguous register automata, for which language equivalence was
shown in [13, Thm. 1] to be decidable in 2ExpSpace, and in ExpSpace for a
fixed number of registers. These upper bounds were improved to 2ExpTime and
ExpTime, respectively, in [7, Thm. 2]. None of these proofs use weighted
automata.

From the point of view of register automata, the main contributions of this
paper are:

  1. 1.

We introduce a weighted version of register automata, and we prove that their
equivalence problem can be solved in ExpTime, and in polynomial time for a
fixed number of registers.

  2. 2.

We show that our weighted automata have a robust theory, in particular they
can be described in several different ways and admit canonical syntactic
automata.

  3. 3.

As an immediate application of our equivalence algorithm for weighted
automata, we show that the language equivalence problem for unambiguous
register automata can be solved in the same complexity, improving
exponentially on prior work [7, 13].

  4. 4.

In [7, 13], the equivalence algorithms work only for automata which are non-
guessing, in the sense that every pair (state, input letter) has finitely many
outgoing transitions. Without the non-guessing assumption, decidability is
only known in the case where one of the automata has just a single register
[13, Thm. 10]. Our algorithm can be adapted so that it works for general
unambiguous automata, without the non-guessing assumption, with the same
complexity.

  5. 5.

Apart from atoms with equality only, our algorithm for weighted automata, and
its applications to unambiguous automata, also work for atoms equipped with a
total order. Previous algorithms for ordered atoms assume that one of the
automata has a single register [13, Thm. 2].

In our opinion, perhaps the most interesting aspect of this paper is not the
applications described above, but the theory that is developed in order to
obtain them. Our central objects of study are vector spaces which are spanned
by orbit-finite set of vectors. A typical example is the vector space
$\operatorname{\mathsf{Lin}}(\mathbb{A}^{k})$, which consists of finite linear
combinations of $k$-tuples of atoms. Such a vector space has two kinds of
structure: we can take linear combinations of vectors, and we can apply atom
automorphisms to them. A natural concept – which appears in our equivalence
algorithm for weighted automata – is the _equivariant subspaces_ , i.e.
subsets of the vector space closed under both linear combinations and atom
automorphisms. Our principal technical result is that for every $k$, there is
a finite (exponential in $k$) bound on the maximal length of chains

$\displaystyle\underbrace{V_{1}\subsetneq V_{2}\subsetneq\cdots\subsetneq
V_{n}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-3.1111pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
equivariant
subspaces}\crcr}}}}}}\subseteq\operatorname{\mathsf{Lin}}(\mathbb{A}^{k}).}$

This bound is used in the equivalence algorithm for weighted automata, but it
also has many consequences for vector spaces spanned by orbit-finite sets,
e.g. their closure under Cartesian products, tensor products and dual spaces.
We hope that these results can be used in future work, beyond applications to
unambiguous automata.

##  II Orbit-finite sets

Our paper is based on the approach to register automata that uses _sets with
atoms_. The idea is to consider automata where all components are closed under
atom automorphisms, and the states and input alphabets have finitely many
elements up to atom automorphisms. This more abstract view avoids cumbersome
notation for representing states and transitions of register automata. We can
also leverage existing results that treat atoms with more structure than
equality only, e.g. order.

Our notation is based on [3]. Fix a countably infinite relational structure
$\mathbb{A}$, in the sense of model theory, i.e. an underlying set equipped
with some relations. Elements of this fixed structure will be called _atoms_.
In this paper we mostly focus on two such structures:

  * •

the equality atoms $\mathbb{A}=({\mathbb{N}},=)$, and

  * •

the ordered atoms $\mathbb{A}=({\mathbb{Q}},<)$.

The main results of this paper, notably the finite length property in Section
IV, are proved for these atoms only, and we leave other atoms as future work.

An _atom automorphism_ is any bijection of the underlying set of atoms which
is consistent with all relations in $\mathbb{A}$. For the equality atoms this
is any permutation of ${\mathbb{N}}$; for the ordered atoms, any order-
preserving bijection on ${\mathbb{Q}}$. In both settings, the set of all atoms
is orbit-finite, which means that it has finitely many elements up to atom
automorphisms. More complicated sets constructed with atoms are also orbit-
finite, such as:

$\displaystyle\underbrace{\mathbb{A}^{k}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-3.1111pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize$k$-tuples
of
atoms}\crcr}}}}}}\qquad\qquad\underbrace{\mathbb{A}^{(k)}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-6.12915pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
non-repeating }\\\\\hbox{{\ignorespaces\scriptsize$k$-tuples of
atoms}\crcr}}}}}}\qquad\qquad\underbrace{\textstyle{\mathbb{A}\choose
k}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
sets of $k$ atoms}\crcr}}}}}}.}}}}$ (5)

To formally define “sets constructed with atoms” and the orbit-finite
restriction, we use the cumulative hierarchy from set theory. The _cumulative
hierarchy (over atoms $\mathbb{A}$)_ is indexed by ordinal numbers, and
defined as follows: on level 0 we find the atoms, and on level indexed by an
ordinal $\alpha>0$ we find the atoms and every set which has all elements
taken from levels $<\alpha$. For example, on level 1 we find every subset of
the atoms. Automorphisms $\pi:\mathbb{A}\to\mathbb{A}$ of the atoms act on
sets in the cumulative hierarchy in the expected way.

In the cumulative hierarchy one can encode data structures such as tuples,
words, relations, functions etc., using standard set-theoretic machinery.
Automorphisms $\pi$ then act on tuples as expected:
$\pi((x_{1},\ldots,x_{n}))=(\pi(x_{1}),\ldots,\pi(x_{n}))$.

For a tuple of atoms $\bar{a}\in\mathbb{A}^{*}$, an $\bar{a}$-automorphism is
an atom automorphism $\pi$ such that $\pi(\bar{a})=\bar{a}$. A tuple $\bar{a}$
is said to _support_ an element $x$ of the cumulative hierarchy if $\pi(x)=x$
for every $\bar{a}$-automorpism $\pi$. We say that an element $x$ of the
cumulative hierarchy is _finitely supported_ if it is supported by some tuple
of atoms in $\mathbb{A}^{*}$. An element is called equivariant if it is
supported by the empty tuple. An equivariant set may contain non-equivariant
elements; e.g., the set of all atoms is equivariant, but its elements are not.
A _set with atoms_ is defined to be a set in the cumulative hierarchy which is
finitely supported and with each of its members (and their members, and so on)
finitely supported.

Sets with atoms provide a relaxed notion of finiteness, called orbit-
finiteness. We say that two sets with atoms $x$ and $y$ are in the same
$\bar{a}$-orbit if there is some $\bar{a}$-automorphism $\pi$ such that
$y=\pi(x)$. Being in the same $\bar{a}$-orbit is clearly an equivalence
relation; its equivalence classes are called $\bar{a}$-orbits. A set with
atoms $x$ is called _orbit-finite_ if there is some atom tuple $\bar{a}$ such
that $x$ is a finite union of $\bar{a}$-orbits.

Example 1.

  * •

Over equality atoms, the set $\mathbb{A}$ of atoms is orbit-finite, also for
every $k\in\\{1,2,\ldots\\}$ the sets $\mathbb{A}^{(k)}$ and
$\mathbb{A}\choose k$ from (5) are orbit-finite, with a single equivariant
orbit each. The set $\mathbb{A}^{k}$ is also orbit-finite, with the number of
equivariant orbits equal to the $k$-th Bell number.

  * •

Over ordered atoms, the sets $\mathbb{A}$ and $\mathbb{A}\choose k$ have
single equivariant orbit each. The set $\mathbb{A}^{(k)}$ is also orbit-
finite, with $k!$ equivariant orbits; one of these orbits is the increasing
$k$-tuples of atoms. Each of these orbits is in an equivariant bijection with
$\mathbb{A}\choose k$.

  * •

Over the ordered atoms, for every atom $a\in\mathbb{A}$ the set
$\mathbb{A}-\\{a\\}$ has two $a$-orbits: the open intervals $(-\infty;a)$ and
$(a;\infty)$.

  * •

The set $\mathbb{A}^{*}$ is not orbit-finite, neither for equality nor for
ordered atoms, as words of different length are necessarily in distinct
orbits. $\Box$

An atom structure $\mathbb{A}$ is called _oligomorphic_ if for every $k$, the
set $\mathbb{A}^{k}$ is orbit-finite. For oligomorphic atoms, orbit-finite
sets behave well, e.g. they are closed under products and finitely supported
subsets [3, Lem. 3.24]. In this paper we only consider oligomorphic atoms.

Orbit-finite sets can be represented in a finite way so that they can be used
as inputs for algorithms. Two examples of such representations are set builder
expressions [3, Sec. 4.1] or the $G$-set representation [4, Sec. 8]. The
reader does not need to know these representations in detail; the important
thing is that they support basic operations such as products, Boolean
operations, or inclusion and membership checks.

##  III Weighted orbit-finite automata

We now introduce the main model for this paper, an orbit-finite generalization
of weighted automata.

######  Definition III.1 (Weighted orbit-finite automaton)

Fix an oligomorphic atom structure $\mathbb{A}$ and a field $\mathbb{F}$. A
_weighted orbit-finite automaton_ consists of orbit-finite sets $Q$ and
$\Sigma$, called the _states and alphabet_ , and finitely supported functions

$\displaystyle\underbrace{I:Q\to\mathbb{F}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
initial}\crcr}}}}}}\quad\underbrace{\delta:Q\times\Sigma\times
Q\to\mathbb{F}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.33751pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
transitions}\crcr}}}}}}\quad\underbrace{F:Q\to\mathbb{F}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
final}\crcr}}}}}}.}}}$

Furthermore, we require the _non-guessing condition:_

  * (*)

there are finitely many states with nonzero initial weight, and also for every
state $q$ and input letter $a$, there are finitely many states $p$ such that
the transition $(q,a,p)$ has nonzero weight.

Weights of runs and words is defined in the same way as for the classical
model of weighted automata with finitely many states. The non-guessing
condition ensures that each word has finitely many runs; otherwise there could
be difficulties in summing up the weights of infinitely many runs.

Example 2.  Consider any oligomorphic atoms $\mathbb{A}$ and the field of
rational numbers. We define a weighted orbit-finite automaton which maps a
word $w\in\mathbb{A}^{*}$ to the number of distinct atoms that appear in $w$.
The states are

$\displaystyle\underbrace{\\{\bot\\}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-6.2222pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
initial weight 1}\\\\\hbox{{\ignorespaces\scriptsize final weight
0}\crcr}}}}}}\qquad+\qquad\underbrace{\mathbb{A}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-6.2222pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
initial weight 0}\\\\\hbox{{\ignorespaces\scriptsize final weight
1}\crcr}}}}}}}}}}$

for some $\bot\not\in\mathbb{A}$. The transition weight is $1$ for all triples

$\displaystyle(\bot,a,\bot)\ (\bot,a,a)\ (a,b,a)\qquad\text{for }a\neq
b\in\mathbb{A},$

and $0$ for all other triples. For every input word, all runs have weight $0$,
except for the following runs, which have weight $1$: start in $\bot$, stay
there until the last occurrence of some atom $a$, and then stay in state $a$
until the end of the word. Since the number of runs with weight $1$ is the
number of distinct atoms $a$ that appear in the word, the output of the
automaton is the number of distinct atoms.

This automaton is equivariant, in the sense that its state space and all three
weight functions are equivariant. $\Box$

Example 3.  The automaton in the previous example is a special case of a more
general construction: counting accepting runs of a nondeterministic automaton.
Define a _nondeterministic orbit-finite automaton_ like a nondeterministic
finite automaton, except that all components (alphabet, states, transitions,
initial and finite sets) are required to be orbit-finite sets, see [3, Def.
5.7]. To such an automaton one can associate a weighted orbit-finite automaton
(over the field of rational numbers) as follows: the alphabet and states are
the same, and the remaining components are defined by replacing “yes” with
weight 1 and “no” with weight 0. This weighted automaton maps a word to the
number of accepting runs of the nondeterministic automaton. The construction
makes sense only if the original nondeterministic automaton is non-guessing in
the sense that there are finitely many inputs states, and for every pair
(state, letter) there are finitely many outgoing transitions. $\Box$

As mentioned in Section II, orbit-finite sets can be represented in a finite
way. Therefore, weighted orbit-finite automata can also be represented in a
finite way (assuming that field elements can be represented in a finite way).
This is because (a) a finitely supported relation on an orbit-finite set is
also orbit-finite; and (b) a finitely supported function from an orbit-finite
set to any set is itself an orbit-finite set.

Example 4.  A special case of weighted orbit-finite automata, where the finite
representation is easier to see, is a weighted $k$-register automaton. This is
a weighted orbit-finite automaton where the input alphabet is finitely many
disjoint copies of the atoms, the states are finitely many copies of
$(\mathbb{A}+\\{\bot\\})^{k}$, and all weight functions are equivariant. For
equality and ordered atoms, the weight functions can be finitely represented
using quantifier-free formulas, see [3, p. 6]. $\Box$

We now state the main result of this paper, which is an algorithm for
equivalence problem of weighted orbit-finite automata, assuming that the atom
structure is either the equality atoms or the ordered atoms. We do not know if
the problem is decidable for other atom structures.

###### Theorem III.2

Assume that the atoms are the equality atoms $({\mathbb{N}},=)$ or the ordered
atoms $({\mathbb{Q}},<)$. The equivalence problem for equivariant111This
theorem would also work for finitely supported automata, but the notation for
the complexity and orbit counts would be more involved. weighted orbit-finite
automata can be solved in deterministic time

$\displaystyle 2^{\mathrm{poly}(k)}\cdot n^{O(k)}$

where

  * $n$

is the orbit count, i.e. the number of equivariant orbits in the disjoint
union of the two state sets;

  * $k$

is the atom dimension of the state spaces of the automata, i.e. the smallest
$k$ such that every state in both automata is supported by at most $k$ atoms.

In particular, the equivalence problem is in ExpTime, and polynomial time when
the atom dimension $k$ is fixed.

A lower bound for the problem is PSpace, which is the complexity of language
equivalence of deterministic register automata. We do not know the exact
complexity; it is worth pointing out that for weighted finite automata there
is an equivalence algorithm in randomized polylogarithmic parallel time [11,
Sec. 3.2] that uses the Isolating Lemma.

We now present a proof strategy for the theorem, which will be carried out in
the next sections. The first observation is that the equivalence problem
reduces to the zeroness problem, which asks whether a single weighted orbit-
finite automaton outputs zero for every word. The reduction is as follows:
given two equivariant weighted orbit-finite automata ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$, we create a new weighted orbit-finite automaton
${\mathcal{A}}_{1}-{\mathcal{A}}_{2}$, which is obtained by taking the
disjoint union of ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$, and flipping
the sign of the final weights in ${\mathcal{A}}_{2}$. The new automaton maps
all words to zero if and only if the original two automata were equivalent.
Also, in the reduction, the atom dimension does not change, neither does the
orbit count.

It remains to give an algorithm for zeroness of a single equivariant weighted
orbit-finite automaton, with states $Q$. Our proof follows the same lines as
Schützenberger’s algorithm. Write $\operatorname{\mathsf{Lin}}Q$ for the set
of finite linear combinations (over the field $\mathbb{F}$) of states, seen as
a vector space with basis $Q$. For an input word $w$, define its
_configuration_ to be the vector in $\operatorname{\mathsf{Lin}}Q$ which maps
a state $q$ to the sum of pre-weights of all runs over $w$ that end in state
$q$; the pre-weight of a run is defined by multiplying the initial weight of
the first state and the weights of all transitions, without taking into
account the final weights. Thanks to condition (*) in Definition III.1, each
configuration is indeed a finite linear combination, since there are finitely
many runs with nonzero pre-weight. Consider the chain

$\displaystyle V_{0}\subseteq V_{1}\subseteq
V_{2}\subseteq\cdots\subseteq\operatorname{\mathsf{Lin}}Q$

where $V_{i}$ is the subspace of $\operatorname{\mathsf{Lin}}Q$ that is
spanned by the configurations of words of length at most $i$. (We do not
intend to compute the subspaces in this chain, whatever that would mean; the
chain is only used in the analysis of the algorithm.) Because the automaton is
equivariant, one can easily see that each subspace $V_{n}$ is also
equivariant.

In the finite-dimensional case studied by Schützenberger, where $Q$ was a
finite set, we could conclude that the chain must stabilize in a number of
steps that is bounded by the finite dimension of the vector space
$\operatorname{\mathsf{Lin}}Q$. In the orbit-finite case, the vector space has
infinite dimension, and thus it is not clear why the chain should stabilize in
finitely many steps. Our main technical contribution is a proof that the chain
does indeed stabilize, and furthermore the time to stabilize is consistent
with the bounds in the statement of Theorem III.2. This stabilization property
is the subject of the next section, and in the section after that we use the
property to conclude the proof of Theorem III.2.

##  IV Finite length property

A standard result in linear algebra says that a vector space has finite
dimension if and only if it has finite length, where the length is defined to
be the longest chain of its subspaces. Because of this easy correspondence the
notion of length is seldom explicitly applied to vector spaces, and it becomes
more important only in more general structures such as modules over a ring.
However, the situation becomes more interesting for chains of equivariant
subspaces. We define:

######  Definition IV.1 (Length)

The length of an equivariant vector space $V$, denoted
$\operatorname{\mathsf{length}}(V)$, is the maximal length $n$ of a chain of
proper inclusions on equivariant subspaces of $V$:

$\displaystyle V_{1}\subsetneq V_{2}\subsetneq\cdots\subsetneq V_{n}\subsetneq
V.$

If a maximal length does not exist, we say that $V$ has infinite length. An
atom structure $\mathbb{A}$ has the _finite length property_ if for every
number $k$, the vector space $\operatorname{\mathsf{Lin}}\mathbb{A}^{k}$ has
finite length.

The finite length property easily implies oligomorphicity, but we do not know
if the converse implication holds. The purpose of this section is to prove
that both the equality atoms $({\mathbb{N}},=)$ and the ordered atoms
$({\mathbb{Q}},<)$ have the finite length property (Lemmas IV.9 and IV.8).
Furthermore, the length of $\operatorname{\mathsf{Lin}}\mathbb{A}^{k}$ grows
exponentially (and not worse) with $k$. The results of this section apply to
an arbitrary field $\mathbb{F}$.

Definition IV.1 speaks of equivariant subspaces. At the end of this section,
we show that for the equality and ordered atoms, allowing a fixed support
would make no difference.

Example 5.  Consider the equality atoms. The vector space
$\operatorname{\mathsf{Lin}}\mathbb{A}$ has length 2, because it has exactly 3
equivariant subspaces which form a chain of two proper inclusions:

$\displaystyle\\{0\\}\quad\subsetneq\quad\underbrace{\operatorname{\mathsf{Span}}\\{a-b:a\neq
b\in\mathbb{A}\\}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
call this
$V$}\crcr}}}}}}\quad\subsetneq\quad\operatorname{\mathsf{Lin}}\mathbb{A}.}$

Equivalently, $V$ is the vector space of all vectors where all coefficients
sum up to $0$. Let us prove that there are no other equivariant subspaces.
Suppose that $W$ is an equivariant subspace which contains some nonzero vector

$\displaystyle w=\lambda_{1}a_{1}+\cdots+\lambda_{n}a_{n}\quad\text{where
$\lambda_{i}\in\mathbb{F}\setminus\\{0\\}$.}$ (6)

Since $W$ is equivariant, it also contains the vector obtained from $w$ by
replacing $a_{n}$ with some fresh atom $b_{n}$. By taking the difference of
these vectors and dividing by $\lambda_{n}$, we see that $W$ contains
$a_{n}-b_{n}$. By equivariance, $W$ contains all vectors of the form $a-b$ for
distinct atoms $a,b$, and thus $V\subseteq W$.

We now show that $W$ is either $V$ or the entire space
$\operatorname{\mathsf{Lin}}\mathbb{A}$. Indeed, suppose that $W$ contains
some $w$ as in (6) that is not in $V$. If $n>1$ then we can subtract from $w$
the vector $\lambda_{1}\cdot(a_{1}-a_{2})\in V$, which results in another
vector that is in $W$ but not in $V$, with a smaller $n$. By repeating this
process, we see that $W$ contains a vector of the form $\lambda_{1}a_{1}$ with
$\lambda_{1}\neq 0$, and hence, by equivariance, it is the entire space.
$\Box$

Definition IV.1 differs from the classical definition of length in that we
only consider equivariant subspaces. Some classical properties of length
easily transfer to our case. One may even say that our definition is a special
case of the classical one: an equivariant vector space can be seen as a module
over the (non-commutative) group ring $\mathbb{F}[G]$, where $\mathbb{F}$ is
the underlying field and $G$ is the automorphism group of $\mathbb{A}$. To
keep the presentation elementary we do not pursue this correspondence, but we
remark that all properties of length which are valid for modules over (non-
commutative) rings, remain true for our definition. For example, the following
lemma has the same proof (see Appendix A) as for the classical notion of
length of a module, (see e.g. [9, Prop. 4.12]), and works for arbitrary
oligomorphic atoms:

###### Lemma IV.2

For any equivariant spaces $V\subseteq W$, and equivariant sets $P$, $Q$ with
their disjoint union $P+Q$:

  * (i)

$\operatorname{\mathsf{length}}(W)=\operatorname{\mathsf{length}}(V)+\operatorname{\mathsf{length}}(W/V)$;

  * (ii)

$\operatorname{\mathsf{length}}(\operatorname{\mathsf{Lin}}(P+Q))=\operatorname{\mathsf{length}}(\operatorname{\mathsf{Lin}}P)+\operatorname{\mathsf{length}}(\operatorname{\mathsf{Lin}}Q)$;

  * (iii)

if there is an equivariant surjective function from $P$ to $Q$ then
$\operatorname{\mathsf{length}}(\operatorname{\mathsf{Lin}}Q)\leq\operatorname{\mathsf{length}}(\operatorname{\mathsf{Lin}}P)$.

From this we infer that in Definition IV.1, we could have equivalently talked
about arbitrary equivariant orbit-finite set, instead of just sets of the form
$\mathbb{A}^{k}$:

###### Corollary IV.3

For atoms with the finite length property, $\operatorname{\mathsf{Lin}}Q$ has
finite length for every equivariant orbit-finite $Q$.

###### Proof.

An orbit-finite set is a finite disjoint union of single-orbit sets, and for
oligomorphic atoms every single-orbit set $Q$ is an image of a surjective
function from $\mathbb{A}^{k}$ [5], for $k$ the atom dimension of $Q$. Hence,
we can use the closure properties from Lemma IV.2. ∎

The following lemma is the key step in proving the finite length property for
the equality and ordered atoms:

###### Lemma IV.4

Consider the ordered atoms $\mathbb{A}=({\mathbb{Q}},<)$. For every $k$, the
length of $\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$ is finite, and
satisfies

$\textstyle\operatorname{\mathsf{length}}\big{(}\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k}\big{)}\quad\leq\quad
1+k\cdot\operatorname{\mathsf{length}}\big{(}\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k-1}\big{)}.$

###### Proof.

For any set $\alpha$ of $2k$ atoms:

$\displaystyle\underbrace{a_{1}<b_{1}<\cdots<a_{k}<b_{k}}_{\alpha}$ (7)

and for any $I\subseteq k=\\{1,\ldots,k\\}$, define $\alpha\rtimes
I\in{\mathbb{A}\choose k}$ by:

$\alpha\rtimes I=\\{a_{i}\mid i\not\in I\\}\cup\\{b_{i}\mid i\in I\\}.$

In words, $\alpha\rtimes I$ picks either $a_{i}$ or $b_{i}$ from $\alpha$
according to $I$. Define the cog (on $\alpha$),
$\nu^{\alpha}\in\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$, to be the
vector:

$\nu^{\alpha}=\sum_{I\subseteq k}(-1)^{|I|}(\alpha\rtimes I).$

Notice that all cogs form a single orbit in
$\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$.

###### Claim IV.5

Every nontrivial equivariant subspace
$V\subseteq\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$ contains a cog.

###### Proof.

Pick any nonzero $v\in V$ and pick
$\alpha=\\{a_{1},\ldots,a_{k}\\}\in{\mathbb{A}\choose k}$ so that
$v(\alpha)\neq 0$. Choose fresh atoms $b_{1},\ldots,b_{k}$ to form a set as in
(7). For every $i=1,\ldots,k$, choose an atom automorphism $\pi_{i}$ such
that:

  * •

$\pi_{i}(a_{i})=b_{i}$, and

  * •

$\pi_{i}(a_{j})=a_{j}$ and $\pi_{i}(b_{j})=b_{j}$ for $j\neq i$.

Then put $v_{0}=v$ and define $v_{1},\ldots,v_{k}\in V$ by induction:

$v_{i}=v_{i-1}-\pi_{i}(v_{i-1})$

($\pi(v_{i-1})\in V$ since $V$ is equivariant). It is easy to prove by
induction that $v_{i}(\alpha)=v(\alpha)$ for all $i$, and so in particular all
$v_{i}$ are nonzero. Also by straightforward induction, each $v_{i}$ has the
following properties:

  * •

$v_{i}(\beta)$ is nonzero only if for each $1\leq j\leq i$, $\beta$ contains
either $a_{j}$ or $b_{j}$ but not both,

  * •

if $\beta^{\prime}$ arises from such $\beta$ by replacing $a_{j}$ with $b_{j}$
(or vice versa) for exactly one $j\leq i$, while keeping the other components
unchanged, then $v_{i}(\beta)+v_{i}(\beta^{\prime})=0$.

For $i=k$ this implies that $v_{k}$, divided by the scalar $v(\alpha)$, is a
cog. ∎

Claim IV.5 implies that $\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$ has
a unique least nontrivial equivariant subspace: the one spanned by all cogs.
We shall now give an explicit description of that subspace.

A vector $v\in\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$ is called
balanced if for every set $S\in{\mathbb{A}\choose{k-1}}$, and for every
$S$-orbit $I\subseteq\mathbb{A}$ such that $I\cap S=\emptyset$:

$\displaystyle\textstyle\sum_{a\in I}v(S\cup\\{a\\})=0.$ (8)

Note that if $S=\\{a_{1},\ldots,a_{k-1}\\}$ where $a_{1}<\cdots<a_{k-1}$, then
$S$-orbits disjoint from $S$ are exactly the $k$ open intervals:

$\displaystyle(-\infty,a_{1}),\ (a_{1},a_{2}),\ldots,(a_{k-2},a_{k-1}),\
(a_{k-1},+\infty).$ (9)

It is easy to check that balanced vectors form an equivariant subspace of
$\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$. We denote this space by
$B$. An immediate corollary of Claim IV.5 is that every cog is balanced.

We will show that $B$ is the subspace generated by all cogs. For this, it is
enough to show that every balanced vector is a linear combination of cogs. To
this end, we will prove that every balanced vector supported by some fixed
$T=\\{a_{1},\ldots,a_{n}\\}$ (that is, every vector in
$B\cap\operatorname{\mathsf{Lin}}{T\choose k}$) is a linear combination of
cogs supported by $T$ (or, in short, cogs over $T$). We shall do this by
calculating the (finite!) dimension of the space
$B\cap\operatorname{\mathsf{Lin}}{T\choose k}$. But first, let us count the
cogs:

###### Claim IV.6

There are at least ${n-k}\choose k$ linearly independent cogs over $T$.

###### Proof.

Call a set $\alpha$ as in (7) narrow if no element in $T$ lies in between
$a_{i}$ and $b_{i}$ for any $i$. For a narrow $\alpha$, the cog $\nu^{\alpha}$
will also be called narrow.

There are exactly ${n-k}\choose{k}$ narrow sets in $T$: choosing a narrow set
from the $n$-element set $T$ amounts to choosing $k$ elements from an
$(n-k)$-element set, and then viewing the chosen elements as neighbouring
pairs $(a_{i},b_{i})$ in the narrow set.

All narrow cogs over $T$ are linearly independent. To see why, consider the
componentwise partial order $\sqsubseteq$ on $T\choose k$:

$(a_{1}<\cdots<a_{k})\sqsubseteq(a^{\prime}_{1}<\cdots<a^{\prime}_{k})\quad\text{if}\quad
a_{i}\leq a^{\prime}_{i}\quad\text{for all $i$}.$

Note that on narrow sets, the mapping:

$\underbrace{a_{1}<b_{1}<\cdots<a_{k}<b_{k}}_{\alpha}\quad\mapsto\quad\underbrace{a_{1}<\cdots<a_{k}}_{\alpha\rtimes\emptyset}$

is injective, so $\sqsubseteq$ lifts to a partial order on the set of narrow
sets, and hence on the set of narrow cogs.

Assume that narrow cogs are linearly dependent, and so there is some linear
combination:

$\sum_{\alpha}p_{\alpha}\nu^{\alpha}=0$ (10)

where the sum ranges over all narrow sets $\alpha$ in $T$, and
$p_{\alpha}\in\mathbb{F}$. Note that this equation lives in the vector space
$\operatorname{\mathsf{Lin}}{T\choose k}$.

Let $\alpha$ be a minimal (with respect to $\sqsubseteq$) narrow set such that
$p_{\alpha}\neq 0$. Notice that, for every $\alpha$, $\nu^{\alpha}$ is the
greatest (with respect to $\sqsubseteq$) narrow cog in which
$\alpha\rtimes\emptyset$ appears with a nonzero coefficient. Since every
narrow cog smaller than $\nu^{\alpha}$ has coefficient zero on the left-hand
side of (10), then $\alpha\rtimes\emptyset$ has a nonzero coefficient in the
sum of the left-hand side of (10), which contradicts the equation in (10). ∎

The main technical result in the proof of the present lemma is the following
claim, which is proved in Appendix B.

###### Claim IV.7

$B\cap\operatorname{\mathsf{Lin}}{T\choose k}$ is of dimension at most
${{n-k}\choose k}$.

Claims IV.6 and IV.7 together imply that $B$ is the space generated by all
cogs, and therefore – by Claim IV.5 – that it is the smallest nontrivial
equivariant subspace of $\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$.

To finish the proof of Lemma IV.4, for every $i\in\\{1,\ldots,k\\}$ consider
the equivariant linear map:

$\textstyle g_{i}:\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k}\to\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k-1}$

defined by:

$\textstyle g_{i}(v)(S)=\sum_{a\in I}v(S\cup\\{a\\})$

where $I$ is the $i$’th orbit on the list (9). Tupling these functions for all
$i$ we obtain an equivariant linear map:

$\textstyle g:\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k}\to\left(\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k-1}\right)^{k}.$

By definition, the kernel of $g$ is $B$, so there is a subspace embedding:

$\textstyle\left(\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}\right)/B\
\subseteq\ \left(\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k-1}\right)^{k}.$

Note that $B$ does not have any nontrivial equivariant subspaces, so
$\operatorname{\mathsf{length}}(B)=1$. By Lemma IV.2(i) applied to $V=B$ and
$W=\operatorname{\mathsf{Lin}}{\mathbb{A}\choose k}$ we thus obtain:

$\displaystyle\textstyle\operatorname{\mathsf{length}}\big{(}\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k}\big{)}=1+\operatorname{\mathsf{length}}\left(\left(\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k}\right)/B\right)\leq$ $\displaystyle\textstyle\leq
1+\operatorname{\mathsf{length}}\left(\left(\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k-1}\right)^{k}\right)=1+k\cdot\operatorname{\mathsf{length}}\big{(}\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k-1}\big{)}$

and conclude the proof of Lemma IV.4. ∎

The following is now easy:

###### Lemma IV.8

The ordered atoms $\mathbb{A}=({\mathbb{Q}},<)$ have the finite length
property. For an equivariant orbit-finite set $Q$, the space
$\operatorname{\mathsf{Lin}}Q$ has length at most

$\displaystyle\text{(orbit count of $Q$)}\cdot(1+{\text{atom dimension of
$Q$}})!$

###### Proof.

If $Q$ has only one orbit, then it is an image of an equivariant surjective
function from $\mathbb{A}\choose k$, where $k$ is the atom dimension of $Q$.
By induction on $k$, using Lemma IV.4, we obtain

$\displaystyle\textstyle\operatorname{\mathsf{length}}\big{(}\operatorname{\mathsf{Lin}}{\mathbb{A}\choose
k}\big{)}\leq(1+k)!$ (11)

The lemma then follows by Lemma IV.2(iii).

Finally, the case of multi-orbit $Q$ follows from Lemma IV.2(ii). ∎

From this it is easy to deduce the finite length property for equality atoms.

###### Lemma IV.9

The equality atoms $\mathbb{A}=({\mathbb{N}},=)$ have the finite length
property. For an equivariant orbit-finite set $Q$, the space
$\operatorname{\mathsf{Lin}}Q$ has length at most

$\displaystyle\text{(orbit count of $Q$)}\cdot k!\cdot(1+k)!$

where $k$ is the atom dimension of $Q$.

###### Proof.

The set $\mathbb{A}^{(k)}$, a single-orbit set over equality atoms, can be
seen as an equivariant set over ordered atoms as well, with $k!$ disjoint
orbits. Each of these orbits is equivariantly (over ordered atoms) isomorphic
to $\mathbb{A}\choose k$. Lemma IV.8 then implies that
$\operatorname{\mathsf{Lin}}\big{(}\mathbb{A}^{(k)}\big{)}$ has length at most
$k!\cdot(1+k)!$.

Every single-orbit equivariant set $Q$ is an image of an equivariant
surjective function from $\mathbb{A}^{(k)}$, where $k$ is the atom dimension
of $Q$; the lemma follows by Lemma IV.2(iii). The case of multi-orbit $Q$
follows from Lemma IV.2(ii). ∎

So far, we have bounded the lengths of chains of equivariant subspaces. Lemma
IV.10 below, proved in Appendix C, extends these bounds to finitely supported
chains. Here it is important that all subspaces the chain are required to have
the same support.

###### Lemma IV.10

Consider the equality or ordered atoms. Let $\bar{a}$ be a tuple of atoms. For
every $\bar{a}$-supported orbit-finite set $Q$, there is a finite upper bound
on the length of chains of $\bar{a}$-supported subspaces of
$\operatorname{\mathsf{Lin}}Q$.

##  V The equivalence algorithm

In this section, we use the finite length properties from Section IV to
complete the proof of Theorem III.2. We assume that the atoms $\mathbb{A}$ are
the equality or ordered atoms.

###### Lemma V.1

Let ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ be equivariant weighted orbit-
finite automata, and let $n$ and $k$ be as in Theorem III.2. If the recognized
weighted languages are different, then this difference is witnessed by some
input word of length at most

$\displaystyle 2^{\mathrm{poly}(k)}\cdot n.$

###### Proof.

Let $Q$ be the state space of the difference automaton
${\mathcal{A}}_{1}-{\mathcal{A}}_{2}$ as described in the reduction from
equivalence to zeroness. For an input word $w\in\Sigma^{*}$, let
$[w]\in\operatorname{\mathsf{Lin}}Q$ be its corresponding configuration in the
difference automaton, and let $V_{i}\subseteq\operatorname{\mathsf{Lin}}Q$ be
the subspace that is spanned by configurations of input words of length at
most $i$. By Lemmas IV.9 and IV.8, we know that the chain $\\{V_{i}\\}_{i}$
must stabilize in a number of steps that is bounded as in the statement of the
lemma. This means that for every input word, its configuration is a linear
combination of configurations of short words; in particular the difference
automaton can produce a nonzero output if and only if it can produce a nonzero
output on a short input word. ∎

At this point, we could solve the equivalence problem by guessing a short
differentiating word, leading to a nondeterministic algorithm for non-
equivalence, with running time as in the bound from Lemma V.1. We can,
however, improve this to get a deterministic algorithm, by using a reduction
to the equivalence problem for finite weighted automata. Short input words
necessarily use few atoms, and therefore the equivalence problem boils down to
testing equivalence for input words that have few atoms. The latter problem is
solved in the following lemma.

###### Lemma V.2

Consider the following problem.

  * •

Input. Two equivariant weighted orbit-finite automata ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$ and a number $\ell\in\\{1,2,\ldots\\}$;

  * •

Question. Are the two automata equivalent on all input words supported by at
most $\ell$ atoms?

This problem can be solved in time polynomial in $n\cdot\ell^{k}$, where the
parameters $n$ and $k$ are defined as in Theorem III.2.

###### Proof.

Choose a tuple $\bar{a}$ of $\ell$ atoms. Since the automata are equivariant,
they are equivalent on inputs with at most $\ell$ atoms if and only if they
are equivalent on inputs words supported by $\bar{a}$.

By equivariance and condition (*) from Definition III.1, if a state $q$ and an
input letter $\sigma$ are both supported by $\bar{a}$, then the same is true
for every state $p$ such that $(q,\sigma,p)$ is a transition with nonzero
weight. Therefore, when restricted to input words that are supported by
$\bar{a}$, both automata only use states that are supported by $\bar{a}$.
These observations motivate the following definition: for $i\in\\{1,2\\}$, let
${\mathcal{A}}_{i,\bar{a}}$ the weighted automaton that is obtained from
${\mathcal{A}}_{i}$ by restricting the states and alphabet to elements
supported by $\bar{a}$, and restricting the transitions and weight functions
to the new alphabet and states. These automata are finite, with size bounded
by $n\cdot\ell^{k}$. The lemma follows by applying the polynomial time
algorithm for equivalence of finite weighted automata. ∎

The above two lemmas complete the proof of Theorem III.2. The algorithm for
zeroness is simply the algorithm from Lemma V.2, with $\ell$ being the bound
from Lemma V.1.

##  VI Vector spaces with atoms

In this section, we study in more depth vector spaces that are spanned by
orbit-finite sets. Apart from their independent interest, these results will
be used in Section VII to minimize weighted automata, and in Section VIII to
decide equivalence for unambiguous automata.

So far we have discussed vector spaces of the form
$\operatorname{\mathsf{Lin}}Q$, where $Q$ is an orbit-finite set. One could
call these spaces orbit-finite-dimensional, since they have an orbit-finite
basis. Although they are good enough to treat weighted orbit-finite automata,
such vector spaces are not very robust. The reason is that extracting a basis
uses choice, see [2, Thm. 1], and the principle of choice fails for sets with
atoms.

Example 6.  Recall the vector space $\operatorname{\mathsf{Lin}}\mathbb{A}$
that was discussed in Example IV, and the subspace $V$ that was spanned by

$\displaystyle X=\\{a-b:a\neq b\in\mathbb{A}\\}.$

The set $X$ is not a basis, since the vectors $a-b$ and $b-a$ (or $a-b$, $b-c$
and $a-c$) are linearly dependent. However, $X$ is a single equivariant orbit,
so it does not have any nonempty proper subset that is equivariant. Therefore,
no equivariant subset of $X$ is a basis. In fact, $V$ does not have any
equivariant basis, even if we allow bases that are not contained in $X$. It
does have, however, a finitely supported basis contained in $X$: for any fixed
atom $a_{0}\in\mathbb{A}$, the set

$\displaystyle\\{a_{0}-b:b\in\mathbb{A}-\\{a_{0}\\}\\}$

is a basis. $\Box$

In the previous example, there was no equivariant basis, but there was a
finitely supported one. In the next example there is no finitely supported
basis at all.

Example 7.  Consider the equality atoms and the space
$\operatorname{\mathsf{Lin}}(\mathbb{A}^{(2)})$. A vector in this space can be
visualized as a weighted directed finite graph, where vertices are atoms and
the weight of an edge $(a,b)$ is the corresponding coefficient in the vector.
Consider the subspace of $\operatorname{\mathsf{Lin}}(\mathbb{A}^{(2)})$
spanned by

$\displaystyle X=\\{(a,b)-(b,a):a\neq b\in\mathbb{A}\\}.$

This subspace consists of graphs where for every pair of vertices, the
connecting edges in both directions have opposite weights. We claim that there
is no finitely supported subset of $X$ that is a basis of this space. Indeed,
suppose that $Y\subseteq X$ is a finitely supported basis. It is easy to see
that for every two distinct atoms $a,b$, the set $Y$ must contain one of the
vectors

$(a,b)-(b,a)\qquad\text{or}\qquad(b,a)-(a,b).$

If the atoms $a,b$ are fresh (i.e. they do not belong to the least support of
$Y$), by swapping these two atoms we map one of the vectors to the other,
hence both vectors must belong to $Y$. However, the two vectors are linearly
dependent and so $Y$ is not a basis. Using a similar argument one can show
that the subspace spanned by $X$ does not have any finitely supported basis,
even if we allow bases that are not contained in $X$. $\Box$

The above example shows that vector spaces with an orbit-finite basis are not
closed under finitely supported subspaces. The same issue appears with
finitely supported quotients (images of surjective linear maps). These issues
will become a problem in the next section, where we minimize weighted orbit-
finite automata, since minimization will require taking subspaces and
quotients. To deal with these issues, we propose an obvious generalization:
vector spaces that are spanned by an orbit-finite set (which need not be
independent).

######  Definition VI.1 (Orbit-finitely spanned vector space)

Fix a field $\mathbb{F}$ and an atom structure. A _vector space with atoms_ is
a vector space such that the underlying set $V$ is a set with atoms, and the
operations

$\displaystyle\underbrace{+:V\times V\to V}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-3.1111pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
binary addition}\crcr}}}}}}\qquad\underbrace{\cdot:\mathbb{F}\times V\to
V}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-3.1111pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
scalar multiplication}\crcr}}}}}}}}$

are finitely supported. A vector space with atoms is called _orbit-finitely
spanned_ if there is an orbit-finite subset of the vector space which spans
it.

As we have seen in Example VI, some orbit-finitely spanned vector spaces do
not have any orbit-finite basis. They do, however, have finite length:

###### Lemma VI.2

For atoms with the finite length property, equivariant orbit-finitely spanned
vector spaces have finite length.

###### Proof.

Let $V$ be spanned by an equivariant orbit-finite set $Q$, and let

$f\colon\operatorname{\mathsf{Lin}}Q\to V$

be the unique linear map which extends the inclusion of $Q$ in $V$. This is a
surjective finitely supported linear map, so (by Lemma IV.2(iii)) the length
of $V$ is not greater than the length of $\operatorname{\mathsf{Lin}}Q$, which
is finite by the finite length property. ∎

######  Theorem VI.3 (Closure properties)

Assume that the atoms have the finite length property. Equivariant orbit-
finitely spanned vector spaces are closed under equivariant quotients,
equivariant subspaces, direct sums and tensor products.

###### Proof.

Quotients and direct sums are immediate. For the tensor product $U\otimes V$,
suppose $U$ and $V$ are spanned by $Q$ and $P$. Since
$\operatorname{\mathsf{Lin}}Q\otimes\operatorname{\mathsf{Lin}}P$ is
isomorphic to $\operatorname{\mathsf{Lin}}(Q\times P)$, it follows that
$U\otimes V$ is spanned by $Q\times P$, which is orbit-finite.

We are left with the subspaces. Suppose that $V$ is equivariant and orbit-
finitely spanned, and let $U$ be an equivariant subspace. For
$n\in\\{1,2,\ldots\\}$ define $U_{n}$ to be the subspace of $U$ that is
spanned by vectors from $U$ that are supported by at most $n$ atoms. This is a
chain

$\displaystyle U_{1}\subseteq U_{2}\subseteq\cdots$

of equivariant vector spaces, and therefore by the finite length property it
stabilizes after finitely many steps. It remains to show that every $U_{n}$ is
orbit-finitely spanned. For every tuple $\bar{b}$ of $n$ atoms, the vectors in
$V$ that are supported by $\bar{b}$ form a finite-dimensional vector space,
and so they have a finite basis. By closing this basis under atom
automorphisms, we get an orbit-finite spanning set for $U_{n}$. ∎

Thanks to Lemma IV.10, in the equality and ordered atoms, Lemma VI.2 and
Theorem VI.3 hold also for orbit-finitely spanned vector spaces that are not
necessarily equivariant.

In the remainder of this section, we discuss another closure property of
orbit-finitely spanned vector spaces: if $V$ is an equivariant orbit-finitely
spanned vector space, then the same is true for its _finitely supported dual_
, which is the vector space of finitely supported linear maps from $V$ to
$\mathbb{F}$. We will prove closure under finitely supported duals for the
equality and ordered atoms, and we do not know if it holds for other
oligomorphic atoms.

Before considering finitely supported duals, we discuss a slightly simpler
vector space, namely the finitely supported functions from some orbit-finite
set to the underlying field. Let $Q$ be an orbit-finite set. Define

$\displaystyle Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$

to be the set of finitely supported functions from $Q$ to the field. This set
can be viewed as a vector space, with coordinate-wise addition and scalar
multiplication. We have

$\displaystyle\operatorname{\mathsf{Lin}}Q\ \subseteq\
Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F},$

and the inclusion is strict when $Q$ is infinite, as witnessed by the function
that returns $1$ on all arguments.

Example 8.  For the equality atoms, the space
$\mathbb{A}\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$ is spanned
by the functions

$\displaystyle\\{f_{\mathbb{A}}\\}\ \cup\ \\{f_{a}:a\in\mathbb{A}\\}$ (12)

where $f_{\mathbb{A}}$ maps all atoms to $1$, while $f_{a}$ maps $a$ to $1$
and the remaining atoms to $0$. Indeed, every function
$f:\mathbb{A}\to\mathbb{F}$ supported by an atom tuple $\bar{a}$ can be
presented as:

$\displaystyle f\ =\ \underbrace{f(c)}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-5.26944pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize$c$
is some fresh }\\\\\hbox{{\ignorespaces\scriptsize atom not in
$\bar{a}$}\crcr}}}}}}\cdot f_{\mathbb{A}}\ +\
\sum_{a\in\bar{a}}(f(a)-f(c))\cdot f_{a}.}}$

The functions from (12) are linearly independent, and therefore they form an
orbit-finite basis of
$\mathbb{A}\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$.

A similar result holds for the ordered atoms, except that there the spanning
set of functions is

$\displaystyle\\{f_{\mathbb{A}}\\}\ \cup\ \\{f_{a}:a\in\mathbb{A}\\}\ \cup\
\\{f_{>a}:a\in\mathbb{A}\\}$

where $f_{\mathbb{A}}$ and $f_{a}$ are as before and $f_{>a}$ maps $b$ to $1$
precisely if $b>a$. $\Box$

The above example shows that
$\mathbb{A}\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$ is orbit-
finitely spanned. This is true for every orbit-finite set, not just
$\mathbb{A}$:

###### Theorem VI.4

Assume the equality or the ordered atoms. If $Q$ is an orbit-finite set, then
$Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$ is orbit-finitely
spanned.

###### Proof.

To simplify notation, we assume that $Q$ is equivariant; this implies the
general case anyway, because every orbit-finite set is contained in some
equivariant orbit-finite set. Furthermore, it is safe to assume that $Q$ is a
single-orbit set.

We need to exhibit an orbit-finite set $\Phi$ of finitely supported functions,
so that every finitely supported function $f:Q\to\mathbb{F}$ is a linear
combination of functions from $\Phi$. It is enough to show this for the case
where $f$ is the characteristic function of a finitely supported set
$R\subseteq Q$, since such characteristic functions are easily seen to span
the space of all finitely supported functions. So consider such a set $R$,
supported by some tuple $\bar{a}$ of atoms. $R$ is then a disjoint union of
$\bar{a}$-orbits, and it is enough to consider the case where $R$ is a single
$\bar{a}$-orbit.

From here, the arguments for the equality and the ordered atoms begin to
differ.

For the case of ordered atoms, we know that $Q$ is in equivariant bijection
with $\mathbb{A}\choose k$ for some number $k$, so it is enough to deal with
$Q={\mathbb{A}\choose k}$. Let $R$ be the $\bar{a}$-orbit of some

$\textstyle r=\\{a_{1},\ldots,a_{k}\\}\in{\mathbb{A}\choose k}.$

Each $a_{i}$ belongs to some $\bar{a}$-orbit of atoms. This orbit is an
interval, so it is equal to the orbit determined by at most two atoms from
$\bar{a}$. (One atom is enough if $a_{i}$ belongs to $\bar{a}$, or if it is
larger than (or smaller than) every atom in $\bar{a}$.) Picking these atoms
for each $i=\\{1,\ldots,k\\}$, we obtain a tuple $\bar{b}\subseteq\bar{a}$ of
at most $2k$ atoms, such that $R$ is equal to the $\bar{b}$-orbit of $r$. As a
consequence, $R$ is supported by $\bar{b}$.

As a result, we may take $\Phi$ to be the set of characteristic functions of
subsets of $Q$ supported by at most $2k$ atoms. Since $k$ is fixed for a given
$Q$, this is an orbit-finite set.

The argument for the equality atoms is only a little more complicated. Here
for $\Phi$ we take the set of characteristic functions of subsets of $Q$
supported by at most $k$ atoms.

We know that $Q$ is the image of an equivariant surjection from
$\mathbb{A}^{(k)}$ for some number $k$, so it is enough to deal with
$Q=\mathbb{A}^{(k)}$. Let $R$ be the $\bar{a}$-orbit of some

$\textstyle r=(a_{1},\ldots,a_{k})\in\mathbb{A}^{(k)}.$

We proceed by induction on the number of atoms in $r$ that are not in
$\bar{a}$. If this number is zero, then $R$ is the singleton of $r$ and the
characteristic function of $R$ is in $\Phi$, so there is nothing to do. If
there are some atoms in $r$ that not in $\bar{a}$, denote by
$I\subseteq\\{1,\ldots,k\\}$ the set of coordinates where these atoms occur in
$r$. Then an $s\in\mathbb{A}^{(k)}$ belongs to $R$ if and only if:

  * (i)

$s$ is equal to $r$ on all coordinates apart from $I$,

  * (ii)

atom in $s$ on coordinates from $I$ do not belong to $\bar{a}$.

Let $\hat{R}\subseteq Q$ be the set of tuples $s$ that satisfy condition (i)
above; obviously $R\subseteq\hat{R}$. Moreover, $\hat{R}$ has a support of
size $k-|I|$, so $\chi_{\hat{R}}$, the characteristic function of $\hat{R}$,
belongs to $\Phi$.

Let $\\{r_{1},\ldots,r_{n}\\}$ be the set of all $k$-tuples in
$\mathbb{A}^{(k)}$ that can be obtained from $r$ by replacing some (not
necessarily all, but at least one) atoms on coordinates from $I$ by some atoms
from $\bar{a}$. Let $R_{i}$ be the $\bar{a}$-orbit of $r_{i}$, for each $i$.
The sets $R_{i}$ are pairwise disjoint, and their union is equal to the
difference $\hat{R}\setminus R$, therefore there is a linear equation:

$\textstyle\chi_{R}=\chi_{\hat{R}}-\sum_{i=1}^{n}\chi_{R_{i}}.$

By the inductive assumption, each $\chi_{R_{i}}$ is a linear combination of
functions from $\Phi$, which completes the proof. ∎

###### Corollary VI.5

Assume the equality or ordered atoms. If $V$ is an orbit-finitely spanned
vector space, then the same is true for its finitely supported dual.

###### Proof.

If a vector space is spanned by an orbit-finite set $Q$, then its finitely
supported dual embeds into the space
$Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$, which is orbit-
finitely spanned by Theorem VI.4. The corollary follows since orbit-finitely
spanned vector spaces are closed under subspaces. ∎

In contrast to the finite-dimensional case, orbit-finitely spanned vector
spaces are not isomorphic to their finitely supported duals. Indeed, Example
VI shows that the finitely supported dual of
$\operatorname{\mathsf{Lin}}\mathbb{A}$ is equivariantly isomorphic to the
space $\operatorname{\mathsf{Lin}}(1+\mathbb{A})$. There is no linear
isomorphism between them which is equivariant, or even finitely supported.

The following example shows that the restriction to equality or ordered atoms
was important in Theorem VI.4. This example hints on the difficulties one may
encounter when generalizing our theory to, say, arbitrary oligomorphic atom
structures.

Example 9.  Consider the graph atoms [3, Section 7.3.1], i.e. the case when
the atoms structure $\mathbb{A}$ is the Rado graph. For an atom tuple
$\bar{a}$, define $\chi_{\bar{a}}:\mathbb{A}\to\mathbb{F}$ to be the
characteristic function of the common neighborhood of $\bar{a}$, i.e. the
function which maps an atom to 1 if it has an edge to all atoms in $\bar{a}$,
and otherwise maps the atom to 0. This is a finitely supported function, so it
belongs to $\mathbb{A}\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$.
For $n\in\\{1,2,\ldots\\}$, let

$\displaystyle
V_{n}\subseteq\mathbb{A}\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$

to be the subspace which is spanned by functions of the form $\chi_{\bar{a}}$,
where $\bar{a}$ is a tuple of at most $n$ atoms. We will show that
$V_{n}\subsetneq V_{n+1}$ for every $n$.

Indeed, assume to the contrary a linear equation

$\textstyle\chi_{\bar{a}}=\sum_{i=1}^{n}p_{i}\cdot\chi_{\bar{b_{i}}}$

where all $p_{i}\neq 0$ and where $\bar{a}$ strictly larger than every
$\bar{b_{i}}$. Pick $i$ such that $\bar{b_{i}}$ is minimal in the equation,
i.e. such that $\bar{b_{j}}\not\subseteq\bar{b_{i}}$ for all $j\neq i$. Pick
an atom $c$ that is in the common neighborhood of $\bar{b_{i}}$ but not in the
common neighborhood of $\bar{a}$ or any other $\bar{b_{j}}$; it exists by the
universal property of the Rado graph. Then $\chi_{\bar{b_{i}}}(c)=1$,
$\chi_{\bar{a}}(c)=0$ and $\chi_{\bar{b_{j}}}(c)=0$ for $j\neq i$, therefore
$p_{i}=0$, a contradiction.

It follows that the vector space
$\mathbb{A}\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$ does not
have finite length. We do not know if the problem is that: (a) the finite
length property fails; (b) the property of being orbit-finitely spanned does
not extend to dual spaces. $\Box$

##  VII Minimization

Schützenberger’s original paper on weighted automata contained a minimization
procedure. We now describe a version of that procedure in the orbit-finite
setting using the theory of orbit-finitely spanned vector spaces from Section
VI.

Consider a weighted orbit-finite automaton ${\mathcal{A}}$ with states $Q$. We
assume that the automaton is reachable, in the following sense: every vector
in $\operatorname{\mathsf{Lin}}Q$ is a linear combination of configurations
corresponding to input words. For a vector $v\in\operatorname{\mathsf{Lin}}Q$,
define the weighted language of $v$ to be the weighted language recognized by
the automaton obtained from ${\mathcal{A}}$ by setting the initial map to $v$,
i.e. the initial weight of a state is its coefficient in the vector $v$.
Define the _syntactic congruence_ $\sim$ to be the equivalence relation on
$\operatorname{\mathsf{Lin}}Q$ which identifies two vectors if the
corresponding weighted languages are equal. It is not hard to see that $\sim$
is closed under both linear combinations and applying atom automorphisms, one
can speak of an equivariant quotient vector space
$(\operatorname{\mathsf{Lin}}Q)/_{\sim}$. Equivalently, this is the quotient
of the vector space $\operatorname{\mathsf{Lin}}Q$ under the subspace which
consists of vectors $v$ whose corresponding weighted language is 0 everywhere.
This quotient space is orbit-finitely spanned by the equivalence classes of
states in $Q$.

In the finite dimensional case studied by Schützenberger, a minimal automaton
is obtained by choosing some basis for this vector space, and using it as the
state space of the minimal automaton. This idea, however, will not work in the
orbit-finite setting, due to the difficulties with finding a basis that were
described in Examples VI and VI.

Example 10.  For the equality atoms and the field of rational numbers,
consider the weighted language $L\colon\mathbb{A}^{*}\to\mathbb{F}$:

$L(w)=\begin{cases}1&\text{if }w=aba\text{ for some }a\neq b\in\mathbb{A},\\\
-1&\text{if }w=abb\text{ for some }a\neq b\in\mathbb{A},\\\
0&\text{otherwise.}\end{cases}$

This is recognized by a weighted orbit-finite automaton where the set of
states $Q$ is

$\underbrace{\\{\perp\\}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-6.2222pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
initial weight 1}\\\\\hbox{{\ignorespaces\scriptsize final weight
0}\crcr}}}}}}\quad+\quad\underbrace{\mathbb{A}+\mathbb{A}^{(2)}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-6.2222pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
initial weight 0}\\\\\hbox{{\ignorespaces\scriptsize final weight
0}\crcr}}}}}}\quad+\quad\underbrace{\\{\top\\}}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-6.2222pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
initial weight 0}\\\\\hbox{{\ignorespaces\scriptsize final weight
1}\crcr}}}}}}}}}}}}$

and the transitions with nonzero weight are

$\underbrace{(\perp,a,a),\ (a,b,(a,b)),\
((a,b),a,\top)}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-3.1111pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
weight 1}\crcr}}}}}},\
\underbrace{((a,b),b,\top)}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-3.1111pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
weight -1}\crcr}}}}}}}}$

for every $a\neq b\in\mathbb{A}$. For the syntactic congruence $\sim$, it is
not hard to see that $(a,b)\sim-(b,a)$ for every $a\neq b$. The quotient space
$\operatorname{\mathsf{Lin}}Q/_{\sim}$ is:

$\ \operatorname{\mathsf{Lin}}(\,\\{\perp,\top\\}+\mathbb{A}\,)\ \oplus\ X,$

where $X$ is the space from Example VI. This space has no finitely supported
basis. $\Box$

This example shows that in the orbit-finite setting the minimization procedure
can leave the realm of weighted orbit-finite automata. To overcome this issue,
we use an alternative model for weighted automata, which we call _orbit-
finitely spanned automata_. These are deterministic automata where the state
spaces are orbit-finitely spanned vector spaces and all weight functions are
linear maps.

######  Definition VII.1 (Orbit-finitely spanned automaton)

An orbit-finitely spanned automaton consists of:

  1. 1.

an orbit-finite input alphabet $\Sigma$;

  2. 2.

an orbit-finitely spanned vector space $V$;

  3. 3.

a finitely supported transition function

$\displaystyle\delta:V\times\Sigma\ \to\ V$

such that $v\mapsto\delta(v,a)$ is a linear map for every $a\in\Sigma$;

  4. 4.

an initial vector $v_{0}\in V$;

  5. 5.

a finitely supported linear map $F:V\to\mathbb{F}$.

An orbit-finitely spanned automaton recognizes a weighted language as
expected: given an input word, it computes an element of $\mathbb{F}$ by
starting in the initial vector, then applying the transition functions
corresponding to the input letters, and finally applying the final function
$F$.

###### Theorem VII.2

The same weighted languages are recognized by orbit-finitely spanned automata
and weighted orbit-finite automata.

The theorem is proved in Appendix D. It differs from an analogous construction
in the finite-dimensional setting in one aspect: if one converts a weighted
orbit-finite automaton with states $Q$ to an orbit-finitely spanned automaton
in the natural way, then the resulting vector space
$\operatorname{\mathsf{Lin}}Q$ has an orbit-finite basis. Not every orbit-
finitely spanned automaton arises this way though, because we do not require
the vector space to have an orbit-finite basis. A key step in the proof of
Theorem VII.2 is that every orbit-finitely spanned automaton is equivalent to
one whose state space has a basis.

The point of orbit-finitely spanned automata is that they can be minimized.
Define a _homomorphism_ between orbit-finitely spanned automata
${\mathcal{A}}$ and ${\mathcal{B}}$ to be a finitely supported linear map from
the state space of ${\mathcal{A}}$ to the state space of ${\mathcal{B}}$,
which is consistent with the structure of the automata in the natural way, see
[3, Sec. 6.2]. If ${\mathcal{A}}$ is an orbit-finitely spanned automaton that
is reachable (i.e. its vector space is spanned by vectors that can be reached
via input words), and $\sim$ is its syntactic congruence (defined in the same
way as for weighted orbit-finite automata), then there is a well defined
quotient automaton ${\mathcal{A}}_{/\sim}$. The quotient automaton admits a
homomorphism from every reachable orbit-finitely spanned automaton that
recognizes the same weighted language as ${\mathcal{A}}$. Hence, the quotient
automaton is unique up to isomorphism, and can thus be called _the_ minimal
automaton.

We finish this section with a third perspective on weighted languages, this
time phrased in terms of monoids. Define an _orbit-finitely spanned monoid_ to
be a monoid $(M,\cdot,1)$ where the underlying set $M$ is an orbit-finitely
spanned vector space, and the monoid operation is bi-linear (i.e. linear in
each of the two coordinates). We say that a weighted language
$L\colon\Sigma^{*}\to\mathbb{F}$ is recognized by such a monoid if the diagram

$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\scriptstyle{L}$$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F}$$\textstyle{\mathbb{F}}$

commutes for some finitely supported monoid homomorphism $h$ and some finitely
supported linear map $F$. The following result is somewhat unexpected, because
in the non-weighted setting, orbit-finite automata and orbit-finite monoids do
not recognize the same languages [3, Exercise 91].

###### Theorem VII.3

Orbit-finitely spanned monoids recognize the same weighted languages as
weighted orbit-finite automata and orbit-finitely spanned automata.

###### Proof.

From an orbit-finitely spanned monoid we can easily construct an orbit-
finitely spanned automaton, with the same underlying vector space. For the
converse direction, starting with a weighted orbit-finite automaton with
states $Q$, we build a monoid out of finitely supported functions:

$\displaystyle f:(Q\times
Q)\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$

such that for every $p\in Q$ there are finitely many states $q\in Q$ such that
$f(p,q)\neq 0$. By Theorem VI.4, this vector space is orbit-finitely spanned.
The monoid operation is defined by:

$\displaystyle(f\cdot g)(p,q)=\sum_{r\in Q}f(p,r)\cdot g(r,q),$

with the sum being finite by the assumption on $f$. This operation is finitely
supported and bi-linear. The recognizing homomorphism is built using the same
construction as when converting a nondeterministic automaton into a monoid. ∎

An advantage of the monoid approach is the symmetry between reading the input
word left-to-right and right-to-left. In particular, the languages recognized
by orbit-finitely spanned monoids are easily seen to be closed under
reversals; this is harder to see for the remaining models.

##  VIII Application to unambiguous automata

A classical application of weighted automata is a polynomial time algorithm
for language equivalence of unambiguous finite automata, i.e.,
nondeterministic automata with at most one accepting run for every input word.
Two unambiguous finite automata are equivalent (i.e. they recognize the same
language) if and only if they have the same number of accepting runs for every
input word (since the number of accepting runs is zero or one). For every
nondeterministic finite automaton, one can easily construct in polynomial time
a weighted finite automaton which maps every input word to the number of
accepting runs of the nondeterministic finite automaton; and therefore two
unambiguous finite automata are equivalent if and only if the corresponding
weighted finite automata are equivalent.

In this section, we show how this result can be lifted from finite to orbit-
finite automata. Consider first the case of unambiguous orbit-finite automata
which are non-guessing, in the sense that they have finitely many initial
states, and for every state $q$ and input letter $\sigma$, there are finitely
many transitions of the form $(q,a,p)$. As explained in Example III.1, for
such automata we can easily count runs using a weighted orbit-finite
automaton, and thus we can solve the language equivalence problem in the same
time as in Theorem III.2. However, our techniques apply also to unambiguous
orbit-finite automata without the non-guessing restriction.

###### Theorem VIII.1

Assume that the atoms are either $({\mathbb{N}},=)$ or $({\mathbb{Q}},<)$. The
equivalence problem for equivariant222As for Theorem III.2, this theorem would
also work for finitely supported automata, but the notation would become more
involved. unambiguous register automata333We state the theorem using
unambiguous register automata, see [13, Sect. 2] and not for general
unambiguous orbit-finite automata, so that it can be more easily compared to
existing results in the literature., which are allowed to use guessing, is in
ExpTime, and in polynomial time when the number of registers is fixed.

This improves on previous work [13, 14] in that: (a) we allow unrestricted
guessing; (b) we allow ordered atoms and not just equality atoms;and (c) we
improve the previous upper bounds of 2ExpSpace for an unbounded number of
registers and ExpSpace for a fixed number of registers.

The rest of this section is devoted to proving the above theorem. The main
observation is that an orbit-finitely spanned automaton can count accepting
runs for a nondeterministic orbit-finite automaton, as stated in the following
lemma.

###### Lemma VIII.2

Consider an equivariant nondeterministic orbit-finite automaton
${\mathcal{A}}$, which has finitely many accepting runs for every input word.
There is an equivariant orbit-finitely spanned automaton ${\mathcal{B}}$, over
the field of rational numbers, which outputs for every word the number of
accepting runs of ${\mathcal{A}}$. Furthermore, the length of the vector space
used by the automaton ${\mathcal{B}}$ is at most

$\displaystyle 2^{poly(k)}\cdot n^{O(k)}.$ (13)

where $k$ and $n$ are as in Theorem III.2.

###### Proof.

Let $\Sigma$ be the input alphabet, and let $Q$ be the state space of
${\mathcal{A}}$. Without loss of generality we assume that every state can
reach some accepting state; the remaining states can be eliminated from the
automaton without affecting the recognized language or the numbers of
accepting runs [3, Cor. 9.12].

For an input word $w\in\Sigma^{*}$, define its _configuration_

$\displaystyle[w]\in Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$

to be the function which maps each state $q$ to the number of runs on $w$ that
begin in an initial state and end in state $q$. The configuration produces
only finite numbers, because there cannot be a state $q$ that can be reached
via infinitely many runs over the same input word $w$; otherwise we could
append some word to $w$ and get infinitely many accepting runs. Define

$\displaystyle V=\operatorname{\mathsf{Span}}\\{[w]:w\in\Sigma^{*}\\}\subseteq
Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$

to be the subspace of $Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$
that is spanned by configurations. Although the definition of $V$ uses a
spanning set that is not necessarily orbit-finite (because $\Sigma^{*}$ is not
orbit-finite), the space $V$ is orbit-finitely spanned, as an equivariant
subspace of an orbit-finitely spanned vector space, see Theorem VI.3.

We use $V$ as the state space of a orbit-finitely spanned automaton
${\mathcal{B}}$. Let us first prove the length bound (13). It is enough to
prove the bound for the length of
$Q\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$, since $V$ is an
equivariant subspace of it. To this end, note that the set $Q$ can be
decomposed as a disjoint union of $n$ single-orbit sets with dimension at most
$k$. Since

$\operatorname{\mathsf{length}}((Q_{1}\\!+\\!Q_{2})\\!\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\\!\mathbb{F})=\operatorname{\mathsf{length}}(Q_{1}\\!\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\\!\mathbb{F})+\operatorname{\mathsf{length}}(Q_{2}\\!\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\\!\mathbb{F})$

it is enough to show that every equivariant single-orbit set $P$ of atom
dimension at most $k$ satisfies

$\displaystyle\operatorname{\mathsf{length}}(P\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F})\leq
2^{poly(k)}.$

Since $P\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$ embeds into
$\mathbb{A}^{(k)}\stackrel{{\scriptstyle\mathrm{fs}}}{{\to}}\mathbb{F}$, it is
enough to show that the length of the latter space is at most exponential in
$k$. This follows from the proof of Theorem VI.4.

We now describe the remaining structure of the orbit-finitely spanned
automaton. The initial state is the configuration $[\varepsilon]$, which maps
initial states to $1$ and non-initial states to $0$. Let us now define the
transition functions. For an input letter $\sigma\in\Sigma$, define a function
$\delta_{\sigma}:V\to V$ as follows

$\displaystyle\sum_{i\in I}\alpha_{i}[w_{i}]\quad\mapsto\quad\sum_{i\in
I}\alpha_{i}[w_{i}\sigma].$

We need to justify that this is well-defined. The potential problem is that
the same element of $V$ might have several decompositions as weighted sums of
configurations, and the output of $\delta_{\sigma}$ should not depend on the
choice of decomposition. Consider an element of $V$ with two decompositions:

$\displaystyle\sum_{w\in W}\alpha_{w}[w]=\sum_{w\in W}\beta_{w}[w],$

for some finite set $W\subseteq\Sigma^{*}$ of input words, and some
coefficients $\alpha_{w}$ and $\beta_{w}$ in the field. We need to show that
$\delta_{\sigma}$ produces the same output for both decomposition, i.e.

$\displaystyle\sum_{w\in W}\alpha_{w}[w\sigma]=\sum_{w\in
W}\beta_{w}[w\sigma].$ (14)

Both sides in (14) are functions from states to the field; and hence to prove
the equality we need to show that the functions on both sides give the same
output for every state $q\in Q$. Fix $q$. Let $P$ be the set of states $p\in
Q$ such that the automaton has a transition $(p,\sigma,q)$, and furthermore
$p$ appears in the configuration of some $w\in W$ with nonzero coefficient. An
important observation is that $P$ is a finite set: because the automaton
${\mathcal{A}}$ has finitely many accepting runs for every input word, the set
$P$ contains finitely many states for every word in $W$. For every word $w\in
W$ we have

$\displaystyle[w\sigma](q)=\sum_{p\in P}[w](p).$

Therefore, to prove that both functions in the equality (14) give the same
value for state $q$, we need to show

$\displaystyle\sum_{\begin{subarray}{c}w\in W\\\ p\in
P\end{subarray}}\alpha_{w}[w](p)=\sum_{\begin{subarray}{c}w\in W\\\ p\in
P\end{subarray}}\beta_{w}[w](p).$

This equality is indeed true, because our assumption implies a stronger
equality, namely that for every $p\in P$ we have

$\displaystyle\sum_{w\in W}\alpha_{w}[w](p)=\sum_{w\in W}\beta_{w}[w](p).$

The function $\delta_{\sigma}$ is clearly a linear map, and thus we can set
the transition function of the automaton to be
$\delta(v,\sigma)=\delta_{\sigma}(v)$. The automaton is defined so that after
reading an input word $w$, its state is $[w]$. The final map simply takes a
configuration to the sum of all coefficients that are accepting states. This
concludes the proof of Lemma VIII.2. ∎

###### of Theorem VIII.1.

Consider two unambiguous register automata ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$ for which we want to decide equivalence. Apply Lemma
VIII.2 to each one of them, yielding orbit-finitely spanned automata
${\mathcal{B}}_{1}$ and ${\mathcal{B}}_{2}$. Using a product construction, we
get another orbit-finitely spanned automaton ${\mathcal{B}}$ that outputs zero
for words where the automata ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$
agree, and nonzero for other words. The length of the vector space in
${\mathcal{B}}$ is at most twice the length of the vector spaces in
${\mathcal{B}}_{1}$ and ${\mathcal{B}}_{2}$, and hence it is at most

$\displaystyle 2^{poly(k)}\cdot n^{O(k)}$ (15)

where $k$ is the maximal number of registers used by the automata, and $n$ is
the sum of the numbers of control states. As in the proof of Theorem III.2, we
conclude that the automata ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ are
equivalent if and only if they are equivalent using input words and runs that
use a number of atoms as bounded by (15), and the latter equivalence can be
tested using Schützenberger’s polynomial time algorithm for equivalence on
weighted finite automata. ∎

Acknowledgments.
We are grateful to Arka Ghosh and Sławomir Lasota, who found significant
mistakes in a previous version of this paper.

## References

  * [1] Borja Balle and Mehryar Mohri.  Learning weighted automata.  In International Conference on Algebraic Informatics, pages 1–21. Springer, 2015.
  * [2] Andreas Blass.  Existence of bases implies the axiom of choice.  Contemporary Mathematics, 31:31–33, 1984.
  * [3] Mikołaj Bojańczyk.  Slightly infinite sets, 2019.  Draft from September 11, 2019, https://www.mimuw.edu.pl/ bojan/upload/main-10.pdf.
  * [4] Mikołaj Bojańczyk, Bartek Klin, and Slawomir Lasota.  Automata theory in nominal sets.  Logical Methods in Computer Science, 10(3), 2014.
  * [5] Mikołaj Bojańczyk, Bartek Klin, and Slawomir Lasota.  Automata theory in nominal sets.  Log. Methods Comput. Sci., 10(3), 2014.
  * [6] Mikołaj Bojańczyk and Rafal Stefanski.  Single use register automata for data words.  CoRR, abs/1907.10504, 2019.
  * [7] Lorenzo Clemente and Corentin Barloy.  Bidimensional linear recursive sequences and universality of unambiguous register automata.  In STACS 2021, to appear. 2021.
  * [8] Thomas Colcombet.  Unambiguity in automata theory.  In DCFS, volume 9118 of Lecture Notes in Computer Science, pages 3–18. Springer, 2015.
  * [9] K. R. Goodearl and R. B. Warfield, Jr.  An Introduction to Noncommutative Noetherian Rings.  London Mathematical Society Student Texts. Cambridge University Press, 2 edition, 2004.
  * [10] Michael Kaminski and Nissim Francez.  Finite-Memory Automata.  Theor. Comput. Sci., 134(2):329–363, 1994.
  * [11] Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell.  On the complexity of equivalence and minimisation for q-weighted automata.  Log. Methods Comput. Sci., 9(1), 2013.
  * [12] Daniel Krob.  The equality problem for rational series with multiplicities in the tropical semiring is undecidable.  In W. Kuich, editor, Automata, Languages and Programming, pages 101–112, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg.
  * [13] Antoine Mottet and Karin Quaas.  The containment problem for unambiguous register automata.  In STACS, volume 126 of LIPIcs, pages 53:1–53:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [14] Antoine Mottet and Karin Quaas.  On the containment problem for unambiguous single-register automata with guessing.  CoRR, abs/1905.12445, 2019.
  * [15] Masakazu Nasu and Namio Honda.  Mappings induced by pgsm-mappings and some recursively unsolvable problems of finite probabilistic automata.  Information and Control, 15(3):250–273, 1969.
  * [16] Frank Neven, Thomas Schwentick, and Victor Vianu.  Finite state machines for strings over infinite alphabets.  ACM Trans. Comput. Log., 5(3):403–435, 2004.
  * [17] Marcel Paul Schützenberger.  On the definition of a family of automata.  Information and control, 4(2–3):245–270, 1961.

##  Appendix A Proof of Lemma IV.2

For item (i), let $g:W\to W/V$ be the (equivariant) quotient map. For the
“$\geq$” direction, for any chains:

$\displaystyle V_{1}\subsetneq\cdots\subsetneq V_{n}$ $\displaystyle\subsetneq
V$ ($n$ proper inclusions) $\displaystyle U_{1}\subsetneq\cdots\subsetneq
U_{m}$ $\displaystyle\subsetneq W/V$ ($m$ proper inclusions)

the chain

$V_{1}\subsetneq\cdots\subsetneq V_{n}\subsetneq V\subseteq
g^{-1}(U_{1})\subsetneq\cdots\subsetneq g^{-1}(U_{m})\subsetneq W$

has $n+m$ proper inclusions. For the “$\leq$” direction, for any chain of
proper inclusions:

$\displaystyle W_{1}\subsetneq\cdots\subsetneq W_{n}\subsetneq W$ (16)

consider chains:

$\displaystyle W_{1}\cap V$ $\displaystyle\subseteq\cdots\subseteq W_{n}\cap
V\subseteq V$ (17) $\displaystyle\overrightarrow{g}(W_{0})$
$\displaystyle\subseteq\cdots\subseteq\overrightarrow{g}(W_{n})\subseteq W/V.$
(18)

All these inclusions are not necessarily proper. However, if the $i$-th
inclusion in the first chain is an equality:

$W_{i}\cap V=W_{i+1}\cap V$

then there is some $v\in W_{i+1}\setminus W_{i}$ such that $v\not\in V$. Since
$V$ is the kernel of $g$, the $i$-th inclusion in the second chain is then
proper:

$\overrightarrow{g}(W_{i})\subsetneq\overrightarrow{g}(W_{i+1}),$

so the length of (16) does not exceed the sum of lengths of (17) and (18).

For item (ii), apply item (i) to $W=\operatorname{\mathsf{Lin}}(P+Q)$ and
$V=\operatorname{\mathsf{Lin}}P$, noting that then
$W/V=\operatorname{\mathsf{Lin}}Q$.

For item (iii), assume an equivariant surjection $q:P\to Q$, let
$\bar{q}:\operatorname{\mathsf{Lin}}P\to\operatorname{\mathsf{Lin}}Q$ be the
unique linear extension of $q$, and apply item (i) to $W=P$ and
$V=\ker(\bar{q})$, noting that then $W/V=\operatorname{\mathsf{Lin}}Q$.

##  Appendix B Proof of Claim IV.7

Recall that a vector is in $B$ iff it satisfies all the conditions (8). Since
we consider vectors in $\operatorname{\mathsf{Lin}}{T\choose k}$, only
conditions (8) with $S\in{T\choose k-1}$ matter. There are $k\cdot{n\choose
k-1}$ such conditions, and each of them takes the form of a linear equation
over $n\choose k$ variables, with all coefficients equal to $1$.

$B\cap\operatorname{\mathsf{Lin}}{T\choose k}$ is therefore the null space of
a $0$-$1$ matrix with $n\choose k$ columns and $k\cdot{n\choose k-1}$ rows,
where columns correspond to subsets of $T$ of size $k$, and rows correspond to
conditions (8). We will denote this matrix by $\mathbf{M}^{n}_{k}$. By the
rank-nullity theorem, it is enough to prove that

$\textstyle\mathrm{rank}(\mathbf{M}^{n}_{k})\geq{n\choose k}-{n-k\choose k}.$

The matrix $\mathbf{M}^{n}_{k}$ is naturally divided into $k$ equally sized
parts:

$\displaystyle\mathbf{M}^{n}_{k}=\left[\begin{array}[]{c}{}^{0}\mathbf{M}^{n}_{k}\\\
\hline\cr{}^{1}\mathbf{M}^{n}_{k}\\\ \hline\cr\vdots\\\
\hline\cr{}^{k-1}\mathbf{M}^{n}_{k}\end{array}\right]$ (23)

where each ${}^{i}\mathbf{M}^{n}_{k}$ stores conditions that concern the
$i$-th orbits in the order shown in (9). Each ${}^{i}\mathbf{M}^{n}_{k}$ has
$n\choose k-1$ rows and $n\choose k$ columns. The precise definition of the
matrix ${}^{i}\mathbf{M}^{n}_{k}$ is that:

  * •

its columns are indexed by subsets $R\in{T\choose k}$;

  * •

its rows are indexed by subsets $S\in{T\choose k-1}$;

  * •

the entry $({}^{i}\mathbf{M}^{n}_{k})_{S,R}$ is equal to $1$ if
$R=S\cup\\{a\\}$ for some atom $a\in T$ that is strictly greater than exactly
$i$ atoms in $R$; and it is $0$ otherwise.

We will look at these component matrices more closely now. Let us begin with
$i=0$. Let $a$ be the smallest atom in $T$. Arrange both the columns and the
rows of ${}^{0}\mathbf{M}^{n}_{k}$ so that they are lexicographically ordered.
Then the first $n-1\choose k-1$ columns and the first $n-1\choose k-2$ rows
correspond to subsets of $T$ that contain $a$, and the remaining $n-1\choose
k$ columns and $n-1\choose k-1$ rows correspond to subsets that do not contain
$a$. We thus identify four parts of ${}^{0}\mathbf{M}^{n}_{k}$:

$\displaystyle{}^{0}\mathbf{M}^{n}_{k}=\left[\begin{array}[]{c|c}A&B\\\
\hline\cr C&D\end{array}\right].$ (26)

Notice that $C$ is a square matrix.

Looking at the definition of ${}^{0}\mathbf{M}^{n}_{k}$, we get that:

  * •

$A$ and $B$ are zero matrices;

  * •

$C$ is the identity matrix of order $n-1\choose k-1$,

  * •

$D$ is equal to the matrix ${}^{0}\mathbf{M}^{n-1}_{k}$.

Altogether we obtain:

${}^{0}\mathbf{M}^{n}_{k}=\left[\begin{array}[]{c|c}{\bf 0}&{\bf 0}\\\
\hline\cr{\bf I}&{}^{0}\mathbf{M}^{n-1}_{k}\end{array}\right].$

Now consider $0<i<k$. Still focusing on $a$ the smallest atom in $T$, arrange
rows and columns of ${}^{i}\mathbf{M}^{n}_{k}$ as before to obtain a
decomposition as in (26). Looking at the definition of
${}^{i}\mathbf{M}^{n}_{k}$, this time we get that:

  * •

$A$ is equal to the matrix ${}^{i-1}\mathbf{M}^{n-1}_{k-1}$,

  * •

$B$ and $C$ are zero matrices,

  * •

$D$ is equal to the matrix ${}^{i}\mathbf{M}^{n-1}_{k}$.

Altogether we obtain:

$\displaystyle{}^{i}\mathbf{M}^{n}_{k}=\left[\begin{array}[]{c|c}{}^{i-1}\mathbf{M}^{n-1}_{k-1}&{\bf
0}\\\ \hline\cr{\bf 0}&{}^{i}\mathbf{M}^{n-1}_{k}\end{array}\right].$ (29)

Note that we applied the same arrangement of columns for all $i$. Coming back
to (23), we therefore obtain:

$\displaystyle\mathbf{M}^{n}_{k}=\left[\begin{array}[]{c|c}{\bf 0}&{\bf 0}\\\
\hline\cr{\bf I}&{}^{0}\mathbf{M}^{n-1}_{k}\\\
\hline\cr{}^{0}\mathbf{M}^{n-1}_{k-1}&{\bf 0}\\\ \hline\cr{\bf
0}&{}^{1}\mathbf{M}^{n-1}_{k}\\\ \hline\cr{}^{1}\mathbf{M}^{n-1}_{k-1}&{\bf
0}\\\ \hline\cr{\bf 0}&{}^{2}\mathbf{M}^{n-1}_{k}\\\ \hline\cr\vdots&\vdots\\\
\hline\cr{}^{k-2}\mathbf{M}^{n-1}_{k-1}&{\bf 0}\\\ \hline\cr{\bf
0}&{}^{k-1}\mathbf{M}^{n-1}_{k}\end{array}\right]$

Applying some rearrangement of rows, and removing some zero rows, we obtain:

$\displaystyle\mathrm{rank}(\mathbf{M}^{n}_{k})=\mathrm{rank}\left[\begin{array}[]{c|c}{}^{0}\mathbf{M}^{n-1}_{k-1}&{\bf
0}\\\ \hline\cr{}^{1}\mathbf{M}^{n-1}_{k-1}&{\bf 0}\\\
\hline\cr\vdots&\vdots\\\ \hline\cr{}^{k-2}\mathbf{M}^{n-1}_{k-1}&{\bf 0}\\\
\hline\cr{\bf I}&{}^{0}\mathbf{M}^{n-1}_{k}\\\ \hline\cr{\bf
0}&{}^{1}\mathbf{M}^{n-1}_{k}\\\ \hline\cr{\bf
0}&{}^{2}\mathbf{M}^{n-1}_{k}\\\ \hline\cr\vdots&\vdots\\\ \hline\cr{\bf
0}&{}^{k-1}\mathbf{M}^{n-1}_{k}\end{array}\right]$ (39)

Now we use the general fact that

$\mathrm{rank}\left[\begin{array}[]{c|c}A&B\\\ \hline\cr{\bf
0}&C\end{array}\right]\geq\mathrm{rank}(A)+\mathrm{rank}(C)$

to conclude

$\displaystyle\mathrm{rank}(\mathbf{M}^{n}_{k})\geq\mathrm{rank}\left[\begin{array}[]{c}{}^{0}\mathbf{M}^{n-1}_{k-1}\\\
\hline\cr{}^{1}\mathbf{M}^{n-1}_{k-1}\\\ \hline\cr\vdots\\\
\hline\cr{}^{k-2}\mathbf{M}^{n-1}_{k-1}\\\ \hline\cr{\bf
I}\end{array}\right]+\mathrm{rank}\left[\begin{array}[]{c}{}^{1}\mathbf{M}^{n-1}_{k}\\\
\hline\cr{}^{2}\mathbf{M}^{n-1}_{k}\\\ \hline\cr\vdots\\\
\hline\cr{}^{k-1}\mathbf{M}^{n-1}_{k}\end{array}\right].$ (49)

Thanks to the identity component, the first summand above equals ${n-1\choose
k-1}$. Let us now calculate the rank:

$R^{n}_{k}=\mathrm{rank}\left[\begin{array}[]{c}{}^{1}\mathbf{M}^{n}_{k}\\\
\hline\cr{}^{2}\mathbf{M}^{n}_{k}\\\ \hline\cr\vdots\\\
\hline\cr{}^{k-1}\mathbf{M}^{n}_{k}\end{array}\right].$

This is similar to the matrix $\mathbf{M}^{n}_{k}$, but without the $0$’th
component. Use (29) again and rearrange rows to obtain:

$\displaystyle
R^{n}_{k}\\!=\\!\mathrm{rank}\\!\\!\left[\begin{array}[]{c|c}{}^{0}\mathbf{M}^{n-1}_{k-1}&{\bf
0}\\\ \hline\cr{}^{1}\mathbf{M}^{n-1}_{k-1}&{\bf 0}\\\
\hline\cr\vdots&\vdots\\\ \hline\cr{}^{k-2}\mathbf{M}^{n-1}_{k-1}&{\bf 0}\\\
\hline\cr{\bf 0}&{}^{1}\mathbf{M}^{n-1}_{k}\\\ \hline\cr{\bf
0}&{}^{2}\mathbf{M}^{n-1}_{k}\\\ \hline\cr\vdots&\vdots\\\ \hline\cr{\bf
0}&{}^{k-1}\mathbf{M}^{n-1}_{k}\end{array}\right]\\!\\!=\\!\mathrm{rank}(\mathbf{M}^{n-1}_{k-1})\\!+\\!R^{n-1}_{k}.$

This entails

$R^{n}_{k}=\textstyle\sum_{m=k-1}^{n-1}\mathrm{rank}(\mathbf{M}^{m}_{k-1}).$

Combining this with (49) we obtain:

$\displaystyle\textstyle\mathrm{rank}(\mathbf{M}^{n}_{k})\\!\geq\\!{n-1\choose
k-1}+R^{n-1}_{k}\\!=\\!{n-1\choose
k-1}+\sum_{m=k-1}^{n-2}\mathrm{rank}(\mathbf{M}^{m}_{k-1}).$ (50)

There is also the base case $\mathrm{rank}(\mathbf{M}^{k}_{k})=1$ since the
matrix $\mathbf{M}^{k}_{k}$ has only one column (and $k$ nonzero rows).
Another base case is $\mathrm{rank}(\mathbf{M}^{n}_{1})=1$, since the matrix
$\mathbf{M}^{n}_{1}$ has only one row (filled with $n$ ones). Denote
$S^{n}_{k}=\mathrm{rank}(\mathbf{M}^{n}_{k})$ and pretend that the inequality
in (50) is an equality; we then obtain the recurrence:

$\displaystyle S^{k}_{k}$ $\displaystyle=1$ $\displaystyle S^{n}_{1}$
$\displaystyle=1$ $\displaystyle S^{n}_{k}$
$\displaystyle=\textstyle{n-1\choose
k-1}+\sum_{m=k-1}^{n-2}S^{m}_{k-1}\quad\text{for }n>k>1.$

The formula

$S^{n}_{k}=\textstyle{n\choose k}-{n-k\choose k}$

satisfies the recurrence. Indeed, calculate:

$\displaystyle\textstyle{n-1\choose k-1}+\sum_{m=k-1}^{n-2}\left({m\choose
k-1}-{m-k+1\choose k-1}\right)=$ $\displaystyle\textstyle={n-1\choose
k-1}+\sum_{m=n-k}^{n-2}{m\choose k-1}=$
$\displaystyle\textstyle=\sum_{m=n-k}^{n-1}{m\choose k-1}={n\choose
k}-{n-k\choose k},$

where the last equality follows from a repeated application of Pascal’s rule:

$\textstyle{m\choose k-1}+{m\choose k}={m+1\choose k}.$

This proves that $S^{n}_{k}\geq{n\choose k}-{n-k\choose k}$ and completes the
proof of Claim IV.7.

##  Appendix C Proof of Lemma IV.10

Define the $\bar{a}$-length of a vector space to be the maximal length of
$\bar{a}$-supported subspaces. In the special case when $\bar{a}$ is the empty
tuple, we get the notion of length from Definition IV.1. Every
$\bar{a}$-supported orbit-finite set can be obtained, using images under
$\bar{a}$-supported functions and disjoint unions, from $\bar{a}$-orbits
contained in $\mathbb{A}^{k}$. Since Lemma IV.2 holds, with the same proof,
for $\bar{a}$-length, it remains to show that the $\bar{a}$-length is finite
for $\operatorname{\mathsf{Lin}}Q$ when $Q$ is a single $\bar{a}$-orbit
contained in $\mathbb{A}^{k}$. We now split into two proofs, depending on
whether we deal with the equality or ordered atoms.

  * •

_Equality atoms._ Choose some bijection

$\displaystyle
f:\underbrace{(\mathbb{A}-\bar{a})}_{\mathclap{\hbox{\hbox{\kern
0.0pt\raise-5.94998pt\vbox{\halign{\relax\hfil\txtline@@{#}\hfil\cr\hbox{{\ignorespaces\leavevmode\scriptsize
atoms that do }\\\\\hbox{{\ignorespaces\scriptsize not appear in
$\bar{a}$}\crcr}}}}}}\to\mathbb{A},}}$

which is possible since both sets are countably infinite. (Note that $f$
cannot be finitely supported.) Let $\ell\in\\{1,\ldots,k\\}$ be the number of
coordinates that are not from $\bar{a}$ in some (equivalently, every) tuple
from the $\bar{a}$-orbit $Q$. We can lift $f$ to an injective function (in
fact, a bijection)

$\displaystyle g:Q\to\mathbb{A}^{(\ell)},$

which erases the coordinates that use atoms from $\bar{a}$ and applies $f$ to
the remaining coordinates. One can easily see that

$\displaystyle\operatorname{\mathsf{Lin}}g:\operatorname{\mathsf{Lin}}Q\to\operatorname{\mathsf{Lin}}\mathbb{A}^{(\ell)}$

maps $\bar{a}$-supported subspaces of $\operatorname{\mathsf{Lin}}Q$ to
equivariant subspaces of $\operatorname{\mathsf{Lin}}\mathbb{A}^{(\ell)}$, and
preserves strict inclusions. Therefore the $\bar{a}$-length of
$\operatorname{\mathsf{Lin}}Q$ is at most the (equivariant) length of
$\operatorname{\mathsf{Lin}}\mathbb{A}^{(\ell)}$, and the latter length is
finite by Lemma IV.9.

  * •

_Ordered atoms._ Let the atoms in $\bar{a}$ be

$\displaystyle a_{1}<\cdots<a_{n}.$

For every $i\in\\{0,1,\ldots,n\\}$, consider the interval

$\displaystyle\mathbb{A}_{i}=\\{a:a_{i}<a<a_{i+1}\\},$

where $a_{0}$ is $-\infty$ and $a_{n+1}$ is $\infty$. Choose some order-
preserving bijection

$\displaystyle f_{i}:\mathbb{A}_{i}\to\mathbb{A}.$

As in the previous item, let $\ell$ be the coordinates from $Q$ which avoid
atoms from $\bar{a}$. By erasing the coordinates which use atoms from
$\bar{a}$, and applying the appropriate functions $f_{i}$ to the remaining
coordinates, we get an injective function

$\displaystyle g:Q\to\mathbb{A}^{\ell}.$

Since the functions $f_{i}$ all have the same co-domain, namely $\mathbb{A}$,
the image of the function will contain tuples that are not necessarily
strictly increasing. Nevertheless, the linear lifting

$\displaystyle
g:\operatorname{\mathsf{Lin}}Q\to\operatorname{\mathsf{Lin}}\mathbb{A}^{\ell}$

maps $\bar{a}$-supported subspaces in $\operatorname{\mathsf{Lin}}Q$ to
equivariant subspaces in $\operatorname{\mathsf{Lin}}\mathbb{A}^{\ell}$, and
hence we obtain a finite bound on $\bar{a}$-supported chains in
$\operatorname{\mathsf{Lin}}Q$.

##  Appendix D Equivalence of linear and weighted automata

We begin with the easier inclusion.

###### Lemma D.1

For every weighted orbit-finite automaton ${\mathcal{W}}$ there is an orbit-
finitely spanned automaton ${\mathcal{L}}$ which recognizes the same weighted
language.

###### Proof.

If $Q$ are the states of ${\mathcal{W}}$, then the vector space of
${\mathcal{L}}$ is $\operatorname{\mathsf{Lin}}Q$, and the transition function

$\displaystyle\delta:\operatorname{\mathsf{Lin}}Q\times\mathbb{A}\to\operatorname{\mathsf{Lin}}Q$

is defined so that for every input letter $a\in\Sigma$ and states $q,p\in Q$
(which are basis vectors of the vector space $\operatorname{\mathsf{Lin}}Q$),
the coefficient for state $p$ in the vector $\delta(q,a)$ is the weight of the
transition $(q,a,p)$. In other words, linear map $\delta(\\_,a)$ is defined by
a $Q\times Q$ matrix where the coefficient in cell $(q,p)$ is the weight of
the transition $(q,a,p)$. Note how condition (*) from Definition III.1 is used
to ensure that the $\delta(q,a)$ is a well-defined vector, in the sense that
it has finitely many nonzero coordinates. The initial vector of
${\mathcal{L}}$ consists of the initial weights in ${\mathcal{W}}$, and the
final function is the linear extension of the original final weight function.
∎

Example 11.  Recall the weighted orbit-finite automaton from Example VII. We
have already described the state space of the corresponding orbit-finitely
spanned automaton:

$V\ =\
{\color[rgb]{0,0,1}\operatorname{\mathsf{Lin}}(\,\\{\bot,\top\\}+\mathbb{A}\,)}\
\oplus\ {\color[rgb]{1,0,0}X},$

and we will now define the rest od it. We define the transition function on
the generators of the state space:

$\displaystyle\delta({\color[rgb]{0,0,1}\bot},a)={\color[rgb]{0,0,1}a}\quad\delta({\color[rgb]{0,0,1}\top},a)=0\quad\delta({\color[rgb]{0,0,1}a},b)={\color[rgb]{1,0,0}(a,b)-(b,a)}$
$\displaystyle\delta({\color[rgb]{1,0,0}(a,b)-(b,a)},c)=\begin{cases}{\color[rgb]{0,0,1}\top}&\text{if
$c=a$,}\\\ {\color[rgb]{0,0,1}-\top}&\text{if $c=b$,}\\\
0&\text{otherwise.}\end{cases}$

Formally, one has to show that $\delta$ is well-defined on
${\color[rgb]{1,0,0}X}$, i.e. it satisfies
$\delta({\color[rgb]{1,0,0}(a,b)-(b,a)},c)=-\delta({\color[rgb]{1,0,0}(b,a)-(a,b)},c)$.
Similarly for the final function, we define it for generators:

$F({\color[rgb]{0,0,1}\bot})=0\quad F({\color[rgb]{0,0,1}\top})=1\quad
F({\color[rgb]{0,0,1}a})=0\quad F({\color[rgb]{1,0,0}(a,b)-(b,a)})=0.$

The initial vector is simply $v_{0}={\color[rgb]{0,0,1}\bot}$. This automaton
accepts the same language $L$ and is in fact minimal. $\Box$

Call an orbit-finitely spanned automaton basic if its state vector space has a
basis. For a basic automaton an equivalent weighted orbit-finite automaton can
be easily produced, by using the basis as the states. Therefore, to complete
the proof of Theorem VII.2, we prove the following:

###### Lemma D.2

For every orbit-finitely spanned automaton, there is a basic one that
recognizes the same weighted language.

###### Proof.

Consider an orbit-finitely spanned automaton ${\mathcal{A}}$ with a state
space $V$ is spanned by an orbit-finite set $Q$. Define a _polynomial orbit-
finite set_ , see [6, Definition 1], to be any set which is a finite disjoint
union of sets of the form $\mathbb{A}^{k}$. As for every orbit-finite set,
there exists a polynomial orbit-finite set $P$ with a surjective finitely
supported function from $P$ to $Q$. Extend this function to surjective a
linear map

$\displaystyle h:\operatorname{\mathsf{Lin}}P\to V.$

We will define a orbit-finitely spanned automaton ${\mathcal{B}}$ with vector
space $\operatorname{\mathsf{Lin}}P$ so that $h$ becomes a homomorphism of
orbit-finitely spanned automata, that is: a finitely supported linear map
between the underlying vector spaces, which is consistent with the initial
states, transition functions and final functions in the expected way, see [3,
Sec. 6.2]. If two orbit-finitely spanned automata are connected by a
homomorphism, then they recognize the same weighted language. Therefore, to
prove the lemma it remains to define the initial state, transition function
and final function in ${\mathcal{B}}$ so that $h$ is a homomorphism.

For the initial state in ${\mathcal{B}}$ we choose some vector that is mapped
by $h$ to the initial state of ${\mathcal{A}}$, and for the final function we
use the composition of $h$ and the final function of ${\mathcal{A}}$. The
transition function is defined using the following claim.

###### Claim D.3

There is a finitely supported function $\gamma$ which makes the following
diagram commute

###### Proof.

Consider the composition of the following relations: the function $(h,id)$,
the transition function of ${\mathcal{A}}$, and the inverse of $h$. This is a
finitely supported binary relation

$\displaystyle R\subseteq(P\times\Sigma)\times\operatorname{\mathsf{Lin}}P$

such that every element of $P\times\Sigma$ is related with at least one
element of $\operatorname{\mathsf{Lin}}P$ (thanks to the surjectivity of $h$).
By the Uniformization Lemma from [6, Lemma 20], there exists a finitely
supported function $\gamma$ which is contained in $R$, thus proving the lemma.
It is worth pointing out that the Uniformization Lemma changes supports: even
if $R$ is equivariant, it could be the case that $\gamma$ needs non-empty
support. ∎

Extend, using linearity, the function $\gamma$ from the claim to a finitely
supported function

$\displaystyle\bar{\gamma}:\operatorname{\mathsf{Lin}}P\times\Sigma\to\operatorname{\mathsf{Lin}}P$

which is a linear map for every fixed input letter; the resulting function can
then be used as the transition function for ${\mathcal{B}}$. The commuting
diagram in the claim ensures that $h$ is a homomorphism. ∎