在复数、具有分支截断等情况下的程序验证
摘要：数值程序的可靠性主要关注数字精度的语义限制。然而，对于程序可靠性的研究通常忽略了数字计算。本论文的主题是存在一类问题介于这两者之间，可以描述为“低级算术是否实现了高级数学”。许多这类问题是因为数学，特别是复数的数学，比预期更加困难：例如，复杂函数log不是连续的，编写计算逆函数的程序比仅仅求解一个方程更加复杂，许多代数化简规则不是普适的。 好消息是，这些问题在理论上是可解的，并且在几个现实世界的例子中实际上已经很接近解决。然而，在实现上与理论可能性相匹配还有很长的路要走。
作者：James H. Davenport, Russell Bradford, Matthew England and David Wilson
论文ID：1212.5417
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2014-04-25