Nicola Botta ; Patrik Jansson ; Cezar Ionescu ; David R. Christiansen ; Edwin Brady - Sequential decision problems, dependent types and generic solutions

lmcs:3191 - Logical Methods in Computer Science, March 17, 2017, Volume 13, Issue 1 - https://doi.org/10.23638/LMCS-13(1:7)2017
Sequential decision problems, dependent types and generic solutionsArticle

Authors: Nicola Botta ; Patrik Jansson ; Cezar Ionescu ; David R. Christiansen ; Edwin Brady

    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.


    Volume: Volume 13, Issue 1
    Published on: March 17, 2017
    Accepted on: March 17, 2017
    Submitted on: March 17, 2017
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Center of Excellence for Global Systems Science; Funder: European Commission; Code: 676547
    • Global systems Rapid Assessment tools through Constraint FUnctional Languages; Funder: European Commission; Code: 640954

    1 Document citing this article

    Consultation statistics

    This page has been seen 1685 times.
    This article's PDF has been downloaded 520 times.