agda - 如何在agda中定义实数？

Question

我想在 Agda (Ada)中实现Dedekind的剪切。我试图先代表实数。但是我无法在Agda中定义它。如何定义它？

Answer 1

实数可以在few different ways中构造:

遵循Erret Bishop在“构造分析”中构造实数之后，可以在Agda中将实数形式化为有理数序列，并证明该序列具有收敛性:

-- Constructible Real numbers as described by Bishop
-- A real number is defined to be a sequence along 
-- with a proof that the sequence is regular
record ℝ : Set where
  constructor Real
  field
    f : ℕ -> ℚ
    reg : {n m : ℕ} -> ∣ f n - f m ∣ ≤ (suc n)⁻¹ + (suc m)⁻¹

checkout this repository以使用此定义形式化等价关系。

定义实数的另一种方法是使用Dedekind cuts，如@vitrus所述，它在 the Homotopy Type Theory book的第11章中进行了讨论。