2017-07-17

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

Agda

今回は 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 :: []

2017-05-07

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

Agda

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

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ℕ

2017-04-23

Ubuntu 16.04 に Agda をインストールする

Agda Emacs Ubuntu

Ubuntu 16.04 に Agda をインストールする

Ubuntu 16.04 上に Agda と推奨開発環境の Emacs をインストールします。なお Emacs の設定を簡単に済ませるために Spacemacs を使用します。 Spacemacs を使用しない場合は Agda 2 Readme にしたがって Emacs の設定を行ってください。

The Haskell tool stack

公式ドキュメントの手順にしたがって stack をインストールします。

$ curl -sSL https://get.haskellstack.org/ | sh
$ stack update
$ stack setup
$ stack install ghc-mod
$ stack install apply-refact hlint stylish-haskell hoogle

Agda

stack を使って、Adga 本体と必要なライブラリをインストールします。

$ sudo apt-get install libtinfo-dev
$ stack install Agda
$ stack install alex happy cpphs

2017/03/01 の時点では Agda version 2.5.2 がインストールされました。

agda-stdlib

標準ライブラリである agda-stdlib は自前でインストールする必要があります。ダウンロードページから version 0.13 (agda-stdlib-0.13.tar.gz) をダウンロードして、以下の手順でインストールします。

$ cd ~
$ mkdir -p .agda/lib
$ cd ~/.agda/lib
$ mv ~/Downloads/agda-stdlib-0.13.tar.gz .
$ tar zxfv ~/Downloads/agda-stdlib-0.13.tar.gz
$ echo "$HOME/.agda/lib/agda-stdlib-0.13/standard-library.agda-lib" > ~/.agda/libraries

Emacs & Spacemacs

$ sudo apt-get install emacs
$ git clone https://github.com/syl20bnr/spacemacs ~/.emacs.d

前述の設定を行ったあとに Emacs を起動すると、 Spacemacs の初期設定が行われます。まず最初に、キーバインドを Emacs 本来のものにするか、 Vim like にするか確認されるので、お好みに応じて選択してください。それ以降の質問に対しては初期選択されている項目を選択しておけば問題ないです。

Agda layer

Spacemacs では Emacs Lisp パッケージ群とその設定が configuration layer という単位でまとめられています。 Agda layer が用意されているので、これを利用します。 Agda layer を有効にするために、~/.spacemacs の dotspacemacs/layers で定義されている dotspacemacs-configuration-layers へ agda を追加します。

(defun dotspacemacs/layers ()
  (setq-default
   dotspacemacs-configuration-layers
   '(
     agda   ;; 追加
     ...
     )
   ))

設定後 Emacs を再起動すると、 Adga layer に関連するパッケージがインストールされます。 Layer 設定の詳細は Spacemacs Documentation を参照してください。

Park the bus

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

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

Constant Definitions

Decimal Notation for Natural Numbers

Infix Notation

Mutually Recursive Sets

Exercise: 各ノードが有限個の子を持つ木を定義せよ

Parametric Sets

Definition of List

Cartesian Product

Mutually recursive sets

Exercise: `List₁ ⊤ Bool` の最も小さい最初の5要素を示せ

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

Modules

Enumerated Sets

The Bool set

Isomorphisms

Representation and interpretation

Special finite sets

Types vs. sets

Recursive Sets

Definition of ℕ

Rationale behind different representations

Binary trees

Ubuntu 16.04 に Agda をインストールする

Ubuntu 16.04 に Agda をインストールする

The Haskell tool stack

Agda

agda-stdlib

Emacs & Spacemacs

Agda layer

Constant Definitions

Decimal Notation for Natural Numbers

Infix Notation

Mutually Recursive Sets

Exercise: 各ノードが有限個の子を持つ木を定義せよ

Parametric Sets

Definition of List

Cartesian Product

Mutually recursive sets

Exercise: List₁ ⊤ Bool の最も小さい最初の5要素を示せ

Modules

Enumerated Sets

The Bool set

Isomorphisms

Representation and interpretation

Special finite sets

Types vs. sets

Recursive Sets

Definition of ℕ

Rationale behind different representations

Binary trees

Ubuntu 16.04 に Agda をインストールする

The Haskell tool stack

Agda

agda-stdlib

Emacs & Spacemacs

Agda layer

Exercise: `List₁ ⊤ Bool` の最も小さい最初の5要素を示せ