# Revisiting Semiring Provenance for Datalog

Camille Bourgaux1 Pierre Bourhis2 Liat Peterfreund3 Michaël Thomazo1
1DI ENS, ENS, CNRS, PSL University & Inria, Paris, France
2CRIStAL, CNRS, University of Lille, Inria, Lille, France
3LIGM, CNRS, Université Gustave Eiffel, ENPC, Paris, France
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Data provenance consists in bookkeeping meta information during query
evaluation, in order to enrich query results with their trust level,
likelihood, evaluation cost, and more. The framework of semiring provenance
abstracts from the specific kind of meta information that annotates the data.
While the definition of semiring provenance is uncontroversial for unions of
conjunctive queries, the picture is less clear for Datalog. Indeed, the
original definition might include infinite computations, and is not consistent
with other proposals for Datalog semantics over annotated data. In this work,
we propose and investigate several provenance semantics, based on different
approaches for defining classical Datalog semantics. We study the relationship
between these semantics, and introduce properties that allow us to analyze and
compare them.

##  1 Introduction

Datalog is a rule language widely studied both in the database community,
where it is seen as a query language, and in the KR community, as an ontology
language.

In relational databases, the framework of _semiring provenance_ was introduced
to generalize computations over annotated databases, e.g., the semantics of
probabilistic databases (?), the bag semantics, lineage or why-provenance (?).
In this framework, the semantics of positive relational algebra queries over
databases annotated with elements of any commutative semiring is inductively
defined on the structure of the query (?; ?). _Provenance semirings_ are
expressions (such as polynomials) built from variables associated to each
tuple of the database (?). A provenance expression provides a general
representation of how tuples have been used to derive a query result, and can
be faithfully evaluated in any semiring in which the considered provenance
semiring can be homomorphically embedded.

Semiring provenance has also been studied for Datalog queries, for which it
was defined based on the set of all _derivation trees_ for the query (?; ?;
?). However, this definition seems less axiomatic than in the case of
relational databases. Indeed, there may be infinitely many derivation trees,
leading to infinite provenance expressions, while Datalog programs have finite
models that can be computed efficiently (?). A consequence is that this
definition is valid only for a restricted class of semirings, namely
$\omega$-continuous. Recently, ? (?) restrict the semiring even further by
considering fully-chain complete semirings in order to extend provenance
definition to logical languages featuring negation and fixed-point. Even if
numerous useful semirings are $\omega$-continuous, or can be extended to a
such semiring, infinite provenance expressions may be considered unintuitive
in some cases. Consider, for example, the counting semiring (i.e., natural
numbers with standard operations) for which provenance of positive relational
algebra queries corresponds to their bag semantics. This semiring can be
extended to an $\omega$-continuous one by adding $\infty$ to the natural
numbers, hence providing a way to capture the bag semantics for Datalog
queries (?; ?). However, query answers having infinite multiplicities may not
seem very natural or informative. Moreover, alternative bag semantics for
languages close to Datalog have been defined, and would not lead to such
infinite multiplicities when applied to Datalog. This is in particular the
case of the bag semantics for ontology-based data access (?; ?), which
corresponds to one of the two semantics proposed for source-to-target tuple
generating dependencies in the context of data exchange (?). Interestingly,
these bag semantics are not based on derivation trees but are _model-
theoretic_ semantics: they define annotated interpretations, and conditions
for rules satisfaction over such interpretations. Such model-theoretic
semantics have also been used in other contexts to evaluate Datalog and
variants over annotated databases, such as fuzzy Datalog (?) or description
logic knowledge bases annotated with provenance tokens (?; ?). Finally, yet
other semantics definitions have been proposed for some use cases. For
instance, ? (?) consider _minimal depth proof trees_ , which correspond to a
Datalog _evaluation algorithm_ , with the intended use of understanding the
computation of the result, and guiding debugging.

The fact that the above semantics are not encompassed by the definition of
semiring provenance for Datalog, along with the need of handling infinite
computations which are entailed by this definition, motivate us to investigate
alternative natural semantics that might be a better fit in different
contexts.

In this paper we introduce several natural provenance semantics for Datalog
over annotated data. Our definitions are based on different classical
approaches: model-theoretic, execution-based and proof tree-based. They
capture the semantics mentioned previously, and are inspired by practical
needs. For instance, our semantics definition based on minimal depth
derivation trees capture the behavior of Datalog engines, such as Soufflé (?),
that store only minimal depth derivation trees instead of storing them all
(which might be impossible in case there are infinitely many); Our semantics
based on non-recursive derivation trees (in which a fact is not derived from
itself) resembles the approach taken by some graph query languages, e.g.,
SPARQL and Cypher, to handle queries with possibly infinite outputs by
allowing to explicitly restrict the output to include only simple paths. In
addition, some of the semantics suggested in the paper are closely related to
paradigms for weighted reasoning in the context of words and trees (?; ?).

After defining these different semantics, we study under which conditions they
coincide and investigate their connections. We then provide a general
framework for defining such provenance semantics, and present several
properties relevant for provenance semantics that allow us to compare them. We
briefly discuss some complexity issues in conclusion. Proofs and additional
discussion are available in the appendix.

##  2 Preliminaries

###  2.1 Datalog

We use the standard Datalog settings (cf. (?) part D).

#### Syntax

Let $\bf{P}$, $\bf{C}$, and $\bf{V}$ be mutually disjoint, possibly infinite
sets of _predicates_ , _constants_ , and _variables_ respectively. Elements of
$\bf{C}\cup\bf{V}$ are called _terms_. An _atom_ has the form
$p(t_{1},\dots,t_{n})$ where $p\in\bf{P}$ is an $n$-ary predicate, and
$t_{i}$’s are terms. A _fact_ (or _ground atom_) is a variable-free atom. A
_(Datalog) rule_ is an expression:
$\forall\vec{x}\forall\vec{y}(\phi(\vec{x},\vec{y})\rightarrow\psi(\vec{x}))$
where $\vec{x}$ and $\vec{y}$ are tuples of variables and
$\phi(\vec{x},\vec{y})$ and $\psi(\vec{x})$ are conjunctions of atoms whose
variables are $\vec{x}\cup\vec{y}$ and $\vec{x}$ respectively. We call
$\phi(\vec{x},\vec{y})$ and $\psi(\vec{x})$ the _body_ and _head_ of the rule,
respectively. From now on, we assume that rules are in _normalized form_ ,
i.e., the head consists of a single atom $H(\vec{x})$, and quantifiers are
implicit. The _domain_ $\mathcal{D}(\mathcal{A})$ of a set $\mathcal{A}$ of
atoms is the set of terms that appear in its atoms.

A _database_ $D$ is a finite set of facts, and a _Datalog program (or
ontology)_ $\Sigma$ is a finite set of Datalog rules. The _schema_ of $D$
(resp. $\Sigma$) denoted $\mathcal{S}(D)$ (resp. $\mathcal{S}(\Sigma)$) is the
set of predicates that appear in its atoms.111 Note that we do not require the
set of predicates of atoms appearing in heads of rules to be disjoint from
$\mathcal{S}(D)$; naturally, all of our results are valid under this
assumption as well.

#### Semantics

The semantics of Datalog can classically be defined in three ways: through
models, fixpoints or derivation trees. All three definitions rely on the
notion of homomorphism: a _homomorphism_ from a set $\mathcal{A}$ of atoms to
a set $\mathcal{B}$ of atoms is a function
$h:\mathcal{D}(\mathcal{A})\rightarrow\mathcal{D}(\mathcal{B})$ such that
$h(t)=t$ for all $t\in\bf{C}$, and $p(t_{1},\dots,t_{n})\in\mathcal{A}$
implies $h(p(t_{1},\cdots,t_{n})):=p(h(t_{1}),\dots,h(t_{n}))\in\mathcal{B}.$
We denote by $h(\mathcal{A})$ the set $\\{h(p(t_{1},\dots,t_{n}))\mid
p(t_{1},\dots,t_{n})\in\mathcal{A}\\}$. The homomorphism definition is
extended to conjunctions of atoms by viewing them as the sets of atoms they
contain.

A set $I$ of facts is a _model_ of a rule
$r:=\phi(\vec{x},\vec{y})\rightarrow\psi(\vec{x})$, denoted by $I\models r$,
if every homomorphism $h$ from $\phi(\vec{x},\vec{y})$ to $I$ is also a
homomorphism from $\psi(\vec{x})$ to $I$; it is a _model_ of a Datalog program
$\Sigma$ if $I\models r$ for every $r\in\Sigma$; it is a _model_ of a database
$D$ if $D\subseteq I$. A fact $\alpha$ is _entailed_ by $D$ and $\Sigma$,
denoted $\Sigma,D\models\alpha$, if $\alpha\in I$ for every model $I$ of
$\Sigma$ and $D$.

######  Example 1.

Let $\Sigma$ contain the rules $B(x)\rightarrow A(x)$, $R(x,y)\wedge
A(y)\rightarrow B(x)$, and $R(x,y)\rightarrow R(y,x)$, and
$D:=\\{B(a),B(b),R(a,b),R(b,a)\\}$. Each model of $D$ and $\Sigma$ contains
all facts in $D$ as well as $A(a)$ and $A(b)$, which are thus entailed by
$\Sigma,D$.

An equivalent way to define the entailment of a fact $\alpha$ by $D$ and
$\Sigma$ is to check if there is a homomorphism from $\alpha$ to a specific
model, defined as the _least fixpoint_ containing $D$ of the immediate
consequence operator: An immediate consequence for $D$ and $\Sigma$ is either
$\alpha\in D$, or $\alpha$ such that there exists a rule
$r:=\phi(\vec{x},\vec{y})\rightarrow\psi(\vec{x})$ and a homomorphism $h$ from
$\phi(\vec{x},\vec{y})$ to $D$ such that $h(\psi(\vec{x}))=\alpha$.

Finally, a third definition relies on derivation trees.

######  Definition 1 (Derivation Tree).

A _derivation tree_ $t$ of a fact $\alpha$ w.r.t. a database $D$ and a program
$\Sigma$ is a finite tree whose leaves are labeled by facts from $D$ and non-
leaf nodes are labeled by triples $(p(t_{1},\ldots,t_{m}),r,h)$ where

  * •

$p(t_{1},\ldots,t_{m})$ is a fact over the schema $\mathcal{S}(\Sigma)$;

  * •

$r$ is a rule from $\Sigma$ of the form $\phi(\vec{x},\vec{y})\rightarrow
p(\vec{x})$;

  * •

$h$ is a homomorphism from $\phi(\vec{x},\vec{y})$ to the facts of the labels
of the node children, such that $h(p(\vec{x}))=p(t_{1},\ldots,t_{m})$;

  * •

there is a bijection $f$ between the node children and the atoms of
$\phi(\vec{x},\vec{y})$, such that for every
$q(\vec{z})\in\phi(\vec{x},\vec{y})$, $f(q(\vec{z}))$ is of the form
$(h(q(\vec{z})),r^{\prime},h^{\prime})$ or is a leaf labeled by
$h(q(\vec{z}))$.

Moreover, if $(p(t_{1},\cdots,t_{m}),r,h)$ or $p(t_{1},\cdots,t_{m})$ is the
root of $t$, then $p(t_{1},\cdots,t_{m})=\alpha$.

######  Example 2.

Let $\Sigma$ contain $r_{1}:=R(x,y)\rightarrow H(x,x)$,
$r_{2}:=R(x,y)\rightarrow H(x,y)$ and $r_{3}:=S(x,y,z)\wedge
S(x,z,y)\rightarrow H(x,x)$. If $D=\\{R(a,a),S(a,b,c),S(a,c,b)\\}$, then the
fact $\alpha:=H(a,a)$ has the following derivation trees
$(\alpha,r_{1},h)$$R(a,a)$ $(\alpha,r_{2},h)$$R(a,a)$
$(\alpha,r_{3},h_{3})$$S(a,b,c)$$S(a,c,b)$
$(\alpha,r_{3},h_{3}^{\prime})$$S(a,c,b)$$S(a,b,c)$ where $h(x)=h(y)=a$,
$h_{3}(x)=a$, $h_{3}(y)=b$, $h_{3}(z)=c$ and $h^{\prime}_{3}(x)=a$,
$h^{\prime}_{3}(y)=c$, $h^{\prime}_{3}(z)=b$.

Note that when the program at hand is recursive (i.e., the dependency graph of
its predicates contains cycles) a fact may have infinitely many derivation
trees. Figure 1 depicts some of the infinitely many derivation trees of $A(a)$
from Example 1. In this example, and from this point on, we omit rules and
homomorphisms from trees when there is no ambiguity.

$A(a)$$B(a)$

$A(a)$$B(a)$$R(a,b)$$A(b)$$B(b)$

$A(a)$$B(a)$$R(a,b)$$R(b,a)$$A(b)$$B(b)$

Figure 1:  Some derivation trees of $A(a)$ in Example 1.

#### Queries

A _conjunctive query_ (CQ) is an existentially quantified formula
$\exists\vec{y}\,\phi(\vec{x},\vec{y})$ where $\phi(\vec{x},\vec{y})$ is a
conjunction of atoms with variables in $\vec{x}\cup\vec{y}$; a _union of
conjunctive queries_ (UCQ) is a disjunction of CQs (over the same free
variables). A query is _Boolean_ if it has no free-variables. A set of facts
$I$ satisfies a Boolean CQ (BCQ) $q:=\exists\vec{y}\,\phi(\vec{y})$, written
$I\models q$, if and only if there is a homomorphism from $\phi(\vec{y})$ to
$I$. A BCQ $q$ is _entailed_ by a Datalog program $\Sigma$ and database $D$,
written $\Sigma,D\models q$, if and only if $I\models q$ for every model $I$
of $\Sigma$ and $D$. Note that $\Sigma,D\models q$ if and only if
$\Sigma\cup\\{\phi(\vec{y})\rightarrow\mathsf{goal}\\},D\models\mathsf{goal}$,
where $\mathsf{goal}$ is a nullary predicate such that
$\mathsf{goal}\notin\mathcal{S}(\Sigma)\cup\mathcal{S}(D)$. A tuple of
constants $\vec{a}$ is an _answer_ to a CQ
$q(\vec{x}):=\exists\vec{y}\,\phi(\vec{x},\vec{y})$ over $\Sigma$ and $D$ if
$\vec{a}$ and $\vec{x}$ have the same arity and $\Sigma,D\models q(\vec{a})$
where $q(\vec{a})$ is the BCQ obtained by replacing the variables from
$\vec{x}$ with the corresponding constants from $\vec{a}$. When
$\Sigma=\emptyset$, it amounts to the existence of a homomorphism from
$q(\vec{a})$ to $D$, which corresponds to the semantics of CQs over relational
databases.

###  2.2 Annotated Databases

To equip databases with extra information, their facts might be annotated
with, e.g., trust levels, clearance degree required to access them, or
identifiers to track how they are used.

In the framework of semiring provenance, annotations are elements of algebraic
structures known as commutative semirings. A _semiring_
$\mathbb{K}=(K,+_{\mathbb{K}},\times_{\mathbb{K}},0_{\mathbb{K}},1_{\mathbb{K}})$
is a set $K$ with distinguished elements $0_{\mathbb{K}}$ and
$1_{\mathbb{K}}$, equipped with two binary operators: $+_{\mathbb{K}}$, called
the _addition_ , which is an associative and commutative operator with
identity $0_{\mathbb{K}}$, and $\times_{\mathbb{K}}$, called the
_multiplication_ , which is an associative operator with identity
$1_{\mathbb{K}}$. It also holds that $\times_{\mathbb{K}}$ distributes over
$+_{\mathbb{K}}$, and $0_{\mathbb{K}}$ is annihilating for
$\times_{\mathbb{K}}$. When multiplication is commutative, the semiring is
said to be _commutative_. We use the convention according to which
multiplication is applied before addition to omit parentheses. We omit the
subscript of operators and distinguished elements when there is no ambiguity.

######  Definition 2.

An _annotated database_ is a triple $(D,\mathbb{K},\lambda)$ where $D$ is a
database,
$\mathbb{K}=(K,+_{\mathbb{K}},\times_{\mathbb{K}},0_{\mathbb{K}},1_{\mathbb{K}})$
is a semiring, and $\lambda:D\mapsto K\setminus\\{0_{\mathbb{K}}\\}$ maps
facts into semiring elements different from $0_{\mathbb{K}}$.

######  Example 3 (Ex. 1 cont’d).

The semiring $\mathbb{N}=(\mathbb{N},+,\times,0,1)$ of the natural numbers
equipped with the usual operations is used for bag semantics. The tropical
semiring $\mathbb{T}=(\mathbb{R}^{\infty}_{+},\mathsf{min},+,\infty,0)$ is
used to compute minimal-cost paths. We define
$\lambda_{\mathbb{N}}:D\mapsto\mathbb{N}\setminus\\{0\\}$ by
$\lambda_{\mathbb{N}}(B(a))=3$, $\lambda_{\mathbb{N}}(B(b))=1$,
$\lambda_{\mathbb{N}}(R(a,b))=2$, $\lambda_{\mathbb{N}}(R(b,a))=1$; And
$\lambda_{\mathbb{T}}:D\mapsto\mathbb{R}_{+}$ by
$\lambda_{\mathbb{T}}(B(a))=10$, $\lambda_{\mathbb{T}}(B(b))=1$,
$\lambda_{\mathbb{T}}(R(a,b))=5$, $\lambda_{\mathbb{T}}(R(b,a))=2$.

We next list some possible properties of semirings. A semiring is _$+\,$
-idempotent_ (resp. _$\times$ -idempotent_) if for every $a\in K$, $a+a=a$
(resp. $a\times a=a$). It is _absorptive_ if for every $a,b\in K$, $a\times
b+a=a$. It is _positive_ if for every $a,b\in K$, $a\times b=0$ if and only if
($a=0$ or $b=0$), and $a+b=0$ if and only if $a=b=0$. Finally, an important
class is that of $\omega$-continuous commutative semirings in which infinite
sums are well-defined. Given a semiring, we define the binary relation
$\sqsubseteq$ such that $a\sqsubseteq b$ if and only if there exists $c\in K$
such that $a+c=b$. A commutative semiring is _$\omega$ -continuous_ if
$\sqsubseteq$ is a partial order, every (infinite) $\omega$-chain
$a_{0}\sqsubseteq a_{1}\sqsubseteq a_{2}\dots$ has a least upper bound
$\sup((a_{i})_{i\in\mathbb{N}})$, and for every $a$,
$a+\sup((a_{i})_{i\in\mathbb{N}})=\sup((a+a_{i})_{i\in\mathbb{N}})$ and
$a\times\sup((a_{i})_{i\in\mathbb{N}})=\sup((a\times
a_{i})_{i\in\mathbb{N}})$.

