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是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 n,fsucc m是类型的成员Fin (succ n).

所以fzero是其成员Fin n的所有n除零和fsucc m是其成员Fin n的所有n代表一个大于fsucc m.

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