Loading…

Sequential decision problems, dependent types and generic solutions

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

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2017, Vol.13 (1)
Main Authors: Botta, N., Jansson, Patrik, Ionescu, Cesar, Christiansen, D. R., Brady, E.
Format: Article
Language:English
Subjects:
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
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.
ISSN:1860-5974
1860-5974
DOI:10.23638/LMCS-13(1:7)2017