二进制有符号数字表示中实数的极限
摘要：从构造性证明中提取确切实数计算的验证算法。为此，我们使用实数的共递归表示作为二进制有符号数字流。本文的主要目标是对实数相对于极限的封闭性进行形式化证明。主定理和第一个应用的所有证明均在Minlog证明系统中进行实现，并进一步转换为Haskell。我们比较了两种方法。第一种方法是直接证明。在第二种方法中，我们利用了实数由一个柯西序列的有理数表示。利用两种表示之间的转换以及柯西实数的完备性，证明非常简短。在两种情况下，我们使用Minlog的程序提取机制自动提取一个经过形式验证的程序，该程序将一组收敛的实数序列，即一组二进制有符号数字流和收敛模数，转换为其极限的二进制有符号数字表示。提取项的正确性直接来自程序提取的健全性定理。作为第一个应用，我们使用提取的算法和Heron方法构造了一个相对于二进制有符号数字表示计算平方根的算法。在第二个应用中，我们使用收敛定理证明实数的有符号数字表示在乘法下是封闭的。
作者：Franziskus Wiesnet and Nils K"opp
论文ID：2103.15702
分类：Logic
分类简称：math.LO
提交时间：2023-06-22