实数的单子函数实现

大规模实数计算是许多现代数学证明中的关键要素。由于此类冗长计算无法通过手工验证，因此一些数学家希望使用软件证明助手来验证这些证明的正确性。本文通过利用度量空间完成运算的单子特性，发展出一种用于此类证明的构造实数的新实现方法以及初等函数。将Bishop和Bridges的正则序列概念推广到我称为正则函数的概念，这些函数形成任何度量空间的完成。使用单子运算，length空间上连续函数（一种常见的度量空间子类）通过提升原始空间上的连续函数来创建。已创建原型Haskell实现。我相信，这种方法产生的实数库在计算上相对高效，并且仍然足够简单，以便轻易验证其正确性。