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

Question

我正在关注 Agda 的 The Haskell Road to Logic, Maths and Programming。
书中指出:

The empty set is trivially a relation and is the smallest relation between two sets A and B

在 Agda :

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 _≤ℕ_

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

不能是空集，因为我之前已经将它定义为无人居住的类型

导致错误 Set₁ != Set when checking that the expression Set has type Set即使用不同的符号定义为 Ø : Relation 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