[labelstyle=]

# Convergence of Datalog over (Pre-) Semirings

Mahmoud Abo Khamis relationalAI USA ,  Hung Q. Ngo relationalAI USA ,
Reinhard Pichler TU Wien Austria ,  Dan Suciu University of Washington USA and
Yisu Remy Wang University of Washington USA

(2022; Date: December 2020)

###### Abstract.

Recursive queries have been traditionally studied in the framework of datalog,
a language that restricts recursion to monotone queries over sets, which is
guaranteed to converge in polynomial time in the size of the input. But modern
big data systems require recursive computations beyond the Boolean space. In
this paper we study the convergence of datalog when it is interpreted over an
arbitrary semiring. We consider an ordered semiring, define the semantics of a
datalog program as a least fixpoint in this semiring, and study the number of
steps required to reach that fixpoint, if ever. We identify algebraic
properties of the semiring that correspond to certain convergence properties
of datalog programs. Finally, we describe a class of ordered semirings on
which one can use the semi-naive evaluation algorithm on any datalog program.

Datalog; Semirings; Fixpoint

††journalyear: 2022††copyright: rightsretained††conference: Proceedings of the
41st ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems; June
12–17, 2022; Philadelphia, PA, USA††booktitle: Proceedings of the 41st ACM
SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS ’22),
June 12–17, 2022, Philadelphia, PA, USA††doi: 10.1145/3517804.3524140††isbn:
978-1-4503-9260-0/22/06††ccs: Theory of computation Database query languages
(principles)

##  1\. Introduction

Traditionally, database systems have focused on non-recursive (loop-free)
queries. However, modern data processing and tensor computations require
iteration and fixpoint computation. Some systems, like Spark
(DBLP:journals/cacm/ZahariaXWDADMRV16, ), have iteration embedded natively,
while others, like Tensorflow (DBLP:conf/osdi/AbadiBCCDDDGIIK16, ) are
routinely run by a driver, e.g. in order to iterate the computation until
convergence.

Theoretically, the database community has studied the evaluation and
optimization problem for iterative programs in the context of datalog
(DBLP:books/aw/AbiteboulHV95, ), a language that restricts recursion to
monotone queries over sets. However, today’s applications need to iterate
expressions that are not monotone queries over sets. For example standard
tensor operations (e.g. Einsum, convolution) are not monotone w.r.t. set
inclusion. Even some purely relational problems such as computing betweenness
centrality (Freeman1977Set, ) or all-pairs shortest paths (APSP) (MR2572804, )
require algebraic computations, and thus are not monotone in the datalog-
sense.

Recursive computations beyond the Boolean space lead to three major
challenges. First, non-monotonicity of general aggregations leads to difficult
semantic conundra (liu2020recursive, ; DBLP:journals/logcom/LiuS20, ). Second,
finite convergence behavior of the computation is no longer easy to be swept
under the rug (see examples below). Third, computational optimization
techniques developed for datalog, such as semi-naïve evaluation
(DBLP:books/aw/AbiteboulHV95, ), break beyond the confine of Boolean
monotonicity.

To address the demand for more expressive computations, this paper introduces
the language $\text{\sf datalog}^{\circ}$, pronounced datalogo, which allows
for expressing recursive computations over general semirings. $\text{\sf
datalog}^{\circ}$ is powerful in that it can be used to express problems such
as transitive closure, all-pairs shortest-paths (APSP), minimum spanning tree
(MST), or computing a local minimum of a (class of) optimization problem(s).
To address the challenges, we equip $\text{\sf datalog}^{\circ}$ with a
natural (least fixpoint) semantics, study convergence behavior of $\text{\sf
datalog}^{\circ}$ programs, and generalize semi-naïve evaluation to work over
semirings (modulo specific assumptions). In what follows, we informally
describe $\text{\sf datalog}^{\circ}$ and how we took steps towards addressing
the challenges.

#### Expressiveness

A Datalog program is a collection of (unions of) conjunctive queries,
operating on relations. Analogously, a $\text{\sf datalog}^{\circ}$ program is
a collection of (sum-)sum-product queries over a (pre-) semiring, operating on
$S$-relations.111The notion of K-relations was introduced by Green et al.
(DBLP:conf/pods/GreenKT07, ); we prefer to call them $S$-relations in this
paper where $S$ stands for “semiring”. An $S$-relation is a function from the
set of tuples to a semiring $S$, which is a set equipped with two operations,
$\oplus$ and $\otimes$, and relational algebra extends naturally to
$S$-relations.

###### Example 1.1.

A real-valued matrix $A$ is an $\mathbb{R}$-relation, where each tuple
$A(i,j)$ has the value $a_{ij}$; and, $\mathbb{R}$ denotes the sum-product
semiring $(\mathbb{R},+,\cdot,0,1)$. Both the objective and gradient of the
ridge linear regression problem $\min_{x}J(x)$, with
$J(x)=\frac{1}{2}\|Ax-b\|^{2}+(\lambda/2)\|x\|^{2}$, are expressible in
$\text{\sf datalog}^{\circ}$, because they are sum-sum-product queries. The
gradient $\mbox{\boldmath$\nabla$}J(x)=A^{\top}Ax-A^{\top}b+\lambda x$, for
example, is the following sum-sum-product query:

$\displaystyle\mbox{\boldmath$\nabla$}(i)=\sum_{j}\sum_{k}a(k,i)\cdot
a(k,j)\cdot x(j)+\sum_{j}(-1)\cdot a(j,i)\cdot b(j)+\lambda()\cdot x(i)$

The gradient has the same dimensionality as $x$; the group by variable is $i$.
Gradient descent is an algorithm to solve for the solution of
$\mbox{\boldmath$\nabla$}J(x)=0$, or equivalently to solve for a fixpoint
solution to the $\text{\sf datalog}^{\circ}$ program $x=f(x)$ where
$f(x)=\mbox{\boldmath$\nabla$}J(x)+x$.

###### Example 1.2.

The APSP problem is to compute the shortest path length $P(x,y)$ between any
pair $x,y$ of vertices in the graph, given the length $E(x,y)$ of edges in the
graph. The value-space of $E(x,y)$ can be the reals $\mathbb{R}$ or the non-
negative reals $\mathbb{R}_{+}$. The APSP problem in $\text{\sf
datalog}^{\circ}$ can be expressed very compactly as

(1) $\displaystyle P(x,y)$ $\displaystyle\text{ :-
}E(x,y)\oplus\bigoplus_{z}P(x,z)\otimes E(z,y),$

where $(\oplus,\otimes)=(\min,+)$ are the “addition” and “multiplication”
operators in one of the $\min$-$+$ tropical semirings $\text{\sf
Trop}:=(\mathbb{R}\cup\\{\infty\\},\min,+,\infty,0)$, or $\text{\sf
Trop}^{+}:=(\mathbb{R}_{+}\cup\\{\infty\\},\min,+,\infty,0)$. Here
$\mathbb{R}_{+}$ denotes the set of non-negative reals.

By changing the semiring, $\text{\sf datalog}^{\circ}$ is able to express
similar problems in exactly the same way. For example, (1) becomes transitive
closure over the Boolean semiring, top $p$-shortest-paths over the $\text{\sf
Trop}^{+}_{p}$ semiring (semiring_book, ) (see Example 4.6), and so forth.

#### Semantics

It should be clear that $\text{\sf datalog}^{\circ}$ is very powerful.
Unfortunately, “with great power comes great responsibility”. In Datalog, the
least fixpoint semantics was defined w.r.t. set inclusion
(DBLP:books/aw/AbiteboulHV95, ). Generalizing to semirings, Green at
al.(DBLP:conf/pods/GreenKT07, ) observed that, in order to define the
semantics of datalog over S-relations, one needs a partial order,
$\sqsubseteq$, because the least fixpoint is defined w.r.t. some partial
order. They proposed to use semirings which are naturally ordered, where
$x\sqsubseteq y$ is defined as $\exists z:x+z=y$. However, some important
semirings are not naturally ordered. For example, $(\mathbb{R},+,\times,0,1)$
is not naturally ordered, because the relation $\exists z:x+z=y$ is not anti-
symmetric: for any $x\neq y$ there is a $z$ where $x+z=y$ and $y+(-z)=x$. This
means recursive programs over arrays, matrices, or tensors cannot be
interpreted using the framework in (DBLP:conf/pods/GreenKT07, ).

In $\text{\sf datalog}^{\circ}$ we decouple the semiring structure from the
partial order. We define a partially ordered, pre-semiring222A pre-semiring is
a semiring without the axiom $x\otimes 0=0\otimes x=0$ (semiring_book, ); see
Sec. 2., denoted by POPS, to be any pre-semiring with a partial order, where
both $\oplus$ and $\otimes$ are monotone operations. The value-space of every
$S$-relation is some partially ordered pre-semiring.

In some cases, e.g. the Booleans, the partial order of POPS is the natural
one, but in other cases it is not. For example, we can define a non-standard
order relation on $\mathbb{R}$ by adding a new element,
$\mathbb{R}_{\bot}\stackrel{{\scriptstyle\text{def}}}{{=}}\mathbb{R}\cup\\{\bot\\}$,
and defining $\bot\sqsubseteq x$ for all $x$. The set $\mathbb{R}_{\bot}$ is
called the lifted reals, and we can use it to define a semantics for recursive
programs over vectors, matrices, or tensors. Adding $\perp$ to create a
partial order is the standard approach for defining the semantics in general
programming languages (Scott71towarda, ). In logic programming, Fitting
(DBLP:journals/jlp/Fitting85a, ) proposed adding $\perp$, leading to the
$3$-valued semantics of logic programs with negation.

With the partial order in place, we define the semantics of a $\text{\sf
datalog}^{\circ}$ program as the least fixpoint of the immediate consequence
operator. $\text{\sf datalog}^{\circ}$ subsumes traditional datalog semantics,
and captures the semantics of complex, recursive computations over vectors,
matrices, tensors, etc.

#### Finite Convergence

Example 1.1 hinted at the difficulty with computing the exact least fixpoint
solution in a general POPS, even when we know that the fixpoint exists. In
practice, numerical optimization problems are often only solved approximately.
This, in principle, remains true with $\text{\sf datalog}^{\circ}$. However,
here we concentrate on ways to compute the exact least fixpoint solution in a
finite number of steps. In particular, we focus on analyzing the number of
iterations needed for the naïve evaluation algorithm333Repeatedly apply the
equation until a fixpoint is reached to converge.

Note that the infinite cardinality of the semiring value-space is not the
reason why a $\text{\sf datalog}^{\circ}$ program does not converge when
iterated naïvely. For example, intuitively we know that the naïve algorithm
for the APSP program (1) may not converge under Trop (due to negative cycles),
but it will always converge under $\text{\sf Trop}^{+}$. This paper makes this
intuitive observation precise: we extract algebraic properties of the POPS
which serve as sufficient conditions under which the naïve algorithm for
$\text{\sf datalog}^{\circ}$ converges in a finite number of steps.
Furthermore, under additional assumptions, we show that the naïve algorithm
converges in poly-time. These results subsume the corresponding results in
traditional Datalog.

For example, our results imply that while the naïve algorithm for (1) may not
converge under Trop, it converges in a linear number of steps if the semiring
is $\text{\sf Trop}^{+}$ or more generally $\text{\sf Trop}^{+}_{p}$. The
property satisfied by $\text{\sf Trop}^{+}$ but not Trop is $\bm{1}\oplus
a=\bm{1}$ for every element $a$ in the value-space and $\bm{1}$ is the
multiplicative identity. Less formally, this says $\min(a,0)=0$ for all
$a\in\mathbb{R}_{+}\cup\\{\infty\\}$.

Beyond the naïve algorithm, we show that the approach of generalizing Gaussian
elimination to closed semirings (MR1059930, ; DBLP:journals/tcs/Lehmann77, )
works for $\text{\sf datalog}^{\circ}$ under POPS too; this leads to
essentially a cubic time algorithm to find a least fixpoint of a linear
$\text{\sf datalog}^{\circ}$ program.

#### Optimization

Semi-naïve evaluation is one of the major optimization techniques for
evaluating Datalog, which we would like to generalize to $\text{\sf
datalog}^{\circ}$. To explain the main ideas, let us consider the Boolean
semiring version of (1):

(2) $\displaystyle P(x,y)$ $\displaystyle\text{ :-
}E(x,y)\vee\bigvee_{z}P(x,z)\wedge E(z,y).$

After initializing $P_{0}(x,y)=\delta_{0}(x,y)=\emptyset$, at the $t$th
iteration semi-naïve evaluation does the following:

(3) $\displaystyle\delta_{t}(x,y)$
$\displaystyle=\left(E(x,y)\vee\bigvee_{z}\delta_{t-1}(x,z)\wedge
E(z,y)\right)\setminus P_{t-1}(x,y)$ (4) $\displaystyle P_{t}(x,y)$
$\displaystyle=P_{t-1}(x,y)\cup\delta_{t}(x,y).$

Furthermore, starting from iteration $t=2$ onwards, we can simplify (3)
further by removing the base-case $E(x,y)$ because we know $E(x,y)\subseteq
P_{t-1}(x,y)$ for $t\geq 2$:

(5) $\displaystyle\delta_{t}(x,y)$
$\displaystyle=\left(\bigvee_{z}\delta_{t-1}(x,z)\wedge E(z,y)\right)\setminus
P_{t-1}(x,y).$

Without these optimizations, we will have rederived a lot of facts in each
iteration. Under $\text{\sf datalog}^{\circ}$, we are able to generalize the
above ideas by defining an appropriate “minus” $\ominus$ operator for certain
semirings that plays the role of the $\setminus$ operator in (3), and we show
that for $\ominus$, both the semi-naïve evaluation step (3) and the base-case
removal optimization (5) hold for general $\text{\sf datalog}^{\circ}$
programs.

###### Example 1.3 (Shortest paths).

The APSP problem is 1 under Trop, where the analog of (5) is:

(6) $\displaystyle\delta_{t}(x,y)$
$\displaystyle=(\min_{z}\delta_{t-1}(x,z)+E(z,y))\ominus P_{t-1}(x,y),$

where the difference operator $\ominus$ is defined later in the paper (23).
Intuitively, the $\ominus$ operator does what we expect: from the new shortest
paths from $x$ to $z$ discovered in the previous iteration, we see if adding a
$(z,y)$ edge gives us a shorter path from $x$ to $y$; if so, we update the
shortest path from $x$ to $y$.

#### Paper organization

Section 2 presents basic concepts on semirings and defines (sum-)sum-product
queries under semirings. Section 3 studies the stability of vector-valued
monotone functions over posets. (Stability of a function is the number of its
applications until a fixpoint is reached.) This fundamental result serves as a
basis for analyzing finite convergence of the naïve algorithm for $\text{\sf
datalog}^{\circ}$. Section 5 formulates the concept of partially preordered
semirings (POPS), which form value-spaces of $\text{\sf datalog}^{\circ}$
programs. It formally defines the syntax for $\text{\sf datalog}^{\circ}$
programs, and introduces the fixpoint semantics of $\text{\sf
datalog}^{\circ}$. A range of possible convergence behaviors of $\text{\sf
datalog}^{\circ}$ programs is studied in Section 6. Section 7 presents a
generalization of semi-naïve evaluation to $\text{\sf datalog}^{\circ}$.

##  2\. Background on Semirings

A pre-semiring (semiring_book, ) is a tuple $\bm{S}=(S,\oplus,\otimes,0,1)$
where $\oplus$ and $\otimes$ are binary operators on $S$ for which
$(S,\oplus,0)$ is a commutative monoid, $(S,\otimes,1)$ is a monoid, and
$\otimes$ distributes over $\oplus$. When $\oplus$ is commutative, then we say
that the pre-semiring is commutative. In this paper we only consider
commutative pre-semirings, and we will simply refer to them as pre-semirings.
When the absorption rule $x\otimes 0=0$ holds for all $x\in S$, we call
$\bm{S}$ a semiring.444Some references, e.g. (DBLP:journals/ai/KohlasW08, ),
define a semiring without absorption.

Common examples are the Booleans
$(\mathbb{B}\stackrel{{\scriptstyle\text{def}}}{{=}}\\{0,1\\},\vee,\wedge,0,1)$,
and sum-product semirings over natural $(\mathbb{N},+,\times,0,1)$ or real
numbers $(\mathbb{R},+,\times,0,1)$. We will refer to them simply as
$\mathbb{B},\mathbb{N}$ and $\mathbb{R}$. Other useful examples were
introduced in Example 1.2: Trop and $\text{\sf Trop}^{+}$. We will illustrate
more semirings in this paper, and also refer the reader to (semiring_book, )
for many more examples.

Fix a pre-semiring $\bm{S}=(S,\oplus,\otimes,0,1)$ and a finite domain $D$;
for example $D$ could be the set $[n]=\\{1,\ldots,n\\}$, or some finite set of
identifiers. An $\bm{S}$-relation is a function $R:D^{k}\rightarrow S$. The
set $D^{k}$ is called the key-space, $S$ is the value-space, and $k$ is the
arity of $R$. The type of $R$ is $D^{k}\rightarrow\bm{S}$. If $\bm{t}\in
D^{k}$ is a tuple of constants, then we call the expression $R(\bm{t})$ a
ground atom. Equivalently, we can view an $\bm{S}$-relation as a mapping from
ground atoms to $S$. Fix a semiring $\bm{S}$ and a vocabulary
$\mathcal{R}=\\{R_{1},R_{2},\ldots\\}$ of relation names, where each relation
$R_{j}$ has type $D^{k_{j}}\to S$.

###### Definition 2.1.

Let $x_{1},\ldots,x_{p}$ be a set of variables, taking values in the domain
$D$. A sum-product query is an expression of the form

(7) $\displaystyle T(x_{1},\ldots,x_{k})$ $\displaystyle\text{ :-
}\bigoplus_{x_{k+1},\ldots,x_{p}\in D}A_{1}\otimes\cdots\otimes A_{m}$

where each $A_{u}$ is either a relational atom,
$R_{i}(x_{t_{1}},\ldots,x_{t_{k_{i}}})$, or an equality predicate,
$[x_{t}=x_{s}]$; the variables $x_{1},\ldots,x_{k}$ are called free variables,
and the others are called bound variables. The body of the query (RHS of (7))
is a sum-product expression.

A sum-sum-product query has the form:

(8) $\displaystyle Q(x_{1},\ldots,x_{k})$ $\displaystyle\text{ :-
}T_{1}(x_{1},\ldots,x_{k})\oplus\cdots\oplus T_{q}(x_{1},\ldots,x_{k})$

where $T_{1},T_{2},\ldots,T_{q}$ are sum-product expressions with the same
free variables $x_{1},\ldots,x_{k}$.

When the value-space $\bm{S}$ is the Boolean semiring, then a sum-product
query is a Conjunctive Query (CQ) under set semantics, and a sum-sum-product
query is a Union of Conjunctive Queries (UCQ). When $\bm{S}=\mathbb{N}$, then
they are a CQ or UCQ under bag semantics; and when $\bm{S}=\mathbb{R}$ then a
sum-product expression is a tensor expression, sometimes called an Einsum
(einsum:rocktaschel, ).

