On the correctness of monadic backward induction

In control theory, to solve a finite-horizon sequential decision problem (SDP) commonly means to find a list of decision rules that result in an optimal expected total reward (or cost) when taking a given number of decision steps. SDPs are routinely solved using Bellman's backward induction. Textbooks typically give more or less formal proofs to show that the backward induction algorithm is correct as solution method for deterministic and stochastic SDPs. In Botta et al. 2017, the authors propose a generic framework for finite horizon, monadic SDPs together with a verified monadic version of backward induction for solving such SDPs. In monadic SDPs, the monad captures a generic notion of uncertainty, while a generic measure function aggregates rewards. In the present paper we extend Botta et al.'s verification result. Under certain conditions on the measure function, we obtain a correctness result for monadic backward induction that is comparable to textbook correctness proofs for ordinary backward induction. The conditions that we impose are fairly general and can be cast in category-theoretical terms using the notion of Eilenberg-Moore-algebra. They hold for familiar measures like the expected value but also imply that certain measures cannot be used for optimization within the Botta et al. framework. Our development is formalized in Idris as an extension of the framework and the sources are available as supplementary material.