Park the bus

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

Agda tutorial を読んでみた: Sets (1)

Agda Tutorial を読んで、自分なりにまとめたメモ。 今回は Modules から Recursive Sets まで。

Modules

すべての Agda module は以下の形式のヘッダから定義が始まります。

module Modules.Basic where
  • module と where は Agda の keyword (予約語)
  • モジュール名とファイルシステム上でのファイル名は一致させる必要があります。先の例ではファイル名を Modules/Basic.agda のようにします
  • EmacsAgda 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

f:id:htk16:20170507164212p:plain

上図の二分木は左から順に下記の項で表現されます。

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ℕ