Documentation

Provenance.Semirings.Nat

Counting m-semiring #

This file shows that ℕ (with standard addition and multiplication) is a commutative m-semiring. The monus is truncated subtraction (Nat.sub). Unlike most provenance semirings, ℕ is neither idempotent nor absorptive.

The natural order is the usual order on natural numbers, and monus coincides with Mathlib's Nat.sub.

source
@[instance_reducible]
instance instSemiringWithMonusNat :
SemiringWithMonus ℕ

ℕ is a commutative m-semiring. The natural order is the usual order on natural numbers, and the monus is truncated subtraction. The δ operator matches ProvSQL's Counting::delta: the support indicator (0 ↦ 0, positive ↦ 1).

Equations
  • One or more equations did not get rendered due to their size.
Dependency graph
source
@[instance_reducible]
instance instCommSemiringWithMonusNat :
CommSemiringWithMonus ℕ
Equations
Dependency graph
source
@[instance_reducible]
instance instHasAltLinearOrderNat :
HasAltLinearOrder ℕ
Equations
Dependency graph
source
theorem Nat.mul_sub_left_distributive :
_root_.mul_sub_left_distributive ℕ
Dependency graph
source
theorem Nat.exclusive :
_root_.exclusive ℕ

ℕ is exclusive: 𝟙 ⊖ a is 0 as soon as a is positive, and a itself is 0 otherwise.

Unlike in Bool, 𝟙 ⊖ a is not a complement of a here: 2 + (1 - 2) = 2 and not 1. Exclusivity asks only for orthogonality, so it holds in a semiring where the monus against 𝟙 collapses as well as in one where it complements.

Dependency graph
source
theorem Nat.not_idempotent :
¬idempotent ℕ
Dependency graph
source
theorem Nat.not_absorptive :
¬absorptive ℕ
Dependency graph
source
theorem Nat.not_isDelta_id :
¬IsDelta id

On ℕ the identity is not an admissible δ: δ(𝟙 ⊕ 𝟙) = 𝟙 would make ℕ idempotent (1 + 1 = 2 ≠ 1). This is why the instance above takes the support indicator.

Dependency graph
source
theorem Nat.charP_zero :
CharP ℕ 0

ℕ has characteristic 0: it satisfies CharZero, hence CharP ℕ 0 via CharP.ofCharZero.

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

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

Dependency graph
source
theorem Nat.no_monusHom_to_Bool :
IsEmpty (SemiringWithMonusHom ℕ Bool)

There is no m-semiring homomorphism from ℕ to 𝔹. The unique ring homomorphism ℕ → 𝔹 is the support map n ↦ (n ≠ 0) (the natural-number cast), but it does not preserve monus: supp (2 ∸ 1) = ⊤ while supp 2 ∸ supp 1 = ⊥. This is the algebraic form of the fact that ℕ-adequacy of the annotated semantics stops at the monotone fragment: possible-worlds equalities transfer along monus-preserving homomorphisms into 𝔹 (as they exist for BoolFunc X, one per valuation), and ℕ has none.

Dependency graph
source
theorem Nat.counterexample_having :
have t₁ := 1; have t₂ := 1; have t₃ := 1; t₁ * t₂ * (1 - t₃) + t₁ * t₃ * (1 - t₂) + t₂ * t₃ * (1 - t₁) ≠ t₁ * t₂ + t₁ * t₃ + t₂ * t₃ - t₁ * t₂ * t₃

Over ℕ, the fused HAVING (COUNT(*) = 2) predicate provenance of a three-tuple group, (t₁ ⊗ t₂) ⊗ (𝟙 ⊖ t₃) ⊕ (t₁ ⊗ t₃) ⊗ (𝟙 ⊖ t₂) ⊕ (t₂ ⊗ t₃) ⊗ (𝟙 ⊖ t₁), differs from the annotation ((t₁ ⊗ t₂) ⊕ (t₁ ⊗ t₃) ⊕ (t₂ ⊗ t₃)) ⊖ (t₁ ⊗ t₂ ⊗ t₃) produced by the join-based rewriting Q₂^{≥2} − Q₂^{≥3}. With t₁ = t₂ = t₃ = 1, the first expression evaluates to 0 while the second evaluates to 2.

Dependency graph