Documentation

Provenance.SemiringWithMonus

Semirings with monus #

This file defines semirings with monus and introduces their main properties.

Many semirings relevant for provenance can be equipped with a monus - operator, resulting in what is called a semiring with monus, or m-semiring. This is standard in semiring theory [Ame84] and was introduced in the setting of provenance semirings by Geerts and Poggi [GP10]. The class is the algebraic structure underlying the annotated query semantics of Section IV-A of Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data (Definition 5).

References #

Definition of a `SemiringWithMonus` #

class SemiringWithMonus (α : Type) extends Semiring α, PartialOrder α, IsOrderedAddMonoid α, CanonicallyOrderedAdd α, Sub α :

A SemiringWithMonus is a naturally ordered semiring with a monus operation that is compatible with the natural order. We do not require the semiring to be necessarily commutative.

In addition to monus, the class carries a δ : α → α operator subject to three axioms (delta_zero, delta_natCast_pos, and delta_regrouping). This is the duplicate-eliminating support operator used to interpret aggregation in the framework of Amsterdamer, Deutch & Tannen, Provenance for aggregate queries, mirroring ProvSQL's Semiring::delta.

add : α → α → α
add_assoc (a b c : α) : a + b + c = a + (b + c)
zero : α
zero_add (a : α) : 0 + a = a
add_zero (a : α) : a + 0 = a
nsmul : ℕ → α → α
nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
add_comm (a b : α) : a + b = b + a
mul : α → α → α
left_distrib (a b c : α) : a * (b + c) = a * b + a * c
right_distrib (a b c : α) : (a + b) * c = a * c + b * c
zero_mul (a : α) : 0 * a = 0
mul_zero (a : α) : a * 0 = 0
mul_assoc (a b c : α) : a * b * c = a * (b * c)
one : α
one_mul (a : α) : 1 * a = a
mul_one (a : α) : a * 1 = a
natCast : ℕ → α
natCast_zero : ↑0 = 0
natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
npow : ℕ → α → α
npow_zero (x : α) : Semiring.npow 0 x = 1
npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
le : α → α → Prop
lt : α → α → Prop
le_refl (a : α) : a ≤ a
le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c
le_add_self (a b : α) : a ≤ b + a
le_self_add (a b : α) : a ≤ a + b
sub : α → α → α
monus_spec (a b c : α) : a - b ≤ c ↔ a ≤ b + c
delta : α → α
Duplicate-eliminating support operator. Sends 0 to 0 and any positive integer iterate of 1 to 1.
delta_zero : delta 0 = 0
δ sends 0 to 0.
delta_natCast_pos {n : ℕ} : 0 < n → delta ↑n = 1
δ sends every positive integer iterate of 1 (i.e., every positive natural-number cast) to 1.
delta_regrouping (s : Multiset α) : delta (Multiset.map delta s).sum = delta s.sum
δ is invariant under regrouping a fine partition into a coarse one: computing δ on each fine group's sum, summing the results, and applying δ again yields the same value as summing all the fine groups directly and applying δ. Formally, δ((Σᵢ δ(aᵢ))) = δ((Σᵢ aᵢ)) for any multiset of annotations.
This strengthens the idempotence axiom of Amsterdamer, Deutch & Tannen, Provenance for aggregate queries, Def. 3.6: idempotence is recovered by taking a singleton multiset (see delta_idempotent). The stronger form is the natural axiom for making grouped aggregation associative-up-to-equivalence under partition coarsening: re-grouping a fine partition to get a coarse one yields the same provenance as grouping directly.

Instances

Main properties #

theorem monus_smallest {α : Type} [K : SemiringWithMonus α] (a b : α) :

a ≤ b + (a - b) ∧ ∀ (c : α), a ≤ b + c → a - b ≤ c

In a SemiringWithMonus, a - b is the smallest element c satisfying a ≤ b + c.

theorem delta_one {α : Type} [K : SemiringWithMonus α] :

