Documentation

Provenance.Semirings.How

How-provenance m-semiring ℕ[X] #

This file shows that the polynomial semiring MvPolynomial X ℕ (multivariate polynomials with natural-number coefficients over a set X of variables) is a commutative m-semiring, sometimes called the How provenance semiring.

It is the universal commutative semiring for provenance Green, Karnouvarakis & Tannen, Provenance Semirings, Proposition 4.2, but is not the universal m-semiring Geerts & Poggi, On database query languages for K-relations, Example 10.

ℕ[X] is neither idempotent nor absorptive. It also does not satisfy left-distributivity of multiplication over monus, contradicting a claim in Amsterdamer, Deutch & Tannen, On the limitations of provenance for queries with differences, Table on p. 4.

References #

source
@[instance_reducible]
instance instLEMvPolynomialNat_provenance {X : Type} :
LE (MvPolynomial X ℕ)
Equations
Dependency graph
source
@[instance_reducible]
noncomputable instance instSubMvPolynomialNat_provenance {X : Type} :
Sub (MvPolynomial X ℕ)
Equations
  • One or more equations did not get rendered due to their size.
Dependency graph
source
theorem coeff_sub {X : Type} (p q : MvPolynomial X ℕ) (n : X →₀ ℕ) :
(p - q).coeff n = p.coeff n - q.coeff n
Dependency graph
source
@[instance_reducible]
instance instPartialOrderMvPolynomialNat_provenance {X : Type} :
PartialOrder (MvPolynomial X ℕ)
Equations
  • One or more equations did not get rendered due to their size.
Dependency graph
source
instance instIsOrderedAddMonoidMvPolynomialNat_provenance {X : Type} :
IsOrderedAddMonoid (MvPolynomial X ℕ)
Dependency graph
source
instance instCanonicallyOrderedAddMvPolynomialNat_provenance {X : Type} :
CanonicallyOrderedAdd (MvPolynomial X ℕ)
Dependency graph
source
instance instCharZeroMvPolynomialNat_provenance {X : Type} :
CharZero (MvPolynomial X ℕ)

ℕ[X] inherits CharZero from ℕ: the constant embedding C : ℕ → MvPolynomial X ℕ is injective, and (n : MvPolynomial X ℕ) = C n. (Equivalent to Mathlib.RingTheory.MvPolynomial.Basic.instCharZero, inlined here to avoid the heavy transitive imports of that file.)

Dependency graph
source
@[instance_reducible]
noncomputable instance instSemiringWithMonusMvPolynomialNat {X : Type} [DecidableEq X] :
SemiringWithMonus (MvPolynomial X ℕ)

Marked as noncomputable only because the proof that MvPolynomial is a CommutativeSemiring is done in a non-computable way in Mathlib. We could redefine MvPolynomial to provide computable proofs.

The δ operator matches ProvSQL's How::delta: the support indicator (0 ↦ 0, any non-zero polynomial ↦ 1).

Equations
  • One or more equations did not get rendered due to their size.
Dependency graph
source
@[instance_reducible]
noncomputable instance instCommSemiringWithMonusMvPolynomialNat {X : Type} [DecidableEq X] :
CommSemiringWithMonus (MvPolynomial X ℕ)
Equations
Dependency graph
source
theorem How.not_idempotent {X : Type} :
¬idempotent (MvPolynomial X ℕ)
Dependency graph
source
theorem How.not_absorptive {X : Type} :
¬absorptive (MvPolynomial X ℕ)
Dependency graph
source
theorem How.not_isDelta_id {X : Type} :
¬IsDelta id

On ℕ[X] the identity is not an admissible δ: δ(𝟙 ⊕ 𝟙) = 𝟙 would make the semiring idempotent, and ℕ[X] counts (1 + 1 = 2 ≠ 1). This is why the instance above takes the support indicator (ProvSQL's How::delta).

Dependency graph
source
theorem How.universal {X : Type} (K : Type) [CommSemiring K] (ν : X → K) :
∃ (h : MvPolynomial X ℕ →+* K), ∀ (i : X), h (MvPolynomial.X i) = ν i

The How[X] semiring is universal among commutative semirings. This was observed in Green, Karnouvarakis, Tannen, Provenance Semirings, Proposition 4.2.

Dependency graph
source
theorem How.not_universal_m {X : Type} [DecidableEq X] [Inhabited X] :
∃ (ν : X → ℕ), ¬∃ (h : SemiringWithMonusHom (MvPolynomial X ℕ) ℕ), ∀ (i : X), (fun (x : MvPolynomial X ℕ) => h.toRingHom x) (MvPolynomial.X i) = ν i

The How[X] semiring is not universal among commutative m-semirings, as long as there is at least one variable in X (if there is none, the notion of universality is trivial). This was shown in Geerts & Poggi, On database query languages for K-relations, Example 10.

Dependency graph
source
theorem How.not_exclusive {X : Type} [DecidableEq X] [Inhabited X] :
¬exclusive (MvPolynomial X ℕ)

ℕ[X] is not exclusive: the monus is coefficientwise truncated subtraction, so 𝟙 ⊖ X keeps the constant term and is 𝟙, whence X ⊗ (𝟙 ⊖ X) = X ≠ 𝟘.

This is the counterexample the possible-world readings turn on: the universal semiring, the one every provenance circuit is built in, is exactly the one where two distinct worlds of an aggregate value fail to annihilate each other. The spurious terms vanish under any homomorphism into an exclusive semiring, since homomorphisms commute with ⊖.

Dependency graph
source
theorem How.not_mul_sub_left_distributive {X : Type} [DecidableEq X] [Inhabited X] :
¬mul_sub_left_distributive (MvPolynomial X ℕ)

In How[X], as long as X is non-empty, times is not distributive over monus. Note that this contradicts Amsterdamer, Deutch & Tannen, On the limitations of provenance for queries with differences, table page 4, which claims this semiring satisfies axiom A13.

Dependency graph
source
theorem How.charP_zero {X : Type} :
CharP (MvPolynomial X ℕ) 0

ℕ[X] has characteristic 0 in the CharP sense, inherited from CharZero via CharP.ofCharZero.

Dependency graph
source
theorem How.no_hom_from_BoolFunc {X Y : Type} [Inhabited Y] :
∃ (ν : Y → MvPolynomial X ℕ), ¬∃ (φ : BoolFunc Y →+* MvPolynomial X ℕ), ∀ (i : Y), φ (BoolFunc.var i) = ν i

There is no semiring homomorphism from BoolFunc Y to ℕ[X] sending the variables to arbitrary values: ℕ[X] is not absorptive, which contradicts var i + 1 = 1 in BoolFunc Y.

Dependency graph