Determination Provenance: From Ambiguity to Algebra
arXiv:2606.10270v1 [cs.DB] 9 Jun 2026
JOSEPH M. HELLERSTEIN, University of California, Berkeley and Amazon Web Services, USA Many data systems admit multiple admissible outcomes for the same input: concurrent transactions may serialize in one of many orders; a logic program may have multiple stable models. Classical data provenance cannot even pose its question in such settings—it explains how a result was derived, but only after something has chosen which result to produce. We introduce determination provenance to track the commitments that resolve this ambiguity. A tuple’s support is the set of resolutions under which it holds. Supports form a commutative semiring, and layered commitments induce a filtration measuring each tuple’s query-relative depth—how many layers of semantic resolution it depends on. Positive relational algebra respects the filtration, enabling compositional robustness analysis and quantitative diagnosis of resolution cost. We instantiate the framework for transactional isolation and for Datalog¬ ; in both, classical semantic variants (isolation levels; negation semantics) correspond to different views of a single shared filtration.
1
Introduction
Algebraic data provenance explains the outputs of a deterministic query—a function from an input database to an output relation [13, 30]. But production data systems are often based on a more ambiguous specification—a relation that maps an input scenario to multiple admissible outputs. Examples include transactional databases (multiple acceptable schedules), distributed systems (multiple consensus decisions), and even Datalog with negation (multiple stable models). Classical data provenance cannot account for this ambiguity; it cannot even formulate a question about a particular outcome (e.g., why vs. why not) because the choice of outcome is undetermined. This paper lays the algebraic foundation for provenance over relational specifications. We introduce determination provenance, a structure that captures the commitments that resolve semantic ambiguity. A determination is a layered sequence of irrevocable, history-indexed commitment events that constrains a relational specification until it determines a single outcome for each input—the semantic counterpart of what a correct implementation achieves on each run. Classical provenance applies within each determination; determination provenance tracks which commitments were needed and how query results depend on them. Example 1.1 (Provenance under transactional ambiguity). Consider a relation 𝑆 (𝑘, 𝑦) with initial contents {𝑆 (0, 𝑏)}. Three transactions execute concurrently with a query: 𝑇1 : ins 𝑆 (1, 𝑏);
𝑇2 : ins 𝑆 (2, 𝑑);
𝑇3 : del 𝑆 (2, 𝑑);
𝑇𝑄 : 𝑄 (𝑦) : − 𝑆 (𝑘, 𝑦).
All four are concurrent; any serialization is possible. Value 𝑏 appears in 𝑄’s result regardless of ordering (the initial tuple 𝑆 (0, 𝑏) is never deleted): 𝑏 is robust. Value 𝑑 is contingent: it appears in serializations where 𝑇𝑄 observes 𝑇2 ’s insert before any effective delete—e.g., 𝑇2 ≺ 𝑇𝑄 ≺ 𝑇3 , or 𝑇3 ≺ 𝑇2 ≺ 𝑇𝑄 (where the delete precedes the insert and is a no-op). It is absent when the query precedes the insert or follows an effective delete. Before resolving this ambiguity, the provenance question for 𝑑 is undetermined: under one determination the question is why; under another it is why-not. Section 4 formalizes this example. Each concrete execution corresponds to one determination (the commitments that the system actually made). But 𝑏’s robustness and 𝑑’s contingency are properties of the space of all possible determinations, not of any single one. To reason about such properties algebraically, we track each tuple’s support: the set of determinations under which it holds. Value 𝑏 has full support (every determination); 𝑑 has partial support (the determinations in which 𝑇𝑄 observes 𝑇2 ’s insert). Supports form a Boolean semiring (join intersects supports; union merges them), and the familiar Author’s Contact Information: Joseph M. Hellerstein, University of California, Berkeley and Amazon Web Services, USA.
2
Joseph M. Hellerstein
power of algebraic provenance transfers: robustness reduces to checking whether support is full; counterfactual questions are read from the support; quantitative diagnosis from its measure. Determination provenance provides richer structure than this flat semiring, however. When commitments are layered—some depending on others’ outcomes—the semiring carries a filtration: a chain of sub-semirings reflecting how much resolution each tuple requires. A robust or impossible tuple has depth 0; a contingent tuple has positive depth reflecting which layer it first depends on. The key property on filtrations: positive RA cannot increase a result tuple’s depth beyond the maximum of its inputs. This enables depth bounds (queries over shallow tuples are unaffected by deeper layers), semantic-change analysis (comparing specifications tuple-by-tuple), and a complexity connection (depth-1 coincides with PDB lineage; higher depths correspond to layered PDB evaluation). We instantiate the framework for transactional isolation and Datalog¬ ; in both, classical semantic variants (isolation levels; negation semantics) are different views of a single filtration. Contributions. Determination provenance provides new layered algebraic structure, expressivity, and applicability: (i) The determination semiring and its filtration: supports over resolving determinations form a commutative semiring whose layered structure is reflected as a chain of sub-semirings that query evaluation respects (Sections 3.1–3.2). (ii) Instantiation for transactional systems: isolation levels (RC, SI, SER) are different resolving subsets of a shared filtration; determination depth is Θ(𝑛) worst-case (in the number of transactions) with scheduling discretion, and SER/SI are incomparable in per-tuple queryrelative depth (Section 4). (iii) Instantiation for Datalog¬ : for programs with stable models, negation semantics (stratified, well-founded, stable) are different reading depths of a shared filtration; monus elimination shows that sealing is support-equivalent to semirings with monus for stratified programs; the determination framework also handles unstratified negation, where monus does not provide a single resolved semantics (Section 5, Appendix F). (iv) Quantitative measures and semantic-change analysis: specifications over the same basis can be compared tuple-by-tuple, quantifying work regret vs. genuine semantic shift (Section 6). (v) Complexity and attribution (appendices): robustness is coNP-complete; a Shapley-value measure attributes contingency to individual commitments (Appendices B, C). 2
Preliminaries: Ambiguous Semantics and Refinement
We now formalize the setting: specifications with multiple admissible outcomes and the irrevocable choice structures—called determinations—that restrict ambiguity until meaning is determinate. 2.1
Histories
Histories are used to model ambiguity in distributed systems [18]; we use them here as well. Definition 2.1 (History). A history is a finite partially ordered set 𝐻 = (𝐸, →), where 𝐸 is a set of events and →⊆ 𝐸 × 𝐸 is a strict (irreflexive and transitive) partial order representing known precedence constraints among events. A history records which events have occurred and their precedence. The class H of all histories represents all possible states across all possible runs. When the partial order is total, a history is a sequence (e.g., a transaction schedule). To model how a history evolves, we define an extension relation. An extension may add new events and precedence edges involving them, but may not revise the past of any existing event.
Determination Provenance: From Ambiguity to Algebra
3
Definition 2.2 (History Extension). For histories 𝐻 1 = (𝐸 1, →1 ) and 𝐻 2 = (𝐸 2, →2 ), we write 𝐻 1 ⊑ 𝐻 2 if: (1) 𝐸 1 ⊆ 𝐸 2 , and (2) →1 =→2 ∩(𝐸 1 × 𝐸 1 ), and (3) no event in 𝐸 1 has a predecessor in 𝐸 2 \ 𝐸 1 . 2.2
Outcomes and Specifications
An outcome is an element of a set 𝑂 of externally observable results (e.g., a query result, a database state, or a model of a logic program). The chosen outcome domain must include a partial order ⪯ [15]. When 𝑜 1 ⪯ 𝑜 2 , replacing outcome 𝑜 1 with 𝑜 2 is not considered to rule out 𝑜 1 but rather to refine it—𝑜 2 adds detail without contradicting 𝑜 1 . The order ⪯ is part of the specification—a modeling choice, not derived from execution structure. Changing ⪯ changes the specification (enlarging ⪯ makes more outcomes compatible, reducing the commitments needed to resolve ambiguity). Definition 2.3 (Specification). A specification is a triple (H, 𝑂, ⪯) together with a relation Spec ⊆ H × 𝑂 associating each history with a set of admissible outcomes. We write Spec(𝐻 ) ≜ {𝑜 ∈ 𝑂 | (𝐻, 𝑜) ∈ Spec} for the admissible set at 𝐻 . Example 2.1 (Specification for Example 1.1). 𝑂 is the set of decision traces (commit/abort sequences for each transaction); ⪯ is trace-prefix extension (a longer trace refines a shorter one); Spec(𝐻 ) is the set of traces consistent with some serialization of the concurrent transactions in 𝐻 . As noted in the introduction, a specification is in general a relation; the goal of determination is to turn it into a function (a unique outcome per history). Since provenance analysis is retrospective— the full history is available—we define the resolved outcome at a history 𝐻 as the maximum element of Spec(𝐻 ) under ⪯. Definition 2.4 (Determined specification). A specification is determined at 𝐻 if Spec(𝐻 ) forms a chain under ⪯ with a maximum element (all outcomes are pairwise comparable and a greatest one exists). For a determined history, we write Spec(𝐻 ) as shorthand for max ⪯ Spec(𝐻 ) (the resolved outcome). A specification is determined if it is determined at every 𝐻 ∈ H . A determined specification defines a function from histories to outcomes; classical provenance applies directly. Ambiguity requiring determination arises only when Spec(𝐻 ) contains ⪯-incomparable outcomes (as in Example 2.1, where multiple serializations yield incomparable decision traces). 2.3
Commitments
Ambiguity is constrained via additional semantic commitments. Commitments are operators that narrow the admissible set; applying a commitment at a specific history produces a commitment event. Definition 2.5 (Commitment and commitment event). A commitment 𝜑 is an operator that can be applied at a history 𝐻 to produce an extended history 𝐻 · 𝜑 with Spec(𝐻 · 𝜑) ⊆ Spec(𝐻 ) ∧ Spec(𝐻 · 𝜑) ≠ ∅. The effect of 𝜑—which outcomes it excludes—depends on the history at which it is applied; a commitment has no history-independent semantics. The resulting event in 𝐻 · 𝜑 is a commitment event: the irrevocable record that 𝜑 was applied at this point. Here 𝐻 · 𝜑 denotes the history obtained by appending the commitment event after all maximal events of 𝐻 (giving 𝐻 ⊑ 𝐻 · 𝜑). Most commitments strictly shrink the admissible set; a sealing commitment 𝜑 seal(𝑆 ) may leave it unchanged, merely declaring a set of events 𝑆 complete and enabling subsequent commitments that depend on that completeness. Because a commitment event succeeds all maximal events, it induces a cut in the history poset, ensuring that commitment events form a total order within any history. Applied sequentially, commitments monotonically narrow the admissible set: Spec(𝐻 ) ⊇ Spec(𝐻 · 𝜑 1 ) ⊇ Spec(𝐻 · 𝜑 1 ·
4
Joseph M. Hellerstein
𝜑 2 ) ⊇ · · · . In general, the effect of 𝜑 may depend on the full admissible set at its point of application, not only on individual outcomes—this is what produces non-commutative commitments. Definition 2.6 (Commitment basis). A commitment basis Φ is a set of commitments (operators) from which determinations are formed. Different bases for the same specification yield different determination structures and different provenance. The choice of commitment basis is a modeling decision as fundamental as the choice of outcome space (𝑂, ⪯). Given an ambiguous specification (a relation), implementations select a single outcome on each run; the commitment basis lifts the strategies that such implementations use into a semantic domain, enabling reasoning across different implementations and their nondeterminism. (In Example 1.1, Φ = {𝜑𝑇𝑖 ≺𝑇𝑗 }: the set of all pairwise ordering operators, capturing shared aspects of 2PL, OCC and MVTO.) Three forces on a history. A history evolves under three forces [16]: environment events extend the history but are not chosen; commitments replace the admissible set with a subset (irrevocably constraining which outcomes remain possible); entailments refine the observed outcome upward in ⪯ without excluding any alternative (they add detail that is compatible with every remaining admissible outcome). In transactional systems, operation interleavings are environment and commit/abort decisions are commitments; in Datalog¬ , EDB facts are environment, sealing and choice predicates are commitments, and the alternating fixpoint’s classifications are entailments. 2.4
Determinations
Individual commitments typically resolve only part of the ambiguity. A full resolution requires a collection of them: Definition 2.7 (Determination). The determination of a history 𝐻 over a commitment basis Φ is the subsequence of commitment events in 𝐻 , listed in the order induced by →: 𝐷 (𝐻 ) = 𝜑 1 · 𝜑 2 · · · · · 𝜑𝑚 . Non-commitment events may occur between successive commitments; the effect of each 𝜑𝑖 depends on the full history at its point of application. A history 𝐻 is resolved if Spec(𝐻 ) is determined (Definition 2.4). Note that Spec itself is a fixed relation—it does not change as history grows. Commitment events can only narrow: Spec(𝐻 · 𝜑) ⊆ Spec(𝐻 ) by definition. Non-commitment events may change the admissible set in either direction; they provide the context in which commitments take effect (and hence why determinations are history-indexed). When the history is clear from context we write 𝐷 for 𝐷 (𝐻 ). Example 2.2 (Determinations for Example 1.1). The ordering decisions 𝜑𝑇2 ≺𝑇𝑄 and 𝜑𝑇𝑄 ≺𝑇3 are commitments: each excludes serializations incompatible with the chosen order. The determination 𝐷 in = 𝜑𝑇2 ≺𝑇𝑄 · 𝜑𝑇𝑄 ≺𝑇3 resolves the specification so that 𝑇𝑄 observes 𝑇2 ’s insert; 𝐷 out = 𝜑𝑇2 ≺𝑇3 · 𝜑𝑇3 ≺𝑇𝑄 resolves it so that 𝑑 is absent. Layer-sequencing notation. Commitments in a determination are sequenced for two reasons. First, non-commitment events may intervene: in 𝐻 · 𝜑 · 𝐸 · 𝜓 , the commitment 𝜓 may depend on event 𝐸, so 𝜑 and 𝜓 cannot be reordered. Second, even contiguous commitment events may not commute: Spec(𝐻 ·𝜑 ·𝜓 ) ≠ Spec(𝐻 ·𝜓 ·𝜑) when one commitment’s effect depends on the other’s exclusions. A layer is a maximal set of contiguous commitment events (no intervening non-commitment events) that commute pairwise. We use ⊲ to denote a sequence of such layers: Definition 2.8 (Seqencing of layers (notation)). Let 𝐿1, . . . , 𝐿𝑘 be multisets of commitments. We write 𝐷 = 𝐿1 ⊲ 𝐿2 ⊲ · · · ⊲ 𝐿𝑘 to indicate that determination 𝐷’s commitments are organized into 𝑘 layers, applied in order with non-commitment events possibly intervening between layers. Within each 𝐿𝑖 , commitments commute; across layers, order matters.
Determination Provenance: From Ambiguity to Algebra
5
The depth of a determination 𝐿1 ⊲ · · · ⊲ 𝐿𝑘 is 𝑘 (the number of layers). Definition 2.9 (Resolving determination). A determination 𝐷 (𝐻 ) is resolving if 𝐻 is resolved (Definition 2.4). Definition 2.10 (Minimal resolving determination). A resolving determination 𝐷 (𝐻 ) is minimal if removing any single commitment event from 𝐻 (while retaining all other events in their original order) yields a history that is not resolved. 2.5
Resolution Enables Provenance
Classical semiring provenance annotates base tuples and propagates annotations through query evaluation [13]. This applies directly to any resolved history: the determination selects a concrete outcome, and standard evaluation traces its derivation. The question is what happens when the specification is not resolved—when incompatible outcomes coexist. Theorem 2.1 (Classical provenance is pointwise in determinations). Classical semiring provenance (a single 𝐾-relation) correctly represents a specification Spec iff all resolving determinations produce the same tuple membership and derivational annotation. When two resolving determinations 𝐷 1, 𝐷 2 disagree on some tuple 𝑡 (𝑃𝐷 1 (𝑡) ≠ 𝑃𝐷 2 (𝑡)), any sound representation must distinguish 𝐷 1 from 𝐷2. Proof. Suppose two resolving determinations 𝐷 1, 𝐷 2 disagree: some tuple 𝑡 satisfies 𝑃𝐷 1 (𝑡) ≠ 𝑃𝐷 2 (𝑡) (where inequality includes one being 0). Since semiring provenance expresses only positive dependence on base facts [13], no single annotation can explain both presence under 𝐷 1 and absence under 𝐷 2 . Hence any sound representation must distinguish 𝐷 1 from 𝐷 2 . Conversely, if all resolving determinations agree, the common 𝐾-relation is sound and complete for all of them. □ 3
The Algebra of Determinations
Classical provenance owes its power to algebraic structure: derivations compose through a commutative semiring, and query evaluation preserves that structure [13]. One might expect that layered determinations—sequences of non-commuting commitments—resist such clean algebraic treatment. In fact, supports over resolving determinations form a commutative semiring, and the layering within each determination is reflected as a filtration of sub-semirings that query evaluation respects. Throughout, we fix a specification Spec over a history class H and a commitment basis Φ. Elements of DSpec,Φ (abbreviated D) are resolved histories with minimal determinations, identified up to outcome equivalence: 𝐻 1 ∼ 𝐻 2 when 𝐷 (𝐻 1 ) and 𝐷 (𝐻 2 ) produce the same resolved outcome and the same conditioned provenance for every tuple. Concretely, each element of D is a representative resolved history 𝐻 whose determination 𝐷 (𝐻 ) is minimal (Definition 2.10). Unlike abstract possible worlds, elements of D are grounded in event structure: the same commitment may have different effects at different histories, so determinations are history-indexed records, not symbolic labels. 3.1
The Determination Semiring
Fix a commutative semiring (𝐾, +, ·, 0, 1) for derivational provenance (e.g., the polynomial semiring N[𝑋 ] of [13]). A 𝐾-relation assigns each tuple a value in 𝐾: alternative derivations combine by +, joint use of facts by ·, absence by 0. For a determination 𝐷 ∈ D extracted from a resolved history 𝐻 , the conditioned provenance 𝑃𝐷 (𝑡) ∈ 𝐾 is the classical semiring provenance of tuple 𝑡 computed over the resolved outcome of 𝐻 . Conditioned provenance suffices for explaining a single execution. But some questions require reasoning across determinations: Does this result hold under every admissible commit ordering, or
6
Joseph M. Hellerstein
is it contingent on a particular one? Answering such questions requires comparing provenance across multiple determinations. Observables and provenance queries. To connect outcomes to provenance, we fix a relational schema S and an observation function obs : 𝑂 → Inst(S) mapping each outcome to a database instance. In our Datalog¬ examples, obs is the identity (outcomes are models, i.e., database instances); for transactions, obs maps a decision trace to the database state that results from applying committed transactions’ writes. A provenance query is a positive relational algebra expression over S; conditioned provenance is the familiar 𝐾-relational evaluation of Green et al. [13] applied to obs(Spec(𝐻 )). This is where the framework gains expressive power beyond per-commitment analysis: provenance queries can select individual tuples or join across transactions — enabling fine-grained and cross-transaction sensitivity analysis. Throughout, “tuple” refers to a tuple in obs(𝑜) or in a query result over it. Definition 3.1 (Determination Provenance). Fix a specification Spec and a provenance query 𝑄 over S. Each determination 𝐷 ∈ D corresponds to a resolved history 𝐻 ; evaluating 𝑄 over obs(Spec(𝐻 )) yields a 𝐾-annotation for each tuple 𝑡. The determination provenance of 𝑡 is the function 𝑃Spec (𝑡) : D → 𝐾 mapping each determination to the conditioned provenance 𝑃𝐷 (𝑡) (= 0𝐾 when 𝑡 is absent). When Spec is clear from context, we write 𝑃 (𝑡). Determination provenance is an element of the product semiring 𝐾 D (pointwise addition and multiplication): it assigns each 𝐷 ∈ D a semiring value recording how 𝑡 is derived under 𝐷. Conditioned provenance is the special case of evaluating at a single determination: 𝑃 (𝑡) (𝐷) = 𝑃𝐷 (𝑡). Classical provenance is the special case where |D | = 1 (the specification is already determined; no commitments needed). Definition 3.2 (Support and the determination semiring). The support of a tuple 𝑡 is supp(𝑃 (𝑡)) ≜ { 𝐷 ∈ D | 𝑃 (𝑡) (𝐷) ≠ 0 }: the set of determinations under which 𝑡 holds. Supports form a Boolean algebra (2 D , ∪, ∩, ∅, D) under the operations induced by query evaluation (join intersects supports; union merges them). This algebra is elementary; the non-trivial structure is the filtration (Section 3.2), which reflects the layered commitment process. Example 3.1 (Determination provenance for Example 1.1). Two resolved histories arise from Example 1.1: one in which 𝑇2 ’s insert is visible to 𝑇𝑄 (determination 𝐷 in ) and one in which 𝑇3 ’s delete precedes 𝑇𝑄 (determination 𝐷 out ). With D = {𝐷 in, 𝐷 out }: 𝑃 (𝑏) = {(𝐷 in, 𝑥 0 ), (𝐷 out, 𝑥 0 )} = D × {𝑥 0 },
𝑃 (𝑑) = {(𝐷 in, 𝑥 2 )}.
Here 𝑥 0 annotates the initial tuple 𝑆 (0, 𝑏) and 𝑥 2 annotates 𝑇2 ’s insert of 𝑆 (2, 𝑑). 𝑃 (𝑏) has full support (D): 𝑏 is robust. 𝑃 (𝑑) has partial support ({𝐷 in }): 𝑑 is contingent. Composition operates on both components: a join intersects supports (multiplies 𝐾-values pointwise); a union takes their union (adds 𝐾-values pointwise). Computational cost. When D is finite, |D | may be exponential in the number of commitments (each binary commitment doubles the space). Naively enumerating supports is therefore impractical. For single-layer determinations, supports admit compact representation as positive Boolean formulas over commitment variables (Proposition 3.2).
Determination Provenance: From Ambiguity to Algebra
3.2
7
Filtration of the Determination Semiring
The Boolean algebra on supports tells us whether a tuple is contingent, but not why—which commitment layer it depends on. Every determination 𝐷 is a sequence of commitment events (Definition 2.7); within that sequence, a layer is a maximal contiguous set of commitments that commute pairwise in the history at which they are applied. The layers of 𝐷 are its Foata normal form [21]: the coarsest grouping into commuting stages. (In general, commutativity may be dynamic—dependent on the current admissible set—making canonical layering subtle; see Appendix J. In both instantiations below, commutativity is history-independent, so the layer structure is unambiguous.) Write 𝐿1 (𝐷), 𝐿2 (𝐷), . . . for the successive layers of 𝐷; the depth of 𝐷 is its number of layers. Definition 3.3 (Level-𝑘 agreement). Two determinations 𝐷, 𝐷 ′ ∈ D agree at level 𝑘, written 𝐷 ≡𝑘 𝐷 ′ , if they have the same history through layer 𝑘 (same events, same commitments, same order, including all intervening non-commitment events). Each ≡𝑘 is an equivalence relation; classes refine as 𝑘 increases. Definition 3.4 (Filtration). A set 𝑆 ⊆ D is a level-𝑘 support if it is a union of ≡𝑘 classes (closed under level-𝑘 agreement). Define F𝑘 ≜ {𝑆 ⊆ D | 𝑆 is a level-𝑘 support}. This yields a filtration: F0 ⊆ F1 ⊆ · · · , with F0 = {∅, D} and F𝑑 = 2 D once all determinations are distinguished. A tuple with qdepth 0 is robust (full support) or impossible (empty support); positive qdepth reflects which layer first differentiates the tuple’s membership across determinations. Observation 3.1 (Shared filtration across specifications). When a domain’s conflict structure determines a natural commitment basis Φ (ordering and abort operators for transactions; sealing and choice operators for Datalog¬ ), different specifications over that basis share a single filtration. For transactions, isolation levels (RC, SI, SER) are different resolving subsets within one filtration. For Datalog¬ , negation semantics (stratified, well-founded, stable) are different reading depths of one filtration. In both cases, the filtration is a property of the workload’s conflict or dependency structure, not of the policy imposed on it. For cross-specification comparison, we fix an ambient determination space DΦ★: the set of resolvedhistory classes generated by the basis before imposing any particular specification’s admissibility predicate. Each specification 𝐼 selects a resolving subset D𝐼 ⊆ DΦ★; we extend each support by zero outside D𝐼 , so all supports are subsets of the common carrier DΦ★ and qdepth is compared over this shared space. Remark 3.1 (Uniform layering in the instantiations). In both instantiations of this paper, commutativity is history-independent (it holds universally or not at all), so all determinations share the same layer structure: for transactions, independent ordering decisions form a single layer while cycle-breaking decisions form subsequent layers; for Datalog¬ , stratum sealing forms layers 1, . . . , 𝑘 and choice predicates form layer 𝑘+1. We exploit this uniform structure in the instantiation sections without further comment. F0 captures the coarsest distinction: D is the support of a robust outcome (holds under every determination) and ∅ is the support of an impossible one (holds under none). No layer information is needed to make this distinction. Proposition 3.1 (Filtration respects the determination semiring). Each F𝑘 is closed under ∪ and ∩, hence (F𝑘 , ∪, ∩, ∅, D) is a sub-semiring of the determination semiring for each 𝑘. Proof. Unions and intersections of unions-of-equivalence-classes are again unions-of-equivalenceclasses. □
8
Joseph M. Hellerstein
Concretely, the filtration gives each support the structure of a trie (layer 𝑘 branches conditioned on layers 1, . . . , 𝑘−1). We discuss the analogy to N[𝑋 ] universality—and its limits—in Appendix J. Proposition 3.2 (Single-layer case). When all commitments commute (a single layer), the filtration has exactly two levels (F0 = {∅, D} and F1 = 2 D ), and supports coincide with PosBool(Φ)— positive Boolean formulas over commitment variables, interpreted over valid minimal determinations. This connects to PDB lineage in Section 6. Proof. With a single layer, two determinations agree at level 1 iff they apply the same set of commitments—that is, iff they are the same determination. The level-1 equivalence classes are therefore singletons {𝐷 }. A level-1 support is any union of such singletons (by definition), which is an arbitrary subset of D; hence F1 = 2 D . Each determination corresponds to a conjunction of commitment variables (which commitments were applied); supports correspond to disjunctions of such conjunctions—exactly PosBool(Φ). □ Definition 3.5 (Query-relative depth). The query-relative depth of a tuple 𝑡 is qdepth(𝑡) ≜ min{𝑘 | supp(𝑃 (𝑡)) ∈ F𝑘 }. Proposition 3.3 (Characterization). (a) qdepth(𝑡) = 0 iff 𝑡 is robust (supp = D) or impossible (supp = ∅). (b) qdepth(𝑡) = 𝑘 iff all determinations agreeing on layers 1, . . . , 𝑘 agree on whether 𝑡 holds, but some pair agreeing on layers 1, . . . , 𝑘−1 disagrees. (c) qdepth(𝑡) = 𝑑 iff 𝑡’s presence depends on the full determination. Proof. Immediate from the definitions of F𝑘 and query-relative depth.
□
Example 3.2 (Query-relative depth for transactions). In Example 1.1, the conflict graph is acyclic, so all transaction-commit ordering commitments commute and the determination has a single layer. Value 𝑏 has qdepth(𝑏) = 0: it holds under every determination (robust). Value 𝑑 has qdepth(𝑑) = 1: its support is a proper subset of D (determinations where 𝑇𝑄 observes 𝑇2 ’s insert), which is not in F0 = {∅, D}. Classical provenance works for 𝑏; determination provenance is needed for 𝑑. Corollary 3.1 (Query evaluation respects the filtration). Under positive relational algebra: qdepth(𝑡 1 ⊲⊳ 𝑡 2 ) ≤ max(qdepth(𝑡 1 ), qdepth(𝑡 2 )) and qdepth(𝑡 1 ∪𝑡 2 ) ≤ max(qdepth(𝑡 1 ), qdepth(𝑡 2 )). Query evaluation cannot increase query-relative depth beyond the maximum depth of its inputs. Proof. Join computes supp(𝑡 1 ) ∩ supp(𝑡 2 ); union computes supp(𝑡 1 ) ∪ supp(𝑡 2 ). By Proposition 3.1, both remain in Fmax(𝑘1,𝑘2 ) . Selection by a determination-independent predicate either preserves a tuple’s support or removes the tuple entirely, hence preserves filtration membership. Projection unions supports over matching tuples; since F𝑘 is closed under union, projection preserves filtration membership. □ 4
Transactions as Semantic Ambiguity
In transactional systems, semantic ambiguity arises from conflict resolution: when concurrent transactions conflict, the system must decide which effects persist. We show that any isolation level forbidding a conflict cycle has worst-case determination depth Θ(𝑛) (in the number of transactions) given scheduling discretion—a result that holds regardless of concurrency control protocol. The filtration refines the classical incomparability of SER and SI [1] to a per-tuple depth comparison, and extends per-transaction portability analysis [32] to arbitrary provenance queries over the resulting database.
Determination Provenance: From Ambiguity to Algebra
4.1
9
Transactional Histories
Definition 4.1 (Transactional history). A transactional history is a history 𝐻 = (𝐸, →) whose event set 𝐸 contains: • begin(𝑇𝑖 ), commit(𝑇𝑖 ), abort(𝑇𝑖 ) — lifecycle events for transaction 𝑇𝑖 ; • r(𝑇𝑖 , 𝑥, 𝑣), w(𝑇𝑖 , 𝑥, 𝑣) — read and write operations by 𝑇𝑖 on object 𝑥 with value 𝑣. The partial order → records precedence: within a transaction, operations are totally ordered; across transactions, 𝑒 1 → 𝑒 2 when 𝑒 1 is known to precede 𝑒 2 (e.g., a write that a subsequent read observes). Under protocols with scheduling discretion, ordering decisions among conflicting operations are the commitment events (Section 4.2); commit and abort outcomes follow from the chosen orderings. All other events (arrivals, reads, writes) are non-commitment events; they extend the history and may introduce conflict edges but do not themselves exclude outcomes. Aborted transactions remain in 𝐸: an abort records that a conflict was resolved against that transaction. Definition 4.2 (Conflict). Two operations from distinct transactions 𝑇𝑖 ≠ 𝑇 𝑗 conflict if they access the same object 𝑥 and at least one is a write. Following Adya [1], we distinguish three conflict types: write-write (ww: both write 𝑥), write-read (wr: 𝑇𝑖 writes 𝑥, 𝑇 𝑗 reads 𝑥), and read-write (rw: 𝑇𝑖 reads 𝑥, 𝑇 𝑗 writes 𝑥; also called an anti-dependency). Definition 4.3 (Conflict graph). The conflict graph 𝐺 (𝐻 ) derived from a transactional history 𝐻 is a directed graph whose vertices are the active (uncommitted, non-aborted) transactions in 𝐻 . An ℓ
edge 𝑇𝑖 → − 𝑇 𝑗 (labeled ℓ ∈ {ww, wr, rw}) exists whenever 𝑇𝑖 and 𝑇 𝑗 conflict on some object with conflict type ℓ and 𝑇𝑖 ’s conflicting operation precedes 𝑇 𝑗 ’s in →. For an extension 𝐻 ⊑ 𝐻 ′ , the graph 𝐺 (𝐻 ′ ) omits from 𝐺 (𝐻 ) transactions that committed or aborted in 𝐻 ′ . 4.2
Commitment Basis and Specifications
Standard concurrency-control protocols all effectively order conflicting transactions: OCC via validation order, MVTO via timestamp assignment, 2PL via the time of first lock release or deadlockdriven abort. We capture this shared structure with an ordering commitment basis: Definition 4.4 (Ordering commitments). The ordering basis is Φ = {𝜑𝑇𝑖 ≺𝑇𝑗 | 𝑇𝑖 ,𝑇 𝑗 conflict}, where 𝜑𝑇𝑖 ≺𝑇𝑗 irrevocably records that 𝑇𝑖 is serialized before 𝑇 𝑗 . The transactional specification appeared in Example 2.1: 𝑂 is the set of decision traces (commit/abort events, partially ordered by conflict edges), and ⪯ is sub-trace inclusion. Following Adya [1], each isolation level 𝐿 constrains which labeled cycle patterns are admissible; Spec𝐿 (𝐻 ) admits extensions consistent with 𝐿’s constraint. We consider: read committed (RC; no constraint), serializability (SER; forbids all directed cycles regardless of edge labels), and snapshot isolation (SI; permits rw-only cycles but enforces first-committer-wins on ww edges; Appendix D.1). Example 4.1 (Running example: depth 1 under SER). Returning to Example 1.1: the conflict graph is acyclic, so all ordering commitments commute and form a single layer. Two query-outcome equivalence classes of determinations arise (we write representative members): 𝐷 in ≜ 𝜑𝑇2 ≺𝑇𝑄 ·𝜑𝑇𝑄 ≺𝑇3 (all orderings where 𝑇𝑄 observes 𝑇2 ’s insert) and 𝐷 out ≜ 𝜑𝑇2 ≺𝑇3 ·𝜑𝑇3 ≺𝑇𝑄 (orderings where 𝑑 is absent). The determination provenance is: 𝑃 (𝑏) = D × {𝑥 0 },
𝑃 (𝑑) = {(𝐷 in, 𝑥 2 )}.
𝑏 is robust (qdepth = 0); 𝑑 is contingent (qdepth = 1). Figure 1 summarizes the determination structure across isolation levels.
10
4.3
Joseph M. Hellerstein
Determination Depth by Isolation Level
Theorem 4.1 (Determination depth for transactions). The following bounds depend only on the protocol’s resolution class: (a) Under any isolation level that forbids no cycle type (e.g., read committed): depth 0. No conflict resolution is required to satisfy the isolation specification. (b) Under any isolation level 𝐿 that forbids some cycle type (serializability, snapshot isolation, repeatable read, etc.), with a fully reactive protocol (no scheduling discretion): depth 0. Every response is entailed by the current state and the arriving request. (c) Under any such 𝐿 with scheduling discretion (batching, commit-order choice, or victim selection), whose forbidden cycle pattern can be generated repeatedly around a surviving discretionary transaction: worst-case depth Θ(𝑛), where 𝑛 is the number of transactions. Per-batch depth is 2 (seal the batch; choose a processing order within it). Proof sketch. (a) If no cycle type is forbidden, validation always passes and no transaction need abort; all outcomes are ⪯-comparable. (b) A fully reactive protocol processes each event deterministically given the current state. Witness: textbook OCC (validate on commit request; abort iff cycle exists) or textbook MVTO (assign timestamp on arrival; force abort on violation). No system choice arises; depth 0. (c) Upper bound: each commitment resolves at least one transaction’s fate; with 𝑛 transactions, at most 𝑛 sequential commitments suffice. Lower bound: a long-running transaction 𝑇∞ (reading object 𝑥, writing object 𝑦) forms a two-edge rw-rw cycle with each fresh arrival 𝑇𝑖 (which writes rw rw 𝑥 and reads 𝑦): 𝑇∞ −−→ 𝑇𝑖 and 𝑇𝑖 −−→ 𝑇∞ . Each round forces a binary decision: abort 𝑇∞ (resolving all future conflicts) or abort 𝑇𝑖 (letting 𝑇∞ survive to the next round). If the system keeps 𝑇∞ alive for 𝑛−1 rounds, each round’s decision depends on the previous (had 𝑇∞ been aborted earlier, no further conflict would arise), giving depth 𝑛−1. Per-batch: within a sealed batch, the system makes a single commitment: the choice of processing order 𝜋 (a total order on pending transactions). All consequences (conflict edges, aborts, commits) are entailed by 𝜋. Hence per-batch depth is 2: seal + order selection. (Under 2PL the second layer is victim selection rather than order selection, but the seal is still needed to prevent new cycles from forming after resolution. Details in Appendix E.) □ Example 4.2 (Per-batch depth under OCC with batch validation). Three transactions 𝑇1,𝑇2,𝑇3 execute concurrently and complete their read/write phases. The system seals the batch (layer 1): no further transactions will join this validation round. It then chooses a validation order 𝜋 (layer 2) — say 𝑇1 ≺ 𝑇2 ≺ 𝑇3 . Under 𝜋, 𝑇2 ’s write set is checked against 𝑇1 ’s; if they conflict, 𝑇2 aborts (entailed by 𝜋, not a separate commitment). Choosing 𝑇2 ≺ 𝑇1 ≺ 𝑇3 instead might let 𝑇2 commit and abort 𝑇1 . The two layers do not commute: the seal determines which transactions are in the batch; the order determines which survive validation. 4.4
Per-Tuple Isolation Sensitivity
Vandevoort et al. [32] certify individual transactions as isolation-insensitive — a per-transaction result. Provenance queries over the resulting database enable a richer cut: both finer grain (a query selecting a single tuple) and cross-transaction questions (a join combining outputs of multiple transactions). The filtration’s compositionality (Corollary 3.1) guarantees that insensitivity propagates through any such query. Proposition 4.2 (SER/SI qdepth incomparability). In the Adya conflict-graph model, the following two patterns witness the two directions of SER/SI qdepth incomparability for transaction-local output tuples:
Determination Provenance: From Ambiguity to Algebra
11
Isolation / Case
Resolving determination
Depth
Read committed SER, no cycles SER, 𝑑 visible SER, 𝑑 absent SER, overlapping cycles Snapshot isolation
(none—no outcome contradicted) {𝜑𝑇1 ≺𝑇2 , 𝜑𝑇2 ≺𝑇𝑄 , . . .} (all commute) 𝜑𝑇2 ≺𝑇𝑄 · 𝜑𝑇𝑄 ≺𝑇3 𝜑𝑇2 ≺𝑇3 · 𝜑𝑇3 ≺𝑇𝑄 𝜑 a (𝑇1 ) ⊲ 𝜑 a (𝑇2 ) (Thm. 4.1c) {𝜑 snap(𝑇6 )=∅ , 𝜑 snap(𝑇7 )=∅ } ⊲ 𝜑 fcw(𝑆 (5),𝑇6 ) ⊲ 𝜑 snap(𝑇𝑄 )={··· }
0 1 1 1 𝑂 (𝑛) 𝑂 (𝑛)
𝜑𝑇𝑖 ≺𝑇 𝑗 = ordering; 𝜑 a (𝑇 ) = abort; { · · · } = commuting set; ⊲ = non-commuting sequence.
Fig. 1. Determination structure across isolation levels (Example 1.1), assuming scheduling discretion. Depth is 0 under RC or fully reactive protocols; 𝑂 (𝑛) worst-case under SER or SI with discretion (Theorem 4.1).
(a) Write skew (qdepthSER > qdepthSI ): 𝑇𝑖 is on an rw-rw cycle. SER must break the cycle (making 𝑡 contingent); SI allows it (𝑡 is robust). (b) FCW-forced abort (qdepthSI > qdepthSER ): 𝑇𝑖 has a write-write conflict with no enclosing cycle. SER commits both (ordering them; 𝑡 is robust); SI aborts one via FCW (making 𝑡 contingent). Proof. (a) 𝑇𝐴 reads 𝑥, writes 𝑦; 𝑇𝐵 reads 𝑦, writes 𝑥 (write skew). Under SI: no write-write conflict, both commit; qdepthSI (𝑡) = 0. Under SER: the rw-rw cycle is forbidden; one must abort; qdepthSER (𝑡) > 0. (b) 𝑇1 writes 𝑥 and inserts 𝑡 into a separate relation 𝑅; 𝑇2 writes 𝑥; no other conflicts. Under SER: both commit (no cycle); qdepthSER (𝑡) = 0. Under SI: FCW forces one to abort; qdepthSI (𝑡) > 0. □ Corollary 4.1 (Compositional isolation insensitivity). If every transaction contributing to a provenance query 𝑄 is isolation-insensitive, then every output tuple of 𝑄 is also isolation-insensitive: same qdepth under SER and SI. Proof. Immediate from Corollary 3.1: positive RA cannot increase qdepth beyond its inputs. □ Example 4.3 (Compositional insensitivity). Transactions 𝑇1,𝑇2,𝑇3 each insert into relations 𝑅1, 𝑅2, 𝑅3 . None participates in a write-skew or FCW pattern, so each is isolation-insensitive. A provenance query 𝑄 = 𝑅1 ⊲⊳ 𝑅2 ⊲⊳ 𝑅3 joins their outputs. The corollary guarantees that every tuple in 𝑄’s result is also insensitive—without analyzing 𝑄’s interaction with the conflict graph. This is the compositional extension of Vandevoort et al.’s [32] per-transaction certification: the filtration certifies query results, not just transactions. 5
Beyond Transactions: Negation and the Filtration
We now turn to our second instantiation. In Datalog¬ , the non-monotone operation is negation: concluding ¬𝑝 requires establishing that 𝑝 has no (further) derivation—a completeness guarantee that classical approaches handle via monus [8]. Determination provenance decomposes this into a commitment (declaring a set of derivations complete, thereby licensing negation) followed by monotone evaluation (the entailment that propagates consequences of that commitment). The payoff is twofold. First, determination provenance explains why-not under ambiguity: an atom can be absent because of a semantic commitment, not a blocked derivation. Second, the filtration’s compositionality lets one check whether a query result holds under multiple semantics by inspecting supports algebraically. (Full details in Appendix F.)
12
Joseph M. Hellerstein
Setup. Consider the program 𝑝 (𝑐) ← 𝑎(𝑐).
𝑟 (𝑐) ← ¬𝑠 (𝑐).
𝑞(𝑐) ← ¬𝑝 (𝑐).
𝑠 (𝑐) ← ¬𝑟 (𝑐).
with EDB {𝑎(𝑐)}. The stratification depth is 1: stratum 0 contains {𝑎, 𝑝}, stratum 1 contains {𝑞} (which negates 𝑝). Independently, the pair (𝑟, 𝑠) forms an unstratified cycle through negation. The specification. Outcomes assign each atom a value in {t, f, u, ⊥} (⊥ = not yet evaluated, u = genuinely ambiguous), ordered ⊥ ⪯ u ⪯ {t, f } (with t and f incomparable); outcomes are total assignments over the Herbrand base (unevaluated atoms receive ⊥), and 𝑜 1 ⪯ 𝑜 2 iff 𝑜 1 (𝑎) ⪯ 𝑜 2 (𝑎) for every atom 𝑎. The commitment basis has one sealing predicate 𝜑 seal (𝑝) (fixing 𝑝’s derivation, which licenses ¬𝑝 in 𝑞’s rule) and two choice predicates 𝜑𝑎=𝑣 (fixing a ¬-cycle atom to 𝑣 ∈ {t, f }). The specification Spec admits all assignments consistent with the program rules and EDB [11]. After all commitments are discharged, two resolved outcomes remain: 𝑜𝑟 = {𝑎(𝑐), 𝑝 (𝑐), 𝑟 (𝑐)} and 𝑜𝑠 = {𝑎(𝑐), 𝑝 (𝑐), 𝑠 (𝑐)}—the two stable models, each the minimal model of the Gelfond-Lifschitz reduct under the corresponding truth assignment. (Our choice predicates enumerate exactly the minimal models of the local GL reduct for each negative SCC; Appendix F proves the correspondence.) The resolving determinations are D = {𝐷 (𝑟 ) , 𝐷 (𝑠 ) }: 𝐷 (𝑟 ) = 𝜑 seal (𝑝) ⊲ 𝜑𝑟 (𝑐 )=t · 𝜑𝑠 (𝑐 )=f ,
𝐷 (𝑠 ) = 𝜑 seal (𝑝) ⊲ 𝜑𝑠 (𝑐 )=t · 𝜑𝑟 (𝑐 )=f ,
sharing the sealing layer (layer 1, one seal) and branching at the choice layer (layer 2). The filtration index counts discharged layers: F0 is the state before any commitment; F1 reflects the sealing layer (which all determinations share, so no new distinctions arise); and F2 reflects the choice layer where the determinations diverge. Concretely: F0 = F1 = {∅, D} (all determinations agree through layer 1) and F2 = 2 D (once the choice layer is discharged, all determinations are distinguished so all subsets are possible). 𝑃 (𝑝 (𝑐)) = D × {𝑥𝑎 } (robust) 𝑃 (𝑞(𝑐)) = {} (robustly absent)
𝑃 (𝑟 (𝑐)) = {(𝐷 (𝑟 ) , 1)} 𝑃 (𝑠 (𝑐)) = {(𝐷 (𝑠 ) , 1)}
Atoms 𝑟 (𝑐) and 𝑠 (𝑐) are contingent: each holds under exactly one determination. Under 𝐷 (𝑟 ) , 𝑠 (𝑐) is absent because of the commitment 𝜑𝑟 (𝑐 )=t itself—not a blocked derivation but a semantic choice. Reading the filtration only through the sealing layer (F1 here), these atoms have partial support—they are contingent in our terminology, which is exactly the well-founded classification u. Conversely, atoms with full or empty support are robust (WFS’s t and f respectively): their truth values are settled without discharging the choice layer. Theorem 5.1 (Negation semantics as filtration levels). For a finite Datalog¬ program whose negative SCCs admit a layered choice basis sound and complete for stable models (Appendix F.1), with 𝑘 stratification layers and 𝑑 negative SCCs in the longest dependency chain, the determination semiring has depth 𝑘+𝑑. The classical negation semantics correspond to filtration levels: (a) Stable-model semantics reads F𝑘+𝑑 (all choice layers discharged). (b) Well-founded semantics reads F𝑘 ; atoms with full or empty support are robust (WFS’s t and f); atoms with partial support are contingent (WFS’s u). (c) Stratified semantics reads F𝑘 and is defined only when 𝑑 = 0. Proof sketch. The commitment basis has 𝑘 sealing predicates followed by 𝑑 choice layers (one per negative SCC in topological order). The sealing prefix is shared by all determinations (stratified evaluation is unique), so F𝑘 = {∅, D}. Each choice layer 𝑘+𝑖 resolves SCC 𝐶𝑖 ; when SCCs interact,
Determination Provenance: From Ambiguity to Algebra
13
later choices depend on earlier outcomes, giving 𝑑 non-commuting layers and depth 𝑘+𝑑. WFS reads F𝑘 (the sealing prefix) and classifies residual ambiguity as u. Full proof in Appendix F. □ The provenance payoff is compositionality: supports compose through positive RA (Corollary 3.1), so one can check whether a query result holds under multiple semantics by inspecting supports algebraically, not re-running evaluation. Note the structural contrast: negation semantics form a chain within the filtration, while isolation levels are incomparable resolving subsets (Observation 3.1). Theorem 5.2 (Monus elimination). For any finite stratified Datalog¬ program and any naturally ordered, zero-divisor-free, 𝜔-continuous commutative semiring 𝐾: the support of every atom computed via sealing commitments over (𝐾, +, ·) equals the support computed via least fixpoint with monus over (𝐾, −) ¤ [8]. Proof. See Appendix F.
□
Sealing replaces monus: rather than subtracting provenance annotations, one commits to a stratum’s completeness (sealed-absent atoms contribute 1𝐾 ; sealed-present atoms contribute 0𝐾 ). Within each determination, derivational provenance uses ordinary positive 𝐾-evaluation. For unstratified programs, monus is undefined (no unique model to subtract against), while determination provenance remains well-defined: each stable model is a determination, and supports track which models produce each atom. 6
Consequences of the Filtration
Observation 3.1 established that different specifications over the same commitment basis share a single filtration. The preceding sections showed that isolation levels (Section 4) and negation semantics (Section 5) are both instances of this principle. We now develop two consequences: quantitative specification comparison and a connection to PDB query complexity. 6.1
Quantitative Measures
The filtration assigns each tuple a depth relative to a provenance query 𝑄 (Definition 3.1). A tuple with qdepth(𝑡) = 𝑗 is settled once layers 1, . . . , 𝑗 are discharged; layers 𝑗+1, . . . , 𝑑 were irrelevant. Proposition 6.1 (Compositional depth bound). If every input tuple of a positive relational provenance query 𝑄 has qdepth < 𝑘, then so does every output tuple (Cor. 3.1): layers 𝑘, . . . , 𝑑 are inert. Certifying this is coNP-complete in the residual width 𝑊 ≥𝑘 (by reduction from robustness, Theorem B.1), but both instantiations admit polynomial sufficient checks: in transactions, absence from 𝐿-forbidden cycles [1]; in Datalog¬ , absence of transitive dependency on any negative SCC [10]. Because different specifications over the same commitment basis share a filtration (Observation 3.1), we can compare per-tuple qdepth across specifications. Given a workload executed under specification 𝐼 (e.g., SER) and a candidate alternative 𝐼 ′ (e.g., SI), the difference decomposes into two components: Work regret. Tuples that are robust under both 𝐼 and 𝐼 ′ but have qdepth𝐼 (𝑡) > qdepth𝐼 ′ (𝑡) exhibit work regret: the extra commitment layers under 𝐼 did not change the outcome. For transactions this is bidirectional (Proposition 4.2). Semantic shift. Tuples whose support differs between 𝐼 and 𝐼 ′ — robust under one, contingent under the other — represent a genuine change in meaning, not wasted work. For transactions, write-skew and FCW patterns (Proposition 4.2) witness the shift in each direction; for Datalog¬ , shifting from stable-model to well-founded semantics converts choice-layer atoms to u.
14
Joseph M. Hellerstein
Together, work regret and semantic shift measure how much resolution each tuple costs and which tuples genuinely change semantics across specifications. 6.2
Commitment Responsibility
Work regret identifies wasted layers; determination responsibility identifies the single commitment most responsible for a tuple’s contingency. We adapt the Shapley value from cooperative game theory [19]: each commitment in the determination is a player, and the game measures how much each commitment contributes to a tuple’s contingency. The Shapley value of commitment 𝜑 for tuple 𝑡 is 𝜑’s average marginal contribution over all removal orderings (formal definition in Appendix C). In Example 4.1, responsibility is concentrated on the ordering commitments that determine whether 𝑇𝑄 observes 𝑇2 ’s insert before an effective delete. In deeper filtrations (e.g., the 𝑇∞ construction), responsibility distributes across layers: each round’s victim decision contributes a fraction of the total contingency, and the Shapley value quantifies how much. This lifts the classical tuple-level responsibility of Meliou et al. [22] from data tuples to semantic commitments: where they ask “which input tuple is most responsible for an output,” we ask “which commitment is most responsible for the output holding under this resolution.” Unifying the two into a single joint game is an open question in Appendix J. Full development, including hardness and approximation results, appears in Appendix C. 6.3 Provenance Query Complexity The filtration also connects determination provenance to the well-studied complexity landscape of probabilistic databases. Proposition 6.2 (Depth-1 = tuple-independent PDB). A depth-1 determination semiring over 𝑛 binary commitments is isomorphic to a tuple-independent PDB over 𝑛 tuple-existence events: supports are positive Boolean formulas, and query evaluation has the same complexity. At higher depths, the filtration structures the correlations: within each layer, commitments commute (giving PDB-style lineage), while cross-layer dependencies introduce conditioning. Determination provenance thus sits between tuple-independent PDBs (depth 1) and general correlated PDBs (intractable): each layer admits the PDB complexity toolkit, and depth measures how many layers must be composed. Appendix I develops transformations for reducing depth. 7 Related Work Algebraic provenance. Semiring provenance [13] and its extensions to probabilistic [30], factorized [23], and aggregate [27] settings operate after the semantic model is fixed—a single database instance with no unresolved ambiguity (depth 0 in our framework). Why-not provenance [6], causal responsibility [22], and counterfactual explanations [14] likewise condition on a single outcome. Determination provenance generalizes these by making the commitments that precede derivational provenance explicit and composable. Determination responsibility (Section 6) lifts Shapley-value attribution [19, 22] from data tuples to semantic commitments; the two games are sequential, not competing: determination responsibility attributes the resolution; tuple-level responsibility attributes the derivation under that resolution. Possible-worlds and probabilistic provenance. Probabilistic databases [30] add flat uncertainty over tuple-existence events (no non-commuting commitment layers); lineage is a Boolean formula over these events. A tuple-independent PDB is the depth-1 special case of our framework (Proposition 3.2): all commitments commute in a single layer. The filtration generalizes this to layered, non-commuting commitments; PDB tractability dichotomies [7, 30] concern formula complexity within a single layer—an orthogonal axis that applies equally within each layer of a determination.
Determination Provenance: From Ambiguity to Algebra
15
Provenance beyond the monotone fragment. Dannert et al. [8] extend semiring provenance to stratified negation within a single model; for stratifiable programs, our within-determination provenance coincides with theirs. Deutch et al. [9] and Köhler et al. [17] likewise assume a resolved semantics. Our contribution addresses unstratified negation, where multiple stable models coexist and the determination semiring tracks which models support each tuple. Provenance in systems settings. Database provenance systems (Perm [12], GProM [3], Smoke [24]) trace derivations under a fixed execution. Vandevoort et al. [32] study which transactions can run at weaker isolation while preserving serializable behavior—a cross-specification support comparison in our framework. Our framework separates semantic commitments from derivational explanation, enabling per-execution provenance to be composed across alternative resolutions (Appendix H). Other related frameworks. Ameloot et al. [2] characterize when coordination-free evaluation is possible; Hellerstein [16] develops a related complexity theory for the cost of semantic resolution. We take determinations as given and explain how query results depend on them algebraically. Arenas et al. [4] and Wijsen [33] define certain answers as tuples holding in every repair—analogous to robustness, but over flat repairs rather than layered determinations. 8
Conclusion
Determination provenance makes the commitments that resolve semantic ambiguity explicit and composable. Supports over resolving determinations form a filtered semiring; the filtration measures query-relative depth, is respected by positive relational algebra, and recovers classical provenance at depth 0. Transactions and Datalog¬ instantiate the framework; in both, classical semantic variants (isolation levels; negation semantics) correspond to different views of a shared filtration. The filtration enables quantitative diagnosis — work regret, semantic shift, and per-commitment responsibility — that goes beyond binary robustness to explain how much and why a tuple depends on each layer of resolution. This work extends algebraic data provenance to settings like transactional databases and distributed systems, where semantic ambiguity is the norm and where provenance can pay off in full. The practical implication is a recipe: given a system’s event trace, define an outcome space and refinement order that identifies the commitments. The full algebraic machinery then applies—robustness, counterfactuals, responsibility attribution, cross-specification comparison—over existing observability infrastructure. Appendix H develops this direction. Looking further ahead, the determination semiring has the structure of a probability space: D is a sample space, supports are measurable sets, and the filtration—which emerged here from the algebraic structure of commitments—is a filtration in the measure-theoretic sense (level-𝑘 supports are exactly the F𝑘 -measurable sets). Under a probability measure on D, support ratios become probabilities, work regret becomes expected regret, and responsibility becomes conditional expectation. That the algebraic structure of determination provenance lands so close to the machinery of stochastic processes suggests a deeper connection; developing it is a natural next step. The remaining appendices provide: algebraic details (Appendix A), robustness and responsibility proofs (Appendices B and C), worked examples for transactions (Appendices D and E) and Datalog¬ (Appendix F), heredity canonicalization (Appendix G), depth reduction (Appendix I), and open theory directions (Appendix J).
16
A
Joseph M. Hellerstein
Algebraic Details
This appendix develops the algebraic structures introduced in Section 3.1: first the structure within a single determination, then the determination semiring and filtration that operate across determinations. A.1
Within a Determination
A single determination of depth 𝑘 is a sequence of conditional commutative monoids connected by the sequencing operator ⊲: (𝑀1, ◦1 ) ⊲ (𝑀2, ◦2 ) ⊲ · · · ⊲ (𝑀𝑘 , ◦𝑘 ) ⊲ (𝐾, +, ·). Each 𝑀ℓ is the commutative monoid of commitments at layer ℓ: within a layer, commitments commute (Specℓ (𝐻 · 𝜑 ·𝜓 ) = Specℓ (𝐻 ·𝜓 · 𝜑)); across layers they do not, because later commitments depend on which outcomes earlier commitments eliminated. The operator ⊲ discharges one layer’s monoid and conditions the specification for the next; it is not an algebraic operation. The terminal element is the derivational semiring 𝐾 of Green et al. [13], which requires a fixed database instance. Prior to resolution, obs maps multiple admissible outcomes to different instances; after resolution, exactly one outcome remains and 𝐾-relational evaluation applies. Classical provenance is the degenerate case 𝑘 = 0: no commitment layers, just 𝐾. A.2
Support Propagation Under Relational Algebra
The set 2 D of all supports forms a commutative semiring under (∪, ∩, ∅, D): union is addition, intersection is multiplication, and distributivity holds because (2 D , ∪, ∩) is a distributive lattice. The following proposition shows that positive RA evaluation respects this structure. Proposition A.1. The supports supp(𝑃 (𝑡)) ⊆ D compose through positive relational algebra as follows (assuming 𝐾 is zero-divisor-free, as holds for N[𝑋 ] and all standard provenance semirings): (a) Join: supp(𝑃 (𝑡 1 ⊲⊳ 𝑡 2 )) = supp(𝑃 (𝑡 1 )) ∩ supp(𝑃 (𝑡 2 )). (b) Union: supp(𝑃 (𝑡 1 ) ∪ 𝑃 (𝑡 2 )) = supp(𝑃 (𝑡 1 )) ∪ supp(𝑃 (𝑡 2 )). (c) Projection/Selection: supp(𝑃 (𝜋 (𝑡))) ⊇ supp(𝑃 (𝑡)) and supp(𝑃 (𝜎 (𝑡))) ⊆ supp(𝑃 (𝑡)). Proof. (a) A join requires both premises to hold simultaneously. Under determination 𝐷, 𝑡 1 ⊲⊳ 𝑡 2 is nonempty iff both 𝑃𝐷 (𝑡 1 ) ≠ 0 and 𝑃𝐷 (𝑡 2 ) ≠ 0 (semiring multiplication has no zero divisors in N[𝑋 ]). Hence 𝐷 ∈ supp(𝑃 (𝑡 1 ⊲⊳ 𝑡 2 )) iff 𝐷 ∈ supp(𝑃 (𝑡 1 )) ∩ supp(𝑃 (𝑡 2 )). (b) A union provides alternative derivation paths. 𝑃𝐷 (𝑡 1 ∪ 𝑡 2 ) = 𝑃𝐷 (𝑡 1 ) + 𝑃𝐷 (𝑡 2 ); this is nonzero iff at least one summand is nonzero. (c) Projection can only add derivation paths (combining tuples that agree on projected attributes); selection can only remove them. □ A.3
Filtration Details
The filtration F0 ⊆ F1 ⊆ · · · ⊆ F𝑑 = 2 D is defined in Section 3.2. Here we verify that it interacts correctly with the determination semiring operations and with query evaluation. Proposition A.2 (Filtration closure under semiring operations). For any 𝑘, if 𝑆 1, 𝑆 2 ∈ F𝑘 , then 𝑆 1 ∪ 𝑆 2 ∈ F𝑘 and 𝑆 1 ∩ 𝑆 2 ∈ F𝑘 . Proof. A set is in F𝑘 iff it is a union of ≡𝑘 classes (Definition 3.3). The union of two such sets is again a union of ≡𝑘 classes. For intersection: if 𝐷 ∈ 𝑆 1 ∩ 𝑆 2 and 𝐷 ′ ≡𝑘 𝐷, then 𝐷 ′ ∈ 𝑆 1 (since 𝑆 1 ∈ F𝑘 ) and 𝐷 ′ ∈ 𝑆 2 (since 𝑆 2 ∈ F𝑘 ), so 𝐷 ′ ∈ 𝑆 1 ∩ 𝑆 2 . □
Determination Provenance: From Ambiguity to Algebra
17
Corollary A.1 (Query evaluation preserves filtration level). If supp(𝑃 (𝑡 1 )) ∈ F𝑗 and supp(𝑃 (𝑡 2 )) ∈ F𝑘 , then supp(𝑃 (𝑡 1 ⊲⊳ 𝑡 2 )) ∈ Fmax( 𝑗,𝑘 ) and supp(𝑃 (𝑡 1 ∪ 𝑡 2 )) ∈ Fmax( 𝑗,𝑘 ) . Positive RA cannot increase query-relative depth beyond the maximum depth of its inputs. B
Robustness Proofs
Theorem B.1 (Robustness is coNP-complete in width). For any instantiation where the widest layer has 𝑛 independent binary commitments, validity checking is polynomial, and query evaluation is polynomial, deciding robustness is coNP-complete. B.1
Transactional Hardness (Full Proof)
We reduce from DNF-Validity: given a DNF formula 𝜓 = 𝑡 1 ∨ · · · ∨ 𝑡 ℓ over variables 𝑥 1, . . . , 𝑥𝑛 , is 𝜓 true under every truth assignment? This problem is coNP-complete. Construction. Using the ordering basis (Section 4.2) with all transactions committing: for each variable 𝑥𝑖 , create two transactions 𝑇𝑖+ and 𝑇𝑖− , each writing to a distinct object 𝑜𝑖 . 𝑇𝑖+ writes true; 𝑇𝑖− writes false. Both are concurrent; their write-write conflict on 𝑜𝑖 creates an edge. The ordering commitment 𝜑𝑇𝑖+ ≺𝑇𝑖− or 𝜑𝑇𝑖− ≺𝑇𝑖+ determines the final value of 𝑜𝑖 (last-writer-wins). Since each pair conflicts only on its own object, no cycles arise and every combination of orderings is a valid resolving determination. The set D has 2𝑛 elements, one per truth assignment. Query. For each term 𝑡 𝑗 = ℓ1 ∧ · · · ∧ ℓ𝑚 of 𝜓 , define a conjunctive query 𝑄 𝑗 that selects a distinguished tuple 𝑡 ∗ iff the objects corresponding to the literals of 𝑡 𝑗 have the matching values. The overall query is 𝑄 = 𝑄 1 ∪ · · · ∪ 𝑄 ℓ (a union of conjunctive queries). Correctness. Under any resolving determination 𝐷, the ordering of each pair (𝑇𝑖+,𝑇𝑖− ) induces a truth assignment 𝛼 𝐷 to 𝑥𝑖 . The tuple 𝑡 ∗ is present in 𝑄’s result under 𝐷 iff 𝛼 𝐷 satisfies at least one term of 𝜓 —that is, iff 𝛼 𝐷 |= 𝜓 . Hence 𝑡 ∗ is robust (present under every 𝐷 ∈ D) iff 𝜓 is valid (true under every assignment). Polynomial conditions. Condition (i): each determination is a sequence of 𝑛 ordering commitments (polynomial-size). Condition (ii): checking validity amounts to verifying that the committed conflict graph under the chosen ordering has no forbidden cycles (trivially true here, since no cycles exist). Condition (iii): evaluating a UCQ over a polynomial-size database is in polynomial time. B.2
Datalog Hardness
The general theorem (Theorem B.1) applies directly to the Datalog¬ instantiation, providing an independent proof of coNP-hardness via the DNF-Validity reduction. Instantiation. Given 𝑛 disjoint ¬-cycles of length 2, the choice layer has 𝑛 independent binary commitments (one per cycle). The DNF-Validity gadget of the transactional proof applies verbatim: encode a DNF 𝜓 as a UCQ over the choice-induced truth values, so that the distinguished tuple is robust iff 𝜓 is valid. This yields coNP-hardness for the Datalog¬ instantiation. The result coincides with the known coNP-completeness of skeptical reasoning under stablemodel semantics [20]—the robustness question “is supp(𝑃 (𝑎)) = D?” is exactly the skeptical reasoning question “does 𝑎 hold in every stable model?” The match validates that the determination semiring’s width-based abstraction captures the right source of hardness. Polynomial conditions. Condition (i): a determination is a sequence of sealing and choice commitments, one per stratum plus one per ¬-cycle atom (polynomial-size). Condition (ii): checking that a determination produces a valid stable model requires computing the Gelfond–Lifschitz reduct [11]
18
Joseph M. Hellerstein
and verifying that the proposed model is its minimal model (polynomial time). Condition (iii): evaluating a Datalog¬ query over a fixed model is in polynomial time. C
Responsibility: Additional Results
This appendix develops determination responsibility: a Shapley-value measure of each commitment’s contribution to a contingent tuple. Fix 𝑛 independent binary commitments 𝜑 1, . . . , 𝜑𝑛 , a realized determination 𝐷 ∗ (the resolution that actually occurred), and a tuple 𝑡 with support 𝑆 ⊆ D. The presence game is the cooperative game (𝑁 , 𝑣) with player set 𝑁 = {1, . . . , 𝑛}: for a coalition 𝐶 ⊆ 𝑁 , |{𝐷 ∈ 𝑆 | 𝐷 agrees with 𝐷 ∗ on every 𝜑𝑖 , 𝑖 ∈ 𝐶}| 𝑣 (𝐶) ≜ . 2𝑛− |𝐶 | Intuitively, 𝑣 (𝐶) is the probability that 𝑡 holds when the outcomes of the commitments in 𝐶 have been revealed (matching 𝐷 ∗ ) and the remaining commitments are still unknown (uniformly random). The determination responsibility of 𝜑𝑖 is its Shapley value in this game. Theorem C.1 (Hardness). Computing determination responsibility is #P-hard, even for single-layer determinations with support given as DNF. Proof sketch. We follow the approach of [19]. Reduction from counting satisfying assignments of a monotone DNF. Given a DNF 𝜙 over variables 𝑥 1, . . . , 𝑥𝑛 , construct a determination with one binary commitment per variable and support 𝑆 = sat(𝜙). Then 𝑣 ({𝑖}) − 𝑣 (∅) requires computing |sat(𝜙 |𝑥𝑖 =𝐷𝑖∗ )|, which is #P-hard for monotone DNF [19]. □ Theorem C.2 (Tractability at bounded support treewidth). For a single-layer determination whose monotone support formula has primal-graph treewidth 𝑤, determination responsibility is computable in time 𝑂 (2𝑤 · 𝑛 2 · 𝑝 (𝑛))—FPT in 𝑤. Proof sketch. We follow the approach of [19]. Computing 𝑣 (𝐶) reduces to weighted model counting on the support formula with variables in 𝐶 fixed. On bounded-treewidth formulas, weighted model counting runs in 𝑂 (2𝑤 · 𝑝 (𝑛)) via dynamic programming on a tree decomposition [19]. The Shapley value requires 𝑂 (𝑛 2 ) such evaluations (one per coalition size and player), giving the stated bound. □ C.1
Additive Approximation
When support treewidth is unbounded, sampling provides an efficient additive approximation. Proposition C.3 (Additive approximation). For any 𝜀, 𝛿 > 0, 𝜌 (𝜑𝑖 , 𝑡) can be additively 𝜀approximated with probability ≥ 1 − 𝛿 in time 𝑂 (𝑛/𝜀 2 · log(1/𝛿) · 𝑝 (𝑛)). Proof. By standard permutation sampling of Shapley values [19, 28]: each sample draws a random permutation, fixes preceding players to 𝐷 ∗ -values, completes the rest uniformly, and measures 𝜑𝑖 ’s marginal effect. Hoeffding’s inequality gives the bound. □ C.2
Worked Example: Multi-Layer Responsibility
For depth 𝑑 > 1, responsibility is defined per layer: the responsibility of a commitment at layer 𝑘 is its Shapley value in the presence game conditioned on layers 1, . . . , 𝑘−1 being discharged. This respects non-commutativity—one does not ask “what if layer-2 commitments were resolved before layer-1?” because that is not a valid determination. Complexity per layer is the same as the single-layer case. The filtration provides the stopping criterion: if qdepth(𝑡) = 𝑘, only layers 1, . . . , 𝑘 contribute nonzero responsibility.
Determination Provenance: From Ambiguity to Algebra
19
Example C.1 (Multi-layer responsibility). Three transactions with two overlapping directed 2-cycles: 𝑇1 ⇌ 𝑇2 and 𝑇2 ⇌ 𝑇3 . Under the ordering basis, each 2-cycle requires exactly one abort. Let 𝜑 1 resolve the first cycle (abort 𝑇1 or 𝑇2 ) and 𝜑 2 resolve the second (abort 𝑇2 or 𝑇3 ). If 𝜑 1 aborts 𝑇2 , the second cycle is auto-resolved (depth 1); otherwise both commitments are needed (depth 2). Tuple 𝑡 is written by 𝑇3 ; it holds iff 𝑇3 is not aborted. The determination space is a tree (not a product): if 𝜑 1 aborts 𝑇2 , layer 2 is never discharged. 𝐷1: 𝐷2: 𝐷3:
commitments abort 𝑇2 abort 𝑇1 , abort 𝑇2 abort 𝑇1 , abort 𝑇3
outcome 𝑡 holds 𝑡 holds 𝑡 absent
Support: |supp(𝑡)| = 2 out of 3. Prior Pr[𝑡 holds] = 2/3 (uniform over determinations). Responsibility at each layer is the change in 𝑡’s conditional presence probability caused by that layer’s realized commitment: 𝜌 (𝜑𝑘 ) = Pr[𝑡 holds | layers 1. . .𝑘 fixed to 𝐷 ∗ ] − Pr[𝑡 holds | layers 1. . .(𝑘−1) fixed]. Total responsibility sums across layers to 1 − Pr[𝑡 holds] when 𝑡 holds in 𝐷 ∗ (the gain from prior uncertainty to certainty). For 𝐷 ∗ = 𝐷 2 — we observe 𝑡 holds, with both 𝑇1 and 𝑇3 surviving (aborts: 𝑇1 at layer 1, 𝑇2 at layer 2): 𝜌 (𝜑 1 ) = 1/2 − 2/3 = −1/6 (negative—keeping 𝑇2 alive reduced 𝑡’s probability from 2/3 to 1/2); 𝜌 (𝜑 2 ) = 1 − 1/2 = 1/2 (positive—directly saving 𝑇3 raised it from 1/2 to certainty). Total: −1/6 + 1/2 = 1/3 = 1 − 2/3. For 𝐷 ∗ = 𝐷 1 — we observe 𝑡 holds, with 𝑇2 aborted (resolving both cycles at layer 1): 𝜌 (𝜑 1 ) = 1 − 2/3 = 1/3, no layer-2 responsibility. The same total budget (1/3) is concentrated entirely on the single commitment that made 𝑡 certain. For 𝐷 ∗ = 𝐷 3 — we observe 𝑡 absent (𝑇3 aborted): 𝜌 (𝜑 1 ) = 1/2−2/3 = −1/6; 𝜌 (𝜑 2 ) = 0−1/2 = −1/2. Total: −1/6 + (−1/2) = −2/3 = 0 − 2/3. Both commitments bear negative responsibility for 𝑡’s absence. D
Transactional Determination Provenance: SI and Cross-Level Comparison
The body develops determination provenance for serializability in detail (Examples 1.1 and 4.1). This appendix extends the treatment to snapshot isolation (SI), where first-committer-wins (FCW) introduces a different commitment structure, and then characterizes the fine-grained separation between SER and SI in terms of query-relative depth. D.1 Snapshot Isolation Fully reactive SI: depth 0. Under a fully reactive SI implementation, snapshot assignment is deterministic (each transaction reads the committed state at its start time) and first-committer-wins (FCW) is deterministic (whichever transaction’s commit request arrives first wins on a contested object; the other aborts). All decisions are entailed by the environment; depth is 0. SI with scheduling discretion: depth 𝑂 (𝑛). When the system has discretion over commit ordering (choosing which concurrent writer commits first) or batching (choosing when to assign snapshots), depth grows to 𝑂 (𝑛) via the same structural argument as serializability. Proposition D.1 (Worst-case SI depth). Under snapshot isolation with commit-order discretion, worst-case determination depth is Θ(𝑛). Proof. The construction mirrors Theorem 4.1. Consider 𝑛 pairs of transactions (𝑇1,𝑇1′ ), (𝑇2,𝑇2′ ), . . . , (𝑇𝑛 ,𝑇𝑛′ ), where 𝑇𝑖 and 𝑇𝑖′ both write object 𝑥𝑖 (creating an FCW conflict), and 𝑇𝑖+1 reads 𝑥𝑖 before writing 𝑥𝑖+1 (so its snapshot depends on who won FCW on 𝑥𝑖 ).
20
Joseph M. Hellerstein
At each layer 𝑖, the system chooses the FCW winner on 𝑥𝑖 . This determines which version of 𝑥𝑖 appears in 𝑇𝑖+1 ’s snapshot, potentially affecting 𝑇𝑖+1 ’s write to 𝑥𝑖+1 (e.g., 𝑇𝑖+1 writes 𝑥𝑖+1 only if it reads a specific value of 𝑥𝑖 ). The FCW decision at layer 𝑖 + 1 therefore depends on the outcome at layer 𝑖: the two decisions do not commute. This chain of FCW-to-snapshot dependencies gives depth 𝑛. The upper bound (𝑛 transactions, each resolved by at most one commitment) gives 𝑂 (𝑛). □ Per-batch depth. Within a single batch of pending requests, depth is 2 (seal + commit-order selection), as in serializability (Theorem 4.1). Worked example. To illustrate FCW-induced depth concretely, consider two transactions writing the same object concurrently. Assume the database initially contains 𝑆 (5, 𝑒), and: 𝑇6 : write 𝑆 (5, 𝑒 ′ )
𝑇7 : write 𝑆 (5, 𝑒 ′′ ).
A query transaction 𝑇𝑄 reads the value of key 5 in 𝑆 after both 𝑇6 and 𝑇7 request commit. Under SI, only one of 𝑇6 or 𝑇7 can commit (FCW on key 5); the other must abort. If the system has commitorder discretion, this is a genuine commitment: choosing 𝑇6 as the FCW winner determines that 𝑇𝑄 reads 𝑒 ′ ; choosing 𝑇7 gives 𝑒 ′′ . The determination has depth 2 (seal the batch of commit requests, then choose the winner): 𝐷 SI = 𝜑 seal ⊲ 𝜑 fcw(𝑆 (5),𝑇6 ) . ′ Under 𝐷 SI , 𝑇𝑄 reads 𝑆 (5, 𝑒 ); the derivational provenance is 𝑃𝐷 SI (𝑒 ′ ) = 𝑥 6 . Under the alternative 𝜑 fcw(𝑆 (5),𝑇7 ) , 𝑇𝑄 reads 𝑆 (5, 𝑒 ′′ )—a contingent outcome. D.2
Fine-Grained Separation of SER and SI
Proposition 4.2 establishes that query-relative depth is incomparable across SER and SI. Here we develop the characterization in full. Setup. Fix a workload 𝑊 (a set of transactions with their read/write sets) and a conflict graph 𝐺 induced by 𝑊 . For each isolation level 𝐿 ∈ {SER, SI}, the determination semiring D𝐿 and filtration F0𝐿 ⊆ · · · ⊆ F𝑑𝐿 are defined over the same workload but with different admissibility constraints. A tuple 𝑡 derived from transaction𝑇𝑖 has qdepth𝐿 (𝑡) = 0 iff𝑇𝑖 commits in every resolving determination under 𝐿 (robust), and qdepth𝐿 (𝑡) > 0 iff 𝑇𝑖 ’s fate varies across determinations (contingent). Characterization. The qdepth of 𝑡 (derived from 𝑇𝑖 ) differs across levels precisely when 𝑇𝑖 participates in a conflict pattern that one level must resolve but the other does not: (a) Write skew (qdepthSER (𝑡) > qdepthSI (𝑡)): 𝑇𝑖 is on a cycle whose edges are all rw-type (anti-dependencies). SER forbids all cycles: at least one transaction on the cycle must abort, making 𝑡 contingent (qdepthSER > 0). SI allows rw-only cycles: all transactions commit in every SI determination, so 𝑡 is robust (qdepthSI = 0). (b) FCW-forced abort (qdepthSI (𝑡) > qdepthSER (𝑡)): 𝑇𝑖 has a write-write conflict with 𝑇 𝑗 on some object 𝑥, but 𝑇𝑖 and 𝑇 𝑗 are not on any cycle in 𝐺 (no serialization anomaly). Under SER: both commit (ordered on 𝑥, no cycle results); 𝑡 is robust (qdepthSER = 0). Under SI: FCW on 𝑥 forces one to abort; 𝑡 holds only if 𝑇𝑖 wins; qdepthSI > 0. Tight condition for qdepth equality. qdepthSER (𝑡) = qdepthSI (𝑡) iff 𝑇𝑖 is not involved in either pattern above: it participates in no rw-only cycle (so SER and SI agree on whether the cycle must be broken) and in no write-write conflict without an enclosing cycle (so SER and SI agree on whether both writers commit). These are exactly the transactions whose commit/abort fate is the same under both levels—the “robustly portable” transactions of [32].
Determination Provenance: From Ambiguity to Algebra
21
Compositionality. By Corollary 3.1, positive relational algebra cannot increase qdepth. Hence if all base tuples in a query have equal qdepth across SER and SI, the query result does too. A query result can have different qdepth across levels only if at least one of its base tuples participates in a write-skew or FCW pattern. This gives a sufficient condition for safe isolation-level change: if no base tuple of a query is in the SER/SI gap, the query’s provenance is identical under both levels. D.3
Certificates and Semantic-Change Queries
A certificate over-approximates a commitment’s effect: it summarizes which outcomes a commitment excludes, admitting possibly more but never fewer (formal definition in Appendix H). Under serializability, a certificate need only record ordering predicates sufficient to justify the observation. Under snapshot isolation, answering semantic-change queries—such as whether an SI outcome admits a serial explanation—requires preserving the snapshot structure itself. Certificates are query-parametric: richer questions require retaining more semantic information (Appendix H). E
Protocol-Specific Determination Structures
Theorem 4.1 establishes protocol-agnostic depth bounds via the 𝑇∞ witness. Here we show how 2PL and MVTO instantiate the ordering basis and confirm that the bounds are tight. OCC requires no separate treatment: its determination structure (seal + transaction-ordering layer) is the body’s default presentation (Example 4.2), with all conflict detection and aborts entailed by the chosen validation order. We first compare per-batch structure across all three protocols, then give protocolspecific details for 2PL and MVTO. E.1
Per-Batch Structure
2PL with batching. Under 2PL, lock acquisition and release are fully reactive (entailed by the arrival order of requests); the only discretion is victim selection when a deadlock cycle forms. Without sealing, victim choices cascade: aborting a victim releases locks, enabling new requests that may form new cycles, giving Θ(𝑛) depth. Sealing a batch (refusing new lock requests) cuts this feedback loop: all deadlock cycles in the sealed wait-for graph are present simultaneously, and victim choices across distinct cycles commute (aborting one victim cannot create a new cycle when no new edges can form). Per-batch depth: 2 (seal + one commuting layer of victim selections). OCC with batching. A batch of pending commit requests is sealed; the system then chooses a validation order. Transactions validated earlier can commit (if no cycle among already-committed); those validated later may find cycles and abort. The commit-order choice is isomorphic to 2PL victim selection: the last transaction validated on a cycle is the one that aborts. Per-batch depth: 2 (seal + ordering layer). MVTO with batching. For each batch, the system starts with existing transactions (with timestamps) and an acyclic conflict graph whose topological sort is consistent with those timestamps. The batch contains new requests (starts needing timestamp assignment, reads, writes, commit requests). The system’s only choice is the order in which to process the batch; all responses (timestamp assignments, read values, forced aborts for transactions that read between writes, commit acknowledgments) are entailed by the chosen order. Per-batch depth: 2 (seal + action-ordering layer). E.2
Two-Phase Locking (2PL)
Under strict 2PL, a transaction acquires locks before accessing objects and holds them until commit. The following details supplement the protocol-agnostic analysis above.
22
Joseph M. Hellerstein
Lock acquisition as ordering commitment. Each lock acquisition implicitly fixes a serialization ordering: if 𝑇𝑖 holds a write lock on 𝑥 and 𝑇 𝑗 requests a conflicting lock, 𝑇 𝑗 blocks until 𝑇𝑖 commits (strict 2PL holds locks until commit), irrevocably establishing 𝑇𝑖 ≺ 𝑇 𝑗 . Under the ordering basis (Section 4.2), this is exactly the ordering commitment 𝜑𝑇𝑖 ≺𝑇𝑗 . The key difference from the protocolagnostic view is distribution: ordering commitments are made incrementally as locks are acquired (throughout execution), rather than concentrated at commit time. Deadlock as forced abort. A deadlock cycle 𝑇1 → 𝑇2 → · · · → 𝑇𝑚 → 𝑇1 in the wait-for graph means the lock-acquisition commitments already made are jointly inconsistent with all transactions committing. The system resolves this by aborting one transaction (the “victim”), which is an abort commitment 𝜑 abort(𝑇𝑣 ) . The choice of victim is itself a commitment: different victims yield different determinations. Determination structure. Under strict 2PL (locks held until commit), ordering commitments made during the growing phase on distinct objects commute (when read/write sets are static, ordering 𝑇𝑖 on object 𝑥 does not affect the lock state of unrelated object 𝑦). Non-commutativity arises when deadlock forces a victim choice that affects subsequent lock availability. In the fully reactive case (deadlock detected and resolved immediately on each lock request, with the requestor as victim), all decisions are entailed and depth is 0. With victim-selection discretion, depth grows to 𝑂 (𝑛) (Theorem 4.1): deadlock cycles in the wait-for graph correspond to conflict cycles requiring resolution. E.3
Multiversion Timestamp Ordering (MVTO)
Under MVTO [25], each transaction 𝑇𝑖 receives a unique timestamp 𝑡𝑠𝑖 at start. Reads and writes are governed by the timestamp order: 𝑇𝑖 reads the latest version of 𝑥 written by a transaction with timestamp ≤ 𝑡𝑠𝑖 , and 𝑇𝑖 ’s write of 𝑥 creates a new version tagged 𝑡𝑠𝑖 . A write by 𝑇𝑖 is rejected (and 𝑇𝑖 aborted) if some transaction 𝑇 𝑗 with 𝑡𝑠 𝑗 > 𝑡𝑠𝑖 has already read an earlier version of 𝑥: 𝑇 𝑗 ’s read arrived before 𝑇𝑖 ’s write, so the system already committed to 𝑇 𝑗 seeing the old version, and 𝑇𝑖 ’s write would retroactively invalidate that commitment. Semantic commitments. In the fully reactive case (timestamps assigned on arrival), the primary commitment is timestamp assignment: assigning 𝑡𝑠𝑖 < 𝑡𝑠 𝑗 irrevocably fixes 𝑇𝑖 ≺ 𝑇 𝑗 in the serial order on every object they both access. This is an ordering commitment 𝜑𝑇𝑖 ≺𝑇𝑗 in the ordering basis (Section 4.2), with a structural property: a single timestamp assignment simultaneously fixes the ordering of 𝑇𝑖 relative to all other active transactions. With batching, the commitment is finer-grained: the system chooses a processing order over individual actions (reads, writes, starts), not just transactions. This action-level ordering subsumes timestamp assignment (timestamps are assigned when a transaction’s start or first read/write operation is processed) and determines which reads see which versions, hence which transactions are forced to abort. Forced aborts. Unlike 2PL, MVTO never blocks: conflicting operations are either served from an appropriate version (reads) or rejected immediately (writes that arrive too late—after a highertimestamped transaction has already read an earlier version). Rejection forces an abort, but this is not a free choice—it is entailed by the timestamp assignments already made. MVTO is therefore deadlock-free. Determination structure. The determination under MVTO mirrors the other protocols (seal + ordering layer) but at action granularity rather than transaction granularity. The action ordering is quotiented by commutativity of adjacent non-conflicting actions (swapping two actions on disjoint objects has no observable effect), and forced aborts add no independent commitments—they are
Determination Provenance: From Ambiguity to Algebra
23
entailed by the ordering. Fully reactive MVTO has depth 0 (timestamp assignment is entailed by environment event arrival order, and aborts are forced). With batching, per-batch depth is 2: the seal commitment (declaring the batch complete) followed by a single commitment choosing the processing order over buffered actions (one total order determines all version visibility and forced aborts). E.4
Comparison Across Protocols.
All three protocols share a common determination structure (seal + resolution layer) and the same worst-case depth bounds (Theorem 4.1): depth 0 when fully reactive, Θ(𝑛) with discretion, depth 2 per batch. They differ in commitment basis: OCC uses a transaction-ordering basis (choose a validation order); MVTO uses an action-ordering basis (choose a processing order over starts, reads and writes); 2PL uses a victim-selection basis (choose which transaction to abort on deadlock). These bases are incomparable—they record different aspects of the system’s discretion—but yield the same depth structure. F
Datalog¬ Worked Determination Provenance
This appendix instantiates determination provenance for Datalog¬ in full generality, then illustrates the machinery on a running example. We first develop the canonical commitment basis for programs with arbitrarily nested negative cycles, prove soundness and completeness, and state the general semantics-as-filtration theorem. We then show how the three classical negation semantics (stable, well-founded, stratified) are recovered as different readings of the determination semiring, and close with the monus elimination proof. Example F.1 (Running example). Consider the following program 𝑃 with EDB fact 𝑎(𝑐): 𝑝 (𝑐) ← 𝑎(𝑐).
𝑟 (𝑐) ← ¬𝑠 (𝑐).
𝑞(𝑐) ← ¬𝑝 (𝑐).
𝑠 (𝑐) ← ¬𝑟 (𝑐).
The pair (𝑃, {𝑎(𝑐)}) has a stratified fragment (𝑝, 𝑞: one stratum boundary) and a single negative SCC (𝑟 ↔ ¬𝑠). Parameters: 𝑘 = 1, 𝑑 = 1. We instantiate the general constructions on this example throughout. Throughout, we use sealing predicates 𝜑 seal (𝑋 ), which commit that the set of atoms 𝑋 is complete: no additional atoms in 𝑋 will be derived in any admissible outcome. Such predicates rule out outcomes and therefore constitute genuine semantic commitments. F.1
The Canonical Layered Choice Basis
Setup. Let 𝑃 be a finite Datalog¬ program with 𝑘 stratification layers and 𝑑 negative SCCs in the longest dependency chain after SCC condensation. Let 𝐶 1, . . . , 𝐶𝑑 be a topological ordering of the negative SCCs (if 𝐶𝑖 ’s resolution affects 𝐶 𝑗 ’s admissible models, then 𝑖 < 𝑗). SCCs that are incomparable in the DAG (no dependency path between them) have choice predicates that do not interact: neither’s rules reference the other’s atoms. Their choices therefore commute and are placed in the same determination layer. The nesting depth 𝑑 counts the longest chain of dependent SCCs, not the total number; independent SCCs at the same DAG level share a layer. Relationship to the Gelfond-Lifschitz reduct. In the original formulation [11], a candidate model 𝐼 is stable if 𝐼 equals the minimal model of the Gelfond-Lifschitz (GL) reduct 𝑃 𝐼 —the positive program obtained by (i) dropping every rule whose body contains ¬𝐶 with 𝐶 ∈ 𝐼 , and (ii) deleting all remaining negated literals. This is a global, verify-and-check definition. Our layered choice basis reformulates it constructively: once atoms outside a negative SCC 𝐶 𝑗 are fixed (by the stratified
24
Joseph M. Hellerstein
prefix and earlier SCC resolutions), the GL reduct of 𝐶 𝑗 ’s rules depends only on those fixed atoms, and its minimal models are exactly the locally stable extensions that our choice predicates enumerate. Definition F.1 (Canonical layered choice basis). The commitment basis has 𝑘 sealing predicates 𝜑 seal (𝑆 1 ), . . . , 𝜑 seal (𝑆𝑘 )—where 𝑆𝑖 is the set of atoms sealed at step 𝑖, declaring their derivations complete and licensing negation of 𝑆𝑖 -atoms in subsequent rules—followed by 𝑑 choice layers: layer 𝑘+𝑖 contains choice predicates that select a local stable extension of 𝐶𝑖 , applied after all layers 𝑘+1, . . . , 𝑘+𝑖−1 are discharged. Sealing predicates do not commute across dependent strata (sealing 𝑆𝑖 is a prerequisite for evaluating rules that negate 𝑆𝑖 -atoms); within a single choice layer, choice predicates commute. A resolving determination takes the form 𝐷 ≜ 𝜑 seal (𝑆 1 ) ⊲ · · · ⊲ 𝜑 seal (𝑆𝑘 ) ⊲ 𝜑𝐶1 ⊲ · · · ⊲ 𝜑𝐶𝑑 , where 𝜑𝐶 𝑗 denotes the (commuting) set of choice predicates that resolve SCC 𝐶 𝑗 . The determination depth is 𝑘+𝑑. Proposition F.1 (Soundness and completeness). For finite Datalog¬ programs whose negative SCCs admit the layered choice decomposition of Definition F.1 (each SCC has finitely many local stable extensions given its fixed context, and composing local extensions in topological order is sound and complete for global stable models), the canonical layered choice basis is sound and complete: each resolving determination produces a stable model, and every stable model is produced by exactly one resolving determination. Proof. The full GL reduct decomposes along the SCC DAG: once atoms outside 𝐶𝑖 are fixed, the reduct of 𝐶𝑖 ’s rules depends only on those fixed atoms. Soundness: composing local stable extensions in topological order yields a global stable model (each local extension is a minimal model of its local reduct; their composition is a minimal model of the full reduct). Completeness: given a stable model 𝑀, define 𝐷 𝑀 by taking the shared sealing prefix 𝜑 seal (𝑆 1 ) ⊲ · · · ⊲ 𝜑 seal (𝑆𝑘 ) followed by the choice 𝜑𝐶𝑖 = 𝑀 |𝐶𝑖 at each layer 𝑘+𝑖. Local minimality of 𝑀 |𝐶𝑖 follows from global minimality of 𝑀 (a smaller local model would give a smaller global one). The map 𝑀 ↦→ 𝐷 𝑀 is injective. □ Instantiation (Example F.1). With 𝑘 = 1 (one seal: 𝑆 1 = {𝑝}) and 𝑑 = 1 (one SCC: {𝑟, 𝑠}), the two resolving determinations are: 𝐷 (𝑟 ) ≜ 𝜑 seal (𝑆 1 ) ⊲ 𝜑𝑟 (𝑐 )=t · 𝜑𝑠 (𝑐 )=f ,
𝐷 (𝑠 ) ≜ 𝜑 seal (𝑆 1 ) ⊲ 𝜑𝑠 (𝑐 )=t · 𝜑𝑟 (𝑐 )=f .
Depth = 𝑘+𝑑 = 2. F.2
Negation Semantics as Filtration Levels
Theorem F.2 (General negation semantics as filtration levels). For a finite Datalog¬ program satisfying the layered-choice decomposition of Proposition F.1, with 𝑘 stratification layers and nesting depth 𝑑, the determination semiring under the canonical layered choice basis (Definition F.1) has depth 𝑘+𝑑. The semantics correspondence is: (a) Stable-model semantics reads F𝑘+𝑑 : all choice layers discharged, yielding a two-valued model. (b) Well-founded semantics reads F𝑘+𝑑 ∗ where 𝑑 ∗ ≤ 𝑑 is the number of consecutive choice layers (starting from 𝑘+1) whose resolution is forced (uniquely determined by the preceding prefix). Atoms with full or empty support are robust (WFS’s t and f); atoms with partial support are contingent (WFS’s u). (c) Stratified semantics reads F𝑘 : defined only when no negative cycles exist (𝑑 = 0).
Determination Provenance: From Ambiguity to Algebra
25
Proof. Depth 𝑘+𝑑. The 𝑘 sealing layers are shared by all resolving determinations (uniqueness of stratified evaluation). Each choice layer 𝑘+𝑖 resolves the atoms in 𝐶𝑖 ; since 𝐶𝑖 ’s rules reference atoms in earlier cycles, the choices available at layer 𝑘+𝑖 depend on the outcomes of layers 𝑘+1, . . . , 𝑘+𝑖−1. Hence layers 𝑘+1, . . . , 𝑘+𝑑 do not commute in general, giving depth 𝑘+𝑑. (a) Stable models. Each resolving determination 𝐷 discharges all 𝑘+𝑑 layers, producing a unique two-valued assignment—a stable model. Conversely, every stable model corresponds to a resolving determination. Hence stable models biject with D, and stable-model semantics reads F𝑘+𝑑 = 2 D . (b) Well-founded semantics. WFS applies the alternating fixpoint [31] after the sealing prefix. At each choice layer 𝑘+𝑖, the alternating fixpoint checks whether 𝐶𝑖 has a unique stable extension given the discharged prefix. If so, that layer is forced and WFS discharges it. If not, 𝐶𝑖 ’s atoms are classified as u and WFS stops discharging further layers that depend on 𝐶𝑖 . Let 𝑑 ∗ be the number of consecutive forced layers starting from 𝑘+1. WFS reads F𝑘+𝑑 ∗ : atoms resolved by layers 1, . . . , 𝑘+𝑑 ∗ have full or empty support (t or f); atoms depending on layers 𝑘+𝑑 ∗ +1, . . . , 𝑘+𝑑 have partial support (u). In the restricted case of Theorem 5.1 (𝑑 = 1, independent cycles), 𝑑 ∗ = 0 and WFS reads F𝑘 . (c) Stratified semantics. When 𝑑 = 0, the sealing prefix resolves all atoms. |D | = 1 and F𝑘 = {∅, D}. □ The alternating fixpoint as entailment. The distinction between the alternating fixpoint and a commitment is: a commitment operates on 2𝑂 (replacing the admissible set with a subset); the alternating fixpoint operates on 𝑂 via ⪯ (refining the observed outcome upward without excluding alternatives). It is the specification’s choice of ⪯ that makes the alternating fixpoint an entailment rather than a commitment. Provenance structure. For atoms determined by the stratified prefix, all resolving determinations agree: conditioned provenance is classical. For atoms in negative SCCs, determination provenance records which resolving determination is assumed; only after this choice does ordinary derivational provenance apply. WFS does not select a determination; it reports contingent atoms as u. But the determination semiring retains the full contingency structure: the support records exactly which determinations make each atom hold. This is not provenance—provenance requires resolution (Theorem 2.1)—but a property of the determination provenance function, read at filtration level 𝑘 without selecting a determination. Example F.2 (Nested cycles). Consider: 𝑎 ← ¬𝑏. 𝑏 ← ¬𝑎. 𝑐 ← 𝑎, ¬𝑑. 𝑑 ← ¬𝑐. with EDB ∅. The (𝑎, 𝑏) cycle is at layer 𝑘+1; the (𝑐, 𝑑) cycle is at layer 𝑘+2 (it depends on 𝑎). When 𝑎 = t, the (𝑐, 𝑑) cycle has two stable extensions ({𝑎, 𝑐} and {𝑎, 𝑑 }); when 𝑏 = t, 𝑐 cannot be derived so 𝑑 = t is forced—giving three stable models total. WFS: the alternating fixpoint cannot force (𝑎, 𝑏) (both extensions are consistent), so 𝑑 ∗ = 0 and all four atoms are u. If we add the rule 𝑎 ← . (making 𝑎 true by derivation), then (𝑎, 𝑏) is forced (𝑎 = t, 𝑏 = f), so 𝑑 ∗ = 1; WFS then evaluates (𝑐, 𝑑) and finds it unforced, giving 𝑐 = 𝑑 = u. F.3
Worked Instantiation (Example F.1)
We trace the three semantics through the running example (𝑘 = 1, 𝑑 = 1, D = {𝐷 (𝑟 ) , 𝐷 (𝑠 ) }). Stable models. The two stable models are 𝑜𝑟 = {𝑎, 𝑝, 𝑟 } and 𝑜𝑠 = {𝑎, 𝑝, 𝑠}. Provenance: 𝑃𝐷 (𝑟 ) (𝑟 (𝑐)) = 1, 𝑃𝐷 (𝑠 ) (𝑠 (𝑐)) = 1, 𝑃𝐷 (𝑟 ) (𝑝 (𝑐)) = 𝑃𝐷 (𝑠 ) (𝑝 (𝑐)) = 𝑥𝑎 (the EDB annotation of 𝑎(𝑐)). Well-founded semantics. The stratified prefix determines 𝑝 (𝑐) = t (robust), 𝑞(𝑐) = f (robustly absent). The ¬-cycle atoms have partial support: 𝑃 (𝑟 (𝑐)) = {(𝐷 (𝑟 ) , 1)}, 𝑃 (𝑠 (𝑐)) = {(𝐷 (𝑠 ) , 1)}. WFS reports 𝑟 (𝑐) = 𝑠 (𝑐) = u (contingent).
26
Joseph M. Hellerstein
Adding the rule 𝑑 (𝑐) ← 𝑟 (𝑐); 𝑑 (𝑐) ← 𝑠 (𝑐) gives supp(𝑃 (𝑑 (𝑐))) = {𝐷 (𝑟 ) } ∪ {𝐷 (𝑠 ) } = D: full support, read off algebraically without iterative fixpoint. Stratified semantics. The stratified fragment (𝑝, 𝑞) is resolved by the sealing prefix alone: 𝑃𝐷 strat (𝑝 (𝑐)) = 𝑃 (𝑎(𝑐)). The cycle (𝑟, 𝑠) is outside its scope. Cross-semantics comparison. 𝑝 (𝑐) has full support—it holds under every stable model, is robust under WFS, and is derived by stratified evaluation. 𝑟 (𝑐) has partial support ({𝐷 (𝑟 ) }): it holds under one stable model, is contingent (u) under WFS, and is undefined under stratified semantics. F.4
Proof of Monus Elimination (Theorem 5.2)
Let 𝑃 be a finite stratified Datalog¬ program with stratification 𝑆 0, 𝑆 1, . . . , 𝑆𝑘 (where 𝑆 0 is the EDB stratum), and let (𝐾, +, ·, 0𝐾 , 1𝐾 ) be a naturally ordered, zero-divisor-free, 𝜔-continuous commutative semiring. The zero-divisor-free condition (𝑎 · 𝑏 = 0𝐾 implies 𝑎 = 0𝐾 or 𝑏 = 0𝐾 ) is satisfied by all semirings commonly used in provenance: N[𝑋 ] (the provenance polynomials of Green et al. [13]), PosBool[𝑋 ], the Viterbi semiring, the tropical semiring, and the access-control semiring—but not by semirings with absorbing elements such as ({0, 1, . . . , 𝑘 }, max, min, 0, 𝑘) for finite 𝑘 > 1. The 𝜔-continuity condition (directed suprema distribute over + and ·) is the standard assumption for datalog fixpoint semantics over semirings [8, 13]; it holds for all the semirings above. We prove that for every derived atom 𝑎, the support of 𝑎 (the set of determinations under which 𝑎’s annotation is nonzero) is the same whether negation is handled via sealing or via monus. Setup. Fix a single resolving determination 𝐷. Under 𝐷, the specification is resolved: there is a unique outcome (a model of the program), and classical semiring provenance [13] assigns each atom 𝑎 an annotation 𝑃𝐷 (𝑎) ∈ 𝐾 recording how 𝑎 is derived from EDB facts. The question is how to compute 𝑃𝐷 (𝑎) when the program contains negation. Both strategies below produce a 𝐾-annotation for every atom; they differ only in how negated literals are handled. We compare them and show they agree on the zero/nonzero distinction. Definitions. We recall the two evaluation strategies. Both proceed bottom-up through the stratification, computing a least fixpoint at each stratum over (𝐾, +, ·). EDB atoms are annotated by their base semiring labels (or 0𝐾 if absent); positive body literals contribute their annotation multiplicatively (as in standard 𝐾-relational evaluation [13]); alternative derivations (multiple rules for the same head) combine additively. The strategies differ only in the annotation assigned to a negated literal ¬𝑏 𝑗 appearing in a rule body, where 𝑏 𝑗 is in some lower stratum whose fixpoint has already been computed. Sealing evaluation. After stratum 𝑖’s fixpoint stabilizes, seal it. At this point, standard 𝐾-relational evaluation [13] has assigned each atom 𝑏 in stratum 𝑖 a semiring value—call it val(𝑏) ∈ 𝐾—which is a polynomial in the EDB annotations (in N[𝑋 ]) or more generally an element of 𝐾 built from the base annotations via + and ·. This is the familiar provenance polynomial of 𝑏; it equals 0𝐾 iff 𝑏 is not derivable from the EDB. For a rule in stratum 𝑖+1 containing ¬𝑏 𝑗 (with 𝑏 𝑗 in stratum ≤ 𝑖, already sealed), the negated literal contributes: ( 1𝐾 if val(𝑏 𝑗 ) = 0𝐾 (atom absent from the model), ⟦¬𝑏 𝑗 ⟧seal ≜ 0𝐾 if val(𝑏 𝑗 ) ≠ 0𝐾 (atom present). That is, a successful negation contributes 1𝐾 (the multiplicative identity—it does not block the derivation) and a failed negation contributes 0𝐾 (killing the rule’s contribution).
Determination Provenance: From Ambiguity to Algebra
27
Monus evaluation [8]. The same bottom-up fixpoint computation, but the negated literal contributes: ⟦¬𝑏 𝑗 ⟧monus ≜ 1𝐾 −¤ val(𝑏 𝑗 ), where −¤ is the monus (truncated subtraction) of 𝐾, defined by 𝑎 −¤ 𝑏 ≜ max{ 𝑐 ∈ 𝐾 | 𝑏 + 𝑐 ≤ 𝑎 } in the natural order ≤ (where 𝑥 ≤ 𝑦 iff ∃𝑑. 𝑥 +𝑑 = 𝑦). Here val(𝑏 𝑗 ) is the same provenance polynomial as in the sealing case—the two strategies compute the same fixpoint for positive rules and differ only in how they interpret ¬𝑏 𝑗 . Key lemma. The only non-obvious step is showing that monus against 1𝐾 acts as a zero-test— the same behavior as sealing. The tricky aspect of monus is that 1𝐾 −¤ 𝑣 could in principle be some nonzero value less than 1𝐾 when 𝑣 ≠ 0𝐾 ; the zero-divisor-free condition rules this out. (For the Boolean support abstraction PosBool[𝑋 ], where all nonzero elements are ≥ 1𝐾 , the result is immediate; the lemma below provides the stronger algebraic condition covering all standard provenance semirings.) Lemma F.1. In a naturally ordered, zero-divisor-free, 𝜔-continuous commutative semiring 𝐾: 1𝐾 −𝑣 ¤ = 1𝐾 if 𝑣 = 0𝐾 , and 1𝐾 −¤ 𝑣 = 0𝐾 if 𝑣 ≠ 0𝐾 . Proof. The case 𝑣 = 0𝐾 is immediate: max{𝑐 | 𝑐 ≤ 1𝐾 } = 1𝐾 . For 𝑣 ≠ 0𝐾 : suppose for contradiction that 𝑐 ≠ 0𝐾 satisfies 𝑣 +𝑐 ≤ 1𝐾 . Since 𝑣, 𝑐 ≤ 1𝐾 , monotonicity gives 𝑣𝑐 ≤ 𝑣 and 𝑣𝑐 ≤ 𝑐, so 𝑣𝑐 + 𝑣𝑐 ≤ 𝑣 + 𝑐 ≤ 1𝐾 . Zero-divisor-freeness gives 𝑣𝑐 ≠ 0𝐾 . Squaring preserves both properties (𝑤 ≠ 0𝐾 and 𝑤 + 𝑤 ≤ 1𝐾 imply 𝑤 2 ≠ 0𝐾 and 𝑤 2 + 𝑤 2 ≤ 1𝐾 ), so repeated 𝑛 squaring yields a descending chain (𝑣𝑐) 2 , all nonzero, all satisfying 𝑤 + 𝑤 ≤ 1𝐾 . By 𝜔-continuity ∞ this chain has an infimum 𝑒 = (𝑣𝑐) 2 , still nonzero, with 𝑒 2 = 𝑒 and 𝑒 + 𝑒 ≤ 1𝐾 . We claim 𝑒 = 1𝐾 : write 𝑒 + 𝑓 = 1𝐾 ; if 𝑓 ≠ 0𝐾 then 𝑒 𝑓 ≠ 0𝐾 (zero-divisor-free) and 𝑒 𝑓 + 𝑒 𝑓 ≤ 𝑒 + 𝑓 = 1𝐾 , so 𝑒 𝑓 is another nonzero element below 𝑒 satisfying the same bound—contradicting 𝑒 being the infimum. So 𝑓 = 0𝐾 and 𝑒 = 1𝐾 . But then 1𝐾 + 1𝐾 ≤ 1𝐾 implies 0𝐾 ≥ 1𝐾 , a contradiction. □ Main argument. Given the lemma, the two strategies assign the same zero/nonzero value to every negated literal (both yield 1𝐾 when the atom is absent, 0𝐾 when present). Since positive evaluation is identical in both strategies, and 𝐾 is zero-divisor-free (a product is nonzero iff all factors are; a sum is nonzero iff some summand is), a straightforward induction on strata shows that every atom has the same zero/nonzero provenance value under sealing and monus. Supports (the zero/nonzero distinction across determinations) therefore agree. □ Remark F.1. Under the assumptions of the theorem (zero-divisor-free, 𝜔-continuous), the lemma shows that monus and sealing assign identical values to negated literals—both collapse to {0𝐾 , 1𝐾 }— so no quantitative information is lost. If one relaxes zero-divisor-freeness (e.g., the bounded semiring ({0, . . . , 𝑘 }, max, min, 0, 𝑘)), monus can assign intermediate values 1𝐾 −¤ 𝑣 ∉ {0𝐾 , 1𝐾 }, encoding a quantitative residual that sealing discards. Whether this residual can be captured within the determination framework—perhaps via a richer commitment structure that records how much of a derivation was overcome, not merely whether it was present—is an open question (Appendix J). G
Heredity Canonicalization
A commitment is hereditary if the outcomes it excludes stay excluded as the history grows: once ruled out, an outcome never becomes admissible again. This is a natural monotonicity property— commitments should be irrevocable—but not all commitment bases satisfy it syntactically. For example, a commitment “proposal 𝐴 wins the vote based on the majority so far” excludes outcomes where 𝐴 loses; but if new voters submit ballots, the majority can flip, and the exclusion no longer holds. The commitment’s effect depends on context that has not yet stabilized. We care about
28
Joseph M. Hellerstein
heredity because it guarantees that the admissible set shrinks monotonically along any history extension, which simplifies reasoning about determination structure: one need not worry that a later event could “undo” an earlier commitment’s exclusion. We show that heredity is without loss of generality in the retrospective setting: any nonhereditary commitment basis can be transformed into a hereditary one (i.e., one where 𝑜 ∉ Spec(𝐻 1 · 𝜑) ⇒ 𝑜 ∉ Spec(𝐻 2 · 𝜑) for all 𝐻 1 ⊑ 𝐻 2 ) that preserves not only resolved outcomes but the full determination structure—the same set D, the same supports, the same filtration, and the same 𝐾-valued provenance annotations. Definition G.1 (Dependency set). The dependency set of a commitment 𝜑 at history 𝐻 is the set of events 𝑆 ⊆ 𝐸 (𝐻 ) whose presence or absence affects which outcomes 𝜑 excludes. Formally, 𝑆 is minimal such that 𝜑’s exclusion set is determined by 𝑆 ∩ 𝐸 (𝐻 ) for all 𝐻 . Definition G.2 (Sealing commitment). For a set of events 𝑆, the sealing commitment 𝜑 seal(𝑆 ) declares that 𝑆 is complete: it excludes outcomes that are admissible only if additional events of the types in 𝑆 occur. Proposition G.1 (Heredity canonicalization preserves determination structure). Let 𝜑 be a non-hereditary commitment with dependency set 𝑆, applied at history 𝐻 within a completed history 𝐻 ∗ (so that 𝑆 has stabilized: no further events of types in 𝑆 occur in any extension within 𝐻 ∗ ). Write Spec𝐻 ∗ (𝐻 ′ ) for the admissible set at 𝐻 ′ conditioned on the completed history 𝐻 ∗ (i.e., restricted to outcomes consistent with 𝐻 ∗ ’s event structure). Define the replacement: 𝜑 seal(𝑆 ) followed by the deterministic function 𝑓𝜑 that computes 𝜑’s effect over the sealed state (an entailment, not a commitment). Then: (a) 𝜑 seal(𝑆 ) is hereditary. (b) The seal is non-filtering at 𝐻 relative to 𝐻 ∗ : Spec𝐻 ∗ (𝐻 · 𝜑 seal(𝑆 ) ) = Spec𝐻 ∗ (𝐻 ) (since 𝑆 has already stabilized within 𝐻 ∗ , the seal excludes no outcome that was previously admissible). (c) The entailment 𝑓𝜑 reproduces 𝜑’s exclusions exactly: Spec𝐻 ∗ (𝐻 · 𝜑 seal(𝑆 ) · 𝑓𝜑 ) = Spec𝐻 ∗ (𝐻 · 𝜑). (d) The remainder of the determination is unchanged: for any subsequent commitments 𝜑 2 · 𝜑 3 · · · , Spec𝐻 ∗ (𝐻 · 𝜑 seal(𝑆 ) · 𝑓𝜑 · 𝜑 2 · 𝜑 3 · · · ) = Spec𝐻 ∗ (𝐻 · 𝜑 · 𝜑 2 · 𝜑 3 · · · ). (e) The canonicalization preserves the set of resolving determinations D, all supports, the filtration, and all 𝐾-valued provenance annotations. Proof. (a) Once 𝑆 is declared complete, that declaration holds at all extensions (the seal event cannot be retracted). Any outcome excluded by sealing remains excluded: heredity holds. (b) Since 𝐻 ⊑ 𝐻 ∗ and 𝑆 has stabilized within 𝐻 ∗ , no further 𝑆-type events will arrive. The seal declares complete a set that is already complete; it excludes no outcome that was previously admissible. Hence Spec𝐻 ∗ (𝐻 · 𝜑 seal(𝑆 ) ) = Spec𝐻 ∗ (𝐻 ). (c) Non-heredity of 𝜑 arose because its exclusion set depended on which events in 𝑆 had occurred. After sealing, 𝑆 ∩ 𝐸 (𝐻 ) is fixed; 𝜑’s effect is a deterministic function of this fixed set. The entailment 𝑓𝜑 computes exactly this function, producing the same exclusion set as 𝜑. Combined with (b): Spec𝐻 ∗ (𝐻 ) = Spec𝐻 ∗ (𝐻 · 𝜑 seal(𝑆 ) ), so 𝑓𝜑 applied to Spec𝐻 ∗ (𝐻 ) gives Spec𝐻 ∗ (𝐻 · 𝜑). (d) By (c), 𝜑 2 sees the same admissible set Spec𝐻 ∗ (𝐻 · 𝜑) in both cases. Since 𝜑 2 ’s effect depends only on the admissible set at its point of application, it behaves identically. By induction on the remaining commitments, the entire tail is unchanged. (e) By (d), each resolving determination 𝐷 in the original basis maps to a determination in the canonicalized basis that produces the same admissible set at every point. The resolved outcome is identical; hence supports supp(𝑃 (𝑡)) are identical for every tuple 𝑡. Since supports are preserved, the filtration (defined over supports) is preserved. Since the resolved outcome under each 𝐷 is the
Determination Provenance: From Ambiguity to Algebra
29
same fixed instance, classical semiring provenance over that instance yields the same 𝐾-valued annotations. □ The key insight is that in the retrospective setting, the seal is a non-filtering guard (the dependency set has already stabilized, so no outcome is excluded at the point of application), and the entailment is not a commitment (it excludes nothing beyond what 𝜑 would have excluded). The replacement is therefore invisible to the rest of the determination: subsequent commitments see the same admissible set, commutativity relations are unchanged, and the layer structure is preserved. Heredity is without loss of generality for the retrospective analysis that determination provenance performs. H
Systems Directions
Algebraic data provenance [13] offers powerful compositional analysis—robustness, counterfactuals, quantitative attribution—but applies only after semantics is fixed: a single database, a single execution, a single model. Systems observability (distributed tracing [29], workflow provenance [26]) is broadly deployed but expressively weak: it records which events occurred, not how they combined or whether the outcome would survive a different execution. Determination provenance bridges the two. Here we sketch some opportunities and open problems. From traces to algebraic provenance. Standard systems traces are histories in our sense: partially ordered event records. The only additional modeling step is to define an outcome space 𝑂 and refinement order ⪯ (e.g., consistent serializations ordered by sub-trace inclusion). The commitment events—those that narrow the admissible set—are then determined in principle, though identifying them efficiently requires domain structure (conflict graphs, dependency annotations) rather than brute-force comparison of Spec(𝐻 ) before and after each event; developing general-purpose extraction algorithms is an open problem. The layer structure follows from the specification and the identified commitments. Once the determination is extracted, the full algebraic machinery applies to the trace: supports give robustness and fragility; the filtration gives depth bounds and layer-specific diagnosis; responsibility attributes root causes to individual commitments; cross-specification comparison answers “what if” questions about alternative policies. The framework applies whenever provenance queries can be expressed in positive RA over the observation function—including semi-structured settings (select, filter, join over trace spans or log entries). The determination also compresses: rather than retaining every intermediate state, the system stores only the commitment sequence and reconstructs derivational detail on demand. As a concrete example: in distributed tracing [29], unsynchronized clocks leave the relative ordering of concurrent spans ambiguous. A determination commits to clock alignments between hosts, fixing a single timeline. The support of a critical-path predicate then answers questions that current tracing cannot: is the database robustly on the critical path (full support), or only under certain clock assumptions (partial support)? Or one could ask a counterfactual: if the clock alignment had gone differently (a different determination in the same D), would the ad server rather than the database have been the bottleneck? The support supp(𝑃 (cp = 𝐴)) answers this directly. Quantitative fragility and scheduler design. The support ratio |supp(𝑃 (𝑡))|/|D | measures outcome fragility structurally—from the commitment basis and conflict graph rather than from repeated execution. Computing it exactly requires enumerating D (exponential in general), but compact representations (Boolean formulas at depth 1; factorized supports at higher depths) and the Shapleyvalue approximation of Appendix C make tractable estimates feasible for bounded-treewidth conflict structures. Given a determination structure extracted from prior runs—and assuming the workload’s
30
Joseph M. Hellerstein
conflict structure is stable across runs—a scheduler could minimize maximum responsibility for an SLA predicate by avoiding the high-responsibility commitments (e.g., preferring orderings that keep fragile tuples robust). This is a new optimization objective: optimize across the space of determinations rather than within a single execution. Parsimony: truncation and certificates. A full determination may record far more than any particular query needs. Two orthogonal dimensions of compression apply. Vertical parsimony (truncation). The filtration tells us which layers matter: if a query family depends only on tuples with qdepth ≤ 𝑘, layers 𝑘+1, . . . , 𝑑 are irrelevant and can be discarded from the stored determination. For a depth-𝑑 determination with 𝑛 commitments per layer, this reduces the stored commitment sequence from 𝑂 (𝑛𝑑) to 𝑂 (𝑛𝑘). Horizontal parsimony (certificates). Within a retained layer, the full commitment may carry more detail than the query requires. We envision a certificate for commitment 𝜑: a predicate 𝐶 that over-approximates 𝜑’s effect. It must satisfy Spec(𝐻 · 𝜑) ⊆ {𝑜 | 𝐶 (𝑜)} (soundness—every outcome that 𝜑 retains is also retained by 𝐶), but may admit additional outcomes that 𝜑 would have excluded. A certificate is sufficient for a query family Q if replacing 𝜑 with 𝐶 yields the same query answers. The space savings come from the gap between the full commitment (which may encode an entire conflict graph or the complete state of a stratum) and the minimal certificate (which need only record the aspects relevant to Q—e.g., the ordering predicates in a tuple’s conflict neighborhood rather than the full serialization order). Richer queries require stronger certificates: derivational provenance needs only local conflict information, while cross-specification queries need the full conflict-graph structure. Together, truncation and certificates define a parameterized design space for parsimonious determination storage; fixing the parameters—choosing the query family, computing minimal certificates, implementing adaptive retention—is the systems work that remains. I
Depth Reduction: Bounding Determination Complexity
The filtration measures determination complexity: a specification with depth 𝑑 requires 𝑑 sequential, non-commuting commitment decisions to resolve. High depth means long chains of dependent decisions — each contingent on the previous — and correspondingly high resolution cost. A natural question: given a specification with depth 𝑑, how can we reduce it to a target depth 𝑑 ∗ < 𝑑? We identify three mechanisms for depth reduction, each corresponding to a different structural change to the specification or its commitment basis. Definition I.1 (Depth reduction mechanisms). Let Spec have depth 𝑑 under commitment basis Φ. A depth reduction to 𝑑 ∗ < 𝑑 is achieved by one of: (i) Coarsening ⪯: enlarge the outcome order to ⪯′ ⊇⪯ so that outcomes distinguished by some layer 𝑘 become ⪯′ -comparable. Layer 𝑘’s commitments become unnecessary (nothing to choose among) and the layer is eliminated. (ii) Commutation: impose additional structure so that commitments in adjacent layers 𝑘 and 𝑘+1 commute. The two layers merge into one, reducing depth by one. (iii) Entailment: replace a layer-𝑘 commitment with a deterministic function of the discharged prefix (an entailment). The decision is no longer discretionary; the layer is eliminated. Each mechanism has a cost: (i) weakens the specification (more outcomes are considered equivalent); (ii) restricts the commitment basis (decisions lose independence); (iii) removes discretion (the system commits to a policy). The filtration diagnoses where depth arises and which mechanism applies at each layer.
Determination Provenance: From Ambiguity to Algebra
31
Example I.1 (Transactional depth reduction). The 𝑇∞ construction (Theorem 4.1) has depth Θ(𝑛): each round’s victim decision depends on the previous. The three mechanisms yield different bounded-depth protocols: • Coarsening (SER → SI): the rw-rw cycle that forced victim selection is no longer forbidden under SI. The layer that broke the cycle is eliminated; depth drops for tuples involved in write-skew patterns. • Commutation (commutative basis rewriting): replace non-commutative commitments with globally commutative variants. For example, replace cycle-based victim selection (𝜑 abort(𝑇𝑣 ) , whose effect depends on which other aborts have already occurred—non-commutative) with per-transaction age-based abort predicates (𝜑 abort-if-old(𝑇𝑖 ) : abort 𝑇𝑖 if its age exceeds a threshold). The age predicates commute unconditionally (each depends only on its own transaction’s metadata), so all abort decisions collapse into a single layer. The cost: the rewritten basis may abort transactions that precise victim selection would have spared—a semantic change, but one that buys global commutativity and reduces depth from Θ(𝑛) to 1. • Entailment (reactive protocol): process each event deterministically given the current state (e.g., OCC: validate on commit, abort if cycle exists; MVTO: assign timestamp on arrival, abort on violation). No system choice arises; victim selection is entailed by the protocol and the arriving request. Depth drops to 0. Example I.2 (Datalog¬ depth reduction). A program with 𝑘 stratification layers and 𝑑 nested negative SCCs has depth 𝑘+𝑑 (Theorem 5.1). • Coarsening (stable → well-founded): enlarge ⪯ so that u refines to both t and f. The choice layers become unnecessary (all outcomes are ⪯′ -comparable); depth drops from 𝑘+𝑑 to 𝑘. • Commutation (conservative choice): dependent SCC-resolution choices do not commute (𝐶 𝑗 ’s choice reads 𝐶𝑖 ’s outcome). Replace the precise choice for 𝐶 𝑗 (minimal model of the GL reduct given 𝐶𝑖 ’s resolution) with a conservative one: include every atom in 𝐶 𝑗 that is derivable under any resolution of 𝐶𝑖 . This choice no longer depends on 𝐶𝑖 ’s outcome, so the two layers commute and merge. The cost: the resulting model may not be minimal—it over-derives, including atoms that a precise reduct would have excluded. This parallels the transactional case (age-based abort over-aborts); both trade precision for commutativity. We present this merely as an illustration; whether such conservative models correspond to a natural semantics (perhaps supported models or some relaxation of stability) is unclear. • Entailment (deterministic choice): impose a policy that selects a unique stable extension for each negative SCC (e.g., order atoms alphabetically and assign t to the lowest in each cycle). The choice layer becomes deterministic — an entailment, not a commitment. Each such SCC reduces 𝑑 by one. J
Open Questions
Several structural questions about determinations remain open. Algebraic structure of the determination space. Three related questions concern the internal algebra of determinations. Equivalence: In classical trace theory [21], the Foata normal form canonically represents a word in a partially commutative monoid as a sequence of maximal independent layers. The layered structure of a determination is the analog—but commutation is dynamic: whether 𝜑 and 𝜓 commute depends on the current admissible set, which changes as earlier layers are discharged. Characterizing when two determinations are equivalent (produce the same resolved specification) would give determinations a precise algebraic identity beyond their definition. Composition: When two determinations share a common prefix, they share initial layers. A formal treatment of determination morphisms—how determinations relate under prefix extension, restriction, and
32
Joseph M. Hellerstein
substitution—would enable compositional reasoning across sub-specifications. Factorized representation: Within-layer commutativity gives D the structure of a trie (each layer branches on the choice of commitment set; a determination is a root-to-leaf path), yielding a factorized representation [23] over the determination space. A level-𝑘 support is a union of complete subtrees rooted at depth 𝑘, specified by its depth-𝑘 prefixes without enumerating exponentially many leaves. This trie plays a role analogous to N[𝑋 ] in classical provenance: one computes the support trie once and reads off robustness, qdepth, responsibility, or cross-spec comparison as different views. But the analogy is imperfect: N[𝑋 ]’s universality is algebraic (all specializations are semiring homomorphisms), whereas our specializations include combinatorial operations (Shapley values) and metric ones (|supp|/|D |) that are not semiring maps. Whether there is a formal category in which the support trie is universal—and what efficient algorithms the factorized structure enables—remain open. Reversible commitments. In settings with rollback (speculative execution, backtracking search, optimistic replication with conflict resolution), commitments can be undone. Extending the framework to reversible commitments—replacing monoids with groups at each layer, in the spirit of incremental computation via group-structured changes [5]—is open. Depth under history extension. Under a hereditary basis (Appendix G), the admissible set can only shrink as history grows: Spec(𝐻 ′ ) ⊆ Spec(𝐻 ) for all 𝐻 ⊑ 𝐻 ′ . One would expect that determination depth is also non-increasing—as more events arrive, fewer commitments should be needed to resolve the remaining ambiguity. Conjecture: under a hereditary basis, determination depth is monotonically non-increasing under history extension. Joint attribution. Classical provenance asks “which input tuples are most responsible for an output?”—a game where base tuples are players and the Shapley value measures each tuple’s marginal contribution to the output [19]. Determination responsibility (Appendix C) asks a different question: “which commitments are most responsible for this output holding under this resolution?”— a game where commitments are players. These two games are currently sequential: first attribute the resolution (determination responsibility), then attribute the derivation within that resolution (tuplelevel responsibility). Formalizing their composition into a single joint game—with both commitments and tuples as players, and a unified Shapley value measuring each player’s contribution to the final output—would unify the two dimensions of provenance into a single attribution. The challenge is that the two player sets interact: a commitment can make a tuple relevant (by including it in the resolved model), and a tuple can make a commitment relevant (by participating in a conflict that forces the commitment). Program-bounded vs. input-recurrent depth. The Θ(𝑛) transactional depth arises from recurring structure: the same seal-plus-victim pair repeated as new conflicts arrive. In Datalog¬ , depth is bounded by the program’s dependency structure regardless of EDB size. Characterizing when a specification’s depth is bounded by its static structure vs. when it grows with the input stream — and whether recurring depth admits uniform depth certification (a single check covering all recurrences) — is open. Quantitative negation beyond zero-divisor-free semirings. Theorem 5.2 shows that sealing and monus agree on supports under zero-divisor-free, 𝜔-continuous semirings. In semirings that violate zero-divisor-freeness (e.g., bounded lattice semirings ({0, . . . , 𝑘 }, max, min, 0, 𝑘)), monus can assign intermediate values 1𝐾 −¤ 𝑣 ∉ {0𝐾 , 1𝐾 } to negated literals, encoding a quantitative residual—how much of a derivation was “overcome” by the negation. Sealing discards this information. Whether the determination framework can be extended to capture such quantitative negation—perhaps via
Determination Provenance: From Ambiguity to Algebra
33
graded commitments that record residual strength rather than binary presence/absence—remains open. Acknowledgments Generative AI tools (Claude and ChatGPT) were used as interactive writing and reviewing assistants during the preparation of this work, including drafting and revising text, checking mathematical arguments, and suggesting edits. All content was reviewed, validated, and approved by the authors. References [1] Atul Adya. 1999. Weak consistency: A generalized theory and optimistic implementations. Ph. D. Dissertation. MIT. [2] Tom J. Ameloot, Frank Neven, and Jan Van den Bussche. 2013. Relational transducers for declarative networking. J. ACM 60, 2 (2013), 15:1–15:38. doi:10.1145/2450142.2450151 [3] Bahareh Sadat Arab, Dieter Gawlick, Vasudha Krishnaswamy, Venkatesh Radhakrishnan, and Boris Glavic. 2018. GProM - A Swiss Army Knife for Your Provenance Needs. In IEEE Data Engineering Bulletin, Vol. 41. 51–62. [4] Marcelo Arenas, Leopoldo Bertossi, and Jan Chomicki. 1999. Consistent Query Answers in Inconsistent Databases. In Proceedings of the Eighteenth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS). 68–79. doi:10.1145/303976.303983 [5] Mihai Budiu, Tej Chajed, Frank McSherry, Leonid Ryzhyk, and Val Tannen. 2023. DBSP: Automatic Incremental View Maintenance. Proceedings of the VLDB Endowment 16, 7 (2023), 1601–1614. doi:10.14778/3587136.3587137 [6] Peter Buneman, Sanjeev Khanna, and Wang-Chiew Tan. 2001. Why and Where: A Characterization of Data Provenance. In Database Theory - ICDT 2001, 8th International Conference, London, UK, January 4-6, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 1973), Jan Van den Bussche and Victor Vianu (Eds.). Springer, London, UK, 316–330. doi:10.1007/3-540-44503-X_20 [7] Nilesh Dalvi and Dan Suciu. 2012. The dichotomy of probabilistic inference for unions of conjunctive queries. J. ACM 59, 6 (2012), 30:1–30:87. doi:10.1145/2395116.2395119 [8] Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. 2021. Semiring Provenance for LFP and Strategy Analysis. In Proceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS). 276–289. doi:10.1145/3452021.3458325 [9] Daniel Deutch, Tova Milo, Sudeepa Roy, and Val Tannen. 2014. Circuits for Datalog Provenance. In Proceedings of the 17th International Conference on Database Theory (ICDT). 201–212. doi:10.5441/002/icdt.2014.22 [10] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. 2012. Answer Set Solving in Practice. Morgan & Claypool. [11] Michael Gelfond and Vladimir Lifschitz. 1988. The stable model semantics for logic programming. ICLP (1988). [12] Boris Glavic and Gustavo Alonso. 2009. Perm: Processing Provenance and Data on the Same Data Model through Query Rewriting. In Proceedings of the 25th IEEE International Conference on Data Engineering (ICDE). 174–185. doi:10.1109/ICDE.2009.15 [13] Todd J. Green, Giorgos Karvounarakis, and Val Tannen. 2007. Provenance Semirings. In Proceedings of the Twenty-Sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS). Association for Computing Machinery, Beijing, China, 31–40. doi:10.1145/1265530.1265535 [14] Joseph Halpern and Judea Pearl. 2001. Causes and explanations: A structural-model approach. MIT Press. [15] Joseph M. Hellerstein. 2025. Complete CALM: A Coordination Criterion for Specifications. arXiv:2602.09435 [cs.DC] https://arxiv.org/abs/2602.09435 [16] Joseph M. Hellerstein. 2025. On the Complexity of Determinations. (2025). Under review. [17] Sven Köhler, Bertram Ludäscher, and Yannis Smaragdakis. 2012. Declarative Datalog Debugging for Mere Mortals. In Datalog 2.0. 111–122. doi:10.1007/978-3-642-36524-8_12 [18] Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (1978), 558–565. doi:10.1145/359545.359563 [19] Ester Livshits, Leopoldo Bertossi, Benny Kimelfeld, and Moshe Sebag. 2021. The Shapley Value of Tuples in Query Answering. In Proceedings of the 24th International Conference on Database Theory (ICDT). 20:1–20:19. doi:10.4230/ LIPIcs.ICDT.2021.20 [20] V. Wiktor Marek and Miroslaw Truszczyński. 1991. Autoepistemic Logic. J. ACM 38, 3 (1991), 588–619. doi:10.1145/ 116825.116836 [21] Antoni Mazurkiewicz. 1977. Concurrent Program Schemes and Their Interpretations. In DAIMI Report Series, Vol. 6. Aarhus University. doi:10.7146/dpb.v6i78.7691
34
Joseph M. Hellerstein
[22] Alexandra Meliou, Wolfgang Gatterbauer, Joseph Y. Halpern, Christoph Koch, Katherine F. Moore, and Dan Suciu. 2010. Causality in databases. IEEE Data Engineering Bulletin 33, 3 (2010), 59–67. http://sites.computer.org/debull/ A10sept/suciu.pdf [23] Dan Olteanu and Jakub Závodnỳ. 2015. Factorized databases. SIGMOD (2015). [24] Fotis Psallidas and Eugene Wu. 2018. Smoke: Fine-Grained Lineage at Interactive Speed. In Proceedings of the 2018 International Conference on Management of Data (SIGMOD). 719–734. doi:10.1145/3183713.3190515 [25] David P. Reed. 1978. Naming and Synchronization in a Decentralized Computer System. Ph. D. Dissertation. Massachusetts Institute of Technology. [26] Margo Seltzer, Y. Zhang, et al. 2005. Provenance in Systems. In Proceedings of the 7th USENIX Conference on File and Storage Technologies (FAST). USENIX Association, San Francisco, CA, 99–116. [27] Pierre Senellart. 2018. Provenance and Probabilistic Databases. Cambridge University Press. [28] Lloyd S. Shapley. 1953. A Value for 𝑛-Person Games. In Contributions to the Theory of Games, Harold W. Kuhn and Albert W. Tucker (Eds.). Annals of Mathematics Studies, Vol. 2. Princeton University Press, 307–317. [29] Benjamin H. Sigelman, Luiz André Barroso, Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag. 2010. Dapper, a Large-Scale Distributed Systems Tracing Infrastructure. Technical Report. Google. [30] Dan Suciu, Dan Olteanu, Christopher Ré, and Christoph Koch. 2011. Probabilistic Databases. Morgan & Claypool. [31] Allen Van Gelder, Kenneth Ross, and John Schlipf. 1991. The well-founded semantics for general logic programs. JACM (1991). [32] Brecht Vandevoort, Alan Fekete, Bas Ketsman, Frank Neven, and Stijn Vansummeren. 2025. Using Read Promotion and Mixed Isolation Levels for Performant Yet Serializable Execution of Transaction Programs. arXiv preprint arXiv:2501.18377v3 (2025). [33] Jef Wijsen. 2019. Certain Conjunctive Query Answering in First-Order Logic. ACM Transactions on Database Systems 44, 1 (2019), 3:1–3:45. doi:10.1145/3284551