Min-max semiring

This file defines the min-max semiring MinMax α over a bounded linear order α, where addition is min and multiplication is max. The natural order is the reverse of the order on α (so ⊤ is the additive identity and ⊥ the multiplicative identity). This semiring models security levels or (dually) the fuzzy semiring.

Also defined:

• MaxMin α = MinMax (OrderDual α) – the dual semiring with max for addition and min for multiplication
• TVL – three-valued logic {⊥, unknown, ⊤}, an instance of MaxMin

MinMax α is absorptive and idempotent. The dual MaxMin TVL does not satisfy left-distributivity of multiplication over monus.

The security/access control semiring is discussed in Green & Tannen, The Semiring Framework for Database Provenance.

References

• Green & Tannen, The Semiring Framework for Database Provenance

structure MinMax (α : Type) : Type

The min-max semiring over a bounded linear order: addition is min, multiplication is max, zero is ⊤ and one is ⊥. The natural order is the reverse of α's order.

• val : α

theorem MinMax.ext {α : Type} {x y : MinMax α} (val : x.val = y.val) : x = y

theorem MinMax.ext_iff {α : Type} {x y : MinMax α} : x = y ↔ x.val = y.val

@[instance_reducible]

instance instCoeMinMax {α : Type} : Coe (MinMax α) α

Equations

• instCoeMinMax = { coe := MinMax.val }

@[instance_reducible]

instance instTopMinMax {α : Type} [LinearOrder α] [OrderTop α] : Top (MinMax α)

Equations

• instTopMinMax = { top := { val := ⊤ } }

@[instance_reducible]

instance instBotMinMax {α : Type} [LinearOrder α] [OrderBot α] : Bot (MinMax α)

Equations

• instBotMinMax = { bot := { val := ⊥ } }

@[instance_reducible]

instance instLEMinMax {α : Type} [LinearOrder α] : LE (MinMax α)

Equations

• instLEMinMax = { le := fun (a b : MinMax α) => b.val ≤ a.val }

@[instance_reducible]

instance instLinearOrderMinMax {α : Type} [LinearOrder α] : LinearOrder (MinMax α)

Equations

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

@[instance_reducible]

instance instZeroMinMax {α : Type} [LinearOrder α] [OrderTop α] : Zero (MinMax α)

Equations

• instZeroMinMax = { zero := ⊤ }

@[instance_reducible]

instance instAddMinMax {α : Type} [LinearOrder α] : Add (MinMax α)

Equations

• instAddMinMax = { add := fun (a b : MinMax α) => { val := min a.val b.val } }

@[instance_reducible]

instance instOneMinMax {α : Type} [LinearOrder α] [OrderBot α] : One (MinMax α)

Equations

• instOneMinMax = { one := ⊥ }

@[instance_reducible]

instance instMulMinMax {α : Type} [LinearOrder α] : Mul (MinMax α)

Equations

• instMulMinMax = { mul := fun (a b : MinMax α) => { val := max a.val b.val } }

@[instance_reducible]

instance instSubMinMax {α : Type} [LinearOrder α] [OrderTop α] : Sub (MinMax α)

Equations

• instSubMinMax = { sub := fun (a b : MinMax α) => if a.val ≥ b.val then { val := ⊤ } else { val := a.val } }

@[instance_reducible]

