はじめに
Agda あるいは一般に定理照明器を触るにあたって基本的な数学を"実装"してみようというのはおそらく自然な欲求だと思う、みょんさんみたいに米田の補題とかためしてみるのとかクールだと思う。
圏論をためしてみるの良いよと河野先生もおっしゃってくれてるのでいずれ挑戦しようと思ってます。
てなわけで、Agda Tutorialを上から写経していこうと思い立ったのでまずは第一弾、集合。
Modules.Basic
Agda のモジュールはmodule header が必要、とのこと。
（単なるAgda ファイルならどうなんだろう？）
Emacs にロードさせて（解釈させて）シンタックスハイライトさせるためにはC-c C-lと打ちましょう。
Sets.Enumerated
列挙ですね、外延的なのかな？
The Bool set
Haskell に似て非なるBoolean
data Bool : Set where
true : Bool
false : Bool
これは1
- Bool は Set の"要素”
- true とfalse は Bool の"要素"
なお後述（される予定）のようにRussel のパラドクス回避のために
Setᵢ : Setᵢ₊₁
のように再帰的に型が定義されます。
Special finite sets
Boolean の他に大事な有限集合として、空集合と一点集合（シングルトン）があります：
data ⊥ : Set where
data ⊤ : Set where
tt : ⊤
空集合はその名前から明らかなようにコンストラクターが不在です。
Types vs. sets
型と集合の違い
-ある要素に対して、型はユニークに決まるがその要素が属する集合は一つとは限らない
-型は要素を集めたものではない、それはどちらかと言うと集合
Sets.Recursive
再帰というとリストとか二分木とかですね。
Import List
module Sets.Recursive where
open import Sets.Enumerated using (Bool; true; false)
open import はその作用としてはBool 型の定義をこの場所に展開するのと等しいらしい。
Definition of ℕ
いわゆるペアノ数と呼ばれる再帰的な自然数の定義
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
これによって十進法で言うところの0 をzero で、1 をsuc zero で、2 をsuc (suc zero)で、というふうに表していけることになる。
Type-checking of expressions
Emacs 上でC-c C-d (deduce) と打つとAgda による型チェックを行うことが出来る。
例えば、C-c C-d と打ってからsuc (suc zero) と打つとこれはℕ だよと教えてくれるわけだ。
Binary representation of ℕ
ペアノ数はいわば一進法に相当するわけで、二進法のもある、もちろん同型であるわけだが証明が必要。
data ℕ⁺ : Set where
one : ℕ⁺
double : ℕ⁺ → ℕ⁺
double+1 : ℕ⁺ → ℕ⁺
data ℕ₂ : Set where
zero : ℕ₂
id : ℕ⁺ → ℕ₂
Binary trees
二分木の構造だけ、データは入っていない。
data BinTree : Set where
leaf : BinTree
node : BinTree → BinTree → BinTree
Constants
Import List
module Constants where
open import Sets.Enumerated using (Bool; true; false)
open import Sets.Recursive using (ℕ; zero; suc)
Constant definitions
ちょっとだけプログラミングらしくなるところ。
nine : ℕ
nine = suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))
ten : ℕ
ten = suc nine
Haskell のそれとは異なり型宣言は必須、とのこと。
一回用意したものを再利用（ten の中で使われてるnine）可能。
Normal form
C-c C-n (normal)と押してten と叩くとそれはsuc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) と教えてくれる、これをnormal form と呼ぶ、日本語だと正規形だろうか？それとも標準形？
Syntax.Decimal_Naturals
、、、要はペアノ数と普段使ってる十進法の間に組み込みの対応を用意してますよーとのこと。
Syntax.Infix
module Syntax.Infix where
open import Sets.Enumerated using (Bool; true; false)
Infix notation
_をプレースホルダーとして使うのがややややこしいかもしれない。
なお適応順はおそらく左端から。
data BinTree' : Set where
x : BinTree'
_+_ : BinTree' → BinTree' → BinTree'
この定義からは以下のような二分木型が作れます。
BinTree' : Set
x : BinTree'
x + x : BinTree'
(x + x) + x : BinTree'
x + (x + x) : BinTree'
(x + x) + (x + x) : BinTree'
右結合か左結合かを明示的に宣言できます、数値は作用素としての強さですね
infixr 3 _+_
こう宣言することで
x + x + x : BinTree'
x + (x + x) : BinTree'
の２つは同じになります、すなわち右結合。
Sets.Mutual
module Sets.Mutual where
open import Sets.Enumerated using (Bool; true; false)
open import Syntax.Decimal_Naturals using (ℕ; zero; suc)
Mutual definitions
mutual definitions のためには先にdata で（型）宣言をする必要があります：
data L : Set
data M : Set
data L where
nil : L
_∷_ : ℕ → M → L
data M where
_∷_ : Bool → L → M
Sets.Parametric
module Sets.Parametric where
open import Data.Nat
Definition of List
さてリストの定義、糖衣構文を剥がしたHaskell のそれとそっくりですね。
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
infixr 5 _∷_
A : Set の仮定の下、List A : Set となり、このときA をリストのパラメタと呼びます。
従ってList Bool 型の要素は例えば
[]
true ∷ []
false ∷ []
true ∷ true ∷ []
false ∷ true ∷ []
true ∷ false ∷ []
false ∷ false ∷ []
...
となります。
×: Cartesian Product
デカルト積です。
data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
infixr 4 _,_
infixr 2 _×_
型とそのインスタンスは少々ややこしいですが、例えば Bool × Bool 型は全部列挙できて
true , true
true , false
false , true
false , false
というわけです。
⊎: Disjoint Union (Sum)
今度は直和です。
data _⊎_ (A B : Set) : Set where
inj₁ : A → A ⊎ B
inj₂ : B → A ⊎ B
infixr 1 _⊎_
Sets.Indexed
module Sets.Indexed where
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; zero; suc)
Fin, family of finite sets
ℕ でインデックスされた集合族を考えます、つまりFin n は要素がn 個の集合です。
このとき、明らかに数が等しいので
- Fin 0 ~ ⊥
- Fin 1 ~ ⊤ ~ Maybe ⊥ ~ ⊤ ⊎ ⊥
- Fin 2 ~ Bool ~ Maybe ⊤ ~ Maybe (Maybe ⊥) ~ ⊤ ⊎ ⊤ ⊎ ⊥
- Fin 3 ~ Maybe Bool ~ Maybe (Maybe (Maybe ⊥)) ~ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊥
- Fin 4 ~ Maybe (Maybe (Maybe (Maybe ⊥))) ~ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊥
などの同型関係があります。
Definition of Fin
data Fin : ℕ → Set where
zero : (n : ℕ) → Fin (suc n)
suc : (n : ℕ) → Fin n → Fin (suc n)
Vec A n ~ Aⁿ
data Vec (A : Set) : ℕ → Set where
[] : Vec A zero
cons : (n : ℕ) → A → Vec A n → Vec A (suc n)
Term_Inference
module Term_Inference where
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat using (ℕ; zero; suc)
Term inference
アンダースコア(_) が置かれた項をAgda のコンパイラは推論してくれます。
例えばn はsuc の引数なのでℕ 型だというわけです。
data Fin′ : ℕ → Set where
zero : (n : _) → Fin′ (suc n) -- ℕ is inferred
suc : (n : _) → Fin′ n → Fin′ (suc n) -- ℕ is inferred
x : Fin′ 3
x = suc _ (zero _) -- 2 and 1 are inferred
Implicit arguments
アンダースコアは隠すこともできます、とのこと。
引数を"暗示的に”扱う際は{}を使いなさい、とのこと。
data Fin : ℕ → Set where
zero : {n : _} → Fin (suc n)
suc : {n : _} → Fin n → Fin (suc n)
このとき
x′ : Fin 3
x′ = suc {_} (zero {_})
{_} can be deleted:
とかけるそうですが、さらに{_} も消去できて
x″ : Fin 3
x″ = suc zero
となりますが、これが普通の書き方な気がするなぁ、、、
と思いましたが、この定義だとzero やsuc なども暗示的に要素数n を持っているのでいちいち書かなくても型宣言の時一回のみで良いというのが利点ですね。
Syntactic abbreviations
明示的に書く場合は以下のように書けます。
data Fin′ : ℕ → Set where
zero : (n : _) → Fin′ (suc n)
suc : (n : _) → Fin′ n → Fin′ (suc n)
data Fin′ : ℕ → Set where
zero : ∀ n → Fin′ (suc n)
suc : ∀ n → Fin′ n → Fin′ (suc n)
同様に
data Fin : ℕ → Set where
zero : {n : _} → Fin (suc n)
suc : {n : _} → Fin n → Fin (suc n)
data Fin : ℕ → Set where
zero : ∀ {n} → Fin (suc n)
suc : ∀ {n} → Fin n → Fin (suc n)
Sets.Propositions
module Sets.Propositions where
open import Data.Nat using (ℕ; zero; suc)
Proofs as data
Agda のキモである証明について。
真である命題の証明
いわゆる終対象である一点集合をもって真なる命題の証明を表します、すなわち
data ⊤ : Set where
tt : ⊤
なるほど、だからttなのか。
偽である命題の証明
こんどは始対象に相当する空集合ですね、すなわち偽なる命題は証明を持たないので
data ⊥ : Set where
論理積あるいはAND
A, B を命題としてそれらの論理積を型A × B で表す。
data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
infixr 4 _,_
infixr 2 _×_
a を命題A の証明だとする、同様にb をB の証明だとする。
このとき型A × B はa , b なる証明を持つことになる、というわけです。
論理和あるいはOR
論理積の双対ですね。
data _⊎_ (A B : Set) : Set where
inj₁ : A → A ⊎ B
inj₂ : B → A ⊎ B
infixr 1 _⊎_
すなわちA ⊎ B はinj₁ a あるいはinj₂ b という証明がありますよ、ということです。
≤: Less-or-equal predicate
n ≤ m (n, m = 0, 1, ...)なる命題の証明を考えます。
以下のようにm, n でインデックスされた集合を定義します。
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m : ℕ} → {n : ℕ} → m ≤ n → suc m ≤ suc n
infix 4 _≤_
この定義によって以下の様な命題とその証明が生成されることになります。
z≤n {0} : 0 ≤ 0
z≤n {1} : 0 ≤ 1
z≤n {2} : 0 ≤ 2
...
s≤s (z≤n {0}) : 1 ≤ 1
s≤s (z≤n {1}) : 1 ≤ 2
s≤s (z≤n {2}) : 1 ≤ 3
...
s≤s (s≤s (z≤n {0})) : 2 ≤ 2
s≤s (s≤s (z≤n {1})) : 2 ≤ 3
s≤s (s≤s (z≤n {2})) : 2 ≤ 4
...
型を整理すると
0 ≤ 0
0 ≤ 1, 1 ≤ 1
0 ≤ 2, 1 ≤ 2, 2 ≤ 2
0 ≤ 3, 1 ≤ 3, 2 ≤ 3, 3 ≤ 3
...
となり、これらの命題（型）を持つ命題はその証明を得たことになります。
1 ≤ 0
上記に載ってない1 ≤ 0 なども空集合があるという意味では正しい命題です、もちろん偽なので証明はありません。
これはAgda においては1 ≤ 0 なる型の要素はありません、と表現されます。
Proving emptiness
要は再帰を遡っていって直接空であることを示せるところまで降りたら良い、ということみたいですね。
すなわち、例えば型7 ≤ 3 を考えてみます。
これが空で無ければ、あるx : 6 ≤ 2 があって、 s≤s x : 7 ≤ 3 となります。
再帰的にこれは結局4 ≤ 0 という型まで降りてくるわけですが、これが以下のように空であることが分かるので7 ≤ 3 は偽だと証明出来るわけです。
4 ≤ 0
z≤n の定義より、0 ≤ 0, 0 ≤ 1, 0 ≤ 2, .. は存在しますが、この左辺は4 には成り得ないのでここには4 ≤ 0 は存在しません。
s≤s の定義より、z≤n で作られた0 ≤ n から始まってm ≤ (n + m) は存在しますが、やはりここには4 ≤ 0 は存在しません。
従って型4 ≤ 0 は空であることが示せました。
のちほど
上記で省略した”再帰的に”のくだりをAgda では
7≰3 : 7 ≤ 3 → ⊥
7≰3 (s≤s (s≤s (s≤s ())))
と表すことが出来るそうです。
ここで() は空集合の"値"を表しているそうです、Haskell ではユニットと呼ばれるやはり特殊な値に使われている記号ですね。
読み方としては"関数"7≰3が"入力"の型7 ≤ 3 に対して"空"()なる型⊥を返すことで、7 ≤ 3が偽であることが示される、という感じですかね。
また、一旦空集合であることが示せたら他の証明でも使えます。
8≰4 : 8 ≤ 4 → ⊥
8≰4 (s≤s x) = 7≰3 x
Alternative representation
違うやり方。
data _≤′_ : ℕ → ℕ → Set where
≤′-refl : {m : ℕ} → m ≤′ m
≤′-step : {m : ℕ} → {n : ℕ} → m ≤′ n → m ≤′ suc n
infix 4 _≤′_
これによって
≤′-refl : 0 ≤ 0
≤′-step ≤′-refl : 0 ≤ 1
≤′-step (≤′-step ≤′-refl) : 0 ≤ 2
...
≤′-refl : 1 ≤ 1
≤′-step ≤′-refl : 1 ≤ 2
≤′-step (≤′-step ≤′-refl) : 1 ≤ 3
...
≤′-refl : 2 ≤ 2
≤′-step ≤′-refl : 2 ≤ 3
≤′-step (≤′-step ≤′-refl) : 2 ≤ 4
...
が生成されます。
もちろん作り方が異なるのでm ≤ n とm ≤′ n は異なるわけですが、考える問題によってどっちが良いかが決まります。
人間の脳コンパイラはこの辺を吸収して自動的によろしい方を選択するわけですね、なんと賢い。
Syntactic abbreviations
以下のコードはすべて正しいコードとなります、どれが良い書き方なんでしょうかね？
個人的にはふたつ目のはあまり美しくない気がする、好みなのはやはり最初か最後かな。
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m : ℕ} → {n : ℕ} → m ≤ n → suc m ≤ suc n
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m : ℕ} {n : ℕ} → m ≤ n → suc m ≤ suc n
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m n : ℕ} → m ≤ n → suc m ≤ suc n
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : _} → zero ≤ n
s≤s : {m n : _} → m ≤ n → suc m ≤ suc n
data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n
_+≡: Addition predicate
m + n ≡ k の形の命題の証明を考えます。
方針としてはm + n ≡ k という型の集合を考え、それが空か否かを判定するということになります。
従って2 + 2 ≡ 5 は空集合という意味で正しくて、m + n ≡ k なる集合が空集合でない必要十分条件はn + m = k となります。
Definition of _+≡
data _+_≡_ : ℕ → ℕ → ℕ → Set where
znn : ∀ {n} → zero + n ≡ n
sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k
これは以下のコードと同値です。
data _+_≡_ : ℕ → ℕ → ℕ → Set where
znn : {n : ℕ} → zero + n ≡ n
sns : {m : ℕ} → {n : ℕ} → m + n ≡ k → suc m + n ≡ suc k
これらはsuc を使うことで一刻みに網羅する方針。
Definition reuse
さらにあるいは
data _≤″_ : ℕ → ℕ → Set where
≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k
と定義することによって任意のn について網羅することが出来ます。
Sets.Parameters_vs_Indices
open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.List using (List; []; _∷_)
Parameters vs. indices
（型とインスタンスの）引数の位置が対応していればパラメータとして書き下せるそうです、以下がもとの文章です。
The first index can be turned into a new parameter if each constructor has the same variable on the first index position (in the result type).
これは例を見たほうがわかりやすいと思います。
例１
以下の２つは”似ている”そうです。
data _≤′_ : ℕ → ℕ → Set where
≤′-refl : {m : ℕ} → m ≤′ m
≤′-step : {m : ℕ} → {n : ℕ} → m ≤′ n → m ≤′ suc n
data _≤′_ (m : ℕ) : ℕ → Set where
≤′-refl : m ≤′ m
≤′-step : {n : ℕ} → m ≤′ n → m ≤′ suc n
例２
このみっつも似ているそうです。
data _≤″_ : ℕ → ℕ → Set where
≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k
data _≤″_ (m : ℕ) : ℕ → Set where
≤+ : ∀ {n k} → m + n ≡ k → m ≤″ k
data _≤″_ (m : ℕ) (k : ℕ) : Set where
≤+ : ∀ {n} → m + n ≡ k → m ≤″ k
Design decision
まだ書き直す前の定義の方がわかりやすく感じるのですが、パラメータを使うというのは選択肢として良いらしいです。
-集合の構造について多く記載することによって、Agda コンパイラが推測できる性質が増える。
-コンストラクタの引数が減るのでわかりやすくなる。
例えばパラメータを一つ固定するだけで
data 10≤′ : ℕ → Set where
10≤′-refl : 10≤′ 10
10≤′-step : {n : ℕ} → 10≤′ n → 10≤′ suc n
という形で簡単に定義が可能になります。
General equality: ≡
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
infix 4 _≡_
集合A を暗に固定しておいて、x をパラメータとした定義ですね。
∈ proposition
data _∈_ {A : Set}(x : A) : List A → Set where
first : ∀ {xs} → x ∈ x ∷ xs
later : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs
infix 4 _∈_
これもx をパラメータとした定義ですね。
おわり
とりあえずAgda による集合の扱いに触ってみた、という段階です。
Haskell のようでHaskell でないAgda 、なかなかおもしろそうです。
カリー化された型定義と数学の作法に似た定義をそのまま書ける感じはおそらくHaskell ゆずりなんでしょう、冬休みの間にもう少し理解が進むと良いですね。
コードを書き下す際に、lang:FileName.agdaと書くとプレビューではシンタックスハイライトされずにすべてagda としたのでやや参照しづらいですね、これは投稿したら実は上手くなってたりするのだろうか、というわけで以下は実験。
data _∈_ {A : Set}(x : A) : List A → Set where
first : ∀ {xs} → x ∈ x ∷ xs
later : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs
infix 4 _∈_
-
この部分は英語の方が文法的に良く出来ていて例えば Bool is a Set. のように表現されます。 ↩