The semantics of queries from the positive relational algebra, and in
particular of UCQs, over annotated databases is defined inductively on the
structure of the query (?). Intuitively, joint use of data (conjunction)
corresponds to multiplication, and alternative use of data (union or
projection) corresponds to addition.

######  Example 4 (Ex. 3 cont’d).

The BCQ $\exists xy\,(R(x,y)\wedge B(y))$ is entailed from
$(D,\mathbb{N},\lambda_{\mathbb{N}})$ with multiplicity
$\lambda_{\mathbb{N}}(R(a,b))\times\lambda_{\mathbb{N}}(B(b))+\lambda_{\mathbb{N}}(R(b,a))\times\lambda_{\mathbb{N}}(B(a))=5$,
and from $(D,\mathbb{T},\lambda_{\mathbb{T}})$ with minimal cost
$\mathsf{min}(\lambda_{\mathbb{T}}(R(a,b))+\lambda_{\mathbb{T}}(B(b)),\lambda_{\mathbb{T}}(R(b,a))+\lambda_{\mathbb{T}}(B(a)))=6$.

A semantics of Datalog over annotated databases has been defined by ? (?)
using derivation trees, that we shall name the _all-tree semantics_. It
associates to each fact $\alpha$ entailed by $\Sigma$ and $D$ the following
sum, where $T^{\Sigma}_{D}(\alpha)$ is the set of all derivation trees for
$\alpha$ w.r.t. $\Sigma$ and $D$ and $\Lambda(t):=\prod_{v\text{ is a leaf of
$t$}}\lambda(v)$ is the $\mathbb{K}$-annotation of the derivation tree $t$
(since $\mathbb{K}$ is commutative, the result of the product is well-
defined).

$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\sum_{t\in
T^{\Sigma}_{D}(\alpha)}\Lambda(t).$

Since $T^{\Sigma}_{D}(\alpha)$ may be infinite, $\mathcal{P}^{\texttt{AT}}$ is
well-defined for all $\Sigma$, $(D,\mathbb{K},\lambda)$ and $\alpha$ only in
the case where $\mathbb{K}$ is $\omega$-continuous.

######  Example 5 (Ex. 3 cont’d).

The fact $\alpha:=A(a)$ is entailed with minimal cost:
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{T},\lambda_{\mathbb{T}},\alpha)=\mathsf{min}_{t\in
T^{\Sigma}_{D}(\alpha)}\Sigma_{v\text{ is a leaf of
$t$}}\lambda_{\mathbb{T}}(v)=3$. Since $\mathbb{N}$ is not
$\omega$-continuous,
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$
is not defined.

###  2.3 Provenance Semirings

Provenance semirings have been introduced to abstract from a particular
semiring by associating a unique provenance token to each fact of the
database, and building expressions that trace their use. Given a set $X$ of
_variables_ that annotate the database, a _provenance semiring_
$\mathit{Prov}(X)$ is a semiring over a space of provenance expressions with
variables from $X$.

Various such semirings were introduced in the context of relational databases
(?): The most expressive annotations are provided by the _provenance
polynomials_ semiring $\mathbb{N}[X]:=(\mathbb{N}[X],+,\times,0,1)$ of
polynomials with coefficients from $\mathbb{N}$ and variables from $X$, and
the usual operations. Less general provenance semirings include, for example,
the semiring $\mathbb{B}[X]:=(\mathbb{B}[X],+,\times,0,1)$ of polynomials with
Boolean coefficients, and the semiring
$\mathit{PosBool}(X):=(\mathit{PosBool}(X),\vee,\wedge,\mathsf{false},\mathsf{true})$
of positive Boolean expressions.

In the Datalog context, it is important to allow for infinite provenance
expressions, as there can be infinitely many derivation trees. A _formal power
series_ with variables from $X$ and coefficients from $K$ is a mapping that
associates to each monomial over $X$ a coefficient in $K$. A formal power
series $S$ can be written as a possibly infinite sum
$S=\Sigma_{m\in\mathsf{mon}(X)}S(m)m$ where $\mathsf{mon}(X)$ is the set of
monomials over $X$ and $S(m)$ is the coefficient of the monomial $m$. The set
of formal power series with variables from $X$ and coefficients from $K$ is
denoted $K\llbracket X\rrbracket$. ? (?) define the _Datalog provenance
semiring_ as the semiring $\mathbb{N}^{\infty}\llbracket X\rrbracket$ of
formal power series with coefficients from
$\mathbb{N}^{\infty}=\mathbb{N}\cup\\{\infty\\}$.

A _semiring homomorphism_ from
$\mathbb{K}=(K,+_{\mathbb{K}},\times_{\mathbb{K}},0_{\mathbb{K}},1_{\mathbb{K}})$
to
$\mathbb{K^{\prime}}=(K^{\prime},+_{\mathbb{K^{\prime}}},\times_{\mathbb{K^{\prime}}},0_{\mathbb{K^{\prime}}},1_{\mathbb{K^{\prime}}})$
is a mapping $h:K\rightarrow K^{\prime}$ such that
$h(0_{\mathbb{K}})=0_{\mathbb{K^{\prime}}}$,
$h(1_{\mathbb{K}})=1_{\mathbb{K^{\prime}}}$, and for all $a,b\in K$,
$h(a+_{\mathbb{K}}b)=h(a)+_{\mathbb{K^{\prime}}}h(b)$ and
$h(a\times_{\mathbb{K}}b)=h(a)\times_{\mathbb{K^{\prime}}}h(b)$. A semiring
homomorphism between $\omega$-continuous semirings is _$\omega$ -continuous_
if it preserves least upper bounds:
$h(\sup((a_{i})_{i\in\mathbb{N}}))=\sup((h(a_{i}))_{i\in\mathbb{N}})$.

Following ? (?), we say that a provenance semiring $\mathit{Prov}(X)$
_specializes_ correctly to a semiring $\mathbb{K}$, if any valuation
$\nu:X\rightarrow K$ extends uniquely to a ($\omega$-continuous if
$\mathit{Prov}(X)$ and $\mathbb{K}$ are $\omega$-continuous) semiring
homomorphism $h:\mathit{Prov}(X)\rightarrow K$, allowing the computations for
$\mathbb{K}$ to factor through the computations for $\mathit{Prov}(X)$. A
provenance semiring $\mathit{Prov}(X)$ is _universal for a set of semirings_
if it specializes correctly to each semiring of this set. ? (?) showed that
$\mathbb{N}[X]$ is universal for commutative semirings, and
$\mathbb{N}^{\infty}\llbracket X\rrbracket$ is universal for commutative
$\omega$-continuous semirings.

##  3 Alternative Semantics

In this section we propose several natural ways of defining the semantics of
Datalog over annotated databases, and investigate their connections. We have
seen that the semantics of Datalog can equivalently be defined through models,
fixpoints or derivation trees. The semantics we propose also fall into these
three approaches. For presentation purposes, we see each semantics as a
partial function $\mathcal{P}$ that associates to a Datalog program $\Sigma$,
annotated database $(D,\mathbb{K},\lambda)$, and fact $\alpha$, a semiring
element $\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.

###  3.1 Model-Based Semantics

We first investigate two provenance semantics based on Datalog’s model-
theoretic semantics. In both cases, we will define interpretations
$(I,\mu^{I})$ where $I$ is a set of facts and $\mu^{I}$ is a function that
annotates facts of $I$, and formulate requirements for them to be models of
$\Sigma$ and $(D,\mathbb{K},\lambda)$, extending standard models of $\Sigma$
and $D$ with fact annotations.

#### Annotated Model-based

? (?) define two bag semantics in the context of data exchange: the
_incognizant_ and _cognizant_ semantics. The difference between them arise
from the two different semantics of bag union: the incognizant semantics uses
the maximum-based union, while the cognizant semantics uses the sum-based
union.

In more details, both semantics are based on the following semantics for
source-to-target tuple generating dependencies (s-t tgds): a pair $(I,J)$ of
source and target instances satisfies an s-t tgd $q_{1}(\vec{x})\rightarrow
q_{2}(\vec{x})$ if for every answer $\vec{a}$ to $q_{1}$ over $I$, $\vec{a}$
is an answer to $q_{2}$ over $J$ with at least the same multiplicity. Given a
set of s-t tgds $\Sigma$ and a source $I$, a target $J$ is an _incognizant
solution_ for $I$ w.r.t. $\Sigma$ if $(I,J)$ satisfies every s-t tgd in
$\Sigma$. It is a _cognizant solution_ if for every $r\in\Sigma$, there is a
target instance $J_{r}$ such that $(I,J_{r})$ satisfies $r$ and $\uplus
J_{r}\subseteq J$, where $\uplus$ denotes the sum-union of bags (i.e., the
multiplicity of each element of the sum-union is equal to the sum of its
multiplicities). The incognizant (resp. cognizant) _certain answers_ to a
query $q$ w.r.t. $\Sigma$ on $I$ are defined using bag intersection of the
answers over the incognizant (resp. cognizant) solutions for $I$ w.r.t.
$\Sigma$, i.e., the multiplicity of an answer is the minimum of its
multiplicities over the solutions. Note that for BCQs, the only possible
certain answer is the empty tuple.

For example, consider $\Sigma=\\{B(x)\rightarrow A(x),C(x)\rightarrow A(x)\\}$
and $D=\\{(B(a),1),(C(a),1)\\}$. Under the incognizant semantics, the
multiplicity of the certain answer of the Boolean query $A(a)$ w.r.t. $\Sigma$
and $D$ is $1$ while under the cognizant semantics it is $2$. Indeed,
$J=\\{(A(a),1)\\}$ is an incognizant solution for $D$ w.r.t. $\Sigma$ as it
satisfies both s-t tgds, but is not a cognizant solution as the sum of
multiplicities that arise from the two rules is $2$.

It is easy to show that the cognizant semantics is equivalent to
$\mathcal{P}^{\texttt{AT}}$ on the counting semiring
$\mathbb{N}=(\mathbb{N},+,\times,0,1)$, and thus coincides with the classical
bag semantics for Datalog. However, we have seen that the incognizant and
cognizant semantics differ. Moreover, note that in the field of ontology-based
data access, the bag semantics defined by ? for DL-LiteR (?; ?) coincides with
the _incognizant_ semantics, thus disagrees with the classical Datalog bag
semantics (?; ?).

We hence define a provenance semantics that coincides with these semantics
when used with the counting semiring. Since it is based on greatest lower
bounds, it is defined on a restricted class of semirings.

Let $\mathbb{K}=(K,+,\times,0,1)$ be a commutative $\omega$-continuous
semiring such that for every $K^{\prime}\subseteq K$, the greatest lower bound
$\inf(K^{\prime})$ of $K^{\prime}$ is well defined (i.e., there exists a
unique $z\in K$ such that $z\sqsubseteq x$ for every $x\in K^{\prime}$ and
every $z^{\prime}$ such that $z^{\prime}\sqsubseteq x$ for every $x\in
K^{\prime}$ is such that $z^{\prime}\sqsubseteq z$), $\Sigma$ be a Datalog
program, and $(D,\mathbb{K},\lambda)$ be an annotated database. We define
_$\mathbb{K}$ -annotated interpretations_ as pairs $(I,\mu^{I})$ where $I$ is
a set of facts, and $\mu^{I}$ is a function from $I$ to $K$. We say that a
$\mathbb{K}$-annotated interpretation $(I,\mu^{I})$ is a _model_ of $\Sigma$
and $(D,\mathbb{K},\lambda)$, denoted by
$(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)$, if

  1. 1.

$D\subseteq I$, and for every $\alpha\in D$,
$\lambda(\alpha)\sqsubseteq\mu^{I}(\alpha)$;

  2. 2.

for every $\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ in $\Sigma$, whenever
there is a homomorphism $h:\phi(\vec{x},\vec{y})\mapsto I$, then
$h(H(\vec{x}))\in I$ and
$\displaystyle\sum_{h^{\prime}:\phi(\vec{x},\vec{y})\mapsto
I,h^{\prime}(\vec{x})=h(\vec{x})}\prod_{\beta\in
h^{\prime}(\phi(\vec{x},\vec{y}))}\mu^{I}(\beta)\sqsubseteq\mu^{I}(h(H(\vec{x})))$.

The _annotated model-based provenance semantics_ $\mathcal{P}^{\texttt{AM}}$
is defined by

$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\inf(\\{\mu^{I}(\alpha){\mid}(I,\mu^{I}){\models}(\Sigma,D,\mathbb{K},\lambda)\\}).$

######  Proposition 1.

If the Datalog rules in $\Sigma$ are (1) s-t tgds, or (2) formulated in DL-
LiteR, then for every BCQ $q$,
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
is equal to the multiplicity of the empty tuple in (1) the incognizant certain
answers or (2) the bag certain answers to $q$ w.r.t. $\Sigma$ and
$(D,\mathbb{N},\lambda_{\mathbb{N}})$.

#### Set-Annotated Model-based

We adapt the work on provenance for the description logics DL-LiteR and
$\mathcal{ELH}^{r}$ (?; ?), where the semiring is assumed to be a
$\times$-idempotent provenance semiring $\mathit{Prov}(X)$ and rules are also
annotated. Annotated models of annotated knowledge bases are defined as set of
facts annotated with sets of monomials from $\mathit{Prov}(X)$. Given a fact
$\alpha$ and a monomial $m$ over $X$,
$(\Sigma,D,\mathit{Prov}(X),\lambda_{X})\models(\alpha,m)$ holds when $m$
belongs to the annotation set of $\alpha$ in every models of $\Sigma$ and
$(D,\mathit{Prov}(X),\lambda_{X})$.

To obtain an analog provenance semantics for Datalog, we define
interpretations which associate facts with (possibly infinite) _sets of
annotations_ , and formulate the requirements for them to be models of
$\Sigma$ and $(D,\mathbb{K},\lambda)$.

Let $\mathbb{K}=(K,+,\times,0,1)$ be a commutative $\omega$-continuous
semiring, $\Sigma$ be a Datalog program, and $(D,\mathbb{K},\lambda)$ be an
annotated database. We define _$\mathbb{K}$ -set-annotated interpretations_ as
pairs $(I,\mu^{I})$ where $I$ is a set of facts, and $\mu^{I}$ is a function
from $I$ to the _power-set of $K$_. We say that a $\mathbb{K}$-set-annotated
interpretation $(I,\mu^{I})$ is a model of $\Sigma$ and
$(D,\mathbb{K},\lambda)$, denoted by
$(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)$, if

  1. 1.

$D\subseteq I$, and for every $\alpha\in D$,
$\lambda(\alpha)\in\mu^{I}(\alpha)$;

  2. 2.

for every $\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ in $\Sigma$, whenever
there is a homomorphism $h:\phi(\vec{x},\vec{y})\mapsto I$, then
$h(H(\vec{x}))\in I$ and if
$h(\phi(\vec{x},\vec{y}))=\beta_{1}\wedge\dots\wedge\beta_{n}$,
$\\{\Pi_{i=1}^{n}k_{i}\mid(k_{1},\dots,k_{n})\in\mu^{I}(\beta_{1})\times\dots\times\mu^{I}(\beta_{n})\\}\subseteq\mu^{I}(h(H(\vec{x})))$.

The _set-annotated model-based provenance semantics_
$\mathcal{P}^{\texttt{SAM}}$ is defined by

$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\sum_{k\in\bigcap_{(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)}\mu^{I}(\alpha)}k.$

#### Connections between semantics

Let $\sqsubseteq$ be the binary relation between provenance semantics such
that $\mathcal{P}\sqsubseteq\mathcal{P}^{\prime}$ if and only if
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)\sqsubseteq\mathcal{P}^{\prime}(\Sigma,D,\mathbb{K},\lambda,\alpha)$
for every $\Sigma$, $(D,\mathbb{K},\lambda)$ and $\alpha$ on which
$\mathcal{P}$ and $\mathcal{P}^{\prime}$ are well-defined.

######  Proposition 2.

The following holds:

$\mathcal{P}^{\texttt{AM}}\sqsubseteq\mathcal{P}^{\texttt{AT}}\text{ and
}\mathcal{P}^{\texttt{SAM}}\sqsubseteq\mathcal{P}^{\texttt{AT}}.$

Next examples show that $\mathcal{P}^{\texttt{AM}}$ and
$\mathcal{P}^{\texttt{SAM}}$ are incomparable.

######  Example 6.

Let $\Sigma=\\{A(x)\rightarrow\mathsf{goal},B(x)\rightarrow\mathsf{goal}\\}$,
$D=\\{A(a),B(a)\\}$, $\lambda_{\mathbb{N}}(A(a))=2$ and
$\lambda_{\mathbb{N}}(B(a))=3$.

Annotated models of $\Sigma$ and $(D,\mathbb{N},\lambda_{\mathbb{N}})$ are
such that $\mu^{I}(\mathsf{goal})\geq 3$, so
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})=3$.

Set-annotated models of $\Sigma$ and $(D,\mathbb{N},\lambda_{\mathbb{N}})$ are
such that $\\{2,3\\}\subseteq\mu^{I}(\mathsf{goal})$, so
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})=5$.

Hence
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal}){<}\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$.

######  Example 7.

Let $\Sigma=\\{R(x,y)\rightarrow\mathsf{goal}\\}$, $D=\\{R(a,b),R(a,c)\\}$,
$\lambda_{\mathbb{N}}(R(a,b))=2$ and $\lambda_{\mathbb{N}}(R(a,c))=2$.

Annotated models of $\Sigma$ and $(D,\mathbb{N},\lambda_{\mathbb{N}})$ are
such that $\mu^{I}(\mathsf{goal})\geq 4$, so
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})=4$.

Set-annotated models of $\Sigma$ and $(D,\mathbb{N},\lambda_{\mathbb{N}})$ are
such that $\\{2\\}\subseteq\mu^{I}(\mathsf{goal})$, so
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})=2$.

Hence
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal}){>}\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$.

Despite of their inherently different approaches, $\mathcal{P}^{\texttt{AM}}$,
$\mathcal{P}^{\texttt{SAM}}$ and $\mathcal{P}^{\texttt{AT}}$ coincide on a
large class of semirings.

######  Proposition 3.

If $\mathbb{K}$ is a commutative $+\,$-idempotent $\omega$-continuous
semiring, then for every $\Sigma$, $(D,\mathbb{K},\lambda)$, and $\alpha$,
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha).$

Additional insights on the connection between definitions can be gained by
considering the provenance semiring $\mathbb{N}^{\infty}\llbracket
X\rrbracket$: the monomials with non-zero coefficients are the same with all
semantics but their coefficients may differ ($\mathcal{P}^{\texttt{AT}}$
leading to the highest coefficients by Proposition 2).

######  Proposition 4.

