Hidden Markov Models

Title:	Hidden Markov Models
Author:	Simon Wimmer
Submission date:	2018-05-25
Abstract:	This entry contains a formalization of hidden Markov models [3] based on Johannes Hölzl's formalization of discrete time Markov chains [1]. The basic definitions are provided and the correctness of two main (dynamic programming) algorithms for hidden Markov models is proved: the forward algorithm for computing the likelihood of an observed sequence, and the Viterbi algorithm for decoding the most probable hidden state sequence. The Viterbi algorithm is made executable including memoization. Hidden markov models have various applications in natural language processing. For an introduction see Jurafsky and Martin [2].
BibTeX:	@article{Hidden_Markov_Models-AFP, author = {Simon Wimmer}, title = {Hidden Markov Models}, journal = {Archive of Formal Proofs}, month = may, year = 2018, note = {\url{http://isa-afp.org/entries/Hidden_Markov_Models.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Markov_Models, Monad_Memo_DP
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.