SemiringWithMonus.delta 1 = 1

In a SemiringWithMonus, δ 1 = 1.

theorem delta_idempotent {α : Type} [K : SemiringWithMonus α] (a : α) :

SemiringWithMonus.delta (SemiringWithMonus.delta a) = SemiringWithMonus.delta a

In a SemiringWithMonus, δ is idempotent: applying it twice equals applying it once. This is the singleton case of delta_regrouping: the fine partition with a single group reduces to applying δ once or twice on the same value.

theorem monus_self {α : Type} [K : SemiringWithMonus α] (a : α) :

a - a = 0

In a SemiringWithMonus, a - a = 0.

theorem zero_monus {α : Type} [K : SemiringWithMonus α] (a : α) :

0 - a = 0

In a SemiringWithMonus, 0 - a = 0.

theorem monus_zero {α : Type} [K : SemiringWithMonus α] (a : α) :

a - 0 = a

In a SemiringWithMonus, a - 0 = a.

theorem add_monus {α : Type} [K : SemiringWithMonus α] (a b : α) :

a + (b - a) = b + (a - b)

In a SemiringWithMonus, a + (b -a) = b + (a - b).

theorem monus_add {α : Type} [K : SemiringWithMonus α] (a b c : α) :

a - (b + c) = a - b - c

In a SemiringWithMonus, monus is left-distributive over plus.

Additional properties #

The following properties do not always hold in an arbitrary m-semiring.

@[reducible, inline]

abbrev idempotent (α : Type u_1) [Semiring α] :

A Semiring is idempotent if a + a = a.

Equations

idempotent α = ∀ (a : α), a + a = a

Instances For

@[reducible, inline]

abbrev absorptive (α : Type u_1) [Semiring α] :

A Semiring is absorptive (also called 0-closed or 0-bounded) if 1 + a = a.

Equations

absorptive α = ∀ (a : α), 1 + a = 1

Instances For

@[reducible, inline]

abbrev mul_sub_left_distributive (α : Type) [SemiringWithMonus α] :

We define left-distributivity of times over monus in a SemiringWithMonus.

Equations

mul_sub_left_distributive α = ∀ (a b c : α), a * (b - c) = a * b - a * c

Instances For

theorem idempotent_of_absorptive {α : Type u_1} [K : Semiring α] :

absorptive α → idempotent α

Absorptivity implies idempotence

theorem le_iff_add_eq {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b : α) :

a ≤ b ↔ a + b = b

In an idempotent SemiringWithMonus, a ≤ b iff a + b = b.

theorem plus_is_join {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b : α) :

(a ≤ a + b ∧ b ≤ a + b) ∧ ∀ (u : α), a ≤ u ∧ b ≤ u → a + b ≤ u

In an idempotent SemiringWithMonus, plus is the join of the semilattice

theorem idempotent_of_add_monus {α : Type} [K : SemiringWithMonus α] (h : ∀ (a b c : α), a + b - c = a - c + (b - c)) :

In a SemiringWithMonus, right-distributivity of monus over plus implies idempotence.

theorem add_monus_of_idempotent {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b c : α) :

a + b - c = a - c + (b - c)

In a SemiringWithMonus, idempotence implies right-distributivity of monus over plus.

theorem idempotent_iff_add_monus {α : Type} [SemiringWithMonus α] :

idempotent α ↔ ∀ (a b c : α), a + b - c = a - c + (b - c)

A SemiringWithMonus is idempotent iff monus is right-distributive over plus.

theorem add_monus_of_idempotent_multiset {α : Type} [SemiringWithMonus α] (h : idempotent α) (s : Multiset α) (c : α) :

s.sum - c = (Multiset.map (fun (x : α) => x - c) s).sum

Finite-family version of add_monus_of_idempotent: in an idempotent SemiringWithMonus, monus distributes over the sum of any multiset of annotations, (⨁ᵢ aᵢ) ⊖ c = ⨁ᵢ (aᵢ ⊖ c).

