agda - Agda 中有限集的定义

Question

我是阿格达的新手。我正在阅读 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成日常英语吗？这可能是我理解本文这一部分所需的全部内容。

感谢您花时间阅读我的问题。我很感激。

score 26 · Accepted Answer

data Fin : Nat -> Set where

Fin 是由自然数参数化的数据类型（或者：Fin是一个类型级函数，它接受 aNat并返回 a Set（基本类型），即对于任何自然数n，Fin n是 a 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 nfsucc mFin (succ n)

Sofzero是除零以外Fin n的所有人的成员，并且是代表大于的数字的所有人的成员。nfsucc mFin nnfsucc m

基本上Fin n表示小于的所有自然数的集合n，即大小列表的所有有效索引的集合n。

1 回答 1