agda - Agda中有限集的定义

Question

我是Agda的新手。我正在阅读Ana Bove和Peter Dybjer撰写的论文“工作中的依赖类型”。我不了解有限集的讨论(我的副本中的第15页)。

该文件定义了Fin类型:

data Fin : Nat -> Set where
    fzero : {n : Nat} -> Fin (succ n)
    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

我肯定想念一些明显的东西。我不明白这个定义是如何工作的。有人可以简单地将 Fin的定义翻译成日常英语吗？我可能只需要了解本文的这一部分。

感谢您抽出宝贵时间阅读我的问题。我很感激。

Answer 1

data Fin : Nat -> Set where

Fin是由自然数参数化的数据类型(或: Fin是一种类型级别的函数，它接受 Nat并返回 Set(基本类型)，即对于任何自然数 n Fin n都是 Set)。

    fzero : {n : Nat} -> Fin (succ n)

对于所有自然数 n fzero是类型/集合 Fin (succ n)的成员，对于所有正数 n(即除零以外的所有自然数)， fzero是 Fin n的成员。

    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

对于所有自然数 n和所有值 m的值 Fin n， fsucc m是 Fin (succ n)类型的成员。

因此，除零外， fzero是所有 Fin n的 n的成员，而 fsucc m是所有 Fin n的 n的成员，代表所有大于 fsucc m的数字。
基本上 Fin n表示小于 n的所有自然数的集合，即 n大小列表的所有有效索引的集合。