在抽象精确实数上形式化波兰空间子集上的超空间与运算

基于我们先前在构造性依赖类型论中形式化实数和复数上的非确定性一阶部分计算以实现精确实数计算公理化的工作，我们提出了一个框架，通过形式化各种高阶数据类型和运算，在子集超空间上进行认证计算。我们首先以抽象拓扑方式定义一般空间上的开子集、闭子集、紧子集和开核子集，这种方式允许简洁优雅的证明，其计算内容与可计算分析和构造性数学中的标准定义一致。从这些证明中，我们可以提取用于测试集合包含、重叠等的程序。为了提高提取程序的效率，我们随后聚焦于波兰空间，在那里我们基于空间的度量性质给出更高效的编码。由于各种计算性质依赖于编码函数的连续性，我们引入了一个非确定性的连续性原理版本，该原理在我们的形式化中很自然，并且在标准的第二型可实现性解释下是有效的。利用这一原理，我们进一步推导了通用编码和度量编码之间的计算等价性。我们的理论已在Coq证明助手中完全实现。从该Coq形式化中的证明中，我们可以提取用于子集上无误差运算的认证程序。作为一个应用，我们提供了一个函数，该函数通过极限运算从迭代函数系统构造欧几里得空间中的分形，例如谢尔宾斯基三角形。所得程序可用于绘制任意所需分辨率下的此类分形。