Provenance Semirings: Where Facts Come From

📍 Where we are: Part VI · Annotated and Temporal Logic — Chapter 18. Reasoning Benchmarks measured how fast a reasoner answers whether a fact holds; now we ask a different question about the same fact — where did it come from? — and find that provenance and confidence turn out to be one idea wearing two costumes.

A plain reasoner answers "is this entailed?" with a bare yes or no. But a real knowledge base wants more from a derived fact: which asserted facts it rests on, how confident we should be in it, and sometimes when it holds. This chapter takes the first of those — provenance, the record of where a fact comes from — and shows it is not a bolt-on feature but a single algebraic move. Attach a label to every base fact, run the ordinary forward-chaining fixpoint, and let the labels combine as the derivation combines. Change the algebra the labels live in and the same run reports different information about the same conclusion.

The simple version

Imagine a rumor reaching you by two routes at once. One friend tells you directly; another heard it through a mutual acquaintance who heard it from a third person. If you want to know whether the rumor reached you, either route is enough — you say "yes" if either path delivered it. But if you want to know what the rumor depends on, the two-person chain needs both links to have worked, while the direct route needs only its one link. "Either path suffices" and "every link in a path is required" are two different ways of combining evidence — and it turns out those are the only two operations you need to track exactly where any derived fact comes from.

What this chapter covers

• The semiring, decoded — a commutative semiring $(K, \oplus, \otimes, 0, 1)$ is just a set of labels with a "plus" and a "times"; the reading that makes it provenance is that a rule body (a conjunction) combines with $\otimes$ and alternative derivations of the same fact combine with $\oplus$.
• The annotated fixpoint — the exact same least-fixpoint loop as Datalog, now threading a semiring value through every derivation instead of a bare truth value.
• One graph, two derivations — a three-edge citation graph where reach(p3, p1) can be proved two different ways, which is precisely what makes $\oplus$ do visible work.
• Four readings of one derivation — Boolean, Which, Why, and the $\mathbb{N}[X]$ polynomial semiring, each a different $(\oplus, \otimes)$ over the same run.
• The committed run — one fact, four labels, quoted from the program's real output, with the ordering of the provenance polynomial explained.
• Why provenance is trust — a derived fact that can name the base facts and paths it depends on is auditable, the symbolic counterpart to the explanation a neural model cannot give.

The semiring, decoded

Strip the intimidating word down. A semiring is a set $K$ of labels together with two ways of combining them: an addition $\oplus$ (say "oh-plus") and a multiplication $\otimes$ (say "oh-times"), each with an identity element — $0$ is the label that $\oplus$ ignores ($a \oplus 0 = a$) and $1$ is the label that $\otimes$ ignores ($a \otimes 1 = a$). Both operations are associative and commutative, $\otimes$ distributes over $\oplus$, and $0$ annihilates under $\otimes$. That whole bundle is written as the five-tuple $(K, \oplus, \otimes, 0, 1)$. It is a ring that has lost the ability to subtract — which is exactly right for provenance, because you can combine evidence but never un-derive a fact.

Now the reading that turns this algebra into provenance. A derived fact is proved by firing rules. Look at any one rule firing: its body is a conjunction of facts that must all hold, so the label of that firing is the $\otimes$-product of the labels of the facts it used. A fact may be provable by several firings — several alternative derivations — and since any one of them suffices, the fact's overall label is the $\oplus$-sum over all of them. Two words, two operators:

• $\otimes$ (times) combines the facts within one rule body — an "and", every link required.
• $\oplus$ (plus) combines alternative derivations of the same fact — an "or", any witness suffices.

The companion program encodes the semiring as literally four operations plus two constants — no more structure than the definition above (annotated.py lines 38–46):

class Semiring:
    """A commutative semiring (K, ⊕, ⊗, 0, 1) as four operations + two constants."""

    def __init__(self, zero, one, plus, times, name=""):
        self.zero = zero
        self.one = one
        self.plus = plus
        self.times = times
        self.name = name

Everything downstream is generic in this object: pick a different Semiring and the reasoning engine does not change one line, only the labels it threads. Formally, the label of a head atom $h$ is

$$\text{ann}(h) \;=\; \bigoplus_{\substack{\text{rule } h \,\leftarrow\, b_1,\dots,b_k \\ \text{that fires}}} \ \bigotimes_{i=1}^{k} \text{ann}(b_i),$$

