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
@[implicit_reducible]
instance instLEMvPolynomialNat_provenance {X : Type} :
LE (MvPolynomial X ℕ)
Equations
source
@[implicit_reducible]
instance instSubMvPolynomialNat_provenance {X : Type} [DecidableEq X] :
Sub (MvPolynomial X ℕ)
Equations
  • One or more equations did not get rendered due to their size.
source
theorem coeff_sub {X : Type} [DecidableEq X] (p q : MvPolynomial X ℕ) (n : X →₀ ℕ) :
MvPolynomial.coeff n (p - q) = MvPolynomial.coeff n p - MvPolynomial.coeff n q
source
@[implicit_reducible]
instance instPartialOrderMvPolynomialNat_provenance {X : Type} :
PartialOrder (MvPolynomial X ℕ)
Equations
  • One or more equations did not get rendered due to their size.
source
instance instIsOrderedAddMonoidMvPolynomialNat_provenance {X : Type} :
IsOrderedAddMonoid (MvPolynomial X ℕ)
source
instance instCanonicallyOrderedAddMvPolynomialNat_provenance {X : Type} :
CanonicallyOrderedAdd (MvPolynomial X ℕ)
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.)

source
@[implicit_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.
source
@[implicit_reducible]
noncomputable instance instCommSemiringWithMonusMvPolynomialNat {X : Type} [DecidableEq X] :
CommSemiringWithMonus (MvPolynomial X ℕ)
Equations
source
theorem How.not_idempotent {X : Type} :
¬idempotent (MvPolynomial X ℕ)
source
theorem How.not_absorptive {X : Type} :
¬absorptive (MvPolynomial X ℕ)
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.

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.

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.

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.

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.