[1] #1= [1] #1≤ [1] #1≥ [1] *#1 != !≤ * $(*)$= $(*)$≤ $(*)$≥ [1]*=$(#1)$
[1]*≤$(#1)$ [1]*≥$(#1)$

11institutetext: RWTH Aachen University, Germany
11email<EMAIL_ADDRESS>

# Computing Least and Greatest Fixed Points
in Absorptive Semirings

Matthias Naaf

###### Abstract

We present two methods to algorithmically compute both least and greatest
solutions of polynomial equation systems over absorptive semirings (with
certain completeness and continuity assumptions), such as the tropical
semiring. Both methods require a polynomial number of semiring operations,
including semiring addition, multiplication and an infinitary power operation.

Our main result is a closed-form solution for least and greatest fixed points
based on the fixed-point iteration. The proof builds on the notion of
(possibly infinite) derivation trees; a careful analysis of the shape of these
trees allows us to collapse the fixed-point iteration to a linear number of
steps. The second method is an iterative symbolic computation in the semiring
of generalized absorptive polynomials, largely based on results on Kleene
algebras.

###### Keywords:

Fixed-Point Computation, Absorptive Semirings, Semiring Provenance

##  1 Introduction

A recent line of research on semiring provenance analysis for databases [12,
5, 13], logic [10, 4] and games [11] has identified the class of absorptive,
commutative semirings as an appropriate domain for provenance semantics of
fixed-point logics [4] and games with fixed-point semantics, such as Büchi or
parity games. The underlying idea is to replace the Boolean evaluation of
formulae by computations in certain semirings. From this point of view, a
formula is essentially a polynomial expression over some semiring, and fixed-
point formulae evaluate to least or greatest solutions of polynomial equation
systems. To guarantee the existence and meaningfulness (when interpreted as
provenance information) of these fixed points, one assumes that the semiring
is equipped with a natural order that is a complete lattice (for the
existence) and that the semiring is absorptive, that is, $1+a=1$ for all
elements $a$. Absorption guarantees a duality of the semiring operations in
the sense that addition is increasing, with least element $0$, while
multiplication is decreasing, with greatest element $1$, and it is this
property that leads to meaningful provenance information of greatest fixed
points [4].

This raises the question how one can (efficiently) compute least and greatest
solutions of polynomial equation systems over such semirings. The textbook
approach is the fixed-point iteration: start by setting all indeterminates to
the smallest (or greatest) semiring value, then repeatedly evaluate the
equations to obtain new values for all indeterminates. In the Boolean setting,
this terminates in at most $n$ steps on $n$ indeterminates (due to
monotonicity), but we are also interested in larger and especially infinite
semirings such as the tropical semiring111We use $+_{\mathbb{R}}$ for the
addition on $\mathbb{R}$ to distinguish it from the semiring operation $+$.
$\mathbb{T}=(\mathbb{R}_{\\_}{\geq
0}\cup\\{\infty\\},\min,+_{\mathbb{R}},\infty,0)$. Several techniques have
been developed to compute least solutions. For $\omega$-continuous semirings
(where suprema exist and are compatible with the semiring operations), Hopkins
and Kozen [15] have defined a faster iteration scheme based on differentials
and more recently, Esparza, Kiefer and Luttenberger [6] have used this idea to
generalize Newton’s method to $\omega$-continuous semirings. This works
surprisingly well for a wide variety of semirings (in fact, their results for
idempotent semirings subsume our result for least fixed points). Gondran and
Minoux [8] use quasi-inverses of elements and matrices to compute least
solutions of linear systems and univariate polynomial equations over dioids.
This applies to absorptive semirings, where elements have the trivial quasi-
inverse $a^{*}=1$ and hence quasi-inverses of matrices always exist.

Our goal is to complement the results in [15, 6] by also computing _greatest_
solutions, as our motivation stems from semiring provenance where both least
and greatest fixed points are considered. To this end, we work with
absorptive, _fully_ continuous semirings (requiring continuity for both
suprema and infima).

Example. Consider the following graph whose edges are annotated by cost values
in the tropical semiring. A natural example of a greatest fixed point is the
minimal cost of an infinite path. This corresponds to the greatest solution of
the equation system given on the right, where each node is represented by an
indeterminate and costs appear as coefficients (notice that the right-hand
sides are indeed polynomial expressions in terms of the semiring operations).

$a$$b$$c$$1$$0$$1$$20$

$\begin{aligned} X_{\\_}a&=1+_{\mathbb{R}}X_{\\_}a\\\
X_{\\_}b&=\min(1+_{\mathbb{R}}X_{\\_}a,20+_{\mathbb{R}}X_{\\_}c)\\\
X_{\\_}c&=0+_{\mathbb{R}}X_{\\_}c\end{aligned}$

When we speak of _least_ or _greatest_ solutions, we always refer to the
natural order of the semiring. In the case of the tropical semiring, this is
the inverse of the standard order, so
$\infty<_{\\_}\mathbb{T}20<_{\\_}\mathbb{T}1<_{\\_}\mathbb{T}0$. While the
least solution of the above system is trivially
$X_{\\_}a=X_{\\_}b=X_{\\_}c=\infty$, the fixed-point iteration for the
greatest solution is infinite:

${\scriptsize\begin{pmatrix}0\\\ 0\\\
0\end{pmatrix}}\mapsto{\scriptsize\begin{pmatrix}1\\\ 1\\\
0\end{pmatrix}}\mapsto{\scriptsize\begin{pmatrix}2\\\ 2\\\
0\end{pmatrix}}\mapsto{\scriptsize\begin{pmatrix}3\\\ 3\\\
0\end{pmatrix}}\mapsto\cdots\mapsto{\scriptsize\begin{pmatrix}20\\\ 20\\\
0\end{pmatrix}}\mapsto{\scriptsize\begin{pmatrix}21\\\ 20\\\
0\end{pmatrix}}\mapsto{\scriptsize\begin{pmatrix}22\\\ 20\\\
0\end{pmatrix}}\mapsto{\scriptsize\begin{pmatrix}23\\\ 20\\\
0\end{pmatrix}}\mapsto\cdots$

and converges to the greatest solution: $X_{\\_}a=\infty$, $X_{\\_}b=20$ and
$X_{\\_}c=0$.

Main Result. The essential idea to compute such solutions is that greatest
fixed points are composed of two parts: a cyclic part that is repeated
indefinitely (the loop at $a$ or $c$) and a reachability part to get to the
cycle (the edges from $b$). As both parts can consist of at most $n$ nodes,
all information we need is already present after $n$ steps of the fixed-point
iteration; we can use this information to abbreviate the iteration. The formal
proof of this observation is based on (infinite) derivation trees, inspired by
the derivation trees in the analysis of Newton’s method [6] and infinite
strategy trees in [4]. We show that these trees provide an alternative
description of the fixed-point iteration; a careful analysis of the shape of
the derivation trees then leads to our main result:

###### Theorem 1.1

Let $F$ be the operator induced by a polynomial equation system in $n$
indeterminates over an absorptive, fully-continuous, commutative semiring. We
can compute in a polynomial number of semiring operations:

  * •

the least solution: $F^{n}(\mathbf{0})$,

  * •

the greatest solution: $F^{n}(\,F^{n}(\mathbf{1})^{\infty}\,)$.

Here, $a^{\infty}$ is the _infinitary power_ operation
$a^{\infty}\coloneqq\bigsqcap_{\\_}{n\in\mathbb{N}}a^{n}$ which is well-
defined (and usually easy to compute) in the absorptive semirings we consider.
For instance, in the tropical semiring we have $0^{\infty}=0$ and
$a^{\infty}=\infty$ for $a\neq 0$.

Symbolic Approach. Our second approach is a technique to eliminate
indeterminates one by one, based on the work of Hopkins and Kozen on Kleene
algebras [15]. We apply their symbolic approach to the semiring
${\mathbb{S}}^{\infty}[{\bm{X}}]$ of generalized absorptive polynomials, which
is perhaps the most relevant semiring for provenance analysis with fixed
points, and extend it to include greatest solutions.

Outline. This paper is structured as follows: Section 2 introduces the problem
setting, in particular the relevant class of semirings, as well as derivation
trees. Section 3 establishes the connection between derivation trees and the
fixed-point iteration, and Section 4 builds on this concept to prove our main
result. The symbolic approach for absorptive polynomials is discussed in
Section 5. There are two appendices: Appendix A contains few auxiliary proofs
and Appendix B discusses an axiomatization of the infinitary power operation.

##  2 Preliminaries

This section introduces polynomial equation systems, gives an overview on the
semirings we are interested in and introduces the notion of derivation trees.

###  2.1 Polynomial Equation Systems

Throughout the paper, we always fix a finite set
${\bm{X}}=\\{X_{\\_}1,\dots,X_{\\_}\ell\\}$ of $\ell$ pairwise different
indeterminates. A monomial over ${\bm{X}}$ is a product of powers of
indeterminates, represented as mapping $m\colon{\bm{X}}\to\mathbb{N}$
assigning exponents to the indeterminates.

We use bold symbols to denote tuples:
$\mathbf{a}=(a_{\\_}1,\dots,a_{\\_}\ell)$. In particular,
$\mathbf{0}=(0,\dots,0)$ and $\mathbf{1}=(1,\dots,1)$. To simplify the
presentation, we often avoid numbered indices. Given
${\bm{X}}=\\{X_{\\_}1,\dots,X_{\\_}\ell\\}$, we instead index tuples by these
indeterminates. That is, for a tuple $\mathbf{a}=(a_{\\_}1,\dots,a_{\\_}\ell)$
and an indeterminate $X\in{\bm{X}}$, we write $\mathbf{a}_{\\_}X$ for the
entry $a_{\\_}i$ such that $X_{\\_}i=X$.

###### Definition 1

A _polynomial_ $P$ over a semiring $(K,+,\cdot,0,1)$ and indeterminates
${\bm{X}}$ is a finite formal sum of the form
$P=\sum_{\\_}{i=1}^{k}c_{\\_}i\cdot m_{\\_}i$, where the $m_{\\_}i$ are
pairwise different monomials over ${\bm{X}}$ and $c_{\\_}i\in
K\setminus\\{0\\}$ are arbitrary coefficients.

Abusing notation, we write $m\in P$ if there is an $i$ with $m=m_{\\_}i$, and
$c\cdot m\in P$ if additionally $c=c_{\\_}i$. We may write
$P(X_{\\_}1,\dots,X_{\\_}\ell)$ to make the indeterminates explicit. Then,
$P(a_{\\_}1,\dots,a_{\\_}\ell)\in K$ is the semiring value obtained by
instantiating each indeterminate $X_{\\_}i$ by $a_{\\_}i\in K$ and evaluating
the resulting expression in $K$.

###### Definition 2

A _polynomial equation system_ $\mathcal{E}$ over a semiring $K$ and
indeterminates ${\bm{X}}=\\{X_{\\_}1,\dots,X_{\\_}\ell\\}$ is a family of
equations
$\mathcal{E}\colon\big{(}X_{\\_}i=P_{\\_}i(X_{\\_}1,\dots,X_{\\_}\ell)\big{)}_{\\_}{1\leq
i\leq\ell}$ with polynomials $P_{\\_}i$ over ${\bm{X}}$ and $K$.

We associate with $\mathcal{E}$ the operator $F_{\\_}\mathcal{E}\colon
K^{\ell}\to K^{\ell}$ defined by
$F_{\\_}\mathcal{E}(a_{\\_}1,\dots,a_{\\_}\ell)_{\\_}X=P_{\\_}X(a_{\\_}1,\dots,a_{\\_}\ell)$,
for $X\in{\bm{X}}$. The least (greatest) solution to $\mathcal{E}$ is thus the
least (greatest) fixed point of $F_{\\_}\mathcal{E}$. We drop the index if
$\mathcal{E}$ is clear from the context.

Notice that these are quadratic systems, with the number of equations equal to
the number of indeterminates. We recall the example from the introduction in
the tropical semiring (where semiring addition is $\min$ and semiring
multiplication is $+_{\mathbb{R}}$). Using
${\bm{X}}=\\{X_{\\_}a,X_{\\_}b,X_{\\_}c\\}$, we refer to the polynomial
equation system as $(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$. For example,
$P_{\\_}{X_{\\_}b}$ is the polynomial
$\min(1+_{\mathbb{R}}X_{\\_}a,20+_{\mathbb{R}}X_{\\_}c)$ consisting of the two
coefficient-monomial pairs $1+_{\mathbb{R}}X_{\\_}a$ and
$20+_{\mathbb{R}}X_{\\_}c$.

###  2.2 Semirings

###### Definition 3

A (commutative) _semiring_ is an algebraic structure $(K,+,\cdot,0,1)$, with
$0\neq 1$, such that $(K,+,0)$ and $(K,\cdot,1)$ are commutative monoids,
$\cdot$ distributes over $+$, and $0\cdot a=a\cdot 0=0$. It is _idempotent_ if
$a+a=a$ and _absorptive_ if $1+a=1$, for all $a\in K$.

In an idempotent semiring $K$, the _natural order_ $\leq_{\\_}K$ is the
partial order with $a\leq_{\\_}Kb$ if $a+b=b$, for $a,b\in K$. We drop the
index if $K$ is clear from the context.

All semirings considered in this paper are commutative and absorptive (except
for ${\mathbb{N}}^{\infty}$ below). Absorption (also called _0-closed_ or
_bounded_ [18]) implies idempotence and is equivalent to $1$ being the
$\leq_{\\_}K$-maximal element and to multiplication being decreasing, i.e.,
$ab\leq_{\\_}Ka$ for all $a,b\in K$ (dually to increasing addition).

To guarantee the existence of fixed points, we further require that the
natural order is a complete lattice so that suprema $\bigsqcup$ and infima
$\bigsqcap$ always exist (with respect to $\leq_{\\_}K$). In addition, we make
a continuity assumption stating that the semiring operations commute with the
lattice operations on chains (a chain is a totally ordered set). This is
crucial for most of our proofs, but does not seem to be a strong restriction
in practice: all natural examples of complete-lattice semirings we are aware
of are in fact also fully continuous (a notable exception are binary relations
with union and composition, but the latter is not commutative).

###### Definition 4

An idempotent semiring $K$ is _fully continuous_ if $\leq_{\\_}K$ is a
complete lattice and for all $a\in K$, all nonempty chains $C\subseteq K$ and
$\circ\in\\{+,\cdot\\}$,

$\bigsqcup(a\circ C)=a\circ\bigsqcup C\quad\text{and}\quad\bigsqcap(a\circ
C)=a\circ\bigsqcap C.$

A homomorphism $h\colon K_{\\_}1\to K_{\\_}2$ on fully-continuous semirings is
_fully continuous_ if $h(\bigsqcup C)=\bigsqcup h(C)$ and $h(\bigsqcap
C)=\bigsqcap h(C)$, for all nonempty chains $C\subseteq K_{\\_}1$.

###### Remark 1

We note that requiring suprema and infima of chains in fact suffices to
guarantee the existence of fixed points. However, in idempotent semirings this
already implies the existence of arbitrary suprema and infima [4] and is thus
equivalent to our assumption of a complete lattice. For continuity, the
situation is more complicated: compatibility of $+$ and $\cdot$ with suprema
of chains implies compatibility with arbitrary suprema (see Appendix 0.A), but
the same does, in general, not hold for infima.

Following the above remark, we see that fully-continuous semirings are similar
to quantales. Indeed, since multiplication is compatible with suprema of
arbitrary sets, every absorptive, fully-continuous semiring $K$ induces a
quantale $(K,\bigsqcup,\cdot)$ with the top element $1$ as unit. The main
difference to quantales is that we additionally require compatibility of
semiring operations with infima (but only of chains). Another related concept
is that of topological dioids in [8] which requires that both operations are
compatible with suprema of countable chains.

Since multiplication is decreasing in absorptive semirings, powers of an
element $a$ form a descending chain $1\geq a\geq a^{2}\geq\dots$ whose infimum
we denote by $a^{\infty}$.

###### Definition 5

In an absorptive, fully-continuous semiring $K$, the _infinitary power_
operation is defined by
$a^{\infty}\coloneqq\bigsqcap_{\\_}{n\in\mathbb{N}}a^{n}$, for each $a\in K$,
and
$\mathbf{a}^{\infty}\coloneqq(a_{\\_}1^{\infty},\dots,a_{\\_}\ell^{\infty})$
for tuples $\mathbf{a}\in K^{\ell}$.

Using continuity of multiplication, one can easily verify the properties
$(ab)^{\infty}=a^{\infty}b^{\infty}$, $(a^{n})^{\infty}=a^{\infty}$ and
$(a+b)^{\infty}=a^{\infty}+b^{\infty}$ (see [3] for details). We remark that
it is usually quite easy to compute the infinitary power. One can further
define infinite sum and product operations on families $(a_{\\_}i)_{\\_}{i\in
I}$ over $K$ with arbitrary index set $I$. Summation is simply defined as
supremum, products can be defined as infimum over finite subproducts (see [3,
Appendix]). Here we only need infinite products over finite domain
$\\{a_{\\_}i\mid i\in I\\}$ (as the polynomials we consider have finitely many
coefficients), which are commutative, associative and commute with fully-
continuous homomorphisms and the infinitary power.

Fully-continuous homomorphisms further preserve fixed points of monotone
functions, in particular least and greatest solutions of polynomial systems:

###### Lemma 1

Let $h\colon K_{\\_}1\to K_{\\_}2$ be a fully-continuous homomorphism on
absorptive, fully-continuous semirings. Let
$\mathcal{E}\colon(X_{\\_}i=P_{\\_}i)_{\\_}{1\leq i\leq n}$ be a polynomial
equation system over $K_{\\_}1$. Let
$h(\mathcal{E})\colon(X_{\\_}i=h(P_{\\_}i))_{\\_}{1\leq i\leq n}$ result from
$\mathcal{E}$ by applying $h$ to all coefficients. Then,
$\operatorname{\mathbf{lfp}}(F_{\\_}{h(\mathcal{E})})=h(\operatorname{\mathbf{lfp}}(F_{\\_}\mathcal{E}))$
and
$\operatorname{\mathbf{gfp}}(F_{\\_}{h(\mathcal{E})})=h(\operatorname{\mathbf{gfp}}(F_{\\_}\mathcal{E}))$.

###### Proof

Recall that the semiring operations are fully continuous in $K_{\\_}1$ and
$K_{\\_}2$. Hence $F_{\\_}\mathcal{E}$ and $F_{\\_}{h(\mathcal{E})}$ are fully
continuous as well, and by Kleene’s fixed-point Theorem and the continuity of
$h$, we get

$h(\operatorname{\mathbf{lfp}}(F_{\\_}\mathcal{E}))=h\Big{(}\bigsqcap_{\\_}{n\in\mathbb{N}}F_{\\_}{\mathcal{E}}^{n}(\mathbf{0})\Big{)}=\bigsqcap_{\\_}{n\in\mathbb{N}}h\big{(}F_{\\_}{\mathcal{E}}^{n}(\mathbf{0})\big{)}\overset{\clap{\scriptsize(*)}}{=}\bigsqcap_{\\_}{n\in\mathbb{N}}\big{(}F_{\\_}{h(\mathcal{E})}^{n}(\mathbf{0})\big{)}=\operatorname{\mathbf{lfp}}(F_{\\_}{h(\mathcal{E})}),$

where $(*)$ is easy to see by induction, since $h$ is a homomorphism and the
operators are defined by polynomials. The proof for greatest solutions is
symmetric. ∎

#### Examples.

Some examples of absorptive, fully-continuous semirings are:

  * •

The _Boolean semiring_ $\mathbb{B}=(\\{0,1\\},\vee,\wedge,0,1)$ is the habitat
of logical truth.

  * •

$\mathbb{T}=(\mathbb{R}_{\\_}{\geq 0}^{\infty},\min,+_{\mathbb{R}},\infty,0)$
is the _tropical_ semiring used for cost computations.

  * •

The _Viterbi_ semiring $\mathbb{V}=([0,1],\max,\cdot,0,1)$ is isomorphic to
$\mathbb{T}$ and can be used to model confidence scores.

  * •

The _Łukasiewicz_ semiring $\mathbb{L}=([0,1],\max,\star,0,1)$ with $a\star
b=\max(0,a+b-1)$, used in many-valued logics.

  * •

The _min-max_ semiring on a totally ordered set $(A,\leq)$ with least element
$a$ and greatest element $b$ is the semiring $(A,\max,\min,a,b)$.

  * •

The semiring of _generalized absorptive polynomials_
${\mathbb{S}}^{\infty}[{\bm{X}}]$, defined below.

We write ${\mathbb{N}}^{\infty}$ for the semiring of natural numbers extended
by a special element $\infty$ (with $n\cdot\infty=n+\infty=\infty$, for $n\neq
0$). It is neither absorptive nor idempotent (but fully continuous w.r.t the
standard order on natural numbers).

#### Absorptive Polynomials.

The most important absorptive, fully-continuous semiring, both from a
provenance perspective and for our proofs, is the semiring of _(generalized
222${\mathbb{S}}^{\infty}[{\bm{X}}]$ generalizes the semiring
$\mathrm{Sorp}({\bm{X}})$ of absorptive polynomials in [5] by adding the
exponent $\infty$ (which is needed for _fully_ -continuous homomorphisms in
Theorem 2.1). We only use ${\mathbb{S}}^{\infty}[{\bm{X}}]$ in this paper and
hence drop _generalized_ in the following.) absorptive polynomials_
${\mathbb{S}}^{\infty}[{\bm{X}}]$. We briefly summarize its definition and key
properties from [4]. Given a finite set ${\bm{X}}$ of indeterminates, a
(generalized) monomial over ${\bm{X}}$ is a mapping
$m\colon{\bm{X}}\to{\mathbb{N}}^{\infty}$ (here we also allow the exponent
$\infty$), multiplication adds exponents and the neutral element is $1\colon
X\mapsto 0$. We say that a monomial $m_{\\_}1$ _absorbs_ $m_{\\_}2$, denoted
$m_{\\_}1\succeq m_{\\_}2$, if $m_{\\_}1(X)\leq m_{\\_}2(X)$ for all
$X\in{\bm{X}}$ (notice that absorption is the _inverse_ of the pointwise order
on the exponents). In order to mimic the algebraic property of absorption,
polynomials are _antichains_ of monomials (which are always finite). Addition
and multiplication are defined as usual, but we drop monomials that are
absorbed after each operation. For example, $(XY^{2}+X^{2}Y)\cdot
X^{\infty}=X^{\infty}Y^{2}+X^{\infty}Y=X^{\infty}Y$.

###### Definition 6

The semiring $({\mathbb{S}}^{\infty}[{\bm{X}}],+,\cdot,0,1)$ of _(generalized)
absorptive polynomials_ consists of all antichains of monomials (w.r.t.
absorption). We write $0$ for the empty antichain and $1$ for the antichain
$\\{1\\}$. Given $P,Q\in{\mathbb{S}}^{\infty}[X]$, define

$P+Q=\mathsf{Maximals}(P\cup Q),\quad P\cdot
Q=\mathsf{Maximals}\\{m_{\\_}1\cdot m_{\\_}2\mid m_{\\_}1\in P,m_{\\_}2\in
Q\\},$

where $\mathsf{Maximals}(M)$ denotes the set of $\succeq$-maximal monomials in
$M$.

This semiring is fully continuous, with $\bigsqcup S=\sum
S=\mathsf{Maximals}(\bigcup S)$ for sets $S$, and absorptive. Moreover,
${\mathbb{S}}^{\infty}[{\bm{X}}]$ is the most general such semiring, as made
explicit in the following universal property. Together with Lemma 1, this is a
fruitful tool to simplify reasoning about all absorptive, fully-continuous
semirings.

######  Theorem 2.1 (universal property, [4])

Every mapping $h\colon{\bm{X}}\to K$ into an absorptive, fully-continuous
semiring $K$ uniquely extends to a fully-continuous semiring homomorphism
$h\colon{\mathbb{S}}^{\infty}[{\bm{X}}]\to K$ (by means of polynomial
evaluation).

For our technical results, we also need the following observations based on
[3] (statements (1) and (3) in fact hold in all absorptive, fully-continuous
semirings, but the proof is much simpler in ${\mathbb{S}}^{\infty}[{\bm{X}}]$,
see Appendix 0.A).

######  Lemma 2 ([3])

Let $S\subseteq{\mathbb{S}}^{\infty}[{\bm{X}}]$ and
$P\in{\mathbb{S}}^{\infty}[{\bm{X}}]$. Then,

  1. 1.

$P\cdot\sum S=\sum\\{P\cdot Q\mid Q\in S\\}$, and

  2. 2.

$(\sum S)^{\infty}=\sum\\{Q^{\infty}\mid Q\in S\\}$, and

  3. 3.

$h(\sum S)=\sum h(S)$, if $h\colon{\mathbb{S}}^{\infty}[{\bm{X}}]\to K$ is a
fully-continuous homomorphism.

######  Lemma 3 ([3])

Let $(P_{\\_}i)_{\\_}{i\in\mathbb{N}}$ be a descending $\omega$-chain with
$P_{\\_}i\in{\mathbb{S}}^{\infty}[{\bm{X}}]$. Then,

$\bigsqcap_{\\_}{i\in\mathbb{N}}P_{\\_}i=\bigsqcup\Big{\\{}\bigsqcap_{\\_}{i\in\mathbb{N}}m_{\\_}i\;\Big{|}\;\begin{array}[]{l}\text{$(m_{\\_}i)_{\\_}{i\in\mathbb{N}}$
is a descending $\omega$-chain }\\\ \text{of monomials with $m_{\\_}i\in
P_{\\_}i$}\end{array}\Big{\\}}.$

To clearly distinguish between indeterminates in polynomial equation systems
and absorptive polynomials, we often use the indeterminate set
${\bm{A}}=\\{A_{\\_}1,\dots,A_{\\_}k\\}$ for the latter, in particular when we
use values from ${\mathbb{S}}^{\infty}[{\bm{A}}]$ as coefficients.

###  2.3 Derivation Trees

Inspired by the analysis of Newton’s method [6], we use derivation trees to
describe the behaviour of polynomial equation systems. For the intuition
behind this notion, think of a polynomial system as a formal grammar: The
indeterminates are the nonterminal symbols, coefficients the terminal symbols,
and each monomial in $P_{\\_}X$ gives rise to a production rule for $X$. We
essentially consider derivation trees of this grammar in the usual sense,
except that we ignore the order of children (we use commutative semirings) and
allow infinite derivations.

While our notion of derivation trees is conceptually identical to [6], we
should note that the definition of the yield labeling is slightly different.

###### Definition 7

A _derivation tree_ $T=(V,E,\mathsf{var},\mathsf{yd})$ over a semiring $K$ and
indeterminates ${\bm{X}}$ is a (possibly infinite) tree $(V,E)$ with node
labelings $\mathsf{var}\colon V\to{\bm{X}}$ and $\mathsf{yd}\colon V\to K$,
the _yield_ of $v$. We say that $T$ is _from $X$_ if for the root
$\varepsilon$, we have $\mathsf{var}(\varepsilon)=X$. For convenience, we
often write $v\in T$ instead of $v\in V$ and refer to $v$ with
$\mathsf{var}(v)=X$ as an occurrence of $X$ in $T$.

We associate with each node the monomial $\mathsf{mon}(v)=\prod_{\\_}{w\in
vE}\mathsf{var}(w)$ composed of its children’s indeterminates. We say that $T$
is _compatible with the system $(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$_ if for each
node, $\mathsf{yd}(v)\cdot\mathsf{mon}(v)\in P_{\\_}{\mathsf{var}(v)}$. The
set of all derivation trees from $X$ that are compatible with the system
$\mathcal{E}$ is denoted $\mathcal{T}(\mathcal{E},X)$.

Given an equation system $\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$
and an indeterminate $X$, a derivation tree $T\in\mathcal{T}(\mathcal{E},X)$
first chooses from the equation $X=P_{\\_}X$ a monomial
$\mathsf{mon}(\varepsilon)$ together with its coefficient
$\mathsf{yd}(\varepsilon)$. On the next level, it then makes analogous choices
for all indeterminates occurring in $\mathsf{mon}(\varepsilon)$, where the
exponent specifies how often an indeterminate occurs. The leaves $v$ of such a
derivation tree (if they exist) have $\mathsf{mon}(v)=1$ and correspond to
absolute coefficients in one of the equations. See Fig. 1 for an example. We
define the yield of an entire tree as the combined yield of all nodes (recall
that we assume $K$ to be absorptive and fully-continuous, so infinite products
are well-defined):

###### Definition 8

The _yield_ of a derivation tree $T=(V,E,\mathsf{var},\mathsf{yd})$ over $K$
is the (possibly infinite) product $\mathsf{yd}(T)=\prod_{\\_}{v\in
V}\mathsf{yd}(v)\in K$.

We compare the yields of two trees by counting occurrences of coefficients or,
equivalently, of monomials from the polynomial equation system.

###### Definition 9

Let $\mathcal{E}$ be an equation system over ${\bm{X}}$, let $Y\in{\bm{X}}$
and $m\in P_{\\_}Y$. For derivation trees $T\in\mathcal{T}(\mathcal{E},X)$, we
define

$|{T}|_{m,Y}=\big{|}\\{v\in T\mid\text{$\mathsf{mon}(v)=m$,
$\mathsf{var}(v)=Y$}\\}\big{|}\in{\mathbb{N}}^{\infty}$

as the number of occurrences of $m\in P_{\\_}Y$ in $T$. Notice that we use
pairs $(m,Y)$ to unambiguously refer to $m\in P_{\\_}Y$, as $m$ may also occur
in other polynomials of $\mathcal{E}$.

######  Lemma 4 (yield comparison)

Given a polynomial system $\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$
over an absorptive, fully-continuous semiring and trees
$T,T^{\prime}\in\mathcal{T}(\mathcal{E},X)$,

  * •

if $|{T}|_{m,Y}\geq|{T^{\prime}}|_{m,Y}$ for all $m\in P_{\\_}Y$,
$Y\in{\bm{X}}$, then $\mathsf{yd}(T)\leq\mathsf{yd}(T^{\prime})$,

  * •

if $|T|_{\\_}{m,Y}=0$ implies $|T^{\prime}|_{\\_}{m,Y}=0$ for all $m,Y$, then
$\mathsf{yd}(T)^{\infty}\leq\mathsf{yd}(T^{\prime})^{\infty}$.

###### Proof

We use the properties of infinite products to group the yields by monomials.
For each $m\in P_{\\_}Y$, let $c_{\\_}{m,Y}\in K$ be its coefficient, such
that $c\cdot m\in P_{\\_}Y$. Then,

$\displaystyle\mathsf{yd}(T)=\prod_{\\_}{v\in
T}\mathsf{yd}(v)=\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\ m\in
P_{\\_}Y\end{subarray}}\prod_{\\_}{\begin{subarray}{c}v\in T,\\\
\mathsf{var}(v)=Y,\\\
\mathsf{mon}(v)=m\end{subarray}}\mathsf{yd}(v)=\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\
m\in P_{\\_}Y\end{subarray}}(c_{\\_}{m,Y})^{|{T}|_{m,Y}},$

and the same applies to $T^{\prime}$. The product on the right is finite and
by absorption, larger exponents lead to smaller values, hence
$\mathsf{yd}(T)\leq\mathsf{yd}(T^{\prime})$. If we apply the infinitary power,
we similarly get
$\mathsf{yd}(T)^{\infty}=\prod_{\\_}{m,Y}(c_{\\_}{m,Y})^{\infty\cdot|{T}|_{m,Y}},$
where $\infty\cdot|{T}|_{m,Y}$ is either $\infty$ (if $|{T}|_{m,Y}>0$) or $0$,
implying the second statement. ∎

##  3 Derivation Trees and the Fixed-Point Iteration

As a first step towards our main result, this section shows that we can
express least and greatest solutions in terms of the yields of derivation
trees. Notice that a single derivation tree does not correspond to a solution
of the equation system, but only to (the derivation of) a single term in the
solution. We thus consider the sum over all derivation trees.

For least solutions, this was already shown (for a slightly different notion
of derivation trees) in [6]. Here we are mostly concerned with the proof for
greatest solutions, as this is much more involved due to the trees being
infinite.

###### Theorem 3.1

Let $K$ be an absorptive, fully-continuous semiring. Let
$\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$ be a polynomial equation
system over $K$. Then for each $X\in{\bm{X}}$,

$\operatorname{\mathbf{lfp}}(F_{\\_}\mathcal{E})_{\\_}X=\sum_{\\_}{\begin{subarray}{c}T\in\mathcal{T}(\mathcal{E},X),\\\
T\text{ is
finite}\end{subarray}}\mathsf{yd}(T),\qquad\operatorname{\mathbf{gfp}}(F_{\\_}\mathcal{E})_{\\_}X=\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T).$