the $\oplus$-sum over every firing that concludes $h$, of the $\otimes$-product of that firing's body labels [1]. Read left to right: multiply within a body, add across bodies.

The annotated fixpoint

Where does $\text{ann}(h)$ actually get computed? In the very loop Volume 1 built for Datalog. Recall the immediate-consequence operator: seed with the base facts, fire every rule whose body currently holds, repeat until a round adds nothing — the least fixpoint. The annotated version keeps that shape exactly and threads a semiring value through it (annotated.py lines 79–95):

def provenance_lfp(edb_annot, rules, sr: Semiring, max_iter: int = 100):
    """Least fixpoint of the semiring-annotated immediate-consequence operator.

    Each round recomputes every fact's annotation as the ⊕-sum, over all one-step
    derivations, of the ⊗-product of the body annotations — starting from the EDB
    tokens, which persist. Converges for any ω-continuous semiring on an acyclic
    program (all five below, on the DAG example)."""
    ann = dict(edb_annot)
    for _ in range(max_iter):
        new = dict(edb_annot)          # base tokens persist; IDB is recomputed
        for head, body in rules:
            for sub, prod in _match_body(body, ann, sr, {}, sr.one):
                h = _apply(head, sub)
                new[h] = sr.plus(new.get(h, sr.zero), prod)
        if new == ann:
            return ann
        ann = new

Three lines carry the whole idea. _match_body walks a rule body and threads the $\otimes$-product of every fact it matches, starting from the multiplicative identity sr.one and multiplying in each fact's label as it goes — its recursive step is literally sr.times(acc, label) (annotated.py line 71). Each firing yields a prod, the label of that one derivation. Then new[h] = sr.plus(new.get(h, sr.zero), prod) folds that derivation into the head's running total with $\oplus$, starting from the additive identity sr.zero. And if new == ann: return ann is the same fixpoint test as plain Datalog — stop when a round changes nothing. EDB here is the extensional database, the asserted base facts; IDB is the intensional database, the derived ones. The base tokens persist each round (new = dict(edb_annot)); the derived labels are recomputed from scratch, which is why every alternative derivation gets re-summed and none is double-counted [2].

One graph, two derivations

To see $\oplus$ earn its keep we need a fact with more than one derivation. The example is a tiny citation graph of three papers with three edges, each carrying a distinct provenance token (annotated.py lines 151–155):

EDGES = [
    ("p3", "p2", "r", 0.9),
    ("p2", "p1", "s", 0.8),
    ("p3", "p1", "t", 0.5),
]

Read the tokens off the edges: r labels the edge p3 → p2, s labels p2 → p1, and t labels the direct edge p3 → p1. (Ignore the fourth number in each row for now — it is a confidence, and the bridge at the end of the chapter is what it is for.) Reachability is the two-clause transitive rule you have met before: an edge is reachability, and an edge followed by a reachability is reachability (annotated.py lines 157–160):

REACH_RULES = [
    (("reach", "?x", "?y"), [("edge", "?x", "?y")]),
    (("reach", "?x", "?z"), [("edge", "?x", "?y"), ("reach", "?y", "?z")]),
]

Now watch reach(p3, p1). It has two derivations. The base clause fires on the direct edge, giving the one-token label $t$. The recursive clause fires on p3 → p2 followed by the reachability p2 → p1, a body of two facts whose labels multiply: $r \otimes s$. Since either derivation independently establishes the fact, its label is their $\oplus$-sum:

$$\text{ann}\big(\text{reach}(p_3, p_1)\big) \;=\; \underbrace{t}_{\text{direct}} \ \oplus \ \underbrace{(r \otimes s)}_{\text{two-hop}}.$$

Every semiring below is just a different reading of that one expression $t \oplus (r \otimes s)$.

Four readings of one derivation

Here are four semirings, each a different choice of what a label is and how $\oplus$ and $\otimes$ act on it. The domains climb in information content — from a single bit up to a full polynomial — and the last column shows what each computes for our doubly-derived fact.