Let $\lambda_{X}$ be an injective function from $D$ to $X$.

  * •

A monomial occurs in
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$ if and only if it occurs in
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$.

  * •

$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$ is obtained by setting all non-zero
coefficients to $1$ in
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$.

An example where $\mathcal{P}^{\texttt{AT}}$ and $\mathcal{P}^{\texttt{AM}}$
or $\mathcal{P}^{\texttt{SAM}}$ differ on $\mathbb{N}^{\infty}\llbracket
X\rrbracket$ is the following: Let $\Sigma$ contain $A(x)\rightarrow B(x)$,
$B(x)\rightarrow A(x)$, $D=\\{A(a)\\}$ and $\lambda_{X}(A(a))=x$. Since there
are infinitely many derivation trees for $A(a)$,
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda_{X},A(a))=\infty x$
while for
$\mathcal{P}\in\\{\mathcal{P}^{\texttt{AM}},\mathcal{P}^{\texttt{SAM}}\\}$,
$\mathcal{P}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},A(a))=x$, as $\\{A(a),B(a)\\}$ with both facts
annotated with $x$ (resp. $\\{x\\}$) is a (resp. set-)annotated model for
$\Sigma$ and $(D,\mathbb{N}^{\infty}\llbracket X\rrbracket,\lambda_{X})$.

Note that $\mathcal{P}^{\texttt{AM}}$ and $\mathcal{P}^{\texttt{SAM}}$ can
still lead to infinite provenance expressions: Let $\Sigma=\\{A(x)\wedge
B(x)\rightarrow A(x)\\}$, $D=\\{A(a),B(a)\\}$, $\lambda_{X}(A(a))=x$ and
$\lambda_{X}(B(a))=y$. For
$\mathcal{P}\in\\{\mathcal{P}^{\texttt{AM}},\mathcal{P}^{\texttt{SAM}}\\}$,
$\mathcal{P}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},A(a))=x+xy+xy^{2}+xy^{3}+\dots$.

###  3.2 Execution- and Tree-Based Semantics

We saw that when annotations are present there is more than one way to define
a model-based semantics for Datalog and that it differs from the all-tree
semantics. We now investigate definitions based on classical Datalog
evaluation algorithms.

We extend the notion of _immediate consequence operator_ describing the
application of rules onto facts, with the computation of annotation. To this
end, we introduce the _annotation aware immediate consequence operator_
$T_{\Sigma}$. Applying $T_{\Sigma}$ on a set of annotated facts
$(I,\mathbb{K},\lambda)$ results in
$(I_{T_{\Sigma}},\mathbb{K},\lambda_{T_{\Sigma}})$ where $I_{T_{\Sigma}}$ is
the result of applying the immediate consequence operator to $\Sigma$ and $I$,
and $\lambda_{T_{\Sigma}}$ annotates facts in $I_{T_{\Sigma}}$ with the
relational provenance (over $(I,\mathbb{K},\lambda)$) of the UCQ formed by the
bodies of the rules that create them. Formally,

$\displaystyle{I_{T_{\Sigma}}}:=\\{H(\vec{a})\mid
I\models\exists\vec{y}\,\phi(\vec{a},\vec{y})\,,\,\phi(\vec{x},\vec{y})\rightarrow
H(\vec{x})\in\Sigma\\}$
$\displaystyle\lambda_{T_{\Sigma}}(H(\vec{a})):=\sum_{\begin{subarray}{c}h(\vec{x})=\vec{a},\,I\models
h(\phi(\vec{x},\vec{y}))\\\ \phi(\vec{x},\vec{y})\rightarrow
H(\vec{x})\in\Sigma\end{subarray}}\,\,\prod_{\beta\in
h(\phi(\vec{x},\vec{y}))}\lambda(\beta)$

We define a union operator for annotated databases (over the same semiring):
$(I,\mathbb{K},\lambda)\cup(I^{\prime},\mathbb{K},\lambda^{\prime}):=(I\cup
I^{\prime},\mathbb{K},\lambda^{\prime\prime})$ where
$\lambda^{\prime\prime}(\alpha):=\lambda(\alpha)+\lambda^{\prime}(\alpha)$
where we slightly abuse notation by setting $\lambda(\alpha)=0$ if
$\alpha\notin I$, and $\lambda^{\prime}(\alpha)=0$ if $\alpha\notin
I^{\prime}$.

#### Naive Evaluation / All Trees

In the naive evaluation algorithm, all rules are applied in parallel until a
fixpoint is reached. The ‘annotation aware’ version of it is as follows: We
set $I_{\mathsf{n}}^{0}(\Sigma,D,\mathbb{K},\lambda):=(D,\mathbb{K},\lambda)$,
and define inductively
$I_{\mathsf{n}}^{i+1}(\Sigma,D,\mathbb{K},\lambda):=T_{\Sigma}(I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda))\cup(D,\mathbb{K},\lambda)$.
Note that the subscript $\mathsf{n}$ of $I_{\mathsf{n}}$ is an abbreviation
for ‘naive’, and the superscript $i$ indicates how many times $T_{\Sigma}$ was
applied.

Let $(I_{\mathsf{n}}^{i},\mathbb{K},\lambda_{\mathsf{n}}^{i})$ denote
$I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda)$. We say that
$I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda)$ _converges_ if there is some
$k$ such that $I_{\mathsf{n}}^{\ell}=I_{\mathsf{n}}^{k}$ for every $\ell\geq
k$, and $\sup(\lambda_{\mathsf{n}}^{i}(\alpha))$ exists for every $\alpha\in
I_{\mathsf{n}}^{k}$.

######  Proposition 5.

For every $\Sigma,D,\mathbb{K},\lambda$, if $\mathbb{K}$ is
$\omega$-continuous then $I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda)$
converges.

In this case, we define $I_{\mathsf{n}}^{\infty}:=I_{\mathsf{n}}^{k}$ and
$\lambda_{\mathsf{n}}^{\infty}:=\sup_{i\rightarrow\infty}\lambda_{\mathsf{n}}^{i}$.
The _naive execution provenance semantics_ $\mathcal{P}^{\texttt{NE}}$ is
defined by

$\mathcal{P}^{\texttt{NE}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\left\\{\begin{matrix}\lambda_{\mathsf{n}}^{\infty}(\alpha)&\alpha\in
I_{\mathsf{n}}^{\infty}\\\ 0&\text{otherwise}\end{matrix}\right.$

and is equivalent to the all-tree semantics.

######  Proposition 6.

It holds that $\mathcal{P}^{\texttt{NE}}=\mathcal{P}^{\texttt{AT}}$.

#### Optimized Naive Evaluation / Minimal Depth Trees

We consider an optimized version of the naive algorithm that stops as soon as
the desired fact is derived. We define the ‘annotation aware’ version of this
algorithm by
$I_{\mathsf{o,\alpha}}^{0}(\Sigma,D,\mathbb{K},\lambda):=(D,\mathbb{K},\lambda)$,
and

$I_{\mathsf{o,\alpha}}^{i+1}(\Sigma,D,\mathbb{K},\lambda):=\\\
\left\\{\begin{matrix}T_{\Sigma}(I_{\mathsf{o,\alpha}}^{i}(\Sigma,D,\mathbb{K},\lambda))\cup(D,\mathbb{K},\lambda)&\alpha\notin
I_{\mathsf{o,\alpha}}^{i}\\\
I_{\mathsf{o,\alpha}}^{i}(\Sigma,D,\mathbb{K},\lambda)&\text{otherwise}\end{matrix}\right.$

where $I_{\mathsf{o,\alpha}}^{i}$ is such that
$I_{\mathsf{o,\alpha}}^{i}(\Sigma,D,\mathbb{K},\lambda):=(I_{\mathsf{o,\alpha}}^{i},\mathbb{K},\lambda_{\mathsf{o,\alpha}}^{i})$.

######  Proposition 7.

For every $\Sigma,D,\mathbb{K},\lambda$, and $\alpha$ such that
$\Sigma,D\models\alpha$ , there exists $k\geq 0$ such that
$I_{\mathsf{o,\alpha}}^{k}(\Sigma,D,\mathbb{K},\lambda)=I_{\mathsf{o,\alpha}}^{\ell}(\Sigma,D,\mathbb{K},\lambda)$
for every $\ell\geq k$.

With $k$ as provided by Proposition 7, we define the _optimized execution
provenance semantics_ $\mathcal{P}^{\texttt{OE}}$ by:

$\mathcal{P}^{\texttt{OE}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\left\\{\begin{matrix}\lambda_{\mathsf{o,\alpha}}^{k}(\alpha)&\alpha\in
I_{\mathsf{o,\alpha}}^{k}\\\ 0&\text{otherwise}\end{matrix}\right.$

We show that an equivalent tree-based semantics can be obtained by considering
only minimal depth trees for the desired fact. This approach has been
considered useful, for example to present a ‘small proof’ for debugging (?).
Formally, let $\texttt{depth}(t)$ denote the depth of tree $t$. We say that
$t\in T^{\Sigma}_{D}(\alpha)$ is _of minimal depth_ if for every
$t^{\prime}\in T^{\Sigma}_{D}(\alpha)$ it holds that
$\texttt{depth}(t)\leq\texttt{depth}(t^{\prime})$. The _minimal depth tree
provenance semantics_ $\mathcal{P}^{\texttt{MDT}}$ is defined by

$\mathcal{P}^{\texttt{MDT}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of minimal
depth}\end{subarray}}\Lambda(t)$

and is equivalent to the optimized naive execution.

######  Proposition 8.

It holds that $\mathcal{P}^{\texttt{OE}}=\mathcal{P}^{\texttt{MDT}}.$

#### Seminaive Evaluation / Hereditary Minimal Depth Trees

In the seminaive evaluation algorithm, facts are derived only once. We
introduce a new consequence operator $\Delta_{\Sigma}$ that derives only new
facts and is defined as follows:
$\Delta_{\Sigma}(I,\mathbb{K},\lambda):=(I_{\Delta_{\Sigma}},\mathbb{K},\lambda_{\Delta_{\Sigma}})$
where
$T_{\Sigma}(I,\mathbb{K},\lambda):=(I_{T_{\Sigma}},\mathbb{K},\lambda_{T_{\Sigma}})$,
$I_{\Delta_{\Sigma}}:=I_{T_{\Sigma}}\setminus I$, and
$\lambda_{\Delta_{\Sigma}}$ is the restriction of $\lambda_{T_{\Sigma}}$ to
$I_{\Delta_{\Sigma}}$. We can now define the annotation aware version of the
seminaive evaluation:
$I_{\mathsf{sn}}^{0}(\Sigma,D,\mathbb{K},\lambda):=(D,\mathbb{K},\lambda)$ and
$I_{\mathsf{sn}}^{i+1}(\Sigma,D,\mathbb{K},\lambda):=I_{\mathsf{sn}}^{i}(\Sigma,D,\mathbb{K},\lambda)\cup\Delta_{\Sigma}(I_{\mathsf{sn}}^{i}(\Sigma,D,\mathbb{K},\lambda))$.

######  Proposition 9.

For every $\Sigma,D,\mathbb{K},\lambda$, there exists $k\geq 0$ such that
$I_{\mathsf{sn}}^{k}(\Sigma,D,\mathbb{K},\lambda)=I_{\mathsf{sn}}^{\ell}(\Sigma,D,\mathbb{K},\lambda)$
for every $\ell\geq k$.

Note that, unlike in Proposition 5, we do not require $\mathbb{K}$ to be
$\omega$-continuous. With $k$ provided by Proposition 9, the _seminaive
execution provenance semantics_ $\mathcal{P}^{\texttt{SNE}}$ is defined by

$\mathcal{P}^{\texttt{SNE}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\left\\{\begin{matrix}\lambda_{\mathsf{sn}}^{k}&\alpha\in
I_{\mathsf{sn}}^{k}\\\ 0&\text{otherwise}\end{matrix}\right.$

To capture this with the tree-based approach we need to further restrict all
subtrees to be of minimal depth. Formally, a derivation tree $t\in
T^{\Sigma}_{D}(\alpha)$ is a _hereditary minimal-depth (derivation) tree_ if
for every node $n$ of $t$ labeled by $(\beta,r,h)$, the subtree $t_{\beta}$
with root $n$ is a minimal-depth derivation tree for $\beta$. The _hereditary
minimal depth tree provenance semantics_ $\mathcal{P}^{\texttt{HMDT}}$ is
defined by

$\mathcal{P}^{\texttt{HMDT}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is hereditary minimal-
depth}\end{subarray}}\Lambda(t)$

and is equivalent to the seminaive execution.

######  Proposition 10.

It holds that $\mathcal{P}^{\texttt{SNE}}=\mathcal{P}^{\texttt{HMDT}}.$

###  3.3 Non-Recursive Tree-Based Semantics

Both execution-based semantics $\mathcal{P}^{\texttt{OE}}$ and
$\mathcal{P}^{\texttt{SNE}}$ take into account finite subsets of derivation
trees (and hence converge). Is there a more informative tree-based semantics
(i.e., one that takes into account a bigger subset of derivation trees) that
still converges? We present such a semantics based on the intuition that
deriving a fact from itself is redundant.

Formally, a _non-recursive (derivation) tree_ is a derivation tree that does
not contain two nodes labeled with the same fact and such that one is the
descendant of the other. The _non-recursive tree provenance semantics_
$\mathcal{P}^{\texttt{NRT}}$ is defined by

$\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,\alpha):=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is non-recursive}\end{subarray}}\Lambda(t).$

#### Connections between semantics

Next proposition follows from the fact that hereditary minimal-depth trees are
of minimal-depth and non recursive. The sets of minimal depth trees and non-
recursive trees are incomparable, so that
$\mathcal{P}^{\texttt{NRT}}\not\sqsubseteq\mathcal{P}^{\texttt{MDT}}$ and
$\mathcal{P}^{\texttt{MDT}}\not\sqsubseteq\mathcal{P}^{\texttt{NRT}}$.

######  Proposition 11.

The following hold:

$\mathcal{P}^{\texttt{HMDT}}\sqsubseteq\mathcal{P}^{\texttt{NRT}}\sqsubseteq\mathcal{P}^{\texttt{AT}}\
\text{ and
}\quad\mathcal{P}^{\texttt{HMDT}}\sqsubseteq\mathcal{P}^{\texttt{MDT}}\sqsubseteq\mathcal{P}^{\texttt{AT}}$

Moreover $\mathcal{P}^{\texttt{NRT}}$ and $\mathcal{P}^{\texttt{AT}}$ coincide
on specific semirings.

######  Proposition 12.

For every $\Sigma,D,\mathbb{K},\lambda$ and $\alpha$, if $\mathbb{K}$ is a
commutative absorptive $\omega$-continuous semiring, then
$\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.

If $\mathbb{K}$ is not absorptive, there exists $\Sigma$,
$(D,\mathbb{K},\lambda)$ and $\alpha$ such that
$\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)\neq\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$,
even in the case where $\mathbb{K}$ is $+\,$-idempotent and
$\times$-idempotent: Let $\Sigma$ consist of the rule $A(x)\wedge
B(x)\rightarrow A(x)$ and $D=\\{A(a),B(a)\\}$. Then
$\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,A(a))=\lambda(A(a))$
while
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,A(a))=\lambda(A(a))+\lambda(A(a))\times\lambda(B(a))$.

The other semantics differ even under strong restrictions.

######  Example 8.

This example shows that $\mathcal{P}^{\texttt{NRT}}$,
$\mathcal{P}^{\texttt{MDT}}$ and $\mathcal{P}^{\texttt{HMDT}}$ differ even if
$\mathbb{K}$ is $+$ and $\times$-idempotent and absorptive.

$\displaystyle\text{Let }\Sigma=$ $\displaystyle\\{B(x)\wedge C(x)\rightarrow
A(x),\ D(x)\rightarrow B(x),$ $\displaystyle E(x)\rightarrow C(x),\
F(x)\rightarrow E(x)\\}$ $\displaystyle D=$ $\displaystyle\\{C(a),\ D(a),\
E(a),\ F(a)\\}$

The three derivation trees of $A(a)$ w.r.t. $\Sigma$ and $D$ are non-
recursive, but only the first two are of minimal depth and only the first one
is a hereditary minimal-depth tree.

$A(a)$$B(a)$$D(a)$$C(a)$$A(a)$$B(a)$$D(a)$$C(a)$$E(a)$$A(a)$$B(a)$$D(a)$$C(a)$$E(a)$$F(a)$

Thus, if $(D,\mathbb{K},\lambda)$ is such that $\lambda(C(a))=c$,
$\lambda(D(a))=d$, $\lambda(E(a))=e$, and $\lambda(F(a))=f$ then

$\displaystyle\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,A(a))=$
$\displaystyle c\times d+d\times e+d\times f$
$\displaystyle\mathcal{P}^{\texttt{MDT}}(\Sigma,D,\mathbb{K},\lambda,A(a))=$
$\displaystyle c\times d+d\times e$
$\displaystyle\mathcal{P}^{\texttt{HMDT}}(\Sigma,D,\mathbb{K},\lambda,A(a))=$
$\displaystyle c\times d$

##  4 Basics Properties

In this section, we provide a framework allowing to compare the provenance
semantics presented in the previous section. It is clear that they all fulfill
the following definition.

######  Definition 3 (Provenance semantics).

A _provenance semantics_ is a partial function that assigns to a Datalog
program $\Sigma$, annotated database $(D,\mathbb{K},\lambda)$ and fact
$\alpha$, an element $\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)$ in $K$
such that:

  1. 1.

$\Sigma,D\not\models\alpha$ implies
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0_{\mathbb{K}}$.

  2. 2.

If $\mathbb{K}$ is positive,
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0_{\mathbb{K}}$ implies
$\Sigma,D\not\models\alpha$.

We call the _semiring domain_ of $\mathcal{P}$ the maximal set $S$ of
semirings such that $\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)$ is
defined for every $\mathbb{K}\in S$, and every $\Sigma$,
$(D,\mathbb{K},\lambda)$ and $\alpha$.

Intuitively, Definition 3 means that the semantics reflects fact
(non)-entailment. It is extremely permissive: We could define such a semantics
that associates to each entailed fact a random semiring element different from
zero, and does not bring any information beyond facts entailment. In the
sequel, we state and discuss a number of properties that may be expected to be
satisfied by a provenance semantics.

Throughout this section, when not stated otherwise, $\mathcal{P}$, $\Sigma$,
$D$, $\mathbb{K}$, $\lambda$ and $\alpha$ denote respectively an arbitrary
provenance semantics, Datalog program, database, commutative semiring
$(K,+,\times,0,1)$, function from $D$ to $K\setminus\\{0\\}$, and fact. We
phrase properties as conditions, and say that $\mathcal{P}$ _satisfies_ a
property if it satisfies the condition. We also denote by $\lambda_{X}$ an
injective function $\lambda_{X}:D\mapsto X$.

