Skip to content

Research at St Andrews

Sequential decision problems, dependent types and generic solutions

Research output: Contribution to journalArticle

Author(s)

Nicola Botta, Patrik Jansson, Cezar Ionescu, David Christiansen, Edwin Charles Brady

School/Research organisations

Abstract

We present a computer-checked generic implementation for solving finite horizon sequential decision problems. This is a wide class of problems, including intertemporal 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.
Close

Details

Original languageEnglish
Article number7
Number of pages23
JournalLogical Methods in Computer Science
Volume13
Issue number1
DOIs
StatePublished - 17 Mar 2017

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Type driven development of concurrent communicating systems

    Brady, E. C. 7 Jul 2017 In : Computer Science. 18, 3, 22 p., 1413

    Research output: Contribution to journalArticle

  2. Type-driven development with Idris

    Brady, E. C. Mar 2017 Shelter Island: Manning Publications Co.480 p.

    Research output: Book/ReportBook

  3. Automatically proving equivalence by type-safe reflection

    Slama, F. & Brady, E. C. 2017 Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 40-55 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Elaborator reflection: extending Idris in Idris

    Christiansen, D. & Brady, E. C. 4 Sep 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. New York: ACM, p. 284-297

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. The Idris Programming Language: Implementing Embedded Domain Specific Languages with Dependent Types

    Brady, E. C. 2015 CEFP 2013. Springer, Vol. 8606

    Research output: Chapter in Book/Report/Conference proceedingChapter

Related by journal

  1. A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems

    Dyckhoff, R., Lengrand, S. & McKinna, J. H. 2011 In : Logical Methods in Computer Science. 7, 1:6, p. 1--35 35 p.

    Research output: Contribution to journalArticle

ID: 246979433