论文标题
使用连续物体计算：统一的共感性方法
Computing with Continuous Objects: A Uniform Co-inductive Approach
论文作者
论文摘要
出现了使用无限对象，例如实数，这些元素，紧凑型集和均匀连续地图的统一计算方法。在Berger的工作中，它显示了如何从建设性证明中提取与签名数字表示的认证算法。伯杰（Berger）和现任作者将这种方法概括为完成度量空间，并展示了如何处理紧凑型集合。在这里，我们统一了这项工作，并为应用程序中发生的更全面的紧凑型豪斯多夫空间做了类似的基础。该方法与Weihrauch的型号有效性理论具有相同的计算能力。
A uniform approach to computing with infinite objects like real numbers, tuples of these, compacts sets, and uniformly continuous maps is presented. In work of Berger it was shown how to extract certified algorithms working with the signed digit representation from constructive proofs. Berger and the present author generalised this approach to complete metric spaces and showed how to deal with compact sets. Here, we unify this work and lay the foundations for doing a similar thing for the much more comprehensive class of compact Hausdorff spaces occurring in applications. The approach is of the same computational power as Weihrauch's Type-Two Theory of Effectivity.
