Tropical m-semiring

This file shows that the tropicalization of any linearly ordered additive commutative monoid with an absorbing top element (e.g., ℕ ∪ {∞}, ℚ ∪ {∞}, ℝ ∪ {∞}) is a commutative m-semiring. Addition is min (inherited from the tropical structure in Mathlib), multiplication is the original addition of the monoid, zero is ⊤, and one is 0.

The tropical semiring is absorptive and idempotent, and satisfies left-distributivity of multiplication over monus.

The tropical semiring is used as a provenance semiring in Green, Karvounarakis & Tannen, Provenance Semirings.

Note: Geerts & Poggi, On database query languages for K-relations, Example 4 claims that the tropical semiring cannot be extended to an m-semiring. That claim is incorrect: the paper gives a wrong definition of the monus operator.

References

• Green, Karvounarakis & Tannen, Provenance Semirings
• Geerts & Poggi, On database query languages for K-relations

@[instance_reducible]

instance instToStringWithTop_provenance {α : Type u_1} [ToString α] : ToString (WithTop α)

Equations

• instToStringWithTop_provenance = { toString := fun (x : WithTop α) => match x with | none => "⊤" | some x => toString x }

@[instance_reducible]

instance instToStringTropical_provenance {α : Type u_1} [ToString α] : ToString (Tropical α)

Equations

• instToStringTropical_provenance = { toString := fun (x : Tropical α) => toString (Tropical.untrop x) }

theorem tropical_order_ge {α : Type u_1} [LinearOrder α] (a b : Tropical α) : Tropical.untrop a ≥ Tropical.untrop b ↔ a + b = b

In the tropicalization of a linear order, a ≥ b if and only if a+b = b.

@[instance_reducible]

noncomputable instance instSemiringWithMonusTropicalOfLinearOrderedAddCommMonoidWithTop {α : Type} [LinearOrderedAddCommMonoidWithTop α] : SemiringWithMonus (Tropical α)

The tropical semiring is an m-semiring. The natural order of the semiring is the reverse of the usual order. The monus a-b is defined as ⊤ if a≥b (for the usual order, not the natural semiring order), and as a otherwise.

Equations

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

@[instance_reducible]

noncomputable instance instCommSemiringWithMonusTropicalOfLinearOrderedAddCommMonoidWithTop {α : Type} [LinearOrderedAddCommMonoidWithTop α] : CommSemiringWithMonus (Tropical α)

Equations

• instCommSemiringWithMonusTropicalOfLinearOrderedAddCommMonoidWithTop = { toSemiringWithMonus := instSemiringWithMonusTropicalOfLinearOrderedAddCommMonoidWithTop, mul_comm := ⋯ }

@[instance_reducible]

noncomputable instance instSemiringWithMonusTropicalWithTopNat : SemiringWithMonus (Tropical (WithTop ℕ))

The tropical semiring over ℕ ∪ {∞} is a semiring with monus.

Equations

• instSemiringWithMonusTropicalWithTopNat = inferInstance

@[instance_reducible]

noncomputable instance instCommSemiringWithMonusTropicalWithTopNat : CommSemiringWithMonus (Tropical (WithTop ℕ))

Equations

• instCommSemiringWithMonusTropicalWithTopNat = inferInstance

@[instance_reducible]

noncomputable instance instSemiringWithMonusTropicalWithTopRat : SemiringWithMonus (Tropical (WithTop ℚ))

The tropical semiring over ℚ ∪ {∞} is a semiring with monus.

Equations

• instSemiringWithMonusTropicalWithTopRat = inferInstance

@[instance_reducible]

noncomputable instance instCommSemiringWithMonusTropicalWithTopRat : CommSemiringWithMonus (Tropical (WithTop ℚ))

Equations

• instCommSemiringWithMonusTropicalWithTopRat = inferInstance

@[instance_reducible]

noncomputable instance instSemiringWithMonusTropicalWithTopInt : SemiringWithMonus (Tropical (WithTop ℤ))

