如何在agda中定义实数？

Question

我想实现Dedekind在Agda中的切入.我试图先代表实数.但我无法在Agda中定义它.如何定义？

Answer 1

实数可以用几种不同的方式构造：

\n\n

遵循 Erret Bishop 在构造分析中构建实数中对实数的构造，实数可以在 Agda 中形式化为有理数序列以及该序列的收敛性证明：

\n\n

-- Constructible Real numbers as described by Bishop\n-- A real number is defined to be a sequence along \n-- with a proof that the sequence is regular\nrecord \xe2\x84\x9d : Set where\n  constructor Real\n  field\n    f : \xe2\x84\x95 -> \xe2\x84\x9a\n    reg : {n m : \xe2\x84\x95} -> \xe2\x88\xa3 f n - f m \xe2\x88\xa3 \xe2\x89\xa4 (suc n)\xe2\x81\xbb\xc2\xb9 + (suc m)\xe2\x81\xbb\xc2\xb9\n

\n\n

签出这个存储库了解使用此定义的等价关系的形式化构造。

\n\n

定义实数的另一种方法是使用 Dedekind cut，正如 @vitrus 提到的，在同伦类型理论一书中的第 11 章中讨论了这种方法

\n