Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Markov chains and Markov decision processes in Isabelle/HOL
Hölzl J.  Journal of Automated Reasoning 59 (3): 345-387, 2017. Type: Article
Date Reviewed: Jan 11 2018

The intermingling of rather different domains can, at times, produce rather interesting results. Here the author explores the intersection of probability theory (in the guise of Markov chains and Markov decision processes) and formal proof (through the interactive theorem prover Isabelle/HOL), and even throws in some programming language semantics as an application. Given the explosion of interest in machine learning, the largest application of probability theory, and the current worries that parts of it are closer to alchemy than to modern science, it is rather important that certain parts of it be formally understood.

The task that the author has set for himself is rather clear, if daunting: based on some pre-existing foundations in Isabelle/HOL, formalize the theory around Markov chains and Markov decision processes. And, not content with just doing that, ensure that the resulting theories can be applied to work on both the operational and denotational semantics of a small probabilistic programming language. And, as if that weren’t enough, throw in a healthy measure of aesthetics, where the author chooses a nontraditional route to this formalization, namely via co-algebras, order theory, and fixed points.

The latter choice might seem like complete insanity to a classically minded mathematician. However, to a computer scientist steeped in the current best practices of formalization of the semantics of programming languages (like me), the thought is rather the opposite: that’s the only reasonable way to attack the problem! Satisfyingly, it is the latter opinion that proves to produce a “most efficient” formalization, as the author demonstrates.

This paper, which is fairly dense and fairly long, actually represents an even larger piece of work (278 pages!) of formalized mathematics, available online [1]. The author does an excellent job of providing an overview of the work and some of the background material before diving in to the actual contribution. The previously existing formalizations that could be reused are well documented, and the reason some were not reused but instead redone in a different way is also documented. A survey of related work is also given. The bulk of the paper and its contributions are in the three long sections: 3, 4, and 5.

Work such as this presents a conundrum: it should be done, it should be of this quality, and it should be published because it represents a significant scientific advance. The few people who are working on formalizing these topics in other systems should definitely read this paper. Anyone else? That is harder to say. It relies on quite a lot of background knowledge from different topics, which few will possess. I have only learned the appropriate material in the last two years. It is a research paper, not an introduction or a survey. I enjoyed it, even though I have no intention of formalizing this part of mathematics myself.

Reviewer:  Jacques Carette Review #: CR145764 (1803-0154)
1) Markov Models. (12/14/2017).
Bookmark and Share
  Editor Recommended
Featured Reviewer
Markov Processes (G.3 ... )
Formal Definitions And Theory (D.3.1 )
Mechanical Verification (F.3.1 ... )
Would you recommend this review?
Other reviews under "Markov Processes": Date
Answer set programming for non-stationary Markov decision processes
Ferreira L., Bianchi R., Santos P., Lopez de Mantaras R.  Applied Intelligence 47(4): 993-1007, 2017. Type: Article
Mar 13 2018
MixedTrails: Bayesian hypothesis comparison on heterogeneous sequential data
Becker M., Lemmerich F., Singer P., Strohmaier M., Hotho A.  Data Mining and Knowledge Discovery 31(5): 1359-1390, 2017. Type: Article
Dec 7 2017
Markov chain aggregation for agent-based models
Banisch S.,  Springer International Publishing, New York, NY, 2015. 195 pp. Type: Book (978-3-319248-75-2)
Jul 12 2017

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2019 ThinkLoud, Inc.
Terms of Use
| Privacy Policy