The tropical semiring over ℤ ∪ {∞} is a semiring with monus. Like the ℚ and ℝ variants it is idempotent and ⊗-over-⊖ distributive but not absorptive; unlike them its carrier is kernel-computable, which makes it the tropical semiring of choice for decide-checked counterexamples.

Equations

• instSemiringWithMonusTropicalWithTopInt = inferInstance

@[instance_reducible]

noncomputable instance instCommSemiringWithMonusTropicalWithTopInt : CommSemiringWithMonus (Tropical (WithTop ℤ))

Equations

• instCommSemiringWithMonusTropicalWithTopInt = inferInstance

@[instance_reducible]

instance instHasAltLinearOrderTropicalWithTopInt : HasAltLinearOrder (Tropical (WithTop ℤ))

Equations

• instHasAltLinearOrderTropicalWithTopInt = { altOrder := inferInstance }

@[instance_reducible]

noncomputable instance instSemiringWithMonusTropicalWithTopReal : SemiringWithMonus (Tropical (WithTop ℝ))

The tropical semiring over ℝ ∪ {∞} is a semiring with monus. Note that this contradicts Geerts & Poggi, On database query languages for K-relations, Example 4 which claims this semiring cannot be extended to a semiring with monus: indeed, that paper gives a wrong definition of the monus operator in the tropical semiring.

Equations

• instSemiringWithMonusTropicalWithTopReal = inferInstance

@[instance_reducible]

noncomputable instance instCommSemiringWithMonusTropicalWithTopReal : CommSemiringWithMonus (Tropical (WithTop ℝ))

Equations

• instCommSemiringWithMonusTropicalWithTopReal = inferInstance

theorem Tropical.absorptive {α : Type} [LinearOrderedAddCommMonoidWithTop α] [CanonicallyOrderedAdd α] : _root_.absorptive (Tropical α)

The tropical semiring is absorptive, as long as the order in the addition monoid corresponds to a canonical order (e.g., as in ℕ) -

theorem TropicalN.absorptive : _root_.absorptive (Tropical (WithTop ℕ))

theorem TropicalN.not_isDelta_id : ¬IsDelta id

