关于命令式程序的可判定增长率性质
计算机科学中的逻辑
2010-05-20 v1 编程语言
摘要
2008年，Ben-Amram、Jones和Kristiansen证明，对于一种简单的“核心”编程语言——一种具有有界循环且算术运算仅限于加法和乘法的命令式语言——可以精确判定程序是否具有某些增长率性质，即计算值或运行时间的多项式（或线性）界。这项工作强调了核心语言在缓解程序性质众所周知的不可判定性问题中的作用，从而处理可判定问题。一个自然且引人入胜的问题是，是否可以在保持增长率性质可判定的同时，向核心语言添加更多元素以提高其实用性。特别是，所提出的方法无法处理将变量重置为零的命令。本文展示了如何处理重置操作。该分析以逻辑风格（证明规则）给出，并证明其复杂度为PSPACE完全（相比之下，没有重置时，问题是PTIME的）。分析算法以有趣的方式从先前的解决方案演变而来：重点从证明界转向证伪界，并且算法采用自顶向下而非自底向上的工作方式。
引用
@article{arxiv.1005.0518,
title = {On Decidable Growth-Rate Properties of Imperative Programs},
author = {Amir M. Ben-Amram},
journal= {arXiv preprint arXiv:1005.0518},
year = {2010}
}