Sequential decision problems, dependent types and generic solutions
Authors: Nicola Botta, Patrik Jansson, Cezar Ionescu, David Christiansen and Edwin Brady
- 2014-08-15: Paper submitted to LMCS.
- 2015-01-13: Source code repository for this paper and a follow-up is being migrated to github
- (2015-03-28: A follow-up paper (aimed at a different audience) submitted to MSS.)
- 2015-06-02: LMCS reviews (with many useful suggestions) finally arrive basically saying "revise and resubmit".
- 2015-07-29: Paper resubmitted to LMCS (Pre-print).
We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman's principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research.
Logics of programs, Program development and specification, Formalized mathematics, Reasoning about actions and planning, Functional programming and lambda calculus, Interactive proof checking, Type theory and constructive mathematics, Computer-aided verification