# Sequential decision problems, dependent types and generic solutions

arXiv: https://arxiv.org/abs/1610.07145 · HTML: https://mlsanity.com/paper/1610.07145/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Oct 2016.

## Built on by (most cited first, 1 of 1)

- [Reinforcement Learning in Categorical Cybernetics](https://mlsanity.com/paper/2404.02688/) (2024)

## Abstract (arXiv)

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.