Coq 中的可计算分析与连续性概念
计算机科学中的逻辑
2023-06-22 v5
摘要
我们给出可计算分析领域中若干定理的形式化证明。我们的许多结果指定了可执行算法，这些算法通过对有限近似进行操作来处理无限输入，并在可计算分析意义下被证明正确。该开发在证明助手 Coq 中完成，并严重依赖用于信息论连续性的 Incone 库。该库由作者之一开发，本文可作为该库的入门介绍，详细描述了其许多最重要的特性。虽然在对实数等数学陈述的形式化开发中具备完全可执行性并非 Incone 库独有，其原创贡献在于遵循可计算分析惯例，为连续结构上的算法推理提供通用接口。提供完整计算内容的结果包括：实数上的代数运算与高效极限算子是可计算的；某些可数无穷乘积同构于函数空间；自然数子集的枚举表示与自然数开子集空间的抽象定义兼容；以及连续可实现性蕴含序列连续性。我们还形式化了支持我们定义正确性的非计算结果的证明。这些包括：库中使用的信论连续性概念等价于 Baire 空间上的度量连续性；由度量和表示空间结构产生的不同连续性概念的完整比较；以及无限制实数极限算子和从自然数闭子集选取元素任务的间断性。
引用
@article{arxiv.1904.13203,
title = {Computable analysis and notions of continuity in Coq},
author = {Florian Steinberg and Laurent Thery and Holger Thies},
journal= {arXiv preprint arXiv:1904.13203},
year = {2023}
}