下面这个文章非常有意思。其理论基础是constructive real analysis。
换言之，其回到了Poincare的观点。
Poincare的思路是这样的。
数学的第一概念是计算。
而不是numbers，几何,代数等结构和对象。
数学系统应该这样来建设。
先有不言自明的计算概念。
然后根据计算来定义numbers等其他东西。
例如有了计算之后，real numbers之定义很简单。
real numbers定义为一个计算机程序之输出。
也就是说，实数是一个程序。
所以不可计算数不存在。康托集合论，罗素悖论，哥德尔定理就全没了。
这是个很爽快的解决办法！
作者等于是(部分的）实证了这件事。（见4.4开头的定义）
This serves as the starting point for our work. It uses a fundamentally
different approach: A real number 𝑥 is represented
as a computable function 𝑓𝑥 mapping an error tolerance &#
119890; to
a rational number 𝑓𝑥 (𝑒), such that the difference
between 𝑥
and 𝑓𝑥 (𝑒) is less than the error tolerance 𝑒
;. https://dl.acm.org/doi/pdf/10.1145/3385412.3386037
Towards an API for the real numbers
Share on
Author:
Hans-J. Boehm
Authors Info & Affiliations
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming
Language Design and ImplementationJune 2020 Pages 562–576https://doi.org/10
.1145/3385412.3386037