###  4.1 Compatibility with Classical Notions

Property 1 is a sanity check: if a Datalog program amounts to a UCQ, the
provenance should be the same as the one defined for relational databases (?).
A Datalog program $\Sigma$ is _UCQ-defined_ if its rules are of the form
$\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ where $H$ is a predicate that
does not occur in the body of any rule. In this case, the equivalent UCQ
$Q^{\Sigma}$ of $\Sigma$ is $\bigcup_{\phi(\vec{x},\vec{y})\rightarrow
H(\vec{x})\in\Sigma}\exists\vec{y}\phi(\vec{x},\vec{y})$.

######  Property 1 (Algebra Consistency).

If $\Sigma$ is UCQ-defined with rule head $H(\vec{x})$ and
$H\notin\mathcal{S}(D)$, then for every tuple $\vec{a}$ of same arity as
$\vec{x}$, the relational provenance of $Q^{\Sigma}(\vec{a})$ is equal to
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,H(\vec{a}))$.

While Property 1 considers the behavior of a provenance semantics on a
restricted class of queries, we can alternatively consider its behavior on a
specific semiring. Boolean provenance has a very natural definition, based on
the database subsets that entail the query, and is widely used, notably for
probabilistic databases (?), but also for ontology-mediated query explanation
(e.g., in Datalog+/- or description logics (?; ?)). It is formalized with the
semiring $\mathit{PosBool}(X)$.

######  Property 2 (Boolean Compatibility).

$\mathcal{P}(\Sigma,D,\mathit{PosBool}(X),\lambda_{X},\alpha)=\bigvee_{\begin{subarray}{c}D^{\prime}\subseteq
D\\\ \Sigma,D^{\prime}\models\alpha\end{subarray}}\bigwedge_{\beta\in
D^{\prime}}\lambda_{X}(\beta)$

Property 2 expresses ‘insensibility’ to syntax, that is, every provenance
semantics that satisfies Property 2 agrees on equivalent programs (i.e., those
that have the same models) for the semiring $\mathit{PosBool}(X)$. This is
related to ideas from (?) on the provenance of equivalent UCQs.

###  4.2 Compatibility with Specialization

Semiring provenance has been introduced to abstract from the particular
semiring at hand, and factor the computations in some provenance semiring
which specializes correctly to any semiring of interest. The next property
allows one to do so (Appendix B.1), and is thus highly desirable.

######  Property 3 (Commutation with Homomorphisms).

If there is a semiring homomorphism $h$ from $\mathbb{K}_{1}$ to
$\mathbb{K}_{2}$, then
$h(\mathcal{P}(\Sigma,D,\mathbb{K}_{1},\lambda,\alpha))=\mathcal{P}(\Sigma,D,\mathbb{K}_{2},h\circ\lambda,\alpha)$.

We call Property 3 restricted to $\omega$-continuous homomorphisms
_Commutation with $\omega$-Continuous Homomorphisms_.

Specializing correctly is all the more useful when $\mathcal{P}$ is well-
defined for a lot of semirings, in particular on all commutative or at least
all commutative $\omega$-continuous semirings.

######  Property 4 (Any ($\omega$-Continuous) Semiring).

$\mathcal{P}$ satisfies the _Any Semiring Property_ (resp. _Any
$\omega$-Continuous Semiring Property_) if the semiring domain of
$\mathcal{P}$ contains the set of all commutative (resp. commutative
$\omega$-continuous) semirings.

###  4.3 Joint and Alternative Use of the Data

How is the actual usage of the data reflected in the provenance semantics? The
next property formalizes that multiplication reflects joint use of the data,
and addition alternative use. For the rest of this section, we set
$\mathsf{goal}$ to be a nullary predicate not in
$\mathcal{S}(\Sigma)\cup\mathcal{S}(D)$.

######  Property 5 (Joint and Alternative Use).

For all tuples of facts $(\alpha^{1}_{1},\cdots,\alpha^{1}_{n_{1}})$, $\dots$,
$(\alpha^{m}_{1},\cdots,\alpha^{m}_{n_{m}})$, it holds that

$\mathcal{P}(\Sigma^{\prime},D,\mathbb{K},\lambda,\mathsf{goal})=\Sigma_{i=1}^{m}\Pi_{j=1}^{n_{i}}\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha^{i}_{j})$

where
$\Sigma^{\prime}=\Sigma\cup\\{\bigwedge_{j=1}^{n_{i}}\alpha^{i}_{j}\rightarrow\mathsf{goal}\mid
1\leq i\leq m\\}$.

We weaken the above by referring to each mode separately:

######  Property 6 (Joint Use).

For all facts $\alpha_{1},\cdots,\alpha_{n}$,

$\mathcal{P}(\Sigma^{\prime},D,\mathbb{K},\lambda,\mathsf{goal})=\Pi_{j=1}^{n}\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha_{j})$

where
$\Sigma^{\prime}=\Sigma\cup\\{\bigwedge_{j=1}^{n}\alpha_{j}\rightarrow\mathsf{goal}\\}$.

######  Property 7 (Alternative Use).

For all facts $\alpha_{1},\cdots,\alpha_{m}$,

$\mathcal{P}(\Sigma^{\prime},D,\mathbb{K},\lambda,\mathsf{goal})=\Sigma_{i=1}^{m}\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha_{i})$

where $\Sigma^{\prime}=\Sigma\cup\\{\alpha_{i}\rightarrow\mathsf{goal}\mid
1\leq i\leq m\\}$.

###  4.4 Fact Roles in Entailment.

After considering how facts can be combined or used alternatively to entail a
result, we ponder their possible roles w.r.t. the entailment. Property 8
asserts that the original annotation of a fact takes part in the provenance of
its entailment.

######  Property 8 (Self).

If $\alpha\in D$, then
$\lambda(\alpha)\sqsubseteq\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.

Moreover, if a database fact cannot be alternatively derived using the rules,
then its provenance should be exactly its original annotation. To phrase this
property we use the _grounding_ $\Sigma_{D}$ of $\Sigma$ w.r.t. $D$, defined
by $\Sigma_{D}=\\{h(\phi(\vec{x},\vec{y}))\rightarrow
h(H(\vec{x}))\mid\phi(\vec{x},\vec{y})\rightarrow
H(\vec{x})\in\Sigma,h:\vec{x}\cup\vec{y}\mapsto\mathcal{D}(D)\\}$. It holds
that $\Sigma,D\models\alpha$ if and only if $\Sigma_{D},D\models\alpha$.

######  Property 9 (Parsimony).

If $\alpha\in D$ does not occur in any rule head in $\Sigma_{D}$ then
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\lambda(\alpha)$.

Parsimony Property together with other constraints guarantee Algebra
Consistency Property.

######  Proposition 13.

If $\mathcal{P}$ satisfies Properties 5 (Joint and Alternative Use) and 9
(Parsimony), and is such that for every $\Sigma,D,\mathbb{K},\lambda,\alpha$,
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\mathcal{P}(\Sigma_{D},D,\mathbb{K},\lambda,\alpha)$,
then it satisfies Property 1 (Algebra Consistency).

Property 10 states that $\mathcal{P}$ reflects the necessity of a fact for the
entailment. We say that $\beta\in D$ is _necessary_ to $\Sigma,D\models\alpha$
if $\Sigma,D\setminus\\{\beta\\}\not\models\alpha$, and denote by
$\mathit{Nec}$ the set of such facts.

######  Property 10 (Necessary Facts).

There exists $e\in K$ such that
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\Pi_{\beta\in\mathit{Nec}}\lambda({\beta})\times
e$.

A fact is _usable_ to $\Sigma,D\models\alpha$ if it occurs in some derivation
tree in $T^{\Sigma}_{D}(\alpha)$. Usable facts are related to the notion of
_lineage_ (?) and can be defined without resorting to derivation trees (cf.
Appendix B.3). Intuitively, if a fact is not usable to derive another fact, it
should not have any influence on its provenance.

######  Property 11 (Non-Usable Facts).

For every $\lambda^{\prime}$ that differs from $\lambda$ only on facts that
are not usable to $\Sigma,D\models\alpha$, it holds that
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\mathcal{P}(\Sigma,D,\mathbb{K},\lambda^{\prime},\alpha)$.

###  4.5 Data Modification

The last two properties indicate how provenance is impacted when facts are
inserted or deleted.

######  Property 12 (Insertion).

For every $(D^{\prime},\mathbb{K},\lambda^{\prime})$ such that $D\cap
D^{\prime}=\emptyset$,

$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)+\mathcal{P}(\Sigma,D^{\prime},\mathbb{K},\lambda^{\prime},\alpha)$

Maintaining provenance upon fact deletion is very useful in practice. We
formalize this using a provenance semiring, which allows us to keep track of
the facts. A partial evaluation of a provenance expression $p(X)$ over
variables $X$ is an expression obtained from $p(X)$ by replacing some of the
variables by a given value.

######  Property 13 (Deletion).

For every provenance semiring $\mathit{Prov}(X)$ and $D^{\prime}\subseteq D$,
if $\lambda^{\prime}$ is the restriction of $\lambda_{X}$ to $D^{\prime}$ and
$\Delta=D\setminus D^{\prime}$, then
$\mathcal{P}(\Sigma,D^{\prime},\mathit{Prov}(X),\lambda^{\prime},\alpha)$ is
equal to the partial evaluation of
$\mathcal{P}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\alpha)$ obtained by
setting the annotations of facts in $\Delta$ to $0$:
$\mathcal{P}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\alpha)[\\{\lambda_{X}(x)=0\\}_{x\in\Delta}]$.

##  5 Semantics Analysis w.r.t. Properties

In this section, we analyze the semantics proposed in Section 3 w.r.t. the
properties introduced in Section 4. The properties each semantics satisfies
are summarized in Table 1. Proofs of the positive cases are given in
Appendices C and D and we discuss the negative cases, which may be more
characteristic, in the sequel.

| $\mathcal{P}^{\texttt{AT}}$ | $\mathcal{P}^{\texttt{NRT}}$ | $\mathcal{P}^{\texttt{MDT}}$ | $\mathcal{P}^{\texttt{HMDT}}$ | $\mathcal{P}^{\texttt{AM}}$ | $\mathcal{P}^{\texttt{SAM}}$
---|---|---|---|---|---|---
Algebra Consistency | ✓ | ✓ | ✓ | ✓ |  |
Boolean Compat. | ✓ | ✓ |  |  | ✓ | ✓
Com. with Hom. |  | ✓ | ✓ | ✓ |  |
Com. with $\omega$-Cont. | ✓ | ✓ | ✓ | ✓ |  |
Any Semiring |  | ✓ | ✓ | ✓ |  |
Any $\omega$-Cont. Sem. | ✓ | ✓ | ✓ | ✓ |  | ✓
Joint and Alt. Use | ✓ | ✓ |  |  |  |
Joint Use | ✓ | ✓ |  | ✓ | ✓ |
Alternative Use | ✓ | ✓ |  |  |  |
Self | ✓ | ✓ | ✓ | ✓ | ✓ | ✓
Parsimony | ✓ | ✓ | ✓ | ✓ | ✓ | ✓
Necessary Facts | ✓ | ✓ | ✓ | ✓ |  | ✓
Non-Usable Facts | ✓ | ✓ | ✓ | ✓ | ✓ | ✓
Insertion | ✓ | ✓ |  |  |  |
Deletion | ✓ | ✓ |  |  | ✓ | ✓
Table 1:  Does a property hold for a provenance semantics?

###  5.1 Tree- and Execution-Based Semantics Cases

We first discuss $\mathcal{P}^{\texttt{MDT}}$ and
$\mathcal{P}^{\texttt{HMDT}}$, which have not been much investigated and stand
out compared to $\mathcal{P}^{\texttt{AT}}$ and $\mathcal{P}^{\texttt{NRT}}$.
The next example shows that they do not satisfy the Boolean Compatibility,
Joint and Alternative Use, Alternative Use, Insertion and Deletion Properties.

######  Example 9.

Consider $\Sigma$ and $(D,\mathit{Prov}(X),\lambda_{X})$ as follows.

$\displaystyle\Sigma=$ $\displaystyle\\{A(x)\rightarrow\mathsf{goal},\
B(x)\rightarrow\mathsf{goal},\ C(x)\rightarrow B(x)\\}$ $\displaystyle D=$
$\displaystyle\\{A(a),\ C(a)\\}\text{ with }\lambda_{X}(A(a))=a,\
\lambda_{X}(C(a))=c$

It holds that both
$\mathcal{P}^{\texttt{MDT}}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\mathsf{goal})$
and
$\mathcal{P}^{\texttt{HMDT}}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\mathsf{goal})$
are equal to $a$. For
$\mathcal{P}\in\\{\mathcal{P}^{\texttt{MDT}},\mathcal{P}^{\texttt{HMDT}}\\}$
we then have the following:

$(i)$ The Boolean provenance of $\mathsf{goal}$ is $a\vee c$, hence
$\mathcal{P}$ does not satisfy the Boolean Compatibility Property.

$(ii)$ Since $\mathcal{P}(\emptyset,D,\mathit{Prov}(X),\lambda_{X},A(a))=a$
and $\mathcal{P}(\emptyset,D,\mathit{Prov}(X),\lambda_{X},C(a))=c$,
$\mathcal{P}$ does not satisfy the Alternative Use, nor the Joint and
Alternative Use Property.

$(iii)$ Let $D^{\prime}=\\{\mathsf{goal}\\}$ and
$\lambda^{\prime}(\mathsf{goal})=g$. It holds that $\mathcal{P}(\Sigma,D\cup
D^{\prime},\mathit{Prov}(X),\lambda_{X}\cup\lambda_{X}^{\prime},\mathsf{goal})=g$,
which is different from
$\mathcal{P}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\mathsf{goal})+\mathcal{P}(\Sigma,D^{\prime},\mathit{Prov}(X),\lambda_{X}^{\prime},\mathsf{goal})+e$
for every $e\in\mathit{Prov}(X)$. Hence $\mathcal{P}$ does not satisfy the
Insertion Property.

$(iv)$ Let $D^{\prime}=D\setminus\\{A(a)\\}=\\{C(a)\\}$. The partial
evaluation of
$\mathcal{P}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\mathsf{goal})$ where $a$
is set to $0$ is equal to $0$ while
$\mathcal{P}(\Sigma,D^{\prime},\mathit{Prov}(X),\lambda_{X},\mathsf{goal})=c$.
Hence $\mathcal{P}$ does not satisfy the Deletion Property.

We now illustrate the difference between $\mathcal{P}^{\texttt{HMDT}}$ and
$\mathcal{P}^{\texttt{MDT}}$: $\mathcal{P}^{\texttt{HMDT}}$ satisfies the
Joint Use Property while $\mathcal{P}^{\texttt{MDT}}$ does not.

######  Example 10.

Let $\Sigma=\\{C(x)\rightarrow B(x),\ D(x)\rightarrow A(x)\\}$,
$D=\\{B(a),C(a),D(a)\\}$ and $\lambda(B(a))=b$, $\lambda(C(a))=c$,
$\lambda(D(a))=d$, and consider $\Sigma^{\prime}=\Sigma\cup\\{A(a)\wedge
B(a)\rightarrow\mathsf{goal}\\}$.
$\mathcal{P}^{\texttt{MDT}}(\Sigma^{\prime},D,\mathbb{K},\lambda,\mathsf{goal})=b\times
d+c\times d$ while
$\mathcal{P}^{\texttt{MDT}}(\Sigma,D,\mathbb{K},\lambda,A(a))=d$ and
$\mathcal{P}^{\texttt{MDT}}(\Sigma,D,\mathbb{K},\lambda,B(a))=b$. Hence
$\mathcal{P}^{\texttt{MDT}}$ does not satisfy the Joint Use Property.

We conclude this discussion with the remark that $\mathcal{P}^{\texttt{AT}}$
satisfies the Commutation with $\omega$-Continuous Homomorphisms but not the
Commutation with Homomorphisms Property.

######  Example 11.

Consider the semiring $\mathbb{N}^{\infty}$ with the classical operations, and
define $\mathbb{N}^{\infty,\infty^{\prime}}$ as its extension by an element
$\infty^{\prime}$ such that for every $n\in\mathbb{N}\cup\\{\infty\\}$,
$n+\infty^{\prime}=\infty^{\prime}$, and
$n\times\infty^{\prime}=\infty^{\prime}$ if $n\neq 0$, and $0$ otherwise. Both
semirings are $\omega$-continuous and
$h:\mathbb{N}^{\infty}\mapsto\mathbb{N}^{\infty,\infty^{\prime}}$ defined by
$h(n)=n$ for every $n\in\mathbb{N}$, $h(\infty)=\infty^{\prime}$ is a semiring
homomorphism (which is not $\omega$-continuous). Assume that
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty},\lambda,\mathsf{goal})=\Sigma_{i\in\mathbb{N}}1=\infty$.
Then
$h(\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty},\lambda,\mathsf{goal}))=\infty^{\prime}$
is different from
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty,\infty^{\prime}},h\circ\lambda,\mathsf{goal})=\Sigma_{i\in\mathbb{N}}h(1)=\infty$.

###  5.2 Model-Based Semantics Cases

On $+\,$-idempotent semirings, $\mathcal{P}^{\texttt{AM}}$ and
$\mathcal{P}^{\texttt{SAM}}$ coincide with $\mathcal{P}^{\texttt{AT}}$ so
verify the same properties, and the semiring $\mathbb{B}\llbracket
X\rrbracket$ of formal power series with Boolean coefficients can be used to
compute them in any $+\,$-idempotent semiring (Appendix E.1). However, on non-
idempotent semirings, they do not satisfy several properties, and in
particular the Commutation with ($\omega$-Continuous) Homomorphisms
Properties.

######  Example 12.

Let $\Sigma=\\{A(x)\rightarrow\mathsf{goal},B(x)\rightarrow\mathsf{goal}\\}$
and $D=\\{A(a),B(a)\\}$ and consider the provenance semiring
$\mathbb{N}^{\infty}\llbracket X\rrbracket$ with $\lambda_{X}(A(a))=x$ and
$\lambda_{X}(B(a))=y$.

It holds that both
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\mathsf{goal})$ and
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\mathsf{goal})$ are equal to $x+y$.

Consider now the semiring $\mathbb{N}^{\infty}$,
$\lambda_{\mathbb{N}}(A(a))=2$ and $\lambda_{\mathbb{N}}(B(a))=2$. Both
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})$
and
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})$
are equal to $2$.

For $\mathcal{P}\in\\{\mathcal{P}^{\texttt{AM}},\mathcal{P}^{\texttt{SAM}}\\}$
we then have the following:

