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...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2017-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/3191/pdf |
| _version_ | 1797268612576182272 |
|---|---|
| author | Nicola Botta Patrik Jansson Cezar Ionescu David R. Christiansen Edwin Brady |
| author_facet | Nicola Botta Patrik Jansson Cezar Ionescu David R. Christiansen Edwin Brady |
| author_sort | Nicola Botta |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:15Z |
| format | Article |
| id | doaj.art-26cc1087053f4b338c3fe8bd22bfac07 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:15Z |
| publishDate | 2017-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-26cc1087053f4b338c3fe8bd22bfac072024-03-08T09:49:43ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742017-03-01Volume 13, Issue 110.23638/LMCS-13(1:7)20173191Sequential decision problems, dependent types and generic solutionsNicola BottaPatrik JanssonCezar IonescuDavid R. ChristiansenEdwin BradyWe 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.https://lmcs.episciences.org/3191/pdfcomputer science - logic in computer science |
| spellingShingle | Nicola Botta Patrik Jansson Cezar Ionescu David R. Christiansen Edwin Brady Sequential decision problems, dependent types and generic solutions Logical Methods in Computer Science computer science - logic in computer science |
| title | Sequential decision problems, dependent types and generic solutions |
| title_full | Sequential decision problems, dependent types and generic solutions |
| title_fullStr | Sequential decision problems, dependent types and generic solutions |
| title_full_unstemmed | Sequential decision problems, dependent types and generic solutions |
| title_short | Sequential decision problems, dependent types and generic solutions |
| title_sort | sequential decision problems dependent types and generic solutions |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/3191/pdf |
| work_keys_str_mv | AT nicolabotta sequentialdecisionproblemsdependenttypesandgenericsolutions AT patrikjansson sequentialdecisionproblemsdependenttypesandgenericsolutions AT cezarionescu sequentialdecisionproblemsdependenttypesandgenericsolutions AT davidrchristiansen sequentialdecisionproblemsdependenttypesandgenericsolutions AT edwinbrady sequentialdecisionproblemsdependenttypesandgenericsolutions |