The semantics of (7) is the following. The value of each ground atom
$T(\bm{t})$ is defined as the (finite!) sum on the right, where we substitute
the variables $x_{1},\ldots,x_{k}$ with the constants in the tuple $\bm{t}$.
The semantics of (8) is the sum of terms on the right.

The problem of computing efficiently (sum-)sum-products over semirings has
been extensively studied both in the database and in the AI literature. In
databases, the query optimization and evaluation problem is a special case of
sum-sum-product computation over the value-space of Booleans (set semantics)
or natural numbers (bag semantics). The functional aggregate queries (FAQ)
framework (DBLP:conf/pods/KhamisNR16, ) extends the formulation to queries
over multiple semirings. In AI, this problem was studied by Shenoy and Schafer
(DBLP:conf/uai/ShenoyS88, ), Dechter (DBLP:journals/constraints/Dechter97, ),
Kohlas and Wilson (DBLP:journals/ai/KohlasW08, ) and others. Surveys and more
examples can be found in (DBLP:journals/tit/AjiM00, ;
DBLP:books/daglib/0008195, ).

###### Remark 2.2.

The notation pair $(\oplus,\otimes)$ helps reduce confusion when we discuss
semirings such as the a tropical semiring where $\min$ is $\oplus$ and $+$ is
$\otimes$. However, $\oplus$ and $\otimes$ are quite cumbersome to parse;
thus, in the rest of this paper we will mostly use $+$ and $\circ$ instead of
$(\oplus,\otimes)$ to lighten the notational density. Furthermore, just as
with arithmetic multiplication, we will also sometimes drop $\circ$, writing
$ab$ for $a\circ b$ for instance.

##  3\. Least Fixpoints over Product Spaces

We review partially ordered sets and present two technical results that allow
us to prove the convergence of $\text{\sf datalog}^{\circ}$ programs.

Fix a partially ordered set (poset), $\bm{L}=(L,\sqsubseteq)$. In this paper
we will assume that each poset has a minimum element $\bot$, unless otherwise
specified. We denote by $\bigvee A$, or $\bigwedge A$ respectively, the least
upper bound, or greatest lower bound of a set $A\subseteq L$, when it exists.
A function $f$ between two posets is called monotone if $x\sqsubseteq y$
implies $f(x)\sqsubseteq f(y)$, and is called strict if $f(\bot)=\bot$.

Given a monotone function $f\colon\bm{L}\rightarrow\bm{L}$, a fixpoint is an
element $x$ such that $f(x)=x$. We denote by $\text{\sf lfp}_{\bm{L}}(f)$ the
least fixpoint of $f$, when it exists, and drop the subscript $\bm{L}$ when it
is clear from the context. Consider the following $\omega$-sequence:

(9) $\displaystyle f^{(0)}(\bot)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\bot$ $\displaystyle
f^{(n+1)}(\bot)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
f(f^{(n)}(\bot))$

If $x$ is any fixpoint of $f$, then $f^{(n)}(\bot)\sqsubseteq x$ (by induction
on $n$). There are several restrictions on the poset $\bm{L}$ and/or function
$f$ that ensure that $\bigvee_{n}f^{(n)}(\bot)$ is the least fixpoint of $f$,
see (davey1990introduction, ). The most common restriction is for $f$ to be
monotone and $\omega$-continuous: the least fixpoint exists due to Kleene’s
theorem. This line was studied extensively in the formal language literature
(MR1470001, ; DBLP:conf/popl/CousotC77, ). In the database literature, Green
et al. (DBLP:conf/pods/GreenKT07, ) require the semiring to be naturally
ordered ($\bm{L}$ captures the order) and $\omega$-continuous in order to give
a semantics to datalog programs over semirings.

In this paper we are interested in conditions that ensure that the sequence
(9) reaches a fixpoint after a finite number of steps, and for this reason we
introduce here two alternative conditions. An $\omega$-chain in a poset
$\bm{L}$ is a sequence $x_{0}\leq x_{1}\leq\ldots$ We say that the chain is
finite if there exists $n_{0}$ such that
$x_{n_{0}}=x_{n_{0}+1}=x_{n_{0}+2}=\cdots$; equivalently, $x_{n_{0}}=\bigvee
x_{n}$.

###### Definition 3.1 (ACC).

A poset $\bm{L}$ satisfies the Ascending Chain Condition, or ACC (MR1728440,
), if it has no infinite $\omega$-chains. The rank of a strictly increasing
chain $x_{0}<x_{1}<\cdots<x_{k}$ is $k$. We say that $\bm{L}$ has rank $k$ if
every strictly increasing chain has rank $\leq k$ (MR2868112, ).

###### Definition 3.2.

A monotone function $f$ on $\bm{L}$ (i.e. $f\colon\bm{L}\rightarrow\bm{L}$) is
called $p$-stable if $f^{(p+1)}(\bot)=f^{(p)}(\bot)$. The stability index of
$f$ is the minimum $p$ for which $f$ is $p$-stable. The function $f$ is said
to be stable if it is $p$-stable for some $p\geq 0$.

If $\bm{L}$ has rank $k$ then every monotone function $f$ is $k$-stable. If
ACC holds, then every monotone $f$ is stable. If a function $f$ is $p$-stable,
then it has a least fixpoint and $\text{\sf lfp}(f)=f^{(p)}(\bot)$.

In this paper we need to compute the least fixpoint of functions over product
spaces, $\bm{L}_{1}\times\bm{L}_{2}$, or $\bm{L}^{D}$ for some set $D$,
ordered pointwise. The ACC immediately extends to products
(davey1990introduction, ):

######  Proposition 3.3.

Suppose posets $\bm{L}_{1},\bm{L}_{2},\bm{L}$ satisfy ACC. Then
$\bm{L}_{1}\times\bm{L}_{2}$ satisfies ACC. If $D$ is finite, $\bm{L}^{D}$
also satisfies ACC. If $\bm{L}_{1},\bm{L}_{2},\bm{L}$ have ranks
$k_{1},k_{2},k$ then $\bm{L}_{1}\times\bm{L}_{2}$ has rank $k_{1}+k_{2}$ and
$\bm{L}^{D}$ has rank $k\cdot|D|$.

Next, we consider stability of functions over product spaces. We start by
considering two posets, $\bm{L}_{1},\bm{L}_{2}$, and two functions:

$\displaystyle f:$
$\displaystyle\bm{L}_{1}\times\bm{L}_{2}\rightarrow\bm{L}_{1}$ $\displaystyle
g:$ $\displaystyle\bm{L}_{1}\times\bm{L}_{2}\rightarrow\bm{L}_{2}$

Denote by
$h\stackrel{{\scriptstyle\text{def}}}{{=}}(f,g):\bm{L}_{1}\times\bm{L}_{2}\rightarrow\bm{L}_{1}\times\bm{L}_{2}$
and, for any $u\in\bm{L}_{1}$, denote by
$g_{u}(y)\stackrel{{\scriptstyle\text{def}}}{{=}}g(u,y)$. We prove:

######  Lemma 3.4.

Assume that $p,q$ are two numbers such that, for all $u\in\bm{L}_{1}$, the
function $g_{u}$ is $q$-stable, and the function
$F(x)\stackrel{{\scriptstyle\text{def}}}{{=}}f(x,g_{x}^{(q)}(\bot))$ is
$p$-stable. Then the following hold:

  * •

The function $h$ has the least fixpoint $(\bar{x},\bar{y})$, where