$(i)$ Let $h$ be a $\omega$-continuous homomorphism from
$\mathbb{N}^{\infty}\llbracket X\rrbracket$ to $\mathbb{N}^{\infty}$ such that
$h(x)=2$ and $h(y)=2$. Since $h(x+y)=h(x)+h(y)=4$, $\mathcal{P}$ does not
satisfy the Commutation with $\omega$-Continuous Homomorphisms Property.

$(ii)$ The relational provenance of $Q^{\Sigma}()$ w.r.t.
$\mathbb{N}^{\infty}$ and $\lambda_{\mathbb{N}}$ is $4$ so $\mathcal{P}$ does
not satisfy the Algebra Consistency Property.

$(iii)$
$\mathcal{P}(\emptyset,D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},A(a))+\mathcal{P}(\emptyset,D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},B(a))=4$
so $\mathcal{P}$ does not satisfy the Alternative Use nor the Joint and
Alternative Use Property.

$(iv)$ Since
$\mathcal{P}(\Sigma,\\{A(a)\\},\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})+\mathcal{P}(\Sigma,\\{B(a)\\},\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})=4$
is strictly greater than
$\mathcal{P}(\Sigma,D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})$,
$\mathcal{P}$ does not satisfy the Insertion Property.

Moreover, $\mathcal{P}^{\texttt{SAM}}$ does not satisfy the Joint Use
Property.

######  Example 13.

Let

$\displaystyle\Sigma=\\{$ $\displaystyle
A(x)\rightarrow\mathsf{g}_{1},A(x)\rightarrow\mathsf{g}_{2},B(x)\rightarrow\mathsf{g}_{1},B(x)\rightarrow\mathsf{g}_{2}\\}$
$\displaystyle D=\\{$ $\displaystyle A(a),B(a)\\}\text{ with
}\lambda_{X}(A(a))=x,\lambda_{X}(B(a))=y.$

Both $\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\mathsf{g}_{1})$ and
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\mathsf{g}_{2})$ are equal to $x+y$ but
$\mathcal{P}^{\texttt{SAM}}(\Sigma\cup\\{\mathsf{g}_{1}\wedge\mathsf{g}_{2}\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\mathsf{goal})=x^{2}+y^{2}+xy\neq(x+y)^{2}$.

We show that $\mathcal{P}^{\texttt{AM}}$ does not satisfy the Necessary Facts
Property in Appendix D.1 because we needed to craft a specific semiring to get
a counter-example.

##  6 Complexity Considerations and Conclusion

In this paper, we present alternative provenance semantics for Datalog based
on models, execution algorithms and derivation trees, and compare them through
the lens of different properties. $\mathcal{P}^{\texttt{NRT}}$ is the only one
that satisfies all the studied properties but does not coincide with an
execution based semantics contrary to the other tree-based semantics
$\mathcal{P}^{\texttt{AT}}$, $\mathcal{P}^{\texttt{MDT}}$, and
$\mathcal{P}^{\texttt{HMDT}}$. The equivalence between the tree-based
$\mathcal{P}^{\texttt{AT}}$, $\mathcal{P}^{\texttt{NRT}}$ and model-based
$\mathcal{P}^{\texttt{AM}}$ and $\mathcal{P}^{\texttt{SAM}}$ definitions on
absorptive semirings may also indicates a robust provenance on this restricted
setting.

One of the main complexity sources of Datalog provenance stems from its
infinite representation. ? (?) studied semirings for which the provenance
expressions given by $\mathcal{P}^{\texttt{AT}}$ are finite, and showed that
they can be represented by polynomial size circuits. We show (Appendix F) that
the annotations produced at each iteration of our execution algorithms can be
represented by arithmetic circuits of polynomial size in the data.
Consequently, both $\mathcal{P}^{\texttt{MDT}}$ and
$\mathcal{P}^{\texttt{HMDT}}$ can be represented by polynomial size circuits
regardless of the semiring. On the contrary, we show that (assuming
$\mathsf{P}\neq\mathsf{NP}$) there is no polynomially computable circuit that
computes $\mathcal{P}^{\texttt{NRT}}$ on $\mathbb{N}^{\infty}\llbracket
X\rrbracket$, by a reduction from a result by ? (?). Whether it is possible to
polynomially compute circuits for $\mathcal{P}^{\texttt{NRT}}$ on provenance
semirings less expressive than $\mathbb{N}^{\infty}\llbracket X\rrbracket$ but
non-absorptive remains open.

## Acknowledgements

This work is supported by the ANR project CQFD (ANR-18-CE23-0003).

## References

  * 1995 Abiteboul, S.; Hull, R.; and Vianu, V.  1995\.  Foundations of Databases.  Addison-Wesley.
  * 1995 Achs, Á., and Kiss, A.  1995\.  Fuzzy extension of datalog.  Acta Cybern. 12(2):153–166.
  * 2012 Arenas, M.; Conca, S.; and Pérez, J.  2012\.  Counting beyond a yottabyte, or how SPARQL 1.1 property paths will prevent adoption of the standard.  In Mille, A.; Gandon, F.; Misselis, J.; Rabinovich, M.; and Staab, S., eds., Proceedings of the 21st World Wide Web Conference 2012, WWW 2012, Lyon, France, April 16-20, 2012, 629–638.  ACM.
  * 2020 Bourgaux, C.; Ozaki, A.; Peñaloza, R.; and Predoiu, L.  2020\.  Provenance for the description logic elhr.  In Bessiere, C., ed., Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, 1862–1869.  ijcai.org.
  * 2019 Calvanese, D.; Lanti, D.; Ozaki, A.; Peñaloza, R.; and Xiao, G.  2019\.  Enriching ontology-based data access with provenance.  In Kraus, S., ed., Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, 1616–1623.  ijcai.org.
  * 2019 Ceylan, İ. İ.; Lukasiewicz, T.; Malizia, E.; and Vaicenavicius, A.  2019\.  Explanations for query answers under existential rules.  In Kraus, S., ed., Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, 1639–1646.  ijcai.org.
  * 2020 Ceylan, İ. İ.; Lukasiewicz, T.; Malizia, E.; and Vaicenavicius, A.  2020\.  Explanations for ontology-mediated query answering in description logics.  In Giacomo, G. D.; Catalá, A.; Dilkina, B.; Milano, M.; Barro, S.; Bugarín, A.; and Lang, J., eds., ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, volume 325 of Frontiers in Artificial Intelligence and Applications, 672–679.  IOS Press.
  * 2009 Cheney, J.; Chiticariu, L.; and Tan, W. C.  2009\.  Provenance in databases: Why, how, and where.  Found. Trends Databases 1(4):379–474.
  * 2000 Cui, Y.; Widom, J.; and Wiener, J. L.  2000\.  Tracing the lineage of view data in a warehousing environment.  ACM Trans. Database Syst. 25(2):179–227.
  * 2021 Dannert, K. M.; Grädel, E.; Naaf, M.; and Tannen, V.  2021\.  Semiring provenance for fixed-point logic.  In Baier, C., and Goubault-Larrecq, J., eds., 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, 17:1–17:22.  Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
  * 2014 Deutch, D.; Milo, T.; Roy, S.; and Tannen, V.  2014\.  Circuits for datalog provenance.  In Schweikardt, N.; Christophides, V.; and Leroy, V., eds., Proc. 17th International Conference on Database Theory (ICDT), Athens, Greece, March 24-28, 2014, 201–212.  OpenProceedings.org.
  * 2018 Deutch, D.; Gilad, A.; and Moskovitch, Y.  2018\.  Efficient provenance tracking for datalog using top-k queries.  VLDB J. 27(2):245–269.
  * 2011 Esparza, J., and Luttenberger, M.  2011\.  Solving fixed-point equations by derivation tree analysis.  In Corradini, A.; Klin, B.; and Cîrstea, C., eds., Algebra and Coalgebra in Computer Science, 19–35.  Berlin, Heidelberg: Springer Berlin Heidelberg.
  * 2017 Green, T. J., and Tannen, V.  2017\.  The semiring framework for database provenance.  In Sallinger, E.; den Bussche, J. V.; and Geerts, F., eds., Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2017, Chicago, IL, USA, May 14-19, 2017, 93–99.  ACM.
  * 2007 Green, T. J.; Karvounarakis, G.; and Tannen, V.  2007\.  Provenance semirings.  In Libkin, L., ed., Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 11-13, 2007, Beijing, China, 31–40.  ACM.
  * 2009 Green, T. J.  2009\.  Containment of conjunctive queries on annotated relations.  In Fagin, R., ed., Database Theory - ICDT 2009, 12th International Conference, St. Petersburg, Russia, March 23-25, 2009, Proceedings, volume 361 of ACM International Conference Proceeding Series, 296–309.  ACM.
  * 2017 Hernich, A., and Kolaitis, P. G.  2017\.  Foundations of information integration under bag semantics.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, 1–12.  IEEE Computer Society.
  * 1990 Mumick, I. S.; Pirahesh, H.; and Ramakrishnan, R.  1990\.  The magic of duplicates and aggregates.  In McLeod, D.; Sacks-Davis, R.; and Schek, H., eds., 16th International Conference on Very Large Data Bases, August 13-16, 1990, Brisbane, Queensland, Australia, Proceedings, 264–277.  Morgan Kaufmann.
  * 2017 Nikolaou, C.; Kostylev, E. V.; Konstantinidis, G.; Kaminski, M.; Grau, B. C.; and Horrocks, I.  2017\.  The bag semantics of ontology-based data access.  In Sierra, C., ed., Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, 1224–1230.  ijcai.org.
  * 2019 Nikolaou, C.; Kostylev, E. V.; Konstantinidis, G.; Kaminski, M.; Grau, B. C.; and Horrocks, I.  2019\.  Foundations of ontology-based data access under bag semantics.  Artif. Intell. 274:91–132.
  * 2017 Senellart, P.  2017\.  Provenance and probabilities in relational databases.  SIGMOD Rec. 46(4):5–15.
  * 2020 Soufflé.  2020\.  https://souffle-lang.github.io/index.html.
  * 2008 Stüber, T., and Vogler, H.  2008\.  Weighted monadic datalog.  Theoretical Computer Science 403(2):221–238.
  * 2020 Zhao, D.; Subotic, P.; and Scholz, B.  2020\.  Debugging large-scale datalog: A scalable provenance evaluation strategy.  ACM Trans. Program. Lang. Syst. 42(2):7:1–7:35.

[sections] [sections]l1

##  Appendix A Discussion and Proofs for Section 3

###  A.1 Relationships between Provenance Semantics and Different Bag
Semantics

#### Connection between Incognizant and Cognizant Bag Semantics and Provenance
Semantics

To compare the bag semantics defined by ? (?) in the context of information
integration and a provenance semantics $\mathcal{P}$ with counting semiring
$\mathbb{N}$, we consider the case where $\Sigma$ is a set of Datalog rules
(in normalized form with a single atom in the head) which are also s-t tgds,
i.e., such that the predicates used in the rule heads and bodies are disjoint.
For a provenance semantics $\mathcal{P}$, we want to know whether for every
such $\Sigma$, $D$ over the source schema (i.e., predicates that occur in the
Datalog rule bodies),
$\lambda_{\mathbb{N}}:D\mapsto\mathbb{N}\setminus\\{0\\}$ and BCQ $q$ over the
target schema (i.e., predicates that occur in Datalog rule heads),
$\mathcal{P}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
is equal to the multiplicity of the empty tuple in the the incognizant or
cognizant certain answers of $q$ w.r.t. $\Sigma$ and $D$. Note that in this
context, all derivation trees of $\mathsf{goal}$ w.r.t. $D$ and $\Sigma$ are
non-recursive and of depth 2. Hence, all derivation tree-based (and execution-
based) semantics coincide. We show below that they are in line with the
cognizant bag semantics. We have shown in Section 3.1 that this is not the
case for the incognizant semantics, i.e., only the cognizant bag semantics for
information integration agrees with the traditional bag semantics for Datalog.

######  Proposition 14.

For
$\mathcal{P}\in\\{\mathcal{P}^{\texttt{AT}},\mathcal{P}^{\texttt{NRT}},\mathcal{P}^{\texttt{HMDT}},\mathcal{P}^{\texttt{MDT}},\mathcal{P}^{\texttt{NE}},\mathcal{P}^{\texttt{SNE}},\mathcal{P}^{\texttt{OE}}\\}$,
$\Sigma$, $D$, $\lambda_{\mathbb{N}}$, and $q$ as required,
$\mathcal{P}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
is equal to the multiplicity of the empty tuple in the cognizant certain
answers of $q$ w.r.t. $\Sigma$ and $D$.

###### Proof.

We first show that for every fact $\alpha=p(\vec{a})$ over the target schema
such that $\Sigma,D\models\alpha$,
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$ is equal to the
multiplicity $n_{\alpha}$ of the empty tuple in the cognizant certain answers
of the Boolean query $\alpha$ w.r.t. $\Sigma$ and $D$.

  * •

The set of derivation trees for $\alpha$ correspond precisely to the set of
pairs $(r,h)$ such that $r\in\Sigma$ is of the form
$\phi(\vec{x},\vec{y})\rightarrow p(\vec{x})$ and $h$ is an homomorphism from
$\phi(\vec{x},\vec{y})$ to $D$ such that $h(\vec{x})=\vec{a}$. Hence
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$ is equal to the
sum over all s-t tgd $r:=\phi(\vec{x},\vec{y})\rightarrow p(\vec{x})$ in
$\Sigma$ of the multiplicity of $\vec{a}$ in the answer to
$\phi(\vec{x},\vec{y})$ on $D$.

  * •

Let $J$ be a cognizant solution for $D$ w.r.t. $\Sigma$. The multiplicity of
$\alpha$ in $J$ is at least the sum over the rules
$r:=\phi(\vec{x},\vec{y})\rightarrow p(\vec{x})$ in $\Sigma$ of the
multiplicities of $\vec{a}$ in the answers of $\phi(\vec{x},\vec{y})$ on $D$.
Hence the multiplicity of $\alpha$ in $J$ is greater or equal to
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$. Since this is
true for every cognizant solution $J$, it follows that
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)\leq n_{\alpha}$.

  * •

If $J$ is a cognizant solution for $D$ w.r.t. $\Sigma$, then $J^{\prime}$
obtained from $J$ by setting the multiplicity of $\alpha$ to
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$ is also a
cognizant solution. Indeed, for each $r:=\phi(\vec{x},\vec{y})\rightarrow
p(\vec{x})$ in $\Sigma$, $J_{r}=\\{(p(\vec{b}),n_{r,\vec{b}})\mid
h:\phi(\vec{x},\vec{y})\mapsto D,h(\vec{x})=\vec{b},n_{r,\vec{b}}\text{
multiplicity of }\vec{b}\text{ in answers to }\phi(\vec{x},\vec{y})\text{ on
}D\\}$ satisfies $r$, and $\sum_{r:=\phi(\vec{x},\vec{y})\rightarrow
p(\vec{x})\in\Sigma}n_{r,\vec{a}}=\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$.
It follows that
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)\geq n_{\alpha}$.

Hence, the multiplicity $n_{\alpha}$ of the empty tuple in the cognizant
certain answers of the Boolean query $\alpha$ w.r.t. $\Sigma$ and $D$ is equal
to $\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$. We now show
that
$\mathcal{P}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
is equal to the multiplicity $n_{q}$ of the empty tuple in the cognizant
certain answers of $q$ w.r.t. $\Sigma$ and $D$. Let
$q=\exists\vec{x}\bigwedge_{i=1}^{n}p_{i}(\vec{x})$.

  * •

Let $J=\\{\alpha\mid\Sigma,D\models\alpha\\}$. For each homomorphism
$h:\bigwedge_{i=1}^{n}p_{i}(\vec{x})\mapsto J$, the derivation trees for
$\mathsf{goal}$ with root labeled by
$(\mathsf{goal},q\rightarrow\mathsf{goal},h)$ have children
$h(p_{1}(\vec{x}))=\alpha_{1},\dots,h(p_{n}(\vec{x}))=\alpha_{n}\in J$ and
correspond to the choice of $t_{1},\dots,t_{n}$ where each $t_{i}$ is a
derivation tree for $\alpha_{i}$. Hence,

$\displaystyle\mathcal{P}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})=$
$\displaystyle\sum_{h:\bigwedge_{i=1}^{n}p_{i}(\vec{x})\mapsto
J}\sum_{(t_{1},\dots,t_{n})\in T^{\Sigma}_{D}(\alpha_{1})\times\dots\times
T^{\Sigma}_{D}(\alpha_{n})}\Lambda(t_{i})$ $\displaystyle=$
$\displaystyle\sum_{h:\bigwedge_{i=1}^{n}p_{i}(\vec{x})\mapsto
J}\prod_{i=1}^{n}\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha_{i}).$

  * •

Let $J$ be a cognizant solution for $D$ w.r.t. $\Sigma$. The multiplicity of
the empty tuple in the answers of $q$ over $J$ is the sum over the
homomorphisms $h:q\mapsto J$ of the product of the multiplicities of
$\alpha_{i}=h(p_{i}(\vec{x}))$ in $J$. Moreover, every such $\alpha_{i}$ is
such that $\Sigma,D\models\alpha_{i}$ so its multiplicity in $J$ is at least
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha_{i})$. Since this
holds for any cognizant solution $J$, it follows that
$n_{q}\geq\mathcal{P}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$.

  * •

A cognizant solution $J$ for $D$ w.r.t. $\Sigma$ can be obtained by setting
the multiplicity of each fact on the target schema $\alpha$ to
$\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$. It follows
that $n_{q}\leq\sum_{h:\bigwedge_{i=1}^{n}p_{i}(\vec{x})\mapsto
J}\prod_{i=1}^{n}\mathcal{P}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha_{i})=\mathcal{P}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$.

Hence the multiplicity $n_{q}$ of the empty tuple in the cognizant certain
answers of $q$ w.r.t. $\Sigma$ and $D$ is equal to
$\mathcal{P}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$.
∎

We show below that the incognizant semantics coincides with
$\mathcal{P}^{\texttt{AM}}$ with the counting semiring. The examples we gave
in Section 3.1 to show that $\mathcal{P}^{\texttt{AM}}$ and
$\mathcal{P}^{\texttt{SAM}}$ differ show that this is not the case of
$\mathcal{P}^{\texttt{SAM}}$.

######  Proposition 15.

For every $\Sigma$, $D$, $\lambda_{\mathbb{N}}$, and $q$ as required,
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
is equal to the multiplicity of the empty tuple in the incognizant certain
answers of $q$ w.r.t. $\Sigma$ and $D$.

###### Proof.

We first show that for every fact $\alpha=p(\vec{a})$ over the target schema
such that $\Sigma,D\models\alpha$,
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$
is equal to the multiplicity $n_{\alpha}$ of the empty tuple in the
incognizant certain answers of the Boolean query $\alpha$ w.r.t. $\Sigma$ and
$D$.

  * •

