The goal of this paper is to advertise the application of fixed points and ω-complete partial orders (ω-cpos) in the formalization and analysis of probabilistic programming languages. The presented work is formalized in the Isabelle theorem prover.
By applying ω-cpos to the analysis of MDPs we get a nice theory of fixed points. This allows us to transfer least and greatest fixed points through expectation on Markov chains and maximal and minimal expectation on MDPs. One application is to define the operational semantics of pGCL by MDPs, e.g. relating the denotational and operational semantics of pGCL is now a matter of fixed point equations and induction.
Note: After acceptance I discovered that large parts of the presented work were already developed by Monniaux [1]. Still, the main contribution of the presented work is the formalization in the interactive theorem prover Isablle/HOL.
