• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Symposium on Symbolic and Algebraic Computation Aug 3-6, 2003 Philadelphia, Pennsylvania, USA >High-level Proofs of Mathematical Programs Using Automatic Differentiation, Simplification, and some Common Sense
【24h】

High-level Proofs of Mathematical Programs Using Automatic Differentiation, Simplification, and some Common Sense

机译：使用自动微分，简化和一些常识的数学程序的高级证明

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

One problem in applying elementary methods to prove correctness of interesting scientific programs is the large discrepancy in level of discourse between low-level proof methods and the logic of scientific calculation, especially that used in a complex numerical program. The justification of an algorithm typically relies on algebra or analysis, but the correctness of the program requires that the arithmetic expressions are written correctly and that iterations converge to correct values in spite of truncation of infinite processes or series and the commission of numerical roundoff errors. We hope to help bridge this gap by showing how we can, in some cases, state a high-level requirement and by using a computer algebra system (CAS) demonstrate that a program satisfies that requirement. A CAS can contribute program manipulation, partial evaluation, simplification or other algorithmic methods. A novelty here is that we add to the usual list of techniques automatic differentiation, a method already widely used in optimization contexts where algorithms are differentiated. We sketch a proof of a numerical program to compute sine, and display a related approach to a version of a Bessel function algorithm for J_0(x) based on a recurrence.
机译：应用基本方法来证明有趣的科学程序的正确性的一个问题是，低层次的证明方法与科学计算的逻辑（尤其是用于复杂数值程序的逻辑）之间的论述水平存在很大差异。算法的合理性通常依赖于代数或分析，但程序的正确性要求正确地编写算术表达式，并且尽管无穷多个过程或序列被截断并且产生了数字舍入误差，但迭代收敛到正确的值。我们希望通过展示在某些情况下如何陈述高级要求并通过使用计算机代数系统（CAS）演示程序满足该要求来帮助弥合这一差距。 CAS可以有助于程序操纵，部分评估，简化或其他算法方法。这里的新颖之处在于，我们在通常的技术列表中增加了自动微分，这是一种在算法被区分的优化环境中已经广泛使用的方法。我们绘制了一个用于计算正弦的数值程序的证明，并基于递归显示了针对J_0（x）的贝塞尔函数算法版本的相关方法。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号