# Provenance Circuits
for Trees and Treelike Instances
(Extended Version)

Antoine Amarilli Télécom ParisTech; Institut Mines–Télécom; CNRS LTCI
<EMAIL_ADDRESS>Pierre Bourhis CNRS CRIStAL; Université
Lille 1; INRIA Lille<EMAIL_ADDRESS>Pierre Senellart Institut
Mines-Télécom; Télécom ParisTech; CNRS LTCI National University of Singapore;
CNRS IPAL<EMAIL_ADDRESS>
###### Abstract

Query evaluation in monadic second-order logic (MSO) is tractable on trees and
treelike instances, even though it is hard for arbitrary instances. This
tractability result has been extended to several tasks related to query
evaluation, such as counting query results [arnborg1991easy] or performing
query evaluation on probabilistic trees [cohen2009running]. These are two
examples of the more general problem of computing augmented query output, that
is referred to as _provenance_. This article presents a provenance framework
for trees and treelike instances, by describing a linear-time construction of
a circuit provenance representation for MSO queries. We show how this
provenance can be connected to the usual definitions of semiring provenance on
relational instances [green2007provenance], even though we compute it in an
unusual way, using tree automata; we do so via intrinsic definitions of
provenance for general semirings, independent of the operational details of
query evaluation. We show applications of this provenance to capture existing
counting and probabilistic results on trees and treelike instances, and give
novel consequences for probability evaluation.

##  1 Introduction

A celebrated result by Courcelle [Courcelle90] has shown that evaluating a
fixed monadic second-order (MSO) query on relational instances, while
generally hard in the input instance for any level of the polynomial hierarchy
[AjtaiFS98], can be performed in linear time on input instances of _bounded
treewidth_ (or _treelike_ instances), by encoding the query to an automaton on
tree encodings of instances. This idea has been extended more recently to
monadic Datalog [gottlob2010monadic]. In addition to query evaluation, it is
also possible to _count_ in linear time the number of query answers over
treelike instances [arnborg1991easy, pichler2010counting].

However, query evaluation and counting are special cases of the more general
problem of capturing _provenance information_ [CheneyCT09,
green2007provenance] of query results, which describes the link between input
and output tuples. Provenance information can be expressed through various
formalisms, such as _provenance semirings_ [green2007provenance] or Boolean
formulae [suciu2011probabilistic]. Besides counting, provenance can be
exploited for practically important tasks such as answering queries in
incomplete databases [ImielinskiL84], maintaining access rights [ParkNS12], or
computing query probability [suciu2011probabilistic]. To our knowledge, no
previous work has looked at the general question of efficient evaluation of
expressive queries on treelike instances while keeping track of provenance.

Indeed, no proper definition of provenance for queries evaluated via tree
automata has been put forward. The first contribution of this work (Section 3)
is thus to introduce a general notion of _provenance circuit_
[deutch2014circuits] for tree automata, which provides an efficiently
computable representation of all possible results of an automaton over a tree
with uncertain annotations. Of course, we are interested in the provenance of
_queries_ rather than automata; however, in this setting, the provenance that
we compute has an intrinsic definition, so it does not depend on which
automaton we use to compute the query.

We then extend these results in Section 4 to the provenance of queries on
treelike relational instances. We propose again an intrinsic definition of
provenance capturing the subinstances that satisfy the query. We then show
that, in the same way that queries can be evaluated by compiling them to an
automaton on tree encodings, we can compute a provenance circuit for the query
by compiling it to an automaton, computing a tree decomposition of the
instance, and performing the previous construction, in linear time overall in
the input instance. Our intrinsic definition of provenance ensures the
provenance only depends on the logical query, not on the choice of query plan,
of automaton, or of tree decomposition.

Our next contribution in Section 5 is to extend such definitions of provenance
from Boolean formulae to $\mathbb{N}[X]$, the _universal provenance semiring_
[green2007provenance]. This poses several challenges. First, as semirings
cannot deal satisfactorily with negation [geerts2010database,
amsterdamer2011limitations], we must restrict to _monotone_ queries, to obtain
monotone provenance circuits. Second, we must keep track of the multiplicity
of facts, as well as the multiplicity of matches. For this reason, we restrict
to unions of conjunctive queries (UCQ) in that section, as richer languages do
not directly provide notions of multiplicity for matched facts. We generalize
our notion of provenance circuits for automata to instances with unknown
multiplicity annotations, using arithmetic circuits. We show that, for UCQs,
the standard provenance for the universal semiring [green2007provenance]
matches the one defined via the automaton, and that a provenance circuit for
it can be computed in linear time for treelike instances.

Returning to the non-monotone Boolean provenance, we show in Section 6 how the
tractability of provenance computation on treelike instances implies that of
two important problems: determining the probability of a query, and counting
query matches. We show that probability evaluation of fixed MSO queries is
tractable on probabilistic XML models with local uncertainty, a result already
known in [cohen2009running], and extend it to trees with event annotations
that satisfy a condition of having bounded _scopes_. We also show that MSO
query evaluation is tractable on treelike block-independent-disjoint (BID)
relational instances [suciu2011probabilistic]. These tractability results for
provenance are achieved by applying message passing [lauritzen1988local] on
our provenance circuits. Last, we show the tractability of counting query
matches, using a reduction to the probabilistic setting, capturing a result of
[arnborg1991easy].

##  2 Preliminaries

We introduce basic notions related to trees, tree automata, and Boolean
circuits.

Given a fixed _alphabet_ $\Gamma$, we define a _$\Gamma$ -tree_
$T=(V,L,R,\lambda)$ as a set of _nodes_ $V$, two partial mappings $L,R:V\to V$
that associate an internal node with its left and right child, and a _labeling
function_ $\lambda:V\to\Gamma$. Unless stated otherwise, the trees that we
consider are rooted, directed, ordered, binary, and full (each node has either
zero or two children). We write $n\in T$ to mean $n\in V$. We say that two
trees $T_{1}$ and $T_{2}$ are _isomorphic_ if there is a bijection between
their node sets preserving children and labels (we simply write it
$T_{1}=T_{2}$); they have _same skeleton_ if they are isomorphic except for
labels.

A _bottom-up nondeterministic tree automaton_ on $\Gamma$-trees, or _$\Gamma$
-bNTA_, is a tuple $A=(Q,F,\iota,\delta)$ of a set $Q$ of _states_ , a subset
$F\subseteq Q$ of _accepting states_ , an _initial relation_
$\iota:\Gamma\rightarrow 2^{Q}$ giving possible states for leaves from their
label, and a _transition relation_ $\delta:Q^{2}\times\Gamma\rightarrow 2^{Q}$
determining possible states for internal nodes from their label and the states
of their children. A  _run_ of $A$ on a $\Gamma$-tree $T=(V,L,R,\lambda)$ is a
function $\rho:V\to Q$ such that for each leaf $n$ we have
$\rho(n)\in\iota(\lambda(n))$, and for every internal node $n$ we have
$\rho(n)\in\delta(\rho(L(n)),\rho(R(n)),\lambda(n))$. A run is _accepting_ if,
for the root $n_{\mathrm{r}}$ of $T$, $\rho(n_{\mathrm{r}})\in F$; and $A$
_accepts_ $T$ (written $T\models A$) if there is some accepting run of $A$ on
$T$. Tree automata capture usual query languages on trees, such as MSO
[thatcher1968generalized] and tree-pattern queries [Neven02].

A _Boolean circuit_ is a directed acyclic graph $C=(G,W,g_{0},\mu)$ where $G$
is a set of _gates_ , $W\subseteq G\times G$ is a set of _wires_ (edges),
$g_{0}\in G$ is a distinguished _output gate_ , and $\mu$ associates each
_gate_ $g\in G$ with a _type_ $\mu(g)$ that can be $\mathsf{inp}$ (_input
gate_ , with no incoming wire in $W$), $\neg$ (NOT-gate, with exactly one
incoming wire in $W$), $\land$ (AND-gate) or $\lor$ (OR-gate). A _valuation_
of the _input gates_ $C_{\mathsf{inp}}$ of $C$ is a function
$\nu:C_{\mathsf{inp}}\to\\{0,1\\}$; it defines inductively a unique
_evaluation_ $\nu^{\prime}:C\to\\{0,1\\}$ as follows: $\nu^{\prime}(g)$ is
$\nu(g)$ if $g\in C_{\mathsf{inp}}$ (i.e., $\mu(g)=\mathsf{inp}$); it is
$\neg\nu^{\prime}(g^{\prime})$ if $\mu(g)=\neg$ (with $(g^{\prime},g)\in W$);
otherwise it is $\bigodot_{(g^{\prime},g)\in W}\nu^{\prime}(g^{\prime})$ where
$\odot$ is $\mu(g)$ (hence, $\land$ or $\lor$). Note that this implies that
AND- and OR-gates with no inputs always evaluate to $1$ and $0$ respectively.
We will abuse notation and use valuations and evaluations interchangeably, and
we write $\nu(C)$ to mean $\nu(g_{0})$. The _function_ captured by $C$ is the
one that maps any valuation $\nu$ of $C_{\mathsf{inp}}$ to $\nu(C)$.

##  3 Provenance Circuits for Tree Automata

We start by studying a notion of provenance on trees, defined in an uncertain
tree framework. Fixing a finite alphabet $\Gamma$ throughout this section, we
view a $\Gamma$-tree $T$ as an _uncertain tree_ , where each node carries an
unknown Boolean annotation in $\\{0,1\\}$, and consider all possible
_valuations_ that choose an annotation for each node of $T$, calling
$\overline{\Gamma}$ the alphabet of annotated trees:

######  Definition 3.1.

We write $\overline{\Gamma}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\Gamma\times\\{0,1\\}$.
For any $\Gamma$-tree $T=(V,L,R,\lambda)$ and valuation $\nu:V\to\\{0,1\\}$,
$\nu(T)$ is the $\overline{\Gamma}$-tree with same skeleton where each node
$n$ is given the label $(\lambda(n),\nu(n))$.

We consider automata on _annotated_ trees, namely, $\overline{\Gamma}$-bNTAs,
and define their _provenance_ on a $\Gamma$-tree $T$ as a Boolean function
that describes which valuations of $T$ are accepted by the automaton.
Intuitively, provenance keeps track of the dependence between Boolean
annotations and acceptance or rejection of the tree.

######  Definition 3.2.

The _provenance_ of a $\overline{\Gamma}$-bNTA $A$ on a $\Gamma$-tree
$T=(V,L,R,\lambda)$ is the function $\mathrm{Prov}(A,T)$ mapping any valuation
$\nu:V\to\\{0,1\\}$ to $1$ or $0$ depending on whether $\nu(T)\models A$.

We now define a _provenance circuit_ of $A$ on a $\Gamma$-tree $T$ as a
circuit that captures the provenance of $A$ on $T$, $\mathrm{Prov}(A,T)$.
Formally:

######  Definition 3.3.

Let $A$ be a $\overline{\Gamma}$-bNTA and $T=(V,L,R,\lambda)$ be a
$\Gamma$-tree. A _provenance circuit_ of $A$ on $T$ is a Boolean circuit $C$
with $C_{\mathsf{inp}}=V$ that captures the function $\mathrm{Prov}(A,T)$.

An important result is that provenance circuits can be tractably constructed:

######  Proposition 3.1.

A provenance circuit of a $\overline{\Gamma}$-bNTA $A$ on a $\Gamma$-tree $T$
can be constructed in time $O(\left|A\right|\cdot\left|T\right|)$.

The proof is by creating one gate in $C$ per state of $A$ per node of $T$, and
writing out in $C$ all possible transitions of $A$ at each node $n$ of $T$,
depending on the input gate that indicates the annotation of $n$. In fact, we
can show that $C$ is treelike for fixed $A$; we use this in Section 6 to show
the tractability of tree automaton evaluation on probabilistic XML trees from
$\mathsf{PrXML}^{\mathsf{mux,ind}}$ [kimelfeld2013probabilistic].

It is not hard to see that this construction gives us a way to capture the
provenance of any _query_ on trees that can be expressed as an automaton, no
matter the choice of automaton. A _query_ $q$ is any logical sentence on
$\overline{\Gamma}$-trees which a $\overline{\Gamma}$-tree $T$ can _satisfy_
(written $T\models q$) or _violate_ ($T\not\models q$). An automaton $A_{q}$
_tests_ query $q$ if for any $\overline{\Gamma}$-tree $T$, we have $T\models
A_{q}$ iff $T\models q$. We define $\mathrm{Prov}(q,T)$ for a $\Gamma$-tree
$T$ as in Definition 3.2, and run circuits for queries as in Definition 3.3.
It is immediate that Proposition 3.1 implies:

######  Proposition 3.2.

For any fixed query $q$ on $\overline{\Gamma}$-trees for which we can compute
an automaton $A_{q}$ that tests it, a provenance circuit of $q$ on a
$\Gamma$-tree $T$ can be constructed in time $O(\left|T\right|)$.

Note that provenance does not depend on the automaton used to test the query.

##  4 Provenance on Tree Encodings

We lift the previous results to the setting of _relational instances_.

A _signature_ $\sigma$ is a finite set of _relation names_ (e.g., $R$) with
associated _arity_ $\mathrm{arity}(R)\geqslant 1$. Fixing a countable domain
$\mathcal{D}=\\{a_{k}\mid k\geqslant 0\\}$, a _relational instance_ $I$ over
$\sigma$ (or $\sigma$-instance) is a finite set $I$ of _ground facts_ of the
form $R(\mathbf{a})$ with $R\in\sigma$, where $\mathbf{a}$ is a tuple of
$\mathrm{arity}(R)$ elements of $\mathcal{D}$. The _active domain_
$\operatorname{dom}(I)\subseteq\mathcal{D}$ of $I$ is the finite set of
elements of $\mathcal{D}$ used in $I$. Two instances $I$ and $I^{\prime}$ are
_isomorphic_ if there is a bijection $\varphi$ from $\operatorname{dom}(I)$ to
$\operatorname{dom}(I^{\prime})$ such that $\varphi(I)=I^{\prime}$. We say
that an instance $I^{\prime}$ is a _subinstance_ 111Subinstances are not
necessarily “induced” by a subset of the domain, they can be arbitrary subsets
of facts. of $I$, written $I^{\prime}\subseteq I$, if it is a subset of the
facts of $I$, which implies
$\operatorname{dom}(I^{\prime})\subseteq\operatorname{dom}(I)$.

A _query_ $q$ is a logical formula in (function-free) first- or second-order
logic on $\sigma$, without free second-order variables; a $\sigma$-instance
$I$ can _satisfy_ it ($I\models q$) or _violate_ it ($I\not\models q$). For
simplicity, unless stated otherwise, we restrict to _Boolean queries_ , that
is, queries with no free variables, that are _constant-free_. This limitation
is inessential for _data complexity_ , namely complexity for a fixed query: we
can handle non-Boolean queries by building a provenance circuit for each
possible output result (there are polynomially many), and we encode constants
by extending the signature with fresh unary predicates for them.

As before, we consider unknown Boolean annotations on the facts of an
instance. However, rather than annotating the facts, it is more natural to say
that a fact annotated by $1$ is kept, and a fact annotated by $0$ is deleted.
Formally, given an instance $\sigma$, a _valuation_ $\nu$ is a function from
the facts of $I$ to $\\{0,1\\}$, and we define $\nu(I)$ as the subinstance
$\\{F\in I\mid\nu(F)=1\\}$ of $I$. We then define:

######  Definition 4.1.

The _provenance_ of a query $q$ on a $\sigma$-instance $I$ is the function
$\mathrm{Prov}(q,I)$ mapping any valuation $\nu:I\to\\{0,1\\}$ to $1$ or $0$
depending on whether $\nu(I)\models q$. A _provenance circuit_ of $q$ on $I$
is a Boolean circuit $C$ with $C_{\mathsf{inp}}=I$ that captures
$\mathrm{Prov}(q,I)$.

We study provenance for treelike instances (i.e., bounded-treewidth
instances), encoding queries to automata on tree encodings. Let us first
define this. The _treewidth_ $0pt(I)$ of an instance $I$ is a standard measure
[robertson1986graph] of how close $I$ is to a tree: the treewidth of a tree is
$1$, that of a cycle is $2$, and that of a $k$-clique or $k$-grid is $k-1$;
further, we have $0pt(I^{\prime})\leqslant 0pt(I)$ for any
$I^{\prime}\subseteq I$. It is known [Courcelle90, flum2002query] that for any
fixed $k\in\mathbb{N}$, there is a finite alphabet $\Gamma^{k}_{\sigma}$ such
that any $\sigma$-instance $I$ of treewidth $\leqslant k$ can be encoded in
linear time [bodlaender1996linear] to a $\Gamma^{k}_{\sigma}$-tree $T_{I}$,
called the _tree encoding_ , which can be decoded back to $I$ up to
isomorphism (i.e., up to the identity of constants). Each fact in $I$ is
encoded in a node for this fact in the tree encoding, where the node label
describes the fact.

The point of tree encodings is that queries in _monadic second-order logic_ ,
the extension of first-order logic with second-order quantification on sets,
can be encoded to automata which are then evaluated on tree encodings.
Formally:

######  Definition 4.2.

For $k\in\mathbb{N}$, we say that a $\Gamma^{k}_{\sigma}$-bNTA $A^{k}_{q}$
_tests_ a query $q$ for treewidth $k$ if, for any $\Gamma^{k}_{\sigma}$-tree
$T$, we have $T\models A^{k}_{q}$ iff $T$ decodes to an instance $I$ such that
$I\models q$.

######  Theorem 4.1 ([Courcelle90]).

For any $k\in\mathbb{N}$, for any MSO query $q$, one can compute a
$\Gamma^{k}_{\sigma}$-bNTA $A^{k}_{q}$ that tests $q$ for treewidth $\leqslant
k$.

