Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.viterbi

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/viterbi.clj2 definitions, 3 theorems

AHoF Viterbi Algorithm: find the single most-likely hidden-state sequence of a Hidden Markov Model given observations -- the standard decoder for HMMs (speech recognition, POS tagging, gene finding). The DP value delta_t(j) is the highest probability of any state path ending in state j at time t: path-prob prev transition emission = prev * transition * emission cell current-best candidate = max(current-best, candidate) where the candidate for predecessor i is delta_{t-1}(i) * a_ij * b_j(o_t), and the cell takes the max over predecessors, over exact-rational probabilities. Proved native and axiom-free: the path-probability product; a worked path probability; the max-selection cell (decidable rational max via logic/if-data); a worked cell; and the certificate that the surviving path probability dominates a competing one (native nnrat/at-most). The backpointer bookkeeping and observation sequence are executable; what is proved is the Viterbi cell recurrence. Requires nnrat/multiply, audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.viterbi` prints this classification.

viterbi/path-prob :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

viterbi/cell :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

viterbi/path-prob-example :
  → viterbi/path-prob 1/2 1/2 1 = 1/4

viterbi/keeps-most-probable :
  → viterbi/cell 1/4 1/2 = 1/2

viterbi/survivor-dominates :
  → 1/4 ≤ 1/2