We recall that summation is equivalent to supremum (in idempotent semirings).
Here and in the following, we use summation in reminiscence of the general,
non-idempotent case (cf. [6]) and only switch to supremum as needed. Towards a
proof, we first observe that it suffices to prove Theorem 3.1 for the most
general semiring $K={\mathbb{S}}^{\infty}[{\bm{A}}]$. That is, with the
coefficients being absorptive polynomials (not to be confused with the
polynomials of the equation system $\mathcal{E}$).

###### Claim

If Theorem 3.1 holds for $K={\mathbb{S}}^{\infty}[{\bm{A}}]$, then it also
holds for any absorptive, fully-continuous semiring $K$.

###### Proof

Let $K$ be an absorptive, fully-continuous semiring. Given
$\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$ over $K$, we construct a
symbolic abstraction
$\mathcal{E}^{\prime}\colon(X=P^{\prime}_{\\_}X)_{\\_}{X\in{\bm{X}}}$ over
${\mathbb{S}}^{\infty}[{\bm{A}}]$. To this end, let $P^{\prime}_{\\_}X$ result
from $P_{\\_}X$ by replacing all coefficients with pairwise different
indeterminates from ${\bm{A}}$. Let $h\colon{\bm{A}}\to K$ be the
corresponding instantiation of these indeterminates that reverses this
process, so that $h(\mathcal{E}^{\prime})=\mathcal{E}$. By Theorem 2.1, this
mapping induces a fully-continuous homomorphism
$h\colon{\mathbb{S}}^{\infty}[{\bm{A}}]\to K$, so by Lemma 1, we have for each
$X$,

