一句话：用依赖类型构造性地形式化政策建议、生存性、可达性与可避免性，并研究其可判定条件与通用评估过程。
本文为政策建议与可避免性问题建立计算理论的初步框架。作者将政策、生存性、可达性等概念形式化，并提出以“可避免性”为核心辅助决策的新思路：把可避免性定义为当前状态与未来状态之间的关系，考察该关系在何种条件下可判定，并给出评估可避免性的通用过程。形式化采用构造性方法，充分利用依赖类型与逻辑命题之间的对应，使可判定判断可通过计算获得。论文强调该工作属于计算理论，旨在凸显计算机科学在全球系统科学中可用于政策分析与决策支持的作用；评估以理论构造与可判定性分析为主，未涉及实证或工具实现。
Abstract We present the starting elements of a mathematical theory of policy advice and avoidability. More specifically, we formalize a cluster of notions related to policy advice, such as policy , viability , reachability , and propose a novel approach for assisting decision making, based on the concept of avoidability . We formalize avoidability as a relation between current and future states, investigate under which conditions this relation is decidable and propose a generic procedure for assessing avoidability. The formalization is constructive and makes extensive use of the correspondence between dependent types and logical propositions, decidable judgments are obtained through computations. Thus, we aim for a computational theory, and emphasize the role that computer science can play in global system science.
@article{BottaJI17,
title = {Contributions to a computational theory of policy advice and avoidability},
author = {NICOLA BOTTA and PATRIK JANSSON and CEZAR IONESCU},
journal = {Journal of Functional Programming},
volume = {27},
year = {2017},
doi = {10.1017/s0956796817000156}
}