On the tropical semiring over ℕ ∪ {∞} the identity is not an admissible δ, even though this semiring is absorptive (TropicalN.absorptive): what delta_absorb asks of δ := id is the lattice law a ⊗ (a ⊕ b) = a, i.e., a + min(a, b) = a in ℕ, and at a = b = trop 1 it reads trop 2 ≠ trop 1. This is why the instance takes the support indicator (ProvSQL's Tropical::delta).

theorem Tropical.mul_sub_left_distributive {α : Type} [LinearOrder α] [AddCancelCommMonoid α] [IsOrderedAddMonoid α] [AddLeftStrictMono α] : _root_.mul_sub_left_distributive (Tropical (WithTop α))

Times distributes over monus on tropical semirings made of an order strictly compatible with addition, with an additional top element.

theorem TropicalN.mul_sub_left_distributive : _root_.mul_sub_left_distributive (Tropical (WithTop ℕ))

theorem TropicalQ.mul_sub_left_distributive : _root_.mul_sub_left_distributive (Tropical (WithTop ℚ))

theorem TropicalR.mul_sub_left_distributive : _root_.mul_sub_left_distributive (Tropical (WithTop ℝ))

theorem Tropical.idempotent {α : Type} [LinearOrderedAddCommMonoidWithTop α] : _root_.idempotent (Tropical α)

The tropical semiring is idempotent -

instance TropicalN.instCharPZero : CharP (Tropical (WithTop ℕ)) 0

The tropical semiring over WithTop R (for any R with Zero R) has characteristic 0 in the CharP sense: it is idempotent, and (0 : Tropical (WithTop R)) = trop ⊤ differs from (1 : Tropical (WithTop R)) = trop 0 since ⊤ ≠ 0 in WithTop R.

instance TropicalQ.instCharPZero : CharP (Tropical (WithTop ℚ)) 0

instance TropicalR.instCharPZero : CharP (Tropical (WithTop ℝ)) 0

theorem TropicalN.not_mul_idempotent : ¬∀ (a : Tropical (WithTop ℕ)), a * a = a

The tropical semiring over ℕ ∪ {∞} does not have idempotent multiplication: Tropical.trop 1 * Tropical.trop 1 = Tropical.trop 2 ≠ Tropical.trop 1. (Tropical multiplication is the original additive monoid operation, which is not idempotent on ℕ.)

theorem TropicalN.no_hom_from_BoolFunc {Y : Type} [Inhabited Y] : ∃ (ν : Y → Tropical (WithTop ℕ)), ¬∃ (φ : BoolFunc Y →+* Tropical (WithTop ℕ)), ∀ (i : Y), φ (BoolFunc.var i) = ν i

There is no semiring homomorphism from BoolFunc Y to the tropical semiring over ℕ ∪ {∞} sending the variables to arbitrary values: tropical multiplication is not idempotent, contradicting var i * var i = var i in BoolFunc Y.

Counterexample to Having.F_eq_S without absorptivity

Unlike Tropical (WithTop ℕ) (canonically ordered, hence absorptive via Tropical.absorptive), Tropical (WithTop ℝ) is not absorptive: with a = trop (-1) we have 1 + a = trop (min 0 (-1)) = trop (-1) ≠ trop 0 = 1.

The tropical m-semiring over ℝ is still idempotent and satisfies mul_sub_left_distributive, so it satisfies the “idempotent + ⊗-over-⊖ distributive” hypotheses one might hope to suffice for Having.F_eq_S. The witness below shows that the strengthened hypothesis (absorptivity) is genuinely required: on U = {true, false} ⊆ Bool and α ≡ trop (-1) we have S_1(U) = trop (-1) but F_1(U) = trop (-2).

theorem TropicalR.not_absorptive : ¬absorptive (Tropical (WithTop ℝ))

Tropical (WithTop ℝ) is not absorptive: 1 + trop (-1) = trop (-1) ≠ 1. The proof goes through tropical_order_ge: a + 1 = 1 would force untrop a ≥ untrop 1 = 0, but with a = trop (-1) we have untrop a = -1.

theorem TropicalR.F_ne_S : Having.F TropicalR.α_ce✝ Finset.univ 1 ≠ Having.S TropicalR.α_ce✝ Finset.univ 1

The HAVING-count identity F_C(U) = S_C(U) from Having.F_eq_S fails in Tropical (WithTop ℝ): with U = Finset.univ : Finset Bool, α ≡ trop (-1), and C = 1, we have F_1(U) = trop (-2) while S_1(U) = trop (-1). This shows that Having.F_eq_S genuinely needs the absorptivity hypothesis (cf. TropicalR.not_absorptive): the weaker “idempotent + mul_sub_left_distributive” combination satisfied by Tropical (WithTop ℝ) (and likewise by Tropical (WithTop ℚ)) is insufficient.

theorem TropicalR.minScan_ne_prov : (Having.prov TropicalR.α_ce✝ Finset.univ fun (W : Finset Bool) => CompOp.ge.eval (Having.minAgg TropicalR.t_ce✝ W) ↑0) ≠ Having.minScan TropicalR.α_ce✝ Finset.univ TropicalR.t_ce✝ CompOp.ge 0

The MIN-scan collapse (Having.minScan_correct) fails in Tropical (WithTop ℝ): on U = {true, false} with α ≡ trop (-1), t ≡ 0 and the predicate MIN(t) ≥ 0, the possible-world provenance is trop (-2) while the scan returns trop (-1). This is the same instance as TropicalR.F_ne_S, and shows that the absorptivity hypothesis of Having.minScan_correct (and, by symmetry, of Having.maxScan_correct and Having.firstScan_correct) is genuinely required: the weaker “idempotent + mul_sub_left_distributive” combination satisfied by Tropical (WithTop ℝ) is insufficient.

Home · Documentation · Publications · Contributors · Source · Cite