Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Markov chains and Markov decision processes in Isabelle/HOL
Hölzl J. Journal of Automated Reasoning59 (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. https://www.isa-afp.org/entries/Markov_Models.html (12/14/2017).
Bookmark and Share
  Editor Recommended
Featured Reviewer
 
 
Markov Processes (G.3 ... )
 
 
Mechanical Verification (F.3.1 ... )
 
 
Formal Definitions And Theory (D.3.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Markov Processes": Date
Continuous-time Markov chains and applications
Yin G., Zhang Q., Springer-Verlag New York, Inc., New York, NY, 1998. Type: Book (9780387982441)
Jan 1 1999
Stochastic dynamic programming and the control of queueing systems
Sennott L., Wiley-Interscience, New York, NY, 1999. Type: Book (9780471161202)
Jan 1 1999
Lower bounds for randomized mutual exclusion
Kushilevitz E., Mansour Y., Rabin M., Zuckerman D. SIAM Journal on Computing 27(6): 1550-1563, 1998. Type: Article
Jul 1 1999
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy