顺序决策问题，依赖类型和通用解决方案
摘要：计算机检查的通用实现用于解决有限时间顺序决策问题。这是一类广泛的问题，包括时间跨度最优化、背包问题、最优配对、调度等等。该实现可以处理时间步相关的控制和状态空间，以及不确定性的单调表示（如随机、不确定、模糊或组合）。这种级别的通用性可以在具有依赖类型的编程语言（我们使用了Idris和Agda）中实现。依赖类型也是我们获得实现的核心组件Bellman最优原理和相关的后向归纳算法的形式化和计算机检查证明的手段。该形式化澄清了后向归纳的某些方面，并通过明确可行性和可达性等概念，成为单调动力系统可控性理论的起点，这在气候影响研究等领域经常遇到。
作者：Nicola Botta, Patrik Jansson, Cezar Ionescu, David R. Christiansen, Edwin Brady
论文ID：1610.07145
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22