theorem monus_le {α : Type} [SemiringWithMonus α] (a b : α) :

a - b ≤ a

theorem le_plus_monus {α : Type} [SemiringWithMonus α] (a b : α) :

a ≤ b + (a - b)

Characteristic of idempotent semirings #

In an idempotent semiring (a + a = a), every positive natural-number cast collapses to 1. With 1 ≠ 0 this yields CharP K 0. Note that this is strictly weaker than CharZero K, which fails for idempotent semirings since the cast ℕ → K is not injective.

theorem natCast_pos_eq_one_of_idempotent {K : Type} [Semiring K] (h : idempotent K) {n : ℕ} :

0 < n → ↑n = 1

In a semiring with idempotent addition, the cast of any positive natural number equals 1.

theorem CharP.zero_of_idempotent {K : Type} [Semiring K] [Nontrivial K] (h : idempotent K) :

A nontrivial idempotent semiring has characteristic 0 in the CharP sense. Unlike CharZero, this does not require the natural-number cast to be injective: in an idempotent semiring every positive natural maps to 1, but 1 ≠ 0 still suffices to give CharP K 0.

Generic constructions of `δ` #

In the m-semirings used for provenance the δ operator is invariably realized in one of two ways: as the identity (when the semiring is idempotent, so every positive natural cast already equals 1) or as the indicator-of-nonzero (a ↦ if a = 0 then 0 else 1). The lemmas below package the proofs of the three δ axioms for both candidates so each concrete instance can plug them in directly.

theorem delta_natCast_pos_id {K : Type} [Semiring K] (h : idempotent K) {n : ℕ} (hn : 0 < n) :

id ↑n = 1

δ := id satisfies delta_natCast_pos in any idempotent semiring: every positive natural-number cast collapses to 1.

theorem delta_regrouping_id {K : Type} [Semiring K] (s : Multiset K) :

id (Multiset.map id s).sum = id s.sum

δ := id satisfies delta_regrouping in any semiring: both sides unfold to s.sum.

structure IsDeltaIndicator {K : Type} [Zero K] [One K] (δ : K → K) :

The “indicator-of-nonzero” recipe: δ a = 0 when a = 0 and δ a = 1 otherwise. Captured abstractly so a single set of axioms can serve all the concrete instances that use it (ℕ, ℕ[X], Tropical, Viterbi, Lukasiewicz).

zero : δ 0 = 0
nonzero (a : K) : a ≠ 0 → δ a = 1

Instances For

theorem delta_natCast_pos_indicator {K : Type} [Semiring K] [Nontrivial K] [CharP K 0] {δ : K → K} (h : IsDeltaIndicator δ) {n : ℕ} (hn : 0 < n) :

δ ↑n = 1

Any δ matching the indicator recipe satisfies delta_natCast_pos in a nontrivial semiring of characteristic 0 (in the CharP sense): positive natural-number casts are nonzero, so δ sends them to 1.

theorem delta_regrouping_indicator {K : Type} [Semiring K] [PartialOrder K] [IsOrderedAddMonoid K] [CanonicallyOrderedAdd K] [Nontrivial K] {δ : K → K} (h : IsDeltaIndicator δ) (s : Multiset K) :

δ (Multiset.map δ s).sum = δ s.sum

Any δ matching the indicator recipe satisfies delta_regrouping in a nontrivial canonically ordered semiring: a sum is zero exactly when every summand is, so applying δ after summing indicators agrees with applying δ after summing the original values.

Existence of a `δ`-like operator #

This is the abstract counterpart of the SemiringWithMonus δ-axioms: we characterise, in an arbitrary nontrivial semiring (no order assumed), when a function δ : K → K satisfying δ 0 = 0, δ ((n : K)) = 1 for 0 < n, and idempotence δ (δ a) = δ a can exist. The class axiom delta_regrouping is strictly stronger than idempotence, so the iff below should be read as a statement about how much of the ProvSQL δ interface is consistent with a given characteristic, not as a full existence proof for the class axiom. (Constructing a witness for delta_regrouping itself requires more structure: in a canonically ordered semiring the indicator works, see delta_regrouping_indicator.)