semiring	domain $K$ (a label is…)	$\oplus$ (combine alternatives)	$\otimes$ (combine a body)	reads reach(p3, p1) as
Boolean	a truth value	∨ (or)	∧ (and)	True
Which	a set of tokens	∪ (union)	∪ (union)	[r, s, t]
Why	a set of token sets	∪ (union)	⋈ (pairwise union)	[[r, s], [t]]
$\mathbb{N}[X]$	a polynomial	+ (add coefficients)	× (multiply)	t + r·s

The Boolean semiring $(\{T, F\}, \vee, \wedge, F, T)$ throws all detail away and answers only "does it hold?" — $t \oplus (r \otimes s)$ becomes $T \vee (T \wedge T) = T$ (annotated.py line 100). The Which-provenance labels make both operations set union (annotated.py lines 102–103), so they accumulate the flat set of all tokens that participate in any derivation: $\{t\} \cup (\{r\} \cup \{s\}) = \{r, s, t\}$. It tells you which sources were touched, but loses how they group into paths — and because both operations are union, the empty set serves as both identities. Strictly, this bends the semiring definition: with $0 = 1 = \varnothing$ the annihilation law $a \otimes 0 = 0$ no longer holds — for a non-empty $a$, $a \cup \varnothing = a \ne \varnothing$ — and $0 = 1$ would collapse any genuine semiring to a single element. So Which is best read not as a semiring proper but as an idempotent commutative monoid reused for both operations, the one degenerate corner of the hierarchy: the lineage case the provenance literature handles with care.

Why-provenance keeps the grouping. A label is a set of witness sets, each witness set being one self-sufficient bundle of tokens that proves the fact. Its $\oplus$ is union (collect the alternative witnesses), but its $\otimes$ is the pairwise-union join ⋈ — combining two bodies forms every pairwise union of their witnesses (annotated.py lines 106–111). For our fact the direct derivation contributes the witness set $\{t\}$ and the two-hop derivation contributes $\{r\} \bowtie \{s\} = \{r, s\}$, giving the two alternative witnesses $\{r, s\}$ and $\{t\}$. Finally the polynomial semiring $\mathbb{N}[X]$ — ordinary polynomials with natural-number coefficients over the tokens as variables (annotated.py lines 114–130) — keeps everything: $\otimes$ is polynomial multiplication and $\oplus$ is addition, so the two derivations become the two monomials $t + r \cdot s$. This is the most informative reading; Boolean and Why are both semiring-homomorphic images of it, obtained by "forgetting" some structure, while Which — lacking annihilation — is the degenerate lineage collapse rather than a clean homomorphic image [1].

The committed run

Running the module evaluates all four (plus a fifth we hold back) on reach(p3, p1) and prints one fact under many labels (annotated.py lines 272–281):

reachability of (p3, p1) — direct edge t, plus two-hop path r·s
  Boolean       : True
  Which-prov    : ['r', 's', 't']
  Why-prov      : [['r', 's'], ['t']]
  Polynomial    : t + r·s
  Confidence    : 0.8

One derivation, four provenance answers, from a single fixpoint run — the whole thesis in five printed lines. The polynomial line reads t + r·s, not r·s + t, and that order is chosen, not accidental. The renderer sorts monomials by degree first, then lexically (annotated.py lines 140–144):

    for m in sorted(p, key=lambda m: (len(m), m)):
        c = p[m]
        mon = "·".join(m) if m else "1"
        terms.append(mon if c == 1 else f"{c}·{mon}")
    return " + ".join(terms)

So the shorter, direct derivation $t$ (one token, degree 1) prints ahead of the longer two-hop derivation $r \cdot s$ (two tokens, degree 2). Reading the polynomial left to right is reading the derivations shortest-path-first. The coefficient on each monomial, incidentally, counts how many distinct derivations produce that exact bundle of tokens — here each is $1$, so both are printed bare; a coefficient of $2$ would flag two different paths using the same sources.

The unsolved part

Every reading above rested on one quiet word in the fixpoint's docstring: the program is acyclic. The citation graph is a directed acyclic graph, so reach(p3, p1) has finitely many derivations and the polynomial $t + r \cdot s$ is a finite object. Add a single back-edge — say p1 also cites p3, so the papers cite in a cycle — and reach(p3, p1) acquires infinitely many derivations: around the loop once, twice, any number of times. The Boolean, Which, and Why readings still converge, because unioning a truth value or a finite token set eventually stabilizes. But the polynomial reading does not: its "full accounting" would be an infinite formal power series, and the plain $\mathbb{N}[X]$ semiring has no way to name it. The code is honest about the boundary — after max_iter rounds without a fixpoint it refuses to lie, raising RuntimeError("annotated fixpoint did not converge (cyclic provenance?)") (annotated.py line 96). Recursive provenance therefore forces a real choice: restrict to acyclic queries, drop to a coarser semiring that does converge, or move to $\omega$-continuous structures and formal power series where the infinite sum has a defined value [2]. The most informative label is exactly the one that is hardest to keep finite — a tension with no free resolution.

Why it matters

Provenance is auditability, and auditability is the property the neuro-symbolic frontier most conspicuously lacks on its neural side. Recall the sharp trade Volume 1 left open: symbolic reasoning is explainable by construction while learned models are opaque by default — they hand back an answer with no readable reason. A provenance-annotated fact closes exactly that gap on the symbolic half. When a reasoner concludes that one paper transitively cites another, it does not merely assert it; the polynomial $t + r \cdot s$ names the base edges and the paths the conclusion depends on. You can audit it: retract token $s$ and the two-hop witness collapses while the direct witness $t$ survives, so the fact stands — the algebra says in advance which conclusions each source underwrites [3]. That is the symbolic counterpart to the explanation a neural network cannot produce, and it is why a hybrid system that must justify an answer, not merely emit one, reaches for exactly this machinery.

A single reachability fact with two derivations, read through four semirings at once: the direct token t combines with the two-hop product r times s under one plus-and-times algebra, and swapping the algebra reprints the same derivation as a truth value, a token set, a set of witness sets, or a full provenance polynomial. Original diagram by the authors, created with AI assistance.

Key terms

• Commutative semiring $(K, \oplus, \otimes, 0, 1)$ — a set of labels with an associative, commutative "plus" and "times", identities $0$ and $1$, distribution, and $0$ annihilating under $\otimes$; a ring without subtraction, so evidence combines but never cancels.
• $\otimes$ (times) / $\oplus$ (plus) — the body-conjunction operator (every fact in a rule body required) and the alternative-derivation operator (any one derivation suffices).
• Provenance token — a distinct label attached to each base fact ($r$, $s$, $t$ on the three edges), so a derived fact's label names the sources it used.
• Annotated fixpoint (provenance_lfp) — the Datalog least-fixpoint loop that threads semiring values, $\oplus$-summing each fact's derivations of $\otimes$-products until a round adds nothing.
• Boolean / Which / Why / $\mathbb{N}[X]$ — four label algebras of increasing detail: does it hold, which tokens, which witness sets, the full polynomial; $\mathbb{N}[X]$ is the most informative, with Boolean and Why its homomorphic images and Which the one degenerate lineage corner (where $0 = 1$, so annihilation fails).
• Witness set — one self-sufficient bundle of tokens that proves a fact; Why-provenance is the set of alternative witness sets, here $\{r, s\}$ and $\{t\}$.
• Provenance polynomial — the $\mathbb{N}[X]$ label, e.g. $t + r \cdot s$; monomials are derivations, degree is path length, coefficients count distinct derivations.
• EDB / IDB — the asserted base facts (extensional) and the derived facts (intensional); base tokens persist each round while derived labels are recomputed.
• Auditability — the trust property provenance buys: a derived fact names the base facts and paths it depends on, the explanation a neural model cannot give.

Where this leads

Look again at the run: below the four provenance labels sat a fifth line, Confidence : 0.8. That is the same fixpoint over the same graph, evaluated in the semiring $([0,1], \max, \min)$ — where a label is a truth degree in the unit interval, $\otimes$ is $\min$ (a chain is only as strong as its weakest link, so $r \otimes s = \min(0.9, 0.8) = 0.8$) and $\oplus$ is $\max$ (the best of the alternatives, so $\max(t, r \otimes s) = \max(0.5, 0.8) = 0.8$). Nothing in provenance_lfp changed; only the algebra did, and out came a confidence instead of a provenance. That is the punchline of the whole framework and the doorway to the next chapter: provenance and graded truth are one construction, distinguished only by which semiring you plug in. The next chapter, Annotated Logic, follows that $([0,1], \max, \min)$ thread out of database provenance and into annotated and fuzzy reasoning, where the labels are no longer bookkeeping about sources but genuine degrees of belief that a rule must respect.