$\operatorname{\mathbf{gfp}}(F_{\\_}\mathcal{E})_{\\_}X=\operatorname{\mathbf{gfp}}(F_{\\_}{h(\mathcal{E}^{\prime})})_{\\_}X\overset{\clap{\scriptsize(\ref{lemHomoPreservesSolutions})}}{=}h(\operatorname{\mathbf{gfp}}(F_{\\_}{\mathcal{E}^{\prime}}))_{\\_}X=h\bigg{(}\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T^{\prime}\in\mathcal{T}(\mathcal{E}^{\prime},X)}\;\mathsf{yd}(T^{\prime})\bigg{)}.$

Notice that the structure of derivation trees $\mathcal{T}(\mathcal{E},X)$
only depends on the monomials occurring in $\mathcal{E}$, but not on the
coefficients. Thus, the derivation trees for $\mathcal{E}$ and
$\mathcal{E}^{\prime}$ are identical up to the labeling $\mathsf{yd}$. Given a
tree $T\in\mathcal{T}(\mathcal{E},X)$, it holds in particular that

$\mathsf{yd}(T)=\prod_{\\_}{v\in T}\mathsf{yd}(v)=\prod_{\\_}{v\in
T^{\prime}}h(\mathsf{yd}(v))=h\Big{(}\prod_{\\_}{v\in
T^{\prime}}\mathsf{yd}(v)\Big{)}=h\big{(}\mathsf{yd}(T^{\prime})\big{)},$

where $T^{\prime}\in\mathcal{T}(\mathcal{E}^{\prime},X)$ is the tree
corresponding to $T$ (so that only $\mathsf{yd}$ is changed according to the
coefficients in $\mathcal{E}^{\prime}$). By using the one-to-one
correspondence between trees $T\in\mathcal{T}(\mathcal{E},X)$ and
$T^{\prime}\in\mathcal{T}(\mathcal{E}^{\prime},X)$, we can conclude

$\operatorname{\mathbf{gfp}}(F_{\\_}\mathcal{E})_{\\_}X=h\bigg{(}\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T^{\prime}\in\mathcal{T}(\mathcal{E}^{\prime},X)}\mathsf{yd}(T^{\prime})\bigg{)}\overset{\clap{\scriptsize*}}{=}{(\ref{lemSinfExtra})}\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T^{\prime}\in\mathcal{T}(\mathcal{E}^{\prime},X)}h\big{(}\mathsf{yd}(T^{\prime})\big{)}=\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T).$

The proof for $\operatorname{\mathbf{lfp}}(\mathcal{E})$ is symmetric. ∎

For the remaining section, we fix a polynomial equation system
$\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$ over
$K={\mathbb{S}}^{\infty}[{\bm{A}}]$ and consider the induced operator $F$. The
proof proceeds by induction on the fixed-point iterations $F^{n}(\mathbf{0})$
and $F^{n}(\mathbf{1})$, but requires some preparation. The idea is that if
complete derivation trees correspond to the fixed points, their prefixes
should correspond to the steps of the iteration. These prefixes are defined by
simply cutting off the derivation trees at a certain depth and assigning a
specific yield to the nodes at the cut-off depth (eventually, we will simply
assign $0$ for the least and $1$ for the greatest fixed point).

###### Definition 10

Let $T=(V,E,\mathsf{var},\mathsf{yd})\in\mathcal{T}(\mathcal{E},X)$,
$n\in\mathbb{N}$ and $\mathbf{b}\in K^{\ell}$. Let $V_{\\_}{\leq n}\subseteq
V$ be the nodes at depth $\leq n$. We define the _$(n,\mathbf{b})$
-truncation_ of $T$ as

$T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{b}}\coloneqq(V_{\\_}{\leq
n},\,E\cap V_{\\_}{\leq
n}^{2},\,\mathsf{var},\,\mathsf{yd}^{\prime}),\quad\mathsf{yd}^{\prime}(v)=\begin{cases}\mathbf{b}_{\\_}{\mathsf{var}(v)},&\text{$v$
at depth $n$,}\\\ \mathsf{yd}(v),&\text{otherwise.}\end{cases}$

This defines a derivation tree (compatible with $\mathcal{E}$ except for its
leaves) and we define $\mathsf{mon}(v)$ and
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{b}})$ as in
Definitions 7 and 8 (cf. Fig. 1).

$\displaystyle X_{\\_}1$ $\displaystyle=aX_{\\_}1+bX_{\\_}2X_{\\_}3$
$\displaystyle X_{\\_}2$ $\displaystyle=cX_{\\_}1^{2}$ $\displaystyle
X_{\\_}3$ $\displaystyle=d$

$X_{\\_}1/b$$X_{\\_}2/c$$X_{\\_}3/d$$X_{\\_}1/a$$X_{\\_}1/a$$X_{\\_}1/a$$X_{\\_}1/a$$T:$$X_{\\_}1/b$$X_{\\_}2/c$$X_{\\_}3/d$$X_{\\_}1/e_{\\_}1$$X_{\\_}1/e_{\\_}1$$T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{2}^{\mathbf{z}}:$

Figure 1: A derivation tree $T$ and its $(2,\mathbf{e})$-truncation for a
sample equation system, with node labels $\mathsf{var}(v)/\mathsf{yd}(v)$. The
trees have yield $\mathsf{yd}(T)=a^{\infty}bcd$ and
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{2}^{\mathbf{e}})=e_{\\_}1^{2}bcd$.

The following, mostly technical lemma establishes the general connection
between truncations of derivation trees and the fixed-point iteration.

######  Lemma 5 (tree iteration)

Let $K={\mathbb{S}}^{\infty}[{\bm{A}}]$ and $\mathbf{b}\in K^{\ell}$. Then,
$F^{n}(\mathbf{b})_{\\_}X=\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{b}})$,
for all $n\in\mathbb{N}$, $X\in{\bm{X}}$.

###### Proof

Induction on $n$. For $n=0$, we trivially have
$F^{n}(\mathbf{b})_{\\_}X=\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{0}^{\mathbf{b}})=\mathbf{b}_{\\_}X$
for all derivation trees $T\in\mathcal{T}(\mathcal{E},X)$. For the induction
step, assume that
$F^{n}(\mathbf{b})_{\\_}X=\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{b}})$
for all $X\in{\bm{X}}$. We have to show that

$\displaystyle
F^{n+1}(\mathbf{b})_{\\_}X=P_{\\_}X(F^{n}(\mathbf{b}))\overset{\clap{\scriptsize!}}{=}\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n+1}^{\mathbf{b}}).$

To simplify notation, let $\mathbf{a}$ be the tuple with
$\mathbf{a}_{\\_}X=\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{b}})$.
We can rewrite the left-hand side as follows (recall that $m(X)$ denotes the
exponent of $X$ in $m$):

$\displaystyle P_{\\_}X(\mathbf{a})$ $\displaystyle=\sum_{\\_}{c\cdot m\in
P_{\\_}X}(c\cdot m)(\mathbf{a})=\sum_{\\_}{c\cdot m\in
P_{\\_}X}\Big{(}c\cdot\prod_{\\_}{X\in{\bm{X}}}\mathbf{a}_{\\_}X^{m(X)}\Big{)}$
$\displaystyle=\sum_{\\_}{c\cdot m\in
P_{\\_}X}c\cdot\big{(}\underbrace{\mathbf{a}_{\\_}{X_{\\_}1}\cdot\mathbf{a}_{\\_}{X_{\\_}1}\cdots\mathbf{a}_{\\_}{X_{\\_}1}}_{\\_}{m(X_{\\_}1)\text{
times}}\;\cdot\;\dots\;\cdot\;\underbrace{\mathbf{a}_{\\_}{X_{\\_}\ell}\cdots\mathbf{a}_{\\_}{X_{\\_}\ell}}_{\\_}{m(X_{\\_}\ell)\text{
times}}\big{)}=\,\dots$

Notice that the unfolded product is finite, since $m$ only has finite
exponents. By Lemma 2, multiplication distributes over the (infinite) sums
$\mathbf{a}_{\\_}{X_{\\_}1},\mathbf{a}_{\\_}{X_{\\_}2},\dots$. The product
$\mathbf{a}_{\\_}{X_{\\_}1}\cdot\mathbf{a}_{\\_}{X_{\\_}1}\cdots\mathbf{a}_{\\_}{X_{\\_}\ell}$
can thus be rewritten as sum:

$\displaystyle=\sum\bigg{\\{}c\cdot\;\prod_{\mathclap{}}^{\mathclap{}}\,{}_{\\_}{1\leq
i\leq\ell}\mathsf{yd}(T_{\\_}{i,1}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{b}})\cdots\mathsf{yd}(T_{\\_}{i,m(X_{\\_}i)}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{b}})\;\bigg{|}\;\begin{array}[]{l}\text{$c\cdot
m\in P_{\\_}X$ and all possible}\\\ \text{choices of trees
$T_{\\_}{i,j}\in\mathcal{T}(\mathcal{E},X_{\\_}i)$}\end{array}\bigg{\\}}$
$\displaystyle=\sum\Big{\\{}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n+1}^{\mathbf{b}})\;\big{|}\;\text{$c\cdot
m\in P_{\\_}X$, $T\in\mathcal{T}(\mathcal{E},X)$ with
$\mathsf{mon}(\varepsilon)=m$, $\mathsf{yd}(\varepsilon)=c$ }\Big{\\}}$
$\displaystyle=\sum\Big{\\{}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n+1}^{\mathbf{b}})\;\big{|}\;\text{$T\in\mathcal{T}(\mathcal{E},X)$}\Big{\\}}.$

For these last three steps, recall that derivation trees from $X$ first choose
a monomial (and corresponding coefficient) $c\cdot m\in P_{\\_}X$. The root
$\varepsilon$ then has yield $c$ and the children are derivation trees from
the indeterminates occurring in $m$. By commutativity of the infinite product
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n+1}^{\mathbf{b}})$, we
can group together the yields of the child subtrees, thereby obtaining a one-
to-one correspondence with the product terms in the first step. ∎

To prove Theorem 3.1, all that is left to do is to consider the supremum of
the iteration $F^{n}(\mathbf{0})$ and the corresponding tree truncations, and
dually the infimum of $F^{n}(\mathbf{1})$. For the infimum, one last obstacle
needs to be resolved: We must show that whenever we pick for each $n$ some
$n$-truncation, their infimum can still be realized as yield of an actual
(infinite) tree, even if we pick a different tree to truncate for each $n$. A
similar observation has been used for strategy trees of model-checking games
in [4], where it was called _puzzle lemma_ (due to a more involved
construction of the infinite tree).

