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

instCommSemiringWithMonusNat = { toSemiringWithMonus := instSemiringWithMonusNat, mul_comm := instCommSemiringWithMonusNat._proof_1 }

Dependency graph

source

@[instance_reducible]

instance instHasAltLinearOrderNat :

HasAltLinearOrder ℕ

Equations

instHasAltLinearOrderNat = { altOrder := inferInstance }

Dependency graph

source

theorem Nat.mul_sub_left_distributive :

_root_.mul_sub_left_distributive ℕ

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

Documentation

Provenance.Semirings.Nat

Counting m-semiring #