Closed forms for numerical loops
Closed forms for numerical loops
复制标题
数值循环的闭合形式
DOI：
10.1145/3290368
复制
发表时间：
2019
影响因子：
--
通讯作者：
T. Reps
中科院分区：
文献类型：
--
作者：
Zachary Kincaid;J. Breck;John Cyphert;T. Reps
本文研究了简单数值循环的非线性行为的推理问题。我们的方法建立在分析线性动力系统的行为的经典技术。众所周知，线性动力系统行为的封闭形式表示总是可以用代数数表示，但这种方法可能会创建对自动推理工具构成障碍的公式。本文描述了线性回路在更简单的理论中具有封闭形式时的特征，这些理论更适合自动推理。本文所描述的计算封闭形式的算法避免了使用代数数，并产生使用多项式和指数在有理数上表示的封闭形式。我们表明，表达封闭形式的逻辑是可判定的，产生的决策程序，验证安全性和终止的一类数字循环有理数。我们还表明，这类数值循环的计算封闭形式的程序可以用来过近似的任意数值程序的行为（不受限制的控制流，非确定性的分配，和递归程序）。
This paper investigates the problem of reasoning about non-linear behavior of simple numerical loops. Our approach builds on classical techniques for analyzing the behavior of linear dynamical systems. It is well-known that a closed-form representation of the behavior of a linear dynamical system can always be expressed using algebraic numbers, but this approach can create formulas that present an obstacle for automated-reasoning tools. This paper characterizes when linear loops have closed forms in simpler theories that are more amenable to automated reasoning. The algorithms for computing closed forms described in the paper avoid the use of algebraic numbers, and produce closed forms expressed using polynomials and exponentials over rational numbers. We show that the logic for expressing closed forms is decidable, yielding decision procedures for verifying safety and termination of a class of numerical loops over rational numbers. We also show that the procedure for computing closed forms for this class of numerical loops can be used to over-approximate the behavior of arbitrary numerical programs (with unrestricted control flow, non-deterministic assignments, and recursive procedures).