######  Lemma 6 (puzzle lemma [4])

Let $X\in{\bm{X}}$ and $K={\mathbb{S}}^{\infty}[{\bm{A}}]$. Let
$(T_{\\_}n)_{\\_}{n\in\mathbb{N}}$ be a family of trees
$T_{\\_}n\in\mathcal{T}(\mathcal{E},X)$ such that their yields
$\mathsf{yd}(T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})$
form a descending chain. Then there is a tree
$T^{\prime}\in\mathcal{T}(\mathcal{E},X)$ with
$\mathsf{yd}(T^{\prime})\geq\bigsqcap_{\\_}n\mathsf{yd}(T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})$.

The proof in our setting is quite similar, so we refer to [4] or Appendix 0.A
for a complete proof. Essentially, the finite number of indeterminates in
${\bm{A}}$ allows us to choose a sufficiently large $n$ such that the
truncation $T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}}$
contains a “nice” part that we can repeat to obtain the infinite tree
$T^{\prime}$. Here, “nice” means that no matter how often we repeat this part,
the yield does not fall below
$\bigsqcap_{\\_}n\mathsf{yd}(T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})$.

With this taken care of, we can prove that the sum of all (finite) derivation
trees gives the least and greatest solutions.

######  Proof (of Theorem 3.1)

Recall that $F$ is fully continuous, as it is defined by polynomial
expressions over a fully-continuous semiring. By Kleene’s fixed-point theorem,
we can thus express its least (or greatest) fixed point as supremum of
$F^{n}(\mathbf{0})$ (or infimum of $F^{n}(\mathbf{1})$) over $n\in\mathbb{N}$.
By idempotence, sums coincide with suprema, so for the least solution we
immediately obtain:

$\displaystyle\operatorname{\mathbf{lfp}}(F)_{\\_}X=\bigsqcup_{\\_}{n\in\mathbb{N}}F^{n}(\mathbf{0})_{\\_}X$
$\displaystyle\overset{\clap{\scriptsize*}}{=}{(\ref{lemTreeIteration})}\bigsqcup_{\\_}{n\in\mathbb{N}}\Big{(}\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{0}})\Big{)}=\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\Big{(}\bigsqcup_{\\_}{n\in\mathbb{N}}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{0}})\Big{)}.$

Now observe that
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{0}})=\mathsf{yd}(T)$
if $T$ has height $<n$, otherwise
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{0}})=0$.
Hence
$\bigsqcup_{\\_}n\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{0}})=\mathsf{yd}(T)$
if $T$ is finite and $0$ otherwise.

It remains to consider the greatest solution. We apply Lemma 3 to express the
infimum in ${\mathbb{S}}^{\infty}[{\bm{A}}]$ as a supremum:

$\displaystyle\operatorname{\mathbf{gfp}}(F)_{\\_}X$
$\displaystyle=\bigsqcap_{\\_}{n\in\mathbb{N}}F^{n}(\mathbf{1})_{\\_}X\,\overset{\clap{\scriptsize(\ref{lemTreeIteration})}}{=}\bigsqcap_{\\_}{n\in\mathbb{N}}\Big{(}\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})\Big{)}$
$\displaystyle\overset{\clap{\scriptsize(\ref{lemSinfInfima})}}{=}\;\bigsqcup\Big{\\{}\bigsqcap_{\\_}{n\in\mathbb{N}}y_{\\_}n\;\Big{|}\;\begin{array}[]{l}\text{\small$(y_{\\_}n)_{\\_}{n\in\mathbb{N}}$
is a descending chain of monomials}\\\ \text{\small with
$y_{\\_}n=\mathsf{yd}(T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})$
for some $T_{\\_}n\in\mathcal{T}(\mathcal{E},X)$}\end{array}\Big{\\}}$
$\displaystyle\overset{\clap{\scriptsize(\ref{lemTreesPuzzle})}}{=}\;\bigsqcup\Big{\\{}\mathsf{yd}(T^{\prime})\;\big{|}\;T^{\prime}\in\mathcal{T}(\mathcal{E},X)\Big{\\}}=\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T).$

In the last line, we apply the puzzle lemma. This gives us for each monomial
chain $(y_{\\_}n)_{\\_}{n\in\mathbb{N}}$ an infinite tree $T^{\prime}$ with
$\mathsf{yd}(T^{\prime})\geq\bigsqcap_{\\_}ny_{\\_}n$. Conversely, each tree
$T^{\prime}$ induces the monomial chain defined by
$y_{\\_}n=\mathsf{yd}(T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})$.
It is easy to see that this chain has infimum $\mathsf{yd}(T^{\prime})$, so we
have equality. ∎

##  4 Closed Form Solution

This section is devoted to the proof of our main result:

###### Theorem 4.1

Let $K$ be an absorptive, fully-continuous semiring. Let
$\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$ be a polynomial equation
system over $K$ and ${\bm{X}}=\\{X_{\\_}1,\dots,X_{\\_}\ell\\}$ with induced
operator $F_{\\_}\mathcal{E}\colon K^{\ell}\to K^{\ell}$. Then,

$\operatorname{\mathbf{lfp}}(F_{\\_}\mathcal{E})=F_{\\_}\mathcal{E}^{\ell}(\mathbf{0}),\quad\operatorname{\mathbf{gfp}}(F_{\\_}\mathcal{E})=F_{\\_}\mathcal{E}^{\ell}(\,F_{\\_}\mathcal{E}^{\ell}(\mathbf{1})^{\infty}\,).$

Towards the proof, we again fix a polynomial equation system
$\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$ over an absorptive, fully-
continuous semiring $K$ with induced operator $F$. Recall that $\ell$ denotes
the number of equations (and indeterminates) of $\mathcal{E}$. Our strategy is
to prove that we can always find derivation trees of a certain shape, and that
the yield of all other derivation trees is absorbed by these trees.

###  4.1 Deterministic Derivation Trees

###### Definition 11

A derivation tree $T=(V,E,\mathsf{var},\mathsf{yd})$ is said to be
_deterministic_ if $\mathsf{mon}(v)$ depends only on $\mathsf{var}(v)$. That
is, the indeterminate labels of the (unordered) children of a node $v$ are
determined by the node’s indeterminate label so that the relation
$\\{(\mathsf{var}(v),\mathsf{mon}(v))\mid v\in V\\}$ is a function.

To reason about $\operatorname{\mathbf{gfp}}(F)$, we must reason about and
construct infinite derivation trees. This is straight-forward for
deterministic trees.

######  Lemma 7 (deterministic construction)

Let ${\bm{X}}_{\\_}0\subseteq{\bm{X}}$. For each $X\in{\bm{X}}_{\\_}0$, let
$m_{\\_}X$ be a monomial with $m_{\\_}X\in P_{\\_}X$ such that all
indeterminates occurring in $m_{\\_}X$ are contained in ${\bm{X}}_{\\_}0$.
Then for each $X\in{\bm{X}}_{\\_}0$, there is a deterministic tree
$T\in\mathcal{T}(\mathcal{E},X)$ with $\mathsf{var}(v)\in{\bm{X}}_{\\_}0$ and
$\mathsf{mon}(v)=m_{\\_}{\mathsf{var}(v)}$ for all nodes $v\in T$.

######  Proof (sketch)

Starting from the root $\mathsf{var}(\varepsilon)=X$, define the (possibly
infinite) tree $T$ inductively by repeatedly adding to each leaf $v$ child
nodes according to $m_{\\_}{\mathsf{var}(v)}$, always maintaining the desired
property for all inner nodes. ∎

It is easy to see that deterministic trees are uniquely defined by their
prefix up to depth $\ell-1$, as at depth $\ell$ each path must either end or
start to repeat (recall that there are only $\ell$ different indeterminates).
Moreover, once we consider the infinitary power $\mathsf{yd}(T)^{\infty}$, it
does not matter how often a particular coefficient $c$ occurs in $T$, since
$(c^{n})^{\infty}=c^{\infty}$ for all $n>0$. This leads to the following
simple but essential observations.

###### Lemma 8

If $T\in\mathcal{T}(\mathcal{E},X)$ is deterministic, every indeterminate that
occurs in $T$ also occurs in the truncation
$T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell-1}^{\mathbf{1}}$. It follows
that
$\mathsf{yd}(T)^{\infty}=\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}$.

###### Corollary 1

For each $T\in\mathcal{T}(\mathcal{E},X)$, there is a deterministic tree
$T^{\prime}\in\mathcal{T}(\mathcal{E},X)$ such that
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}\leq\mathsf{yd}(T^{\prime})^{\infty}$.

######  Proof (sketch)

Choose any way to determinize
$T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}}$ (by Lemma 7)
using only monomials appearing in
$T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}}$. This is always
possible, as $T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}}$
contains at most $\ell$ indeterminates and hence every path must contain a
repetition or end in a leaf (cf. Appendix 0.A). The inequality holds by Lemma
4 (yield comparison). ∎

###  4.2 Constructing Simple Trees

$X$$X$$X$$Y$$X$$X$$Y$$Y$$X$(a) (a)

$X$$X$$Y$$T^{\infty}_{\\_}X$$T^{\infty}_{\\_}X$$T^{\infty}_{\\_}Y$(b) (b)

$\\!Z$$Z\\!$(c) (c)

$X$$Y$$T^{\infty}_{\\_}X$$T^{\infty}_{\\_}Y$(d)$\ell$ (d)

Figure 2: Illustration of the construction steps in the proof of Lemma 9.

The main insight behind Theorem 4.1 is that when we sum over the yield of all
derivation trees, it suffices to consider trees of a particular shape
corresponding to our intuition from the introduction: These trees consist of
an arbitrary prefix up to (at most) depth $\ell$ (the reachability part),
followed by deterministic trees (the cyclic part). See Fig. 2d for an
illustration.

######  Lemma 9 (main lemma)

For each $T\in\mathcal{T}(\mathcal{E},X)$, there is a derivation tree
$T^{\prime}\in\mathcal{T}(\mathcal{E},X)$ such that all subtrees rooted at
depth $\ell$ in $T^{\prime}$ are deterministic and use only monomials $m\in
P_{\\_}Y$ (with $Y\in{\bm{X}}$) that occur infinitely often in $T$. Moreover,
$|{T^{\prime}}|_{m,Y}\leq|{T}|_{m,Y}$ for all $m\in P_{\\_}Y,Y\in{\bm{X}}$.

###### Proof

Let ${\bm{X}}_{\\_}\infty\subseteq{\bm{X}}$ be the set of indeterminates that
occur infinitely often in $T$ (may be empty). We write $V_{\\_}X=\\{v\in
T\mid\mathsf{var}(v)=X\\}$ for the set of nodes labeled $X$. For each
$X\in{\bm{X}}_{\\_}\infty$, the set $V_{\\_}X$ is infinite. As the polynomial
$P_{\\_}X$ is finite, there must thus be infinitely many $v\in V_{\\_}X$ with
the same monomial $\mathsf{mon}(v)$. For each $X\in{\bm{X}}_{\\_}\infty$,
choose such an infinitely often occurring monomial $m_{\\_}X\in P_{\\_}X$.
Using Lemma 7, we obtain for each $X\in{\bm{X}}_{\\_}\infty$ a deterministic
tree $T^{\infty}_{\\_}X\in\mathcal{T}(\mathcal{E},X)$ such that for all $v\in
T^{\infty}_{\\_}X$: $\mathsf{var}(v)\in{\bm{X}}_{\\_}\infty$ and
$\mathsf{mon}(v)$ occurs infinitely often in $T$.

Let $W$ be the set of earliest occurrences of ${\bm{X}}_{\\_}\infty$ in $T$
(cf. Fig. 2a). Formally, $W=\\{v\in
T\mid\mathsf{var}(v)\in{\bm{X}}_{\\_}\infty$, there is no $v^{\prime}\sqsubset
v$ with $\mathsf{var}(v^{\prime})\in{\bm{X}}_{\\_}\infty\\}$. Now let $S$ be
the tree that results from $T$ by replacing the subtree at each $v\in W$ with
the tree $T^{\infty}_{\\_}{\mathsf{var}(v)}$ (cf. Fig. 2b). The tree $S$ is
almost of the desired shape, but the trees $T^{\infty}_{\\_}X$ may be rooted
at depth $>\ell$. To fix this, we consider the prefix up to the subtrees
$T^{\infty}_{\\_}X$ and eliminate all repetitions of indeterminates within the
prefix. As all indeterminates in the prefix occur only finitely often, we can
eliminate repetitions by replacing each first occurrence of an indeterminate
$Z$ by a last occurrence of $Z$ within the prefix (cf. Fig. 2c).

More formally, call a path $v_{\\_}0v_{\\_}1v_{\\_}2\dots v_{\\_}k$ from the
root of $S$ _unresolved_ if $k\geq\ell$ and no node on the path is contained
in one of the deterministic subtrees $T_{\\_}X^{\infty}$. Given an unresolved
path, there must be an indeterminate $Z$ that occurs twice on the path.
Further, $Z\notin{\bm{X}}_{\\_}\infty$, as otherwise the nodes labeled $Z$
would lie within one of the deterministic subtrees by construction of $S$ and
$W$. Let $i<j$ be indices such that $v_{\\_}i$ is the first and $v_{\\_}j$ the
last occurrence of $Z$ on the path, so
$\mathsf{var}(v_{\\_}i)=\mathsf{var}(v_{\\_}j)=Z$. Now let $S^{\prime}$ result
from $S$ by replacing the subtree $S_{\\_}{v_{\\_}i}$ rooted at $v_{\\_}i$
with the subtree $S_{\\_}{v_{\\_}j}$ rooted at $v_{\\_}j$, thereby removing at
least one occurrence of $Z$ from the tree (Fig. 2c).

Apply this elimination step exhaustively, until there are no more unresolved
paths. As all indeterminates in the prefix of $S$ occur only finitely often,
this process terminates. Let $T^{\prime}$ be the resulting tree (notice that
$T^{\prime}$ is not uniquely determined, but this does not affect our
argument). Then $T^{\prime}$ has the desired shape: when no unresolved path
exists, then all nodes at depth $\ell$ (if any) must be contained in one of
deterministic subtrees $T_{\\_}X^{\infty}$.

Moreover, the elimination step only removes nodes of $S$, but neither adds
nodes nor modifies any node labels. It follows that
$|{T^{\prime}}|_{m,Y}\leq|{S}|_{m,Y}$ for all $m\in P_{\\_}Y,Y\in{\bm{X}}$. As
the trees $T_{\\_}X^{\infty}$ only use monomials that occur infinitely often
in $T$, we further have $|{S}|_{m,Y}\leq|{T}|_{m,Y}$ for all $m,Y$, closing
the proof.∎

###  4.3 Proof of the Main Result