Our results apply to any query language that can be rewritten to tree automata
under a bound on instance treewidth. Beyond MSO, this is also the case of
_guarded second-order logic_ (GSO). GSO extends first-order logic with second-
order quantification on arbitrary-arity relations, with a semantic restriction
to _guarded tuples_ (already co-occurring in some instance fact); it captures
MSO (it has the same expressive power on treelike instances [gradel2002back])
and many common database query languages, e.g., _guarded Datalog_
[Gradel:2000:EEM:1765236.1765272] or _frontier-guarded Datalog_
[baget2010walking]. We use GSO in the sequel as our choice of query language
that can be rewritten to automata. Combining the result above with the results
of the previous section, we claim that provenance for GSO queries on treelike
instances can be tractably computed, and that the resulting provenance circuit
has treewidth independent of the instance.

######  Theorem 4.2.

For any fixed $k\in\mathbb{N}$ and GSO query $q$, for any $\sigma$-instance
$I$ such that $0pt(I)\leqslant k$, one can construct a provenance circuit $C$
of $q$ on $I$ in time $O(\left|I\right|)$. The treewidth of $C$ only depends
on $k$ and $q$ (not on $I$).

The proof is by encoding the instance $I$ to its tree encoding $T_{I}$ in
linear time, and compiling the query $q$ to an automaton $A_{q}$ that tests
it, in constant time in the instance. Now, Section 3 worked with
$\overline{\Gamma^{k}_{\sigma}}$-bNTAs rather than
$\Gamma^{k}_{\sigma}$-bNTAs, but the difference is inessential: we can easily
map any $\overline{\Gamma^{k}_{\sigma}}$-tree $T$ to a
$\Gamma^{k}_{\sigma}$-tree $\epsilon(T)$ where any node label $(\tau,1)$ is
replaced by $\tau$, and any label $(\tau,0)$ is replaced by a dummy label
indicating the absence of a fact; and we straightforwardly translate $A$ to a
$\overline{\Gamma^{k}_{\sigma}}$-bNTA $A^{\prime}$ such that $T\models
A^{\prime}$ iff $\epsilon(T)\models A$ for any
$\overline{\Gamma^{k}_{\sigma}}$-tree $T$. The key point is then that, for any
valuation $\nu:T\to\\{0,1\\}$, $\epsilon(\nu(T))$ is a tree encoding of
$\nu(I)$ (defined in the expected way), so we conclude by applying Proposition
3.1 to $A^{\prime}$ and $T$. As in Section 3, our definition of provenance is
intrinsic to the query and does not depend on its formulation, on the choice
of tree decomposition, or on the choice of automaton to evaluate the query on
tree encodings.

Note that tractability holds only in data complexity. For combined complexity,
we incur the cost of compiling the query to an automaton, which is
nonelementary in general [meyer1975weak]. However, for some restricted query
classes, such as _unions of conjunctive queries_ (UCQs), the compilation phase
has lower cost.

##  5 General Semirings

In this section we connect our previous results to the existing definitions of
_semiring provenance_ on arbitrary relational instances [green2007provenance]:

######  Definition 5.1.

A _commutative semiring_ $(K,\oplus,\otimes,0_{K},1_{K})$ is a set $K$ with
binary operations $\oplus$ and $\otimes$ and distinguished elements $0_{K}$
and $1_{K}$, such that $(K,\oplus)$ and $(K,\otimes)$ are commutative monoids
with identity element $0_{K}$ and $1_{K}$, $\otimes$ distributes over
$\oplus$, and $0_{K}\otimes a=0_{K}$ for all $a\in K$.

Provenance for semiring $K$ is defined on instances where each fact is
annotated with an element of $K$. The provenance of a query on such an
instance is an element of $K$ obtained by combining fact annotations following
the semantics of the query, intuitively describing how the query output
depends on the annotations (see exact definitions in [green2007provenance]).
This general setting has many specific applications:

######  Example 5.1.

For any variable set $X$, the monotone Boolean functions over $X$ form a
semiring $(\mathrm{PosBool}[X],\lor,\land,0,1)$. We write them as
propositional formulae, but two equivalent formulae (e.g., $x\vee x$ and $x$)
denote the same $\mathrm{PosBool}[X]$ object. On instances where each fact is
annotated by its own variable in $X$, the $\mathrm{PosBool}[X]$-provenance of
a query $q$ is a monotone Boolean function on $X$ describing which
subinstances satisfy $q$. As we will see, this is what we defined in Section
4, using circuits as compact representations.

The _natural numbers_ $\mathbb{N}$ with the usual $+$ and $\times$ form a
semiring. On instances where facts are annotated with an element of
$\mathbb{N}$ representing a multiplicity, the provenance of a query describes
its number of matches under the bag semantics.

The _security semiring_ [foster2008annotated] $\mathbb{S}$ is defined on the
ordered set $1_{\mathbb{S}}<C<S<T<0_{\mathbb{S}}$ (respectively: _always
available_ , _confidential_ , _secret_ , _top secret_ , _never available_) as
$(\\{1,C,S,T,0\\},\min,\max,0,1)$. The provenance of a query for $\mathbb{S}$
denotes the minimal level of security clearance required to see that it holds.
The _fuzzy semiring_ [amsterdamer2011limitations] is $([0,1],\max,\min,0,1)$.
The provenance of a query for this semiring is the minimal fuzziness value
that has to be tolerated for facts so that the query is satisfied.

The _tropical semiring_ [deutch2014circuits] is
$(\mathbb{N}\sqcup\\{\infty\\},\min,+,\infty,0)$. Fact annotations are costs,
and the tropical provenance of a query is the minimal cost of the facts
required to satisfy it, with multiple uses of a fact being charged multiple
times.

For any set of variables $X$, the _polynomial semiring_ $\mathbb{N}[X]$ is the
semiring of polynomials with variables in $X$ and coefficients in
$\mathbb{N}$, with the usual sum and product over polynomials, and with
$0,1\in\mathbb{N}$.

Semiring provenance does not support negation well [geerts2010database,
amsterdamer2011limitations] and is therefore only defined for _monotone_
queries: a query $q$ is _monotone_ if, for any instances $I\subseteq
I^{\prime}$, if $I\models q$ then $I^{\prime}\models q$. Provenance circuits
for semiring provenance are _monotone_ circuits [deutch2014circuits]: they do
not feature NOT-gates. We can show that, adapting the constructions of Section
3 to work with a notion of _monotone_ bNTAs, Theorem 4.2 applied to monotone
queries yields a _monotone_ provenance circuit:

######  Theorem 5.1.

For any fixed $k\in\mathbb{N}$ and monotone GSO query $q$, for any
$\sigma$-instance $I$ such that $0pt(I)\leqslant k$, one can construct in time
$O(\left|I\right|)$ a monotone provenance circuit of $q$ on $I$ whose
treewidth only depends on $k$ and $q$ (not on $I$).

Hence, for monotone GSO queries for which [green2007provenance] defines a
notion of semiring provenance (e.g., those that can be encoded to _Datalog_ ,
a recursive query language that subsumes UCQs), our provenance
$\mathrm{Prov}(q,I)$ is easily seen to match the provenance of
[green2007provenance], specialized to the semiring $\mathrm{PosBool}[X]$ of
monotone Boolean functions. Indeed, both provenances obey the same intrinsic
definition: they are the function that maps to $1$ exactly the valuations
corresponding to subinstances accepted by the query. Hence, we can understand
Theorem 5.1 as a tractability result for $\mathrm{PosBool}[X]$-provenance
(represented as a circuit) on treelike instances.

Of course, the definitions of [green2007provenance] go beyond
$\mathrm{PosBool}[X]$ and extend to arbitrary commutative semirings. We now
turn to this more general question.

####  $\mathbb{N}[X]$-provenance for UCQs.

First, we note that, as shown by [green2007provenance], the provenance of
Datalog queries for _any_ semiring $K$ can be computed in the semiring
$\mathbb{N}[X]$, on instances where each fact is annotated by its own variable
in $X$. Indeed, the provenance can then be _specialized_ to $K$, and the
actual fact annotations in $K$, once known, can be used to replace the
variables in the result, thanks to a _commutation with homomorphisms_
property. Hence, _we restrict to $\mathbb{N}[X]$-provenance_ and to instances
of this form, which covers all the examples above.

Second, in our setting of treelike instances, we evaluate queries using tree
automata, which are compiled from logical formulae with no prescribed
execution plan. For the semiring $\mathbb{N}[X]$, this is hard to connect to
the general definitions of provenance in [green2007provenance], which are
mainly designed for positive relational algebra operators or Datalog queries.
Hence, to generalize our constructions to $\mathbb{N}[X]$-provenance, _we now
restrict our query language to UCQs_ , assuming without loss of generality
that they contain no equality atoms, We comment at the end of this section on
the difficulties arising for richer query languages.

We formally define the _$\mathbb{N}[X]$ -provenance_ of UCQs on relational
instances by encoding them straightforwardly to Datalog and using the Datalog
provenance definition of [green2007provenance]. The resulting provenance can
be rephrased as follows:

######  Definition 5.2.

The _$\mathbb{N}[X]$ -provenance_ of a UCQ
$q=\bigvee_{i=1}^{n}\exists\mathbf{x}_{i}\,q_{i}(\mathbf{x}_{i})$ (where
$q_{i}$ is a conjunction of atoms with free variables $\mathbf{x}_{i}$) on an
instance $I$ is defined as:
$\mathrm{Prov}_{\mathbb{N}[X]}(q,I)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigoplus_{i=1}^{n}\bigoplus_{\begin{subarray}{c}f:\mathbf{x}_{i}\to\operatorname{dom}(I)\mathrm{~{}such~{}that~{}}I\models
q_{i}(f(\mathbf{x}_{i}))\end{subarray}}\bigotimes_{A(\mathbf{x}_{i})\in
q_{i}}A(f(\mathbf{x}_{i}))$.
In other words, we sum over each disjunct, and over each match of the
disjunct; for each match, we take the product, over the atoms of the disjunct,
of their image fact in $I$, identifying each fact to the one variable in $X$
that annotates it.

We know that $\mathrm{Prov}_{\mathbb{N}[X]}(q,I)$ enjoys all the usual
properties of provenance: it can be specialized to $\mathrm{PosBool}[X]$,
yielding back the previous definition; it can be evaluated in the $\mathbb{N}$
semiring to count the number of matches of a query; etc.

######  Example 5.2.

Consider the instance $I=\\{F_{1}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=R(a,a),\allowbreak
F_{2}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=R(b,c),\allowbreak
F_{3}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=R(c,b)\\}$
and the CQ $q:\exists xy\,R(x,y)R(y,x)$. We have
$\mathrm{Prov}_{\mathbb{N}[X]}(q,I)=F_{1}^{2}+2F_{2}F_{3}$ and
$\mathrm{Prov}(q,I)=F_{1}\vee(F_{2}\wedge F_{3})$. Unlike
$\mathrm{PosBool}[X]$-provenance, $\mathbb{N}[X]$-provenance can describe that
multiple atoms of the query map to the same fact, and that the same
subinstance is obtained with two different query matches. Evaluating in the
semiring $\mathbb{N}$ with facts annotated by $1$, $q$ has $1^{2}+2\times
1\times 1=3$ matches.

#### Provenance circuits for trees.

Guided by this definition of $\mathbb{N}[X]$-provenance, we generalize the
construction of Section 3 of provenance on trees to a more expressive
provenance construction, before we extend it to treelike instances as in
Section 4.

Instead of considering $\overline{\Gamma}$-trees, we consider
$\overline{\Gamma}^{p}$-trees for $p\in\mathbb{N}$, whose label set is
$\Gamma\times\\{0,\ldots,p\\}$ rather than $\Gamma\times\\{0,1\\}$.
Intuitively, rather than uncertainty about whether facts are present or
missing, we represent uncertainty about the _number of available copies_ of
facts, as UCQ matches may include the same fact multiple times. We impose on
$\overline{\Gamma}$ the partial order $<$ defined by $(\tau,i)<(\tau,j)$ for
all $\tau\in\Gamma$ and $i<j$ in $\\{0,\ldots,p\\}$, and call a
$\overline{\Gamma}^{p}$-bNTA $A=(Q,F,\iota,\delta)$ _monotone_ if for every
$\tau<\tau^{\prime}$ in $\overline{\Gamma}^{p}$, we have
$\iota(\tau)\subseteq\iota(\tau^{\prime})$ and
$\delta(q_{1},q_{2},\tau)\subseteq\delta(q_{1},q_{2},\tau^{\prime})$ for every
$q_{1},q_{2}\in Q$. We write $\mathrm{Val}^{p}(T)$ for the set of all _$p$
-valuations_ $\nu:V\to\\{0,\ldots,p\\}$ of a $\Gamma$-tree $T$. We write
$\left|\mathrm{aruns}(A,T)\right|$ for a $\overline{\Gamma}^{p}$-tree $T$ and
$\overline{\Gamma}^{p}$-bNTA $A$ to denote the number of accepting runs of $A$
on $T$. We can now define:

######  Definition 5.3.

The _$\mathbb{N}[X]$ -provenance_ of a $\overline{\Gamma}^{p}$-bNTA $A$ on a
$\Gamma$-tree $T$ is
$\mathrm{Prov}_{\mathbb{N}[X]}(A,T)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigoplus_{\nu\in\mathrm{Val}^{p}(T)}\left|\mathrm{aruns}(A,\nu(T))\right|\bigotimes_{n\in
T}n^{\nu(n)}$
where each node $n\in T$ is identified with its own variable in $X$.
Intuitively, we sum over all valuations $\nu$ of $T$ to $\\{0,\ldots,p\\}$,
and take the product of the tree nodes to the power of their valuation in
$\nu$, with the number of accepting runs of $A$ on $\nu(T)$ as coefficient; in
particular, the term for $\nu$ is $0$ if $A$ rejects $\nu(T)$.

This definition specializes in $\mathrm{PosBool}[X]$ to our earlier definition
of $\mathrm{Prov}(A,T)$, but extends it with the two features of
$\mathbb{N}[X]$: multiple copies of the same nodes (represented as
$n^{\nu(n)}$) and multiple derivations (represented as
$\left|\mathrm{aruns}(A,\nu(T))\right|$). To construct this general
provenance, we need _arithmetic circuits_ :

######  Definition 5.4.

A _$K$ -circuit_ for semiring $(K,\oplus,\otimes,0_{K},1_{K})$ is a circuit
with $\oplus$\- and $\otimes$-gates instead of OR- and AND-gates (and no
analogue of NOT-gates), whose input gates stand for elements of $K$. As
before, the constants $0_{K}$ and $1_{K}$ can be written as $\oplus$\- and
$\otimes$-gates with no inputs. The element of $K$ _captured_ by a $K$-circuit
is the element captured by its distinguished gate, under the recursive
definition that $\oplus$\- and $\otimes$-gates capture the sum and product of
the elements captured by their operands, and input gates capture their own
value.

We now show an efficient construction for such provenance circuits,
generalizing the monotone analogue of Proposition 3.1. The proof technique is
to replace AND- and OR-gates by $\otimes$\- and $\oplus$-gates, and to
consider possible annotations in $\\{0,\ldots,p\\}$ instead of $\\{0,1\\}$.
The correctness is proved by induction via a general identity relating the
provenance on a tree to that of its left and right subtrees.

######  Theorem 5.2.

For any fixed $p\in\mathbb{N}$, for a $\overline{\Gamma}^{p}$-bNTA $A$ and a
$\Gamma$-tree $T$, a $\mathbb{N}[X]$-circuit capturing
$\mathrm{Prov}_{\mathbb{N}[X]}(A,T)$ can be constructed in time
$O(\left|A\right|\cdot\left|T\right|)$.

#### Provenance circuit for instances.

Moving back to provenance for UCQs on bounded-treewidth instances, we obtain a
linear-time provenance construction:

######  Theorem 5.3.

For any fixed $k\in\mathbb{N}$ and UCQ $q$, for any $\sigma$-instance $I$ such
that $0pt(I)\leqslant k$, one can construct a $\mathbb{N}[X]$-circuit that
captures $\mathrm{Prov}_{\mathbb{N}[X]}(q,I)$ in time $O(\left|I\right|)$.

The proof technique is to construct for each disjunct $q^{\prime}$ of $q$ a
$\overline{\Gamma}^{p}$-bNTA $A_{q^{\prime}}$, where $\Gamma\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\Gamma^{k}_{\sigma}$
is the alphabet for tree encodings of width $k$, and $p$ is the maximum number
of atoms in a disjunct of $q$. We want $A_{q^{\prime}}$ to test $q^{\prime}$
on tree encodings over $\Gamma$, _while preserving multiplicities_ : this is
done by enumerating all possible self-homomorphisms of $q^{\prime}$, changing
$\sigma$ to make the multiplicity of atoms part of the relation name, encoding
the resulting queries to automata as usual [Courcelle90] and going back to the
original $\sigma$. We then apply a variant of Theorem 5.2 to construct a
$\mathbb{N}[X]$-circuit capturing the provenance of $A_{q^{\prime}}$ on a tree
encoding of $I$ but for valuations that sum to the number of atoms of
$q^{\prime}$; this restricts to bag-subinstances corresponding exactly to
matches of $q^{\prime}$. We obtain a $\mathbb{N}[X]$-circuit that captures
$\mathrm{Prov}_{\mathbb{N}[X]}(q,I)$ by combining the circuits for each
disjunct, the distinguished gate of the overall circuit being a $\oplus$-gate
of that of each circuit.

Remember that an $\mathbb{N}[X]$-circuit can then be specialized to a circuit
for an arbitrary semiring (in particular, if the semiring has no variable, the
circuit can be used for evaluation); thus, this provides provenance for $q$ on
$I$ for any semiring.

#### Going beyond UCQs.

To compute $\mathbb{N}[X]$-provenance beyond UCQs (e.g., for monotone GSO
queries or their intersection with Datalog), the main issue is fact
multiplicity: multiple uses of facts are easy to describe for UCQs (Definition
5.2), but for more expressive languages we do not know how to define them and
connect them to automata.