We show that
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$
is equal to the maximum over all s-t tgd $\phi(\vec{x},\vec{y})\rightarrow
p(\vec{x})$ in $\Sigma$ of the multiplicity of $\vec{a}$ in the answer to
$\phi(\vec{x},\vec{y})$ on $D$. Let $\phi(\vec{x},\vec{y})\rightarrow
p(\vec{x})$ in $\Sigma$. For every model $(I,\mu^{I})$ of
$(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}})$,
$\Sigma_{h^{\prime}:\phi(\vec{x},\vec{y})\mapsto
I,h^{\prime}(\vec{x})=\vec{a}}\Pi_{\beta\in
h^{\prime}(\phi(\vec{x},\vec{y}))}\mu^{I}(\beta)\leq\mu^{I}(\alpha)$ and for
every $\beta\in h^{\prime}(\phi(\vec{x},\vec{y}))$, $\beta\in D$ because
$\phi(\vec{x},\vec{y})\rightarrow p(\vec{x})$ is a s-t tgd, so
$\mu^{I}(\beta)\geq\lambda_{\mathbb{N}}(\beta)$. Hence $\mu^{I}(\alpha)$ is
greater or equal to the multiplicity of $\vec{a}$ in the answer to
$\phi(\vec{x},\vec{y})$ on $D$. Moreover, the interpretation that annotates
each $\beta\in D$ by $\lambda_{\mathbb{N}}(\beta)$ and each $\gamma$ produced
by applying some s-t tgd by such maximal multiplicity is a model of
$(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}})$.

  * •

We now show that $n_{\alpha}$ is precisely the maximum over all s-t tgd
$\phi(\vec{x},\vec{y})\rightarrow p(\vec{x})$ in $\Sigma$ of the multiplicity
of $\vec{a}$ in the answer to $\phi(\vec{x},\vec{y})$ on $D$. Every
incognizant solution $J$ for $D$ w.r.t. $\Sigma$ is such that the multiplicity
of $\alpha$ is at least the multiplicity of $\vec{a}$ in the answer of
$\phi(\vec{x},\vec{y})$ on $D$ for every $\phi(\vec{x},\vec{y})\rightarrow
p(\vec{x})$ in $\Sigma$. Moreover, if $J$ is a incognizant solution for $D$
w.r.t. $\Sigma$, then $J^{\prime}$ obtained from $J$ by setting the
multiplicity of $\alpha$ to this maximal multiplicity is also a incognizant
solution, as it still satisfies all s-t tgds.

Hence,
$n_{\alpha}=\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha)$.

$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
is the minimal $\mu^{I}(\mathsf{goal})$ over the models $(I,\mu^{I})$ of
$\Sigma\cup\\{q\rightarrow\mathsf{goal}\\}$ and
$(D,\mathbb{N},\lambda_{\mathbb{N}})$. Since such models are models of
$\Sigma$ and $(D,\mathbb{N},\lambda_{\mathbb{N}})$,
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
is equal to the sum of $\prod_{\alpha_{i}\in
h(q)}\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha_{i})$
where $h$ ranges over the homomorphisms from $q$ to the set $J$ of facts
entailed by $\Sigma$ and $D$.

The multiplicity of the empty tuple in the incognizant certain answers of $q$
w.r.t. $\Sigma$ and $D$ is the minimum over the incognizant solutions of the
multiplicity of the empty tuple in the answers of $q$. Given a incognizant
solution $J$, the multiplicity of the empty tuple in the answers of $q$ over
$J$ is the sum over the homomorphisms $h:q\mapsto J$ of the product of the
multiplicities of $\alpha_{i}=h(p_{i}(\vec{x}))$. Moreover, such $\alpha_{i}$
are such that $\Sigma,D\models\alpha_{i}$ so their minimal multiplicities in
some incognizant solution are
$n_{\alpha_{i}}=\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N},\lambda_{\mathbb{N}},\alpha_{i})$.

It follows that the multiplicity of the empty tuple in the incognizant certain
answers of the BCQ $\alpha$ w.r.t. $\Sigma$ and $D$ is equal to
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$.
∎

#### Connection between Description Logics Bag Semantics and Provenance
Semantics

? (?) defined a bag semantics for the description logic DL-Lite then extended
it to the full ontology-based data access setting (?). We focus on the DL-Lite
case with unique name assumption considered in (?) for simplicity, but mapping
rules compatible with our setting could be added.

A bag ABox corresponds to a database annotated with integers
$(D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$. A bag interpretation
$\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ can also
be seen as a (possibly infinite) set of facts annotated with elements from
$\mathbb{N}^{\infty}$. The interpretation function extends to concepts and
roles as follows: $(P^{-})^{\mathcal{I}}(u,v)=P^{\mathcal{I}}(v,u)$ and
$(\exists
R)^{\mathcal{I}}(u)=\sum_{v\in\Delta^{\mathcal{I}}}R^{\mathcal{I}}(u,v)$.
$\mathcal{I}$ is a model of a bag ABox if the multiplicity of every fact in
$\mathcal{I}$ is at least its multiplicity in the ABox; it is a model of a
TBox if it satisfies all its concept and role inclusions where $C\sqsubseteq
D$ is satisfied iff $C^{\mathcal{I}}(\vec{x})\leq D^{\mathcal{I}}(\vec{x})$
for every $\vec{x}$.

The bag answers of a CQ $q=\exists\vec{y}\phi(\vec{x},\vec{y})$ over a bag
interpretation $\mathcal{I}$ are defined by
$q^{\mathcal{I}}(\vec{a})=\sum_{\nu\in
V}\prod_{S(\vec{t})\in\phi(\vec{x},\vec{y})}S^{\mathcal{I}}(\nu(\vec{t}))$
where $V$ is the set of all valuations
$\nu:\vec{x}\cup\vec{y}\mapsto\Delta^{\mathcal{I}}$ such that
$\nu(\vec{x})=\vec{a}^{\mathcal{I}}$ and $\nu(a)=a^{\mathcal{I}}$ for every
constant $a$. Finally the bag certain answers to $q$ is the bag-intersection
of $q^{\mathcal{I}}$ over all models $\mathcal{I}$ of the ABox and TBox, i.e.,
the multiplicity of a certain answer is the minimum of its multiplicities over
the models.

To compare the bag semantics defined by ? (?) for DL-Lite and a provenance
$\mathcal{P}$ with the extended counting semiring $\mathbb{N}^{\infty}$, we
consider the case where $\Sigma$ is a set of Datalog rules which are
formulated in DL-Lite, i.e., use only unary and binary predicates and contains
a single atom in body and head.

We show below that the DL-Lite bag semantics coincides with
$\mathcal{P}^{\texttt{AM}}$ with the (extended) counting semiring. The
examples we gave in Section 3.1 to show that $\mathcal{P}^{\texttt{AM}}$ and
$\mathcal{P}^{\texttt{SAM}}$ differ can be easily adapted to show that
$\mathcal{P}^{\texttt{SAM}}$ does not coincide with the DL-Lite bag semantics
(just replace $\mathsf{goal}$ by $H(x)$ in $\Sigma$ and consider BCQ
$q=\exists xH(x)$), and the example we gave in Section 3.1 to show that the
cognizant and incognizant semantics differ shows that the
execution/derivation-tree based semantics do not coincide with the DL-Lite bag
semantics either.

######  Proposition 16.

For every set $\Sigma$ of Datalog rules which are formulated in DL-Lite, $D$,
$\lambda_{\mathbb{N}}$, and BCQ $q$,
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})$
is equal to the multiplicity of the empty tuple in the bag certain answers to
$q$ over $(\Sigma,D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$.

###### Proof.

Let $n$ be the multiplicity of the empty tuple in the bag certain answers to
$q$ over $(\Sigma,D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$.

Let $\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ be a
model of $\Sigma$ and $(D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$ seen as a
DL-Lite TBox and bag ABox. Assume w.l.o.g. that
$\mathcal{D}(D)\subseteq\Delta$ and that for every $a\in\mathcal{D}(D)$,
$a^{\mathcal{I}}=a$. Let $(I,\mu^{I})$ be the annotated interpretation defined
by $I=\\{S(\vec{a})\mid S^{\mathcal{I}}(\vec{a})>0\\}\cup\\{\mathsf{goal}\\}$
and $\mu^{I}(S(\vec{a}))=S^{\mathcal{I}}(\vec{a})$ for every $S(\vec{a})\in
I$, $\mu^{I}(\mathsf{goal})=q^{\mathcal{I}}()$. We show that $(I,\mu^{I})$ is
an annotated model of $\Sigma$ and
$(D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$.

  * •

Since $\mathcal{I}$ is a model of
$(D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$, then for every $S(\vec{a})\in
D$,
$S^{\mathcal{I}}(\vec{a}^{\mathcal{I}})\geq\lambda_{\mathbb{N}}(S(\vec{a}))$.
Hence $I$ fulfills point (1) of the definition of annotated models.

  * •

Let $r:=\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ be in $\Sigma$ and
$h:\phi(\vec{x},\vec{y})\mapsto I$. We are in one of the following cases.

    * –

$r=A(x)\rightarrow B(x)$, $h(x)=a$, $A(a)\in I$: since $\mathcal{I}$ satisfies
$A\sqsubseteq B$, $A^{\mathcal{I}}(a)\leq B^{\mathcal{I}}(a)$, so $B(a)\in I$
and $\mu^{I}(A(a))\leq\mu^{I}(B(a))$.

    * –

$r=R(x,y)\rightarrow S(x,y)$, $h(x)=a$, $h(y)=b$, $R(a,b)\in I$: since
$\mathcal{I}$ satisfies $R\sqsubseteq S$, $R^{\mathcal{I}}(a,b)\leq
S^{\mathcal{I}}(a,b)$, so $S(a,b)\in I$ and
$\mu^{I}(R(a,b))\leq\mu^{I}(S(a,b))$.

    * –

$r=R(x,y)\rightarrow S(y,x)$, $h(x)=a$, $h(y)=b$, $R(a,b)\in I$: since
$\mathcal{I}$ satisfies $R\sqsubseteq S^{-}$,
$R^{\mathcal{I}}(a,b)\leq(S^{-})^{\mathcal{I}}(a,b)=S^{\mathcal{I}}(b,a)$, so
$S(b,a)\in I$ and $\mu^{I}(R(a,b))\leq\mu^{I}(S(b,a))$.

    * –

$r=R(x,y)\rightarrow B(x)$, $h(x)=a$, $h(y)=b$, $R(a,b)\in I$: since
$\mathcal{I}$ satisfies $\exists R\sqsubseteq B$, $(\exists
R)^{\mathcal{I}}(a)\leq B^{\mathcal{I}}(a)$ with $(\exists
R)^{\mathcal{I}}(a)=\sum_{v\in\Delta^{\mathcal{I}}}R^{\mathcal{I}}(a,v)$, so
$B(a)\in I$ and $\sum_{R(a,v)\in I}\mu^{I}(R(a,v))\leq\mu^{I}(B(a))$.

    * –

$r=R(y,x)\rightarrow B(x)$, $h(x)=a$, $h(y)=b$, $R(b,a)\in I$: since
$\mathcal{I}$ satisfies $\exists R^{-}\sqsubseteq B$, $(\exists
R^{-})^{\mathcal{I}}(a)\leq B^{\mathcal{I}}(a)$ with $(\exists
R^{-})^{\mathcal{I}}(a)=\sum_{v\in\Delta^{\mathcal{I}}}R^{\mathcal{I}}(v,a)$,
so $B(a)\in I$ and $\sum_{R(v,a)\in I}\mu^{I}(R(v,a))\leq\mu^{I}(B(a))$.

In all cases, we have shown that $h(H(\vec{x}))\in I$ and
$\sum_{h^{\prime}:\phi(\vec{x},\vec{y})\mapsto
I,h^{\prime}(\vec{x})=h(\vec{x})}\prod_{\beta\in
h^{\prime}(\phi(\vec{x},\vec{y}))}\mu^{I}(\beta)\sqsubseteq\mu^{I}(h(H(\vec{x})))$.

  * •

Finally, consider $q\rightarrow\mathsf{goal}$ and assume that there is a
homomorphism $h$ from $q$ to $I$. Since
$\mu^{I}(\mathsf{goal})=q^{\mathcal{I}}()=\sum_{\nu\in V}\prod_{S(\vec{t})\in
q}S^{\mathcal{I}}(\nu(\vec{t}))$ where $V$ is the set of all valuations
$\nu:\vec{x}\mapsto\Delta^{\mathcal{I}}$ such that $\nu(a)=a^{\mathcal{I}}$
for every constant $a$, $\mu^{I}(\mathsf{goal})\geq\sum_{h^{\prime}:q\mapsto
I}\prod_{S(\vec{t})\in
q}S^{\mathcal{I}}(h^{\prime}(\vec{t}))=\sum_{h^{\prime}:q\mapsto
I}\prod_{\beta\in h^{\prime}(q)}\mu^{I}(\beta)$.

Hence $I$ fulfills point (2) of the definition of annotated models.

By definition of
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})$,
it follows that
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})\leq\mu^{I}(\mathsf{goal})$.
Hence
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})\leq
q^{\mathcal{I}}()$. Since this is true for any model $\mathcal{I}$ and $n$ is
the minimal $q^{\mathcal{I}}()$ over all models, it follows that
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})\leq
n$.

In the other direction, let $(I,\mu^{I})$ be an annotated model of
$\Sigma\cup\\{q\rightarrow\mathsf{goal}\\}$ and
$(D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$. Let
$\mathcal{I}=\langle\Delta^{\mathcal{I}},\cdot^{\mathcal{I}}\rangle$ be
defined by $\Delta^{\mathcal{I}}=\mathcal{D}(D)$ and
$S^{\mathcal{I}}(\vec{x})=\mu^{I}(S(\vec{x}))$ if $S(\vec{x})\in I$,
$S^{\mathcal{I}}(\vec{x})=0$ otherwise. We show that $\mathcal{I}$ is a model
of $\Sigma$ and $(D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$ seen as a DL-
Lite TBox and bag ABox.

  * •

Since for every $\alpha\in D$,
$\lambda_{\mathbb{N}}(\alpha)\leq\mu^{I}(\alpha)$, the multiplicity of
$\alpha$ in $\mathcal{I}$ is at least its multiplicity
$\lambda_{\mathbb{N}}(\alpha)$ in the ABox, so $\mathcal{I}$ is a model of
$(D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}})$ seen as a bag ABox.

  * •

We show that $\mathcal{I}$ satisfies all concept and role inclusions
corresponding to rules in $\Sigma$.

    * –

For simple concept inclusion $A\sqsubseteq B$, i.e., $A(x)\rightarrow B(x)$,
since for every $a\in\Delta^{\mathcal{I}}$,
$A^{\mathcal{I}}(a)=\mu^{I}(A(a))$, $B^{\mathcal{I}}(a)=\mu^{I}(B(a))$ and
$(I,\mu^{I})$ is a model of $\Sigma$, $A^{\mathcal{I}}(a)\leq
B^{\mathcal{I}}(a)$ so $\mathcal{I}$ satisfies $A\sqsubseteq B$.

    * –

The role inclusion cases $R\sqsubseteq S$ and $R\sqsubseteq S^{-}$ are similar
to $A\sqsubseteq B$.

    * –

For the case $\exists R\sqsubseteq B$, i.e., $R(x,y)\rightarrow B(x)$, for
every $a\in\Delta^{\mathcal{I}}$, $(\exists
R)^{\mathcal{I}}(a)=\sum_{v\in\Delta^{\mathcal{I}}}R^{\mathcal{I}}(a,v)=\sum_{R(a,v)\in
I}\mu^{I}(R(a,v))$ and since $(I,\mu^{I})$ is a model of $\Sigma$,
$\sum_{R(a,v)\in I}\mu^{I}(R(a,v))\leq\mu^{I}(B(a))$ so $(\exists
R)^{\mathcal{I}}(a)\leq B^{\mathcal{I}}(a)$ and $\mathcal{I}$ satisfies
$\exists R\sqsubseteq B$.

    * –

The case $\exists R^{-}\sqsubseteq B$ is similar.

$q^{\mathcal{I}}()=\sum_{\nu\in V}\prod_{S(\vec{t})\in
q}S^{\mathcal{I}}(\nu(\vec{t}))$ where $V$ is the set of all valuations
$\nu:\vec{x}\mapsto\Delta^{\mathcal{I}}$ such that $\nu(a)=a^{\mathcal{I}}$
for every constant $a$, so $q^{\mathcal{I}}()=\sum_{h:q\mapsto
I}\prod_{\beta\in h(q)}\mu^{I}(\beta)$. Since $(I,\mu^{I})$ is a model of
$\Sigma\cup\\{q\rightarrow\mathsf{goal}\\}$, it follows that
$q^{\mathcal{I}}()\leq\mu^{I}(\mathsf{goal})$. Hence, by definition of $n$,
$n\leq q^{\mathcal{I}}()\leq\mu^{I}(\mathsf{goal})$. Since this is true for
any model $(I,\mu^{I})$, it follows that
$n\leq\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})$,
so that
$n=\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})$.
∎

#### Proof of Proposition 1

Proposition 1 follows from Propositions 15 and 16. In particular, note that in
the DL-Lite case, if the database facts are annotated with elements from
$\mathbb{N}$ rather than $\mathbb{N}^{\infty}$, then
$\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N}^{\infty},\lambda_{\mathbb{N}},\mathsf{goal})=\mathcal{P}^{\texttt{AM}}(\Sigma\cup\\{q\rightarrow\mathsf{goal}\\},D,\mathbb{N},\lambda_{\mathbb{N}},\mathsf{goal})$
since there exist finite models of $\Sigma$ and $D$ (because $\Sigma$ contains
only Datalog rules) such that all facts annotations are in $\mathbb{N}$. See 1

###  A.2 Model-Based Semantics

We start by showing a few lemmas that will be useful to prove results from
Section 3.1 as well as later in the proofs of the results in Table 1.

######  Lemma 1.

The annotated interpretation $(I_{0},\mu^{I_{0}})$ defined by
$I_{0}=\\{\alpha\mid\Sigma,D\models\alpha\\}$ and
$\mu^{I_{0}}(\alpha)=\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$
for every $\alpha\in I_{0}$ is a model of $\Sigma$ and
$(D,\mathbb{K},\lambda)$. It follows that
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)\sqsubseteq\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.

###### Proof.

It is easy to check point (1) of the definition: $D\subseteq I_{0}$ and for
every $\alpha\in D$, there exists a derivation tree in
$T^{\Sigma}_{D}(\alpha)$ that consists of a single root node labelled
$\alpha$, so $\lambda(\alpha)\sqsubseteq\mu^{I_{0}}(\alpha)$.

