Определение конечных множеств в Агде

Question

Я новичок в Агде.Я читаю статью «Зависимые типы в работе» Аны Бове и Питера Дибьер.Я не понимаю обсуждения конечных множеств (на странице 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.