Menu
I am new to Agda. I'm reading the paper "Dependent Types at Work" by Ana Bove and Peter Dybjer. I don't understand the discussion of Finite Sets (on page 15 in my copy).
The paper defines a Fin type:
data Fin : Nat -> Set where fzero : {n : Nat} -> Fin (succ n) fsucc : {n : Nat} -> Fin n -> Fin (succ n) I must be missing something obvious. I don't understand how this definition works. Could someone simply translate the definition of Fin into everyday English? That might be all I need to understand this part of the paper.
Thanks for taking the time to read my question. I appreciate it.
601
Finite sets are the sets having a finite/countable number of members. Finite sets are also known as countable sets as they can be counted. The process will run out of elements to list if the elements of this set have a finite number of members. A set of all English Alphabets (because it is countable).
If a set is finite, its elements may be written — in many ways — in a sequence: In combinatorics, a finite set with n elements is sometimes called an n-set and a subset with k elements is called a k-subset. For example, the set {5,6,7} is a 3-set – a finite set with three elements – and {6,7} is a 2-subset of it.
Union of sets is actually defined as the joint junction of 2 or more sets. A union of 2 or more sets contains all the elements contained by the sets being unified. The union of two or more finite sets will always be a finite set, which can be understood since the sets being unified are finite sets.
data Fin : Nat -> Set where Fin is a data type parametrized by a natural number (or: Fin is a type-level function which takes a Nat and returns a Set (basic type), i.e. for any natural number n, Fin n is a Set).
fzero : {n : Nat} -> Fin (succ n) For all natural numbers n, fzero is a member of the type/set Fin (succ n), from which follows that for all positive numbers n (i.e. all naturals except zero), fzero is a member of Fin n.
fsucc : {n : Nat} -> Fin n -> Fin (succ n) For all natural numbers n and all values m of type Fin n, fsucc m is a member of type Fin (succ n).
So fzero is a member of Fin n for all n except zero and fsucc m is a member of Fin n for all n that represent a number greater than fsucc m.
Basically Fin n represents the Set of all natural numbers smaller than n, i.e. of all valid indices for lists of size n.
58
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