In fact, we can build a query $P$, in guarded Datalog
[Gradel:2000:EEM:1765236.1765272], such that the smallest number of
occurrences of a fact in a derivation tree for $P$ cannot be bounded
independently from the instance. We thus cannot rewrite $P$ to a fixed finite
bNTA testing multiplicities on all input instances. However, as guarded
Datalog is monotone and GSO-expressible, we can compute the
$\mathrm{PosBool}[X]$-provenance of $P$ with Theorem 4.2, hinting at a
difference between $\mathrm{PosBool}[X]$ and $\mathbb{N}[X]$-provenance
computation for queries beyond UCQs.

##  6 Applications

In Section 5 we have shown a $\mathbb{N}[X]$-provenance circuit construction
for UCQs on treelike instances. This construction can be specialized to any
provenance semiring, yielding various applications: counting query results by
evaluating in $\mathbb{N}$, computing the cost of a query in the tropical
semiring, etc. By contrast, Section 4 presented a provenance construction for
arbitrary GSO queries, but only for a Boolean representation of provenance,
which does not capture multiplicities of facts or derivations. The results of
both sections are thus incomparable. In this section we show applications of
our constructions to two important problems: _probability evaluation_ ,
determining the probability that a query holds on an uncertain instance, and
_counting_ , counting the number of answers to a given query. These results
are consequences of the construction of Section 4.

#### Probabilistic XML.

We start with the problem of probabilistic query evaluation, beginning with
the setting of _trees_. We use the framework of _probabilistic XML_ , denoted
$\mathsf{PrXML}^{\mathsf{fie}}$, to represent probabilistic trees as trees
annotated by propositional formulas over independent probabilistic events (see
[kimelfeld2013probabilistic] for the formal definitions), and consider the
_data complexity_ of the _query evaluation_ problem for a MSO query $q$ on
such trees (i.e., computing the probability that $q$ holds).

This problem is intractable in general, which is not surprising: it is harder
than determining the probability of a single propositional annotation.
However, for the less expressive _local_ $\mathsf{PrXML}$ model,
$\mathsf{PrXML}^{\mathsf{mux,ind}}$, query evaluation has tractable data
complexity [cohen2009running]; this model restricts edges to be annotated by
only one event literal that is only used on that edge (plus a form of mutual
exclusivity).

We can use the provenance circuits of Section 4 to justify that query
evaluation is tractable for $\mathsf{PrXML}^{\mathsf{mux,ind}}$ and capture
the data complexity tractability result of [cohen2009running]. We say that an
algorithm runs in _ra-linear time_ if it runs in linear time assuming that
arithmetic operations over rational numbers take constant time and rationals
are stored in constant space, and runs in polynomial time without this
assumption. We can show:

######  Theorem 6.1 ([cohen2009running]).

MSO query evaluation on $\mathsf{PrXML}^{\mathsf{mux,ind}}$ has ra-linear data
complexity.

We can also show extensions of this result. For instance, on
$\mathsf{PrXML}^{\mathsf{fie}}$, defining the _scope_ of event $e$ in a
document $D$ as the smallest subtree in the left-child-right-sibling encoding
of $D$ covering nodes whose parent edge mentions $e$, and the _scope size_ of
a node $n$ as the number of events with $n$ in their scope, we show:

######  Proposition 6.1.

For any fixed $k\in\mathbb{N}$, MSO query evaluation on
$\mathsf{PrXML}^{\mathsf{fie}}$ documents with scopes assumed to have size
$\leqslant k$ has ra-linear data complexity.

#### BID instances.

We move from trees to relational instances, and show another bounded-width
tractability result for _block-independent disjoint_ (BID) instances (see
[suciu2011probabilistic], or [barbara1992management, re2007materialized] for
formal definitions). We define the _treewidth_ of a BID instance as that of
its underlying relational instance, and claim the following (remember that
query evaluation on a probabilistic instance means determining the probability
that the query holds):

######  Theorem 6.2.

For any fixed $k\in\mathbb{N}$, MSO query evaluation on an input BID instance
of treewidth $\leqslant k$ has ra-linear data complexity.

This implies the same claim for tuple-independent databases
[dalvi2007efficient, lakshmanan1997probview].

All probabilistic results are proven by rewriting to a formalism of relational
instances with a circuit annotation, such that instance and circuit have a
bounded-width joint decomposition. We compute a treelike provenance circuit
for the instance using Theorem 4.2, combine it with the annotation circuit,
and apply existing message passing techniques [lauritzen1988local] to compute
the probability of the circuit.

#### Counting.

We turn to the problem of counting query results, and reduce it in ra-linear
time to query evaluation on treelike instances, capturing a result of
[arnborg1991easy]:

######  Theorem 6.3 ([arnborg1991easy]).

For any fixed MSO query $q(\mathbf{x})$ with free first-order variables and
$k\in\mathbb{N}$, the number of matching assignments to $\mathbf{x}$ on an
input instance $I$ of width $\leqslant k$ can be computed in ra-linear data
complexity.

##  7 Related Work

#### Bounded treewidth.

From the original results [Courcelle90, flum2002query] on the linear-time data
complexity of MSO evaluation on treelike structures, works such as
[arnborg1991easy] have investigated counting problems, including applications
to probability computation (on graphs). A recent paper
[bodlaender2012probabilistic] also shows the linear-time data complexity of
evaluating an MSO query on a treelike probabilistic network (analogous to a
circuit). Such works, however, do not decouple the computation of a treelike
_provenance_ of the query and the _application_ of probabilistic inference on
this provenance, as we do. We also note results from another approach
[pichler2010counting] on treelike structures, based on monadic Datalog (and
not on MSO as the other works), that are limited to counting.

#### Probabilistic databases.

The _intensional_ approach [suciu2011probabilistic] to query evaluation on
probabilistic databases is to compute a lineage of the query and evaluate its
probability via general purpose methods; tree-like lineages allow for
tractable probabilistic query evaluation [jha2012tractability]. Many works in
this field provide sufficient conditions for lineage tractability, only a few
based on the data [sen2010read, roy2011faster] but most based on the query
[dalvi2007efficient, jha2012tractability]. For treelike instances, as we show,
we can _always_ compute treelike lineages, and we can do so for expressive
queries (beyond UCQs considered in these works), or alternatively generalize
Boolean lineages to connect them to more expressive semirings.

#### Provenance.

Our provenance study is inspired by the usual definitions of semiring
provenance for the relational algebra and Datalog [green2007provenance].
Another notion of provenance, for XQuery queries on trees, has been introduced
in [foster2008annotated]. Both [green2007provenance] and [foster2008annotated]
provide _operational_ definitions of provenance, which cannot be directly
connected to tree automata. A different relevant work on provenance is
[deutch2014circuits], which introduces provenance circuits, but uses them for
Datalog and only on _absorptive_ semirings. Last, other works study provenance
for _transducers_ [bojanczyk2014transducers], but with no clear connections to
semiring provenance or provenance for Boolean queries.

##  8 Conclusion

We have shown that two provenance constructions can be computed in linear time
on trees and treelike instances: one for UCQs on arbitrary semirings, the
other for arbitrary GSO queries as non-monotone Boolean expressions. A
drawback of our results is their high combined complexity, as they rely on
non-elementary encoding of the query to an automaton. One approach to fix this
is monadic Datalog [gottlob2010monadic, pichler2010counting]; this requires
defining and computing provenance in this setting.

#### Acknowledgements.

This work was partly supported by a financial contribution from the Fondation
Campus Paris-Saclay and the French ANR Aggreg project.

## References

_relax_relax

##  A Proofs for Section 3 (Provenance Circuits for Tree Automata)

relaxpropositionrp[3.1]relaxrelaxpropositionrp Throughout the appendix, we
will call _0-gates_ (resp.  _1-gates_) OR-gates (resp. AND-gates) with no
inputs; they always evaluate to $0$ (resp. to $1$).

We first prove this result in the specific case of a _monotone_
$\overline{\Gamma}$-bNTA $A$ (see Definition C.4), showing the same result but
for provenance circuits which are taken to be _monotone_ Boolean circuits
(i.e., they do not feature NOT-gates).

######  Proposition A.1.

A monotone provenance circuit $C$ of a monotone $\overline{\Gamma}$-bNTA $A$
on a $\Gamma$-tree $T$ can be constructed in time
$O(\left|A\right|\cdot\left|T\right|)$.

ix $T=(V,L,R,\lambda)$, $A=(Q,F,\iota,\delta)$, and construct the provenance
circuit $C=(G,W,g_{0},\mu)$. For each node $n$ of $T$, create one input gate
$g^{\mathrm{i}}_{n}$ in $C$ (which we identify to $n$, so that we have
$C_{\mathsf{inp}}=V$), and create one gate $g^{q}_{n}$ for every $q\in Q$. If
$n$ is a leaf node, for $q\in Q$, set $g^{q}_{n}$ to be:

  * •

if $q\in\iota(\lambda(n),0)$, a $1$-gate;

  * •

if $q\in\iota(\lambda(n),1)$ but $q\notin\iota(\lambda(n),0)$, an OR-gate with
sole input $g^{\mathrm{i}}_{n}$;

  * •

if $q\notin\iota(\lambda(n),1)$, a $0$-gate.

If $n$ is an internal node, create gates $g^{q_{\text{L}},q_{\text{R}}}_{n}$
and $g^{q_{\text{L}},q_{\text{R}},\mathrm{i}}_{n}$ for every pair
$q_{\text{L}},q_{\text{R}}\in Q$ (that appears as input states of a transition
of $\delta$), the first one being an AND-gate of $g^{q_{\text{L}}}_{L(n)}$ and
$g^{q_{\text{R}}}_{R(n)}$, the second one being an AND-gate of
$g^{q_{\text{L}},q_{\text{R}}}_{n}$ and of $g^{\mathrm{i}}_{n}$. Now, for
$q\in Q$, set $g^{q}_{n}$ to be an OR-gate of all the
$g^{q_{\text{L}},q_{\text{R}}}_{n}$ such that
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),0))$ and of all the
$g^{q_{\text{L}},q_{\text{R}},\mathrm{i}}_{n}$ such that
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),1))$.

Add gate $g_{0}$ to be an OR-gate of all the $g^{q}_{r}$ such that $q\in F$,
where $r$ is the root of $T$.

This construction is in time $O(\left|A\right|\cdot\left|T\right|)$: more
precisely, for every node of the tree $T$, we create a number of states that
is linear in the number of states in $Q$ and in the number of transitions of
$\delta$.

Now we show that $C$ is indeed a provenance circuit of $A$ on $T$. Let
$\nu:V\to\\{0,1\\}$ be a valuation that we extend to an evaluation of $C$. We
show by induction on $n\in T$ that for any $q\in Q$, we have
$\nu(g^{q}_{n})=1$ iff, letting $T_{n}$ be the subtree of $T$ rooted at $n$,
there is a run $\rho$ of $A$ on $T_{n}$ such that $\rho(n)=q$.

For a leaf node $n$, choosing $q\in Q$, if $\nu(n)=0$ then $\nu(g^{q}_{n})=1$
iff $q\in\iota(\lambda(n),0)$, and if $\nu(n)=1$ then $\nu(g^{q}_{n})=1$ iff
$q\in\iota(\lambda(n),1)$, so in both cases we can define a run $\rho$ as
$\rho(n)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=q$.
Conversely, the existence of a run clearly ensures that $\nu(g^{q}_{n})=1$.

For an internal node $n$, choosing $q\in Q$, if $\nu(n)=0$ then
$\nu(g^{q}_{n})=1$ iff there are some $q_{\text{L}},q_{\text{R}}\in Q$ such
that $q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),0))$,
$\nu(g^{q_{\text{L}}}_{\text{L}(n)})=1$, and
$\nu(g^{q_{\text{R}}}_{\text{R}(n)})=1$. By induction hypothesis this implies
the existence of a run $\rho_{\text{L}}$ of $A$ on $T_{L(n)}$ such that
$\rho_{\text{L}}(\text{L}(n))=q_{\text{L}}$ and a run $\rho_{\text{R}}$ of $A$
on $T_{R(n)}$ such that $\rho_{\text{R}}(\text{R}(n))=q_{\text{R}}$, from
which we construct a run $\rho$ of $A$ on $T_{n}$ such that $\rho(n)=q$, by
setting $\rho(n)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=q$
and setting $\rho(n^{\prime})$ either to $\rho_{\text{L}}(n^{\prime})$ or to
$\rho_{\text{R}}(n^{\prime})$ depending on whether $n^{\prime}\in T_{L(n)}$ or
$n^{\prime}\in T_{R(n)}$. Conversely, the existence of such a run $\rho$
implies the existence of two such runs $\rho_{\text{L}}$ and
$\rho_{\text{R}}$, from which we deduce that $\nu(g^{q}_{n})=1$.

If $\nu(n)=1$ then $\nu(g^{q}_{n})=1$ iff there are some
$q_{\text{L}},q_{\text{R}}\in Q$ such that
$\nu(g^{q_{\text{L}}}_{\text{L}(n)})=1$,
$\nu(g^{q_{\text{R}}}_{\text{R}(n)})=1$, and either
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),0))$ or
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),1))$. By monotonicity of
$A$, this is equivalent to
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),1))$. The rest is analogous
to the previous case.

The claim proven by induction clearly justifies that $C$ is a provenance
circuit, as, applying it to the root of $T$, we deduce that, for any valuation
$\nu$, we have $\nu(C)=1$ iff there is an accepting run of $A$ on $\nu(T)$.

We now generalize this result to automata and provenance circuits which are
not necessarily monotone. relaxoldproof We adapt the construction of
Proposition A.1. The only difference is that we add, for every node $n\in T$,
a gate $g^{\neg\mathrm{i}}_{n}$ which is a NOT-gate of $g^{\mathrm{i}}$, and
we modify the definition of the following nodes:

  * •

for leaf nodes $n$, for any state $q$, we set $g^{q}_{n}$ to be an OR-gate of
$g^{\mathrm{i}}$ if $q\in\iota(\lambda(n),1)$ (and a 0-gate otherwise), and
$g^{\neg\mathrm{i}}$ if $q\in\iota(\lambda(n),0)$ (and a 0-gate otherwise).

  * •

for internal nodes $n$, for every pair $q_{\text{L}},q_{\text{R}}\in Q$ that
appears as input states of a transition of $\delta$, create a gate
$g^{q_{\text{L}},q_{\text{R}},\neg\mathrm{i}}_{n}$ which is an AND-gate of
$g^{q_{\text{L}},q_{\text{R}}}_{n}$ and of $g^{\neg\mathrm{i}}_{n}$. Now, for
any state $q$, we set $g^{q}_{n}$ as before except that we use
$g^{q_{\text{L}},q_{\text{R}}}_{n}$ instead of
$g^{q_{\text{L}},q_{\text{R}},\neg\mathrm{i}}_{n}$.

We show correctness as before, showing by induction on $n\in T$ that for any
$q\in Q$, $\nu(g^{q}_{n})=1$ iff $A_{q}$ accepts $T_{n}$, where $A_{q}$ is
obtained from $A$ by letting $q$ be the only final state. The property is
clearly true on leaf nodes, and at internal nodes, if $\nu(n)=0$ we have
$\nu(g^{q}_{n})=1$ iff there exist $q_{\text{L}},q_{\text{R}}\in Q$ such that
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),0))$,
$\nu(g^{q_{\text{L}}}_{\text{L}(n)})=1$, which by induction hypothesis implies
the existence of sub-runs on $T_{L(n)}$ and $T_{R(n)}$ that we combine as
before. If $\nu(n)=0$ we have $\nu(g^{q}_{n})=1$ iff there exist
$q_{\text{L}},q_{\text{R}}\in Q$ such that
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),1))$ (this time we cannot
have $q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),0))$) so we conclude in
the same way. We conclude by justifying that $g_{0}$ is correctly defined, as
before. relaxoldproof

##  B Proofs for Section 4 (Provenance on Tree Encodings)

###  B.1 Formal preliminaries

We start by giving the omitted formal definitions:

######  Definition B.1.

A _tree decomposition_ of an instance $I$ is a $\mathcal{T}$-tree
$T=(B,L,R,\operatorname{dom})$ where $\mathcal{T}$ is the set of subsets of
$\operatorname{dom}(I)$. The nodes of $T$ are called _bags_ and their label is
written $\operatorname{dom}(b)$. We require:

  1. 1.

for every $a\in\operatorname{dom}(I)$, letting $B_{a}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\\{b\in
B\mid a\in\operatorname{dom}(b)\\}$, for every two bags $b_{1},b_{2}\in
B_{a}$, all bags on the (unique) undirected path from $b_{1}$ to $b_{2}$ are
also in $B_{a}$;

  2. 2.

for every fact $R(\mathbf{a})$ of $I$, there exists a bag $b_{\mathbf{a}}\in
B$ such that $\mathbf{a}\subseteq\operatorname{dom}(b_{\mathbf{a}})$.

The _width_ of $T$ is $0pt(T)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=k-1$
where $k\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\max_{b\in
T}\left|\operatorname{dom}(b)\right|$. The _treewidth_ (or _width_) of an
instance $I$, written $0pt(I)$, is the minimal width $0pt(T)$ of a tree
decomposition $T$ of $I$.

It is NP-hard, given an instance $I$, to determine $0pt(I)$. However, given a
fixed width $k$, one can compute in linear time in $I$ a tree decomposition of
width $\leqslant k$ of $I$ if one exists [bodlaender1996linear].

To represent bounded-treewidth instances as trees on a finite alphabet, we
introduce the notion of _tree encodings_. The representation is up to
isomorphism, i.e., it loses the identity of constants. Our finite alphabet
$\Gamma^{k}_{\sigma}$ is the set of possible facts on an instance of width
fixed to $k$; following the definition of proof trees in
[chaudhuri1992equivalence] we use element co-occurrences between one node and
its parent in the tree as a way to encode element reuse. Formally, we take
$\Gamma^{k}_{\sigma}$ to be the set defined as follows:

######  Definition B.2.

The set of _$k$ -facts_ of the signature $\sigma$, written
$\Gamma^{k}_{\sigma}$, is the set of pairs $\tau=(d,s)$ where:

  * •

the _domain_ $d$ is a subset of size at most $k+1$ of the first $2k+2$
elements of the countable domain $\mathcal{D}$, $a_{1},\ldots,a_{2k+2}$;

  * •

