Documentation

Provenance.Semirings.Which

Which-provenance m-semiring (lineage) #

This file defines the Which (or lineage) provenance semiring Which α. Elements are either a finite set wset s representing the witnesses or wbot (bottom). Addition takes the union of witness sets, and multiplication does likewise.

Which α is idempotent. It is absorptive if and only if α is empty. It does not satisfy left-distributivity of multiplication over monus when α is nonempty.

The lineage semiring is discussed in Green & Tannen, The Semiring Framework for Database Provenance.

References #

Green & Tannen, The Semiring Framework for Database Provenance

inductive Which (α : Type) :

wset {α : Type} : Finset α → Which α
wbot {α : Type} : Which α

Instances For

@[implicit_reducible]

instance instZeroWhich {α : Type} :

Zero (Which α)

Equations

instZeroWhich = { zero := Which.wbot }

@[implicit_reducible]

instance instAddWhich {α : Type} [DecidableEq α] :

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instMulWhich {α : Type} [DecidableEq α] :

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instOneWhich {α : Type} :

Equations

instOneWhich = { one := Which.wset ∅ }

@[implicit_reducible]

instance instSubWhich {α : Type} [DecidableEq α] :

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instLEWhich {α : Type} :

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instCommSemiringWhich {α : Type} [DecidableEq α] :

CommSemiring (Which α)

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instPartialOrderWhich {α : Type} :

PartialOrder (Which α)

Equations

instPartialOrderWhich = { toLE := instLEWhich, lt := fun (a b : Which α) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

instance instCanonicallyOrderedAddWhich {α : Type} [DecidableEq α] :

CanonicallyOrderedAdd (Which α)

instance instIsOrderedAddMonoidWhich {α : Type} [DecidableEq α] :

IsOrderedAddMonoid (Which α)

@[implicit_reducible]

instance instSemiringWithMonusWhich {α : Type} [DecidableEq α] :

SemiringWithMonus (Which α)

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instCommSemiringWithMonusWhich {α : Type} [DecidableEq α] :

CommSemiringWithMonus (Which α)

Equations

instCommSemiringWithMonusWhich = { toSemiringWithMonus := instSemiringWithMonusWhich, mul_comm := ⋯ }

theorem Which.not_absorptive {α : Type} [DecidableEq α] (h : ∃ (x : α), ⊤) :

¬_root_.absorptive (Which α)

Which[X] is not absorptive as long as there is at least one variable

theorem Which.absorptive {α : Type} [DecidableEq α] (h : IsEmpty α) :

_root_.absorptive (Which α)

Which[∅] is absorptive

theorem Which.idempotent {α : Type} [DecidableEq α] :

_root_.idempotent (Which α)

instance instNontrivialWhich {α : Type} :

Nontrivial (Which α)

instance Which.instCharPZero {α : Type} [DecidableEq α] :

CharP (Which α) 0

Which α has characteristic 0 in the CharP sense: it is idempotent and nontrivial (wbot ≠ wset ∅), so every positive natural-number cast equals 1.

theorem Which.not_mul_sub_left_distributive {α : Type} [DecidableEq α] [Inhabited α] :

¬mul_sub_left_distributive (Which α)

In Which[X], as long as X is non-empty, times is not distributive over monus.

theorem Which.no_hom_from_BoolFunc {α : Type} [DecidableEq α] {Y : Type} [Inhabited Y] [Inhabited α] :

∃ (ν : Y → Which α), ¬∃ (φ : BoolFunc Y →+* Which α), ∀ (i : Y), φ (BoolFunc.var i) = ν i

There is no semiring homomorphism from BoolFunc Y to Which α (with α inhabited) sending the variables to arbitrary values: Which α is not absorptive (Which.not_absorptive), which contradicts var i + 1 = 1 in BoolFunc Y.