We relate infinite trees of this shape to the expression
$F^{\ell}(\,F^{\ell}(\mathbf{1})^{\infty}\,)$. The deterministic trees rooted
at depth $\ell$ correspond to the inner term $F^{\ell}(\mathbf{1})^{\infty}$,
relying on Lemma 8 to ensure that $\ell$ applications of $F$ suffice. The
outer applications of $F$ correspond to the prefix on which we impose no
further restrictions (except that it has height at most $\ell$). The following
lemma formalizes this intuition.

###### Lemma 10

Let $\mathbf{b}$ be the tuple with
$\mathbf{b}_{\\_}X=\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}$
for $X\in{\bm{X}}$. For each $T\in\mathcal{T}(\mathcal{E},X)$, there is a tree
$T^{\prime}\in\mathcal{T}(\mathcal{E},X)$ such that
$\mathsf{yd}(T)\leq\mathsf{yd}(T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{b}})$.

###### Proof

Let $T\in\mathcal{T}(\mathcal{E},X)$. Using Lemma 9, we obtain a tree
$T^{\prime}$ of a certain shape: Let $S_{\\_}1,\dots,S_{\\_}k$ be the subtrees
of $T^{\prime}$ rooted at depth $\ell$. These subtrees are deterministic and
all monomials occurring in $S_{\\_}1,\dots,S_{\\_}k$ occur infinitely often in
$T$ and moreover, $|{T^{\prime}}|_{m,Y}\leq|{T}|_{m,Y}$ for all $m\in
P_{\\_}Y,Y\in{\bm{X}}$. We claim that

$\mathsf{yd}(T)\overset{\clap{\scriptsize*}}{\leq}{!}\mathsf{yd}(T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})\cdot\prod_{\\_}{i=1}^{k}\mathsf{yd}(S_{\\_}i)^{\infty}$

To see this, we expand the definition of $\mathsf{yd}$ and rearrange terms.
Borrowing the notation $c_{\\_}{m,Y}$ for the coefficient of $m\in P_{\\_}Y$
from the proof of Lemma 4, we obtain

$\displaystyle\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\ m\in
P_{\\_}Y\end{subarray}}(c_{\\_}{m,Y})^{|{T}|_{m,Y}}\overset{\clap{\scriptsize*}}{\leq}{!}\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\
m\in
P_{\\_}Y\end{subarray}}(c_{\\_}{m,Y})^{|{T^{\prime}\|_{\ell}^{\mathbf{1}}}|_{m,Y}+\sum_{\\_}{i=1}^{k}\infty\cdot|{S_{\\_}i}|_{m,Y}},$

To prove the inequality, it suffices to show that
$|{T}|_{m,Y}\geq|{T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}}}|_{m,Y}+\sum_{\\_}{i=1}^{k}\infty\cdot|{S_{\\_}i}|_{m,Y}$
for all $m,Y$. This holds by construction of $T^{\prime}$: If
$|{S_{\\_}i}|_{m,Y}>0$ for some $i$, then $m$ occurs infinitely often in $T$
and hence $|{T}|_{m,Y}=\infty$. Otherwise, the right-hand side is equal to
$|{T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}}}|_{m,Y}\leq|{T^{\prime}}|_{m,Y}\leq|{T}|_{m,Y}$.
This proves our claim.

Now let $v_{\\_}1,\dots,v_{\\_}k\in T^{\prime}$ be the root nodes of the
deterministic subtrees $S_{\\_}1,\dots,S_{\\_}k$. By Lemma 8,
$\mathsf{yd}(S_{\\_}i)^{\infty}=\mathsf{yd}(S_{\\_}i\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}\leq\mathbf{b}_{\\_}{\mathsf{var}(v_{\\_}i)}$,
and thus

$\mathsf{yd}(T)\leq\mathsf{yd}(T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})\cdot\prod_{\\_}{i=1}^{k}\mathsf{yd}(S_{\\_}i)^{\infty}\leq\mathsf{yd}(T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})\cdot\prod_{\\_}{i=1}^{k}\mathbf{b}_{\\_}{\mathsf{var}(v_{\\_}i)}=\mathsf{yd}(T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{b}}).$

We are now ready to prove our main result. The statement on the least solution
follows rather directly from our earlier considerations. For greatest fixed
points, the previous lemma already proves the difficult direction.

######  Proof (of Theorem 4.1)

It suffices to consider the case $K={\mathbb{S}}^{\infty}[{\bm{A}}]$ (so that
Lemmas 2 and 5 apply), as the general statement follows with Lemma 1. We first
consider the least solution. It is clear by monotonicity of $F$ that
$F^{\ell}(\mathbf{0})_{\\_}X\leq\operatorname{\mathbf{lfp}}(F)_{\\_}X$. By
Theorems 3.1 and 5, it thus suffices to prove

$\operatorname{\mathbf{lfp}}(F)_{\\_}X=\;\;\sum_{\mathclap{}}^{\mathclap{}}\,{}_{\\_}{\begin{subarray}{c}T\in\mathcal{T}(\mathcal{E},X)\\\
T\text{
finite}\end{subarray}}\,\mathsf{yd}(T)\overset{\clap{\scriptsize!}}{\leq}*\,\;\sum_{\mathclap{}}^{\mathclap{}}\,{}_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\,\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{0}})=F^{\ell}(\mathbf{0})_{\\_}X.$

To this end, let $T\in\mathcal{T}(\mathcal{E},X)$ be finite and obtain
$T^{\prime}$ by Lemma 9. As $T$ is finite, no monomials can occur infinitely
often. Hence $T^{\prime}$ has no subtrees rooted at depth $\ell$ and is thus
of height $<\ell$. But then,
$\mathsf{yd}(T)\leq\mathsf{yd}(T^{\prime})=\mathsf{yd}(T^{\prime}\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{0}})\leq
F^{\ell}(\mathbf{0})_{\\_}X$.

For the greatest solution, we know that
$\operatorname{\mathbf{gfp}}(F)_{\\_}X=\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T)$.
On the other hand, Lemma 5 (tree iteration) entails

$(F^{\ell}(\mathbf{1})_{\\_}X)^{\infty}=\Big{(}\sum_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})\Big{)}^{\infty}\overset{\clap{\scriptsize(*)}}{=}{\ref{lemSinfExtra}}\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\,\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}.$

Now let $\mathbf{b}=F^{\ell}(\mathbf{1})^{\infty}$. Applying Lemma 5 again
gives

$F^{\ell}(F^{\ell}(\mathbf{1})^{\infty})_{\\_}X=F^{\ell}(\mathbf{b})_{\\_}X=\smashoperator[r]{\sum_{}^{}}\,_{\\_}{T\in\mathcal{T}(\mathcal{E},X)}\,\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{b}}).$

The direction $\operatorname{\mathbf{gfp}}(F)\leq
F^{\ell}(F^{\ell}(\mathbf{1})^{\infty})$ follows immediately from Lemma 10.
For the other direction, let $T\in\mathcal{T}(\mathcal{E},X)$. Let
$v_{\\_}1,\dots,v_{\\_}k$ be the nodes at depth $\ell$ in $T$. By
distributivity (Lemma 2), we get

$\displaystyle\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{b}})$
$\displaystyle=\;\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})\cdot\;\prod_{\mathclap{}}^{\mathclap{}}\,{}_{\\_}{1\leq
i\leq k}\mathbf{b}_{\\_}{\mathsf{var}(v_{\\_}i)}$
$\displaystyle\overset{\clap{\scriptsize
dist.}}{=}\;\;\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})\cdot\sum\Big{\\{}\smashoperator[r]{\prod_{}^{}}\,_{\\_}{1\leq
i\leq
k}\mathsf{yd}(S_{\\_}i\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}\;\big{|}\;\text{$S_{\\_}i\in\mathcal{T}(\mathcal{E},\mathsf{var}(v_{\\_}i))$
for all $i$}\Big{\\}}$ yd(T

$\|$

—_ℓ^1) ⋅∑{∏ 1 ≤i ≤k yd(Si’)^∞
—$S_{\\_}i^{\prime}\in\mathcal{T}(\mathcal{E},\mathsf{var}(v_{\\_}i))$ for all
$i$} $\displaystyle\overset{\clap{\scriptsize
abs.}}{\leq}\;\;\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})\cdot\sum\Big{\\{}\smashoperator[r]{\prod_{}^{}}\,_{\\_}{1\leq
i\leq
k}\mathsf{yd}(S_{\\_}i^{\prime})\;\big{|}\;\text{$S_{\\_}i^{\prime}\in\mathcal{T}(\mathcal{E},\mathsf{var}(v_{\\_}i))$
for all $i$}\Big{\\}}$ $\displaystyle\overset{\clap{\scriptsize
dist.}}{=}\;\;\sum\Big{\\{}\mathsf{yd}(T)\;\big{|}\;\text{$T\in\mathcal{T}(\mathcal{E},X)$}\Big{\\}}=\operatorname{\mathbf{gfp}}(F)_{\\_}X.$
∎

Using this result, we can compute least and, most importantly, greatest
solutions of polynomial equation systems in a polynomial number of semiring
operations (including the infinitary power). Notice that, although the proof
relied on ${\mathbb{S}}^{\infty}[{\bm{A}}]$, the computation happens only in
the semiring we consider. For instance, recall the example in the tropical
semiring from the introduction.

###### Example 1

We recall $X_{\\_}a=1+_{\mathbb{R}}X_{\\_}a$,
$X_{\\_}b=\min(1+_{\mathbb{R}}X_{\\_}a,20+_{\mathbb{R}}X_{\\_}c)$ and
$X_{\\_}c=0+_{\mathbb{R}}X_{\\_}c$ from the introduction. Notice that the one-
element of the tropical semiring is the real value $0$. Using Theorem 4.1, we
collapse the infinite fixed-point iteration to

