An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and potentially misleading plots, due to accuracy issues inherent to this use case. This paper investigates what it means for a plot to be correct and how to formally verify this property. The Coq proof assistant is then turned into a tool for plotting function graphs using reliable polynomial approximations. This feature is provided as part of the CoqInterval library.
翻译：计算机代数系统的一个非常宝贵的特征是它们能够绘制函数图。 不幸的是,当人们试图设计数学函数库时,由于这一使用案例本身的准确性问题,这一特征往往不尽人意,产生不正确和可能误导的图案。本文调查了图案正确的含义以及如何正式核实这一属性。然后, Coq 校对助理变成了一个使用可靠的多边近似值绘制函数图的工具。该特征作为 Coq Interval 库的一部分提供。
相关内容
微信扫码咨询专知VIP会员