theorem delta_exists_iff_charP_zero {K : Type} [Semiring K] [Nontrivial K] :

(∃ (δ : K → K), δ 0 = 0 ∧ (∀ {n : ℕ}, 0 < n → δ ↑n = 1) ∧ ∀ (a : K), δ (δ a) = δ a) ↔ CharP K 0

In any nontrivial semiring, a function δ : K → K satisfying δ 0 = 0, δ ((n : K)) = 1 for every positive natural cast n, and idempotence δ (δ a) = δ a exists if and only if K has characteristic 0 in the CharP sense. The forward direction follows because δ 0 = 0 and δ ((n : K)) = 1 are inconsistent when (n : K) = 0 for some 0 < n (it would force 0 = 1); idempotence plays no role here. The backward direction defines δ as the indicator of being nonzero, which is automatically a fixed point of itself.

Note that the δ operator is not uniquely determined by these axioms: they only pin its values on the image of ℕ (plus the requirement that any chosen value be a fixed point of δ). Two typical choices are δ as the indicator of being nonzero (δ x = if x = 0 then 0 else 1, used in the backward direction below) and, in an idempotent semiring, δ as the identity (since every positive natural cast then equals 1, see natCast_pos_eq_one_of_idempotent).

Commutative `SemiringWithMonus`s #

SemiringWithMonus is intentionally not assumed to be commutative; however, every provenance semiring used in this library is in fact commutative, and the algebraic identities that drive HAVING-style aggregate provenance (see Provenance.Having) require it. CommSemiringWithMonus packages a SemiringWithMonus together with the commutativity axiom, producing a CommMonoid instance whose Mul matches the one already supplied by SemiringWithMonus, so no Mul diamond appears when Finset.prod is used.

class CommSemiringWithMonus (K : Type) extends SemiringWithMonus K :

A SemiringWithMonus whose multiplication is commutative.

add : K → K → K
add_assoc (a b c : K) : a + b + c = a + (b + c)
zero : K
zero_add (a : K) : 0 + a = a
add_zero (a : K) : a + 0 = a
nsmul : ℕ → K → K
nsmul_zero (x : K) : AddMonoid.nsmul 0 x = 0
nsmul_succ (n : ℕ) (x : K) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
add_comm (a b : K) : a + b = b + a
mul : K → K → K
left_distrib (a b c : K) : a * (b + c) = a * b + a * c
right_distrib (a b c : K) : (a + b) * c = a * c + b * c
zero_mul (a : K) : 0 * a = 0
mul_zero (a : K) : a * 0 = 0
mul_assoc (a b c : K) : a * b * c = a * (b * c)
one : K
one_mul (a : K) : 1 * a = a
mul_one (a : K) : a * 1 = a
natCast : ℕ → K
natCast_zero : ↑0 = 0
natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
npow : ℕ → K → K
npow_zero (x : K) : Semiring.npow 0 x = 1
npow_succ (n : ℕ) (x : K) : Semiring.npow (n + 1) x = Semiring.npow n x * x
le : K → K → Prop
lt : K → K → Prop
le_refl (a : K) : a ≤ a
le_trans (a b c : K) : a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_ge (a b : K) : a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm (a b : K) : a ≤ b → b ≤ a → a = b
add_le_add_left (a b : K) : a ≤ b → ∀ (c : K), a + c ≤ b + c
add_le_add_right (a b : K) : a ≤ b → ∀ (c : K), c + a ≤ c + b
exists_add_of_le {a b : K} : a ≤ b → ∃ (c : K), b = a + c
le_add_self (a b : K) : a ≤ b + a
le_self_add (a b : K) : a ≤ a + b
sub : K → K → K
monus_spec (a b c : K) : a - b ≤ c ↔ a ≤ b + c
delta : K → K
delta_zero : delta 0 = 0
delta_natCast_pos {n : ℕ} : 0 < n → delta ↑n = 1
delta_regrouping (s : Multiset K) : delta (Multiset.map delta s).sum = delta s.sum
mul_comm (a b : K) : a * b = b * a
Multiplication on K is commutative.

