Agda tutorial を読んでみた: Sets (1)
Agda Tutorial を読んで、自分なりにまとめたメモ。 今回は Modules から Recursive Sets まで。
Modules
すべての Agda module は以下の形式のヘッダから定義が始まります。
module Modules.Basic where
- module と where は Agda の keyword (予約語)
- モジュール名とファイルシステム上でのファイル名は一致させる必要があります。先の例ではファイル名を Modules/Basic.agda のようにします
- Emacs で Agda module を開いて agda2-load (C-c C-l) を実行すると、正しく読み込めた場合は Syntax Highlight されます
Enumerated Sets
The Bool set
data Bool : Set where true : Bool false : Bool
上記定義の意味するところは
- Bool の型は Set (任意の集合を要素に持つ集合)
- true, false は Bool の要素でそれぞれ異なる
- true, false 以外には Bool の要素は存在しない
true や false は Bool データ型のコンストラクタ(constructor) と呼ばれます。
Agda では Block 構造をインデントで表します (off-side rule)。 Bool のコンストラクタなどは data … の行よりも一段深く字下げしてから記述します。 なお、: の前後にはスペースが必要です。 Bool: Set のように省略してしまうと Bool: を1識別子として解釈してしまいます。
Isomorphisms
data Bool : Set where true : Bool false : Bool data Bool' : Set where true' : Bool' false' : Bool'
Bool と Bool' は異なるデータ型ですが、 true と true'、false と false' の間に一対一の対応関係があるので同型(isomorphic)です。
Representation and interpretation
解釈 (interpretation) と表現 (representation)は逆の関係です
- Bool は「真理値(Boolean)の集合」と解釈することができます
- 真理値の集合の一つの表現が Bool です
- 真理値の集合の Bool とは異なる表現の一つが Bool' です
Special finite sets
Agda では要素数が n = 0, 1, 2, … の集合を定義することができます。 その中で、 n = 0, 1 の場合の特別な集合に ⊥, ⊤ があります。
data ⊥ : Set where data ⊤ : Set where tt : ⊤
余談ですが ⊥ および ⊤ は input-method を Agda に設定したあと、それぞれ \bot, \top で入力できます。Adga input method で入力できる記号の一覧は こちら
Types vs. sets
型(types) と集合(sets) には次の基本的な違いがあります。
- 要素の型はユニークだが、要素は異なる集合の要素になることができる (例えば true は同時に2つの異なる型の要素にはなれない)
- 型はその要素のコレクションではないが、集合はその要素によって特徴づけられる (例えば異なる空集合が存在する)
data は型を定義するもので、集合を定義するものではありません 。
いくつかの理由から集合より型を好んで使う、とあるのですが自分は今のところその理由は理解できていません。そのうちわかるでしょう、きっと。
Recursive Sets
Definition of ℕ
data ℕ : Set where zero : ℕ suc : ℕ → ℕ
zero は 0 を、suc は自然数 n の後者(successor)を表すコンストラクタとなります。 suc : ℕ → ℕ は ℕ 型の要素をとって ℕ 型の要素を返すコンストラクタを表しています。
Agda 上の項と数値表現の対応は以下のようになります。
項 | 数値表現 |
---|---|
zero | 0 |
suc zero | 1 |
suc (suc zero) | 2 |
suc (suc (suc zero)) | 3 |
… | … |
なお、Emacs の agda2-infer-type-maybe-toplevel (C-c C-d) コマンドを使うと、与えた項の型を確認することができます。 上の表の項 zero, suc zero, … の型が ℕ であることが確認できます。
自然数には、以下のような ℕ とは別の表現を考えることもできます。
data ℕ⁺ : Set where one : ℕ⁺ double : ℕ⁺ → ℕ⁺ double+1 : ℕ⁺ → ℕ⁺ data ℕ₂ : Set where zero : ℕ₂ id : ℕ⁺ → ℕ₂
ℕ₂ でもコンストラクタ zero が定義されています。 曖昧にならない場合に限り、同じ名前のコンストラクタを複数の型で定義することができます(どういう場合に曖昧になるんですかね?)。
ℕ と ℕ₂ は同型で、以下のような対応関係があります。
ℕ | ℕ₂ |
---|---|
zero | zero |
suc zero | id one |
suc (suc zero) | id (double one) |
suc (suc (suc zero)) | id (double+1 one) |
… | … |
Rationale behind different representations
ℕ と ℕ₂ はどちらも自然数を定義する型です。 どちらか一方があれば良いようにも思えますが、使い分けることで扱う問題によっては簡潔な表現ができる場合があります。 例えばある自然数 n に対して n * 2 を計算する場合、 ℕ₂ であれば単に double コンストラクタを使うことで表現できます (実際は ℕ₂ を剥がして ℕ⁺ の値を取り出す必要はありますが)。 一方 ℕ の要素 n に対しては、何らかの手段で ℕ 上の積演算を定義する必要があります。
Binary trees
節点が値を持たない二分木は以下のように定義できます。
data BinTree : Set where leaf : BinTree node : BinTree → BinTree → BinTree
上図の二分木は左から順に下記の項で表現されます。
leaf node leaf leaf node (node leaf leaf) (node leaf leaf) node (node (node leaf leaf) leaf) leaf
また、葉のみが自然数をラベルに持つ二分木は以下のように定義できます。
data BinTreeℕ : Set where leaf : ℕ -> BinTreeℕ node : BinTreeℕ -> BinTreeℕ -> BinTreeℕ