Agda での Programming 技術
Menu Menu
なんで、今、証明支援系なのか?
証明支援系の歴史は古い ( HOL, Coq, Agda も新しくない )Haskell が流行ってるようだが…
Haskell はMonad使いまくり
Monadって何?
この発表は...
Agdaをさんざん触って面白かった
1部 Monad って何? 2部 Agda って何?
Monadって何?
Monad を解説しているサイトは多いが、多くは皮相的
元は圏論の概念
→ だったら、Monad を証明支援系を使って理解すれば良いんじゃないの?
とりあえず、目標は Monad の合成則の証明
圏
Category とは、集合であるオブジェクト A と、オブジェクト間の写像である射 f の組。
id(A) とは、A の要素を同じ要素に写像する射で必ず存在する
f: A->B, g: B->C に対して、射の合成がある。
g ○ f : A->C
合成則
h ○ (g ○ f ) = (h ○ g) ○ f )
A->A への単位射がある。同じ値を同じ値に返す射。
id_a : A->A
これだけ。(あとは、Functor, Natural Transformation, Adjunction, Monad ... )
射と合成則
圏と関数型プログラミングとの関係
射が関数 ( = 関数型プログラミングのプログラム)対象が型 ( 射は、型→型の写像)
これだけ。(あとは、Functor, Natural Transformation, Adjunction, Monad ... )
圏としての型
例えば Integer は、Integer から Integer への関数がある。これを射と考える。関数の合成則は成立しているし、単射もある。
型は圏でもある。
Int → List
Functor
Functor F とは、Category C から D への射
Cの対象aをDの対象a'に対応させる写像をFObjとする。Cの射fをDの射f'に対応させる写像をFMapとする。
射の対応が、以下を満たす時に、F はFunctor と言う。
(1) C の射 f:a->b を Dの射 F(f):F(a)->F(b) に割り当てる (FMap)
(2) id(F(a)) = F(id(a))
(3) f: a->b, g: b->c に対して、
F(g) ○ F(f) : F(g○f) 分配法則
Functor は対象の写像FObjと、射の写像FMapの二つを持つ。
Functor の数学記法は polymorphic
Constructor としての Functor
Integer と List はどちらも圏であり、Integer から List を作る Constructor は、Category から Category への Functor に相当する。つまり、Haskell の data はFunctor になる。
data List a = (::) a (List a)
| []
data Nodes a = Node (Nodes a) (Nodes a)
| Leaf a
List や Node を Functor のFObj(対象の射)として考えることができる。(Leaf や :: は constructor )
FMap
Functor の射の写像は、fmap として(自分で)定義する。
class Functor f where
fmap :: (a->b) -> f a -> f b
fmap f (Leaf a ) = Leaf (f a)
fmap f (Node a b ) = Node (fmap f a) (fmap f b)
fmap は要素の関数 g: a->b を List や Node の関数へ変換している。この時、f は List や Node の要素を操作する関数。
T(f)
T ------------> T
は T の要素に f を作用させると考えて良い。
Natural Transformation (自然変換)
Node から List への変換を考える。これは、Functor から Functor への射になる。例えば、flatten ( 木を深さ順にリストにする) は、そういう射の例である。
Node の要素をIntegerからStringに変換するには show が使える。( show 1 = '1' )
ここで、
flattern ( List.fmap show aNode ) = Node.fmap show ( flattern aNode )これを可換(commute)という。可換なFunctorからFunctorへの射をNatural Transformation とう。
Natural Transformation
Functor で可換を書くと、
ここで、F,G は、データ型。F(a)/F(b)) は FObj 。F(f) / G(f) は FMap。
t は自然変換(引数は要素の型)
Monad
Monad とは、Functor T と二つの自然変換η,μの三つ組 (T,η,μ) で、以下の性質を満たすものである。
T: A -> A T は AからAへのFunctor
η: 1_A -> T ηは、a から T a への自然変換
μ: T^2 -> T μは T T a から T a への自然変換
さらに、Unity Law と呼ばる
μ○Tη = 1_T = μ○ηTと、Association Law と呼ばれる以下の可換図を満たす。
Kleisli 圏
上の Monad で、 a から T b への射を 新しい Kleisli 圏の射と考える。この射の合成を、
f : b -> T(c) g : c -> T(d) g * f = μ(d)T(g)fとして定義する。
Monad の合成則 (g * f ) * h = g * ( f * h ) が成立する。
Haskell での Monad
T はFunctorだからデータ型。メタデータだと思って良い。計算の詳細に関するメタなデータと、元のデータを含むデータ型。Haskell Monad はメタデータを追加して返す関数。 Reflection に相当する。
例えば、IO Monad は、入出力するデータをメタデータとして返す。
Monad の合成
メタデータの変化は自然変換 μ で決まる。
合成則の証明は煩雑
Haskell 使うのに圏論とか必要なのか?
知らなくても困らないMonad とか用語は理解できる
Functor と map はわかる
煩雑な証明を自分でやって理解する
そもそも証明自体が圏論( Curry Howard 対応)
Curry Howard 対応な証明支援系である Agda を使えば?
(これで1部終わり。長かった...)
Curry Howard 対応
証明とλ計算式が対応する。対応は、扱う論理に寄って異なる論理が複雑になる分、λ計算を拡張する必要がある
→ ラムダ計算の拡張の指針になる
証明する論理式は型に対応する
証明するべき式の型になるλ式を作れれば証明されたことになる
Agda とは何か
Haskell実装、Haskellに似た構文
indent による scope の生成型と値
: で型を定義 = で値を定義集合
すべての値は集合
集合のレベル
集合の集合はレベルが上がる
暗黙の引数
{} で省略可能な引数を作れる
λ
module proposition where
postulate A : Set
postulate B : Set
集合であるA,Bを命題変数として使う。
Lemma1 : Set
Lemma1 = A -> ( A -> B ) -> B
これが証明すべき命題論理式になる。実際には式に対応する型。
lemma1 : Lemma1
として、この型を持つ lambda 式を使えば証明したことになる。以下のどれもが証明となり得る。
-- lemma1 a a-b = a-b a
-- lemma1 = \a a-b -> a-b a
-- lemma1 = \a b -> b a
-- lemma1 a b = b a
data
Haskell の data と同じ。
infixr 40 _::_
data List (A : Set ) : Set where
[] : List A
_::_ : A → List A → List A
論理式の排他的論理和を表すのにも使える。
data _∨_ (A B : Set) : Set where
or1 : A -> A ∨ B
or2 : B -> A ∨ B
or1 と or2 が Constructor である。
Lemma6 : Set
Lemma6 = B -> ( A ∨ B )
lemma6 : Lemma6
lemma6 = \b -> or2 b
これは、∨ の導入になっている。削除は、
lemma7: ( A ∨ B ) -> A
lemma7 = ?
equality
さらに、data は等式を表すのにも使う。
data _==_ {A : Set } : List A → List A → Set where
reflection : {x : List A} → x == x
直観主義論理には命題自体に真偽はない。なので、返すのは Set になっている。なので、二重否定は自明には成立しない。
record
record は、論理積を作るのに使う。
record _∧_ (A B : Set) : Set where
field
and1 : A
and2 : B
∧の導入
lemma2 : A → B → A ∧ B
lemma2 a b = record { and1 = a ; and2 = b }
∧の削除 ( open _∧_ が必要 )
lemma3 : A ∧ B → A
lemma3 a = and1 a
record は、ある性質を満たす数学的構造を表すのに使う。
Append の例
postulate A : Set
postulate a : A
postulate b : A
postulate c : A
infixr 40 _::_
data List (A : Set ) : Set where
[] : List A
_::_ : A → List A → List A
infixl 30 _++_
_++_ : {A : Set } → List A → List A → List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
Append の実行
Agda の実行は正規化
Haskell と同じ
l1 = a :: []
l2 = a :: b :: a :: c :: []
l3 = l1 ++ l2
Append の結合則の証明
証明するべき式
list-assoc : {A : Set } → ( xs ys zs : List A ) →
( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
List の持つ性質を表す式
data _==_ {A : Set } : List A → List A → Set where
reflection : {x : List A} → x == x
cong1 : {A : Set } { B : Set } →
( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y
eq-cons : {A : Set } {x y : List A} ( a : A ) → x == y → ( a :: x ) == ( a :: y )
Agda での証明手順
(1) 証明するべき式を型として記述する
(2) 値を = ? と取り敢えず書く
(3) ? をλ式で埋めていく
(4) C-N で正しいかどうかをチェックする
赤 ... 型エラー
黄色 ... 具象化が足りない
停止性を満たさなない
(5) data は patern match で場合分けする
(6) 必要なら式変形を使う
Haskell と Agda の違い
Haskell で結合則を証明できる?Haskell は型に関数やデータ型の constructor を書けない
Haskell のプログラムは Agda のプログラムになる?
float とかはない integer は、succesor で書く必要がある
式変形
λ式では、人間に読める証明にならない
++-assoc A (x :: xs) ys zs = let open ==-Reasoning A in
begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
((x :: xs) ++ ys) ++ zs
==⟨ reflection ⟩
(x :: (xs ++ ys)) ++ zs
==⟨ reflection ⟩
x :: ((xs ++ ys) ++ zs)
==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
x :: (xs ++ (ys ++ zs))
==⟨ reflection ⟩
(x :: xs) ++ (ys ++ zs)
∎
いくつかの技術
等号
?
Unicode の記号
module
暗黙の引数が多すぎる
Agda で証明できないこと
a ≡ b は証明できないfunctional extensionarty
-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
(∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
実際には、
postulate extensionality : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
→ Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
部分集合
異なる集合の要素は異なるので、部分集合を作れない
→ x ∈ P を自分で定義する
合同性 x ≡ y ならば f x ≡ f y 。これは、_≡_ に付いてしか言えない。Relation などで定義すると、合同性は自分で仮定あるいは証明する必要がある。
直観主義論理の限界
あんまり良くわかりません
圏論の定理の証明
Monad の結合性 Monad から作る Kleisli 圏 Kleisli 圏から作る随伴関手 随伴関手での Limit の保存 米田のレンマ
本の証明とAgdaの証明
本の証明は、山登りの道標しか示さない
Agdaの証明は、全部繋がっている
Agda の証明は式なので対称性が目で見える
定理を理解することと証明を理解すること
定理を理解するということは使い方を理解すること
定理は証明のショートカットでもある
証明を理解しても使いこなせない
結局、Monad は役に立つのか?
メタプログラミング(IOや並列処理)として便利構文やややうざい。C のプログラミングみたい。
結合則や Functor(fmapを持つ) は必須ではない
Monad の合成はさらに煩雑 (Beck Law)
Monad Transform も「一度Monadを分解して再合成」
圏論知らなくても使えるが、勉強すれば用語は納得できる
結局、証明 は役に立つのか?
Monad に関しては役に立たない圏論を理解するのは役に立つ
教科書は「道標のみ」
自分で山を登らないと。山を登るためのツール。
Agda は面白い
詰将棋みたいなもの学会でノートPCで内職しているのは Coq
Agda は Coq よりもマイナー
Agda の情報が少ないので面白い
みんな Agda を使おう!
おまけ
Agda は Emacs で使うものVimmer にはつらすぎる (手がつる)
vim emulator を使うと幸せになれます