CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Sequential decision problems, dependent types and generic solutions

Nicola Botta ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) ; Institutionen för data- och informationsteknik (Chalmers)) ; Cezar Ionescu (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; David R. Christiansen ; Edwin Brady
Logical Methods in Computer Science (1860-5974). (2016)
[Artikel, refereegranskad vetenskaplig]

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.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-10-25. Senast ändrad 2016-10-25.
CPL Pubid: 244213