${\scriptsize\begin{pmatrix}0\\\ 0\\\
0\end{pmatrix}}\xmapsto{\\!F\\!}{\scriptsize\begin{pmatrix}1\\\ 1\\\
0\end{pmatrix}}\xmapsto{\\!F\\!}{\scriptsize\begin{pmatrix}2\\\ 2\\\
0\end{pmatrix}}\xmapsto{\\!F\\!}{\scriptsize\begin{pmatrix}3\\\ 3\\\
0\end{pmatrix}}\xmapsto{{}^{\infty}}{\scriptsize\begin{pmatrix}\infty\\\
\infty\\\ 0\end{pmatrix}}\xmapsto{\\!F\\!}{\scriptsize\begin{pmatrix}\infty\\\
20\\\ 0\end{pmatrix}}\,\leavevmode\hbox to11.86pt{\vbox
to18.91pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-4.75275pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}{}}{{}}{}{}\pgfsys@moveto{0.0pt}{5.16666pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{{}{}}}{{}}
{{{}}{{}}}{{}}{{{}}{{{}{}}}}{{}{}}{{}}{}{}{}{}{}{}{}{{}}{{}}{}{}{}{}{{}}{{
{\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}
\pgfsys@moveto{0.0pt}{1.72221pt}\pgfsys@lineto{0.0pt}{-1.72221pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{0.29999pt}{5.16666pt}\pgfsys@curveto{8.56288pt}{5.16666pt}{8.56288pt}{-2.15277pt}{0.4pt}{-2.15277pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.2pt}{5.16666pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.2pt}{-2.15277pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.51866pt}{6.03995pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\scriptsize{$\\!F$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

and obtain the expected solution. In this example, one iteration of $F$ would
actually suffice (instead of $\ell=3$ iterations), since cycles have length
one (see the graph in the introduction). In general, all $\ell$ steps are
required (see below). $\lrcorner$

Coming back to our original motivation from semiring provenance, we can thus
compute semiring provenance information for Büchi games [9] or fixed-point
logics such as the modal $\mu$-calculus $L_{\\_}\mu$ or least fixed-point
logic LFP [4]. If we only need to compute a polynomial number of fixed points,
such as for alternation-free $L_{\\_}\mu$, this information might be
computable in polynomial time – depending on the cost of the semiring
operations. In the most general semiring ${\mathbb{S}}^{\infty}[{\bm{X}}]$, we
cannot assume that semiring operations can be performed efficiently, as each
multiplication can in the worst case double the number of monomials (this is
not avoidable, as one can easily construct equation systems whose solution is
an absorptive polynomial describing all exponentially many paths in a graph).
Even if the solution consists of few monomials, we may get an intermediary
blowup when computing $F^{n}(\mathbf{1})$, as seen in the following example.
In such cases, the symbolic approach presented in Section 5 may be preferable.

###### Example 2

Consider the polynomial equation system over ${\mathbb{S}}^{\infty}[a,b,c]$
shown on the left. (Assuming familiarity with $L_{\\_}\mu$ and semiring
provenance, this results from evaluating $\nu X.\ \Box X\land\Diamond P$ in a
semiring interpretation that uses the indeterminates $a,b,c$ to track whether
the atom $P$ holds at vertices $v_{\\_}1,v_{\\_}2,v_{\\_}3$.)
$\displaystyle X_{\\_}1$ $\displaystyle=b\cdot X_{\\_}2$ $\displaystyle
X_{\\_}2$ $\displaystyle=(b+c)\cdot X_{\\_}2X_{\\_}3$ $\displaystyle X_{\\_}3$
$\displaystyle=a\cdot X_{\\_}1$ $v_{\\_}1$$v_{\\_}2$$v_{\\_}3$

We apply Theorem 4.1 to compute the greatest solution:

$\mathbf{1}\xmapsto{\\!F\\!}{\scriptsize\begin{pmatrix}b\\\ b+c\\\
a\end{pmatrix}}\xmapsto{\\!F\\!}{\scriptsize\begin{pmatrix}b^{2}+bc\\\
ab^{2}+abc+ac^{2}\\\
ab\end{pmatrix}}\xmapsto{\\!F\\!}{\scriptsize\begin{pmatrix}ab^{3}+ab^{2}c+abc^{2}\\\
a^{2}b^{4}+a^{2}b^{3}c+a^{2}b^{2}c^{2}+a^{2}bc^{3}\\\
ab^{2}+abc\end{pmatrix}}\xmapsto{\\!{}^{\infty}\\!}{\scriptsize\begin{pmatrix}a^{\infty}b^{\infty}\\\
a^{\infty}b^{\infty}\\\ a^{\infty}b^{\infty}\end{pmatrix}}\,\leavevmode\hbox
to11.86pt{\vbox to18.91pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-4.75275pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}{}}{{}}{}{}\pgfsys@moveto{0.0pt}{5.16666pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{{}{}}}{{}}
{{{}}{{}}}{{}}{{{}}{{{}{}}}}{{}{}}{{}}{}{}{}{}{}{}{}{{}}{{}}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{5.16666pt}\pgfsys@curveto{8.56288pt}{5.16666pt}{8.56288pt}{-2.15277pt}{0.4pt}{-2.15277pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.2pt}{5.16666pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.2pt}{-2.15277pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.51866pt}{6.03995pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\scriptsize{$\\!F$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

Here we need all $\ell=3$ inner applications of $F$ until $a$ appears in the
first entry. We also see that the intermediate polynomials can become much
longer than the solution. (Interpreting $a^{\infty}b^{\infty}$ as provenance
information, we see that the formula holds at the given graph precisely if $P$
holds at $v_{\\_}1$ and $v_{\\_}2$, and it does not matter if it also holds at
$v_{\\_}3$.) $\lrcorner$

###### Remark 2

One can generalize our main result to polynomial equation systems that allow
$\infty$ as exponent (similar to absorptive polynomials). We have chosen to
spare the reader from the additional complications that arise from the
corresponding derivation trees with infinite degree, in particular infinite
products on the semiring level, as these are not relevant for the main ideas.
Alternatively, the symbolic approach of Sect. 5 can be used in this setting.

##  5 Symbolic Computation

This section complements our main results by a second approach focused
specifically on polynomial equation systems over the semiring
${\mathbb{S}}^{\infty}[{\bm{A}}]$. To this end, we adapt results of Hopkins
and Kozen on Kleene algebras [15] since we can view absorptive semirings as a
special case of Kleene algebras (by setting $a^{*}=1$ for all elements $a$).
These results are based on symbolic derivatives of polynomials (which is also
the basis for Newton’s method [6]) to express least solutions. Here, we
generalize this approach to include the infinitary power operation, eventually
leading to a similar statement also for greatest solutions.

###### Remark 3

Extensions of Kleene algebra by an operation similar to infinitary power have
already been studied in other contexts. For instance, Cohen [2] introduces
$\omega$-algebras by axiomatizing a unary operation $a^{\omega}$, which can be
interpreted as infinite repetition in $\omega$-words or infinite iteration in
the relational model of program analysis. However, Cohen’s axioms seem too
weak for the proofs below; we discuss an alternative axiomatization of
$a^{\infty}$ in Appendix 0.B.

###  5.1 Setting and Derivatives

It is convenient to slightly reformulate our problem setting: Instead of a
system $\mathcal{E}\colon(X=P_{\\_}X)_{\\_}{X\in{\bm{X}}}$ with polynomials
$P_{\\_}X$ over ${\bm{X}}$ and coefficients ${\mathbb{S}}^{\infty}[{\bm{A}}]$,
we now regard $P_{\\_}X$ as an absorptive polynomial
$P_{\\_}X\in{\mathbb{S}}^{\infty}[{\bm{A}}\cup{\bm{X}}]$ (so we no longer
distinguish between indeterminates of the polynomial system and indeterminates
occurring in coefficients). This allows a more uniform treatment when we
eliminate indeterminates one by one, and it is easy to see that it does not
affect the solutions.

To simplify notation, we write ${\mathbb{S}}^{\infty}[{\bm{A}},X]$ for
${\mathbb{S}}^{\infty}[{\bm{A}}\cup\\{X\\}]$. Recall that we write
$P(X)\in{\mathbb{S}}^{\infty}[{\bm{A}},X]$ to make explicit that $X$ may occur
in $P$; then $P(a)\in{\mathbb{S}}^{\infty}[{\bm{A}}]$ denotes the polynomial
that results from $P(X)$ by replacing $X$ with
$a\in{\mathbb{S}}^{\infty}[{\bm{A}}]$. In the following, we use ${\bm{X}}$ to
denote an arbitrary (finite) indeterminate set.

###### Definition 12

Let $X\in{\bm{X}}$ and $P(X)\in{\mathbb{S}}^{\infty}[{\bm{X}}]$. We denote the
_partial derivative_ of $P$ with respect to $X$ as $P^{\prime}$ (leaving $X$
implicit) and define it inductively by

$\displaystyle X^{\prime}=1,\quad Y^{\prime}=0\text{ for $X\neq
Y\in{\bm{X}}$},$ $\displaystyle(PQ)^{\prime}=P^{\prime}\cdot Q+P\cdot
Q^{\prime},\quad(P+Q)^{\prime}=P^{\prime}+Q^{\prime},\quad\big{(}{P^{\infty}}\big{)}^{\prime}=P^{\infty}\cdot
P^{\prime},$

where $P(X),Q(X)\in{\mathbb{S}}^{\infty}[{\bm{X}}]$.

###  5.2 Solutions in One Dimension

We first show how least and greatest solutions of a single equation $X=P(X)$
can be expressed using derivatives, following the proof in [15]. Notice that
${\mathbb{S}}^{\infty}[{\bm{X}}]$, and in fact any absorptive semiring, can be
regarded as a Kleene algebra in the sense of [15] by setting $a^{*}=1$ for all
$a\in K$. Hence, most of the lemmas require no modifications, except for our
addition of the infinitary power.

###### Lemma 11

Let $P(X),Q(X)\in{\mathbb{S}}^{\infty}[{\bm{X}}]$ and further
$a,b,c\in{\mathbb{S}}^{\infty}[{\bm{X}}]$. Then,

  1. 1.

$P(Q)^{\prime}=P^{\prime}(Q)\cdot Q^{\prime}$, (chain rule, cf. [15])

  2. 2.

$P(a+b)=P(a)+P^{\prime}(a+b)\cdot b$ (Taylor’s theorem, cf. [15]),

  3. 3.

$ac\leq bc\;\implies\;P(a)c\leq P(b)c$ (cf. [15]).

###### Proof

By structural induction on $P$. The proof of [15] also applies to
${\mathbb{S}}^{\infty}[{\bm{X}}]$, so we only have to consider the case
$P=H^{\infty}$. For the chain rule, we have

$\displaystyle\big{(}H^{\infty}(Q)\big{)}^{\prime}$
$\displaystyle=\big{(}H(Q)^{\infty}\big{)}^{\prime}=H(Q)^{\infty}\cdot
H(Q)^{\prime}$ $\displaystyle=H(Q)^{\infty}\cdot H^{\prime}(Q)\cdot
H^{\prime}=\big{(}H(Q)^{\infty}\big{)}^{\prime}\cdot
Q^{\prime}=\big{(}H^{\infty}(Q)\big{)}^{\prime}\cdot Q^{\prime},$

and for Taylor’s theorem,

$\displaystyle H^{\infty}(a+b)$ $\displaystyle=H(a+b)^{\infty}$
$\displaystyle=\big{(}H(a)+H^{\prime}(a+b)\cdot b\big{)}^{\infty}$ H(a)^∞+
(H(a) + H’(a+b) ⋅b )^∞⋅H’(a+b) ⋅b
$\displaystyle=H(a)^{\infty}+H(a+b)^{\infty}\cdot H^{\prime}(a+b)\cdot b$
$\displaystyle=H^{\infty}(a)+H^{\infty}(a+b)\cdot H^{\prime}(a+b)\cdot b$
$\displaystyle=H^{\infty}(a)+(H^{\infty})^{\prime}(a+b)\cdot b.$

In $(*)$, we use the fact that $(a+b)^{\infty}=a^{\infty}+(a+b)^{\infty}\cdot
b$ for elements $a,b$ of any absorptive, fully-continuous semiring. For (3),
we apply full continuity:

$\displaystyle
H^{\infty}(a)c=\Big{(}\bigsqcap_{\\_}{n\in\mathbb{N}}H^{n}(a)\Big{)}\cdot
c=\bigsqcap_{\\_}{n\in\mathbb{N}}\big{(}H^{n}(a)c\big{)}\leq\bigsqcap_{\\_}{n\in\mathbb{N}}\big{(}H^{n}(b)c\big{)}=H^{\infty}(b)c.$
∎

For the result about the greatest solution, we need an additional observation
about the infinitary power operation:

###### Lemma 12

Let $K$ be an absorptive, fully-continuous semiring. Then all elements
$a,b,c\in K$ satisfy:

$c+ab\geq b\quad\implies\quad c+a^{\infty}b\geq b.$

###### Proof

We first show by induction that $c+a^{n}b\geq b$ for all $n\in\mathbb{N}$. For
$n=0$, trivially $c+a^{0}b=c+b\geq b$, and for $n=1$ this holds by assumption.
The induction step follows from absorption:

$c+a^{n+1}b\;\overset{\clap{\scriptsize
abs}}{=}\;c+ac+a^{n+1}b=c+a(c+a^{n}b)\geq c+ab\geq b.$

The claim then follows by full continuity:

$c+a^{\infty}b=c+\Big{(}\bigsqcap_{\\_}{n\in\mathbb{N}}a^{n}\Big{)}b=\bigsqcap_{\\_}{n\in\mathbb{N}}(c+a^{n}b)\geq\bigsqcap_{\\_}{n\in\mathbb{N}}b=b.$

Using the observations in Lemma 11, Hopkins and Kozen prove that the least
solution is $P^{\prime}(P(0))^{*}\cdot P(0)$, which in our setting is equal to
$P(0)$ and can in fact be derived directly from absorption, without
derivatives. However, using derivatives allows us to also express greatest
solutions:

###### Theorem 5.1

Let $P(X)\in{\mathbb{S}}^{\infty}[{\bm{A}},X]$. Then $X=P(X)$ has the least
solution $P(0)$ and the greatest solution $P(0)+P^{\prime}(1)^{\infty}$ in
${\mathbb{S}}^{\infty}[{\bm{A}}]$.

###### Proof

See [15] for a proof of the least solution. Alternatively, let
$a_{\\_}0\in{\mathbb{S}}^{\infty}[{\bm{A}}]$ be the absolute coefficient of
$P$ (i.e., the sum of all monomials not containing $X$) so that
$P(0)=a_{\\_}0$. Since we have $m(a_{\\_}0)\leq a_{\\_}0$ for every monomial
$m$ containing $X$, it follows that $P(P(0))=P(a_{\\_}0)=a_{\\_}0$ by
absorption, so $P(0)$ is the least solution.

For the greatest solution, we first prove that $P(0)+P^{\prime}(1)^{\infty}$
is a solution to the inequality $X\leq P(X)$:

We next show that this is the greatest solution to $X\leq P(X)$. To this end,
let $a\in{\mathbb{S}}^{\infty}[{\bm{A}}]$ be a solution, i.e., $a\leq P(a)$.
As $1\geq a$, we get

$P(0)+P^{\prime}(1)\cdot a\geq P(0)+P^{\prime}(a)\cdot
a\overset{\clap{\scriptsize(*)}}{=}{\ref{lemChainTaylor}.2}P(a)\geq a.$

Using Lemma 12, we can conclude

$P(0)+P^{\prime}(1)^{\infty}\overset{\clap{\scriptsize*}}{\geq}{abs}P(0)+P^{\prime}(1)^{\infty}\cdot
a\geq a.$

Finally, note that the greatest solution to $X\leq P(X)$ is also the greatest
solution to $X=P(X)$ by the well-known Knaster-Tarski theorem. ∎

###  5.3 Solutions of Larger Systems

To solve systems with more than one equation, we eliminate indeterminates one
by one, in each step applying Theorem 5.1. The main theoretical underpinning
is the uniformity of the solutions in one indeterminate. In [15], this
uniformity follows from the axiomatic proofs and the fact that instantiations
preserve the axioms of Kleene algebra. Here, we instead appeal to the
universal property of ${\mathbb{S}}^{\infty}[{\bm{X}}]$ and the fact that
fully-continuous semiring homomorphisms preserve least and greatest fixed
points.

For the sake of simplicity, we only consider systems of two equations; we can
inductively apply the same approach to larger systems. Moreover, we only state
the result for greatest solutions, as least solutions are symmetric. We use
the notation $\operatorname{\mathbf{gfp}}(X\mapsto P(X,Y))$ to refer to the
greatest solution of the equation $X=P(X,Y)$ using Theorem 5.1 (where we treat
the additional indeterminate $Y$ as a coefficient, i.e., we apply the theorem
with $Y\in{\bm{A}}$). With this notation, we can formulate the solution of a
system in two indeterminates as follows:

###### Theorem 5.2

Consider the equation system $\mathcal{E}\colon X=P(X,Y),Y=Q(X,Y)$ with
$P,Q\in{\mathbb{S}}^{\infty}[{\bm{A}},X,Y]$. Let further

$\displaystyle H(Y)$ $\displaystyle=\operatorname{\mathbf{gfp}}(X\mapsto
P(X,Y))$ $\displaystyle\in{\mathbb{S}}^{\infty}[{\bm{A}},Y],$ $\displaystyle
b$ $\displaystyle=\operatorname{\mathbf{gfp}}(Y\mapsto Q(H(Y),Y))$
$\displaystyle\in{\mathbb{S}}^{\infty}[{\bm{A}}].$

Then $(H(b),b)$ is the greatest solution of $\mathcal{E}$.

###### Proof

It is easy to see that $(H(b),b)$ is a solution: By definition of $b$, we have
$Q(H(b),b)=b$. By definition of $H$, we further have $P(H(Y),Y)=H(Y)$, and by
applying the instantiation $Y\mapsto b$ we get $P(H(b),b)=H(b)$.

To prove that $(H(b),b)$ is the greatest solution, we make use of the
universal property. Let $(c,d)$ be any solution with
$c,d\in{\mathbb{S}}^{\infty}[{\bm{A}}]$. We claim that
$H(d)=\operatorname{\mathbf{gfp}}(X\mapsto P(X,d))$. To see this, consider the
definition of $H(Y)$ and apply the instantiation $Y\mapsto d$. By the
universal property, this instantiation is fully continuous and thus preserves
greatest fixed points.

Now, since $(c,d)$ is a solution, we have $P(c,d)=c$, and since $H(d)$ is the
greatest solution to $X=P(X,d)$, we must have $H(d)\geq c$. Then also
$Q(H(d),d)\geq Q(c,d)=d$. Since $b$ is the greatest solution to $Q(H(Y),Y)=Y$
and hence also to $Q(H(Y),Y)\geq Y$, we have $b\geq d$. Finally, $H(b)\geq
H(d)\geq c$, so $(H(b),b)$ is indeed the greatest solution. ∎

We can apply this second technique to semirings other than
${\mathbb{S}}^{\infty}[{\bm{A}}]$ by first performing a symbolic abstraction.
That is, we replace all coefficients by pairwise different indeterminates from
${\bm{A}}$, then compute the solution and apply the reverse instantiation
(which preserves solutions).

###### Example 3

Recall our example in the tropical semiring $\mathbb{T}$. By replacing
coefficients with indeterminates $a,b,c$, we obtain the equation system on the
right.

$\displaystyle X_{\\_}a$ $\displaystyle=1+_{\mathbb{R}}X_{\\_}a$
$\displaystyle X_{\\_}a$ $\displaystyle=a\cdot X_{\\_}a$ $\displaystyle
X_{\\_}b$
$\displaystyle=\min(1+_{\mathbb{R}}X_{\\_}a,20+_{\mathbb{R}}X_{\\_}c)\mathrlap{\qquad\rightsquigarrow}$
$\displaystyle X_{\\_}b$ $\displaystyle=a\cdot X_{\\_}a+b\cdot X_{\\_}c$
$\displaystyle X_{\\_}c$ $\displaystyle=0+_{\mathbb{R}}X_{\\_}c$
$\displaystyle X_{\\_}c$ $\displaystyle=c\cdot X_{\\_}c$

We solve the system over
${\mathbb{S}}^{\infty}[X_{\\_}a,X_{\\_}b,X_{\\_}c,a,b,c]$ by the symbolic
approach:

  * •

$\operatorname{\mathbf{gfp}}(X_{\\_}a\mapsto a\cdot
X_{\\_}a)=0+a^{\infty}=a^{\infty}$ (by Theorem 5.1),

  * •

$\operatorname{\mathbf{gfp}}(X_{\\_}b\mapsto a\cdot a^{\infty}+b\cdot
X_{\\_}c)=a^{\infty}+b\cdot X_{\\_}c$ (we first instantiate $X_{\\_}a$ by
$a^{\infty}$)

  * •

$\operatorname{\mathbf{gfp}}(X_{\\_}c\mapsto c\cdot X_{\\_}c)=c^{\infty}$

The greatest solution is thus $X_{\\_}a=a^{\infty}$,
$X_{\\_}b=a^{\infty}+bc^{\infty}$, $X_{\\_}c=c^{\infty}$. Applying the reverse
substitution, we get the expected solution $(\infty,20,0)$ in $\mathbb{T}$.
$\lrcorner$

Usually, the closed-form solution in Theorem 4.1 is preferable, as we can work
directly in the target semiring. The symbolic technique is best suited to
compute solutions in ${\mathbb{S}}^{\infty}[{\bm{A}}]$, which is of interest
for semiring provenance analysis. Compared to the closed-form solution, we
need slightly fewer computation steps and can often avoid an intermediate
blowup in the size of the polynomials.

###### Example 4

Recall the equation system $X_{\\_}1=b\cdot X_{\\_}2$, $X_{\\_}2=(b+c)\cdot
X_{\\_}2X_{\\_}3$, $X_{\\_}3=a\cdot X_{\\_}1$ of Example 2. Eliminating
indeterminates one by one, we get

  * •

$\operatorname{\mathbf{gfp}}(X_{\\_}1\mapsto b\cdot X_{\\_}2)=b\cdot X_{\\_}2$

  * •

$\operatorname{\mathbf{gfp}}(X_{\\_}2\mapsto(b+c)\cdot
X_{\\_}2X_{\\_}3)=\big{(}(b+c)X_{\\_}3\big{)}^{\infty}=b^{\infty}X_{\\_}3^{\infty}+c^{\infty}X_{\\_}3^{\infty}$

  * •

$\operatorname{\mathbf{gfp}}(X_{\\_}3\mapsto
ab\cdot(b^{\infty}X_{\\_}3^{\infty}+c^{\infty}X_{\\_}3^{\infty}))=a^{\infty}b^{\infty}+a^{\infty}b^{\infty}c^{\infty}=a^{\infty}b^{\infty}$

and by substituting the results backwards, we obtain
$X_{\\_}1=X_{\\_}2=X_{\\_}3=a^{\infty}b^{\infty}$. $\lrcorner$

###### Remark 4

An attentive reader may have noticed that we have phrased all results in this
section for the semiring ${\mathbb{S}}^{\infty}[{\bm{X}}]$ of absorptive
polynomials, whereas the results in [15] apply to polynomials $K[{\bm{X}}]$
over an arbitrary Kleene algebra $K$. The reason for this restrictive choice
is that the iterative lifting to multivariate equation systems in Theorem 5.2
requires some form of compositionality: in [15], $K[X,Y]$ is viewed as
$K[X][Y]$. Unfortunately, the usual notion of polynomials $K[X]$ over an
absorptive semiring $K$, as in Definition 1, is itself not absorptive, and it
seems not obvious how one would define an absorptive version of $K[X]$ (for
instance, if $a,b\in K$ are incomparable we want
$(aX+aX^{2})+bX^{2}=aX+bX^{2}$ by absorption, but also
$aX+(aX^{2}+bX^{2})=aX+(a+b)X^{2}$, violating associativity). As our proofs
rely on absorption, they do not apply to $K[X][Y]$.

Since our main result already provides a direct computation in any absorptive,
fully-continuous semiring, we have here restricted our interest to
${\mathbb{S}}^{\infty}[{\bm{X}}]$. In fact, it was this limitation that
motivated our search for a closed form solution.

###### Remark 5

For least solutions, the one-dimensional solution in Theorem 5.1 in fact
implies the solution in Theorem 4.1, as shown in [7, Prop. 28]. It seems an
interesting question if a similar connection holds for greatest solutions,
i.e., can the solution $F^{\ell}(F^{\ell}(\mathbf{1})^{\infty})$ for $\ell$
equations be derived from the solution $P(0)+P^{\prime}(1)^{\infty}$ of a
single equation by algebraic methods, without derivation trees?

##  6 Conclusion

We have presented two methods to compute least and, most importantly, greatest
solutions of polynomial equation systems over absorptive, fully-continuous
semirings. Both methods require only polynomially many applications of the
semiring operations and the infinitary power, in terms of the number of
equations.

While we assume full continuity mostly to guarantee the existence of both
kinds of solutions, absorption is a strong assumption that leads to a
particularly simple way of computing solutions. Our motivation to consider
absorptive semirings comes from semiring provenance of fixed-point logics,
where our methods can directly be applied to compute provenance information,
for example of Büchi games or formulae in fixed-point logics such as
$L_{\\_}\mu$ or LFP.

The first method, and our main result, is a closed-form solution that works in
any absorptive, fully-continuous semiring and is as easy as computing the
standard fixed-point iteration with an added application of the infinitary
power. To prove the correctness for greatest solutions, we extended the notion
of derivation trees used in the analysis of Newton’s method [6] to infinite
trees. Derivation trees provide an intuitive tool to understand the fixed-
point iteration, but require somewhat involved arguments and constructions to
properly handle infinite trees. Our main technical contribution is that it
suffices to consider trees of a particular shape resembling the solution term
$F^{\ell}(F^{\ell}(\mathbf{1})^{\infty})$, intuitively corresponding to a
reachability prefix with infinitely repeating deterministic subtrees. For the
second method, we applied results on least solutions over Kleene algebras [15]
specifically to the semiring of generalized absorptive polynomials, and
extended these results by similar observations for greatest solutions.

Comparing the two proofs, we see that the symbolic approach has a simpler
algebraic proof, raising the question whether we can avoid the constructions
of infinite trees in our main proof in favor of algebraic arguments. A further
direction for future work is to study systems of nested fixed points over
absorptive semirings. Recently, quasipolynomial-time algorithms have been
developed to solve such systems in the Boolean case [1] or over finite
lattices [14]. With the simple computation based on the fixed-point iteration,
absorptive semirings might be a candidate to further increase the
applicability of these algorithms.

#### Acknowledgements.

I would like to thank the anonymous reviewers for their helpful comments and
for suggesting related concepts, in particular [2, 7, 8] which lead to Remark
5 and Appendix 0.B.

## References

  * [1] Arnold, A., Niwiński, D., Parys, P.: A quasi-polynomial black-box algorithm for fixed point evaluation. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 183, pp. 9:1–9:23. Dagstuhl (2021). doi:10.4230/LIPIcs.CSL.2021.9
  * [2] Cohen, E.: Separation and reduction. In: Backhouse, R.C., Oliveira, J.N. (eds.) Mathematics of Program Construction. Lecture Notes in Computer Science, vol. 1837, pp. 45–59. Springer (2000). doi:10.1007/107220104
  * [3] Dannert, K., Grädel, E., Naaf, M., Tannen, V.: Generalized absorptive polynomials and provenance semantics for fixed-point logic. arXiv: 1910.07910 [cs.LO] (2019), https://arxiv.org/abs/1910.07910, full version of [4]
  * [4] Dannert, K., Grädel, E., Naaf, M., Tannen, V.: Semiring provenance for fixed-point logic. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 183, pp. 17:1–17:22. Dagstuhl (2021). doi:10.4230/LIPIcs.CSL.2021.17
  * [5] Deutch, D., Milo, T., Roy, S., Tannen, V.: Circuits for datalog provenance. In: Proc. 17th International Conference on Database Theory ICDT. pp. 201–212. OpenProceedings.org (2014). doi:10.5441/002/icdt.2014.22
  * [6] Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. Journal of the ACM 57(6), 33 (2010). doi:10.1145/1857914.1857917
  * [7] Ghilardi, S., Gouveia, M.J., Santocanale, L.: Fixed-point elimination in the intuitionistic propositional calculus. ACM Trans. Comput. Log. 21(1), 4:1–4:37 (2019). doi:10.1145/3359669
  * [8] Gondran, M., Minoux, M.: Graphs, dioids and semirings: new models and algorithms, Operations Research/Computer Science Interfaces Series, vol. 41. Springer (2008). doi:10.1007/978-0-387-75450-5
  * [9] Grädel, E., Lücking, N., Naaf, M.: Strategy analysis in büchi games by valuations in absorptive semirings. arXiv: 2106.12892 [cs.LO] (2021), https://arxiv.org/abs/2106.12892
  * [10] Grädel, E., Tannen, V.: Semiring provenance for first-order model checking. arXiv:1712.01980 [cs.LO] (2017), https://arxiv.org/abs/1712.01980
  * [11] Grädel, E., Tannen, V.: Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory 9(3), 203–228 (2020). doi:10.2140/moscow.2020.9.203
  * [12] Green, T., Karvounarakis, G., Tannen, V.: Provenance semirings. In: Principles of Database Systems PODS. pp. 31–40 (2007). doi:10.1145/1265530.1265535
  * [13] Green, T., Tannen, V.: The semiring framework for database provenance. In: Proceedings of PODS. pp. 93–99. ACM (2017). doi:10.1145/3034786.3056125
  * [14] Hausmann, D., Schröder, L.: Computing nested fixpoints in quasipolynomial time. arXiv:1907.07020 [cs.CC] (2019), https://arxiv.org/abs/1907.07020
  * [15] Hopkins, M., Kozen, D.: Parikh’s theorem in commutative Kleene algebra. In: Proceedings. 14th Symposium on Logic in Computer Science. pp. 394–401. IEEE (1999). doi:10.1109/LICS.1999.782634
  * [16] Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366–390 (1994). doi:10.1006/inco.1994.1037
  * [17] Markowsky, G.: Chain-complete posets and directed sets with applications. Algebra universalis 6(1), 53–68 (1976)
  * [18] Mohri, M.: Semiring frameworks and algorithms for shortest-distance problems. Journal of Automata, Languages and Combinatorics 7(3), 321–350 (2002). doi:10.25596/jalc-2002-321

##  Appendix 0.A Omitted Proofs

This appendix contains proofs that were omitted or only sketched in the main
paper.

###  0.A.1 Proofs of Section 2

In Remark 1, we mentioned the observation in [4] that the existence of suprema
of chains implies the existence of arbitrary surpema (and thus also arbitrary
infima so that $\leq_{\\_}K$ is a complete lattice). This follows from
arguments of Markowsky [17] on chain-complete posets: first observe that due
to idempotence, the supremum of finitely many elements is simply their sum;
suprema of finite sets and of chains then suffice to guarantee suprema of
arbitrary sets, as shown in [17, Corollary 5]. Following Markowsky’s
arguments, one can further show the following relation between suprema of
chains and sets:

###### Lemma 0.A0

Let $K_{\\_}1,K_{\\_}2$ be fully-continuous semirings. If $f\colon K_{\\_}1\to
K_{\\_}2$ preserves suprema of finite sets and of nonempty chains, then $f$
also preserves suprema of arbitrary sets.

This applies in particular to addition and multiplication with a fixed
element, as both preserve addition and hence suprema of finite sets. It
follows that in every fully-continuous semiring $K$, it holds that
$a\cdot\bigsqcup S=\bigsqcup aS$ for every $a\in K$ and every set $S\subseteq
K$. In other words, $(K,\bigsqcup,\cdot)$ is a quantale.

###### Lemma 2

Let $S\subseteq{\mathbb{S}}^{\infty}[{\bm{X}}]$ and
$P\in{\mathbb{S}}^{\infty}[{\bm{X}}]$. Then,

  1. 1.

$P\cdot\sum S=\sum\\{P\cdot Q\mid Q\in S\\}$, and

  2. 2.

$(\sum S)^{\infty}=\sum\\{Q^{\infty}\mid Q\in S\\}$, and

  3. 3.

$h(\sum S)=\sum h(S)$, if $h\colon{\mathbb{S}}^{\infty}[{\bm{X}}]\to K$ is a
fully-continuous homomorphism.

###### Proof

We recall that summation is the same as supremum in idempotent semirings.
Statement (2) was shown in [3] and the other statements follow by the same
argument: since $\sum S=\mathsf{Maximals}(\bigcup S)$, we can write $\sum S$
as finite sum $\sum S=m_{\\_}1+\dots+m_{\\_}k$ where each $m_{\\_}i$ is
contained in some $Q_{\\_}i\in S$.

For (1), we then have $P\cdot\sum S=Pm_{\\_}1+\dots+Pm_{\\_}k\leq
PQ_{\\_}1+\dots+PQ_{\\_}k\leq\sum\\{PQ\mid Q\in S\\}$ and for (3), $h(\sum
S)=h(m_{\\_}1+\dots+m_{\\_}k)=h(m_{\\_}1)+\dots+h(m_{\\_}k)\leq
h(Q_{\\_}1)+\dots+h(Q_{\\_}k)\leq\sum h(S)$. The other direction follows by
monotonicity in both cases, since $\sum S\geq Q$ for all $Q\in S$. ∎

###  0.A.2 Proofs of Section 3

######  Lemma 6 (puzzle lemma [4])

Let $X\in{\bm{X}}$ and $K={\mathbb{S}}^{\infty}[{\bm{A}}]$. Let
$(T_{\\_}n)_{\\_}{n\in\mathbb{N}}$ be a family of trees
$T_{\\_}n\in\mathcal{T}(\mathcal{E},X)$ such that their yields
$\mathsf{yd}(T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})$
form a descending chain. Then there is a tree
$T^{\prime}\in\mathcal{T}(\mathcal{E},X)$ with
$\mathsf{yd}(T^{\prime})\geq\bigsqcap_{\\_}n\mathsf{yd}(T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})$.

###### Proof

We sketch the main steps of the proof, more details can be found in [3]
(notice that our notion of truncation is simpler, as we cut off at a certain
depth instead of counting $R$-nodes).

  1. 1.

Chain splitting

Let
$e_{\\_}n(m,Y)=|{T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}}}|_{m,Y}\in{\mathbb{N}}^{\infty}$
be the number of occurrences of $m\in P_{\\_}Y$ in the tree
$T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}}$. As usual, let
$c_{\\_}{m,Y}$ be the coefficient of $m$ in $P_{\\_}Y$ so that

