Định nghĩa cho các tập hợp hữu hạn trong Agda

Question

Tôi mới sử dụng Agda. Tôi đang đọc bài báo "Các loại phụ thuộc tại nơi làm việc" của Ana Bove và Peter Dybjer. Tôi không hiểu cuộc thảo luận về Bộ hữu hạn (trên trang 15 trong bản sao của tôi).

giấy Các định nghĩa một loại Fin:

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

tôi phải mất một cái gì đó rõ ràng. Tôi không hiểu cách định nghĩa này hoạt động. Ai đó có thể dịch định nghĩa của Fin sang tiếng Anh hàng ngày? Đó có thể là tất cả những gì tôi cần để hiểu phần này của bài báo.

Cảm ơn bạn đã dành thời gian đọc câu hỏi của mình. Tôi đánh giá cao nó.

Answer 1

data Fin : Nat -> Set where 

Fin là một kiểu dữ liệu parametrized bởi một số tự nhiên (hoặc: Fin là một chức năng loại cấp mà phải mất một Nat và trả về một Set (loại cơ bản), tức là cho bất kỳ số tự nhiên nFin n là một Set).

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

Đối với tất cả các số tự nhiên nfzero là thành viên của các loại/thiết Fin (succ n) (từ mà sau đó cho tất cả các số dương tính (ví dụ: tất cả bẩm trừ zero) nfzero là thành viên của Fin n).

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

Đối với tất cả các số tự nhiên n và tất cả các giá trị m loại Fin n, fsucc m là thành viên của loại Fin (succ n).

---

Vì vậy fzero là thành viên của Fin n cho tất cả n trừ zero và fsucc m là thành viên của Fin n cho tất cả n mà đại diện cho một số lớn hơn fsucc m.

Về cơ bản Fin n đại diện cho Tập hợp tất cả các số tự nhiên nhỏ hơn n, nghĩa là tất cả các chỉ mục hợp lệ cho danh sách có kích thước n.