the _structure_ $s$ is a zero- or single-fact structure over $\sigma$ such
that $\operatorname{dom}(s)\subseteq d$.

A tree encoding is just a $\Gamma^{k}_{\sigma}$-tree. We first explain how
such a tree encoding $E$ can be decoded to a structure $I=\left\langle
E\right\rangle$ (defined up to isomorphism) and a tree decomposition $T$ of
width $k$ of $I$. Process $E$ top-down. At each $(d,s)$-labeled node of $E$
that is child of a $(d^{\prime},s^{\prime})$-labeled node, pick fresh elements
in $\mathcal{D}$ for the elements of $d\backslash d^{\prime}$ (at the root,
pick all fresh elements), add the fact of $s$ to $I$ (replacing the elements
in $d$ by the fresh elements, and by the old elements of
$\operatorname{dom}(I)$ for $d\cap d^{\prime}$), and add a bag to $T$ with the
elements of $I$ matching those in $d$. If we ever attempt to create a fact
that already exists, we abort and set $\left\langle
E\right\rangle\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bot$
(we say that $E$ is _invalid_).

We can now define tree encodings in terms of decoding:

######  Definition B.3.

We call a $\Gamma^{k}_{\sigma}$-tree $T$ a _tree encoding_ of width $k$ of a
$\sigma$-structure $I$ if $\left\langle T\right\rangle$ is isomorphic to $I$.

We note that clearly if a structure $I$ has a tree encoding of width $k$, then
$0pt(I)\leqslant k$. Further, observe that there is a clear injective function
from $\left\langle T\right\rangle$ to $T$, which maps each fact of
$\left\langle T\right\rangle$ to the node of $T$ which encoded this fact. This
function is not total, because some nodes in $T$ contain no fact (their $s$ is
a zero-fact structure).

We now justify that one can efficiently compute a tree encoding of width $k$
of $I$ from a tree decomposition of width $k$ of $I$ (this result is implicit
in [chaudhuri1992equivalence]).

######  Lemma B.1.

From a tree decomposition $T$ of width $k$ of a $\sigma$-structure $I$, one
can compute in linear time a tree encoding $E$ of width $k$ of $I$ with a
bijection from the facts of $I$ to the non-empty nodes of $E$.

he intuition is that we assign each fact $R(\mathbf{a})$ of $I$ to a bag $b\in
T$ such that $\mathbf{a}\subseteq\operatorname{dom}(b)$, which can be done in
linear time [flum2002query]. We then encode each node of $T$ as a chain of
nodes in $E$, one for each fact assigned to $T$.

Fix the $\sigma$-structure $I$ and its tree decomposition $T$ of width $k$.
Informally, we build $E$ by walking through the decomposition $T$ and copying
it by enumerating the new facts in the domain of each bag of $T$ as a chain of
nodes in $E$, picking the labels in $\Gamma^{k}_{\sigma}$ so that the elements
shared between a bag and its parent in $T$ are retained, and the new elements
are chosen so as not to overlap with the parent node. Overlaps between one
node and a non-parent or non-child node are irrelevant.

Formally, we proceed as follows. We start by precomputing a mapping that
indicates, for every tuple $\mathbf{a}$ of $I$ such that some fact
$R(\mathbf{a})$ holds in $I$, the topmost bag
$\operatorname{node}(\mathbf{a})$ of $T$ such that
$\mathbf{a}\subseteq\operatorname{dom}(\operatorname{node}(\mathbf{a}))$. This
can be performed in linear time by Lemma 3.1 of [flum2002query]. Then, we
label the tree decomposition $T$ with the facts of $I$ as follows: for each
fact $F=R(\mathbf{a})$ of $I$, we add $F$ to the label of
$\operatorname{node}(\mathbf{a})$.

Now, to encode a bag $b$ of $T$, consider $b_{\mathrm{p}}$ the parent of $b$
in $T$ and partition $\operatorname{dom}(b)=d_{\mathrm{o}}\sqcup
d_{\mathrm{n}}$ where $d_{\mathrm{o}}$ are the _old elements_ already present
in $\operatorname{dom}(b_{\mathrm{p}})$, and $d_{\mathrm{n}}$ are the _new
elements_ that did not appear in $\operatorname{dom}(b_{\mathrm{p}})$. (If $b$
is the root, then $d_{\mathrm{o}}=\emptyset$ and
$d_{\mathrm{n}}=\operatorname{dom}(b)$.) Under a specific node
$(d_{\mathrm{p}},n_{\mathrm{p}})$ in $E$, with a bijection $f_{\mathrm{p}}$
from $\operatorname{dom}(b_{\mathrm{p}})$ to $d_{\mathrm{p}}$, choose a domain
$d$ of size $\left|\operatorname{dom}(b)\right|$ over the fixed
$a_{1},\ldots,a_{2k+2}$ whose intersection with
$f_{\mathrm{p}}(\operatorname{dom}(b_{\mathrm{p}}))$ is exactly
$f_{\mathrm{p}}(d_{\mathrm{o}})$ (this is possible, as there are $2k+2$
elements to choose from and
$\left|\operatorname{dom}(b_{\mathrm{p}})\right|\leqslant k+1$) and extend the
bijection $f_{p}$ to $f$ so that it maps $\operatorname{dom}(b)$ to $d$. At
the root, choose an arbitrary bijection. Now, encode $b$ as a chain of nodes
in $E$ labeled with $(d,s_{i})$ where each $s_{i}$ encodes one of the facts in
the label of $b$ (thus defining the bijection from $I$ to the non-empty nodes
of $E$). If there are zero such facts, create a $(d,\emptyset)$ zero-fact node
instead, rather than creating no node. Recursively encode the children of $b$
(if any) in $T$, under this chain of nodes in $E$. Add zero-fact
$(\emptyset,\emptyset)$ child nodes so that each non-leaf node has exactly two
children. We assume that all arbitrary choices are done in a consistent manner
so that the process is deterministic.

Hence, when restricting to instances whose width is bounded by a constant $k$,
one can equivalently work with $\Gamma^{k}_{\sigma}$-trees which are encoding
of these instances, instead of working with the instances themselves.

We redefine properly the notion of an automaton testing a query:

######  Definition B.4.

A $\Gamma^{k}_{\sigma}$-bNTA $A$ _tests_ a Boolean query $q$ for treewidth $k$
if for any $\Gamma^{k}_{\sigma}$-tree $E$, $E\models A$ iff $\left\langle
E\right\rangle\models q$. (In particular, if $\left\langle
E\right\rangle=\bot$ then $A$ rejects $E$.)

###  B.2 Proof of Theorem 4.1

We can now state and prove the theorem that says that MSO sentences can be
tested by automata for any treewidth. The main problem is to justify that MSO
sentences can be rewritten to MSO sentences on our tree encodings, as we can
then use [thatcher1968generalized] to compile them to a bNTA. We rely on
[flum2002query] for that result, but we must translate between our tree
encodings and theirs. We do so by a general technique of justifying that
certain product trees annotated with both encodings can be recognized by a
bNTA. Let us state and prove the result: relaxtheoremrp[4.1
relaxCourcelle90]relaxrelaxtheoremrp relaxoldproof In the context of this
proof, we define a _bDTA_ (bottom-up deterministic tree automaton) as a bNTA
but where $\iota$ and $\delta$, rather than returning sets of reachable
states, return a single state. This implies that the automaton has a unique
run on any tree.

Let us fix $k\in\mathbb{N}^{*}$. We denote by $[m]$ the set $\\{1,\ldots,m\\}$
and by $n_{\sigma}$ the number of relations in $\sigma$. Lemma 4.10 of
[flum2002query] shows that for a certain finite alphabet $\Gamma(\sigma,k)$,
for any MSO formula $\varphi$ over the signature $\sigma$, there exists an MSO
formula $\varphi^{*}$ such that for any $\Gamma(\sigma,k)$-tree $t$
representing an instance $I$, $t$ satisfies $\varphi^{*}$ iff $I$ satisfies
$\varphi$. More precisely, one can define a partial
$\left\langle\cdot\right\rangle^{\prime}$ function on $\Gamma(\sigma,k)$-trees
such that for every instance $I$ of treewidth $\leqslant k$ there is a
$\Gamma(\sigma,k)$-tree $t$ such that $\left\langle T\right\rangle^{\prime}$
is well-defined and isomorphic to $I$ and for every $\Gamma(\sigma,k)$-tree
$T$, we have $T\models\varphi^{*}$ iff $\left\langle T\right\rangle^{\prime}$
is well-defined and $\left\langle T\right\rangle^{\prime}\models\varphi$.

We first describe the alphabet $\Gamma(\sigma,k)$. A letter of
$\Gamma(\sigma,k)$ is of the form
$(\gamma_{1},\allowbreak\gamma_{2},\ldots,\allowbreak\gamma_{n_{\sigma}+2})$.
The element $\gamma_{1}$ belongs to $2^{[k]^{2}}$ and describes the equalities
between the elements inside a bag; the element $\gamma_{2}$ belongs to
$2^{[k]^{2}}$ and describes the equalities between the elements from this bag
and its parents; For $i\geqslant 3$, $\gamma_{i}$ belongs to
$2^{k^{\mathrm{arity}(R_{i})}}$ and describes the tuples belonging to the
relation $R_{i}$. In the $\Gamma(\sigma,k)$-trees, the encoding of equalities
between values of the bags and its parents are described explicitly (by
$\gamma_{2}$) rather than implicitly (by element reuse between parent and
child, as in our encoding).

We next describe for which $\Gamma(\sigma,k)$ trees $T$ is their encoding
operation $\left\langle T\right\rangle^{\prime}$ well-defined, and how it is
then computed. We say that $T$ is _well-formed_ if $\left\langle
T\right\rangle^{\prime}$ is well-defined. We accordingly say that a
$\Gamma^{k}_{\sigma}$-tree $T$ is _well-formed_ if $\left\langle
T\right\rangle$ is _well-defined_ , namely, different from $\bot$.

For a $\Gamma(\sigma,k)$-tree $T$, $\left\langle T\right\rangle^{\prime}$ is
well-defined iff for each node $n$ with $\mathbf{\gamma}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\lambda(n)$
and each child $n^{\prime}\in\\{L(n),R(n)\\}$ with
$\mathbf{\gamma^{\prime}}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\lambda(n^{\prime})$:

  * •

$\gamma_{1}$ is closed by transitive closure, i.e., if $(i,j)$ and $(j,e)$
belong to $\gamma_{1}$ then $(i,e)$ belongs to $\gamma_{1}$

  * •

$\gamma_{2}$ is closed by transitive closure (to check this, we need to
consider paths, rather than the mere pair $n$ and $n^{\prime}$) $\gamma_{2}$
is closed by transitive closure.

  * •

for each $(i,j)$ in $\gamma_{1}$ and $(j,e)$ in $\gamma^{\prime}_{2}$ then
$(i,e)$ belongs to $\gamma_{2}^{\prime}$ (and symmetrically, reversing the
roles of $n$ and $n^{\prime}$)

  * •

for each pair $(j_{1},\ldots,j_{l})$ in $\gamma^{\prime}_{m}$ and if for each
$b$ $(i_{b},j_{b})$ in $\gamma_{2}^{\prime}$, then $(i_{1},\ldots,i_{l})$ is
in $\gamma_{m}$ (and vice-versa, reversing the roles of $n$ and $n^{\prime}$);
a similar condition holds with $\gamma_{1}$

Note that these conditions are clearly expressible in MSO. While
[flum2002query] does not precisely describe the behavior of $\varphi^{*}$ on
$\Gamma(\sigma,k)$-trees which are not well-formed, the above justifies our
assumption that $\varphi^{*}$ tests well-formedness and rejects the trees
which are not well-formed.

We now define $\left\langle T\right\rangle^{\prime}$ as follows, if $T$ is
well-formed. Process $E$ top-down. At each node $n\in E$ with
$\mathbf{\gamma}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\lambda(n)$
with parent node $n^{\prime}\in E$ with
$\mathbf{\gamma^{\prime}}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\lambda(n^{\prime})$,
pick fresh elements in $\mathcal{D}$ for the positions $j$ such that there is
no pair $(i,j)$ in $\gamma^{\prime}_{2}$ (at the root, pick all fresh
elements) and if $(j_{1},j_{2})$ belongs to $\gamma^{\prime}_{1}$ then the
same fresh element is assigned for the elements at both positions; if there is
such a pair, pick the existing elements used when decoding $n^{\prime}$. These
choices define a mapping $\nu$ from the positions to the fresh elements and to
existing elements. Now, for each $(j_{1},\ldots,j_{m})$ in $\gamma_{i}$, then
the fact $R_{i}(\nu(j_{1}),\ldots,\nu(j_{m}))$ is added to $I$. If we ever
attempt to create a fact that already exists, we ignore it.

We have reviewed the alphabet $\Gamma(\sigma,k)$ of [flum2002query], the
conditions for the well-definedness of $\left\langle T\right\rangle^{\prime}$
and the semantics of this operation. Now, following [thatcher1968generalized,
flum2002query], with an additional step to determinize the resulting automaton
to a bDTA, the formula $\varphi^{*}$ from [flum2002query] can be translated
into a bDTA $A_{\mathrm{theirs}}$ on $\Gamma(\sigma,k)$-trees such that for
any $\Gamma(\sigma,k)$-tree $T$, $A_{\mathrm{theirs}}$ accepts $T$ iff
$T\models\varphi^{*}$, that is, iff $\left\langle T\right\rangle^{\prime}$ is
well-defined and satisfies $\varphi$. Note that this implies that
$A_{\mathrm{theirs}}$ is encoding-invariant. We now explain how to translate
$A_{\mathrm{theirs}}$ to our desired bDTA $A_{\mathrm{ours}}$ over
$\Gamma^{k}_{\sigma}$ such that for every $\Gamma^{k}_{\sigma}$-tree $T$,
$A_{\mathrm{ours}}$ accepts $T$ iff $\left\langle
T\right\rangle\models\varphi$.

We consider the alphabet $\Sigma=\Gamma^{k}_{\sigma}\times\Gamma(\sigma,k)$,
and call $\pi_{1}$ and $\pi_{2}$ the operations on $\Sigma$-trees that map
them respectively to $\Gamma^{k}_{\sigma}$ and $\Gamma(\sigma,k)$ trees with
same skeleton by keeping the first or second component of the labels. Given a
$\Gamma^{k}_{\sigma}$-tree $T_{1}$ and a $\Gamma(\sigma,k)$-tree $T_{2}$ with
same skeleton, we will write $T_{1}\times T_{2}$ the $\Sigma$-tree obtained
from them.

We will do this by building a $\Sigma$-bDTA $A_{\mathrm{t}}$ with the
following properties:

  1. 1.

If $A_{\mathrm{t}}$ accepts $T$ then $\left\langle\pi_{1}(T)\right\rangle$ and
$\left\langle\pi_{2}(T)\right\rangle^{\prime}$ are well-defined and
isomorphic.

  2. 2.

For every $\Gamma^{k}_{\sigma}$-tree $T_{1}$ such that $\left\langle
T_{1}\right\rangle$ is well-defined, there exists a $\Gamma(\sigma,k)$-tree
$T_{2}$ such that $A_{\mathrm{t}}$ accepts $T_{1}\times T_{2}$.

Then, we can notice that from $A_{\mathrm{theirs}}$, we can build an
$\Sigma$-bDTA $A^{\prime}_{\mathrm{theirs}}$ such that $T$ is recognized by
$A^{\prime}_{\mathrm{theirs}}$ iff $\pi_{2}(T)$ is accepted by
$A^{\prime}_{\mathrm{theirs}}$, and build $A_{\mathrm{ours}}$ as the
conjunction of $A_{\mathrm{t}}$ and $A^{\prime}_{\mathrm{theirs}}$, projected
to the first component (accept a $\Gamma^{k}_{\sigma}$-tree $T_{1}$ iff there
is some $\Gamma(\sigma,k)$-tree $T_{2}$ such that $T_{1}\times T_{2}$ is
accepted, which is possible using non-determinism, and then determinizing). It
is now clear that $A_{\mathrm{ours}}$ thus defined accepts a
$\Gamma^{k}_{\sigma}$-tree $T_{1}$ iff the $\Sigma$-tree $T_{1}\times T_{2}$
is accepted, for some $\Gamma(\sigma,k)$-tree $T_{2}$, by
$A^{\prime}_{\mathrm{theirs}}$ and $A_{\mathrm{t}}$: if this happens then
$T_{2}$ is accepted by $A_{\mathrm{theirs}}$ and $\left\langle
T_{1}\right\rangle$ is isomorphic to $\left\langle
T_{2}\right\rangle^{\prime}$ so $\left\langle
T_{2}\right\rangle\models\varphi$; and conversely, if $\left\langle
T_{1}\right\rangle$ models $\varphi$, there is some $\Gamma(\sigma,k)$-tree
$T_{2}$ such that $A_{\mathrm{t}}$ accepts $T_{1}\times T_{2}$, and this
implies that $\left\langle T_{2}\right\rangle^{\prime}$ is isomorphic to
$\left\langle T_{1}\right\rangle$ so (as $\varphi$, being a constant-free MSO
query, is invariant under isomorphisms) $\left\langle T_{2}\right\rangle$
satisfies $\varphi^{*}$ and $A^{\prime}_{\mathrm{theirs}}$ accepts
$T_{1}\times T_{2}$. So it suffices to build the $\Sigma$-bDTA
$A_{\mathrm{t}}$ with the desired properties.

We now define a simple encoding from $\Gamma^{k}_{\sigma}$ to
$\Gamma(\sigma,k)$ describing what is the tree $T_{2}$, given a well-formed
tree $T_{1}$, such that $A_{\mathrm{t}}$ accepts $T_{1}\times T_{2}$. It will
then suffice to see that it is possible, with a MSO formula $\psi$, to check
on a $\Sigma$-tree $T$ whether $\pi_{2}(T)$ is the encoding of $\pi_{1}(T)$ in
this sense. Indeed, we can then compile $\psi$ to a $\Gamma$-bDTA using
[thatcher1968generalized].