For point (2), let $\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ be a rule in
$\Sigma$ and $h$ be a homomorphism from $\phi(\vec{x},\vec{y})$ to $I_{0}$. By
construction of $I_{0}$, for every $\beta\in h(\phi(\vec{x},\vec{y}))$,
$\Sigma,D\models\beta$. Hence $\Sigma,D\models h(\phi(\vec{x},\vec{y}))$ so
$\Sigma,D\models h(H(\vec{x}))$. It follows that $h(H(\vec{x}))\in I_{0}$ by
definition of $I_{0}$.

Let $h(H(\vec{x}))=\alpha$, and let $\mathcal{S}$ be the set of all
homomorphisms $h^{\prime}:\phi(\vec{x},\vec{y})\mapsto I_{0}$ such that
$h^{\prime}(\vec{x})=h(\vec{x})$. For each such $h^{\prime}\in\mathcal{S}$,
let $\gamma^{h^{\prime}}_{1},\dots,\gamma^{h^{\prime}}_{k_{h^{\prime}}}$ be
the set of facts from $I_{0}$ such that
$h^{\prime}(\phi(\vec{x},\vec{y}))=\gamma^{h^{\prime}}_{1}\wedge\dots\wedge\gamma^{h^{\prime}}_{k_{h^{\prime}}}$.

  1. 1.

By definition of $(I_{0},\mu^{I_{0}})$, $\mu^{I_{0}}(\alpha)=\Sigma_{t\in
T^{\Sigma}_{D}(\alpha)}\Lambda(t)$.

  2. 2.

For every $h^{\prime}\in\mathcal{S}$, and every
$(t_{1},\dots,t_{k_{h^{\prime}}})\in
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{1})\times\dots\times
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{k_{h^{\prime}}})$, there is a derivation
tree $t\in T^{\Sigma}_{D}(\alpha)$ whose root is $(\alpha,r,h^{\prime})$ and
has subtrees $t_{1},\dots,t_{k_{h^{\prime}}}$.

  3. 3.

It follows that
$\Sigma_{h^{\prime}\in\mathcal{S}}\Sigma_{(t_{1},\dots,t_{k_{h^{\prime}}})\in
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{1})\times\dots\times
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{k_{h^{\prime}}})}\Pi_{i=1}^{k_{h^{\prime}}}\Lambda(t_{i})\sqsubseteq\mu^{I_{0}}(\alpha)$.

  4. 4.

By definition of $(I_{0},\mu^{I_{0}})$, for every $h^{\prime}\in\mathcal{S}$
and $1\leq i\leq k_{h^{\prime}}$,
$\mu^{I_{0}}(\gamma^{h^{\prime}}_{i})=\Sigma_{t\in
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{i})}\Lambda(t)$.

  5. 5.

Hence for every $h^{\prime}\in\mathcal{S}$, $\Pi_{\beta\in
h^{\prime}(\phi(\vec{x},\vec{y}))}\mu^{I_{0}}(\beta)=\Pi_{i=1}^{k_{h^{\prime}}}\Sigma_{t\in
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{i})}\Lambda(t)=\Sigma_{(t_{1},\dots,t_{k_{h^{\prime}}})\in
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{1})\times\dots\times
T^{\Sigma}_{D}(\gamma^{h^{\prime}}_{k_{h^{\prime}}})}\Pi_{i=1}^{k_{h^{\prime}}}\Lambda(t_{i})$.

It follows from (3) and (5) that
$\Sigma_{h^{\prime}:\phi(\vec{x},\vec{y})\mapsto
I_{0},h^{\prime}(\vec{x})=h(\vec{x})}\Pi_{\beta\in
h^{\prime}(\phi(\vec{x},\vec{y}))}\mu^{I_{0}}(\beta)\sqsubseteq\mu^{I_{0}}(h(H(\vec{x})))$.
Hence $(I_{0},\mu^{I_{0}})$ is a model of $\Sigma$ and
$(D,\mathbb{K},\lambda)$. ∎

######  Lemma 2.

The set-annotated interpretation $(I_{0},\mu^{I_{0}})$ defined by
$I_{0}=\\{\alpha\mid\Sigma,D\models\alpha\\}$ and
$\mu^{I_{0}}(\alpha)=\\{\Lambda(t)\mid t\in T^{\Sigma}_{D}(\alpha)\\}$ for
every $\alpha\in I_{0}$ is a model of $\Sigma$ and $(D,\mathbb{K},\lambda)$.

###### Proof.

Let $I_{0}=\\{\alpha\mid\Sigma,D\models\alpha\\}$ and
$\mu^{I_{0}}(\alpha)=\\{\Lambda(t)\mid t\in T^{\Sigma}_{D}(\alpha)\\}$ for
every $\alpha\in I_{0}$. We show that $(I_{0},\mu^{I_{0}})$ is a model of
$\Sigma$ and $(D,\mathbb{K},\lambda)$.

It is easy to check point (1) of the definition: $D\subseteq I_{0}$ and for
every $\alpha\in D$, there exists a derivation tree in
$T^{\Sigma}_{D}(\alpha)$ that consists of a single root node labelled
$\alpha$, so $\lambda(\alpha)\in\mu^{I_{0}}(\alpha)$.

For point (2), let $\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ be a rule in
$\Sigma$ and $h$ be a homomorphism from $\phi(\vec{x},\vec{y})$ to $I_{0}$. By
construction of $I_{0}$, for every $\beta\in h(\phi(\vec{x},\vec{y}))$,
$\Sigma,D\models\beta$. Hence $\Sigma,D\models h(\phi(\vec{x},\vec{y}))$ so
$\Sigma,D\models h(H(\vec{x}))$. It follows that $h(H(\vec{x}))\in I_{0}$. Let
$h(H(\vec{x}))=\alpha$ and
$h(\phi(\vec{x},\vec{y}))=\gamma_{1}\wedge\dots\wedge\gamma_{k}$.

  1. 1.

By definition of $(I_{0},\mu^{I_{0}})$, $\mu^{I_{0}}(\alpha)=\\{\Lambda(t)\mid
t\in T^{\Sigma}_{D}(\alpha)\\}$.

  2. 2.

For every $(t_{1},\dots,t_{k})\in T^{\Sigma}_{D}(\gamma_{1})\times\dots\times
T^{\Sigma}_{D}(\gamma_{k})$, there is a derivation tree $t\in
T^{\Sigma}_{D}(\alpha)$ whose root is $(\alpha,r,h^{\prime})$ and has subtrees
$t_{1},\dots,t_{k}$.

  3. 3.

It follows that $\\{\Pi_{i=1}^{k}\Lambda(t_{i})\mid(t_{1},\dots,t_{k})\in
T^{\Sigma}_{D}(\gamma_{1})\times\dots\times
T^{\Sigma}_{D}(\gamma_{k})\\}\subseteq\mu^{I_{0}}(\alpha)$.

  4. 4.

By definition of $(I_{0},\mu^{I_{0}})$, for every $1\leq i\leq k$,
$\mu^{I_{0}}(\gamma_{i})=\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\gamma_{i})\\}$.

It follows from (3) and (4) that
$\\{\Pi_{i=1}^{k}m_{i}\mid(m_{1},\dots,m_{k})\in\mu^{I_{0}}(\gamma_{1})\times\dots\times\mu^{I_{0}}(\gamma_{k})\\}\subseteq\mu^{I_{0}}(h(H(\vec{x}))$.
Hence $(I_{0},\mu^{I_{0}})$ is a model of $\Sigma$ and
$(D,\mathbb{K},\lambda)$ and
$\bigcap_{(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)}\mu^{I}(\alpha)=\\{\Lambda(t)\mid
t\in T^{\Sigma}_{D}(\alpha)\\}$. ∎

######  Lemma 3.

For both annotated interpretations and set-annotated interpretations,
$\Sigma,D\models\alpha$ if and only if $\alpha\in I$ for every model
$(I,\mu^{I})$ of $\Sigma$ and $(D,\mathbb{K},\lambda)$.

###### Proof.

This follows from the facts that

  1. 1.

every (set-)annotated model $(I,\mu^{I})$ of $\Sigma$ and
$(D,\mathbb{K},\lambda)$ is such that $I$ is a model of $\Sigma$ and $D$ by
definition of annotated and set-annotated models; and

  2. 2.

for every model $I$ of $\Sigma$ and $D$, there exists a (set-)annotated model
$(I,\mu^{I})$ of $\Sigma$ and $(D,\mathbb{K},\lambda)$:

     * •

For $\mathcal{P}^{\texttt{AM}}$ such a model can be obtained by setting
$\mu^{I}(\alpha)=\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$
by Lemma 1.

     * •

For $\mathcal{P}^{\texttt{SAM}}$ such a model can be obtained by setting
$\mu^{I}(\alpha)=\\{\Lambda(t)\mid t\in T^{\Sigma}_{D}(\alpha)\\}$ by Lemma
2.∎

######  Lemma 4.

If $\mathbb{K}=(K,+,\times,0,1)$ is a commutative $\omega$-continuous semiring
such that for every $x,y\in K$, the greatest lower bound of $x$ and $y$ is
well defined (i.e., there exists a unique element $z\in K$ such that
$z\sqsubseteq x$, $z\sqsubseteq y$ and every $z^{\prime}$ such that
$z^{\prime}\sqsubseteq x$ and $z^{\prime}\sqsubseteq y$ is such that
$z^{\prime}\sqsubseteq z$), then for every $a,b\in K$, $a\sqsubseteq b$ and
$b\sqsubseteq a$ implies that $a=b$. In particular, $a\sqsubseteq 0$ implies
that $a=0$.

###### Proof.

Let $a,b\in K$ such $a\sqsubseteq b$ and $b\sqsubseteq a$. Since

  * •

$a\sqsubseteq a$, $a\sqsubseteq b$ and every $z^{\prime}$ such that
$z^{\prime}\sqsubseteq a$ and $z^{\prime}\sqsubseteq b$ is such that
$z^{\prime}\sqsubseteq a$; and

  * •

$b\sqsubseteq a$, $b\sqsubseteq b$ and every $z^{\prime}$ such that
$z^{\prime}\sqsubseteq a$ and $z^{\prime}\sqsubseteq b$ is such that
$z^{\prime}\sqsubseteq b$,

then both $a$ and $b$ are the (unique) greatest lower bound of $a$ and $b$. ∎

######  Lemma 5.

For every $\alpha$ such that $\Sigma,D\models\alpha$ and $t\in
T^{\Sigma}_{D}(\alpha)$, for every annotated model $(I,\mu^{I})$ of $\Sigma$
and $(D,\mathbb{K},\lambda)$, $\Lambda(t)\sqsubseteq\mu^{I}(\alpha)$, where
$\Lambda(t)=\Pi_{\beta\text{ is a leaf of $t$}}\lambda(\beta)$. It follows
that for every $t\in T^{\Sigma}_{D}(\alpha)$,
$\Lambda(t)\sqsubseteq\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.

###### Proof.

We show by induction that for every $n\in\mathbb{N}$, for every $\alpha$ such
that $\Sigma,D\models\alpha$ and $t\in T^{\Sigma}_{D}(\alpha)$ which contains
at most $n$ inner nodes (i.e., nodes that have children), for every model
$(I,\mu^{I})$ of $\Sigma$ and $(D,\mathbb{K},\lambda)$,
$\Lambda(t)\sqsubseteq\mu^{I}(\alpha)$.

  * •

Base case: $n=0$. Let $\alpha$ be such that $\Sigma,D\models\alpha$ and let
$t\in T^{\Sigma}_{D}(\alpha)$ do not contain any inner node. In this case, $t$
consists of a single node labeled with $\alpha$. Thus
$\Lambda(t)=\lambda(\alpha)$. Moreover, $\alpha\in D$ so for every model
$(I,\mu^{I})$ of $\Sigma$ and $(D,\mathbb{K},\lambda)$,
$\lambda(\alpha)\sqsubseteq\mu^{I}(\alpha)$.

  * •

Induction step: assume that the property is true for some $n$ and let $\alpha$
be such that $\Sigma,D\models\alpha$ and $t\in T^{\Sigma}_{D}(\alpha)$ contain
at most $n+1$ inner nodes. By definition of a derivation tree, the root of $t$
is of the form $(\alpha,r,h)$ for some rule
$r=\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ that belongs to $\Sigma$ and
its children are of the form
$(\gamma_{1},r_{1},h_{1}),\dots,(\gamma_{k},r,_{k},h_{k})$ where
$\gamma_{1}\wedge\dots\wedge\gamma_{k}=h(\phi(\vec{x},\vec{y}))$ and
$\alpha=h(H(\vec{x}))$. For $1\leq i\leq k$, let $t_{i}$ be the subtree of $t$
rooted in $(\gamma_{i},r_{i},h_{i})$. $t_{i}$ is a derivation tree of
$\gamma_{i}$ w.r.t. $\Sigma,D$ so $\Sigma,D\models\gamma_{i}$. Moreover
$t_{i}$ contains at most $n$ inner nodes. Let $(I,\mu^{I})$ be a model of
$\Sigma$ and $(D,\mathbb{K},\lambda)$. For $1\leq i\leq k$, $\gamma_{i}\in I$
by Lemma 3 and by induction hypothesis,
$\Lambda(t_{i})\sqsubseteq\mu^{I}(\gamma_{i})$. Moreover, since $h$ is a
homomorphism from the body of $r$ to $\\{\gamma_{1},\dots,\gamma_{k}\\}$ such
that $h(H(\vec{x}))=\alpha$, then
$\Pi_{i=1}^{k}\mu^{I}(\gamma_{i})\sqsubseteq\mu^{I}(\alpha)$. It follows that
$\Pi_{i=1}^{k}\Lambda(t_{i})\sqsubseteq\mu^{I}(\alpha)$, hence
$\Lambda(t)\sqsubseteq\mu^{I}(\alpha)$. ∎

######  Lemma 6.

$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\sum_{\\{\Lambda(t)\mid
t\in T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)$, where $\Lambda(t)=\Pi_{\beta\text{
is a leaf of $t$}}\lambda(\beta)$.

###### Proof.

We show by induction that for every $n\in\mathbb{N}$, for every $\alpha$ such
that $\Sigma,D\models\alpha$ and $t\in T^{\Sigma}_{D}(\alpha)$ which contains
at most $n$ inner nodes (i.e., nodes that have children), for every set-
annotated model $(I,\mu^{I})$ of $\Sigma$ and $(D,\mathbb{K},\lambda)$,
$\Lambda(t)\in\mu^{I}(\alpha)$.

  * •

Base case: $n=0$. Let $\alpha$ be such that $\Sigma,D\models\alpha$ and let
$t\in T^{\Sigma}_{D}(\alpha)$ do not contain any inner node. In this case, $t$
consists of a single node labeled with $\alpha$. Thus
$\Lambda(t)=\lambda(\alpha)$. Moreover, $\alpha\in D$ so for every model
$(I,\mu^{I})$ of $\Sigma$ and $(D,\mathbb{K},\lambda)$,
$\lambda(\alpha)\in\mu^{I}(\alpha)$.

  * •

Induction step: assume that the property is true for some $n$ and let $\alpha$
be such that $\Sigma,D\models\alpha$ and $t\in T^{\Sigma}_{D}(\alpha)$ contain
at most $n+1$ inner nodes. By definition of a derivation tree, the root of $t$
is of the form $(\alpha,r,h)$ for some rule
$r=\phi(\vec{x},\vec{y})\rightarrow H(\vec{x})$ that belongs to $\Sigma$ and
its children are of the form
$(\gamma_{1},r_{1},h_{1}),\dots,(\gamma_{k},r,_{k},h_{k})$ where
$\gamma_{1}\wedge\dots\wedge\gamma_{k}=h(\phi(\vec{x},\vec{y}))$ and
$\alpha=h(H(\vec{x}))$. For $1\leq i\leq k$, let $t_{i}$ be the subtree of $t$
rooted in $(\gamma_{i},r_{i},h_{i})$. $t_{i}$ is a derivation tree of
$\gamma_{i}$ w.r.t. $\Sigma,D$ so $\Sigma,D\models\gamma_{i}$. Moreover
$t_{i}$ contains at most $n$ inner nodes. Let $(I,\mu^{I})$ be a model of
$\Sigma$ and $(D,\mathbb{K},\lambda)$. For $1\leq i\leq k$, $\gamma_{i}\in I$
by Lemma 3 and by induction hypothesis,
$\Lambda(t_{i})\in\mu^{I}(\gamma_{i})$. Moreover, since $h$ is a homomorphism
from the body of $r$ to $\\{\gamma_{1},\dots,\gamma_{k}\\}$ such that
$h(H(\vec{x}))=\alpha$, then
$\\{\Pi_{i=1}^{k}m_{i}\mid(m_{1},\dots,m_{k})\in\mu^{I}(\gamma_{1})\times\dots\times\mu^{I}(\gamma_{k})\\}\subseteq\mu^{I}(\alpha)$.
It follows that $\Pi_{i=1}^{k}\Lambda(t_{i})\in\mu^{I}(\alpha)$, hence
$\Lambda(t)\in\mu^{I}(\alpha)$.

Hence for every $\alpha$ such that $\Sigma,D\models\alpha$ and $t\in
T^{\Sigma}_{D}(\alpha)$, for every model $(I,\mu^{I})$ of $\Sigma$ and
$(D,\mathbb{K},\lambda)$, $\Lambda(t)\in\mu^{I}(\alpha)$. Therefore
$\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}\subseteq\bigcap_{(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)}\mu^{I}(\alpha)$.

Since by Lemma 2 the set-annotated interpretation $(I_{0},\mu^{I_{0}})$
defined by $I_{0}=\\{\alpha\mid\Sigma,D\models\alpha\\}$ and
$\mu^{I_{0}}(\alpha)=\\{\Lambda(t)\mid t\in T^{\Sigma}_{D}(\alpha)\\}$ for
every $\alpha\in I_{0}$ is a model of $\Sigma$ and $(D,\mathbb{K},\lambda)$,
it follows that
$\bigcap_{(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)}\mu^{I}(\alpha)=\\{\Lambda(t)\mid
t\in T^{\Sigma}_{D}(\alpha)\\}$. ∎

See 2

###### Proof.

$\mathcal{P}^{\texttt{AM}}\sqsubseteq\mathcal{P}^{\texttt{AT}}$ follows from
Lemma 1 and $\mathcal{P}^{\texttt{AM}}\sqsubseteq\mathcal{P}^{\texttt{AT}}$
follows from Lemma 6. ∎

See 3

###### Proof.

Let $\mathbb{K}$ be a commutative $+\,$-idempotent $\omega$-continuous
semiring. In this case,

$\displaystyle\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=$
$\displaystyle\Sigma_{t\in T^{\Sigma}_{D}(\alpha)}\Lambda(t)$ $\displaystyle=$
$\displaystyle\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)$

