Agda tutorial を読んでみた: Sets (2)
今回は Constant Definitions から Parametric Sets まで。
Constant Definitions
nine : ℕ nine = suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) ten : ℕ ten = suc nine
(定数名) = (式) の形式で定数を定義することができます。 定義の前行に (定数名) : (型) の形式で定数の型を明示しています。 この型は曖昧にならない範囲で省略することができます。
ten
, suc nine
, そして suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))
はどれも自然数10を表現しています。
この中で suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))
のようにコンストラクタだけで表現されたものを 標準形 (normal form) と呼びます。
Decimal Notation for Natural Numbers
zero
と suc
を使った自然数の表現だと、3 あたりから値がいくつなのか把握するのが難しくなってきます。
かといって毎回値に名前をつけるのも面倒です。
幸いなことに、標準ライブラリで定義されている自然数 ℕ では値を十進数で表記することができます。
標準ライブラリの Data.Nat モジュールには自然数を表す型 ℕ 、およびそのコンストラクタ zero
と suc
が定義されています。
Data.Nat モジュールから ℕ, zero, suc
を import することで、型とコンストラクタを利用できるようになります。
open import Data.Nat public using (ℕ; zero; suc) three : ℕ three = 3 three' : ℕ three' = suc (suc (suc zero))
3
は suc (suc (suc zero))
の短縮形となります。
これ以降自然数 ℕ は、自分で定義した自然数ではなく、 Data.Nat モジュールで定義されたものを使用します。
Infix Notation
ここまでの例では、コンストラクタは前置の演算子として定義されていました。 agda では中置のコンストラクタを定義することも可能です。 もっと言えば後置や3つ以上の項を取る演算子も定義可能です。
data BinTree' : Set where x : BinTree' _+_ : BinTree' → BinTree' → BinTree' infixr 3 _+_
BinTree'
は内部ノードがラベルを持たない二分木を表す型です。
x
は葉を、 _+_
は節を表すコンストラクタです。
_+_
のアンダースコアは +
の前と後に1つずつ値をとることを表すプレースホルダです。
infixr 3 _+_
は +
が右結合で、結合の優先度が3 (高いほど優先して結合される)であることを宣言しています。
もし左結合にする場合は infixr
の代わりに infixl
を使います。
なお、これまでの例で出てきたアンダースコアを含まないコンストラクタは、前置の演算子として扱われます。
BinTree | BinTree' |
---|---|
leaf | x |
node leaf leaf | x + x |
node (node leaf leaf) leaf | (x + x) + x |
node leaf (node leaf leaf) | x + (x + x) |
node (node leaf leaf) (node leaf leaf) | (x + x) + (x + x) |
Mutually Recursive Sets
型の定義を行う前に型の宣言を先行して行うことで、相互再帰的な型を定義することができます。
data L : Set data M : Set data L where nil : L _∷_ : ℕ → M → L data M where _∷_ : Bool → L → M L₁ : L L₁ = nil R₁ : R R₁ = true ∷ L₁ L₂ : L L₂ = (suc zero) ∷ R₁
ちなみに ∷
は \::
で入力できます。
あと →
と ->
は等価です。
Exercise: 各ノードが有限個の子を持つ木を定義せよ
木自体はデータ型 Tree
で表すとします。
Tree
のコンストラクタ node
はある(部分)木の根のノードを表します。
node
は Children
データ型で表現される子の列を取ります。
一方 Children
は Tree
の要素をもつリストです。
2つのコンストラクタ nil
と _,_
を持ち、
その要素は t1 , t2 , ... , tn , nil
の形式で表されます (t1
… tn
は Tree
の要素)。
data Tree : Set data Children : Set data Tree where node : Children -> Tree data Children where nil : Children _,_ : Tree -> Children -> Children infixr 5 _,_ root : Tree root = node nil tree1 : Tree tree1 = node (node nil , node nil , nil) tree2 : Tree tree2 = node (tree1 , node nil , tree1 , nil)
Parametric Sets
Definition of List
Agda のデータ型はパラメータを取ることができます。 データ型の宣言で、データ型名の後、コロンの前にパラメータを指定できます。
data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A infixr 5 _∷_
A
および List A
は Set の要素で、 A
は List A
のパラメータです。
List A
は A
型の要素を持つリストとみなすことができます。
例えば List Bool
の要素は true ∷ []
や false ∷ false ∷ []
などのリストです。
それぞれのリストは Bool
型の値を要素としています。
Cartesian Product
data _×_ (A B : Set) : Set where _,_ : A → B → A × B infixr 4 _,_ infixr 2 _×_
A × B
は Set A
と B
の直積集合を表します。
a , b
は A × B
の要素です (a
∈ A
かつ b
∈ B
)。
例えば Bool × Bool
の要素は以下の4つになります。
true , true true , false false , true false , false
なお _×_
が2つのパラメータ A
と B
を取ることを
data _×_ (A B : Set)
の形式で宣言していますが、
data _×_ (A : Set) (B : Set)
と等価です。
Mutually recursive sets
もちろん相互再帰で定義される型もパラメータを持つことができます。
data List₁ (A B : Set) : Set data List₂ (A B : Set) : Set data List₁ (A B : Set) where [] : List₁ A B _∷_ : A → List₂ A B → List₁ A B data List₂ (A B : Set) where _∷_ : B → List₁ A B → List₂ A B
ちなみに以下のような非正規再帰型 (non-regular recursive type) でも同様に定義することができます。
data AlterList (A B : Set) : Set where [] : AlterList A B _∷_ : A → AlterList B A → AlterList A B
Exercise: List₁ ⊤ Bool
の最も小さい最初の5要素を示せ
「最も小さい」の定義は、構成する項数が最も少ないもの、と解釈。
[] true :: tt :: [] false :: tt :: [] true :: tt :: true :: tt :: [] true :: tt :: false :: tt :: []