Viterbi m-semiring #

This file defines the Viterbi semiring over non-negative reals in [0,1]. Addition is max, multiplication is the usual product, zero is 0, and one is 1.

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

This semiring is discussed in Green & Tannen, The Semiring Framework for Database Provenance.

References #

Green & Tannen, The Semiring Framework for Database Provenance

source

def Viterbi :

Type

Viterbi semiring (max-times) over probabilities in [0,1].

Equations

Viterbi = { p : NNReal // p ≤ 1 }

Instances For

Dependency graph

source

@[instance_reducible]

instance Viterbi.instCoeNNReal :

Coe Viterbi NNReal

Equations

Viterbi.instCoeNNReal = { coe := Subtype.val }

Dependency graph

source

theorem Viterbi.ext {a b : Viterbi} (h : ↑a = ↑b) :

a = b

Dependency graph

source

theorem Viterbi.ext_iff {a b : Viterbi} :

a = b ↔ ↑a = ↑b

Dependency graph

source

@[simp]

theorem Viterbi.coe_mk (p : NNReal) (hp : p ≤ 1) :

↑⟨p, hp⟩ = p

Dependency graph

source

@[instance_reducible]

instance Viterbi.instZero :

Zero Viterbi

Equations

Viterbi.instZero = { zero := ⟨0, Viterbi.instZero._proof_1 ⟩ }

Dependency graph

source

@[instance_reducible]

instance Viterbi.instOne :

One Viterbi

Equations

Viterbi.instOne = { one := ⟨1, Viterbi.instOne._proof_1 ⟩ }

Dependency graph

source

@[instance_reducible]

instance Viterbi.instAdd :

Add Viterbi

Equations

Viterbi.instAdd = { add := fun (a b : Viterbi) => ⟨max ↑a ↑b, ⋯⟩ }

Dependency graph

source

@[instance_reducible]

instance Viterbi.instMul :

Mul Viterbi

Equations

Viterbi.instMul = { mul := fun (a b : Viterbi) => ⟨↑a * ↑b, ⋯⟩ }

Dependency graph

source

@[simp]

theorem Viterbi.zero_def :

↑0 = 0

Dependency graph

source

@[simp]

theorem Viterbi.one_def :

↑1 = 1

Dependency graph

source

@[simp]

theorem Viterbi.add_def (a b : Viterbi) :

↑(a + b) = max ↑a ↑b

Dependency graph

source

@[simp]

theorem Viterbi.mul_def (a b : Viterbi) :

↑(a * b) = ↑a * ↑b

Dependency graph

source

@[instance_reducible]

instance Viterbi.instCommSemiring :

CommSemiring Viterbi

Equations

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

Dependency graph

source

theorem Viterbi.viterbi_order_le (a b : Viterbi) :

↑a ≤ ↑b ↔ a + b = b

Dependency graph

source

@[instance_reducible]

instance Viterbi.instPartialOrder :

PartialOrder Viterbi

Equations

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

Dependency graph

source

@[simp]

theorem Viterbi.le_def (a b : Viterbi) :

a ≤ b ↔ ↑a ≤ ↑b

Dependency graph

source

@[instance_reducible]

noncomputable instance Viterbi.instSub :

Sub Viterbi

Equations

Viterbi.instSub = { sub := fun (a b : Viterbi) => if ↑a ≤ ↑b then 0 else a }

Dependency graph

source

instance Viterbi.instIsOrderedAddMonoid :

IsOrderedAddMonoid Viterbi

Dependency graph

source

instance Viterbi.instCanonicallyOrderedAdd :

CanonicallyOrderedAdd Viterbi

Dependency graph

source

instance Viterbi.instNontrivial :

Nontrivial Viterbi

Dependency graph

source

theorem Viterbi.absorptive :

_root_.absorptive Viterbi

Dependency graph

source

theorem Viterbi.idempotent :

_root_.idempotent Viterbi

Dependency graph

source

instance Viterbi.instCharPZero :

CharP Viterbi 0

Viterbi has characteristic 0 in the CharP sense: it is idempotent and nontrivial.

Dependency graph

source

@[instance_reducible]

noncomputable instance Viterbi.instSemiringWithMonus :

SemiringWithMonus Viterbi

Viterbi is a commutative m-semiring. The natural order is the usual order on [0,1], and the monus is a if a > b, 0 if a ≤ b.

Equations

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

Dependency graph

source

@[instance_reducible]

noncomputable instance Viterbi.instCommSemiringWithMonus :

CommSemiringWithMonus Viterbi

Equations

Viterbi.instCommSemiringWithMonus = { toSemiringWithMonus := Viterbi.instSemiringWithMonus, mul_comm := Viterbi.instCommSemiringWithMonus._proof_1 }

Dependency graph

source

theorem Viterbi.not_mul_idempotent :

¬∀ (a : Viterbi), a * a = a

Viterbi multiplication is not idempotent: (1/2) * (1/2) = 1/4 ≠ 1/2.

Dependency graph

source

theorem Viterbi.not_isDelta_id :

¬IsDelta id

On Viterbi the identity is not an admissible δ, even though the semiring is absorptive (Viterbi.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 = 1/4 ≠ 1/2. This is why the instance takes the support indicator (ProvSQL's Viterbi::delta).

Dependency graph

source

theorem Viterbi.no_hom_from_BoolFunc {Y : Type} [Inhabited Y] :

∃ (ν : Y → Viterbi), ¬∃ (φ : BoolFunc Y →+* Viterbi), ∀ (i : Y), φ (BoolFunc.var i) = ν i

There is no semiring homomorphism from BoolFunc Y to Viterbi sending the variables to arbitrary values: Viterbi multiplication (ordinary product on [0,1]) is not idempotent, contradicting var i * var i = var i in BoolFunc Y.

Dependency graph

source

theorem Viterbi.mul_sub_left_distributive :

_root_.mul_sub_left_distributive Viterbi

Dependency graph

Documentation

Provenance.Semirings.Viterbi

Viterbi m-semiring #

References #