By Lemma 6, it follows that
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.

Moreover, by Lemma 1, it follows that
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)\sqsubseteq\sum_{\\{\Lambda(t)\mid
t\in T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)$, and by Lemma 5, for every $t\in
T^{\Sigma}_{D}(\alpha)$,
$\Lambda(t)\sqsubseteq\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$,
i.e.,
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\Lambda(t)+S_{t}$
for some $S_{t}\in\mathbb{K}$. Since $\mathbb{K}$ is $+\,$-idempotent,

$\displaystyle\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=$
$\displaystyle\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$
$\displaystyle=$ $\displaystyle\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}(\Lambda(t)+S_{t})$ $\displaystyle=$
$\displaystyle\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)+\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}S_{t}$

Hence $\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)\sqsubseteq\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.
Since $\mathcal{P}^{\texttt{AM}}$ is defined for $\mathbb{K}$ such that for
every $x,y\in K$, the greatest lower bound of $x$ and $y$ is well defined, by
Lemma 4, $\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)\sqsubseteq\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$
and
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)\sqsubseteq\sum_{\\{\Lambda(t)\mid
t\in T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)$ implies that
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\sum_{\\{\Lambda(t)\mid
t\in
T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)=\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.
∎

See 4

###### Proof.

By Lemma 1, $\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)\sqsubseteq\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$, i.e.,
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)=\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)+S$ for some $S\in\mathbb{N}^{\infty}\llbracket
X\rrbracket$. Moreover, for every monomial $m$ in $S$, $m$ occurs in
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$ so there exists $t\in T^{\Sigma}_{D}(\alpha)$
such that $m=\Lambda(t)$. By Lemma 5,
$m\sqsubseteq\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$.

By Lemma 6, $\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)=\sum_{\\{\Lambda(t)\mid t\in
T^{\Sigma}_{D}(\alpha)\\}}\Lambda(t)$ where $\Lambda(t)=\Pi_{\beta\text{ is a
leaf of $t$}}\lambda_{X}(\beta)$. It is easy to see that this is exactly the
sum of monomials that occur in
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{N}^{\infty}\llbracket
X\rrbracket,\lambda_{X},\alpha)$. ∎

This final lemma shows that $\mathcal{P}^{\texttt{AM}}$ and
$\mathcal{P}^{\texttt{SAM}}$ fulfill the conditions of Definition 3.

######  Lemma 7.

If $\Sigma,D\not\models\alpha$ then
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0$.

If $\mathbb{K}$ is positive, for $\mathcal{P}=\mathcal{P}^{\texttt{AM}}$ and
$\mathcal{P}=\mathcal{P}^{\texttt{SAM}}$,
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0$ implies
$\Sigma,D\not\models\alpha$.

###### Proof.

In $\mathcal{P}^{\texttt{AM}}$ case, by Lemma 1,
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)\sqsubseteq\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.
If $\Sigma,D\not\models\alpha$,
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0$ so by Lemma
4, $\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0$. By Lemma
5, for every $t\in T^{\Sigma}_{D}(\alpha)$,
$\Lambda(t)\sqsubseteq\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.
Hence, if $\mathbb{K}$ is positive,
$\mathcal{P}^{\texttt{AM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0$ implies that
$\Lambda(t)=0$ for every $t\in T^{\Sigma}_{D}(\alpha)$. Since databse facts
cannot be annotated with $0$, this means that
$T^{\Sigma}_{D}(\alpha)=\emptyset$ and $\Sigma,D\not\models\alpha$.

In $\mathcal{P}^{\texttt{SAM}}$ case, by Lemma 3, $\Sigma,D\not\models\alpha$
if and only if there exists a set-annotated model $(I,\mu^{I})$ of $\Sigma$
and $(D,\mathbb{K},\lambda)$ such that $\alpha\notin I$. Hence,

  * •

$\Sigma,D\not\models\alpha$ implies that
$\bigcap_{(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)}\mu^{I}(\alpha)=\emptyset$
and
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=\Sigma_{k\in\bigcap_{(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)}\mu^{I}(\alpha)}k=0$;
and

  * •

if $\mathbb{K}$ is positive,
$\mathcal{P}^{\texttt{SAM}}(\Sigma,D,\mathbb{K},\lambda,\alpha)=0$ implies
that
$\bigcap_{(I,\mu^{I})\models(\Sigma,D,\mathbb{K},\lambda)}\mu^{I}(\alpha)=\emptyset$
and $\Sigma,D\not\models\alpha$.∎

###  A.3 Execution- and Tree-Based Semantics

#### Naive Evaluation / All Trees

We denote $(D,\mathbb{K},\lambda_{\mathsf{n}})$ by
$(I_{\mathsf{n}}^{0},\mathbb{K},\lambda_{\mathsf{n}}^{0})$, and for $i\geq 1$
we denote $I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda_{\mathsf{n}})$ by
$(I_{\mathsf{n}}^{i},\mathbb{K},\lambda_{\mathsf{n}}^{i})$.

######  Lemma 8.

For every fact $\alpha\in I_{\mathsf{n}}^{i}$, it holds that

$\lambda_{\mathsf{n}}^{i}(\alpha)=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth}\leq i\end{subarray}}\Lambda(t)$

###### Proof.

We prove the claim by induction on $i$.

##### Induction Basis

If $i=0$ then $\lambda_{\mathsf{n}}^{0}=D$ and the claim holds since
$\lambda_{\mathsf{n}}^{0}(\alpha)=\lambda(\alpha)$ if $\alpha\in D$, or $0$
otherwise. And, by definition, $\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth}\leq
0\end{subarray}}\Lambda(t)=\lambda(\alpha)$ if $\alpha\in D$, or $0$
otherwise.

##### Induction Step

By definition we have

$\lambda_{\mathsf{n}}^{i}(\alpha)=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth}\leq
i\end{subarray}}\Lambda(t)=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth }\leq
i-1\end{subarray}}\Lambda(t)\oplus\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth }i\end{subarray}}\Lambda(t)$

By definition,

$\sum_{\begin{subarray}{c}t\in T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth
}\leq i\end{subarray}}\Lambda(t)=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth }\leq
i-1\end{subarray}}\Lambda(t)\oplus\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth }i\end{subarray}}\Lambda(t)$

By induction hypothesis,

$\sum_{\begin{subarray}{c}t\in T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth
}\leq
i\end{subarray}}\Lambda(t)=\lambda_{\mathsf{n}}^{i-1}(\alpha)\oplus\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth }i\end{subarray}}\Lambda(t)$

Note that from the definition
$I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda):=T_{\Sigma}(I_{\mathsf{n}}^{i-1}(\Sigma,D,\mathbb{K},\lambda))\cup(D,\mathbb{K},\lambda)$
we can conclude (using a simple induction) that

$I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda)=\underbrace{T_{\Sigma}(\cdots
T_{\Sigma}(}_{i\text{
times}}I_{\mathsf{n}}^{0}(\Sigma,D,\mathbb{K},\lambda)\,)\cdots)\oplus\underbrace{T_{\Sigma}(\cdots
T_{\Sigma}(}_{i-1\text{
times}}I_{\mathsf{n}}^{0}(\Sigma,D,\mathbb{K},\lambda)\,)\cdots)\oplus\cdots\oplus
I_{\mathsf{n}}^{0}(\Sigma,D,\mathbb{K},\lambda)$

By the definition of $T_{\Sigma}$ and the above we conclude the desired
equivalence. ∎

See 5

###### Proof.

Let us denote $I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda)$ by
$(I_{\mathsf{n}}^{i},\mathbb{K},\lambda_{\mathsf{n}}^{i})$. From the
convergence of the naive Datalog evalutaion algoritm (?), we can conclude that
there is a $k$ such that $I_{\mathsf{n}}^{\ell}=I_{\mathsf{n}}^{k}$ for every
$\ell\geq k$. Let $\alpha\in I_{\mathsf{n}}^{k}$. It suffices to show that
$\lambda_{\mathsf{n}}^{i}(\alpha)$ converges. By Lemma 8,

$\lambda_{\mathsf{n}}^{i}(\alpha)=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth
}0\end{subarray}}\Lambda(t)\oplus\cdots\oplus\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of depth }i\end{subarray}}\Lambda(t).$

Since $\mathbb{K}$ is $\omega$-continuous this sum converges, and therefore
$\sup_{i}\lambda_{\mathsf{n}}^{i}(\alpha)$ exists, which concludes the proof.
∎

See 6

###### Proof.

By Lemma 8, the sequence of provenance of a fact $\alpha$ over the
$I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda)$ converge to the sum of the
derivation trees of $\alpha$. Thus, we can conclude that the sequence of
$I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda)$ converge to an annotated
database that the
$T_{\Sigma}(I_{\mathsf{n}}^{\infty}(\Sigma,D,\mathbb{K},\lambda))\cup(D,\mathbb{K},\lambda)$
is equal to $I_{\mathsf{n}}^{\infty}(\Sigma,D,\mathbb{K},\lambda)$ and
therefore, $\mathcal{P}^{\texttt{NE}}$ is equal to
$\mathcal{P}^{\texttt{AT}}$. ∎

#### Optimized Naive Evaluation / Minimal Depth Trees

See 7

###### Proof.

The existence of $k$ such that
$I_{\mathsf{o,\alpha}}^{\ell}=I_{\mathsf{o,\alpha}}^{k}$ for every $\ell\geq
k$ is a consequence of the convergence of the original seminaive Datalog
algorithm (?). It suffices to show that for the same $k$ and for every fact
$\beta\in I_{\mathsf{o,\alpha}}^{k}$ if holds that
$\lambda_{\mathsf{sn}}^{k}(\beta)=\lambda_{\mathsf{sn}}^{\ell}(\alpha)$
whenever $\ell\geq k$. This, indeed, follows directly from the definition of
the operator $\Delta_{\Sigma}$. ∎

######  Lemma 9.

For every fact $\beta\in I_{\mathsf{o,\alpha}}^{i}$ where
$(I_{\mathsf{o,\alpha}}^{i},\mathbb{K},I_{\mathsf{o,\alpha}}^{i}):=I_{\mathsf{o,\alpha}}^{i}(\Sigma,D,\mathbb{K},\lambda)$,
the following holds

$I_{\mathsf{o,\alpha}}^{i}(\beta)=\sum_{\begin{subarray}{c}t\in
T^{\Sigma}_{D}(\alpha)\\\ \text{ is of minimal depth with depth }\leq
i\end{subarray}}\Lambda(t)$

###### Proof.

The proof is a direct proof by induction on $i$. ∎

See 8

###### Proof.

The proof is straightforward from Lemma 9. ∎

#### Seminaive Evaluation / Hereditary Minimal Depth Trees

We denote $(D,\mathbb{K},\lambda_{\mathsf{sn}})$ by
$(I_{\mathsf{sn}}^{0},\mathbb{K},\lambda_{\mathsf{sn}}^{0})$, and for $i\geq
1$ we denote $I_{\mathsf{n}}^{i}(\Sigma,D,\mathbb{K},\lambda_{\mathsf{sn}})$
by $(I_{\mathsf{sn}}^{i},\mathbb{K},\lambda_{\mathsf{sn}}^{i})$.

See 9

###### Proof.

The existence of $k$ such that $I_{\mathsf{sn}}^{\ell}=I_{\mathsf{sn}}^{k}$
for every $\ell\geq k$ is a consequence of the convergence of the original
seminaive Datalog algorithm (?). It suffices to show that for the same $k$ and
for every fact $\alpha\in I_{\mathsf{sn}}^{k}$ if holds that
$\lambda_{\mathsf{sn}}^{k}(\alpha)=\lambda_{\mathsf{sn}}^{\ell}(\alpha)$
whenever $\ell\geq k$. This, indeed, follows directly from the definition of
the operator $\Delta_{\Sigma}$. ∎

######  Lemma 10.

For every fact $\alpha\in I_{\mathsf{sn}}^{i}$ where
$(I_{\mathsf{sn}}^{i},\mathbb{K},\lambda^{i}):=I_{\mathsf{sn}}^{i}(\Sigma,D,\mathbb{K},\lambda)$,
the following holds

$\lambda^{i}(\alpha)=\sum_{\begin{subarray}{c}t\in T^{\Sigma}_{D}(\alpha)\\\
\text{ is of hereditary minimal depth with depth }\leq
i\end{subarray}}\Lambda(t)$

###### Proof.

The proof is a direct proof by induction on $i$. ∎

See 10

###### Proof.

The proof is straightforward from Lemma 10. ∎

See 11

###### Proof.

It is straightforward that
$\mathcal{P}^{\texttt{NRT}}\sqsubseteq\mathcal{P}^{\texttt{AT}}\ \text{ and
}\quad\mathcal{P}^{\texttt{MDT}}\sqsubseteq\mathcal{P}^{\texttt{AT}}$. Since
every hereditary minimal depth tree is also non-recursive, we have
$\mathcal{P}^{\texttt{HMDT}}\sqsubseteq\mathcal{P}^{\texttt{NRT}}$. Since
every hereditary minimal depth tree is also a minimal depth tree, we have
$\mathcal{P}^{\texttt{MDT}}\sqsubseteq\mathcal{P}^{\texttt{AT}}$. ∎

###  A.4 Non-Recursive Tree-Based Semantics

See 12

###### Proof.

Assume that $\mathbb{K}$ is a commutative absorptive $\omega$-continuous
semiring. The sum
$\mathcal{P}^{\texttt{AT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$ of the
annotations of the (possibly infinitely many) derivations trees in
$T^{\Sigma}_{D}(\alpha)$ is defined as the supremum of the set of the sums of
the annotations of any finite subset of $T^{\Sigma}_{D}(\alpha)$. We show that
this supremum coincides with
$\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.

It is clear that
$\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$ is a lower
bound of the supremum, since the set of non-recursive trees is a subset of
$T^{\Sigma}_{D}(\alpha)$.

Conversely, let $\\{t_{1},\ldots,t_{n}\\}$ be a finite subset of
$T^{\Sigma}_{D}(\alpha)$. Let us assume that $\\{t_{1},\ldots,t_{n}\\}$
contains all the non-recursive trees of $T^{\Sigma}_{D}(\alpha)$. Let us
define a non-recursive version $t^{\prime}_{i}$ of $t_{i}$ as follows. A
simplification of $t_{i}$ is obtained from $t_{i}$ by picking a node
$(\beta,r,h)$ which has a descendant $n$ of the form
$(\beta,r^{\prime},h^{\prime})$ or $\beta$, and by replacing the subtree
rooted in $(\beta,r,h)$ by the subtree rooted in $n$. $t^{\prime}_{i}$ is any
tree obtained from $t_{i}$ on which no simplification is performable. It holds
that $\Lambda(t_{i})=\Lambda(t^{\prime}_{i})\times e$ for some $e\in K$, which
is the product of the labels of the leaves that have been removed from $t_{i}$
through successive steps of simplification. Hence, by absorptivity of
$(K,+_{\mathbb{K}},\times_{\mathbb{K}},0_{\mathbb{K}},1_{\mathbb{K}})$,
$\Sigma_{i=1}^{n}\Lambda(t_{i})=\Sigma_{i=1}^{n}\Lambda(t^{\prime}_{i})=\mathcal{P}^{\texttt{NRT}}(\Sigma,D,\mathbb{K},\lambda,\alpha)$.
Since this is true for any finite subset $\\{t_{1},\ldots,t_{n}\\}$ of
$T^{\Sigma}_{D}(\alpha)$ that contains the non-recursive trees of
$T^{\Sigma}_{D}(\alpha)$, this concludes the proof. ∎

##  Appendix B Discussion and Proofs for Section 4

###  B.1 Commutation with Homomorphisms and Universal Semirings

The following proposition explicits the connection between the satisfaction of
the Commutation with Homomorphisms Property or Commutation with
$\omega$-Continuous Homomorphisms Property by a provenance semantics
$\mathcal{P}$ and the ability to use a provenance semiring universal for its
semiring domain to factor the computations.

######  Proposition 17.

If $\mathcal{P}$ satisfies the Commutation with (resp. $\omega$-Continuous)
Homomorphisms Property and $\mathit{Prov}(X)$ is universal for its semiring
domain (resp. which contains only $\omega$-continuous semirings),
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=h(\mathcal{P}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\alpha))$
where $h$ is the unique (resp. $\omega$-continuous) semiring homomorphism that
extends $\nu:X\rightarrow K$ where $\nu(x)=\lambda(\lambda_{X}^{-}(x))$ for
every $x\in X$.

Conversely, if $S$ is a set of (resp. $\omega$-continuous) semirings such that
$\mathit{Prov}(X)$ is universal for $S$ and for every $\mathbb{K}\in S$, it
holds that
$\mathcal{P}(\Sigma,D,\mathbb{K},\lambda,\alpha)=h(\mathcal{P}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\alpha))$
where $h$ is the unique (resp. $\omega$-continuous) semiring homomorphism that
extends $\nu:X\rightarrow K$ where $\nu(x)=\lambda(\lambda_{X}^{-}(x))$ for
every $x\in X$, then the restriction $\mathcal{P}_{S}$ of $\mathcal{P}$ to the
semiring domain $S$ satisfies the Commutation with (resp. $\omega$-Continuous)
Homomorphisms Property.

###### Proof.

Assume that $\mathcal{P}$ satisfies the Commutation with Homomorphisms
Property and let $\mathit{Prov}(X)$ be a universal semiring for the semiring
domain of $\mathcal{P}$. Let $\Sigma$ be a Datalog program,
$(D,\mathbb{K},\lambda)$ be an annotated database and $\alpha$ be a fact. Let
$\lambda_{X}$ associate a distinct variable from $X$ to each fact of $D$ and
$h:\mathit{Prov}(X)\rightarrow K$ be the unique semiring homomorphism that
extends $\nu:X\rightarrow K$ where $\nu(x)=\lambda(\lambda_{X}^{-}(x))$ for
every $x\in X$ (the existence of $h$ is guaranteed by the fact that
$\mathit{Prov}(X)$ specializes correctly to $\mathbb{K}$ by definition of a
universal semiring). By the Commutation with Homomorphisms Property, we have
$h(\mathcal{P}(\Sigma,D,\mathit{Prov}(X),\lambda_{X},\alpha))=\mathcal{P}(\Sigma,D,\mathbb{K},h\circ\lambda_{X},\alpha)$.
Moreover, for every $\beta\in D$,
$h\circ\lambda_{X}(\beta)=\nu(\lambda_{X}(\beta))=\lambda(\lambda_{X}^{-}(\lambda_{X}(\beta)))=\lambda(\beta)$,