Coq中的可计算分析与连续性概念
摘要：可计算分析领域的定理的若干种形式化证明；许多结果指定了可执行算法，通过对有限逼近的操作来处理无穷输入，并在可计算分析意义上被证明是正确的。该发展是在Coq证明助手中完成的，并且在信息论连续性方面严重依赖Incone库。该库由其中一位作者开发，本文可作为该库的介绍，因为它详细描述了许多最重要的特征。尽管能够在关于实数等的数学语句的正式发展中具有完全可执行性不是Incone库独有的特性，但它的原始贡献是遵守可计算分析的约定，为连续结构上的算法推理提供通用接口。提供完整计算内容的结果包括：实数上的代数运算和高效的极限运算符是可计算的，某些可数无穷积物是函数空间的同构，枚举表示法与自然数的开集空间的抽象定义的子集的兼容性，以及连续实现蕴含顺序连续性。我们还形式化证明支持我们定义正确性的非计算结果。其中包括：库中使用的信息论连续性概念与Baire空间上的度量连续性概念等价，来自度量和表示空间结构的不同连续性概念的完整比较，以及实数上的不受限极限运算符的不连续性和选择自然数的闭子集的元素的任务。
作者：Florian Steinberg and Laurent Thery and Holger Thies
论文ID：1904.13203
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22