$y_{\\_}n\coloneqq\mathsf{yd}(T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}})=\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\
m\in P_{\\_}Y\end{subarray}}(c_{\\_}{m,Y})^{e_{\\_}n(m,Y)}.$

Using the chain splitting lemma from [3], we can write the infimum as

$\bigsqcap_{\\_}{n\in\mathbb{N}}y_{\\_}n=\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\
m\in P_{\\_}Y\end{subarray}}(c_{\\_}{m,Y})^{e(m,Y)},\qquad\text{with
}e(m,Y)\coloneqq\bigsqcup_{\\_}{n\in\mathbb{N}}e_{\\_}n(m,Y).$

  2. 2.

Problematic monomials

We say that a monomial $m\in P_{\\_}Y$ is _problematic_ if $e(m,Y)$ is finite.
Unproblematic monomials do not impose any restrictions, as they may appear
arbitrarily often (finite or infinite) in the tree $T^{\prime}$ we construct
(and $T^{\prime}$ still satisfies the desired inequality
$\mathsf{yd}(T^{\prime})\geq\bigsqcap_{\\_}ny_{\\_}n$). As the polynomial
equation system is finite, there are only finitely many problematic monomials.

  3. 3.

Decomposition into $k$-layers

We now decompose each of the trees
$T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}}$ into
$k$-layers, each of which simply consists of $k$ consecutive levels of the
tree. We choose the layers such that they cover the entire tree and do not
overlap. If $k$ is some constant, we can choose a large enough $n$ such that
there is a $k$-layer in
$T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}}$ that does not
contain any problematic monomials (as there are only finitely many).

  4. 4.

