| Summary: | 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.
|
|---|