(10) $\displaystyle\bar{x}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle F^{(p)}(\bot)$
$\displaystyle\bar{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
g_{\bar{x}}^{(q)}(\bot)$

  * •

Further assume that $f,g$ also satisfy the symmetric conditions:
$f_{v}(x)\stackrel{{\scriptstyle\text{def}}}{{=}}f(x,v)$ is $p$-stable for all
$v\in\bm{L}_{2}$, and
$G(y)\stackrel{{\scriptstyle\text{def}}}{{=}}g(f_{y}^{(p)}(\bot),y)$ is
$q$-stable. Then, denoting
$(a_{n},b_{n})\stackrel{{\scriptstyle\text{def}}}{{=}}h^{(n)}(\bot,\bot)$, the
following equalities hold:

(11) $\displaystyle a_{pq+p}=$ $\displaystyle\bar{x}$ $\displaystyle
b_{pq+q}=$ $\displaystyle\bar{y}$

In particular, $h$ is $pq+\max(p,q)$-stable.

Figure 1. Computing the fixpoint of $(f,g)$.

We briefly give here the inutition, and include the formal proof in Appendix
A. The first item of the lemma can be checked by direct calculation:
$g(\bar{x},\bar{y})=g_{\bar{x}}(\bar{y})=\bar{y}$ because $\bar{y}$ is the
least fixpoint of $g_{\bar{x}}$, and one can check similarly that
$f(\bar{x},\bar{y})=\bar{x}$. For the second item, we view the computation in
Eq. (10) as a sequence of steps, each applying either $g$ or $f$, as seen in
Fig. 1. The fixpoint $x_{p}$ is reached after $pq+p$ steps555There are $pq$
$g$-steps plus $p$ $f$-steps., while the fixpoint $y_{pq}$ is reached after
$pq+p+q$ steps. The claim follows by observing that the sequence
$h^{(n)}(\bot,\bot)$ grows at least as fast as the sequence in the figure, and
by using the symmetry between $f$ and $g$.

We note that the main idea for obtaining a fixpoint in Lemma 3.4 is a general
principle that is also used in Floyd-Warshall’s algorithm, and in other
settings (DBLP:journals/tcs/Lehmann77, ; DBLP:conf/lics/HopkinsK99, ).

We generalize the lemma as follows. A clone (DBLP:conf/dagstuhl/2008coc, )
over $n$ posets $\bm{L}_{1},\ldots,\bm{L}_{n}$ is a set $\mathcal{C}$ where
(1) each element $f\in\mathcal{C}$ is some monotone function
$f:\bm{L}_{j_{1}}\times\cdots\times\bm{L}_{j_{k}}\rightarrow\bm{L}_{i}$, (2)
$\mathcal{C}$ contains all projections
$\bm{L}_{j_{1}}\times\cdots\times\bm{L}_{j_{k}}\rightarrow\bm{L}_{j_{i}}$, and
(3) $\mathcal{C}$ is closed under composition, i.e. it contains the function
$g\circ(f_{1},\ldots,f_{k})$ whenever $f_{1},\ldots,f_{k},g\in\mathcal{C}$ and
their types make the composition correct. We call $\mathcal{C}$ a c-clone if
it also contains the constant $\bot$ functions:
$\bot\colon()\rightarrow\bm{L}_{i}$. For a simple illustration, if
$f\colon\bm{L}_{1}\times\bm{L}_{2}\rightarrow\bm{L}_{1}$ and
$g\colon\bm{L}_{1}\times\bm{L}_{2}\rightarrow\bm{L}_{2}$ are in $\mathcal{C}$,
then the functions $f(x,g(x,y))$, $f(f(x,y),g(x,y))$, $g(f(x,y),y)$ are also
in $\mathcal{C}$. Similarly, the functions $g(x,\bot)$, $g(x,g(x,\bot))$, and,
in general, all functions $x\mapsto g_{x}^{(q)}(\bot)$ for $q\geq 0$ are in
$\mathcal{C}$, and so is
$F(x)\stackrel{{\scriptstyle\text{def}}}{{=}}f(x,g_{x}^{(q)}(\bot))$.

######  Theorem 3.5.

Let $\mathcal{C}$ be a c-clone of functions over $n$ posets
$\bm{L}_{1},\ldots,\bm{L}_{n}$, and assume that, for every $i\in[n]$, every
function $f\colon\bm{L}_{i}\rightarrow\bm{L}_{i}$ in $\mathcal{C}$ is
$p_{i}$-stable. WLOG, assume $p_{1}\geq p_{2}\geq\cdots\geq p_{n}$. Then, if
$f_{1},\ldots,f_{n}$ are functions in $\mathcal{C}$ of types
$f_{i}:\prod_{j=1,n}\bm{L}_{j}\rightarrow\bm{L}_{i}$, the function
$h\stackrel{{\scriptstyle\text{def}}}{{=}}(f_{1},\ldots,f_{n})$ is $P$-stable
where $P:=\sum_{k=1}^{n}\prod_{i=1}^{k}p_{i}$. Moreover, this upper bound is
tight: there exist posets $\bm{L}_{1},\ldots,\bm{L}_{n}$, a c-clone
$\mathcal{C}$, and functions $f_{1},\ldots,f_{n}$, such that $P$ is the
stability index of $h$.

##  4\. Partially Ordered Pre-semirings

We define an extension of a pre-semiring $\bm{S}$ with a partial order.

###### Definition 4.1.

A partially ordered pre-semiring, in short POPS666For Partially Ordered Pre-
Semiring., is a tuple $\bm{S}=(S,+,\circ,0,1,\sqsubseteq)$, where
$(S,+,\circ,0,1)$ is a pre-semiring, $(S,\sqsubseteq)$ is a poset, and
$+,\circ$ are monotone.

Recall that in this paper all pre-semirings are assumed to be commutative. A
POPS satisfies the identities $\bot+\bot=\bot$, because
$\bot+\bot\sqsubseteq\bot+0=\bot$, and similarly $\bot\circ\bot=\bot$. We say
that $\circ$ is strict if the identity $x\circ\bot=\bot$ holds. Throughout
this paper we will assume that the $\circ$ is strict, unless otherwise stated.
The following is easily verified:

######  Proposition 4.2.

For any POPS $\bm{S}$ where $\circ$ is strict, the subset
$\bm{S}+\bot\stackrel{{\scriptstyle\text{def}}}{{=}}\\{{x+\bot}\mid{x\in
S}\\}$, with the operations $+,\circ$, is a semiring.

###### Proof.

We check that $\bm{S}+\bot$ is closed under $+$ and $\circ$:
$(x+\bot)+(y+\bot)=(x+y)+\bot+\bot=(x+y)+\bot$, and similarly
$(x+\bot)(y+\bot)=xy+x\bot+y\bot+\bot=xy+\bot$. Finally, it suffices to
observe that $\bot$ (which is equal to $0+\bot$) is the identity for $+$ and
$1+\bot$ is the identity for $\circ$. ∎

###  4.1. Naturally Ordered Pre-Semirings

In any (pre-)semiring $\bm{S}$, the relation $x\preceq_{S}y$ defined as
$\exists z:x+z=y$, is a preorder: it is reflexive and transitive, but not
always anti-symmetric. When $\preceq_{S}$ is anti-symmetric, it is a partial
order, in which case it is called the natural order on $\bm{S}$. Every
naturally ordered semiring is a POPS, where $\bot=0$ and $\circ$ is strict,
but not conversely. Prior semantics to datalog (DBLP:conf/pods/GreenKT07, ) or
fixpoint logic (DBLP:conf/csl/DannertGNT21, ) required the semiring to be
naturally ordered, $\omega$-complete, meaning that every $\omega$-chain has a
least upper bound, and $\omega$-continuous, meaning every countable sum is
associative and commutative, and $\circ$ distributes over countable sums.

In this paper we decouple the order relation from the (pre-)semiring
structure. The reason is that some recursive programs are over a semiring that
is not naturally ordered, or, even when it is, their fixpoint semantics is
over an order different from the natural one. For example, $\mathbb{R}$ is not
naturally ordered, yet all tensor operations are over $\mathbb{R}$-relations,
hence we need a means to interpret recursive programs over $\mathbb{R}$. The
common approach for defining recursive functions over $\mathbb{R}$ or
$\mathbb{N}$ (or any other set) is to “lift” the set. For example, the lifted
integers
$\mathbb{N}_{\bot}\stackrel{{\scriptstyle\text{def}}}{{=}}\mathbb{N}\cup\\{\bot\\}$
with the ordering $\bot\sqsubseteq x$ for all $x$, is used to give a standard
textbook semantics to the recursive definition of factorial:

$\displaystyle P:$ $\displaystyle\texttt{fact}(x)=\texttt{ if }x=0\texttt{
then }1\texttt{ else }x\times\texttt{fact}(x-1)$

The immediate consequence operator $P(\texttt{fact})$ takes a partial function
and returns a new partial function. After $q$ iterations, $P^{(q)}(\bot)$
returns a function that is $=x!$ for $x<q$, and is $=\bot$ for $x\geq q$, and
$\texttt{fact}=\text{\sf lfp}(P)$. Important for our discussion is the fact
that the partial order $\sqsubseteq$ is not the natural order $x\leq y$ on
$\mathbb{N}$, but a different one. This justifies our definition of a POPS
(Def 4.1), where we decoupled the partial order from the (pre-)semiring
operations.

###  4.2. Examples of POPS

We illustrate here several examples of POPS. In each case, we also examine the
set $\bm{S}+\bot$, which is always a semiring by Proposition 4.2. We have
further discussion of POPS in Appendix B.

###### Example 4.3.

The semirings $\mathbb{N}$, $\mathbb{B}$, $\text{\sf Trop}^{+}$ from Sec. 2
are naturally ordered, and therefore they are POPS. In these cases, zero and
bottom coincide, $0=\bot$, and therefore $\bm{S}+\bot=\bm{S}+0=\bm{S}$.

###### Example 4.4.

The lifted reals
$\mathbb{R}_{\bot}\stackrel{{\scriptstyle\text{def}}}{{=}}(\mathbb{R}\cup\\{\bot\\},+,*,0,1,\sqsubseteq)$
where $x+\bot=x*\bot=\bot$ for all $x$, and $\bot\sqsubseteq x$ for all $x$,
is a POPS. In this case $\bm{R}_{\bot}+\bot=\\{\bot\\}$ is a degenerate
semiring consisting of a single element.

###### Example 4.5.

Consider the following POPS:

$\displaystyle\texttt{THREE}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle(\\{\bot,\bm{0},\bm{1}\\},\vee,\wedge,\bm{0},\bm{1},\leq_{k})$

where:

  * •

$\vee,\wedge$ have the semantics of 3-valued logic. More precisely, define the
truth ordering $0<_{t}\bot<_{t}1$ and set $x\vee
y\stackrel{{\scriptstyle\text{def}}}{{=}}\max_{t}(x,y)$, $x\wedge
y\stackrel{{\scriptstyle\text{def}}}{{=}}\min_{t}(x,y)$.

  * •

$\leq_{k}$ is the knowledge order, defined as $\bot<_{k}\bm{0},\bm{1}$.

Here $\texttt{TREE}\vee\bot=\\{\bot,1\\}$ is isomorphic to $\mathbb{B}$. We
will return to this POPS in Appendix E.

For the next two examples are adapted from (semiring_book, , Example 7.1.4)
and (semiring_book, , Chapt.8, Sec.1.3.2) respectively. If $A$ is a set and
$p\geq 0$ a natural number, then we denote by $\mathcal{P}_{p}(A)$ the set of
subsets of $A$ of size $p$, and by $\mathcal{B}_{p}(A)$ the set bags of $A$ of
size $p$. We also set
$\mathcal{P}_{\texttt{fin}}(A)\stackrel{{\scriptstyle\text{def}}}{{=}}\bigcup_{p}\mathcal{P}_{p}(A)$
and
$\mathcal{B}_{\texttt{fin}}(A)\stackrel{{\scriptstyle\text{def}}}{{=}}\bigcup_{p}\mathcal{B}_{p}(A)$.
We denote bags as in $\\{\\{a,a,a,b,c,c\\}\\}$. Given
$\bm{x},\bm{y}\in\mathcal{P}_{fin}(\mathbb{R}_{+}\cup\infty)$, we denote by:

$\displaystyle\bm{x}\cup\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$ set
union of $\bm{x},\bm{y}$
$\displaystyle\bm{x}+\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{{u+v}\mid{u\in\bm{x},v\in\bm{y}}\\}$

Similarly, given
$\bm{x},\bm{y}\in\mathcal{B}_{fin}(\mathbb{R}_{+}\cup\infty)$, we denote by:

$\displaystyle\bm{x}\uplus\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$ bag
union of $\bm{x},\bm{y}$
$\displaystyle\bm{x}+\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{\\{{u+v}\mid{u\in\bm{x},v\in\bm{y}}\\}\\}$

###### Example 4.6.

Consider a bag $\bm{x}=\\{\\{x_{0},x_{1},\ldots,x_{n}\\}\\}$, where $x_{0}\leq
x_{1}\leq\ldots\leq x_{n}$. For any $p\geq 0$, we denote by:

$\displaystyle\min_{p}(\bm{x})\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{\\{x_{0},x_{1},\ldots,x_{\min(p,n)}\\}\\}$

In other words, $\min_{p}$ retains the smallest $p+1$ elements of the bag
$\bm{x}$. Then, for any $p\geq 0$, the following is a semiring:

$\displaystyle\text{\sf Trop}^{+}_{p}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle(\mathcal{B}_{p+1}(\mathbb{R}_{+}\cup\\{\infty\\}),\oplus_{p},\otimes_{p},\bm{0}_{p},\bm{1}_{p})$

where:

$\displaystyle\bm{x}\oplus_{p}\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min_{p}(\bm{x}\uplus\bm{y})$
$\displaystyle\bm{x}\otimes_{p}\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min_{p}(\bm{x}+\bm{y})$
$\displaystyle\bm{0}_{p}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{\infty,\infty,\ldots,\infty\\}$
$\displaystyle\bm{1}_{p}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{0,\infty,\ldots,\infty\\}$

For example, if $p=2$ then
$\\{\\{3,7,9\\}\\}\oplus_{2}\\{\\{3,7,7\\}\\}=\\{\\{3,3,7\\}\\}$ and
$\\{\\{3,7,9\\}\\}\otimes_{2}\\{\\{3,7,7\\}\\}=\\{\\{6,10,10\\}\\}$. The
following identities are easily checked, for any two finite bags
$\bm{x},\bm{y}$:

$\displaystyle\min_{p}(\min_{p}(\bm{x})\uplus\min_{p}(\bm{y}))=$
$\displaystyle\min_{p}(\bm{x}\uplus\bm{y})$ (12)
$\displaystyle\min_{p}(\min_{p}(\bm{x})+\min_{p}(\bm{y}))=$
$\displaystyle\min_{p}(\bm{x}+\bm{y})$

This implies that, an expression in the semiring $\text{\sf Trop}_{p}$ can be
computed as follows. First, convert $\oplus,\otimes$ to $\uplus,+$
respectively, compute the resulting bag, then apply $\min_{p}$ only once, on
the final result. We will show below, in Prop 6.8 that $\text{\sf
Trop}^{+}_{p}$ is naturally ordered, and, therefore, $\text{\sf
Trop}^{+}_{p}\oplus_{p}\bm{0}_{p}=\text{\sf Trop}^{+}_{p}$. Notice that, when
$p=0$, then $\text{\sf Trop}^{+}_{p}=\text{\sf Trop}^{+}$, which we introduced
in Example 1.2.

###### Example 4.7.

Fix a real number $\eta\geq 0$, and denote by
$\mathcal{P}_{\leq\eta}(\mathbb{R}_{+}\cup\\{\infty\\})$ the set of all finite
sets $\bm{x}=\\{x_{0},x_{1},\ldots,x_{p}\\}$ where
$\max(\bm{x})-\min(\bm{x})\leq\eta$. Given any finite set
$\bm{x}\in\mathcal{P}_{\texttt{fin}}(\mathbb{R}_{+}\cup\\{\infty\\})$, we
define

$\displaystyle\min_{\leq\eta}(\bm{x})\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{{u}\mid{u\in\bm{x},u-\min(\bm{x})\leq\eta}\\}$

In other words, $\min_{\leq\eta}$ retains from the set $\bm{x}$ only the
elements at distance $\leq\eta$ from its minimum. The following is a semiring:

$\displaystyle\text{\sf
Trop}^{+}_{\leq\eta}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle(\mathcal{P}_{\leq\eta}(\mathbb{R}_{+}\cup\\{\infty\\}),\oplus_{\leq\eta},\otimes_{\leq\eta})$

where:

$\displaystyle\bm{x}\oplus_{\leq\eta}\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min_{\leq\eta}(\bm{x}\cup\bm{y})$
$\displaystyle\bm{x}\otimes_{\leq\eta}\bm{y}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min_{\leq\eta}(\bm{x}+\bm{y})$
$\displaystyle\bm{0}_{\leq\eta}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{\infty\\}$
$\displaystyle\bm{1}_{\leq\eta}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\\{0\\}$

For example, if $\eta=6.5$ then:
$\\{3,7\\}\oplus_{2}\\{5,9,10\\}=\\{3,5,7,9\\}$ and
$\\{1,6\\}\otimes_{2}\\{1,2,3\\}=\\{2,3,4,7,8\\}$. The following identities
are easily checked, for any two finite sets $\bm{x},\bm{y}$:

$\displaystyle\min_{\leq\eta}(\min_{\leq\eta}(\bm{x})\cup\min_{\leq\eta}(\bm{y}))=$
$\displaystyle\min_{\leq\eta}(\bm{x}\cup\bm{y})$ (13)
$\displaystyle\min_{\leq\eta}(\min_{\leq\eta}(\bm{x})+\min_{\leq\eta}(\bm{y}))=$
$\displaystyle\min_{\leq\eta}(\bm{x}+\bm{y})$

It follows that expressions in $\text{\sf Trop}^{+}_{\leq\eta}$ can be
computed as follows: first convert $\oplus,\otimes$ to $\cup,+$ respectively,
compute the resulting set, and apply the $\min_{\leq\eta}$ operator only once,
on the final result. We will show in Prop. 6.9 that $\text{\sf
Trop}^{+}_{\leq\eta}$ is naturally ordered, hence $\text{\sf
Trop}^{+}_{\leq\eta}\oplus_{\leq\eta}\bm{0}_{\leq\eta}=\text{\sf
Trop}^{+}_{\leq\eta}$. Notice that, when $\eta=0$, then we recover again
$\text{\sf Trop}^{+}_{\leq\eta}=\text{\sf Trop}^{+}$, the semiring introduced
in Example 1.2.

The reader may wonder why $\text{\sf Trop}_{p}$ is defined to consists of bags
of $p+1$ nubmers, while $\text{\sf Trop}_{\leq\eta}$ is defined on sets. The
main reason is for consistency with (semiring_book, ): both identities (12)
and (13) hold on either sets or bags, and these are sufficient to prove the
semiring identities. Later we prove Proposition 6.8 for $\text{\sf Trop}_{p}$,
and 6.9 for $\text{\sf Trop}_{\leq\eta}$: the first one holds for both sets
and bags, but the latter holds only for sets.

Finally, we illustrate an example where the semiring $\bm{S}+\bot$ is non-
trivial. First, we note that if $\bm{S}_{1},\bm{S}_{2}$ are two POPS, then
their cartesian product $\bm{S}_{1}\times\bm{S}_{2}$ is also a pops:
operations are defined element-wise, e.g.
$(x_{1},x_{2})\oplus(y_{1},y_{2})\stackrel{{\scriptstyle\text{def}}}{{=}}(x_{1}\oplus_{1}y_{1},x_{2}\oplus_{2}y_{2})$,
etc, and the order is defined component-wise. The smallest element is
$(\bot_{1},\bot_{2})$.

###### Example 4.8.

Consider the following two POPS.

  * •

A naturally ordered semiring
$\bm{S}=(S,\oplus_{S},\otimes_{S},0_{S},1_{S},\sqsubseteq_{S})$. Since it is
naturally ordered, we have $\bm{S}\oplus_{S}0_{S}=\bm{S}$.

  * •

Any POPS $\bm{T}$ where addition is strict: $x\oplus_{T}\bot=\bot$. For
example, this could be the lifted reals $\mathbb{R}_{\bot}$, or this very
simple POPS: $(\\{\bot,\top\\},\oplus,\otimes,\top,\top)$, where
$\top\oplus\top=\top\otimes\top=\top$ and $x\oplus\bot=x\otimes\bot=\bot$, and
$\bot\sqsubset\top$. In either case, $\bm{T}$ is not naturally ordered, and we
have $\bm{T}\oplus_{T}\bot_{T}=\\{\bot_{T}\\}$.

Define the cartesian product POPS, $\bm{S}\times\bm{T}$. The smallest element
is $(0_{S},\bot_{T})$, and we have
$(\bm{S}\times\bm{T})+(0_{S},\bot_{T})=\bm{S}\times\\{\bot_{T}\\}$, which is a
non-trivial, strict subset of $\bm{S}\times\bm{T}$.

##  5\. $\textsf{DATALOG}^{\circ}$

We introduce here a new recursive language obtained by combining traditional
datalog with tensor expressions. We call the language $\text{\sf
datalog}^{\circ}$, pronounced datalogo, where the superscript “$\circ$” is a
(semi)-ring.

###  5.1. Basic $\text{\sf datalog}^{\circ}$

We first introduce the basic $\text{\sf datalog}^{\circ}$, and discuss
extensions shortly. Throughout this section we denote by $E_{1},\ldots,E_{m}$
the relational symbols representing the EDB predicates, by
$R_{1},\ldots,R_{n}$ the symbols representing the IDB predicates.777EDB and
IDB stand for extensional database and intentional database respectively
(DBLP:books/aw/AbiteboulHV95, ). All EDBs and IDBs are assumed to be over the
same finite domain $D$, and have the same value-space, a POPS $\bm{S}$; thus,
their types are $E_{j}:D^{\ell_{j}}\rightarrow\bm{S}$ and
$R_{i}:D^{k_{i}}\rightarrow\bm{S}$, where $\ell_{j},k_{i}$ are the arities of
$E_{j},R_{i}$ respectively.

A $\text{\sf datalog}^{\circ}$ program $P$ consists of $n$ rules, one for each
IDB predicate:

(14) $\displaystyle P:$ $\displaystyle R_{i}(\texttt{vars}_{i})$
$\displaystyle\text{ :- }f_{i}(E_{1},\ldots,E_{m},R_{1},\ldots,R_{n})$
$\displaystyle i\in[n]$

where each function $f_{1},\ldots,f_{n}$ is a sum-sum-product expression given
by Def. 2.1, Eq. (8). $P$ is called linear if each product contains at most
one IDB predicate. The $\text{\sf datalog}^{\circ}$ program in Ex. 1.2 is
linear.

While in standard datalog rules are required to be safe, meaning that every
variable must occur in some relational atom, we do not need to require this in
$\text{\sf datalog}^{\circ}$ in order to define its semantics, because we
assume the domain $D$ is finite.

###  5.2. Semantics

We define now the semantics of a basic program (14). Denote by
$\bm{D}_{\text{EDB}}\stackrel{{\scriptstyle\text{def}}}{{=}}\bigcup_{j=1,m}D^{\ell_{j}}$
and
$\bm{D}_{\text{IDB}}\stackrel{{\scriptstyle\text{def}}}{{=}}\bigcup_{i=1,n}D^{k_{i}}$,
where the union is a disjoint union. An instance of all EDB predicates is
$\bm{E}\in S^{\bm{D}_{\text{EDB}}}$, and an instance of all IDB predicates is
$\bm{R}\in S^{\bm{D}_{\text{IDB}}}$. For each $\text{\sf datalog}^{\circ}$
rule, the expression $f_{i}$ in (14) defines a function:

$\displaystyle f_{i}$ $\displaystyle:S^{\bm{D}_{\text{EDB}}}\times
S^{\bm{D}_{\text{IDB}}}\rightarrow S^{D^{k_{i}}}$

Denote by
$H\stackrel{{\scriptstyle\text{def}}}{{=}}(f_{1},\ldots,f_{n}):S^{\bm{D}_{\text{EDB}}}\times\bm{S}^{\bm{D}_{\text{IDB}}}\rightarrow
S^{\bm{D}_{\text{IDB}}}$.

###### Definition 5.1.

Fix an EDB instance, $\bm{E}$. The immediate consequence operator (ICO) of the
program $P$ in (14) is the function $F_{P}:S^{\bm{D}_{\text{IDB}}}\rightarrow
S^{\bm{D}_{\text{IDB}}}$ defined as
$F_{P}(\bm{R})\stackrel{{\scriptstyle\text{def}}}{{=}}H(\bm{E},\bm{R})$. The
semantics of the datalog program $P$ is its least fixpoint, $\text{\sf
lfp}(F_{P})$. The naïve evaluation algorithm consists of setting
$\bm{R}^{(0)}\stackrel{{\scriptstyle\text{def}}}{{=}}(\bot,\ldots,\bot)$ and
repeatedly computing
$\bm{R}^{(q+1)}\stackrel{{\scriptstyle\text{def}}}{{=}}F_{P}(\bm{R}^{(q)})$,
until $\bm{R}^{(q+1)}=\bm{R}^{(q)}$. If such a fixpoint exists, then we say
that the program converges, otherwise it diverges.

###  5.3. The Grounded $\text{\sf datalog}^{\circ}$ Program

It is often more convenient to define the semantics of a $\text{\sf
datalog}^{\circ}$ program by refering to its grounded version. Fix a program
$P$ as defined in Eq. (14), and consider a rule
$R_{i}(x_{1},\ldots,x_{k_{i}})\text{ :- }\cdots$, as in Eq. (14). A grounding
of this rule is obtained by choosing a tuple $\bm{t}\in D^{k_{i}}$,
substituting all head variables with the constants in $\bm{t}$, and expanding
each summation operator into an explicit sum of expressions, for example
$\sum_{x\in D}f(x)$ becomes $f(u_{1})+f(u_{2})+\cdots+f(u_{|D|})$, if the
domain is $D=\\{u_{1},\ldots,u_{|D|}\\}$. This results in an expression
consisting of ground EDB atoms and ground IDB atoms connected by the operators
$+$ and $\circ$.

Define $M\stackrel{{\scriptstyle\text{def}}}{{=}}|\bm{D}_{\text{EDB}}|$ and
$N\stackrel{{\scriptstyle\text{def}}}{{=}}|\bm{D}_{\text{IDB}}|$ the number of
ground EDB atoms and ground IDB atoms respectively. Denote these atoms by the
variables $e_{1},\ldots,e_{M}$ and $x_{1},\ldots,x_{N}$ respectively. For
example, one variable $x_{p}$ may stand for the ground atom
$R_{i}(u_{1},\ldots,u_{k_{i}})$, where $u_{1},\ldots,u_{k_{i}}\in D$. The
grounded function $f_{i}$ is a multivariate polynomial in the variables
$e_{1},\ldots,e_{M},x_{1},\ldots,x_{N}$ over the POPS $\bm{S}$;
$f_{i}:\bm{S}^{M}\times\bm{S}^{N}\rightarrow\bm{S}$. If the original program
was linear, then each $f_{i}$ is a linear function in the IDB variables
$x_{1},\ldots,x_{N}$. The grounded program $P^{g}$ consists of all groundings
of all rules in $P$:

(15) $\displaystyle P^{g}:$ $\displaystyle x_{k}$ $\displaystyle\text{ :-
}f_{k}(e_{1},\ldots,e_{M},x_{1},\ldots,x_{N})$ $\displaystyle k\in[N]$

EDB and IDB instances of the original program and the grounded program are the
same. It is immediate to check that the Immediate Consequence Operator of the
original and of the grounded program coincide. In the rest of this paper we
will assume w.l.o.g. that the semantics of a $\text{\sf datalog}^{\circ}$
program (Def. 5.1) is the fixpoint of a system of polynomials (15).

###  5.4. The Naive Evaluation Algorithm

$R_{0}\leftarrow\bm{0}$;

for  _ $t\leftarrow 1$ to $\infty$ _ do

$R_{t}\leftarrow F(R_{t-1})$;

if  _ $R_{t}=R_{t-1}$ _ then

Break

return $R_{t}$

Algorithm 1 Naïve evaluation for $\text{\sf datalog}^{\circ}$

The Naïve Algorithm for evaluating $\text{\sf datalog}^{\circ}$ is shown in
Algorithm 1, and it is quite similar to that for standard, positive datalog
with set semantics. We start with all IDBs at $\bm{\bot}$, which, in case of a
naturally ordered semiring coincides with $\bm{0}$, then repeatedly apply the
ICO $F$, until we reach a fixpoint. The algorithm computes the increasing
sequence $\bot\sqsubseteq F(\bot)\sqsubseteq F^{(2)}(\bot)\sqsubseteq\cdots$
We will show in Sec. 7 that, when $\bm{S}$ is a semiring with some additional
properties, then the algorithm can be improved to a semi-naïve algorithm. To
facilitate the comparison, we assume in Algorithm 1 that $\bm{S}$ is a
semiring, and start with $R_{0}=\bm{0}$, instead of $\bm{\bot}$.

###  5.5. Extensions

We describe here several extensions to $\text{\sf datalog}^{\circ}$ that are
needed to make it practical, and discuss whether they affect its semantics.

Interpreted functions over the key-space We allow the use of interpreted
function over the keyspace, as in the following example, which retrieves the
customers that have placed orders on two consecutive dates:

$\displaystyle Q(\texttt{cust})\text{ :- }$
$\displaystyle\texttt{Order}(\texttt{cust},\texttt{date})\wedge\texttt{Order}(\texttt{cust},\texttt{date}+1)$

Here $\texttt{date}+1$ is an interpreted function applied to date. We continue
to assume that the domain is finite, for example there is an upper bound on
the date, where $\texttt{date}+1=\texttt{date}$.

Conditionals We extend Definition 2.1 with a conditional sum-sum-product
query, which has the form:

(16) $\displaystyle Q(x_{1},\ldots,x_{k})$ $\displaystyle\text{ :-
}\texttt{case }C_{1}:Q_{1};\ \ \ C_{2}:Q_{2};\cdots;\texttt{ else }Q_{n}$

where $C_{1},C_{2},\ldots$ are conditions and $Q_{1},Q_{2},\ldots$ are sum-
sum-product expressions. For example, we may compute the prefix-sum of a
vector $V$ as follows:

$\displaystyle W(i)$ $\displaystyle\text{ :- }\texttt{case }i=0:V(0)\texttt{
else }W(i-1)+V(i)$

The grounding of a rule with conditionals continues to be a polynomial over
the POPS $\bm{S}$. Therefore, the ICO and the semantics of the program are
unaffected.

Multiple Domains We allow both multiple key domains, and multiple value
domains (POPS). An implementation would require all EDB and IDB predicates to
be declared at the beginning, for example:

      E(String, String) : Bool;
      Cost(String, String, N) : Bool;
      Path(String, String) : Trop;

Cast Operator Each $\text{\sf datalog}^{\circ}$ rule is over a single POPS
$\bm{S}$. If we want to compute a program over multiple POPS then we need some
mechanism to compute a rule over two more more POPS. The simplest way is to
combine Boolean predicates with $\bm{S}$-relations over some other POPS, using
an indicator function $[-]:\mathbb{B}\rightarrow\bm{S}$, defined as follows:

$\displaystyle[0]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\bot_{\bm{S}}$
$\displaystyle[1]\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
1_{\bm{S}}$

We call $[-]$ a cast operator. When the cast operator is applied only to
Boolean EDB predicates, then it can be computed during grounding, in other
words, the result of grounding a rule continues to be a multivariate
polynomial over the POPS $\bm{S}$. However, if the condition is applied to
Boolean IDBs, then the ICO is still a monotone operator, since the cast
operator above is monotone, but the grounding is no longer a polynomial, and
the results in the next section may no longer apply.

Summation with Explicit Range We allow and explicit range in the summation of
a monomial. This is necessary when $\bot_{\bm{S}}\neq 0$, because in that case
the indicator function cannot be used to restrict the range of the summation.
More precisely, we extend the definition of a sum-product expression in Def.
2.1 to:

$\displaystyle T(x_{1},\ldots,x_{k})$ $\displaystyle\text{ :-
}\bigoplus_{x_{k+1},\ldots,x_{p}\in D}\\{{A_{1}\otimes\cdots\otimes
A_{m}}\mid{\text{Cond}}\\}$

where Cond is a condition over the variables $x_{k+1},\ldots,x_{p}$,
restricting their range. This extension affects only how we compute the
grounding of a rule: we simply restrict the summation
$f(u_{1})+f(u_{2})+\cdots+f(u_{|D|})$ to include only terms that satisfy the
condition. The result of grounding is still a multivariate polynomial over the
POPS $\bm{S}$.

Keys to Values We allow key values to be used as POPS values, when the types
are right. For example, referring to the declarations above, we may write:

$\displaystyle\texttt{Path}(x,y)$ $\displaystyle\text{ :-
}\min_{c}\left([\texttt{Cost}(x,y,c)]+c\right)$

The expression $[\texttt{Cost}(x,y,c)]$ is a cast from Booleans to the
tropical semiring, i.e. its value is $\infty$ or $0$, and we add to it the
cost $c$, which is of type $\mathbb{N}$, hence can be cast to Trop. The rule
above maps $\mathbb{B}$ to $\text{\sf Trop}^{+}$, and is monotone. In general,
monotonicity may no longer hold.

Stratification In practice, one often needs to stratify programs, in order to
allow for non-monotone interpreted functions over the value domains.

###  5.6. Examples

We start with two examples illustrating how the semantics of a $\text{\sf
datalog}^{\circ}$ program changes, as we consider different POPS for its value
domain.

Figure 2. A graph illustrating Example 5.2

###### Example 5.2.

Consider the following $\text{\sf datalog}^{\circ}$ program, where $E(x,y)$ is
an EDB, and $a$ is some constant:

$\displaystyle L(x)\text{ :- }$
$\displaystyle[x=a]\oplus\bigoplus_{z}(L(z)\otimes E(z,x))$

First, we interpret it over the Boolean domain, $\mathbb{B}$, in which case
the program becomes:

$\displaystyle L(x)\text{ :- }$ $\displaystyle[x=a]\vee\exists_{z}(L(z)\wedge
E(z,x))$

This is a simple reachability program, which computes the set of nodes $x$
reachable from the node $a$.

Next, let’s interpret it over $\text{\sf Trop}^{+}$. In that case, the cast
operator $[x=a]$ returns $0$ when $x=a$ and returns $\infty$ when $x\neq a$.
The program becomes:

$\displaystyle L(x)\text{ :- }\min($ $\displaystyle\texttt{if }x=a\texttt{
then }0\texttt{ else }\infty,$ $\displaystyle\min_{z}(L(z)+E(z,x)))$

This program computes the Single-Source-Shortest-Path (SSSP). Consider the
graph in Fig. 2. The grounding of the program over this graph is, where we
omit the values $E(x,y)=\infty$, and simplify the expressions, e.g.
$\min(\infty+\ldots,v)=v$:

$\displaystyle L(a)\text{ :- }$
$\displaystyle\min(0,L(a)+E(a,a),L(b)+E(a,b),\ldots)=0$ $\displaystyle
L(b)\text{ :- }$ $\displaystyle L(a)+E(a,b)$ $\displaystyle L(c)\text{ :- }$
$\displaystyle\min(L(a)+E(a,c),L(b)+E(b,c))$ $\displaystyle L(d)\text{ :- }$
$\displaystyle L(c)+E(c,d)$

The naive evaluation algorithm converges after 5 steps, as show here:

$\displaystyle\begin{array}[]{l|c|c|c|c|}\cline{2-5}\cr&L(a)&L(b)&L(c)&L(d)\\\
\cline{2-5}\cr L_{0}&\infty&\infty&\infty&\infty\\\ \cline{2-5}\cr
L_{1}&0&\infty&\infty&\infty\\\ \cline{2-5}\cr L_{2}&0&1&5&\infty\\\
\cline{2-5}\cr L_{3}&0&1&4&9\\\ \cline{2-5}\cr L_{4}&0&1&4&8\\\ \cline{2-5}\cr
L_{5}&0&1&4&8\\\ \cline{2-5}\cr\end{array}$

Third, let’s interpret it over $\text{\sf Trop}^{+}_{p}$, defined in Example
4.6. Assume for simplicity that $p=1$. In that case the program computes, for
each node $x$, the two lengths $\\{\\{l_{1},l_{2}\\}\\}$ of the two shortest
paths from $a$ to $x$. The cast operator $[x=a]$ is equal to
$\\{\\{0,\infty\\}\\}$ when $x=a$, and equal to $\\{\\{\infty,\infty\\}\\}$
otherwise. The reader may check that the program converges to:

$\displaystyle L(a)=$ $\displaystyle\\{\\{0,3\\}\\}$ $\displaystyle L(b)=$
$\displaystyle\\{\\{1,4\\}\\}$ $\displaystyle L(c)=$
$\displaystyle\\{\\{4,5\\}\\}$ $\displaystyle L(d)=$
$\displaystyle\\{\\{8,9\\}\\}$

Finally, we can interpret it over $\text{\sf Trop}^{+}_{\leq\eta}$, the
semiring in Example 4.7. In that case the program computes, for each $x$, the
set of all possible lengths of paths from $a$ to $x$ that are no longer than
the shortest path plus $\eta$.

Figure 3. A graph illustrating Example 5.3

###### Example 5.3.

Consider another classic problem: computing the total cost of all subparts. We
assume that $E(x,y)$ means that “$x$ has subpart $y$”, and that $C(x)$ denotes
the cost of the (sub)part $x$. The $\text{\sf datalog}^{\circ}$ program
computing the total cost is:

$\displaystyle T(x)\text{ :- }$ $\displaystyle
C(x)+\sum_{y}\\{{T(y)}\mid{E(x,y)}\\}$

When $E$ is acyclic, then the program terminates. We explain now its semantics
over cyclic graphs, and illustrate with Fig. 3. The grounding of the program
is:

$\displaystyle T(a)\text{ :- }$ $\displaystyle C(a)+T(b)+T(c)$ $\displaystyle
T(b)\text{ :- }$ $\displaystyle C(b)+T(a)+T(c)$ $\displaystyle T(c)\text{ :-
}$ $\displaystyle C(c)+T(d)$ $\displaystyle T(d)\text{ :- }$ $\displaystyle
C(d)$

We consider two choices of the semiring. First, the naturally ordered semiring
$(\mathbb{N},+,*,0,1)$. Here the program diverges, since naive algorithm will
compute ever increasing values for $T(a)$ and $T(b)$. Second, consider the
lifted reals
$\mathbb{R}_{\bot}=(\mathbb{R}\cup\\{\bot\\},+,*,0,1,\sqsubseteq)$. Now the
program converges in 3 steps, as can be seen below:

$\displaystyle\begin{array}[]{l|c|c|c|c|}\cline{2-5}\cr&T(a)&T(b)&T(c)&T(d)\\\
\cline{2-5}\cr T_{0}&\bot&\bot&\bot&\bot\\\ \cline{2-5}\cr
T_{1}&\bot&\bot&\bot&10\\\ \cline{2-5}\cr T_{2}&\bot&\bot&11&10\\\
\cline{2-5}\cr T_{3}&\bot&\bot&11&10\\\ \cline{2-5}\cr\end{array}$

Finally, we illustrate how to combine in a useful way a computation over two
POPS.

###### Example 5.4.

We illustrate the company control example from (DBLP:conf/pods/RossS92, ,
Example 3.2). $S(x,y)=n\in\mathbb{R}_{+}$ represents the fact that company $x$
owns a proportion of $n$ shares in company $y$. We want to compute the
predicate $C(x,y)$, representing the fact that the company $x$ controls
company $y$, where control is defined as follows: $x$ controls $y$ if the sum
of shares it owns in $y$ plus the sum of shares in $y$ owned by companies
controlled by $x$ is $>0.5$. The program is adapted directly from
(DBLP:conf/pods/RossS92, ):

$\displaystyle CV(x,x,y)\text{ :- }$ $\displaystyle S(x,y)$ $\displaystyle
CV(x,z,y)\text{ :- }$ $\displaystyle[C(x,z)]*S(z,y)$ $\displaystyle
T(x,y)\text{ :- }$ $\displaystyle\sum_{z}CV(x,z,y)$ $\displaystyle
C(x,y)\text{ :- }$ $\displaystyle[T(x,y)>0.5]$

Notice the interaction between two POPS: the IDBs $CV$ and $T$ are over the
naturally ordered semiring $(\mathbb{R}_{+},+,*,0,1)$, while $C$ has values in
the Boolean semiring. The value of $CV(x,z,y)$ is the fraction of shares that
$x$ owns in $y$ through its control of company $z$. Notice that the cast
operator $[C(x,z)]$ has type $\mathbb{B}\rightarrow\mathbb{R}_{+}$, and
returns 0 if $x$ does not control $z$, and 1 if $x$ controls $z$. It is
obviously monotone. The last rule checks whether the total amount of shares
that $x$ controls in $y$ is $>0.5$. Here the cast operator $[T(x,y)>0.5]$ maps
$\mathbb{R}_{+}$ to $\mathbb{B}$, in an obvious way, and is also monotone.

##  6\. Convergence Behavior of $\text{\sf datalog}^{\circ}$

In traditional datalog, the naïve evaluation algorithm converges in a number
of iterations that is polynomial in the size of the domain888In standard
datalog the domain is sometimes assumed to be infinite, and instead the
runtime is described in terms of the size of the active domain. In this paper
we assume that the domain is finite, and avoid the need to talk about the
active domain. When the domain is infinite, then one can adopt the approach of
standard datalog and consider the active domain instead., but in $\text{\sf
datalog}^{\circ}$, the picture is more complex. Recall that $D$ denotes the
(finite) domain on which the key-space is based, which is different from the
semiring value-space which can be infinite. Depending on the POPS $\bm{S}$,
and assuming $\oplus$ and $\otimes$ take $O(1)$-time to evaluate, there are
four possibilities for $\text{\sf datalog}^{\circ}$:

  1. (i)

Every program converges in time polynomial in $|D|$.

  2. (ii)

Every program converges in some time $T(|D|)$.

  3. (iii)

Every program converges.

  4. (iv)

Not every program converges.

We study the following question: Given a POPS $\bm{S}$, determine which of the
four cases holds for $\text{\sf datalog}^{\circ}$?

The simplest example is when $\bm{S}$ is the Boolean semiring. This is the
traditional datalog setup when Case (i) holds. This section provides a series
of results pertaining to the question above in the general case. Throughout
this section we will refer the following single-rule $\text{\sf
datalog}^{\circ}$ program:

(17) $\displaystyle X()$ $\displaystyle\text{ :- }A()\circ X()\ \ \ +\ \ \
B()$

Obviously, a necessary condition for every $\text{\sf datalog}^{\circ}$
program to converge (in one of the convergence criteria above) is for (17) to
also converge. Surprisingly, in some cases the converse also holds:
convergence of (17) implies convergence of any $\text{\sf datalog}^{\circ}$
program.

Throughout this section we will assume that the multiplication in the POPS
$\bm{S}$ is strict: $a\circ\bot=\bot$.

A linear function999Strictly speaking, these are affine functions; however, we
use “linear” to align with “linear datalog”. on the POPS $\bm{S}$ is either a
constant function $f(x)\stackrel{{\scriptstyle\text{def}}}{{=}}b$, or is
defined as101010$f(x)=b$ is not a special case of (18), because, in general,
$0\circ x\neq 0$.:

(18) $\displaystyle f(x)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle ax+b$

When $b=1$ then we say that the linear function (18) is simple. A multivariate
function $f:\bm{S}^{k}\rightarrow\bm{S}$ is called linear if it is linear in
each argument; equivalently, $f(x_{1},\ldots,x_{k})=a_{1}\circ
x_{i_{1}}+\cdots+a_{\ell}\circ x_{i_{\ell}}+b$, for $1\leq
i_{1}<i_{2}<\cdots<i_{\ell}\leq k$.

The following lemma can be verified straightforwardly.

######  Lemma 6.1.

Let $\bm{S}$ be a POPS where $\circ$ is strict, and $f$ be a univariate linear
function. If $f(x)=b$, then $f^{(q)}(\bot)=b$ for all $q\geq 1$. If
$f(x)=ax+b$, then, define $g(x)\stackrel{{\scriptstyle\text{def}}}{{=}}ax+1$,
we have

(19) $\displaystyle f^{(q)}(\bot)$
$\displaystyle=b+ab+a^{2}b+\cdots+a^{q-1}b+\bot=g^{(q)}(\bot)\circ b.$

In particular, if every simple linear function is $q$-stable, then every
linear function is $\max(1,q)$-stable.

Notice that, when $f$ not a constant, then the value $f^{(q)}(\bot)$ is always
in the set $\bm{S}+\bot$, which, by Proposition 4.2, is a semiring, thus, the
fixpoint computation of $f$ is entirely within this semiring. When $f$ is a
constant $b$, then its fixpoint may be outside of this semiring, since we may
have $b\not\in\bm{S}+\bot$.

###  6.1. Divergence

It is easy to find examples where programs diverge, thus, Case (iv) is
possible. We have seen such a case in Example 5.3.

###  6.2. Convergence

This section studies conditions under which a $\text{\sf datalog}^{\circ}$
program converges in a finite number of steps that is not only dependent on
$|D|$ but also on the value-space of $\bm{S}$. This corresponds to Case (iii).
The first observation is a simple sufficient condition, which follows
immediately from Proposition 3.3:

######  Theorem 6.2.

If ACC holds for the POPS $\bm{S}$, then every $\text{\sf datalog}^{\circ}$
program $P$ on $\bm{S}$ converges on every input EDB instance. In addition, if
$\bm{S}$ has rank $k$, then the program converges in at most $k\cdot
N=k\cdot|D|^{O(1)}$ iterations (where $N$ is the number of ground IDB atoms).

Beyond the above simple result, we give next a complete characterization of
POPS $\bm{S}$ for which every linear program converges.

######  Theorem 6.3.

Let $\bm{S}$ be a POPS where $\circ$ is strict. Then the following conditions
are equivalent:

  1. (1)

Every linear $\text{\sf datalog}^{\circ}$ program converges in a finite number
of steps.

  2. (2)

Every linear function is stable.

  3. (3)

Every simple linear function is stable.

###### Proof.

Lemma 6.1 proves the equivalence of items 2 and 3. We prove here the
equivalence of 2 and 2.

A necessary condition is for the program (17) to converge in a finite number
of steps, which implies that any linear function given by Eq. (18) must is
stable. Thus, stability of linear functions on $\bm{S}$ is a necessary
condition for Case (iii).

Next, we prove the converse. We prove the following claim, by induction on
$N$: every linear function $h:\bm{S}^{N}\rightarrow\bm{S}^{N}$ is stable. The
claim immediately implies the theorem, because the immediate consequence
operator of a linear $\text{\sf datalog}^{\circ}$ program is a linear function
and its stability implies that the naive algorithm converges in a finite
number of steps. When $N=1$ then the claim holds by assumption. Assume $N>1$
and write the function $h$ as $h(x,y)=(f(x,y),g(x,y))$ where
$f:\bm{S}^{N-1}\times\bm{S}\rightarrow\bm{S}^{N-1}$ and
$g:\bm{S}^{N-1}\times\bm{S}\rightarrow\bm{S}$. For every $x\in\bm{S}^{N-1}$,
the function $g_{x}(y)\stackrel{{\scriptstyle\text{def}}}{{=}}g(x,y)$ is a
linear function, thus either $g(x,y)=b(x)$ or $g(x,y)=ay+b(x)$ for some linear
function $b$. We prove that there exists $q$, independent of $x$, s.t. $g_{x}$
is $q$-stable. In the first case $g_{x}$ is 1-stable. In the second case, by
assumption, the linear function
$\psi(y)\stackrel{{\scriptstyle\text{def}}}{{=}}ay+1$ is stable, and we let
$q$ be such that $\psi$ is $q$-stable; then Lemma 6.1 implies that $g_{x}(y)$
is also $q$-stable, for all $x$. Next, the function
$F(x)\stackrel{{\scriptstyle\text{def}}}{{=}}f(x,g_{x}^{(q)}(\bot))$ defined
in Eq. (10) is linear in $x\in\bm{S}^{N-1}$ and, thus, by induction
hypothesis, it is $p$-stable for some $p$. Finally, by Lemma 3.4, $h$ is
$pq+\max(p,q)$-stable. ∎

Finally, we give an algebraic characterization of the POPS where all linear
$\text{\sf datalog}^{\circ}$ program converge. The following notations and
simple facts can be found in (semiring_book, ). Fix a semiring $\bm{S}$. For
every $a\in\bm{S}$ and $p\geq 0$ define:

(20) $\displaystyle a^{(p)}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle 1+a+a^{2}+\cdots+a^{p}$

###### Definition 6.4.

An element $a$ of a semiring is $p$-stable if $a^{(p)}=a^{(p+1)}$. We say that
$a$ is stable if there exists $p$ s.t. $a$ is $p$-stable.

We call the semiring $\bm{S}$ $p$-stable if all its elements are $p$-stable,
and call it stable if every element is stable.

We recall here a simple, but very nice result from (semiring_book, ), which
helps better understand the concept of stability.

######  Proposition 6.5.

If $1$ is $p$-stable then $\bm{S}$ is naturally ordered. In particular, every
stable semiring is naturally ordered.

###### Proof.

If $1$ is $p$-stable, then $1^{(p+1)}=1^{(p)}$, which means that
$1+1+\cdots+1(\mbox{$p+1$ times})=1+\cdots+1(\mbox{$p$ times})$, or, in short,
$p+1=p$. We prove that, if $a\preceq_{S}b$ and $b\preceq_{S}a$ hold, then
$a=b$. By definition of $\preceq_{S}$, there exists $x,y$ such that $a+x=b$
and $b+y=a$. On one hand have $a=b+y=a+x+y$, which implies $a=a+k(x+y)$ for
every $k\geq 0$. On the other hand we have $b=a+x=a+(k+1)x+ky$ for every
$k\geq 0$. By taking $k=p$ we obtain $a=b$, because $px=(p+1)x$. ∎

The connection between element-stability and function-stability is immediate:

######  Lemma 6.6.

Let $\bm{S}$ be a POPS, and $f(x)=ax+1$ be a simple linear function. Then $f$
is $p+1$-stable iff $a+\bot$ is $p$-stable in the semiring $\bm{S}+\bot$.

###### Proof.

By direct calculation we have:

$\displaystyle(a+\bot)^{(q)}=$ $\displaystyle
1+(a+\bot)+(a+\bot)^{2}+\cdots+(a+\bot)^{q}$ $\displaystyle=$ $\displaystyle
1+a+a^{2}+\cdots+a^{q}+\bot$

and this expression equals $f^{(q+1)}(\bot)$ by Lemma 6.1. ∎

Theorem 6.3 and the lemma immediately imply:

######  Corollary 6.7.

Let $\bm{S}$ be a POPS where $\circ$ is strict. Then, every linear $\text{\sf
datalog}^{\circ}$ program converges in a finite number of steps iff the
semiring $\bm{S}+\bot$ is stable.

We end this section with two examples. First, we prove:

######  Proposition 6.8.

The semiring $\text{\sf Trop}^{+}_{p}$ defined in Example 4.6 is $p$-stable.
In particular, it is naturally ordered, and every linear $\text{\sf
datalog}^{\circ}$ program converges.

###### Proof.

Let $a\in\text{\sf Trop}^{+}_{p}$; recall that $a$ is a bag of $p+1$ elements
in $\mathbb{R}_{+}\cup\\{\infty\\}$. For every $q\geq 1$, $a^{q}$ consists of
the $p+1$ smallest sums of the form $x_{i_{1}}+x_{i_{2}}+\cdots+x_{i_{q}}$,
where each $x_{i_{j}}\in a$. Furthermore, the value
$a^{(q)}=1+a+a^{2}+\cdots+a^{q}$ is obtained as follows: (a) consider all sums
of $\leq q$ numbers in $a$ (b) retain the smallest $p+1$ sums.

We claim that $a^{(p)}=a^{(p+1)}$. To prove the claim, consider such a sum
$y\stackrel{{\scriptstyle\text{def}}}{{=}}x_{i_{1}}+x_{i_{2}}+\cdots+x_{i_{p+1}}$.
We will find $p+1$ distinct terms, belonging to $1,a,a^{2},\ldots,a^{p}$,
which are $\leq y$, proving that $y$ is redundant. These terms are:

$\displaystyle 0\in 1$ $\displaystyle x_{i_{1}}\in a$ $\displaystyle
x_{i_{1}}+x_{i_{2}}\in a^{2}$ $\displaystyle\ldots$ $\displaystyle
x_{i_{1}}+x_{i_{2}}+\cdots+x_{i_{p}}\in a^{p}$

∎

We will prove in section 6.4 a stronger result: that every linear program over
the semiring $\text{\sf Trop}^{+}_{p}$ converges in polynomial time.

######  Proposition 6.9.

The semiring $\text{\sf Trop}^{+}_{\leq\eta}$ defined in Example 4.7 is
stable. In particular it is naturally ordered, and every linear $\text{\sf
datalog}^{\circ}$ program converges.

###### Proof.

The proof is similar to that of Prop 6.8. While the elements of $\text{\sf
Trop}^{+}_{p}$ are bags, those of $\text{\sf Trop}^{+}_{\leq\eta}$ are sets.
Recall that the multiplicative unit is $1=\\{0\\}$. Let $a$ be an element of
$\text{\sf Trop}^{+}_{\leq\eta}$. Then $a^{(q)}=1+a+a^{2}+\cdots+a^{q}$ is
obtained as follows: (a) consider all sums of $\leq q$ numbers; this includes
the empty sum, whose value is $0$. (b) retain only those sums that are
$\leq\eta$. If $a=\\{0\\}$, then $a$ is $0$-stable, so assume w.l.o.g. that
$a$ contains some element $>0$. Let $x_{0}>0$ be the smallest such element,
and let $p=\lceil\frac{\eta}{x_{0}}\rceil$. We claim that $a^{(p)}=a^{(p+1)}$.
To prove the claim, consider a sum of $p+1$ elements
$y=x_{i_{1}}+\cdots+x_{i_{p+1}}$. If any $x_{i_{j}}=0$, then this sum also
belongs to some $a^{q}$, so assume w.l.o.g. that all terms in the sum are
$>0$. It follows that $y\geq(p+1)x_{0}>\eta$, which means that it will not be
included in $a^{(p+1)}$. It follows that $a^{(p)}=a^{(p+1)}$ as required. ∎

Finally, we observe that the POPS $\text{\sf Trop}^{+}_{\leq\eta}$ offers an
example of a POPS that belongs to Case (iii), but not to Case (ii). On one
hand, every $\text{\sf datalog}^{\circ}$ program converges in a finite number
of steps. On the other hand, consider the linear program $P$ in (17), and
assume $A()=\\{x_{0}\\}$, and $B()=\\{0\\}$ (the unit of $\text{\sf
Trop}^{+}_{\leq\eta}$). Base on the discussion above, $P$ requires
$\lceil\frac{\eta}{x_{0}}\rceil$ iterations, which depends on the value
$x_{0}$. We give another example in Appendix C.1.

###  6.3. Convergence in $T(|D|)$ steps

Next, we study conditions under which every program converges in $T(|D|)$
steps, for some function $T$. Unlike the previous case, here we insist that
the number of steps depends only on the size of the domain, and not on the
values in the value-space. This is precisely Case (ii) in our discussion. We
will give a complete characterization of the POPS $\bm{S}$ for this case,
assuming that $\circ$ is strict.

The simplest $\text{\sf datalog}^{\circ}$ program is the linear program (17).
By setting $A()=a\in\bm{S}$ and $B()=1\in\bm{S}$, the ICO of the program
becomes the simple linear function $f(x)=ax+1$, and the program converges in
$p+1$ steps iff $f$ is $p+1$ stable, iff $a$ is $p$-stable in $\bm{S}+\bot$
(Lemma 6.6). It follows that a necessary condition of $\text{\sf
datalog}^{\circ}$ programs to converge in $T(|D|)$ steps is that $\bm{S}+\bot$
be $p$-stable, for some fixed number $p$. We prove that this is also a
sufficient condition:

######  Theorem 6.10.

Let $\bm{S}$ be a POPS such that the semiring $\bm{S}+\bot$ is $p$-stable.
Consider a $\text{\sf datalog}^{\circ}$ program $P$, and recall that $N$ is
the number of ground IDB atoms. Then:

  * (i)

If $p=0$, then $P$ converges in at most $N$ steps.

  * (ii)

If $P$ is linear, then it converges in $\leq\sum_{i=1}^{N}(p+1)^{i}$ steps.

  * (iii)

In general, $P$ converges in $\leq\sum_{i=1}^{N}(p+2)^{i}$ steps.

The bounds given by the theorem are exponential in $N$, except for $0$-stable
POPS. For linear programs (case (ii)), we will see in Theorem 6.16 that $P$
can be computed in PTIME, using a different algorithm than naïve evaluation.
For case (iii), we could neither prove nor disprove a polynomial bound.

In the rest of this section we prove Theorem 6.10. The main technical result
consists in proving the stability of polynomial functions:

(21) $\displaystyle f(x)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle a_{0}+a_{1}x+a_{2}x^{2}+\cdots+a_{k}x^{k}$

We show the following. Recall that, throughout this paper we assume that the
semirings are commutative, i.e. $\otimes$ is commutative.

######  Theorem 6.11.

Let $\bm{S}$ be a $p$-stable semiring and let $f$ be a polynomial function
(21). Then, if $p=0$ then $f$ is $1$-stable; If $f$ is linear, then it is
$p+1$-stable; In general, $f$ is $p+2$-stable.

We include the proof in Appendix C.2, where we also give an example explaining
why in general $f$ is not $p+1$ stable.

Theorem 6.11 generalizes special cases studied by Gondran
(DBLP:journals/dm/Gondran79, ; semiring_book, ). The case of a $0$-stable
semiring has been most extensively studied. Such semirings are called simple
by Lehmann (DBLP:journals/tcs/Lehmann77, ), are called c-semirings by Kohlas
(DBLP:journals/ai/KohlasW08, ), and absorptive by Dannert et al.
(DBLP:conf/csl/DannertGNT21, ). In all cases the authors require $1+a=1$ for
all $a$ (or, equivalently, $b+ab=b$ for all $a,b$ (DBLP:conf/csl/DannertGNT21,
)), which is equivalent to stating that $a$ is 0-stable, and also equivalent
to stating that $(\bm{S},+)$ is a join-semilattice with maximal element $1$.
The tropical semiring is such an example; every distributive lattice is also a
0-stable semiring where we set $+=\vee$ and $\circ=\wedge$.

We will use Theorem 6.11 to prove Theorem 6.10. Let $\bm{S}$ be a POPS; recall
that we assumed $\circ$ is strict. A monomial is a function of the form
$f(x)=ax^{k}$ for some $k\geq 1$, and a polynomial is a sum of monomials. A
polynomial is similar to (21), except that some terms $a_{i}x^{i}$ may be
missing; if $\bm{S}$ does not satisfy the absorption $x\circ 0=0$, then we
can’t make these monomials 0 by setting $a_{i}=0$, but we simply allow them to
be missing. Theorem 6.11 implies:

######  Corollary 6.12.

Let $\bm{S}$ be a POPS such that $\bm{S}+\bot$ is $p$-stable, for some $p\geq
0$. Then every polynomial function $f:\bm{S}\rightarrow\bm{S}$ has the same
stability index as in Theorem 6.11, more precisely: $f$ is $p+2$-stable in
general, it is $1$-stable when $p=0$, and it is $p+1$-stable when $f$ is
linear.

###### Proof.

If $f(x)=b$ is a constant function, then the statement holds trivially, so
assume w.l.o.g. that $f$ contains at least one monomial $a_{k}x^{k}$ for
$k\geq 1$. Since $\bm{S}+\bot$ is a sub-semiring of $\bm{S}$, it follows that
the polynomial $f(x)$ is well defined on $\bm{S}+\bot$. More concretely, once
can check that, unless $f(x)$ is a constant, for every $x$,
$f(x+\bot)=f(x)+\bot$.

Next, we observe that $\bm{S}+\bot$ is naturally ordered. For that, we denote
by $\preceq$ the natural preorder defined by $+$ on $\bm{S}+\bot$, and prove
that $\preceq$ implies $\sqsubseteq$, which is the partial order on the POPS
$\bm{S}$. Since the latter is anti-symmetric, so is the former. To prove the
implication, assume that $a+\bot\preceq b+\bot$. Then there exists $x$ such
that $a+\bot+x=b+\bot$, and it follows that $a+\bot\sqsubseteq
a+\bot+x=b+\bot$.

Since every element in $\bm{S}+\bot$ is $p$-stable, by Theorem 6.11 every
polynomial over $\bm{S}+\bot$ is $q$-stable, for $q$ defined in the theorem.
Let $f(x)=\sum_{i}a_{i}x^{i}$ be a polynomial on $\bm{S}$. We assume w.l.o.g.
that its degree is $\geq 1$. Then $f+\bot$ is a polynomial over $\bm{S}+\bot$,
hence by Theorem 6.11 it is $q$-stable. We prove that $f$ is also $q$-stable.
For that, we first check by induction on $k\geq 1$ that
$f^{(k)}(\bot)=f^{(k)}(\bot)+\bot$. Indeed, when $k=1$,
$f(\bot)=\sum_{i}a_{i}\bot^{i}=a_{0}+\bot=f(\bot)+\bot$. Assuming the claim
holds for $k$, we compute
$f^{(k+1)}(\bot)=f(f^{(k)}(\bot))=f(f^{(k)}(\bot)+\bot)=f^{(k+1)}(\bot)+\bot$.
Next, we check also by induction that
$(f+\bot)^{(k)}(\bot)=f^{(k)}(\bot)+\bot$. The inductive step follows from
$(f+\bot)((f+\bot)^{(k)}(\bot))=(f+\bot)(f^{(k)}(\bot)+\bot)=f^{(k+1)}(\bot)+\bot$.
The $q$-stability of $f$ follows now from
$f^{(q)}(\bot)=(f+\bot)^{(q)}(\bot)=(f+\bot)^{(q+1)}(\bot)=f^{(q+1)}(\bot)$. ∎

We need one more step to complete the proof of Theorem 6.10. We observe that
the set of multivariate polynomials forms a c-clone (see Sec. 2), and
similarly, the set of linear functions forms a c-clone. Theorem 3.5 implies:

######  Corollary 6.13.

Let $\bm{S}$ be a $p$-stable POPS where $\circ$ is strict. Let
$\bm{f}=(f_{1},\ldots,f_{N})\colon\bm{S}^{N}\rightarrow\bm{S}^{N}$ be an
$N$-tuple of multivariate polynomial functions in $N$ variables. Then:

  * •

If $p=0$, then $f$ is $N$-stable.

  * •

If $f$ is linear, then it is $(p+1)+(p+1)^{2}+\cdots+(p+1)^{N}$-stable.

  * •

In general, $f$ is $(p+2)+(p+2)^{2}+\cdots+(p+2)^{N}$-stable.

The corollary immediately implies Theorem 6.10.

###  6.4. Convergence in PTIME

Assume, as before, a $p$-stable POPS where $\circ$ is strict. Theorem 6.10
gives an exponential (in the domain size) upper bound on the number of steps
of the naive evaluation algorithm. Is this bound tight? Or can a $\text{\sf
datalog}^{\circ}$ program be computed in PTIME? In this section we answer
partially these questions for linear $\text{\sf datalog}^{\circ}$ programs. In
this case, the immediate consequence operator is a linear function
$F:\bm{S}^{N}\rightarrow\bm{S}^{N}$.

First, we consider the case of a $p$-stable semiring. In this case the
immediate consequence operator can be written in matrix notation $F(X)=AX+B$,
where $A$ is an $N\times N$ matrix, and $X$, $B$ are $N$-dimensional column
vectors. After $q+1$ iterations, the naive algorithm computes
$F^{(q+1)}(0)=B+AB+A^{2}B+\cdots+A^{q}B=A^{(q)}B$, where
$A^{(q)}\stackrel{{\scriptstyle\text{def}}}{{=}}I_{N}+A+A^{2}+\cdots+A^{q}$.
The naive algorithm converges in $q+1$ steps iff $F$ is $q+1$-stable. A matrix
$A$ is called $q$-stable (semiring_book, ) if $A^{(q)}=A^{(q+1)}$. The
following is easy to check: the matrix $A$ is $q$-stable iff, for every vector
$B$, the linear function $F(X)=AX+B$ is $q+1$ stable. Our discussion implies
that, in order to determine the runtime of the naive algorithm on a linear
$\text{\sf datalog}^{\circ}$ program over a $p$-stable semiring, one has to
compute the stability index of an $N\times N$ matrix $A$ over that semiring.
Surprisingly, no polynomial bound for the stability index of a matrix is known
in general, except for $p=0$, in which case $A$ is $N$-stable (see
(DBLP:journals/dm/Gondran79, ), and also Corollary 6.13). We prove here a
result in the special case when the semiring is $\text{\sf Trop}_{p}$
(introduced in Example 4.6), which is $p$-stable.

######  Lemma 6.14.

Every $N\times N$ matrix over $\text{\sf Trop}_{p}$ semiring is
$(pN+p-1)$-stable. This bound is tight, i.e., there exist $N\times N$-matrices
over $\text{\sf Trop}_{p}$ whose stability index is $(pN+p-1)$.

We give the full proof in Appendix C.3, and sketch here the main idea. We
consider an $N\times N$-matrix over $\text{\sf Trop}_{p}$ as the adjacency
matrix of a directed graph with $N$ vertices and up to $p+1$ parallel edges
from some vertex $i$ to $j$. Then $A^{(k)}$ contains in position $(i,j)$ the
$p+1$ lowest-cost paths of up to $k$ edges from $i$ to $j$. The upper bound is
proved by arguing that $A^{(k)}$ with $k>pN+p-1$ cannot contribute to the
$p+1$ lowest-cost paths due to the existence of at least $p+1$ cycles along
such paths. For proving the lower bound, we take $A$ as the adjacency matrix
of the directed $N$-cycle.

The lemma immediately implies:

######  Corollary 6.15.

Any linear $\text{\sf datalog}^{\circ}$ program over $\text{\sf Trop}_{p}$,
converges in $pN+p-1$ steps, where $N=|D|^{O(1)}$ is the number of ground IDB
tuples. This bound is tight.

Second, we consider arbitrary $p$-stable POPS $\bm{S}$, where $\circ$ is
strict, and prove that every linear $\text{\sf datalog}^{\circ}$ program can
be computed in PTIME, but using an algorithm different from the naïve
algorithm.

When $\bm{S}$ is a semiring, then this follows from adapting Gaussian
elimination to semirings (MR1059930, ; DBLP:journals/tcs/Lehmann77, ), which
coincides with the Floyd-Warshall-Kleene algorithm. The algorithm and its
variants compute the closure $A^{*}$ of an $N\times N$ matrix in $O(N^{3})$
time, in a closed semiring. The same principle applies to a $p$-stable POPS:

######  Theorem 6.16.

Let $\bm{S}$ be a $p$-stable POPS, where $\circ$ is strict, and let
$f_{1},\ldots,f_{N}$ be $N$ linear functions in $N$ variables. Then, there is
an algorithm computing $\text{\sf lfp}(f_{1},\ldots,f_{N})$ in time
$O(pN+N^{3})$.

##  7\. Semi-Naive Optimization

Consider a single $\text{\sf datalog}^{\circ}$ stratum (see, e.g.,
(DBLP:books/aw/AbiteboulHV95, ) for a definition of this standard concept in
datalog) that repeatedly computes $R=F(R)$ until a fixpoint is reached. A
naive evaluation consists of repeatedly applying the immediate consequence
operator, that is we compute $R_{0},R_{1},R_{2},\ldots$ where
$R_{t+1}\stackrel{{\scriptstyle\text{def}}}{{=}}F(R_{t})$. As observed in
standard datalog, this strategy is inefficient because all facts discovered at
iteration $t$ will be re-discovered at iterations $t+1,t+2,\ldots$ The semi-
naive optimization consists of a modified program that computes $R_{t+1}$ by
first computing only the “novel” facts $\delta_{t+1}=F(R_{t})-R_{t}$, which
are then added to $R_{t}$ to form $R_{t+1}$. Efficiently computing
$F(R_{t})-R_{t}$ without fully evaluating $F(R_{t})$ is the incremental
computation problem typical of incremental view maintenance. There are
different incremental computation strategies, one of which is to exploit the
fact that $F$ is essentially multilinear (see definition below) to
incrementally compute $\delta_{t+1}=F(R_{t-1}+\delta_{t})-F(R_{t-1})$ without
fully evaluating $F(R_{t})$. This section generalizes semi-naive evaluation to
$\text{\sf datalog}^{\circ}$.

In standard datalog the difference operator is well defined, since the Boolean
semiring supports a difference operator as
$x-y\stackrel{{\scriptstyle\text{def}}}{{=}}x\wedge\neg y$. For a semi-naive
evaluation in $\text{\sf datalog}^{\circ}$, we need to define the difference
operator.

A dioid is a semiring $(S,+,\circ,0,1)$ for which $+$ is idempotent. It is
known (MR1608370, ) that a dioid is naturally ordered. Furthermore, the
natural order can be simplified by defining $a\sqsubseteq b$ iff $a+b=b$; and,
under this natural order, $+$ is the same as $\vee$. (See Appendix D.1.)
Dioids have many applications in a wide range of areas; see (MR1608370, ) for
many examples.

###### Definition 7.1.

A POPS $\bm{S}=(S,+,\circ,0,1,\sqsubseteq)$ is called a distributive dioid if
$(S,+,\circ,0,1)$ is a dioid, $\sqsubseteq$ is the dioid’s natural order, and
the lattice is distributive. In a distributive dioid, the difference operator
is defined by

(22) $\displaystyle b-a$
$\displaystyle\stackrel{{\scriptstyle\text{def}}}{{=}}\wedge\\{{c}\mid{a+c\sqsupseteq
b}\\}$

For example, the POPS $(2^{\bm{U}},\cup,\cap,\emptyset,\bm{U},\subseteq)$ is a
distributive dioid, whose difference operator is exactly set-difference
$b-a=\wedge\\{{c}\mid{b\subseteq a\cup c}\\}=b\setminus a$. The POPS
$\text{\sf Trop}=(\mathbb{R}\cup\\{\infty\\},\min,+,\infty,0,\geq)$ is a
distributive dioid, whose difference operator is defined by

(23) $\displaystyle b-a=$ $\displaystyle\begin{cases}b&\mbox{if }b\leq a\\\
\infty&\mbox{if }b>a\end{cases}$

$R_{0}\leftarrow\bm{0}$ $\delta_{0}\leftarrow\bm{0}$;

for  _ $t\leftarrow 1$ to $\infty$ _ do

$\delta_{t}\leftarrow F(R_{t-1})-R_{t-1}$;

// incremental computation

$R_{t}\leftarrow R_{t-1}+\delta_{t}$;

if  _ $\delta_{t}=\bm{0}$ _ then

Break

return $R_{t}$

Algorithm 2 Semi-naïve evaluation for $\text{\sf datalog}^{\circ}$

######  Theorem 7.2.

Let $F$ be a $\text{\sf datalog}^{\circ}$ program over a distributive dioid,
then the semi-naïve algorithm 2 returns the same solution as the naïve
algorithm (Algorithm 1).

A proof of the above theorem is in Appendix D. The next pillar of semi-naïve
computation is the fact that the rule $F(R_{t-1})-R_{t-1}$ can be computed
efficiently by incremental computation. Note that in general $F$ is a vector-
valued second-order function, mapping input IDBs to output IDBs. We describe
how to incrementally compute a component function of $F$. Without loss of
generality, consider a component function $f(R_{t-1})$ of $F$. We show how

(24) $\displaystyle f(R_{t-1})-R_{t-1}$
$\displaystyle=f(R_{t-2}+\delta_{t-1})-f(R_{t-2})$

can be computed incrementally.

Note that $f$ is a multivariate polynomial in the input IDBs. For the purpose
of incrementally computing (24) once, we can assume that no IDB in the input
of $f$ occurs twice without loss of generality; because, we can give every
occurrence of an IDB a unique name. (See Example D.4 for an illustration.) Let
$R_{t-2}=(A^{1},\cdots,A^{k})$ be the $k$-tuple of IDBs that $f$ is a function
of, and $\delta_{t-1}=(\delta^{1},\dots,\delta^{k})$.

######  Theorem 7.3.

Let $f$ be a component function of a $\text{\sf datalog}^{\circ}$ program $F$
over a distributive dioid in which every input IDB of $f$ occurs once in the
formula defining $f$. Then, $f$ is multilinear, i.e.

$\displaystyle f(A^{1},\dots,A^{j}+\delta^{j},\dots,A^{k})$ (25)
$\displaystyle=f(A^{1},\dots,A^{j},\dots,A^{k})+f(A^{1},\dots,\delta^{j},\dots,A^{k})$

If $f(\bm{A})=c+f^{\prime}(\bm{A})$ where $c$ is a constant, then the
incremental computation $f(R_{t-1})-R_{t-1}$ can be computed by the following
differential rule

(26) $f(A^{1}+\delta^{1},\dots,A^{k}+\delta^{k})-f(A^{1},\dots,A^{k})=\\\
\sum_{j=1}^{k}f^{\prime}(A^{1}+\delta^{1},\dots,A^{j-1}+\delta^{j-1},\delta^{j},A^{j+1},\dots,A^{k})\\\
-f(A^{1},\dots,A^{k})$

The simplest application of the differential rule (26) is when $F$ is linear,
in which case the rule takes a particularly simple form:

$\displaystyle\delta_{t+1}=F(R_{t-1}+\delta_{t})-F(R_{t-1})=F(\delta_{t})-F(R_{t-1})=F(\delta_{t})-R_{t}$

It should be noted that (26) is not the only way to implement the incremental
computation. We can use (25) to expand $f$ into up to $2^{k}-1$ many terms.
However, the linear expansion such as (26) is the most compact in terms of the
number of rules one has to evaluate to implement the incremental computation.
An example of how (26) works in the context of the APSP problem was presented
in Example 1.3.

##  8\. Related Work

To empower Datalog, researchers have proposed amendments to make datalog
capable of expressing some problems with greedy solutions such as APSP and
MST. Most notably, the non-deterministic choice construct was extensively
studied early on (MR1842100, ; DBLP:conf/pods/GrecoZG92, ;
DBLP:conf/icdt/GrecoSZ95, ). While datalog+choice is powerful, its expression
and semantics are somewhat clunky, geared totwards answering optimization
questions (greedily). In particular, it was not designed to deal with general
aggregations.

To evaluate recursive $\text{\sf datalog}^{\circ}$ program is to solve
fixpoint equations over semirings, which was studied in the automata theory
(MR1470001, ), program analysis (DBLP:conf/popl/CousotC77, ; MR1728440, ), and
graph algorithms (MR556411, ; MR584516, ; MR526496, ) communities since the
1970s. (See (MR1059930, ; DBLP:conf/lics/HopkinsK99, ;
DBLP:journals/tcs/Lehmann77, ; semiring_book, ; MR609751, ) and references
thereof). The problem took slighly different forms in these domains, but at
its core, it is to find a solution to the equation $x=f(x)$, where $x\in
S^{n}$ is a vector over the domain $S$ of a semiring, and $f:S^{n}\to S^{n}$
has multivariate polynomial component functions.

When $f$ is affine, researchers realized that many problems in different
domains are instances of the same problem, with the same underlying algebraic
structure: transitive closure (DBLP:journals/jacm/Warshall62, ), shortest
paths (DBLP:journals/cacm/Floyd62a, ), Kleene’s theorem on finite automata and
regular languages (MR0077478, ), continuous dataflow
(DBLP:conf/popl/CousotC77, ; DBLP:journals/jacm/KamU76, ), etc. Furthermore,
these problems share the same characteristic as the problem of computing
matrix inverse (MR427338, ; tarjan1, ; MR371724, ). The problem is called the
algebraic path problem (MR1059930, ), among other names, and the main task is
to solve the matrix fixpoint equation $\bm{X}=\bm{A}\otimes\bm{X}\oplus\bm{I}$
over a semiring.

There are several classes of solutions to the algebraic path problem, which
have pros and cons depending on what we can assume about the underlying
semiring (whether or not there is a closure operator, idempotency, natural
orderability, etc.). We refer the reader to (semiring_book, ; MR1059930, ) for
more detailed discussions. Here, we briefly summarize the main approaches.

The first approach is to keep iterate until a fixpoint is reached; in
different contexts, this has different names: the naïve algorithm, Jacobi
iteration, Gauss-Seidel iteration, or Kleene iteration. The main advantage of
this approach is that it assumes less about the underlying algebraic
structure: we do not need both left and right distributive law, and do not
need to assume a closure operator.

The second approach is based on Gaussian elimination (also, Gauss-Jordan)
elimination, which, assuming we have oracle access to the solution $x^{*}$ of
the 1D problem $x=1\oplus a\otimes x$, can solve the algebraic path problem in
$O(n^{3})$-time (MR1059930, ; DBLP:journals/tcs/Lehmann77, ).

The third approach is based on specifying the solutions based on the free
semiring generated when viewing $\bm{A}$ as the adjanceny matrix of a graph
(DBLP:journals/jacm/Tarjan81a, ). The underlying graph structure (such as
planarity) may sometimes be exploited for very efficient algorithm (MR584516,
; MR526496, ).

Beyond the affine case, since the 1960s researchers in formal languages have
been studying the structure of the fixpoint solution to $x=f(x)$ when $f$’s
component functions are multivariate polynomials over Kleene algebra
(MR339568, ; MR209093, ; MR912710, ). It is known, for example, that Kleene
iteration does not always converge (in a finite number of steps), and thus
methods based on Galois connection or on widening/narrowing approaches
(MR1252194, ) were studied. These approaches are (discrete) lattice-theoretic.
More recently, a completely different approach drawing inspiration from
Newton’s method for solving a system of (real) equations was proposed
(DBLP:conf/lics/HopkinsK99, ; DBLP:journals/jacm/EsparzaKL10, ).

Recall that Newton’s method for solving a system of equations $g(x)=0$ over
reals is to start from some point $x_{0}$, and at time $t$ we take the first
order approximation $g(x)\approx
g_{t}(x):=g(x_{t})+g^{\prime}(x_{t})(x-x_{t})$, and set $x_{t+1}$ to be the
solution of $g_{t}(x)=0$, i.e.
$x_{t+1}=x_{t}-[g^{\prime}(x_{t})]^{-1}g(x_{t})$. Note that in the
multivariate case $g^{\prime}$ is the Jacobian, and $[g^{\prime}(x_{t})]^{-1}$
is to compute matrix inverse. In beautiful papers, Esparza et al.
(DBLP:journals/jacm/EsparzaKL10, ) and Hopkins and Kozen
(DBLP:conf/lics/HopkinsK99, ) were able to generalize this idea to the case
when $g(x)=f(x)-x$ is defined over $\omega$-continuous semirings. They were
able to define an appropriate minus operator, derivatives of power series over
semirings, matrix inverse, and prove that the method converges at least as
fast as Kleene iteration, and there are examples where Kleene iteration does
not converge, while Newton method does. Furthermore, if the semiring is
commutative and idempotent (in addition to being $\omega$-continuous), then
Newton method always converges in $n$ Newton steps. Each Newton step involves
computing the Jacobian $g^{\prime}$ and computing its inverse, which is
exactly the algebraic path problem!

In (DBLP:journals/jlp/Fitting85a, ), Fitting proposed a three-valued semantics
of logic programs with $\bot$ (= undefined) denoting “neither false (0) nor
true (1)”. In our terminology, this comes down to considering datalog over the
partially ordered semiring THREE =
$(\\{\bot,\bm{0},\bm{1}\\},\vee,\wedge,\bm{0},\bm{1},\leq_{k})$, where
$\leq_{k}$ denotes the knowledge order $\bot\leq_{k}\bm{0},\bm{1}$. Negation
can be introduced as a function “$\mathtt{not}$” with
$\mathtt{not}(\bm{0})=\bm{1}$, $\mathtt{not}(\bm{1})=\bm{0}$, and
$\mathtt{not}(\bot)=\bot$. The immediate consequence operator is monotone
w.r.t. $\leq_{k}$ and thus guarantees the existence of a least fixpoint also
in the presence of negation. In (DBLP:journals/jlp/Fitting91, ;
DBLP:journals/jlp/Fitting93, ), Fitting further extended his approach to
Belnap’s four-valued logic FOUR and, more generally, to arbitrary bilattices.
FOUR $(\\{\bot,\bm{0},\bm{1},\top\\},\leq_{t},\leq_{k})$ constitutes the
simplest non-trivial, complete bilattice. That is, we have a complete lattice
both w.r.t. the truth order $\bm{0}\leq_{t}\bot,\top\leq_{t}\bm{1}$ and w.r.t.
the knowledge order $\bot\leq_{k}\bm{0},\bm{1}\leq_{k}\top$. The additional
truth value $\top$ in FOUR denotes “both false and true”. It provides a means
to deal with contradicting information in a meaningful way. Moreover, it
guarantees the existence of a greatest fixpoint of the immediate consequence
operator. Fitting uses this property to establish precise lower and upper
bounds of the set of stable models in terms of the orders $\leq_{t}$ and
$\leq_{k}$, with the well-founded model (DBLP:journals/jacm/GelderRS91, ) as
the smallest w.r.t. $\leq_{k}$. We provide a more detailed discussion of
Fitting’s work in Appendix E.

Recently, semi-naïve evaluation was extended for a higher-order functional
language called Datafun (DBLP:journals/pacmpl/ArntzeniusK20, ). The book
(semiring_book, ) contains many fundamental results on algebraic structures
related to semirings and computational problems on such structures.

##  9\. Conclusions

A massive number of application domains demand us to move beyond the confine
of the Boolean world: from program analysis (DBLP:conf/popl/CousotC77, ;
MR1728440, ), graph algorithms (MR556411, ; MR584516, ; MR526496, ),
provenance (DBLP:conf/pods/GreenKT07, ), formal language theory (MR1470001, ),
to machine learning and linear algebra (einsum:rocktaschel, ;
DBLP:conf/osdi/AbadiBCCDDDGIIK16, ). Semiring and poset theory – of which POPS
is an instance – is the natural bridge connecting the Boolean island to these
applications.

The bridge helps enlarge the set of problems $\text{\sf datalog}^{\circ}$ can
express in a very natural way. The possibilities are endless. For example,
amending $\text{\sf datalog}^{\circ}$ with an interpretive function such as
sigmoid will allow it to express typical neural network computations. Adding
another semiring to the query language111111In the functional aggregate
queries (DBLP:conf/pods/KhamisNR16, ) sense helps express rectilinear units in
modern deep learning. At the same time, the bridge facilitates the porting of
analytical ideas from Datalog to analyze convergence properties of the
application problems, and to carry over optimization techniques such as semi-
naïve evaluation.

This paper established part of the bridge. There are many interesting open
problems left open; we mention a few here.

The question of whether a $\text{\sf datalog}^{\circ}$ program over $p$-stable
POPS converges in polynomial time in $p$ and $N$ is open. This is open even
for linear programs. Our result on $\text{\sf Trop}_{p}$ indicates that the
linear case is likely in PTIME. If $p$-stability does not hold, then ACC was
the next best barrier. It would be interesting to have a sufficient condition
for convergence beyond ACC.

We can introduce negation to $\text{\sf datalog}^{\circ}$ as an interpreted
predicate. The question is, can we extend semantics results (such as stable
model semantics) from general datalog / logic programing to $\text{\sf
datalog}^{\circ}$ with negation? Section E in the appendix contains more
detailed discussions on this front. Beyond exact solution and finite
convergence, as mentioned in the introduction, it is natural in some domain
applications to have approximate fixpoint solutions, which will allow us to
tradeoff convergence time and solution quality. A theoretical framework along
this line will go a long way towards making $\text{\sf datalog}^{\circ}$ deal
with real machine learning, linear algebra, and optimization problems.

###### Acknowledgements.

Suciu and Wang were partially supported by NSF IIS 1907997 and NSF IIS
1954222. Pichler was supported by the Austrian Science Fund (FWF):P30930.

## References

  * (1) Abadi, M., Barham, P., Chen, J., Chen, Z., Davis, A., Dean, J., Devin, M., Ghemawat, S., Irving, G., Isard, M., Kudlur, M., Levenberg, J., Monga, R., Moore, S., Murray, D. G., Steiner, B., Tucker, P. A., Vasudevan, V., Warden, P., Wicke, M., Yu, Y., and Zheng, X. Tensorflow: A system for large-scale machine learning.  In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016 (2016), K. Keeton and T. Roscoe, Eds., USENIX Association, pp. 265–283.
  * (2) Abiteboul, S., Hull, R., and Vianu, V. Foundations of Databases.  Addison-Wesley, 1995.
  * (3) Aji, S. M., and McEliece, R. J. The generalized distributive law.  IEEE Trans. Inf. Theory 46, 2 (2000), 325–343.
  * (4) Arntzenius, M., and Krishnaswami, N. Seminaïve evaluation for a higher-order functional language.  Proc. ACM Program. Lang. 4, POPL (2020), 22:1–22:28.
  * (5) Backhouse, R. C., and Carré, B. A. Regular algebra applied to path-finding problems.  J. Inst. Math. Appl. 15 (1975), 161–186.
  * (6) Carré, B. Graphs and networks.  The Clarendon Press, Oxford University Press, New York, 1979.  Oxford Applied Mathematics and Computing Science Series.
  * (7) Cormen, T. H., Leiserson, C. E., Rivest, R. L., and Stein, C. Introduction to algorithms, third ed.  MIT Press, Cambridge, MA, 2009.
  * (8) Cousot, P., and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.  In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977 (1977), R. M. Graham, M. A. Harrison, and R. Sethi, Eds., ACM, pp. 238–252.
  * (9) Cousot, P., and Cousot, R. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation.  In Programming language implementation and logic programming (Leuven, 1992), vol. 631 of Lecture Notes in Comput. Sci. Springer, Berlin, 1992, pp. 269–295.
  * (10) Creignou, N., Kolaitis, P. G., and Vollmer, H., Eds.  Complexity of Constraints - An Overview of Current Research Themes [Result of a Dagstuhl Seminar] (2008), vol. 5250 of Lecture Notes in Computer Science, Springer.
  * (11) Dannert, K. M., Grädel, E., Naaf, M., and Tannen, V. Semiring provenance for fixed-point logic.  In 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference) (2021), C. Baier and J. Goubault-Larrecq, Eds., vol. 183 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 17:1–17:22.
  * (12) Davey, B. A., and Priestley, H. A. Introduction to lattices and order.  Cambridge University Press, Cambridge, 1990.
  * (13) Dechter, R. Bucket elimination: a unifying framework for processing hard and soft constraints.  Constraints An Int. J. 2, 1 (1997), 51–55.
  * (14) Esparza, J., Kiefer, S., and Luttenberger, M. Newtonian program analysis.  J. ACM 57, 6 (2010), 33:1–33:47.
  * (15) Fitting, M. A kripke-kleene semantics for logic programs.  J. Log. Program. 2, 4 (1985), 295–312.
  * (16) Fitting, M. Bilattices and the semantics of logic programming.  J. Log. Program. 11, 1&2 (1991), 91–116.
  * (17) Fitting, M. The family of stable models.  J. Log. Program. 17, 2/3&4 (1993), 197–225.
  * (18) Fitting, M. Fixpoint semantics for logic programming a survey.  Theor. Comput. Sci. 278, 1-2 (2002), 25–51.
  * (19) Floyd, R. W. Algorithm 97: Shortest path.  Commun. ACM 5, 6 (1962), 345.
  * (20) Freeman, L. C. A Set of Measures of Centrality Based on Betweenness.  Sociometry 40, 1 (Mar. 1977), 35–41.
  * (21) Gelder, A. V. The alternating fixpoint of logic programs with negation.  In Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 29-31, 1989, Philadelphia, Pennsylvania, USA (1989), A. Silberschatz, Ed., ACM Press, pp. 1–10.
  * (22) Gelder, A. V., Ross, K. A., and Schlipf, J. S. The well-founded semantics for general logic programs.  J. ACM 38, 3 (1991), 620–650.
  * (23) Gelfond, M., and Lifschitz, V. The stable model semantics for logic programming.  In Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, USA, August 15-19, 1988 (2 Volumes) (1988), R. A. Kowalski and K. A. Bowen, Eds., MIT Press, pp. 1070–1080.
  * (24) Gondran, M. Algèbre linéaire et cheminement dans un graphe.  Rev. Française Automat. Informat. Recherche Opérationnelle Sér. Verte 9, V-1 (1975), 77–99.
  * (25) Gondran, M. Les elements p-reguliers dans les dioïdes.  Discret. Math. 25, 1 (1979), 33–39.
  * (26) Gondran, M., and Minoux, M. Graphs, dioids and semirings, vol. 41 of Operations Research/Computer Science Interfaces Series.  Springer, New York, 2008.  New models and algorithms.
  * (27) Greco, S., Saccà, D., and Zaniolo, C. DATALOG queries with stratified negation and choice: from P to d${}^{\mbox{p}}$.  In Database Theory - ICDT’95, 5th International Conference, Prague, Czech Republic, January 11-13, 1995, Proceedings (1995), G. Gottlob and M. Y. Vardi, Eds., vol. 893 of Lecture Notes in Computer Science, Springer, pp. 82–96.
  * (28) Greco, S., and Zaniolo, C. Greedy algorithms in Datalog.  Theory Pract. Log. Program. 1, 4 (2001), 381–407.
  * (29) Greco, S., Zaniolo, C., and Ganguly, S. Greedy by choice.  In Proceedings of the Eleventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 2-4, 1992, San Diego, California, USA (1992), M. Y. Vardi and P. C. Kanellakis, Eds., ACM Press, pp. 105–113.
  * (30) Green, T. J., Karvounarakis, G., and Tannen, V. Provenance semirings.  In Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 11-13, 2007, Beijing, China (2007), L. Libkin, Ed., ACM, pp. 31–40.
  * (31) Gunawardena, J. An introduction to idempotency.  In Idempotency (Bristol, 1994), vol. 11 of Publ. Newton Inst. Cambridge Univ. Press, Cambridge, 1998, pp. 1–49.
  * (32) Hopkins, M. W., and Kozen, D. Parikh’s theorem in commutative kleene algebra.  In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999 (1999), IEEE Computer Society, pp. 394–401.
  * (33) Kam, J. B., and Ullman, J. D. Global data flow analysis and iterative algorithms.  J. ACM 23, 1 (1976), 158–171.
  * (34) Khamis, M. A., Ngo, H. Q., and Rudra, A. FAQ: questions asked frequently.  In Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2016, San Francisco, CA, USA, June 26 - July 01, 2016 (2016), T. Milo and W. Tan, Eds., ACM, pp. 13–28.
  * (35) Kleene, S. C. Representation of events in nerve nets and finite automata.  In Automata studies, Annals of mathematics studies, no. 34. Princeton University Press, Princeton, N. J., 1956, pp. 3–41.
  * (36) Kohlas, J. Information algebras - generic structures for inference.  Discrete mathematics and theoretical computer science. Springer, 2003\.
  * (37) Kohlas, J., and Wilson, N. Semiring induced valuation algebras: Exact and approximate local computation algorithms.  Artif. Intell. 172, 11 (2008), 1360–1399.
  * (38) Kuich, W. The Kleene and the Parikh theorem in complete semirings.  In Automata, languages and programming (Karlsruhe, 1987), vol. 267 of Lecture Notes in Comput. Sci. Springer, Berlin, 1987, pp. 212–225.
  * (39) Kuich, W. Semirings and formal power series: their relevance to formal languages and automata.  In Handbook of formal languages, Vol. 1. Springer, Berlin, 1997, pp. 609–677.
  * (40) Lehmann, D. J. Algebraic structures for transitive closure.  Theor. Comput. Sci. 4, 1 (1977), 59–76.
  * (41) Lipton, R. J., Rose, D. J., and Tarjan, R. E. Generalized nested dissection.  SIAM J. Numer. Anal. 16, 2 (1979), 346–358.
  * (42) Lipton, R. J., and Tarjan, R. E. Applications of a planar separator theorem.  SIAM J. Comput. 9, 3 (1980), 615–627.
  * (43) Liu, Y. A., and Stoller, S. D. Founded semantics and constraint semantics of logic rules.  J. Log. Comput. 30, 8 (2020), 1609–1668.
  * (44) Liu, Y. A., and Stoller, S. D. Recursive rules with aggregation: A simple unified semantics, 2020.
  * (45) Nielson, F., Nielson, H. R., and Hankin, C. Principles of program analysis.  Springer-Verlag, Berlin, 1999.
  * (46) Parikh, R. J. On context-free languages.  J. Assoc. Comput. Mach. 13 (1966), 570–581.
  * (47) Pilling, D. L. Commutative regular equations and Parikh’s theorem.  J. London Math. Soc. (2) 6 (1973), 663–666.
  * (48) Przymusinski, T. C. The well-founded semantics coincides with the three-valued stable semantics.  Fundam. Inform. 13, 4 (1990), 445–463.
  * (49) Rocktäschel, T. Einsum is all you need - Einstein summation in deep learning.  https://rockt.github.io/2018/04/30/einsum.
  * (50) Ross, K. A., and Sagiv, Y. Monotonic aggregation in deductive databases.  In Proceedings of the Eleventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 2-4, 1992, San Diego, California, USA (1992), M. Y. Vardi and P. C. Kanellakis, Eds., ACM Press, pp. 114–126.
  * (51) Rote, G. Path problems in graphs.  In Computational graph theory, vol. 7 of Comput. Suppl. Springer, Vienna, 1990, pp. 155–189.
  * (52) Scott, D., and Strachey, C. Toward a mathematical semantics for computer languages, 1971.
  * (53) Shenoy, P. P., and Shafer, G. Axioms for probability and belief-function proagation.  In UAI ’88: Proceedings of the Fourth Annual Conference on Uncertainty in Artificial Intelligence, Minneapolis, MN, USA, July 10-12, 1988 (1988), R. D. Shachter, T. S. Levitt, L. N. Kanal, and J. F. Lemmer, Eds., North-Holland, pp. 169–198.
  * (54) Stanley, R. P. Enumerative combinatorics. Volume 1, second ed., vol. 49 of Cambridge Studies in Advanced Mathematics.  Cambridge University Press, Cambridge, 2012.
  * (55) Tarjan, R. E. Graph theory and gaussian elimination, 1976.  J.R. Bunch and D.J. Rose, eds.
  * (56) Tarjan, R. E. A unified approach to path problems.  J. ACM 28, 3 (1981), 577–593.
  * (57) Warshall, S. A theorem on boolean matrices.  J. ACM 9, 1 (1962), 11–12.
  * (58) Zaharia, M., Xin, R. S., Wendell, P., Das, T., Armbrust, M., Dave, A., Meng, X., Rosen, J., Venkataraman, S., Franklin, M. J., Ghodsi, A., Gonzalez, J., Shenker, S., and Stoica, I. Apache spark: a unified engine for big data processing.  Commun. ACM 59, 11 (2016), 56–65.
  * (59) Zimmermann, U. Linear and combinatorial optimization in ordered algebraic structures.  Ann. Discrete Math. 10 (1981), viii+380.