Repetition of a $k$-layer

We now construct $T^{\prime}$ by first following the tree $T_{\\_}n$ (for the
chosen $n$), but upon reaching the $k$-layer without problematic monomials, we
continue $T^{\prime}$ by repeating this layer over and over, so that no
further problematic monomials occur in $T^{\prime}$. To this end, note that
the $k$-layer is a forest consisting of several trees. We determinize each
such tree $S$ by Lemma 7 and obtain a (possibly infinite) deterministic tree
$S^{\prime}$ that we use in $T^{\prime}$ to replace $S$. To ensure that Lemma
7 can be applied, we choose $k=\ell+1$, so that each path trough the $k$-layer
must contain a repetition of indeterminates (cf. Corollary 1).

  5. 5.

Conclusion

This construction ensures that the number of occurrences of problematic
monomials in $T^{\prime}$ is bounded by their occurrences in
$T_{\\_}n\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{n}^{\mathbf{1}}$. In other
words, $|{T^{\prime}}|_{m,Y}\leq e_{\\_}n(m,Y)\leq e(m,Y)$ for all problematic
$m\in P_{\\_}Y$ and thus $|{T^{\prime}}|_{m,Y}\leq e(m,Y)$ for all
(problematic and unproblematic) $m,Y$. Hence

$\mathsf{yd}(T^{\prime})=\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\ m\in
P_{\\_}Y\end{subarray}}(c_{\\_}{m,Y})^{|{T^{\prime}}|_{m,Y}}\geq\prod_{\\_}{\begin{subarray}{c}Y\in{\bm{X}},\\\
m\in
P_{\\_}Y\end{subarray}}(c_{\\_}{m,Y})^{e(m,Y)}=\bigsqcap_{\\_}{n\in\mathbb{N}}y_{\\_}n.$

###  0.A.3 Proofs of Section 4

###### Corollary 1

For each $T\in\mathcal{T}(\mathcal{E},X)$, there is a deterministic tree
$T^{\prime}\in\mathcal{T}(\mathcal{E},X)$ such that
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}\leq\mathsf{yd}(T^{\prime})^{\infty}$.

###### Proof

We use Lemma 7 to construct a deterministic tree $T^{\prime}$ with
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}\leq\mathsf{yd}(T^{\prime})^{\infty}$
as follows. We define ${\bm{X}}_{\\_}0$ and monomials $m_{\\_}X$ for
$X\in{\bm{X}}_{\\_}0$ inductively by traversing the tree $T$ level by level,
starting with the root. We always maintain the following invariant: after
traversing level $k$, all indeterminates occurring in $m_{\\_}X$ for
$X\in{\bm{X}}_{\\_}0^{(k)}$ are contained in ${\bm{X}}_{\\_}0^{(k)}$ or occur
at level $k+1$ in $T$.

For level $0$ (consisting only of the root with
$\mathsf{var}(\varepsilon)=X$), we set ${\bm{X}}_{\\_}0^{(0)}\coloneqq\\{X\\}$
and $m_{\\_}X\coloneqq\mathsf{mon}(\varepsilon)$. The invariant holds due to
the children of $\varepsilon$. Assume we have processed level $k$. Let
${\bm{X}}_{\\_}{\text{todo}}^{(k)}$ be the set of indeterminates that occur in
$m_{\\_}X$ for $X\in{\bm{X}}_{\\_}0^{(k)}$, but are not contained in
${\bm{X}}_{\\_}0^{(k)}$. If ${\bm{X}}_{\\_}{\text{todo}}^{(k)}=\varnothing$,
we are done. Otherwise, for each $Y\in{\bm{X}}_{\\_}{\text{todo}}^{(k)}$,
there is a node $v$ at level $k+1$ with $\mathsf{var}(v)=Y$ by the invariant.
Choose any such node and set $m_{\\_}Y\coloneqq\mathsf{mon}(v)$. By definition
of derivation trees, all indeterminates of $m_{\\_}Y$ occur as children of $v$
on level $k+2$, so the invariant holds. Then set
${\bm{X}}_{\\_}0^{(k+1)}\coloneqq{\bm{X}}_{\\_}0^{(k)}\cup{\bm{X}}_{\\_}{\text{todo}}^{(k)}$.

This process never enters level $\ell$: On each level, at least one
indeterminate is added to ${\bm{X}}_{\\_}0^{(k)}$ (or we stop) and there are
only $\ell$ different indeterminates. Hence all monomials $m_{\\_}X$ we choose
occur in the truncation
$T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}}$. Now obtain
$T^{\prime}$ by applying Lemma 7 to $\bigcup_{\\_}k{\bm{X}}_{\\_}0^{(k)}$ and
the chosen monomials $m_{\\_}X$. The inequality
$\mathsf{yd}(T\scalebox{1.0}[1.3]{$\|$}\vphantom{|}_{\ell}^{\mathbf{1}})^{\infty}\leq\mathsf{yd}(T^{\prime})^{\infty}$
follows by Lemma 4.

##  Appendix 0.B On an Axiomatization of the Infinitary Power

This appendix discusses an axiomatization of the infinitary power operation
$a^{\infty}$ in absorptive semirings, similar to Cohen’s $\omega$-algebras
[2]. To justify the new axioms, we derive the common properties of the
infinitary power and provide a completeness result.

###### Definition 13

An _∞ -algebra_ is an algebraic structure $(K,+,\cdot,{}^{\infty},0,1)$ such
that $(K,+,\cdot,0,1)$ is an absorptive semiring and the following axioms
hold:

$\displaystyle a^{\infty}$ $\displaystyle=aa^{\infty}$ ($\infty$ abs)
$\displaystyle b\leq c+ab\;$ $\displaystyle\to\;b\leq c+a^{\infty}b$ ($\infty$
ind)

where $\leq$ denotes the natural order.

We remark that every ∞-algebra is in particular a Kleene algebra (see e.g.
[16]) by setting $a^{*}=1$ for all $a\in K$. For a complete axiomatization, we
can thus use axioms (3) – (13) of [16] together with commutativity $ab=ba$,
absorption $1+a=1$ and the ∞-axioms. Moreover, every ∞-algebra is also an
$\omega$-algebra by setting $a^{\omega}=a^{\infty}$, since ($\infty$ ind) and
absorption imply Cohen’s axiom

$b\leq c+ab\;\to\;b\leq a^{*}c+a^{\infty}.$

Clearly, every absorptive, fully-continuous semiring is an ∞-algebra (by
defining $a^{\infty}$ as in Definition 5), since ($\infty$ ind) holds by Lemma
12 and ($\infty$ abs) follows from continuity:
$aa^{\infty}=a\cdot\bigsqcap_{\\_}na^{n}=\bigsqcap_{\\_}na^{n+1}=a^{\infty}$.
Conversely, we show how to derive the main properties of the infinitary power
in such semirings from the axioms in Definition 13. The first lemma provides
an alternative proof of Lemma 11 (3) and implies that ∞ is monotone w.r.t.
$\leq$ (using $c=1$).

###### Lemma 0.B0

Every ∞-algebra satisfies the implication

$ac\leq bc\;\to\;a^{\infty}c\leq b^{\infty}c.$

###### Proof

Using ($\infty$ abs) and the assumption, we get $a^{\infty}c=a^{\infty}ac\leq
a^{\infty}bc$. By absorption, we thus have $a^{\infty}c\leq b(a^{\infty}c)\leq
b(a^{\infty}c)+b^{\infty}c$. Applying ($\infty$ ind) and absorption then gives
$a^{\infty}c\leq b^{\infty}(a^{\infty}c)+b^{\infty}c=b^{\infty}c$ as claimed.
∎

###### Lemma 0.B0

In every ∞-algebra, ∞ has the following properties:

  1. 1.

$a^{n}\geq a^{\infty}$ and $a^{n}a^{\infty}=a^{\infty}$, for all
$n\in\mathbb{N}$,

  2. 2.

$a^{\infty}a^{\infty}=a^{\infty}$,

  3. 3.

$(a^{\infty})^{\infty}=a^{\infty}$,

  4. 4.

$(ab)^{\infty}=a^{\infty}b^{\infty}$,

  5. 5.

$(a+b)^{\infty}=a^{\infty}+b^{\infty}$.

###### Proof

  1. 1.

Follows inductively from ($\infty$ abs) and absorption.

  2. 2.

Trivially $a^{\infty}a^{\infty}\leq a^{\infty}$ by absorption. For the other
direction, we have $a^{\infty}\leq aa^{\infty}$ by ($\infty$ abs) and thus
$a^{\infty}\leq a^{\infty}a^{\infty}$ by ($\infty$ ind).

  3. 3.

By ($\infty$ abs) and absorption,
$(a^{\infty})^{\infty}=a^{\infty}\cdot(a^{\infty})^{\infty}\leq a^{\infty}$.
Conversely, $a^{\infty}\leq a^{\infty}a^{\infty}$ by (2) and thus
$a^{\infty}\leq(a^{\infty})^{\infty}a^{\infty}\leq(a^{\infty})^{\infty}$ by
($\infty$ ind) and absorption.

  4. 4.

We have $a^{\infty}b^{\infty}\leq(ab)a^{\infty}b^{\infty}$ by ($\infty$ abs)
and thus
$a^{\infty}b^{\infty}\leq(ab)^{\infty}a^{\infty}b^{\infty}\leq(ab)^{\infty}$
by ($\infty$ ind) and absorption. For the other direction, we observe that
$(ab)^{\infty}=ab(ab)^{\infty}\leq a(ab)^{\infty}$ by ($\infty$ abs) and
absorption. Hence $(ab)^{\infty}\leq a^{\infty}(ab)^{\infty}$ by ($\infty$
ind) and symmetrically, $(ab)^{\infty}\leq b^{\infty}(ab)^{\infty}$. Combining
both, we get $(ab)^{\infty}\leq a^{\infty}b^{\infty}(ab)^{\infty}\leq
a^{\infty}b^{\infty}$, with absorption in the last step.

  5. 5.

By monotonicity, $a+b\geq a,b$ implies $(a+b)^{\infty}\geq
a^{\infty},b^{\infty}$ and thus $(a+b)^{\infty}\geq a^{\infty}+b^{\infty}$ by
idempotence (addition is supremum). Conversely, we have
$(a+b)^{\infty}=a(a+b)^{\infty}+b(a+b)^{\infty}$ by ($\infty$ abs). Thus
$(a+b)^{\infty}\leq a^{\infty}(a+b)^{\infty}+b^{\infty}(a+b)^{\infty}\leq
a^{\infty}+b^{\infty}$ by applying ($\infty$ ind) twice, with absorption in
the last step. ∎

The above lemmas provide a sanity check for our axiomatization. It is further
easy to see that we cannot omit ($\infty$ abs) or ($\infty$ ind), as the
remaining axiom would be satisfied by either $a^{\infty}=a$ or $a^{\infty}=0$,
which, in general, violates the property $a^{\infty}=\bigsqcap_{\\_}na^{n}$ we
want to axiomatize. To further justify our axioms, we observe the following
straightforward completeness result.

###### Proposition 0.B0

Let $\alpha,\beta$ be two terms constructed from variables, the constants $0$
and $1$, and the operations $+$, $\cdot$ and ∞. Then, $\alpha=\beta$ holds in
every absorptive, fully-continuous semiring if, and only if, it holds in every
∞-algebra.

###### Proof

One implication is trivial, since every absorptive, fully-continuous semiring
is an ∞-algebra. For the converse, assume that $\alpha=\beta$ holds in every
absorptive, fully-continuous semiring. We show that we can derive
$\alpha=\beta$ from the ∞-axioms and the properties of absorptive semirings.

Using Lemma 0.B0 and distributivity, we can rewrite each term into a sum of
monomials (where we allow $\infty$ as exponent). We can thus derive equalities
of the form $\alpha=m_{\\_}1+\dots+m_{\\_}k$ and
$\beta=m_{\\_}1^{\prime}+\dots+m^{\prime}_{\\_}l$. Let ${\bm{X}}$ be the set
of variables occurring in $\alpha$ and $\beta$. We can then view
$P_{\\_}\alpha\coloneqq m_{\\_}1+\dots+m_{\\_}k$ and $P_{\\_}\beta\coloneqq
m_{\\_}1^{\prime}+\dots+m^{\prime}_{\\_}l$ as absorptive polynomials in
${\mathbb{S}}^{\infty}[{\bm{X}}]$. Since $\alpha=\beta$ and hence
$P_{\\_}\alpha=P_{\\_}\beta$ holds in every absorptive, fully-continuous
semiring, it also holds in ${\mathbb{S}}^{\infty}[{\bm{X}}]$. That is,
$\mathsf{Maximals}\\{m_{\\_}1,\dots,m_{\\_}k\\}=\mathsf{Maximals}\\{m_{\\_}1^{\prime},\dots,m^{\prime}_{\\_}l\\}$.

To prove that we can derive
$P_{\\_}\alpha=\sum\mathsf{Maximals}\\{m_{\\_}1,\dots,m_{\\_}k\\}$, and
analogously for $P_{\\_}\beta$, it suffices to show that whenever $m\succeq
m^{\prime}$ holds for two monomials in ${\mathbb{S}}^{\infty}[{\bm{X}}]$, we
can derive $m\geq m^{\prime}$ from the axioms. Since $\cdot$ is monotone and
${\bm{X}}$ finite, we can reason about each variable in $m,m^{\prime}$
separately. Now assume that $X^{a}\succeq X^{b}$, so $a\leq b$. If
$a,b<\infty$, we can derive $X^{a}\geq X^{b}$ by absorption. If $b=\infty$,
then we can derive $X^{a}\geq X^{b}$ using Lemma 0.B0. It follows that
$P_{\\_}\alpha=P_{\\_}\beta$ and hence $\alpha=\beta$ holds in every
∞-algebra. ∎