SeqDecProb

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).

Abstract

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.

LMCS-Topic

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