复数、具有分支切割的函数等存在下的程序验证
符号计算
2014-04-25 v1
摘要
在考虑数值程序的可靠性时，通常“将我们的研究局限于处理数值精度的语义”(Martel, 2005)。另一方面，有大量关于程序可靠性的工作基本上忽略了数值问题。本文的论点是存在一类介于这两者之间的问题，可以描述为“底层算术是否实现了高层数学”。许多此类问题的产生是因为数学，特别是复数数学，比预期的更困难：例如，复函数 log 不连续，编写计算逆函数的程序比仅仅解方程更复杂，并且许多代数简化规则并非普遍有效。好消息是，这些问题在理论上能够解决，并且在几个现实世界的例子中实际上已接近解决，但尚未完全解决。然而，在实现匹配理论可能性之前，仍有很长的路要走。
引用
@article{arxiv.1212.5417,
title = {Program Verification in the presence of complex numbers, functions with branch cuts etc},
author = {James H. Davenport and Russell Bradford and Matthew England and David Wilson},
journal= {arXiv preprint arXiv:1212.5417},
year = {2014}
}