一句话：用依赖类型语言给出有限时程序列决策问题的计算机检查通用实现与贝尔曼最优性原理证明。
本文研究有限时程序列决策问题，其涵盖跨期优化、背包、最优括号化、调度等广泛问题。作者在 Idris 与 Agda 等依赖类型语言中实现了一个通用求解框架，能够处理随离散时间步变化的控制空间与状态空间，并以 monad 表示随机、非确定、模糊及其组合等不确定性。依赖类型不仅支持这种高度泛化，还使贝尔曼最优性原理及相应逆向归纳算法得以形式化和机器检查证明。该形式化澄清了逆向归纳的一些方面，并通过显式刻画可行性与可达性，为气候影响研究等领域常见的 monadic 动力系统可控性理论提供起点。
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. Comment: 23 pages, 2 figures
@article{paperbot203,
title = {Sequential decision problems, dependent types and generic solutions},
author = {Nicola Botta and Patrik Jansson and Cezar Ionescu and David R. Christiansen and Edwin Brady},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/lmcs-13(1:7)2017}
}