Consider a node $n_{1}\in T_{1}$ and let $(d,s)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\operatorname{dom}(n)$.
We define the label of the corresponding node $n_{2}\in T_{2}$. We define
$\gamma_{1}$ so that the $k+1-\operatorname{dom}(d)$ last elements are all
equal to the $\operatorname{dom}(d)$-th element (i.e., we complete
$\operatorname{dom}(d)$ to always have $k+1$ elements, by “repeating” the last
element, where “last” is according to an arbitrary order on domain elements).
We define $\gamma_{2}$ to indicate which elements of $n_{1}$ were shared with
its parent node, completing it to be consistent with respect to $\gamma_{1}$.
Last, we define $\gamma_{3},\ldots,\gamma_{n_{\sigma}+2}$ to be the tuples of
elements in the various relations of $\sigma$ in $\left\langle
T_{1}\right\rangle$, with repetitions to be consistent according to
$\gamma_{1}$.

It is clear that this encoding maps every tree $T_{1}$ such that $\left\langle
T_{1}\right\rangle$ is well-defined to a tree $T_{2}$ such that $\left\langle
T_{2}\right\rangle$ is well-defined and isomorphic to $\left\langle
T_{1}\right\rangle$. Now, to justify the existence of $\psi$, observe that the
only non-local condition to check on $T$ is the definition of the
$\gamma_{3},\ldots,\gamma_{n_{\sigma}+2}$; but we can clearly define by an MSO
formula, for a node $n\in T$ with $(d,s)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\lambda(n)$,
the exact set of facts stated by $T$ for the elements represented by $d$
(there are only a finite number of such “types”): they are defined to check,
for all facts of the putative type, whether a node with the right fact is
reachable following an undirected path where the same elements are kept along
the path. So we can define an MSO formula checking for each node $n\in T$
whether the type of $\pi_{1}(n)$ in $\pi_{1}(T)$ in this sense matches the
graph stated in $\pi_{2}(n)$. relaxoldproof

###  B.3 Proof of Theorem 4.2

We first give the formal definition of the treewidth of a circuit, which we
omitted. To do so, we must first give a normal form for circuits:

######  Definition B.5.

Let $C=(G,W,g_{0},\mu)$ be a Boolean circuit. The _fan-in_ of a gate $g\in G$
is the number of gates $g^{\prime}\in G$, such that $(g^{\prime},g)\in W$.
Note that our definitions of circuits impose that the fan-in of input gates is
always $0$ and the fan-in of NOT-gates is always $1$. We say $C$ is _arity-
two_ if the fan-in of AND- and OR-gates is always $2$, where we allow constant
$0$\- and $1$-gates as gate types of their own (but require that such gates
have fan-in of $0$).

Clearly this restriction is inessential as circuits can be rewritten in
linear-time to an arity-two circuit by merging AND- and OR-gates with fan-in
of $1$ with their one input, replacing those with fan-in of $0$ by a 0- or
1-gate, and rewriting those with fan-in $>2$ to a chain of gates of the same
type with fan-in $2$.

We now define tree decompositions of circuits, and their relational encoding:

######  Definition B.6.

The relational signature $\sigma_{\mathrm{Circuit}}$ features one unary
relation $R^{\mathrm{i}}$ which applies to input gates, two unary relations
$R^{0}$ and $R^{1}$ which apply to constant 0- and 1-gates, one binary
relation $R^{\neg}(g_{\mathrm{o}},g_{\mathrm{i}})$ which applies to NOT-gates
(the first element is the output and the second is the input), and two ternary
relations $R^{\wedge}(g_{\mathrm{o}},g_{\mathrm{i}},g_{\mathrm{i}}^{\prime})$
and $R^{\vee}(g_{\mathrm{o}},g_{\mathrm{i}},g_{\mathrm{i}}^{\prime})$ which
apply respectively to AND- and OR-gates, with the first element being the
input and the second and third being the inputs. The _relational encoding_ of
an (arity-two non-monotone) Boolean circuit $C$ is the
$\sigma_{\mathrm{Circuit}}$-instance $I_{C}$ obtained in the expected way; we
can clearly construct $I_{C}$ from $C$ in linear time. The _treewidth_
$0pt(C)$ of $C$ is $0pt(I_{C})$ (but we talk of tree decompositions of $C$ as
shorthand).

Now, to prove the theorem, we first take care of a technical issue. Given an
instance $I$ and its tree encoding $T_{I}$, we want to construct provenance
circuits on $T_{I}$, meaning that we wish to consider Boolean-annotated
versions of $T_{I}$. However, the tree encodings of subinstances of $I$ are
not annotated versions of $T_{I}$. We need to justify that they can be taken
to have the same structure as $T_{I}$, with some facts having been removed in
nodes containing no fact.

######  Definition B.7.

For any $k$-fact $\tau=(d,s)\in\Gamma^{k}_{\sigma}$, we define the _neutered
$k$-fact_ $\underline{\tau}$ as $(d,\emptyset)$. In particular, if
$s=\emptyset$ then $\underline{\tau}=\tau$. For $\tau\in\Gamma^{k}_{\sigma}$
and $b\in\\{0,1\\}$, we write $\tau_{[b]}$ to be $\tau$ if $b$ is $1$ and
$\underline{\tau}$ if $b$ is $0$.

Given a $\overline{\Gamma^{k}_{\sigma}}$-tree $E$, we define its _evaluation_
$\epsilon(E)$ as the $\Gamma^{k}_{\sigma}$-tree that has same skeleton, where
for every node $n\in E$ with corresponding node $n^{\prime}$ in $\epsilon(E)$,
letting $\lambda(n)=(\tau,b)\in\Gamma^{k}_{\sigma}\times\\{0,1\\}$, we have
$\lambda(n^{\prime})=\tau_{[b]}$.

This definition allows us to lift $\Gamma^{k}_{\sigma}$-bNTAs, intuitively
testing a query, to $\overline{\Gamma^{k}_{\sigma}}$-bNTAs that test the same
query on Boolean-annotated tree encodings, seen via $\epsilon$ as the tree
encoding of a subinstance. Formally:

######  Lemma B.2.

For any $\Gamma^{k}_{\sigma}$-bNTA $A$, one can compute in linear time a
$\overline{\Gamma^{k}_{\sigma}}$-bNTA $A^{\prime}$ on such that $E\models
A^{\prime}$ iff $\epsilon(E)\models A$.

et $A=(Q,F,\iota,\delta)$. We construct the bNTA
$A^{\prime}=(Q,F,\iota^{\prime},\delta^{\prime})$ according to the following
definition: $\iota^{\prime}((\tau,b))\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\iota(\tau_{[b]})$
and $\delta^{\prime}((\tau,b),q_{1},q_{2})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\delta(\tau_{[b]},q_{1},q_{2})$
for all $b\in\\{0,1\\}$, $\tau\in\Gamma^{k}_{\sigma}$, and $q_{1},q_{2}\in Q$.
The process is clearly in linear time in $\left|A\right|$. Now, it is
immediate that $E\models A^{\prime}$ iff $\epsilon(E)\models A$, because a run
of $A^{\prime}$ on $E$ is a run of $A$ on $\epsilon(E)$, and vice-versa.

We are now ready to state and prove the result:
relaxtheoremrp[4.2]relaxrelaxtheoremrp relaxoldproof Fix $k\in\mathbb{N}$ and
the GSO query $q$. Using Theorem 4.1, let $A$ be a $\Gamma^{k}_{\sigma}$-bNTA
$A^{k}_{q}$ that tests $q$ for treewidth $k$ (remember that Theorem 4.1
extends from MSO to GSO because both collapse on treelike instances
[gradel2002back]). We lift $A$ to a bNTA $A^{\prime}$ on
$\overline{\Gamma^{k}_{\sigma}}$ using Lemma B.2. This is performed in
constant time in the instance.

Now, given the input instance $I$ such that $0pt(I)\leqslant k$, compute in
linear time [bodlaender1996linear] a tree decomposition of $I$, and, from
this, compute in linear time a tree encoding $E_{I}$ of $I$ using Lemma B.1.
We now use Proposition 3.1 to construct a provenance circuit $C$ of
$A^{\prime}$ on $E_{I}$. Consider now the injective function $f$ that maps the
facts of $I$ to the nodes of $E_{I}$ where those facts are encoded. We modify
$C$ to replace the input gate $g^{\mathrm{i}}_{n}$ for any $n\in E_{I}$ not in
the image of $f$, setting it to be a $1$-gate; and renaming the input gates
$g^{\mathrm{i}}_{n}$ for any $n\in E_{I}$ to be $F$, for $F$ the fact such
that $f(F)=n$. Let $C^{\prime}$ be the result of this process. $C^{\prime}$ is
thus a Boolean circuit such that $C^{\prime}_{\mathsf{inp}}=I$, and it was
computed in linear time from $I$. We claim that it captures
$\mathrm{Prov}(q,I)$.

To check that it does, let $\nu:I\to\\{0,1\\}$ be a valuation of $I$. We show
that $\nu(C^{\prime})=1$ iff $\nu(I)\models q$. To do so, the key point is to
observe that, letting $\nu^{\prime}$ be the valuation of $E_{I}$ defined by
$\nu^{\prime}(n)=\nu(F)$ if there is $F\in I$ such that $f(F)=n$, and
$\nu^{\prime}(n)=1$ otherwise, we have that $\epsilon(\nu^{\prime}(E_{I}))$ is
a tree encoding of $\nu(I)$. Indeed, $\epsilon(\nu^{\prime}(E_{I}))$ and
$E_{I}$ have same skeleton, the elements that constitute the domains of node
labels are the same, and a fact $F\in I$ is encoded in
$\epsilon(\nu^{\prime}(E_{I}))$ iff $f(F)$ is annotated by $1$ in
$\nu^{\prime}(E_{I})$ iff we have $F\in\nu(I)$. (Note that our choice to
extend $\nu^{\prime}$ by setting it to be $1$ on nodes that encode no facts
makes no difference, as the annotation of such nodes is projected to the same
label by $\epsilon$, i.e., for such labels $\tau$ in $E_{I}$, we have
$\tau_{[0]}=\tau_{[1]}$.)

Having observed this, we know that, because $A$ tests $q$, $\nu(I)\models q$
iff $\nu^{\prime}(E_{I})\models A$. Now, by definition of Lemma B.2, we have
$\epsilon(\nu^{\prime}(E_{I}))\models A$ iff $\nu^{\prime}(E_{I})\models
A^{\prime}$, which by definition of the provenance circuit $C$ is the case iff
$\nu^{\prime}(C)=1$, which by definition of $C^{\prime}$ is the case iff
$\nu(C^{\prime})=1$. Hence, $C^{\prime}$ is indeed a provenance circuit of $q$
on $I$.

The only point left to justify is that the treewidth of the circuit $C$ is
indeed bounded. Indeed, the number of gates that we create in $C$ for each
node $n$ of $E$ only depends on the automaton $A$ that tests $q$, and wires in
$C$ only go from gates for one node $n$ to gates for nodes $L(n)$ and $R(n)$,
so that the tree decomposition $T$ for $C$ is obtained by putting, in each bag
of the tree decomposition corresponding to node $n$ of $E$, the gates for node
$n$, and $L(n)$ and $R(n)$ if they exist. The additional distinguished gate
$g_{0}$ is added to the bag of the root node of $E$. This construction is
described on the circuit before translating to arity-two, but as the fan-in of
the gates of the original circuit is bounded by a constant, clearly rewriting
to arity-two preserves the property that the number of gates per bag of the
decomposition is bounded by a constant. This proves the claim. relaxoldproof

###  B.4 Proof of EXPTIME rewriting of UCQs

######  Proposition B.1 ([chaudhuri1992equivalence]).

For any UCQ $q$ and $k\in\mathbb{N}$, a $\Gamma^{k}_{\sigma}$-bNTA that tests
$q$ for treewidth $\leqslant k$ can be computed in EXPTIME in $q$ and $k$.

ucqproof

##  C Proofs for Section 5 (General Semirings)

######  Definition C.1.

A _Datalog query_ $P$ over the signature $\sigma$ consists of a signature
$\sigma_{\mathrm{int}}$ of _intensional predicates_ with a special $0$-ary
relation $\mathrm{Goal}$ and a finite set of _rules_ of the form
$R(\mathbf{x})\leftarrow R_{1}(\mathbf{y_{1}}),\ldots,R_{k}(\mathbf{y_{k}})$
where $R\in\sigma_{\mathrm{int}}$, $R_{i}\in\sigma\sqcup\sigma_{\mathrm{int}}$
for $1\leqslant i\leqslant k$, and each variable in the tuple $\mathbf{x}$
also occurs in some tuple $\mathbf{y_{i}}$. The left-hand (resp., right-hand)
side of a Datalog rule is called the _head_ (resp., _body_) of the rule.

A _proof tree_ $T$ of a Datalog query $P$ over an instance $I$ is a (non-
binary) ordered tree with nodes annotated by facts over
$\sigma\cup\sigma_{\mathrm{int}}$ on elements of $\operatorname{dom}(I)$ and
internal nodes annotated by rules, such that the fact of the root of $T$ is
$\mathrm{Goal}$, and, for every internal node $n$ in $T$ with children
$n_{1},\ldots,n_{m}$, the indicated rule
$R(\mathbf{x})\leftarrow\Psi(\mathbf{y})$ on $n$ in $P$ is such that there is
a homomorphism $h$ mapping $R(\mathbf{x})$ to the fact of $n$ and mapping
$\Psi(\mathbf{y})$ to the facts of the $n_{i}$. (Note that this definition
implies that internal nodes are necessarily annotated by a fact of
$\sigma_{\mathrm{int}}$.) We write $I\models P$ if $P$ has a proof tree on
$I$.

The _semiring provenance_ of a Datalog query on an instance is defined as
follows:

######  Definition C.2.

Given a semiring $K$ and an instance $I$ where each fact $F$ carries an
annotation $\alpha(F)\in K$, the _provenance_ of a Datalog query $P$ on $I$ is
the following [green2007provenance]:

$\bigoplus_{T\text{ proof tree of }P}\bigotimes_{n\text{ leaf of
}T}\alpha(n).$

Note that this expression may not always be defined depending on the query,
instance, and semiring. In particular, the number of terms in the sum may be
infinite, so that the result cannot necessarily be represented in the
semiring.

We now use this to define Datalog queries associated to conjunctive queries
(CQs) and unions of CQs (UCQs), which will be useful for provenance.

######  Definition C.3.

We assume that CQs and UCQs contain no equality atoms. The Datalog query
$P_{q}$ _associated_ to a CQ $q$ has only one rule, $\mathrm{Goal}\leftarrow
q$. The Datalog query $P_{q}$ associated to a UCQ $q=\bigvee_{i}q_{i}$ has
rules $\mathrm{Goal}\leftarrow q_{1}$, …, $\mathrm{Goal}\leftarrow q_{n}$.

Observe that in this case the provenance of $P_{q}$ in the sense of Definition
C.2 is always defined, no matter the semiring, as the number of possible
derivation trees is clearly finite.

relaxtheoremrp[5.1]relaxrelaxtheoremrp We first define our notion of
monotonicity for $\overline{\Gamma}$-bNTAs. Intuitively, it implies that if a
$\overline{\Gamma}$-tree is accepted by the automaton, it will not be rejected
when changing annotations from $0$ to $1$. Formally:

######  Definition C.4.

We consider the partial order $<$ on $\overline{\Gamma}$ defined by
$(\tau,0)<(\tau,1)$ for all $\tau\in\Gamma$. We say that a
$\overline{\Gamma}$-bNTA $A=(Q,F,\iota,\delta)$ is _monotone_ if for every
$\tau\leqslant\tau^{\prime}$ in $\overline{\Gamma}$, we have
$\iota(\tau)\subseteq\iota(\tau^{\prime})$ and
$\delta(q_{1},q_{2},\tau)\subseteq\delta(q_{1},q_{2},\tau^{\prime})$ for every
$q_{1},q_{2}\in Q$.

It is easy to see that the provenance of a _monotone_ $\overline{\Gamma}$-bNTA
$A$ on any tree $T$ is a _monotone_ function in the following sense: for any
valuations $\nu$ and $\nu^{\prime}$, if $\nu(g)=1$ implies $\nu^{\prime}(g)=1$
for all $g\in C_{\mathsf{inp}}$ (which we write $\nu\leqslant\nu^{\prime}$),
then $(\mathrm{Prov}(A,T))(\nu)=1$ implies
$(\mathrm{Prov}(A,T))(\nu^{\prime})=1$. Indeed, for any monotone $\Gamma$-tree
$T$ and valuations $\nu\leqslant\nu^{\prime}$, $\nu(T)\models A$ implies
$\nu^{\prime}(T)\models A$.

We already know that the results of Section 3 also hold for monotone bNTAs and
monotone provenance circuits (see Proposition A.1). Hence, if we know that the
monotone GSO sentence $q$ of interest can be tested (Definition B.4) by a
_monotone_ bNTA, i.e., if the analogue of Theorem 4.1 holds for monotone
queries and bNTAs, then clearly the reduction from treelike instances to trees
(Theorem 4.2) generalizes. We first prove an auxiliary lemma:

######  Lemma C.1.

For every $\overline{\Gamma^{k}_{\sigma}}$-trees $E$ and $E^{\prime}$, if
$E\leqslant E^{\prime}$ then
$\left\langle\epsilon(E)\right\rangle\subseteq\left\langle\epsilon(E^{\prime})\right\rangle$.

e follow the decoding process and notice that, as the domains of the
$\Gamma^{k}_{\sigma}$ node labels in $E$ and $E^{\prime}$ are the same, the
same fresh elements are used throughout, so the only difference between
$\left\langle\epsilon(E)\right\rangle$ and
$\left\langle\epsilon(E^{\prime})\right\rangle$ is about the annotation of the
created facts; and we notice that whenever $E\leqslant E^{\prime}$ then every
fact created in $E$ is also created in $E^{\prime}$.

We now prove the analogue of Theorem 4.1 for monotone queries and automata. We
immediately generalize the notion of an automaton testing a query (Definition
B.4) to $\overline{\Gamma^{k}_{\sigma}}$-bNTAs and trees, with $\left\langle
T\right\rangle$ for a $\overline{\Gamma^{k}_{\sigma}}$-tree $T$ defined as
above.