APPENDIX

##  Appendix A Proof of Lemma 3.4

Recall that, for every $a\in\bm{L}_{1}$, $g_{a}$ denotes the function
$g_{a}(y)=g(a,y)$; its type is $\bm{L}_{2}\rightarrow\bm{L}_{2}$, and
$g_{a}^{(k)}\in\mathcal{C}$ for every $k\geq 0$, because $\mathcal{C}$ is a
c-clone. Similarly, the type of
$F(x)\stackrel{{\scriptstyle\text{def}}}{{=}}f(x,g^{(q)}(x,\bot))$ is
$\bm{L}_{1}\rightarrow\bm{L}_{1}$, and $F^{(k)}\in\mathcal{C}$ for all $k\geq
0$.

###### Claim 1.

The pair $(\bar{x},\bar{y})$ defined by (10) is a fixpoint of $h$.

The claim follows immediately from

$g(\bar{x},\bar{y})=g_{\bar{x}}(\bar{y})=g_{\bar{x}}(g_{\bar{x}}^{(q)}(\bot)=g_{\bar{x}}^{(q+1)}(\bot)=g_{\bar{x}}^{(q)}(\bot)=\bar{y}$

by the definition of $\bar{y}$ and the $q$-stability of $g_{\bar{x}}$.
Similarly,

$f(\bar{x},\bar{y})=f(\bar{x},g_{\bar{x}}^{(q)}(\bot))=F(\bar{x})=\bar{x}$

by the definition of $\bar{x}$ and the $p$-stability of $F$, proving that
$(\bar{x},\bar{y})$ is a fixpoint of $h$.

###### Claim 2.

The pair $(\bar{x},\bar{y})$ defined by (10) is a least fixpoint of $h$.

Since $h$ is monotone, it converges to the least fixpoint. It follows that,
for every $n\geq 0$,
$(a_{n},b_{n})\stackrel{{\scriptstyle\text{def}}}{{=}}h^{(n)}(\bot,\bot)\sqsubseteq(\bar{x},\bar{y})$.
Hence, to prove Claim 2 it is sufficient to show that
$(\bar{x},\bar{y})\sqsubseteq(a_{n},b_{n})$ for some $n$.

We will show that $(\bar{x},\bar{y})\sqsubseteq(a_{pq+p+q},b_{pq+p+q})$. To
prove this inequality, we observe that the pair $(\bar{x},\bar{y})$ defined by
(10) is the last term of the following (not necessarily increasing) sequence:

$\displaystyle(\bot,\bot)=$
$\displaystyle(x_{0},y_{0,0}),(x_{0},y_{0,1}),\cdots,(x_{0},y_{0,q}),$
$\displaystyle(x_{1},y_{1,0}),(x_{1},y_{1,1})\cdots(x_{1},y_{1,q}),$
$\displaystyle\ldots$ (27)
$\displaystyle(x_{p},y_{p,0}),(x_{p},y_{p,1}),\cdots,(x_{p},y_{p,q})=(\bar{x},\bar{y})$

where:

$\displaystyle x_{0}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\bot$ $\displaystyle
y_{k,0}\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle\bot$
$\displaystyle x_{k+1}\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
f(x_{k},y_{k,q})$ $\displaystyle
y_{k,\ell+1}\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
g(x_{k},y_{k,\ell})$

In the $(x_{k},y_{k,\ell})$ sequence each element is obtained from the
previous one by applying either a $g$-step (from $(x_{k},y_{k,\ell})$ to
$(x_{k},y_{k,\ell+1})$) or an $f$-step (from $(x_{k},y_{k,q})$ to
$(x_{k+1},y_{k+1,0})$). The sequence (27) can be visualized as:

$\displaystyle(gg\cdots g)\ f\ (gg\cdots g)\ f\ \cdots\ (gg\cdots g)\ f\
(gg\cdots g)$

Instead of proving $(\bar{x},\bar{y})\sqsubseteq(a_{pq+p+q},b_{pq+p+q})$, we
prove a stronger claim, which completes the proof of Claim 2

###### Claim 3.

For every $n\geq 0$, $(x_{k},y_{k,\ell})\sqsubseteq(a_{n},b_{n})$, where
$n=k(q+1)+\ell$ is the position of $(x_{k},y_{k,\ell})$ in the sequence (27).

Before proving the claim, we notice $h^{(n)}(\bot,\bot)\sqsubseteq
h^{(n+1)}(\bot,\bot)$ implies $a_{n}\sqsubseteq f(a_{n},b_{n})$ and
$b_{n}\sqsubseteq g(a_{n},b_{n})$. Now we prove the claim by induction. Assume
the claim holds for $(x_{k},y_{k,\ell})$. If the next element
$(x_{k},y_{k,\ell+1})$ is obtained via a $g$-step then we have:

$\displaystyle(x_{k},y_{k,\ell+1})=$
$\displaystyle(x_{k},g_{x_{k}}(y_{k,\ell}))=(x_{k},g(x_{k},y_{k,\ell}))\sqsubseteq(a_{n},g(a_{n},b_{n}))$
$\displaystyle\sqsubseteq$
$\displaystyle(f(a_{n},b_{n}),g(a_{n},b_{n}))=(a_{n+1},b_{n+1})$

hence the claim holds for $(x_{k},y_{k,\ell+1})$ as well. If the next element
$(x_{k+1},y_{k+1,0})$ is obtained via an $f$-step (which happens when
$\ell=q$) then we use the fact that $y_{k+1,0}=\bot$ and derive:

$\displaystyle(x_{k+1},\bot)=$
$\displaystyle(f(x_{k},y_{k,q}),\bot)\sqsubseteq(f(x_{k},y_{k,q}),y_{k,q})$
$\displaystyle\sqsubseteq$
$\displaystyle(f(a_{n},b_{n}),b_{n})\sqsubseteq(f(a_{n},b_{n}),g(a_{n},b_{n}))=(a_{n+1},b_{n+1})$

This completes the proof of the claim.

Finally, to prove Lemma 3.4, note that $\bar{x}=x_{p}$ was already reached at
the beginning of the last line in (27), thus $\bar{x}=a_{n}$ for $n=pq+p$. By
switching the roles of $f$ and $g$, we can reach the same least fixpoint
$(\bar{x},\bar{y})$ using a sequence $(f\cdots f)g(f\cdots f)g\cdots g(f\cdots
f)$, similar to (27). The end of this sequence is the same $(\bar{x},\bar{y})$
because the least fixpoint is unique. By the same argument as above, we have
$\bar{y}=b_{n}$ for $n=pq+q$. This completes the proof of the lemma.

##  Appendix B More Discussion of POPS

###  B.1. Pre-semirings to POPS

We describe a general procedure to convert a pre-semiring to a POPS.

###### Definition B.1.

Let $\bm{S}$ be a pre-semiring. We say that a POPS $\bm{S}_{1}$ extends
$\bm{S}$ if $\bm{S}\subseteq\bm{S}_{1}$, and the operations
$\oplus,\otimes,0,1$ in $\bm{S}$ are the same as those in $\bm{S}_{1}$.

We describe ways to extend a pre-semiring $\bm{S}=(S,+,*,0,1)$ to a POPS, all
inspired by abstract interpretations in programming languages
(DBLP:conf/popl/CousotC77, ).

Representing Undefined:

The lifting operation is defined by setting
$\bm{S}_{\bot}\stackrel{{\scriptstyle\text{def}}}{{=}}\bm{S}\cup\\{\bot\\}$
and extending the operations to $x+y=x*y=\bot$ whenever $x=\bot$ or $y=\bot$.
The value $\bot$ represents undefined.

Representing Contradiction:

We further extend $\bm{S}_{\bot}$ by defining
$\bm{S}_{\bot}^{\top}\stackrel{{\scriptstyle\text{def}}}{{=}}\bm{S}_{\bot}\cup\\{\top\\}$
and setting $\bot+\top=\bot*\top=\bot$, $0*\top=0$, and $x+\top=x*\top=\top$
when $x\neq\bot,x\neq 0$. The new element $\top$ represents contradiction.
Intuitively: $\bot$ is the empty set $\\{\\}$, while $\top$ is the entire set
$S$.

Incomplete values:

More generally, define
$I\stackrel{{\scriptstyle\text{def}}}{{=}}{\mathcal{P}}_{\text{fin}}(S)\cup\\{S\\}$;
that is, $I$ consists of all finite subsets of $S$, plus $S$ itself (which we
add explicitly when $S$ is infinite). The operations $\oplus,\otimes$ are
defined set-wise, such that, if the result of an operation is an infinite set,
then we replace it with $S$. Intuitively, a finite set $\\{u,v,w\\}\in I$
represents a value that can be either $u$ or $v$ or $w$. Here $\bot=\\{\\}$
and $\top=S$.

###  B.2. Strictness of $\oplus$ and $\otimes$ are independent

We give two examples of POPS where only one of the two operators
$\oplus,\otimes$ is strict.

Strict $\otimes$:

In any non-trivial naturally ordered semiring $\otimes$ is strict, while
$\oplus$ is not. For example, consider $(\mathbb{N},+,*,0,1,\leq)$. Then $*$
is strict because $x*0=0$, while $+$ is not strict because $x+0\neq 0$ for
$x\neq 0$.

Strict $\otimes$:

Next, consider the semiring
$(\mathbb{N}\cup\\{\top\\},\oplus,\otimes,\\{0\\},\\{1\\},\supseteq)$, where
$\top$ the infinite set $\\{0,1,2,\ldots\\}$. We view each element
$x\in\mathbb{N}$ as the singleton set $\\{x\\}$, and define the operations
$\oplus,\otimes$ set-wise: $A\oplus
B\stackrel{{\scriptstyle\text{def}}}{{=}}\\{{x+y}\mid{x\in A,y\in B}\\}$,
$A\otimes B\stackrel{{\scriptstyle\text{def}}}{{=}}\\{{x*y}\mid{x\in A,y\in
B}\\}$, where we replace the result with $\top$ if the resulting set is not a
singleton. Concretely, we have:

$\displaystyle\\{x\\}\oplus\\{y\\}=$ $\displaystyle\\{x+y\\}$
$\displaystyle\\{x\\}\oplus\top=$ $\displaystyle\top$
$\displaystyle\\{x\\}\otimes\\{y\\}=$ $\displaystyle\\{x*y\\}$
$\displaystyle\\{0\\}\oplus\top=$ $\displaystyle\\{0\\}$ $\displaystyle x\neq
0:\ \\{x\\}\oplus\top=\top$

Since $\top$ is the smallest element, $\oplus$ is strict, while $\otimes$ is
not.

###  B.3. Need for Pre-Semirings

$\mathbb{N}_{\bot}$ and the similarly defined $\mathbb{R}_{\bot}$ are pre-
semirings. They are not semirings, because $\bot*0=\bot$, thus $0$ is not
absorptive. It is possible to define an extension $\mathbb{N}\cup\\{\bot\\}$
of $\mathbb{N}$ that is a semiring, by simply re-defining $\bot*0=0$ and
$\bot*x=\bot$ for $x\neq 0$. However, no POPS extension of $\mathbb{R}$ exists
that is a semiring:

###### Lemma B.1.

If $\bm{S}$ is any POPS extension of $(\mathbb{R},+,*,0,1)$, then $\bm{S}$ is
not a semiring, i.e. it fails the absorption law $0*x=0$.

###### Proof.

Let $\bm{S}=(S,+,*,0,1,\sqsubseteq)$ be an ordered semiring that is an
extension of the semiring $(\mathbb{R},+,*,0,1)$. In particular
$\mathbb{R}\subseteq S$ and $S$ has a minimal element $\bot$. Since 0, 1 are
identity elements for $+,*$ we have:

$\displaystyle\bot+0=$ $\displaystyle\bot$ $\displaystyle\bot*1=$
$\displaystyle\bot$

We claim that the following more general identities hold:

$\displaystyle\forall x\in\mathbb{R}:\ \bot+x=$ $\displaystyle\bot$
$\displaystyle\forall x\in\mathbb{R}-\\{0\\}:\bot*x=$ $\displaystyle\bot$

To prove the first identity, we use the fact that $+$ is monotone in $\bm{S}$
and $\bot$ is the smallest element and derive
$\bot+x\sqsubseteq(\bot+(y-x))+x=\bot+y$ for fall $x,y$. This implies
$\bot+x=\bot+y$ for all $x,y$ and the claim follows by setting $y=0$. The
proof of the second identity is similar: first observe that
$\bot*x\sqsubseteq(\bot*\frac{y}{x})*x=\bot*y$ hence $\bot*x=\bot*y$ for all
$x,y\in\mathbb{R}-\\{0\\}$, and the claim follows by setting $y=1$.

Since $\bm{S}$ is a semiring it satisfies the absorption law, hence
$\bot*0=0$. We prove now that $0=\bot$. Choose any $x\in\mathbb{R}-\\{0\\}$,
and derive:

$\displaystyle\bot*(x+(-x))=$ $\displaystyle\bot*0=0$
$\displaystyle(\bot*x)+(\bot*(-x))=$ $\displaystyle\bot+\bot=\bot$

By distributivity, the two lines are equal, hence $0=\bot$, and thus $0$ is
the smallest element in $\bm{S}$. Then, for every $x\in\mathbb{R}$, we have
$x+0\sqsubseteq x+(-x)=0$, which implies implies $x=0$, contradiction. ∎

##  Appendix C Proofs and Extensions of Section 6

###  C.1. Separating Case (iii) from Case (ii)

We describe a POPS $\bm{S}$ such that (1) every $\text{\sf datalog}^{\circ}$
program converges in a finite number of steps, and (2) the program $P$ in (17)
requires a number of steps that depends on the values of $A()$ and $B()$.

###### Example C.1.

For $k\geq 1$, define the semiring

$\bm{S}_{k}=(\\{0,\ldots,k\\},\max,\circ_{k},0,1),$

where $x\circ_{k}y=\min(x\circ y,k)$. $\bm{S}_{k}$ is naturally ordered.
Define $\bm{S}$ to be the following semiring. Its elements are sequences
$(x_{1},x_{2},\ldots)$ where $x_{k}\in\bm{S}_{k}$, such that only finitely
many elements $x_{k}$ are $\geq 2$: in other words, there exists $k_{0}$ such
that $\forall k>k_{0}$, $x_{k}\leq 1$. The semiring operations are defined
component-wise, from the operations on $\bm{S}_{k}$:
$\bm{x}\oplus\bm{y}=(\max(x_{1},y_{1}),\max(x_{2},y_{2}),\cdots)$ and
$\bm{x}\otimes\bm{y}=(x_{1}\circ_{1}y_{1},x_{2}\circ_{2}y_{2},\cdots)$. The
unit elements are $\bm{0}=(0,0,0,\cdots)$ and $\bm{1}=(1,1,1,\cdots)$
respectively. We show claim (2): the number of iterations required by (17)
depends on the values of the EDBs. Indeed, suppose the values of the two EDBs
are $A()=(0,0,\cdots,2,\cdots)$ and $B()=(0,0,\cdots,1,\cdots)$, where the
single non-zero value is on position $k$. After $q\geq 1$ iterations, the
value $X^{(q)}()$ is $(0,0,\cdots,1+2+\cdots+2^{q-1},\cdots)$. The program
converges after $\lceil\log(k)\rceil$ iterations, with the value
$X()=(0,0,\ldots,k,\ldots)$.

It remains to prove claim (1): every $\text{\sf datalog}^{\circ}$ program
converges. Consider any $\text{\sf datalog}^{\circ}$ program and any input EDB
predicate instance. Let $\bm{e}=(e_{1},e_{2},\cdots)$ be any EDB value, and
let $k_{0}=k_{0}(\bm{e})$ be the largest index such that $e_{k_{0}}\geq 2$.
Let $k\stackrel{{\scriptstyle\text{def}}}{{=}}\max_{\bm{e}}k_{0}(\bm{e})$. It
turns out that we may restrict ourselves to the sub-semiring of $\bm{S}$
consisting of all sequences $(x_{0},x_{1},\ldots)$ where $x_{i}\leq 1$ for all
$i>k$. Indeed, this set is a sub-semiring, i.e., it is closed under
$\oplus,\otimes$. It follows that we can evaluate the $\text{\sf
datalog}^{\circ}$ program $P$ in this sub-semiring and, furthermore, it’s rank
is $k$ (see Def. 3.1), therefore, by Theorem 6.2, the $\text{\sf
datalog}^{\circ}$ program converges in $kN$ steps.

###  C.2. Proof of Theorem 6.11

The first two claims are easy to show. Assume $p=0$, then $1+c=1$ for every
$c\in S$. Then $f^{(1)}(0)=a_{0}$ and
$f^{(2)}(0)=a_{0}+\sum_{i=1,k}a_{0}^{i}a_{i}=a_{0}\circ\left(1+\sum_{i=1,k}a_{0}^{i-1}a_{i}\right)=a_{0}\circ
1=a_{0}=f^{(1)}(0)$, proving the first claim. For the second claim, we notice
that, if $f$ is linear, then
$f^{(p+1)}(0)=a_{0}+a_{0}a_{1}+a_{0}a_{1}^{2}+\cdots+a_{0}a_{1}^{p}=a_{0}a_{1}^{(p)}$,
and $f^{(p+1)}(0)=f^{(p+2)}(0)$ because $a_{1}$ is $p$-stable.

The last (and most general) claim requires more work. Fix a semiring $\bm{S}$,
thus the absorption rule $x0=0$ holds (we abbreviate $a\circ b$ with $ab$ for
readability), and also recall that all semirings in this paper are commutative
$xy=yx$. Fix a polynomial $f(x)$, as in (21). For every $q\geq 0$,
$f^{(q)}(0)$ is a sum of a bag of monomials of the form
$m=a_{0}^{r_{0}}a_{1}^{r_{1}}\cdots a_{k}^{r_{k}}$. Some monomial may occur
multiple times in $f^{(q)}(0)$, hence we view $f^{(q)}(0)$ as a bag of
monomials rather than a set. For a simple illustration, consider the
polynomial:

(28) $\displaystyle f(x)=$ $\displaystyle b+ax^{2}$

Then:

$\displaystyle f^{(0)}(0)$ $\displaystyle=0$ $\displaystyle f^{(1)}(0)$
$\displaystyle=b$ $\displaystyle f^{(2)}(0)$ $\displaystyle=b+ab^{2}$
$\displaystyle f^{(3)}(0)$ $\displaystyle=b+a(b+ab^{2})^{2}$
$\displaystyle=b+ab^{2}+2a^{2}b^{3}+a^{3}b^{4}$ $\displaystyle f^{(4)}(0)$
$\displaystyle=b+a(b+ab^{2}+2a^{2}b^{3}+a^{3}b^{4})^{2}$
$\displaystyle=b+ab^{2}+2a^{2}b^{3}+5a^{3}b^{4}+\cdots$

(When $q\geq n$ then the coefficient of $a^{n}b^{n+1}$ is the Catalan number
$\frac{1}{n}\binom{2n}{n-1}$, see e.g. (semiring_book, , pp. 103).) If we
denote by $\texttt{bag}(f^{(q)}(0))$ the bag of monomials in $f^{(q)}(0)$,
then one can check by induction that
$\texttt{bag}(f^{(q)}(0))\subseteq\texttt{bag}(f^{(q+1)}(0))$. Assume that the
semiring $S$ is $p$-stable. Then, we prove that any new monomials contributed
by $f^{(p+3)}(0)$ that were not present in $f^{(p+2)}(0)$ are absorbed by a
sum of monomials present in $f^{(p+2)}(0)$, using the $p$-stability property.
For a simple illustration, assuming $\bm{S}$ is 2-stable, then the monomial
$a^{3}b^{4}$ is already redundant in $f^{(3)}(0)$ (and, thus, redundant in
$f^{(q)}(0)$ for all $q\geq 3$), because $f^{(3)}(0)$ also contains the
monomials $b$, $ab^{2}$, and $a^{2}b^{3}$, and their sum absorbs $a^{3}b^{4}$:

$\displaystyle b+ab^{2}+a^{2}b^{3}+a^{3}b^{4}$
$\displaystyle=b(1+ab+(ab)^{2}+(ab)^{3})$ $\displaystyle=b(1+ab+(ab)^{2})$
$\displaystyle=b+ab^{2}+a^{2}b^{3}.$

The plan for proving Theorem 6.11 is as follows:

  * •

We show in Prop. C.3 the following. For any $q\geq 0$, if $f^{(q)}(0)$
contains some monomial $m=a_{0}^{r_{0}}a_{1}^{r_{1}}\cdots a_{k}^{r_{k}}$ with
at least one degree $r_{\ell}\geq p+1$, then we can write the monomial as
$m=b^{p+1}c$ such that $f^{(q)}(0)$ also contains all monomials
$c,bc,b^{2}c,\ldots,b^{p}c$. In particular, the monomial $m$ is redundant in
$f^{(q)}(0)$, because $c+bc+\ldots+b^{p}c=c+bc+\ldots+b^{p}c+b^{p+1}c$. Thus,
for any $q\geq 0$, we can view $f^{(q)}(0)$ as a sum of monomials where all
degrees are $\leq p$.

  * •

Recall that in a $p$-stable semiring $p+1=1+1+\cdots+1=1+1+\cdots+1+1=p+2$,
which implies that, for any $N,N^{\prime}\geq p+1$, $N=N^{\prime}$. We show in
Prop. C.4 that any monomial $m=a_{0}^{r_{0}}a_{1}^{r_{1}}\cdots a_{k}^{r_{k}}$
with all degrees $\leq p$ that is present in $f^{(n)}(0)$ for some $n\geq
p+3$, is already present in $f^{(p+2)}(0)$ and, moreover, the multiplicities
$N,N^{\prime}$ of $m$ in the two expressions is either equal, or both are
$\geq p+1$; in particular, $Nm=N^{\prime}m$. Together with the previous item,
this implies that $f^{(p+2)}(0)=f^{(n)}(0)$, proving the theorem.

We start by characterizing $\texttt{bag}(f^{(q)}(0))$ using the following
context-free grammar $G$. The grammar has one non-terminal, $x$, has $k+1$
terminals, $a_{0},a_{1},\ldots,a_{k}$, and the following rules:

$\displaystyle x\rightarrow$ $\displaystyle a_{0}$ $\displaystyle
x\rightarrow$ $\displaystyle a_{1}x$ $\displaystyle x\rightarrow$
$\displaystyle a_{2}xx$ $\displaystyle\ldots$ $\displaystyle x\rightarrow$
$\displaystyle a_{k}xx\cdots x$

(there are $k$ copies of $x$ in the last production). We define a derivation
tree using a minor variation121212In the standard textbook definition a node
is labeled with a non-terminal (in our case it is always $x$) and a production
rule $x\rightarrow a_{i}xx\cdots x$, then it has $i+1$ children, where in our
case the first child is a leaf labeled $a_{i}$, and the remaining $i$ children
are each labeled with $x$. Given our simplified grammar, we prefer to move
$a_{i}$ to the node itself instead of making it a child. of the standard
textbook definition.

###### Definition C.2.

A derivation tree, $T$, is an ordered tree where every node
$t\in\text{nodes}(T)$ is labeled with
$\lambda(t)\in\\{x,a_{0},a_{1},\ldots,a_{k}\\}$, such that every node labeled
$\lambda(t)=a_{i}$ has exactly $i$ children, and every node labeled
$\lambda(t)=x$ is a leaf node. A terminal derivation tree is one where no node
is labeled $x$; thus, all its leaf nodes are labeled with $a_{0}$.

The monomial defined by $T$ is
$m\stackrel{{\scriptstyle\text{def}}}{{=}}\prod_{t\in\text{Nodes}(T)}\lambda(t)$.
If the monomial does not include $x$ we call it a terminal monomial. For
example, $a_{0}^{2}a_{2}^{3}x^{2}$ is a monomial, and $a_{0}^{4}a_{2}^{3}$ is
a terminal monomial; we only consider terminal monomials. The depth of a
derivation tree $T$ is the largest number of nodes on any path from the root
to a leaf. For $q\geq 0$, define $\texttt{Tree}_{q}(G)$ the set of terminal
derivation trees of depth $\leq q$, and define the bag
$L_{q}(G)\stackrel{{\scriptstyle\text{def}}}{{=}}\\{{\lambda(T)}\mid{T\in\texttt{Tree}_{q}(G)}\\}$;
thus, the multiplicity of a monomial $m\in L_{q}(G)$ is equal to the number of
derivation trees for $m$. Finally, denote by $L(G)$ the set of all derivation
trees, of any depth:
$L(G)\stackrel{{\scriptstyle\text{def}}}{{=}}\bigcup_{q}L_{q}(G)$. The
following is easily verified and the proof is omitted.

###### Proposition C.1.

For every $q\geq 0$, $\texttt{bag}(f^{(q)}(0))=L_{q}(G)$.

For a simple illustration, referring to our running example (28), the grammar
$G$ is:

$\displaystyle x\rightarrow$ $\displaystyle b$ $\displaystyle x\rightarrow
axx$

There are two derivation trees that produce the terminal monomial $a^{2}b^{3}$
namely:

$\displaystyle x\rightarrow$ $\displaystyle axx\rightarrow abx\rightarrow
ab(axx)\rightarrow ab(abb)$ $\displaystyle x\rightarrow$ $\displaystyle
axx\rightarrow axb\rightarrow a(axx)b\rightarrow a(abb)b$

Both define the same monomial because $\bm{S}$ is commutative.

We view each terminal monomial $m=a_{0}^{r_{0}}a_{1}^{r_{1}}\cdots
a_{k}^{r_{k}}$ as a vector
$\bm{r}=(r_{0},r_{1},\ldots,r_{k})\in\mathbb{N}^{k+1}$; we shall also write
$m=\bm{a}^{\bm{r}}$. Next, we characterize the vectors $\bm{r}$ that define
the monomials $m\in L(G)$.

###### Proposition C.2.

Let $\bm{r}=(r_{0},r_{1},\ldots,r_{k})$ and $m=\bm{a}^{\bm{r}}$. Then the
following conditions are equivalent:

(29) $\displaystyle r_{0}=$ $\displaystyle 1+\sum_{i=1,k}(i-1)r_{i}$ (30)
$\displaystyle m\in$ $\displaystyle L(G)$

###### Proof.

We start by proving that (30) implies (29). This follows from a simple
counting argument. Let $m\in L(G)$, and $T$ be a derivation tree defining $m$.
We count the number of nodes in $T$ in two ways. On one hand
$|\texttt{Nodes}(T)|=\sum_{i=0,k}r_{i}$, since each of the $r_{i}$ occurrences
of $a_{i}$ is the label of a distinct node. On the other hand
$|\texttt{Nodes}(T)|=1+|\texttt{Edges}(T)|=1+\sum_{i=1,k}ir_{i}$, since each
node other than the root has exactly one incoming edge, and each node labeled
$a_{i}$ has exactly $i$ outgoing edges. Therefore:

$\displaystyle r_{0}+r_{1}+\cdots+r_{k}=$ $\displaystyle
1+r_{1}+2r_{2}+\cdots+kr_{k}$

which implies (29).

Next, we prove that (29) implies (30), by induction on the lexicographic
ordering of the vectors $\bm{r}=(r_{0},r_{1},\ldots,r_{k})$. Assume $\bm{r}$
satisfies condition (29). We will describe a derivation tree $T$ that defines
the terminal monomial
$m\stackrel{{\scriptstyle\text{def}}}{{=}}\bm{a}^{\bm{r}}$. Notice that
$r_{1}$ is not constrained in any way by the condition (29). We will assume
w.l.o.g. that $r_{1}=0$: if $r_{1}>0$, then we simply add a chain of length
$r_{1}$ on top of the root, pictorially $a_{1}\rightarrow
a_{1}\rightarrow\cdots\rightarrow a_{1}\rightarrow T$, where $T$ is the
derivation realizing the terminal monomial with exponents
$(r_{0},0,r_{1},r_{2},\ldots,r_{k})$. Thus, we prove by induction on the
lexicographic order of the sequence $\bm{r}=(r_{0},0,r_{1},\ldots,r_{k})$ that
there exists a derivation tree $T$ that defines the terminal monomial
$\lambda(T)=\bm{a}^{\bm{r}}$. Let $\ell$ be the largest index s.t.
$r_{\ell}>0$. We consider two cases:

  * •

If $\ell=0$ then $\bm{r}=(1,0,\ldots,0)$. The corresponding terminal monomial,
$m=a_{0}$, is generated by a single node, labeled $a_{0}$.

  * •

If $\ell\geq 2$; thus, $\bm{r}=(r_{0},0,r_{2},\ldots,r_{\ell},0,0,\ldots,0)$.
Condition (29) implies $r_{0}=1+\sum_{i\geq 1}(i-1)r_{i}\geq
1+(\ell-1)r_{\ell}\geq\ell$. Define: