Data-part adequacy of the annotated semantics

This file relates the annotated semantics Query.evaluateAnnotated to the plain semantics Query.evaluate, on the data parts: what happens when all annotations are forgotten.

For the positive (Diff-free) fragment the two semantics agree exactly, for any m-semiring K (Query.evaluateAnnotated_toPlain_of_noDiff). This is the counterpart, in the copies-as-elements encoding of annotated relations used here, of the ℕ-adequacy theorem of Benzaken, Cohen-Boulakia, Contejean, Keller & Zucchini, A Coq formalization of data provenance: in their function-with-support encoding of K-relations, tuple multiplicities must be carried by the annotations, so adequacy is a statement about K = ℕ; here multiplicities are carried by the multiset structure itself and the data-part statement is annotation-generic.

In the presence of difference the exact correspondence breaks down – necessarily so: over ℕ, monus-based difference and the all-or-nothing plain difference genuinely disagree once duplicate elimination has accumulated annotations (Nat.counterexample_diff_adequacy, at the end of this file). What survives is:

• an equality with the stripped query (Query.evaluateAnnotated_toPlain): the data part of the annotated result is the plain evaluation of the query obtained by replacing every Diff q₁ q₂ with q₁ (Query.stripDiff). This makes precise that the annotated Diff never removes tuple slots; it only rewrites annotations (possibly to 0), faithfully to ProvSQL, where rows are never deleted by difference at the provenance level;
• an inclusion (Query.evaluate_toPlain_le_evaluateAnnotated): the plain evaluation is a sub-multiset of the data part of the annotated evaluation, since plain evaluation is monotone under stripping differences (Query.evaluate_le_stripDiff).

The inclusion cannot be strengthened to an equality on the tuples with non-zero annotation: nesting differences makes the support of the annotated result both under- and over-approximate the plain result.

Main definitions

• Query.stripDiff – replace every Diff q₁ q₂ node with q₁
• Query.noDiff – the Diff-free predicate on queries (mirroring Query.noAgg)
• AnnotatedRelation.toPlain, AnnotatedDatabase.toPlain – forget the annotations

Main results

• Query.evaluateAnnotated_toPlain – data-part equality with the stripped query, for any m-semiring K
• Query.evaluate_le_stripDiff – plain evaluation is monotone under stripping differences
• Query.evaluate_toPlain_le_evaluateAnnotated – the data-part inclusion
• Query.evaluateAnnotated_toPlain_of_noDiff – data-part adequacy for the positive fragment

References

• Benzaken, Cohen-Boulakia, Contejean, Keller & Zucchini, A Coq formalization of data provenance
• Sen, Maniu & Senellart, ProvSQL

def Query.stripDiff {T : Type} {n : ℕ} : Query T n → Query T n

Replace every difference node Diff q₁ q₂ of a query with its left argument q₁, recursively. Since the annotated semantics of Diff keeps every tuple slot of its left argument (only annotations change), the data part of the annotated evaluation of q is the plain evaluation of q.stripDiff (see Query.evaluateAnnotated_toPlain).

Equations

• (Query.Rel n s).stripDiff = Query.Rel n s
• (Π ts q).stripDiff = Π ts q.stripDiff
• (σ φ q).stripDiff = σ φ q.stripDiff
• (q₁ × q₂).stripDiff = q₁.stripDiff × q₂.stripDiff
• (q₁ ⊎ q₂).stripDiff = (q₁.stripDiff ⊎ q₂.stripDiff)
• (ε q).stripDiff = ε q.stripDiff
• (q₁ - a).stripDiff = q₁.stripDiff
• (Query.Agg is ts as q).stripDiff = Query.Agg is ts as q.stripDiff

def Query.noDiff {T : Type} {n : ℕ} (q : Query T n) : Prop

The Diff-free (positive) fragment of the relational algebra, mirroring Query.noAgg.

Equations

• (Query.Rel n s).noDiff = True
• (Π ts q_1).noDiff = q_1.noDiff
• (σ φ q_1).noDiff = q_1.noDiff
• (q₁ × q₂).noDiff = (q₁.noDiff ∧ q₂.noDiff)
• (q₁ ⊎ q₂).noDiff = (q₁.noDiff ∧ q₂.noDiff)
• (ε q_1).noDiff = q_1.noDiff
• (q₁ - a).noDiff = False
• (Query.Agg is ts as q_1).noDiff = q_1.noDiff

theorem Query.stripDiff_of_noDiff {T : Type} {n : ℕ} (q : Query T n) (hd : q.noDiff) : q.stripDiff = q

On Diff-free queries, Query.stripDiff is the identity.

def AnnotatedRelation.toPlain {T K : Type} {n : ℕ} [Zero K] (r : AnnotatedRelation T K n) : Multiset (Tuple T n)

Forget the annotations of an annotated relation, keeping one tuple slot per annotated tuple (including slots whose annotation is 0). The return type is a bare Multiset (Tuple T n) so that Multiset lemmas apply without an extra unfolding step.

Equations

• r.toPlain = Multiset.map Prod.fst r

def AnnotatedDatabase.toPlain {T K : Type} [Zero K] (d : AnnotatedDatabase T K) : Database T

Forget the annotations of an annotated database, relation by relation.

Equations

• d.toPlain = List.map (fun (e : String × (n : ℕ) × AnnotatedRelation T K n) => (e.1, ⟨e.2.fst, e.2.snd.toPlain⟩)) d

theorem AnnotatedDatabase.find_toPlain {T K : Type} [Zero K] (n : ℕ) (s : String) (d : AnnotatedDatabase T K) : Database.find n s d.toPlain = Option.map AnnotatedRelation.toPlain (find n s d)

Helper lemmas: Multiset.map Prod.fst commutes with the operators

All helpers are stated on bare Multiset (α × β) carriers, so that applying them by exact (full-transparency unification) sees through the AnnotatedRelation / ×ₗ type synonyms in the goals.

theorem Query.evaluateAnnotated_toPlain {T K : Type} [ValueType T] [SemiringWithMonus K] [DecidableEq K] {n : ℕ} (q : Query T n) (hq : q.noAgg) (d : AnnotatedDatabase T K) : (q.evaluateAnnotated hq d).toPlain = q.stripDiff.evaluate d.toPlain

Data-part equality. For any non-aggregation query q over any m-semiring K, forgetting the annotations of the annotated evaluation of q yields the plain evaluation of the stripped query q.stripDiff on the plain database: annotated Diff never removes tuple slots, so all the differences disappear from the data part.

theorem Query.evaluate_le_stripDiff {T : Type} [ValueType T] {n : ℕ} (q : Query T n) : q.noAgg → ∀ (d : Database T), q.evaluate d ≤ q.stripDiff.evaluate d

Plain evaluation is monotone (in the sub-multiset order) under stripping differences: the plain Diff is a filter of its left argument, and every other operator is monotone.

theorem Query.evaluate_toPlain_le_evaluateAnnotated {T K : Type} [ValueType T] [SemiringWithMonus K] [DecidableEq K] {n : ℕ} (q : Query T n) (hq : q.noAgg) (d : AnnotatedDatabase T K) : q.evaluate d.toPlain ≤ (q.evaluateAnnotated hq d).toPlain

Data-part inclusion. The plain evaluation of q on the underlying plain database is a sub-multiset of the data part of the annotated evaluation: annotated evaluation never loses tuple slots, it only zeroes annotations. The inclusion is strict in general (Diff slots whose annotation was zeroed remain on the right), and it cannot be strengthened to an equality on non-zero-annotated slots (see Nat.counterexample_diff_adequacy).

theorem Query.evaluateAnnotated_toPlain_of_noDiff {T K : Type} [ValueType T] [SemiringWithMonus K] [DecidableEq K] {n : ℕ} (q : Query T n) (hq : q.noAgg) (hd : q.noDiff) (d : AnnotatedDatabase T K) : (q.evaluateAnnotated hq d).toPlain = q.evaluate d.toPlain

Data-part adequacy for the positive fragment. On Diff-free (and aggregation-free) queries, the annotated semantics computes exactly the plain semantics on the data parts, for any m-semiring K. In the copies-as-elements encoding this is the analogue of the K = ℕ adequacy theorem of Benzaken, Cohen-Boulakia, Contejean, Keller & Zucchini (there, multiplicities live in the annotations, so the statement is ℕ-specific; here they live in the multiset).

ℕ-adequacy genuinely fails beyond the positive fragment

The following counterexample shows that Query.evaluateAnnotated_toPlain_of_noDiff cannot be extended to queries with difference, not even on the tuples with non-zero annotation: over K = ℕ with all base annotations 1, the query (δ R₁) ∖ R₂ on R₁ = {t, t}, R₂ = {t} keeps t with annotation 2 ∸ 1 = 1 in the annotated semantics, while the plain semantics removes it. The Dedup is essential: it accumulates the annotation 2, which the monus difference then decrements instead of zeroing. This is why the ℕ-adequacy theorem of Benzaken, Cohen-Boulakia, Contejean, Keller & Zucchini is necessarily restricted to the positive fragment.

@[implicit_reducible]

instance instValueTypeNat : ValueType ℕ

Natural numbers as a value type (used for kernel-computable counterexamples: unlike String, the order on ℕ reduces by decide).

Equations

• instValueTypeNat = { toZero := Nat.instMulZeroClass.toZero, toAddCommSemigroup := Nat.instAddCommSemigroup, toSub := instSubNat, toMul := instMulNat, toLinearOrder := Nat.instLinearOrder }

theorem Nat.counterexample_diff_adequacy : have t := ![0]; have r₁ := ↑[(t, 1), (t, 1)]; have r₂ := ↑[(t, 1)]; have d := [("R1", ⟨1, r₁⟩), ("R2", ⟨1, r₂⟩)]; have q := ε (Query.Rel 1 "R1") - Query.Rel 1 "R2"; ∃ (hq : q.noAgg), Multiset.map Prod.fst (Multiset.filter (fun (p : AnnotatedTuple ℕ ℕ 1) => p.2 ≠ 0) (q.evaluateAnnotated hq d)) ≠ q.evaluate d.toPlain

Over ℕ, the non-zero-annotated support of the annotated evaluation differs from the plain evaluation on a query combining Dedup and Diff: ℕ-adequacy stops at the positive fragment.

Home · Documentation · Publications · Contributors · Source · Cite