######  Lemma C.2.

Let $k\in\mathbb{N}$, $q$ be a monotone query, and $A$ be a
$\overline{\Gamma^{k}_{\sigma}}$-bNTA that tests $q$ for treewidth $k$. One
can compute in linear time from $A$ a $\overline{\Gamma^{k}_{\sigma}}$-bNTA
$A^{\prime}$ that tests $q$ for treewidth $k$ and is monotone for the partial
order on $\overline{\Gamma^{k}_{\sigma}}$.

ix $k$, $q$, and $A=(Q,F,\iota,\delta)$ the
$\overline{\Gamma^{k}_{\sigma}}$-bNTA. We build the bNTA
$A^{\prime}=(Q,F,\iota^{\prime},\delta^{\prime})$ by setting, for all
$(\tau,i)\in\overline{\Gamma^{k}_{\sigma}}$,
$\iota^{\prime}((\tau,i))\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigcup_{0\leqslant
j\leqslant i}\iota((\tau,j))$ and, for all $q_{1},q_{2}\in Q$, we pose:
$\delta^{\prime}(q_{1},q_{2},(\tau,i))\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigcup_{0\leqslant
j\leqslant i}\delta(q_{1},q_{2},(\tau,j))$.

Clearly $A^{\prime}$ is monotone by construction for
$\overline{\Gamma^{k}_{\sigma}}$. Besides, for any
$\overline{\Gamma^{k}_{\sigma}}$-tree $T$, if $A$ accepts $T$ then
$A^{\prime}$ accepts $T$, so to prove the correctness of $A^{\prime}$ it
suffices to prove the converse implication.

Let us consider such a $T$, and consider an accepting run $\rho$ of
$A^{\prime}$ on $T$. We build a new tree $T^{\prime}$ whose skeleton is that
of $T$ and where for any leaf (resp. internal node) $n^{\prime}\in T^{\prime}$
with corresponding node $n\in T$ with $\lambda(n)=(\tau,j)$, we set
$\lambda(n^{\prime})$ in $T^{\prime}$ to be $(\tau,i)$ for some $i$ such that
$\rho(n)\in\iota((\tau,i))$ (resp.
$\rho(n)\in\delta(\rho(L(n)),\rho(R(n)),(\tau,i))$), the existence of such an
$i$ being guaranteed by the definition of $\iota^{\prime}$ (resp.
$\delta^{\prime}$).

We now observe that, by construction, $\rho$ is a run of $A$ on $T^{\prime}$,
and it is still accepting, so that $T^{\prime}$ is accepted by $A$. Hence,
$\left\langle T^{\prime}\right\rangle\models q$. But now we observe that, once
again by construction, for every node $n^{\prime}$ of $T^{\prime}$ with label
$\tau^{\prime}$ and with corresponding node $n$ in $T$ with label $\tau$, it
holds that $\tau^{\prime}\leqslant\tau$. Hence we have $T^{\prime}\leqslant
T$, for which we can easily prove that $\left\langle
T^{\prime}\right\rangle\subseteq\left\langle T\right\rangle$, and thus, by
monotonicity of $q$, we must have $\left\langle T\right\rangle\models P$.
Thus, $A$ accepts $T$, proving the desired result.

From our earlier explanations, this proves Theorem 5.1.

###  C.1 $\mathbb{N}[X]$-provenance for UCQs

######  Proposition C.1.

For any UCQ $q$, $\mathrm{Prov}_{\mathbb{N}[X]}(q,I)$, is the
$\mathbb{N}[X]$-provenance in the sense of [green2007provenance] of the
associated Datalog query $P_{q}$ on $I$.

he proof trees of each CQ within $q$ have a fixed structure, the only
unspecified part being the assignment of variables. It is then clear that each
variable assignment gives a proof tree, and this mapping is injective because
all variables in the assignment occur in the proof tree. So for each CQ, we
are summing on the same thing, and each term of the sum is the leaves of the
proof tree, which is what we imposed. Further, the set of proof trees of $q$
is the union of the set of proof trees of each CQ, which means we can separate
the sum for each CQ.

###  C.2 Provenance circuits for trees

To prove Theorem 5.3, we need a generalization of $\mathbb{N}[X]$-provenance
of automata on trees. Indeed, while Definition 5.3 is natural for trees, using
it to define the provenance of queries on treelike instances would lead to a
subtle problem. The reason is that this provenance describes _all_ valuations
of the tree for which the automaton accepts (up to the maximal multiplicity
$p$), and not the _minimal_ ones. For UCQs, this would intuitively mean that
the resulting $\mathbb{N}[X]$-provenance would reflect _all_ subinstances
satisfying the query, not the minimal ones. This does not match Definition 5.2
and is undesirable: for instance, the specialization of such a provenance to
$\mathbb{N}$ would have nothing to do with the number of query matches. The
reason why this problem did not occur before is because both choices of
definition collapse in the $\mathrm{PosBool}[X]$ setting of the previous
sections; so this problem is specific to the setting of general semirings such
as $\mathbb{N}[X]$, which are not necessarily _absorptive_
[deutch2014circuits].

However, in the case of UCQs, we can introduce a generalization of Definition
5.3, for which we can show the analogue of Theorem 5.2, and that will give us
the right provenance once lifted to treelike instances as in Section 4. For a
$\Gamma$-tree $T$ and $p,l\in\mathbb{N}$, we introduce for $l\in\mathbb{N}$
the set of $p$-valuations that sum to $l$:
$\mathrm{Val}^{p}_{l}(T)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\\{\nu\in\mathrm{Val}^{p}(T)\mid\sum_{n\in
T}\nu(n)=l\\}$. We take $\mathrm{Val}^{p}_{\mathrm{all}}(T)$ to be
$\mathrm{Val}^{p}(T)$. We can now generalize Definition 5.3 as follows:

######  Definition C.5.

Let $l\in\mathbb{N}\cup\\{\mathrm{all}\\}$. The _$\mathbb{N}[X]$
-$l$-provenance_ of a $\overline{\Gamma}^{p}$-bNTA $A$ on a $\Gamma$-tree $T$
is:

$\mathrm{Prov}_{\mathbb{N}[X]}(A,T,l)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigoplus_{\nu\in\mathrm{Val}^{p}_{l}(T)}\left|\mathrm{aruns}(A,\nu(T))\right|\bigotimes_{n\in
T}n^{\nu(n)}.$

Note that
$\mathrm{Prov}_{\mathbb{N}[X]}(A,T)=\mathrm{Prov}_{\mathbb{N}[X]}(A,T,\mathrm{all})$,
so this definition indeed generalizes Definition 5.3.

We first prove the key lemma about the propagation of provenance throughout
encodings, which will be used in the inductive step of our correctness proof
of provenance circuits:

######  Lemma C.3.

For any $l,p\in\mathbb{N}$, $l\leqslant p$, for any non-singleton
$\Gamma$-tree $T=(V,L,R,\lambda)$, letting $T_{\text{L}}$ and $T_{\text{R}}$
be its left and right subtrees and $n_{\mathrm{r}}$ be its root node, for any
$\overline{\Gamma}^{p}$-bNTA $A=(Q,F,\iota,\delta)$, writing $A_{q}$ for all
$q\in Q$ the bNTA obtained from $A$ by making $q$ the only final state, we
have:

$\mathrm{Prov}_{\mathbb{N}[X]}(A,T,l)=\bigoplus_{\begin{subarray}{c}l_{1}+l_{2}+l^{\prime}=l\\\
q_{\text{L}},q_{\text{R}}\in Q\\\
q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n_{\mathrm{r}}),l^{\prime}))\\\
\end{subarray}}\mathrm{Prov}_{\mathbb{N}[X]}(A_{q_{\text{L}}},T_{\text{L}},l_{1})\otimes\mathrm{Prov}_{\mathbb{N}[X]}(A_{q_{\text{R}}},T_{\text{R}},l_{2})\otimes
n_{\mathrm{r}}^{l^{\prime}}$

e first observe the following identity, for any
$\nu\in\mathrm{Val}^{p}_{l}(T)$ and any $q\in Q$, by definition of automaton
runs:

$\left|\mathrm{aruns}(A_{q},\nu(T))\right|=\sum_{\begin{subarray}{c}q_{\text{L}},q_{\text{R}}\in
Q\\\
q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n_{\mathrm{r}}),\nu(n_{\mathrm{r}})))\end{subarray}}\left|\mathrm{aruns}(A_{q_{\text{L}}},\nu(T_{\text{L}}))\right|\cdot\left|\mathrm{aruns}(A_{q_{\text{R}}},\nu(T_{\text{R}}))\right|$

We then observe that $\mathrm{Val}^{p}_{l}(T)$ can be decomposed as

$\bigsqcup_{l_{1}+l_{2}+l^{\prime}=l}\mathrm{Val}^{p}_{l_{1}}(T_{\text{L}})\times\mathrm{Val}^{p}_{l_{2}}(T_{\text{R}})\times\\{n_{\mathrm{r}}\mapsto
l^{\prime}\\}$

as a valuation of $T$ summing to $l$ can be chosen as a valuation of its left
and right subtree and of $n_{\mathrm{r}}$ by assigning the possible weights.
We also observe that the product over $n\in T$ can be split in a product on
$n_{\mathrm{r}}$, on $n\in T_{\text{L}}$ and on $n\in T_{\text{R}}$. We can
thus rewrite as follows:

$\mathrm{Prov}_{\mathbb{N}[X]}(A,T,l)=\bigoplus_{\begin{subarray}{c}\nu_{\text{L}}\in\mathrm{Val}^{p}_{l_{1}}(T_{\text{L}})\\\
\nu_{\text{R}}\in\mathrm{Val}^{p}_{l_{2}}(T_{\text{R}})\\\
l_{1}+l_{2}+l^{\prime}=l\end{subarray}}\bigoplus_{\begin{subarray}{c}q_{\text{L}},q_{\text{R}}\in
Q\\\ q\in\Delta\end{subarray}}m_{\text{L}}\cdot
m_{\text{R}}\left(\bigotimes_{n\in
T_{\text{L}}}n^{\nu_{\text{L}}(n)}\right)\left(\bigotimes_{n\in
T_{\text{R}}}n^{\nu_{\text{R}}(n)}\right)n_{\mathrm{r}}^{l^{\prime}}$

where we abbreviated $m_{\text{L}}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left|\mathrm{aruns}(A_{q_{\text{L}}},\nu(T_{\text{L}}))\right|$,
$m_{\text{R}}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left|\mathrm{aruns}(A_{q_{\text{R}}},\nu(T_{\text{R}}))\right|$,
and $\Delta\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\delta(q_{\text{L}},q_{\text{R}},(\lambda(n_{\mathrm{r}}),l^{\prime}))$.

Reordering sums and performing factorizations, we obtain:

$\mathrm{Prov}_{\mathbb{N}[X]}(A,T,l)=\bigoplus_{\begin{subarray}{c}q_{\text{L}},q_{\text{R}}\in
Q\\\ l_{1}+l_{2}+l^{\prime}=l\\\
q\in\Delta\end{subarray}}\left(\bigoplus_{\nu_{\text{L}}\in\mathrm{Val}^{p}_{l_{1}}(T_{\text{L}})}m_{\text{L}}\bigotimes_{n\in
T_{\text{L}}}n^{\nu_{\text{L}}(n)}\right)\left(\bigoplus_{\nu_{\text{R}}\in\mathrm{Val}^{p}_{l_{2}}(T_{\text{R}})}m_{\text{R}}\bigotimes_{n\in
T_{\text{R}}}n^{\nu_{\text{R}}(n)}\right)n_{\mathrm{r}}^{l^{\prime}}.$

Plugging back the definition of provenance yields the desired claim.

We then prove the following variant of Theorem 5.2:

######  Theorem C.1.

For any fixed $p\in\mathbb{N}$ and $l\in\mathbb{N}\cup\\{\mathrm{all}\\}$, a
_$\mathbb{N}[X]$ -$l$-provenance circuit_ for a $\overline{\Gamma}^{p}$-bNTA
$A$ and a $\Gamma$-tree $T$ (i.e., a $\mathbb{N}[X]$-circuit capturing
$\mathrm{Prov}_{\mathbb{N}[X]}(A,T,l)$) can be constructed in time
$O(\left|A\right|\cdot\left|T\right|)$.

e modify the proof of Proposition A.1.

We fix $l_{0}$ to be the $l$ provided as input. We will first assume
$l_{0}\in\mathbb{N}$, we explain at the end of the proof how to handle the
(simpler) case $l_{0}=\mathrm{all}$.

For every node $n$ of the tree $T$, we create one input gate
$g^{\mathrm{i}}_{n}$ in $C$ (identified to $n$), and for
$j\in\\{0,\ldots,p\\}$, we create a gate $g^{\mathrm{i},j}_{n}$ which is a
$\otimes$-gate of $j$ copies of the input gate $g^{\mathrm{i}}_{n}$. (By
“copies” we mean $\otimes$\- or $\oplus$-gates whose sole input is
$g^{\mathrm{i}}_{n}$, this being a technical necessity as $K$-circuits are
defined as graphs and not multigraphs.) In particular, $g^{\mathrm{i},0}_{n}$
is always a $1$-gate.

We create one gate $g^{q,l}_{n}$ for $n\in T$, $q\in Q$, and $0\leqslant
l\leqslant l_{0}$.

For leaf nodes $n$, for $q\in Q$, we set $g^{q,l}_{n}$ to be
$g^{\mathrm{i},l}_{n}$ if $q\in\iota(\lambda(n),l)$ and a $0$-gate otherwise.

For internal nodes $n$, for every pair $q_{\text{L}},q_{\text{R}}\in Q$ (that
appears as input states of a transition of $\delta$) and $0\leqslant
l_{1},l_{2}\leqslant l_{0}$ such that $l_{1}+l_{2}\leqslant l_{0}$, we create
the gate $g^{q_{\text{L}},l_{1},q_{\text{R}},l_{2}}_{n}$ as an $\otimes$-gate
of $g^{q_{\text{L}},l_{1}}_{L(n)}$ and $g^{q_{\text{R}},l_{2}}_{R(n)}$, and,
for $0\leqslant l^{\prime}\leqslant l_{0}$ such that
$l_{1}+l_{2}+l^{\prime}\leqslant l_{0}$, we create one gate
$g^{q_{\text{L}},l_{1},q_{\text{R}},l_{2},l^{\prime}}_{n}$ as the
$\otimes$-gate of $g^{q_{\text{L}},l_{1},q_{\text{R}},l_{2}}_{n}$ and
$g^{\mathrm{i},l^{\prime}}$. For $0\leqslant l\leqslant l_{0}$, we set
$g^{q,l}_{n}$ to be a $\oplus$-gate of all the
$g^{q_{\text{L}},l_{1},q_{\text{R}},l_{2},l^{\prime}}_{n}$ such that
$q\in\delta(q_{\text{L}},q_{\text{R}},(\lambda(n),l^{\prime}))$ and
$l_{1}+l_{2}+l^{\prime}=l$.

We define the distinguished gate $g_{0}$ as an $\otimes$-gate of the
$g^{q,l_{0}}_{n_{\mathrm{r}}}$ where $n_{\mathrm{r}}$ is the root of $T$. The
construction is again in $O(\left|A\right|\cdot\left|T\right|)$ for fixed $l$
and $p$.

To prove correctness, we show by induction that the element captured by
$g^{q,l}_{n}$ is $\mathrm{Prov}_{\mathbb{N}[X]}(A_{q},T_{n},l)$ where $A_{q}$
is $A$ with $q$ as the only final state, and $T_{n}$ is $T$ rooted at $n$.

As a general property, note that for any node $n$, the value captured by
$g^{\mathrm{i},j}_{n}$ for $0\leqslant j\leqslant p$ is $n^{j}$.

For a leaf node $n$, $\mathrm{Prov}_{\mathbb{N}[X]}(A_{q},T_{n},l)=n^{l}$ if
$q\in\iota(\lambda(n),l)$ and $0$ otherwise, which is the value captured by
$g^{q,l}_{n}$.

For an internal node $n$, the claim follows immediately by Lemma C.3, applying
the induction hypothesis to $g^{q_{L},l_{1}}_{L(n)}$ and
$g^{q_{R},l_{2}}_{R(n)}$.

We conclude because clearly we have
$\mathrm{Prov}_{\mathbb{N}[X]}(A,T,l_{0})=\bigoplus_{q\in
F}\mathrm{Prov}_{\mathbb{N}[X]}(A_{q},T,l_{0})$, so the value captured by
$g_{0}$ is indeed correct.

Now, if $l_{0}=\mathrm{all}$, we do the same construction, but we only need a
single node $g_{n}^{q}$ for $n\in T$ and $q\in Q$ instead of $l_{0}+1$ nodes
$g_{n}^{q,l}$. For leaf nodes, $g_{n}^{q}$ is the $\oplus$-node of the
$g_{n}^{\mathrm{i},l}$; for internal nodes, $g_{n}^{q}$ is simply the
$\oplus$-gate of all $g_{n}^{q_{L},q_{R},l}$ gates with
$q\in\delta(q_{L},q_{R},(\lambda(n),l))$, each of them being an $\otimes$-gate
of the $g_{n}^{q_{L},q_{R}}$ gate and the $g^{\mathrm{i},l}$ gate. Finally,
$g_{n}^{q_{L},q_{R}}$ is the $\otimes$-gate of $g_{L(n)}^{q_{L}}$ and
$g_{R(n)}^{q_{R}}$. Correctness is shown using a variant of Lemma C.3 on
$\mathrm{Prov}_{\mathbb{N}[X]}(A,T,\mathrm{all})$ which replaces
$l_{1}+l_{2}+l^{\prime}=l$ in the sum subscript by $0\leqslant
l^{\prime}\leqslant p$.

###  C.3 Provenance circuit for instances

relaxtheoremrp[5.3]relaxrelaxtheoremrp We first give some preliminary
definitions. We need to introduce _bag-instances_ , to materialize the
possibility that a fact is used multiple times in a UCQ:

######  Definition C.6.

A _multiset_ is a function $M$ from a finite _support_
$\operatorname{supp}(M)$ to $\mathbb{N}$. We define the relation $M\subseteq
M^{\prime}$ if
$\operatorname{supp}(M)\subseteq\operatorname{supp}(M^{\prime})$ and for all
$s\in\operatorname{supp}(M)$ we have $M(s)\leqslant M^{\prime}(s)$. We write
$x\in M$ to mean that $M(x)>0$. Given a set $S$ and multiset $M$, we write
$M\sqsubseteq S$ to mean that $\operatorname{supp}(M)\subseteq S$, and for
$p\in\mathbb{N}$ we write $M\sqsubseteq^{p}S$ to mean that $M\sqsubseteq S$
and $M(a)\leqslant p$ for all $a\in\operatorname{supp}(M)$.

A _bag-instance_ $J$ is a multiset of facts on $\operatorname{dom}(J)$. Where
necessary to avoid confusion, we call the ordinary instances _set-instances_.
For two bag-instances $J$ and $J^{\prime}$, we say that $J$ is a _bag-
subinstance_ of $J^{\prime}$ if $J\subseteq J^{\prime}$ holds (as multisets).
We say that $J$ is a _bag-subinstance_ of a set-instance $I$ if $J\sqsubseteq
I$, and a _$p$ -bag-subinstance_ of $I$ if $J\sqsubseteq^{p}I$. In other
words, set-instances are understood as bag-instances where facts have an
arbitrarily large multiplicity (and _not_ multiplicity equal to $1$). The
_truncation to $p$_ of a bag-instance $J$ is $J^{\leqslant p}(F)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\min(J(F),p)$
for all $F\in\operatorname{supp}(J)$.

A _bag-homomorphism_ $h$ from a bag-instance $J$ to a bag-instance
$J^{\prime}$ is a mapping from $\operatorname{supp}(J)$ to
$\operatorname{supp}(J^{\prime})$ with the following condition: for each
$F\in\operatorname{supp}(J^{\prime})$, letting $F_{1},\ldots,F_{n}$ be the
facts of $\operatorname{supp}(J)$ such that $h(F_{i})=F$ for $1\leqslant
i\leqslant n$, we have $\sum_{i=1}^{n}J(F_{i})\leqslant J^{\prime}(F)$.

We accordingly define _bag-queries_ as queries on such bag-instances.
Intuitively, bag-queries are like regular Boolean queries on instances, except
that they can “see” the multiplicity of facts. This is crucial to talk about
the required multiplicity of facts in matches, which we need to talk about the
$\mathbb{N}[X]$-provenance of UCQs.

######  Definition C.7.

A _bag-query_ $q$ is a query on bag-instances. The bag-query $q^{\prime}$
_associated_ to a CQ $\exists\mathbf{x}\,q(\mathbf{x})$ is defined as follows.
A _match_ of $q$ in a bag-instance $J$ is a bag-homomorphism from $q$ (seen as
a bag-instance of facts over $\mathbf{x}$) to $J$. We say that $J\models
q^{\prime}$ if $q$ has a match in $J$.

The bag-query associated to a UCQ
$q=\bigvee_{i=1}^{n}\exists\mathbf{x}_{i}\,q_{i}(\mathbf{x}_{i})$ is the
disjunction of the bag-queries for each CQ in the disjunction.

Alternatively it is easily seen that $J\models q^{\prime}$, for $q^{\prime}$
the bag-query associated to a UCQ $q$, iff $J$ contains a bag of facts that
can be used as the leaves of a derivation tree for the Datalog query $P_{q}$
associated to $q$.

We notice that the bag-query associated to a UCQ $q$ is _bounded_ , namely,
the fact that it holds or not cannot depend on the multiplicity of facts
beyond a certain maximal value (the maximal number of atoms in a disjunct of
the UCQ):

######  Definition C.8.

A bag-query $q$ is _bounded_ by $p\in\mathbb{N}$ if, for any bag-instance $J$,
if $J\models q$, then the truncation $J^{\leqslant p}$ of $J$ is such that
$J^{\leqslant p}\models q$. A bag-query is _bounded_ if it is bounded by some
$p\in\mathbb{N}$.

We now extend our definitions of tree encodings and automaton compilation to
bag-queries. First, tree encodings simply generalize to bag-instances as tree
encodings annotated with the multiplicities of facts, that is,
$\overline{\Gamma^{k}_{\sigma}}^{p}$-trees:

######  Definition C.9.

Let $k,p\in\mathbb{N}$ and let $J$ be a bag-instance such that $J(F)\leqslant
p$ for all $F\in J$. Let $I\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\operatorname{supp}(J)$
be the underlying instance of $J$, and let $T_{I}$ be its tree encoding (a
$\Gamma^{k}_{\sigma}$-tree). We define the _$(k,p)$ -tree-encoding_ $T_{J}$ of
$J$ as the tree with same skeleton as $T_{I}$ where any node $n$ encoding a
fact $F$ of $I$ is given the label $(\lambda(n),J(F))$ and other nodes are
given the label $(\lambda(n),1)$. We accordingly define
$\left\langle\cdot\right\rangle$ on $\overline{\Gamma^{k}_{\sigma}}^{p}$-trees
to yield bag-instances in the expected way, again returning $\bot$ whenever
two nodes code the same fact (rather than summing up their multiplicity).

We then define what it means for a $\overline{\Gamma^{k}_{\sigma}}^{p}$-bNTA
to _test_ a bag-query $q$. Note that the definition implies that the automaton
cannot “see” multiplicities beyond $p$, so we require that the query be
$p$-bounded so that the limitation does not matter.

######  Definition C.10.

For $q$ a bag-query and $k,p\in\mathbb{N}$, a
$\overline{\Gamma^{k}_{\sigma}}^{p}$-bNTA $A$ _tests_ $q$ for treewidth $k$ if
$q$ is bounded by $p$ and for every $\overline{\Gamma^{k}_{\sigma}}^{p}$-tree
$E$, we have $E\models A$ iff $\left\langle E\right\rangle\models q$.

We then provide a general definition and prove a lemma about constructing the
union of bNTAs:

######  Definition C.11.

Let $\Gamma$ be a finite label set and let
$A_{i}=(Q_{i},F_{i},\iota_{i},\delta_{i})$ be a family of $\Gamma$-bNTAs.
Assume without loss of generality that the $Q_{i}$ have been renamed so that
they are pairwise disjoint. The _union bNTA_ is the $\Gamma$-bNTA
$A_{\sqcup}=(Q_{\sqcup},F_{\sqcup},\iota_{\sqcup},\delta_{\sqcup})$ defined by
$Q_{\sqcup}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigsqcup_{i}Q_{i}$,
$F_{\sqcup}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigsqcup_{i}F_{i}$,
for every $\tau\in\Gamma$ $\iota_{\sqcup}(\tau)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigsqcup_{i}\iota_{\sqcup}(\tau)$,
and $\delta_{\sqcup}$ is only defined for $q_{1},q_{2}\in Q_{i}$ for some
$Q_{i}$, in which case it is defined as
$\delta_{\sqcup}(q_{1},q_{2},\tau)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\delta_{i}(q_{1},q_{2},\tau)$.

######  Lemma C.4.

For any family of $\Gamma$-bNTAs $A_{i}$, letting $A_{\sqcup}$ be the union
bNTA of the $A_{i}$, for any $\Gamma$-tree $T$, we have $T\models A_{\sqcup}$
iff $T\models A_{i}$ for some $A_{i}$, and more precisely we have
$\left|\mathrm{aruns}(A_{\sqcup},T)\right|=\sum_{i}\left|\mathrm{aruns}(A_{i},T)\right|$.

he claim about acceptance and the number of runs is straightforward by
noticing that the runs of $A_{\sqcup}$ on $T$ are exactly the disjoint union
of the runs of the $A_{i}$ on $T$.

Our last preliminary result is to show that every bag-query corresponding to a
UCQ can be encoded to an automaton that tests it.

######  Proposition C.2.

Let $q$ be a UCQ. There is $p\in\mathbb{N}$ such that, for any
$k\in\mathbb{N}$, we can compute a $\overline{\Gamma^{k}_{\sigma}}^{p}$-bNTA
$A$ that tests $q$ for treewidth $k$.

e introduce some notation. We call $\mathrm{CQ}^{\neq}$ the language of CQs
which can feature atoms of the form $x\neq y$, and $\mathrm{UCQ}^{\neq}$ the
language of UCQs except the disjuncts are in $\mathrm{CQ}^{\neq}$. We write
$\mathrm{Vars}(q)$ for the variables of a query $q$ of $\mathrm{CQ}^{\neq}$.
The bag-query associated to a query in $\mathrm{CQ}^{\neq}$ or
$\mathrm{UCQ}^{\neq}$ is defined as for the corresponding query with no
inequalities, but imposing the inequalities on matches. Formally, a match of a
$\mathrm{CQ}^{\neq}$ query $q^{\prime}$ is a match $h$ of $q^{\prime}$ such
that $h(x)\neq h(y)$ for any two variables $x$ and $y$ such that $x\neq y$
occurs in $q$. (Note that the multiplicity of inequality atoms is irrelevant.)

We first note that, writing the UCQ $q$ as the disjunction of CQs $q_{i}$, if
we can show the claim for each $q_{i}$, then the result clearly follows from
$q$ by computing one bNTA $A_{i}$ for each $q_{i}$ that tests $q_{i}$ for
treewidth $k$ and uses $p=\max_{i}p_{i}$, where $p_{i}$ is the multiplicity
for which the result was shown for each $q_{i}$ (clearly if the claim holds
for a value of $p$ then it must hold for larger values by ignoring larger
multiplicities). We then construct the union bNTA $A_{\sqcup}$ of these bNTAs
to obtain a bNTA that tests $q$ (Lemma C.4).

We see a CQ $q$ as an existentially quantified multiset of atoms (the same
atom, i.e., the same relation name applied to the same variables in the same
order, can occur multiple times; in other words we distinguish, e.g., $\exists
xR(x)$ and $\exists xR(x)R(x)$). Let $\mathrm{Vars}(q)$ be the set of the
variables of $q$ (which are all existentially quantified as $q$ is Boolean).
We call $\mathcal{E}_{q}$ the set of all equivalence classes on
$\mathrm{Vars}(q)$ (which is of course finite), and for
${\sim}\in\mathcal{E}_{q}$ we let $q/{\sim}$ be the query in
$\mathrm{CQ}^{\neq}$ obtained by choosing one representative variable in
$\mathrm{Vars}(q)$ for each equivalence class of $\sim$ and mapping every
$x\in\mathrm{Vars}(q)$ to the representative variable for the class of $x$
(dropping in the result the useless existential quantifications on variables
that do not occur anymore), and adding disequalities $x\neq y$ between each
pair of the remaining variables.

We rewrite a CQ $q$ to the UCQ $q^{\prime}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigvee_{\sim\in\mathcal{E}_{q}}q/{\sim}$.
We claim that for every bag-instance $I$, if $I\models q$ then $I\models
q^{\prime}$, which justifies that for an instance $I^{\prime\prime}$,
considering the subinstances of $I^{\prime\prime}$,
$W_{K}(q,I^{\prime\prime})=W_{K}(q^{\prime},I^{\prime\prime})$. For the
forward implication, assuming that $I\models q$, letting $m$ be the witnessing
match, we consider the $\sim_{m}$ relation defined by $x\sim_{m}y$ iff
$m(x)=m(y)$, and it is easily seen that $I\models q/{\sim_{m}}$. For the
backward implication, if $I\models q/{\sim}$ for some
$\sim\in\mathcal{E}_{q}$, it is immediate that $I\models q$ with the
straightforward match. Hence, using again Lemma C.4, it suffices to show the
result for queries in $\mathrm{CQ}^{\neq}$ which include inequality axioms
between all their variables. We call those _forced queries_.

We now show that the claim holds for forced queries. To see this, considering
such a query $q$ on signature $\sigma$, letting $p$ be the sum of the
multiplicities of all atoms in $q$ (i.e., the number of atoms in the original
CQ $q$), let $\sigma_{p}$ be the signature obtained from $\sigma$ by creating
a relation $R^{i}$ for $1\leqslant i\leqslant p$, with arity
$\mathrm{arity}(R)$, for every relation $R$ of $\sigma$, and let $q^{\prime}$
be the rewriting of $q$ obtained by replacing every atom $R(\mathbf{a})$ with
multiplicity $m$ by the disjunction $\bigvee_{m\leqslant j\leqslant
p}R^{j}(\mathbf{a})$ (and keeping the inequalities), rewritten to a
$\mathrm{UCQ}^{\neq}$. We now see $q^{\prime}$ as a $\mathrm{UCQ}^{\neq}$ in
the usual sense (without multiplicities). We now claim that for any bag-
instance $I$ on $\sigma$ where facts have multiplicity $\leqslant p$, letting
$I^{\prime}$ be the set-instance obtained by replacing every fact
$F=R(\mathbf{a})$ of $I$ with multiplicity $m=I(F)$ by the fact
$R^{m}(\mathbf{a})$, $I\models q$ iff $I^{\prime}\models q^{\prime}$. To see
why, observe that, as $q$ is a forced query, if $q$ has a match $m$ then every
atom $A$ of $q$ must be mapped by $m$ to a fact of $I$ (written $m(A)$) and
this mapping must be injective (because $m$ is), so that the necessary and
sufficient condition is that $I(m(A))\geqslant p_{A}$ (where $p_{A}$ is the
multiplicity of $A$ in $q$) for every atom $A$ of $q$; and this is equivalent
to $I^{\prime}\models q^{\prime}$.

Now, $q^{\prime}$ is a $\mathrm{UCQ}^{\neq}$ so it can be tested _in the sense
of Definition 4.2_ (as it is expressible in GSO, so we can apply Theorem 4.1);
fix $k\in\mathbb{N}^{*}$ and let $A_{q^{\prime}}=(Q,F,\iota,\delta)$ be a
$\Gamma^{k}_{\sigma_{p}}$-bNTA that tests $q^{\prime}$ for width $k$. We build
a $\overline{\Gamma^{k}_{\sigma}}^{p}$-bNTA
$A_{q}=(Q,F,\iota^{\prime},\delta^{\prime})$ by relabeling $A_{q^{\prime}}$ in
the following way. Recall the definition of $\Gamma^{k}_{\sigma}$ (Definition
B.2). For every $((d,f),i)\in\overline{\Gamma^{k}_{\sigma}}^{p}$, set
$f^{\prime}$ to be either $f$ if $f=\emptyset$ and
$f^{\prime}=R^{i}(\mathbf{a})$ if $f=R(\mathbf{a})$, and set
$\iota^{\prime}(((d,f),i))$ to be $\iota((d,f^{\prime}))$ and
$\delta^{\prime}(q_{\text{L}},q_{\text{R}},((d,f),i))$ to be
$\delta(q_{\text{L}},q_{\text{R}},(d,f^{\prime}))$ for every
$q_{\text{L}},q_{\text{R}}\in Q$.

We now claim that $A_{q}$ tests $q$ for treewidth $k$. To see why, it suffices
to observe that for any $\overline{\Gamma^{k}_{\sigma}}^{p}$-tree $T$, letting
$T^{\prime}$ be the $\Gamma^{k}_{\sigma_{p}}$-tree obtained in the
straightforward manner, then $A_{q}$ accepts $T$ iff $A_{q^{\prime}}$ accepts
$T^{\prime}$, which is immediate by construction. Now indeed, as we know that
$A_{q^{\prime}}$ accepts $T^{\prime}$ iff $\left\langle
T^{\prime}\right\rangle\models q^{\prime}$ (as $A_{q^{\prime}}$ tests
$q^{\prime}$), and (as immediately $\left\langle T^{\prime}\right\rangle$ is
the $\sigma_{p}$-instance corresponding to $\left\langle T\right\rangle$ as
$I^{\prime}$ corresponds to $I$ above) that $\left\langle
T^{\prime}\right\rangle\models q^{\prime}$ iff $\left\langle
T\right\rangle\models q$, we have the desired equivalence.

The only thing left is to observe that $A_{q}$ does not only correctly test
$q$ on instances where each fact has multiplicity $\leqslant p$, but correctly
tests $q$ on all bag-instances. But this is straightforward: as $q$ matches at
most $p$ fact occurrences in the instance $I$, we have $I\models q$ iff
$I^{\leqslant p}\models q$. This concludes the proof.

We are now ready to prove Theorem 5.3: relaxoldproof We show the proof for
CQs, and then extend to UCQs.

Let $k\in\mathbb{N}$, $q:\exists\mathbf{x}\,q^{\prime}(\mathbf{x})$ be the CQ.
We rewrite $q$ to
$q^{\prime\prime}:\exists\mathbf{x}\,q^{\prime}(\mathbf{x})\land\bigwedge_{x\in\mathbf{x}}P_{x}(x)$
for fresh unary predicates $P_{x}$. We apply Proposition C.2 to compile
$q^{\prime\prime}$ to a $\overline{\Gamma^{k}_{\sigma}}^{p}$-bNTA $A$, where
$p$ is the number of atoms of $q^{\prime\prime}$, such that $A$ tests
$q^{\prime\prime}$ for treewidth $k$. We can clearly design a
$\overline{\Gamma^{k}_{\sigma}}^{p}$-bNTA $A^{\prime}$ that checks on a
$\overline{\Gamma^{k}_{\sigma}}^{p}$-tree whether, for all $x\in\mathbf{x}$,
the input tree contains exactly one $P_{x}$-fact: this can be done with state
space $2^{\mathbf{x}}$. We intersect $A$ and $A^{\prime}$ to obtain a bNTA
that recognizes all $\overline{\Gamma^{k}_{\sigma}}^{p}$-trees that satisfy
the bag-query associated to $q^{\prime\prime}$ and have exactly one
$P_{x}$-fact for all $x\in\mathbf{x}$, and determinize this bNTA to obtain an
equivalent automaton $A^{\prime\prime}$ which is _deterministic_ : if it has
an accepting run then it has exactly one accepting run.

