这种空集的形式化在 Agda 中是否正确？

Question

我在 Agda 关注 Haskell Road to Logic、Maths and Programming。 书中写道：

空集是平凡的关系，是两个集合 A 和 B 之间的最小关系

在阿格达：

data ∅ : Set where

record ⊤ : Set where

record Σ (A : Set) (B : A → Set) : Set₁ where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁

_×_ : Set → Set → Set₁
A × B = Σ A (λ _ → B)
infixr 5 _×_ _,_

Relation : Set → Set₁
Relation P = P × P → Set

这样，我可以定义特定集合的关系：

lteℕ : Relation ℕ
lteℕ(x , y) = x ≤ℕ y where
  _≤ℕ_ : ℕ → ℕ → Set
  O ≤ℕ O = ⊤
  O ≤ℕ S y = ⊤
  S x ≤ℕ O = ∅
  S x ≤ℕ S y = x ≤ℕ y
  infixr 5 _≤ℕ_

但现在我有一个问题，因为空集关系的签名：

1. 不能是空集，因为我之前已经定义为无人居住类型了
2. 由于需要避免语言中的罗素悖论，即使使用不同的符号定义为 Ø : Relation Set 也会导致错误 Set₁ != Set when checking that the expression Set has type Set。

有没有一种在逻辑上仍然一致的方法？谢谢！

Answer 1

答案取决于你所说的集合。如果集合是指数学集合的表示，例如列表，则空集合仅由空列表表示。

如果你所说的集合是指 Agda Set 表示类型，那么答案有点复杂：没有 空类型，但有尽可能多的你能想到的。更准确地说，空类型与未提供任何构造函数的数据类型一样多。那么问题就变成了“我选择这些类型中的哪一种来为空集建模？”而不是“我如何为空集建模？”。

这是一个强调这一方面的 agda 模块示例：首先，我有一些导入和我的模块的标题：

open import Agda.Primitive
open import Data.Nat hiding (_⊔_)

module EmptySets where

那我从一个空类型开始，你能想到的越简单：

data Empty : Set where

从这个数据类型，可以写出一个消除器：

Empty-elim : ∀ {a} {A : Set a} → Empty → A
Empty-elim ()

这基本上是说如果Empty 成立，任何事情都成立。

但是，我也可以选择将空集表示为空关系，方法是定义一个类型族，所有类型都是空的，它们都是关系。首先，需要定义关系（我从标准库中获取了定义）：

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ lsuc ℓ)
REL A B ℓ = A → B → Set ℓ

然后可以定义空关系族：

data EmptyRelation {a b ℓ} {A : Set a} {B : Set b} : REL A B ℓ where

由于所有这些类型都是空的，它们都提供了一个消除器：

EmptyRelation-elim : ∀ {a b x ℓ} {A : Set a} {B : Set b} {X : Set x} {u : A} {v : B} → EmptyRelation {ℓ = ℓ} u v → X
EmptyRelation-elim ()

因此，可以实例化此泛型类型以获得特定的空类型，例如自然数上的空关系，它永远不会成立：

EmptyNaturalRelation : REL ℕ ℕ lzero
EmptyNaturalRelation = EmptyRelation

这就是书中所解释的：因为关系是一组对，那么空类型是这个关系中最小的一个：其中没有对。

但你也可以使用谓词而不是关系，说空集是给定类型的最小谓词：永远不成立的谓词，在这种情况下，它表示如下：

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Pred A ℓ = A → Set ℓ

data EmptyPredicate {a ℓ} {A : Set a} : Pred A ℓ where

您甚至可以更疯狂地决定将空集建模如下：

data EmptySomething {a} {A B C D E Z : Set a} : A → B → C → D → E → Z → Set where

总而言之，agda 中不存在空集，但空类型可能无穷无尽。

---

至于您在问题中提供的代码，有几个不准确之处：

• 关系通常是在两个参数而不是成对的参数上定义的，如果需要的话，您可以对它们进行curry，以使它们将一对作为参数。

• 为什么要让lteℕ 依赖于_≤ℕ_ 而不是直接定义呢？

• 您应该将lteℕ 定义为数据类型，而不是返回底部或顶部的函数，这将允许您在将来对此类术语进行大小写拆分。通常，这是这样定义的（在标准库中）：

  data _≤_ : Rel ℕ 0ℓ where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n