Instances

@[implicit_reducible, instance 100]

instance instCommMonoidOfCommSemiringWithMonus {K : Type} [h : CommSemiringWithMonus K] :

A CommSemiringWithMonus is automatically a CommMonoid, sharing its multiplicative structure with the underlying SemiringWithMonus. This makes Finset.prod usable without introducing a separate CommSemiring hypothesis that would cause a Mul diamond.

Equations

instCommMonoidOfCommSemiringWithMonus = { toMonoid := h.toMonoidWithZero.toMonoid, mul_comm := ⋯ }

Homomorphisms of `SemiringWithMonus`s #

class SemiringWithMonusHom (α β : Type) [SemiringWithMonus α] [SemiringWithMonus β] extends α →+* β :

Definition of a homomorphism of SemiringWithMonuss. Preserves the semiring structure (via RingHom), the monus (map_sub), and the δ operator (map_delta). The latter is required for hom commutation of the aggregation operator, where δ appears on the row-annotation column (Definition 7 / R5 of Sen, Maniu & Senellart).

toFun : α → β
map_one' : (↑↑self.toRingHom).toFun 1 = 1
map_mul' (x y : α) : (↑↑self.toRingHom).toFun (x * y) = (↑↑self.toRingHom).toFun x * (↑↑self.toRingHom).toFun y
map_zero' : (↑↑self.toRingHom).toFun 0 = 0
map_add' (x y : α) : (↑↑self.toRingHom).toFun (x + y) = (↑↑self.toRingHom).toFun x + (↑↑self.toRingHom).toFun y
map_sub (x y : α) : self.toRingHom (x - y) = self.toRingHom x - self.toRingHom y
map_delta (a : α) : self.toRingHom (SemiringWithMonus.delta a) = SemiringWithMonus.delta (self.toRingHom a)
The hom preserves δ: h (δ a) = δ (h a).

Instances

@[implicit_reducible]

instance instCoeFunSemiringWithMonusHomForall (α β : Type) [SemiringWithMonus α] [SemiringWithMonus β] :

CoeFun (SemiringWithMonusHom α β) fun (x : SemiringWithMonusHom α β) => α → β

Equations

instCoeFunSemiringWithMonusHomForall α β = { coe := fun (f : SemiringWithMonusHom α β) (x : α) => f.toRingHom x }

theorem idempotent_of_injective_homomorphism_idempotent {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνi : Function.Injective fun (x : α) => ν.toRingHom x) :

idempotent β → idempotent α

If ν is an injective m-semiring homomorphism from α to β, and β is idempotent, so is α.

theorem idempotent_of_surjective_homomorphism_idempotent {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνs : Function.Surjective fun (x : α) => ν.toRingHom x) :

idempotent α → idempotent β

If ν is an m-semiring homomorphism from α onto β, and α is idempotent, so is β.

theorem mul_sub_left_of_injective_homomorphism_mul_sub_left {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνi : Function.Injective fun (x : α) => ν.toRingHom x) :

mul_sub_left_distributive β → mul_sub_left_distributive α

If ν is an injective m-semiring homomorphism from α to β, and β has left-distributivity of times over monus, so has α.

theorem mul_sub_left_of_surjective_homomorphism_mul_sub_left {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνs : Function.Surjective fun (x : α) => ν.toRingHom x) :

mul_sub_left_distributive α → mul_sub_left_distributive β

If ν is an m-semiring homomorphism from α onto β, and α has left-distributivity of times over monus, so has β.

Miscellaneous #

class HasAltLinearOrder (α : Type u) :

altOrder : LinearOrder α

Instances