agda - Agdaの有限集合の定義

Question

私はアグダに不慣れです。AnaBoveとPeterDybjerによる「DependentTypesatWork」という論文を読んでいます。有限集合の説明（私のコピーの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 は、自然数によってパラメーター化されたデータ型です (または:は、 a を取り、 a (基本型)を返すFin型レベルの関数です。つまり、任意の自然数に対して、は aです)。NatSetnFin nSet

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

すべての自然数についてn、fzeroは型/セットのメンバーであり、Fin (succ n)それから、すべての正の数n(つまり、ゼロを除くすべての自然数) についてfzeroはのメンバーですFin n。

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

すべての自然数nと type のすべての値に対してm、 typeFin nのfsucc mメンバーですFin (succ n)。

fzeroはゼロ以外のFin nfor allのメンバーであり、より大きい数値を表すfor allのメンバーです。nfsucc mFin nnfsucc m

基本Fin n的に、より小さいすべての自然数のセットn、つまりサイズのリストのすべての有効なインデックスのセットを表しますn。

1 に答える 1