Łukasiewicz m-semiring

This file defines the Łukasiewicz (fuzzy logic) semiring over rationals [0,1]. Addition is max, multiplication is the Łukasiewicz t-norm max(a + b - 1, 0), zero is 0, and one is 1.

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

This semiring is discussed as a provenance semiring in Grädel & Tannen, Provenance Analysis and Semiring Semantics for First-Order Logic.

References

• Grädel & Tannen, Provenance Analysis and Semiring Semantics for First-Order Logic

@[reducible, inline]

abbrev Lukasiewicz : Type

The Łukasiewicz semiring: rationals in [0,1] with max as addition and the Łukasiewicz t-norm max(a + b - 1, 0) as multiplication.

Equations

• Lukasiewicz = { q : ℚ // 0 ≤ q ∧ q ≤ 1 }

@[instance_reducible]

instance instZeroLukasiewicz : Zero Lukasiewicz

Equations

• instZeroLukasiewicz = { zero := ⟨0, instZeroLukasiewicz._proof_1⟩ }

@[instance_reducible]

instance instOneLukasiewicz : One Lukasiewicz

Equations

• instOneLukasiewicz = { one := ⟨1, instOneLukasiewicz._proof_1⟩ }

@[instance_reducible]

instance instAddLukasiewicz : Add Lukasiewicz

Equations

• instAddLukasiewicz = { add := fun (a b : Lukasiewicz) => max a b }

@[instance_reducible]

instance instMulLukasiewicz : Mul Lukasiewicz

Equations

• instMulLukasiewicz = { mul := fun (a b : Lukasiewicz) => let raw := max (↑a + ↑b - 1) 0; have h := ⋯; ⟨raw, h⟩ }

@[instance_reducible]

instance instSubLukasiewicz : Sub Lukasiewicz

Equations

• instSubLukasiewicz = { sub := fun (a b : Lukasiewicz) => if a ≤ b then ⟨0, instZeroLukasiewicz._proof_1⟩ else a }

theorem Lukasiewicz.sub_def (a b : Lukasiewicz) : a - b = if a ≤ b then ⟨0, ⋯⟩ else a

@[instance_reducible]

instance instCommMagmaLukasiewicz : CommMagma Lukasiewicz

Equations

• instCommMagmaLukasiewicz = { toMul := instMulLukasiewicz, mul_comm := instCommMagmaLukasiewicz._proof_1 }

instance instLeftDistribClassLukasiweicz : LeftDistribClass Lukasiewicz

@[instance_reducible]

instance instCommSemiringLukasiewicz : CommSemiring Lukasiewicz

Equations

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

@[instance_reducible]

instance instLinearOrderLukasiewicz : LinearOrder Lukasiewicz

Equations

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

instance instIsOrderedAddMonoidLukasiewicz : IsOrderedAddMonoid Lukasiewicz

instance instCanonicallyOrderedAddLukasiewicz : CanonicallyOrderedAdd Lukasiewicz

instance instNontrivialLukasiewicz : Nontrivial Lukasiewicz

theorem Lukasiewicz.absorptive : _root_.absorptive Lukasiewicz

theorem Lukasiewicz.idempotent : _root_.idempotent Lukasiewicz

instance Lukasiewicz.instCharPZero : CharP Lukasiewicz 0

Lukasiewicz has characteristic 0 in the CharP sense: it is idempotent and nontrivial, so every positive natural-number cast equals 1.

@[instance_reducible]

instance instSemiringWithMonusLukasiewicz : SemiringWithMonus Lukasiewicz

Lukasiewicz is a commutative m-semiring. The natural order is the usual rational order, and the monus is a if a > b, 0 if a ≤ b. The δ operator matches ProvSQL's Lukasiewicz::delta: the support indicator.

Equations

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

@[instance_reducible]

instance instCommSemiringWithMonusLukasiewicz : CommSemiringWithMonus Lukasiewicz

Equations

• instCommSemiringWithMonusLukasiewicz = { toSemiringWithMonus := instSemiringWithMonusLukasiewicz, mul_comm := ⋯ }

theorem Lukasiewicz.not_mul_idempotent : ¬∀ (a : Lukasiewicz), a * a = a

Łukasiewicz multiplication is not idempotent: (1/2) * (1/2) = max(0, 0) = 0 ≠ 1/2.

theorem Lukasiewicz.not_isDelta_id : ¬IsDelta id

On the Łukasiewicz semiring the identity is not an admissible δ, even though the semiring is absorptive (Lukasiewicz.absorptive): what delta_absorb asks of δ := id is the lattice law a ⊗ (a ⊕ b) = a, which at a = b = 1/2 reads 1/2 ⊗ 1/2 = max(0, 0) = 0 ≠ 1/2. This is why the instance takes the support indicator (ProvSQL's Lukasiewicz::delta).

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

There is no semiring homomorphism from BoolFunc Y to the Łukasiewicz semiring sending the variables to arbitrary values: Łukasiewicz multiplication is not idempotent ((1/2) ⊗ (1/2) = 0 ≠ 1/2), contradicting var i * var i = var i in BoolFunc Y.

theorem Lukasiewicz.mul_sub_left_distributive : _root_.mul_sub_left_distributive Lukasiewicz

Home · Documentation · Publications · Contributors · Source · Cite