instance instCommSemiringMinMax {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : CommSemiring (MinMax α)

Equations

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

@[instance_reducible]

instance instSemiringWithMonusMinMax {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : SemiringWithMonus (MinMax α)

MinMax α is a commutative m-semiring for any bounded linear order α.

Equations

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

theorem MinMax.isDelta_id {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : IsDelta id

On MinMax α the identity is an admissible δ, so it is the one used (ProvSQL's MinMax::delta); delta_absorb is the lattice law a ⊔ (a ⊓ b) = a.

@[instance_reducible]

instance instCommSemiringWithMonusMinMax {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : CommSemiringWithMonus (MinMax α)

Equations

• instCommSemiringWithMonusMinMax = { toSemiringWithMonus := instSemiringWithMonusMinMax, mul_comm := ⋯ }

theorem MinMax.absorptive {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : _root_.absorptive (MinMax α)

theorem MinMax.idempotent {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : _root_.idempotent (MinMax α)

instance instNontrivialMinMax {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] [Nontrivial α] : Nontrivial (MinMax α)

instance MinMax.instCharPZero {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] [Nontrivial α] : CharP (MinMax α) 0

MinMax α has characteristic 0 in the CharP sense whenever α is nontrivial: it is idempotent, and (0 : MinMax α) = ⟨⊤⟩ differs from (1 : MinMax α) = ⟨⊥⟩ since ⊥ ≠ ⊤ in a nontrivial bounded order.

@[reducible, inline]

abbrev MaxMin (α : Type) : Type

Equations

• MaxMin α = MinMax αᵒᵈ

@[instance_reducible]

instance instCommSemiringMaxMin {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : CommSemiring (MaxMin α)

Equations

• instCommSemiringMaxMin = { toSemiring := instSemiringWithMonusMinMax.toSemiring, mul_comm := ⋯ }

@[instance_reducible]

instance instSemiringWithMonusMaxMin {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : SemiringWithMonus (MaxMin α)

Equations

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

@[instance_reducible]

instance instCommSemiringWithMonusMaxMin {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : CommSemiringWithMonus (MaxMin α)

Equations

• instCommSemiringWithMonusMaxMin = { toSemiringWithMonus := instSemiringWithMonusMaxMin, mul_comm := ⋯ }

instance instNontrivialOrderDual_provenance {α : Type} [h : Nontrivial α] : Nontrivial αᵒᵈ

inductive TVL : Type

Three-valued logic {⊥, unknown, ⊤}, used as an instance of MaxMin.

• bot : TVL
• unknown : TVL
• top : TVL

@[instance_reducible]

instance instDecidableEqTVL : DecidableEq TVL

Equations

• instDecidableEqTVL x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprTVL : Repr TVL

Equations

• instReprTVL = { reprPrec := instReprTVL.repr }

def instReprTVL.repr : TVL → ℕ → Std.Format

Equations

• instReprTVL.repr TVL.bot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TVL.bot")).group prec✝
• instReprTVL.repr TVL.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TVL.unknown")).group prec✝
• instReprTVL.repr TVL.top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TVL.top")).group prec✝

@[instance_reducible]

instance instOrdTVL : Ord TVL

Equations

• instOrdTVL = { compare := instOrdTVL.ord }

def instOrdTVL.ord : TVL → TVL → Ordering

Equations

• instOrdTVL.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance instLETVL : LE TVL

Equations

• instLETVL = { le := fun (a b : TVL) => (compare a b).isLE = true }

@[instance_reducible]

instance instLinearOrderTVL : LinearOrder TVL

Equations

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

@[instance_reducible]

instance instOrderBotTVL : OrderBot TVL

Equations

• instOrderBotTVL = { bot := TVL.bot, bot_le := instOrderBotTVL._proof_1 }

@[instance_reducible]

instance instOrderTopTVL : OrderTop TVL

Equations

• instOrderTopTVL = { top := TVL.top, le_top := instOrderTopTVL._proof_1 }

@[instance_reducible]

instance instCommSemiringMaxMinTVL : CommSemiring (MaxMin TVL)

Equations

• instCommSemiringMaxMinTVL = inferInstance

@[instance_reducible]

instance instSemiringWithMonusMaxMinTVL : SemiringWithMonus (MaxMin TVL)

Equations

• instSemiringWithMonusMaxMinTVL = inferInstance

@[instance_reducible]

instance instCommSemiringWithMonusMaxMinTVL : CommSemiringWithMonus (MaxMin TVL)

Equations

• instCommSemiringWithMonusMaxMinTVL = inferInstance

instance instNontrivialTVL : Nontrivial TVL

instance MaxMin.instCharPZero {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] [Nontrivial α] : CharP (MaxMin α) 0

MaxMin α has characteristic 0 in the CharP sense whenever α is nontrivial: this lifts the general MinMax instance to the dual order through MaxMin α = MinMax (OrderDual α). In particular it applies to MaxMin TVL since TVL is nontrivial.

theorem TVL.not_mul_sub_left_distributive : ¬mul_sub_left_distributive (MaxMin TVL)

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

There is no semiring homomorphism from BoolFunc Y to MaxMin TVL sending the variables to arbitrary values. The semiring MaxMin TVL is absorptive and has both idempotent addition and idempotent multiplication, so the simple obstructions don't apply: the failure is more subtle.

The argument uses only that a semiring homomorphism preserves + and * (monus is irrelevant here, even though one of the elements we exhibit happens to be written using BoolFunc's monus). In BoolFunc Y, the element c := 1 - var i satisfies two purely additive/multiplicative identities: var i + c = 1 and var i * c = 0. Applying any semiring homomorphism φ and writing y := φ c (an arbitrary element of the target), this forces φ (var i) + y = 1 and φ (var i) * y = 0. Setting φ (var i) = ⟨unknown⟩ in MaxMin TVL: the first equation reduces to max(unknown, y.val) = top, forcing y.val = top; the second reduces to min(unknown, y.val) = bot, forcing y.val = bot. The two are incompatible.

The same obstruction extends to MinMax α whenever α has at least three distinct order values.

Home · Documentation · Publications · Contributors · Source · Cite