Documentation

Provenance.Semirings.Viterbi

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 #

source
def Viterbi :
Type

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

Equations
Instances For
    source
    @[implicit_reducible]
    instance Viterbi.instCoeNNReal :
    Coe Viterbi NNReal
    Equations
    source
    theorem Viterbi.ext {a b : Viterbi} (h : ↑a = ↑b) :
    a = b
    source
    theorem Viterbi.ext_iff {a b : Viterbi} :
    a = b ↔ ↑a = ↑b
    source
    @[simp]
    theorem Viterbi.coe_mk (p : NNReal) (hp : p ≤ 1) :
    ↑⟨p, hp⟩ = p
    source
    @[implicit_reducible]
    instance Viterbi.instZero :
    Zero Viterbi
    Equations
    source
    @[implicit_reducible]
    instance Viterbi.instOne :
    One Viterbi
    Equations
    source
    @[implicit_reducible]
    instance Viterbi.instAdd :
    Add Viterbi
    Equations
    source
    @[implicit_reducible]
    instance Viterbi.instMul :
    Mul Viterbi
    Equations
    source
    @[simp]
    theorem Viterbi.zero_def :
    ↑0 = 0
    source
    @[simp]
    theorem Viterbi.one_def :
    ↑1 = 1
    source
    @[simp]
    theorem Viterbi.add_def (a b : Viterbi) :
    ↑(a + b) = max ↑a ↑b
    source
    @[simp]
    theorem Viterbi.mul_def (a b : Viterbi) :
    ↑(a * b) = ↑a * ↑b
    source
    @[implicit_reducible]
    instance Viterbi.instCommSemiring :
    CommSemiring Viterbi
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem Viterbi.viterbi_order_le (a b : Viterbi) :
    ↑a ≤ ↑b ↔ a + b = b
    source
    @[implicit_reducible]
    instance Viterbi.instPartialOrder :
    PartialOrder Viterbi
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[simp]
    theorem Viterbi.le_def (a b : Viterbi) :
    a ≤ b ↔ ↑a ≤ ↑b
    source
    @[implicit_reducible]
    noncomputable instance Viterbi.instSub :
    Sub Viterbi
    Equations
    source
    instance Viterbi.instIsOrderedAddMonoid :
    IsOrderedAddMonoid Viterbi
    source
    instance Viterbi.instCanonicallyOrderedAdd :
    CanonicallyOrderedAdd Viterbi
    source
    instance Viterbi.instNontrivial :
    Nontrivial Viterbi
    source
    theorem Viterbi.absorptive :
    _root_.absorptive Viterbi
    source
    theorem Viterbi.idempotent :
    _root_.idempotent Viterbi
    source
    instance Viterbi.instCharPZero :
    CharP Viterbi 0

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

    source
    @[implicit_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.
    source
    @[implicit_reducible]
    noncomputable instance Viterbi.instCommSemiringWithMonus :
    CommSemiringWithMonus Viterbi
    Equations
    source
    theorem Viterbi.not_mul_idempotent :
    ¬∀ (a : Viterbi), a * a = a

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

    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.

    source
    theorem Viterbi.mul_sub_left_distributive :
    _root_.mul_sub_left_distributive Viterbi