从共归纳证明到精确实算术：理论与应用
From coinductive proofs to exact real arithmetic: theory and applications
摘要：
基于连续函数的一个新的共归纳特征，我们从构造性证明中提取了精确实数计算的认证程序。提取的程序构造和组合精确的实数算法相对于实数的二进制有符号数字表示。对应于连续函数的共归纳定义的数据类型由描述算法何时写入和读取数字的非良基树组成。我们讨论了几个例子，包括提取多项式的程序，直到二次和连续映射的定积分。
英文摘要：
Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