Let $I$ be the input instance, and $I^{\prime}$ be the instance where we added
one fact $P_{x}(a)$ for all $x\in\mathbf{x}$ and $a\in\operatorname{dom}(I)$:
we call those the _additional facts_. We can clearly compute $I^{\prime}$ from
$I$ in linear time, and the treewidth is unchanged. Let $T_{I^{\prime}}$ be a
tree encoding of $I^{\prime}$, that is, a $\Gamma^{k}_{\sigma}$-tree.

We claim that we can construct, from $A^{\prime\prime}$, a bNTA
$A^{\prime\prime\prime}$ such that, for any valuation $\nu$ of
$T_{I^{\prime}}$ that gives multiplicity $1$ to the additional facts, the
number of accepting runs of $A^{\prime\prime\prime}$ on $\nu(T_{I^{\prime}})$
is the number of valuations $\nu^{\prime}$ from the additional facts to
$\\{0,1\\}$ such that $A^{\prime\prime}$ accepts
$\nu^{\prime\prime}(T_{I^{\prime}})$, where $\nu^{\prime\prime}$ follows
$\nu^{\prime}$ on nodes encoding additional facts and follows $\nu$ otherwise.
We proceed as follows: first, duplicate the states of $A^{\prime\prime}$ so
that every state $q$ is replicated to two states $q$ and $q^{\prime}$, $q$ and
$q^{\prime}$ being treated exactly the same way in terms of transitions in
$\delta$ and in terms of being final (this preserves determinism). Now, ensure
that for any two states $q_{1}$ and $q_{2}$ and labels $(\tau,0)$ and
$(\tau,1)$ in $\overline{\Gamma^{k}_{\sigma}}^{p}$ that encode a present or
absent additional fact, $\delta(q_{1},q_{2},(\tau,0))$ and
$\delta(q_{1},q_{2},(\tau,1))$ are disjoint (as $A^{\prime\prime}$ is
deterministic, those are single facts, so if they are the same fact, replace
one of them by its equivalent copy). Now, modify the transitions of the
automaton so that, for any states $q_{1}$ and $q_{2}$ and $\tau$ encoding an
additional fact, $\delta(q_{1},q_{2},(\tau,1))$ is
$\delta(q_{1},q_{2},(\tau,0))\cup\delta(q_{1},q_{2},(\tau,1))$. It is now
clear that the resulting automaton $A^{\prime\prime\prime}$ satisfies the
desired property: for any valuation $\nu$ as above, there is a bijection
between the accepting runs of $A^{\prime\prime\prime}$ and the valuations
$\nu^{\prime}$ as above such that $\nu^{\prime\prime}(T_{I^{\prime}})$ is
accepted by $A^{\prime\prime}$.

We now apply Theorem C.1 with $l$ the number of facts in the CQ
$q^{\prime\prime}$ to obtain a $\mathbb{N}[X]$-circuit that captures the
$\mathbb{N}[X]$-$l$-provenance of $A^{\prime\prime\prime}$ on
$T_{I^{\prime}}$; and fix to $1$ all inputs except those coding a fact of $I$
(i.e., nodes coding additional facts are set to $1$) and rename the remaining
inputs to match the facts of $I$. Let $l^{\prime}$ be the number of facts in
the original CQ $q$. Then the circuit captures:

$\bigoplus_{\begin{subarray}{c}J\sqsubseteq I\\\ J\models q\\\
\sum_{F\in\operatorname{supp}(J)}J(F)=l^{\prime}\end{subarray}}\left|\\{\>f:\mathbf{x}\to\operatorname{dom}(I)\mid
J\models q^{\prime}(f(\mathbf{x}))\>\\}\right|\bigotimes_{F\in J}F^{J(F)}.$

Now, $J\models q^{\prime}(f(\mathbf{x}))$ just means
$q^{\prime}(f(\mathbf{x}))\subseteq J$ (as bag-instances), and as
$q^{\prime}(f(\mathbf{x}))$ and $J$ have same total multiplicity, this
actually means $J=q^{\prime}(f(\mathbf{x}))$. Hence, the above is equal to:

$\bigoplus_{\begin{subarray}{c}f:\mathbf{x}\to\operatorname{dom}(I)\\\
I\models q^{\prime}(f(\mathbf{x}))\end{subarray}}\bigotimes_{A(\mathbf{x})\in
q^{\prime}}A(f(\mathbf{x})).$

and this is exactly $\mathrm{Prov}_{\mathbb{N}[X]}(q,I)$.

For UCQs, observe that the provenance we need to compute (Definition 5.2) is
simply the sum of the provenance for each CQ. So we can just independently
build a circuit for each CQ and combine the circuits into one (merging the
input gates), while choosing as distinguished gate a $\oplus$-gate of each
distinguished gate. relaxoldproof

###  C.4 Going beyond UCQs

Note that the proof of Theorem 5.3 implicitly relies on the fact that UCQs are
bounded in the sense of Definition C.8, and we cannot hope to rewrite a query
to a $\overline{\Gamma^{k}_{\sigma}}^{p}$-bNTA that sensibly tests it if it is
not bounded. However, we can show:

######  Proposition C.3.

There is a guarded monadic Datalog query $P$ whose associated bag-query
$q_{P}$ is not bounded.

onsider the Datalog query $P$ consisting of the rules $S(y)\leftarrow
S(x),R(x,a,y),A(a)$, $\mathrm{Goal}\leftarrow S(x),T(x)$. For all
$n\in\mathbb{N}$, consider the instance $I_{n}=\\{R(a_{1},a,a_{2}),\allowbreak
R(a_{2},a,a_{3}),\ldots,R(a_{n-1},a,a_{n}),\allowbreak S(a_{1}),\allowbreak
T(a_{n}),\allowbreak A(a)\\}$. It is easily verified that the only proof tree
of $P$ on $I_{n}$ has $n-1$ leaves with the fact $A(a)$. Hence, assuming that
the bag-query $q_{P}$ captured by $P$ is bounded by $p$, considering the bag-
instance $J$ formed of the leaves of the sole proof tree of $P$ on $I_{p+2}$,
it is not the case that $J^{\leqslant p}\models q_{P}$, contradicting
boundedness.

##  D Proofs for Section 6 (Applications)

###  D.1 Preliminaries

All proofs about probability evaluation in this section will use the notion of
_cc-instances_ , which we now introduce.

In this appendix, all Boolean circuits are non-monotone (i.e., they allow NOT-
gates) and arity-two (Definition B.5), unless stated otherwise. We will first
define the formalism of cc-instances, then state a result about the
construction of circuits (the analogue of provenance circuits) for them, using
Theorem 4.2, and finally explain how probability evaluation is performed using
that result using message-passing. We conclude by presenting the similar
formalism of _pc-instances_ , and stating tractability results for them
implied by the results on pcc-instances.

#### cc-instances.

We define the formalism of _cc-instances_ :

######  Definition D.1.

A _cc-instance_ is a triple $J=(I,C,\varphi)$ of a relational
$\sigma$-instance $I$, a (non-monotone arity-two) Boolean circuit $C$, and a
mapping $\varphi$ from the facts of $I$ to gates of $C$. The _inputs_
$J_{\mathsf{inp}}$ of $J$ are $C_{\mathsf{inp}}$. For every valuation $\nu$ of
$J_{\mathsf{inp}}$, the possible world $\nu(J)$ is the subinstance of $I$ that
contains the facts $F$ of $I$ such that $\nu(C)(\varphi(F))=1$, and, as for
c-instances, $\llbracket J\rrbracket$ is the set of possible worlds of $J$.

A pcc-instance is a 4-tuple $J=(I,C,\varphi,\pi)$ such that
$J^{\prime}=(I,C,\varphi)$ is a cc-instance (and
$J_{\mathsf{inp}}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=J^{\prime}_{\mathsf{inp}}$)
and $\pi:J_{\mathsf{inp}}\to[0,1]$ gives a probability to each input. As for
pc-instances, the probability distribution $\llbracket J\rrbracket$ has
universe $\llbracket J^{\prime}\rrbracket$ and probability measure
$\Pr\nolimits_{J}(I^{\prime})=\sum_{\begin{subarray}{c}\nu\mid\nu(J)=I^{\prime}\end{subarray}}\Pr\nolimits_{J}(\nu)$
with the product distribution:

$\Pr\nolimits_{J}(\nu)=\prod_{\begin{subarray}{c}g\in J_{\mathsf{inp}}\\\
\nu(g)=1\end{subarray}}\pi(g)\prod_{\begin{subarray}{c}g\in
J_{\mathsf{inp}}\\\ \nu(g)=0\end{subarray}}(1-\pi(g)).$

We define relational encodings and treewidth for cc-instances:

######  Definition D.2.

Let $\sigma_{\mathrm{Circuit}}$ be the signature of the relational encoding of
Boolean circuits (Definition B.6). Let $\sigma$ be a signature and
$\sigma^{+}$ be the signature with one relation $R^{+}$ of arity
$\mathrm{arity}(R)+1$ for every relation $R$ of $\sigma$. The _relational
encoding_ $I_{J}$ of a cc-instance $J=(I,C,\varphi)$ over signature $\sigma$,
is the $(\sigma_{\mathrm{Circuit}}\sqcup\sigma^{+})$-instance containing both
the $\sigma_{\mathrm{Circuit}}$-instance $I_{C}$ encoding $C$ and one fact
$R^{+}(\mathbf{a},\varphi(F))$ for every fact $F=R(\mathbf{a})$ in $I$.

A _tree decomposition_ of a cc-instance $J$ is a tree decomposition of
$I_{J}$. Tree decompositions of pcc-instances are defined as a tree
decomposition of the corresponding cc-instance (the probabilities are
ignored).

#### Circuits for cc-instances.

We claim the following result about cc-instances, intuitively corresponding to
the provenance circuits of Section 4 for them (combined with their circuit
annotation):

######  Theorem D.1.

For any fixed integer $k$ and GSO sentence $q$, one can compute in linear
time, from a cc-instance $J$ with $0pt(J)\leqslant k$, a Boolean circuit $C$
on $J_{\mathsf{inp}}$ such that for every valuation $\nu$ of
$J_{\mathsf{inp}}$, $\nu(C)=1$ iff $\nu(J)\models q$, with $0pt(C)$ depending
only on $k$ and $q$.

We now prove this result, explaining later what it implies in terms of
probability evaluation. We first introduce the notion of _cc-encoding_. Recall
the definition of tree decompositions of circuits (Definition B.6):

######  Definition D.3.

A _cc-encoding_ of width $k$ is a tuple $E^{\prime}=(E,C,T,\chi)$ of a
$\Gamma^{k}_{\sigma}$-tree $E$ of width $k$, a Boolean circuit $C$, a tree
decomposition $T$ of $C$ of width $k$ with same skeleton as $E$, and a mapping
$\chi:T\rightarrow C$ selecting a _selected gate_ such that
$\chi(b)\in\operatorname{dom}(b)$ for all $b\in T$. The _inputs_
$E^{\prime}_{\mathsf{inp}}$ of $E^{\prime}$ are $C_{\mathsf{inp}}$.

Given a valuation $\nu$ of $C_{\mathsf{inp}}$, we extend it to an evaluation
of $C$, and see it as a Boolean valuation of $E$ by setting
$\nu(n)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\nu(\chi(b))$
for the bag $b$ of $T$ corresponding to $n$ in $E$, and write
$\nu(E^{\prime})$ the resulting $\overline{\Gamma^{k}_{\sigma}}$-tree.

First, we explain how we can compute a cc-encoding of our cc-instance
$J=(I,C,\varphi)$ by “splitting” its tree decomposition $T$ in a tree
decomposition of $C$ and a $\Gamma^{k}_{\sigma}$-tree $E$ of $I$ with same
skeleton, with $\chi$ keeping track of the gate of $C$ to which each node
$n\in E$ was mapped by $\varphi$. Formally:

######  Lemma D.1.

Recall the definition of $\epsilon$ (Definition B.7). Given a cc-instance
$J=(I,C,\varphi)$ and a tree decomposition $T$ of $J$ of width $k$, one can
compute a cc-encoding $E^{\prime}=(E,C^{\prime},T^{\prime},\chi)$ of width
$k$, with $C=C^{\prime}$, such that for any valuation $\nu$ of
$C_{\mathsf{inp}}$, $\epsilon(\nu(E^{\prime}))$ is an encoding of $\nu(J)$.
The computation is in $O(\left|T\right|+\left|C\right|)$.

e process the tree decomposition $T$ of $J$ to construct $E$ and $T^{\prime}$.
We adapt the encoding construction described in Lemma B.1.

Whenever we process a bag $b\in T$, the mapping precomputed with $J$ (see
Lemma B.1) is used to obtain all facts $F$ of $I$ for which $b$ is the topmost
node where domain $\operatorname{dom}(F)\subseteq\operatorname{dom}(b)$ and
$\varphi(F)\in\operatorname{dom}(b)$.

For every such fact $F$, we create one bag $b^{\prime}$ in $T^{\prime}$
labeled with all elements of $\operatorname{dom}(b)$ that are gates of $G$,
and one node $n$ in $E$ which is the encoding of $F$ (considering only the
domain $\operatorname{dom}(b)\cap\operatorname{dom}(I)$) as for a normal
relational instance. Set the selected gate $\chi(b^{\prime})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\varphi(F)$
(which is in $\operatorname{dom}(b^{\prime})$ by the condition according to
which we chose to consider fact $F$).

Because $T$ was a tree decomposition of $J$, it is immediate that the
resulting tree $T^{\prime}$ is indeed a tree decomposition of width $k$ of $C$
and that $E$ is a tree encoding of width $k$ of $I$. By construction
$T^{\prime}$ and $E$ have same skeleton, and clearly the process is in linear
time in $\left|T\right|+\left|J\right|$. We let
$E^{\prime}=(E,C^{\prime},T^{\prime},\chi)$.

It remains to check the last condition. Consider a Boolean valuation $\nu$ of
the inputs of $C$. Consider the instance $\nu(J)$ and its tree decomposition
derived from $T$. It is clear that when one computes a tree encoding of
$\nu(J)$ following $T$, one obtains an encoding $E^{\prime\prime}$ which is
exactly $E$ except that the facts have been removed from the nodes which used
to encode in $E$ a fact that was removed from $\nu(J)$. Hence,
$E^{\prime\prime}$ is exactly $\epsilon(\nu(E^{\prime}))$. This concludes the
proof.

Second, we show the lemmas that will allow us to “glue together” the circuit
$C$ of the cc-instance, which annotates the cc-encoding, with a provenance
circuit for an automaton on the tree encoding.

######  Definition D.4.

Let $C=(G,W,g_{0},\mu)$ and
$C^{\prime}=(G^{\prime},W^{\prime},g_{0}^{\prime},\mu^{\prime})$ be circuits
such that $G\cap G^{\prime}=C^{\prime}_{\mathsf{inp}}$ (we say that $C$ and
$C^{\prime}$ are _stitchable_). The _stitching_ of $C$ and $C^{\prime}$,
denoted $C\circ C^{\prime}$, is the circuit $(G\cup G^{\prime},W\cup
W^{\prime},g_{0}^{\prime},\mu^{\prime\prime})$ where $\mu^{\prime\prime}(g)$
is defined according to $\mu$ for $g\in G$ and according to $\mu^{\prime}$
otherwise. In particular, $(C\circ
C^{\prime})_{\mathsf{inp}}=C_{\mathsf{inp}}$.

In the following lemmas about stitching, for clarity, we distinguish
valuations $\nu$ to the inputs of a circuit and the evaluation on all circuit
gates, which we write $\nu(C)$ where $C$ is the circuit.

The fundamental property of stitching is:

######  Lemma D.2.

For any stitchable circuits $C$ and $C^{\prime}$, for any gate $g$ of
$C^{\prime}$ and valuation $\nu$ of $C_{\mathsf{inp}}$, letting $\nu^{\prime}$
be the restriction of $\nu(C)$ to $C^{\prime}_{\mathsf{inp}}$, we have:
$\nu^{\prime}(C^{\prime})(g)=\nu(C\circ C^{\prime})(g)$.

ix $C$, $C^{\prime}$, $g$, and $\nu$. As $C$ and $C\circ C^{\prime}$ share the
same inputs, $\nu$ is a valuation for both of them. Now, first note that for
any gate $g$ of $C$, $\nu(C)(g)=\nu(C\circ C^{\prime})(g)$. Hence, in
particular, for any input gate $g$ of $C^{\prime}$, as it is a gate of $C$
because $C$ and $C^{\prime}$ are stitchable, we have $\nu(C\circ
C^{\prime})(g)=\nu(C)(g)=\nu^{\prime}(g)$. As this equality holds for any
input gate $g$ of $C^{\prime}$, it inductively holds for any gate of
$C^{\prime}$, which proves the result.

We show that a tree decomposition for $C\circ C^{\prime\prime}$ can be
obtained from two tree decompositions $T$ and $T^{\prime\prime}$ for $C$ and
$C^{\prime\prime}$ that have same skeleton, as the _sum_ $T+T^{\prime\prime}$
with same skeleton where each bag $b^{\prime\prime}$ of $T+T^{\prime}$ is the
union of the corresponding bags $b$ and $b^{\prime}$ in $T$ and $T^{\prime}$.
Namely:

######  Definition D.5.

Given two tree decompositions $T$ and $T^{\prime}$ with same skeleton, the
_sum_ of $T$ and $T^{\prime}$ (written $T+T^{\prime}$) is the tree
decomposition $T$ with same skeleton where every bag $b^{\prime\prime}$ is the
union of the corresponding bags $b$ and $b^{\prime}$ in $T$ and $T^{\prime}$.

The following is immediate:

######  Lemma D.3.

Given two tree decompositions with same skeleton $T$ and $T^{\prime}$ of fixed
width $k$ and $k^{\prime}$ for a Boolean circuit $C$ and a Boolean circuit
$C^{\prime}$, $T+T^{\prime}$ can be computed in linear time in $T$ and
$T^{\prime}$ and has width $\leqslant k+k^{\prime}+1$.