Park the bus

(typically of an away team) play in a very defensive way.

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

zerosuc を使った自然数の表現だと、3 あたりから値がいくつなのか把握するのが難しくなってきます。 かといって毎回値に名前をつけるのも面倒です。 幸いなことに、標準ライブラリで定義されている自然数 ℕ では値を十進数で表記することができます。

標準ライブラリの Data.Nat モジュールには自然数を表す型 ℕ 、およびそのコンストラクタ zerosuc が定義されています。 Data.Nat モジュールから ℕ, zero, suc を import することで、型とコンストラクタを利用できるようになります。

open import Data.Nat public using (ℕ; zero; suc)

three : ℕ
three = 3

three' : ℕ
three' = suc (suc (suc zero))

3suc (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 はある(部分)木の根のノードを表します。 nodeChildren データ型で表現される子の列を取ります。 一方 ChildrenTree の要素をもつリストです。 2つのコンストラクタ nil_,_ を持ち、 その要素は t1 , t2 , ... , tn , nil の形式で表されます (t1tnTree の要素)。

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 の要素で、 AList A のパラメータです。 List AA 型の要素を持つリストとみなすことができます。 例えば 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 AB の直積集合を表します。 a , bA × B の要素です (aA かつ bB)。 例えば Bool × Bool の要素は以下の4つになります。

true , true
true , false
false , true
false , false

なお _×_ が2つのパラメータ AB を取ることを 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 :: []