Viterbi.h File Reference

Viterbi (max-times) m-semiring over \([0,1]\). More...

#include <algorithm>
#include <numeric>
#include <vector>
#include "Semiring.h"

Include dependency graph for Viterbi.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	semiring::Viterbi
	The Viterbi (max-times) m-semiring over double. More...

Namespaces
namespace	semiring

Detailed Description

Viterbi (max-times) m-semiring over \([0,1]\).

The Viterbi m-semiring ( \([0,1]\), \(\max\), \(\times\), 0, 1) is used to model most-likely-derivation provenance: input gates carry probabilities, \(\oplus = \max\) keeps the most likely derivation, and \(\otimes = \times\) multiplies probabilities along a derivation.

Operations:

• zero() → 0
• one() → 1
• plus() → maximum of all operands (empty list → 0)
• times() → product of all operands (empty list → 1)
• monus() → 0 if \(a \le b\), \(a\) otherwise
• delta() → 1 if x is non-zero, else 0

Absorptivity: absorptive() returns true. With inputs in \([0,1]\), \(\mathbb{1} \oplus a = \max(1, a) = 1\). The circuit evaluator may exploit the resulting idempotency to deduplicate operands.

Note

No bounds checking is performed: it is the caller's responsibility to supply input probabilities in \([0,1]\).

See also

https://provsql.org/lean-docs/Provenance/Semirings/Viterbi.html Lean 4 verified instance: instSemiringWithMonusViterbi, with proofs of Viterbi.absorptive, Viterbi.idempotent, and Viterbi.mul_sub_left_distributive.

Definition in file Viterbi.h.