圏をつくろう(前編) -Why do we use Coq?-

この記事は Theorem Prover Advent Calendar 2013 の 8 日目の記事です.

Packaging Mathematical Structures を参考にして 圏をつくってみた というテーマで,当初はコードを載せてダラダラと説明をする予定でしたが,ちょいと変更し,今回は前編としてその動機たる部分をほんわかと書いていこうと思います.

実際にコードを見ていくのは後日載せる予定の後編になります.

なお,記事は会話形式です.被ってしまった

目次

1 Hello, World!

「こんにちは」

「こんにちわー」

「今日は定理証明系と圏論,両方に関わる話をしていきたいと思います」

「はーい」

「具体的には,定理証明系の上で圏をつくってみよう,というお話です」

「なるほどー」

「定理証明系には幾つかありますが,今回は Coq を使って進めていきます」

「はいはーい,質問がありまーす」

「なんでしょう」

「どうして Agda とか Isabelle じゃなくて,Coq を使うんですか」

「……定理証明系の上で圏論を展開するとき,Coq には色々と便利な機能がね,いくつもあるんですよ」

「例えば何ですか」

「え,その, StructureCanonical とか……」

圏論を展開するとき どんな風に便利なんですか?」

「あ,えっと」

「Coq しか使えないからですよね」

「……」

「『今回 』なんて言ってますけど,いくつもの選択肢から Coq を選んだんじゃなくて, Coq しか使えないんですよね」

「……うぅ」

Structure とか Canonical って圏論を展開するのに便利っていうよりも,いざ作った道具を使う段になったときに,タイプ量が少なくて済むとか簡便な記述ができるとか,そういう類の利便性を提供する機能ですよね.そもそもこの2つってセットで使うコマンド群じゃないですか」

「……」

「圏論を展開する上で他の定理証明系に比べて Coq にはアドバンテージがある,とかではなく, Coq しか使えないから Coq を使う,ということですよね」

「……はい」

「そういう線引きはしっかりしたほうがいいですよ」

「はい……」

「それじゃぁ本題に行きましょうかー.お願いしまーす」

「……(先行きが暗い)……あ,Coq の説明は割愛します」

Theorem Prover Advent Calendar 2013 なのにですか」

「……割愛します」

Theorem Prover Advent Calendar 2013 なのにですか

「ごめんなさい時間ありませんCoqの説明慣れてないので終わりません」

「わかりました.まるで慣れていないだけでやろうと思えばできるような口ぶりが気になるけど.でも,それで全く説明なしに話が進んでも目的が見えないんで,軽くでいいんで定理証明系の上で圏をつくろうと思った動機みたいなものを話してもらえますか」

「……はい」

「どうぞ」

2 Hello, Formal World!

圏に限らず色んな代数構造に言えることですが,そういった数学的対象の構成要素には,台集合や演算のような 実体をもつ何か だけではなく,それらが満たすべき性質,あるいは 性質を満たしているという事実 も含まれます.

「『群の公理』とか『モナド則』とか呼ばれてるやつのことですね」

はい.そしてそいった数学的対象を利用したいときは,そういった性質が重要である場合がほとんどです.モナドを使う場合は特にそうですね.モナド則が成り立つという前提の下だからこそ,様々な計算効果を純粋な文脈のもとで便利に扱えるわけです.

Haskell ですね.Haskell はそんな風に数学的な性質を利用する傾向が強い言語ってイメージです」

モナド自体はプログラミング言語を限定するものではないですけど,えぇ,確かに,モナドといったらまずは Haskell が思い浮かぶ方が多いと思います.型クラスのおかげでモナド自体も扱い易い環境が整っていますし.

「そういえば Coq にも型クラスがありますね」

えぇ, Haskell の型クラスとは違って,既存の機能を使って提供されています.挙動も少し違うので, Coq の型クラスに慣れてから Haskell の型クラスに触れると戸惑うことがあるかもしれません.

「そういう人はあんまりいないんじゃないかなぁと思いますけど」

どうでしょうね.さて,せっかくですから Haskell の Monad を例に取ってみましょう.

class Monad m where
  (>>=)  :: m a -> (a -> m b) -> m b
  return :: a -> m a

これが Haskell に於ける Monad の定義です.

「定義だけ見せられても何が何だかって感じです」

そうでしょうね.でも今はその中身にはあまり踏み込む必要はありませんので,このコードからは次の事実を読み取ってもらえれば大丈夫です.

  1. Monad という構造は,型変換子 m によってパラメタライズされている
  2. その構造には >>=return という 2 つの関数が含まれている
  3. 即ち, Monad という構造は,型変換子 m, 関数 >>=, 関数 return という 3 つの要素から構成されている

「この Monadどういった意味を持つものか はさておき,その形に目を向けてみましょう,ということですか」

えぇ,そういうことです.より正確には Monad はある種の構造の雛形のようなもので,その実体は改めて与える必要があります.インスタンスと呼ばれているものです.型クラスは,そのインスタンス全てに対して共通のインタフェースを与える機能と考えることも出来ます.

さて, Haskell に於けるこの Monad ですが,実は,ある性質が満たされることが期待されています.それらはときに『モナド則』と呼ばれることもある 3 つの等式です.

1. (return x) >>= f == f x
2. m >>= return == m
3. m >>= f >>= g == m >>= (\x -> f x >>= g)

今は,この等式についてもどんな意味を持つのかどうかを気にせずにいて構いません. Monad には 満たすべき性質が 3 つある ということが重要なのです.

「と言われても,意味がわからないとなんだかもやもやするんですけど」

どうしましょうか.等式の意味を説明するためには先ほど省いた >>=return の説明もしなければならなくなってしまうんですよね……

「雰囲気だけでも教えてもらえませんかー」

そうですね……しっかり伝わりきるか自身はないですが,軽く説明しておきましょう.

特に Haskell のような純粋関数型言語という副作用の存在しない世界では, Monad は様々な計算効果を明示的に扱うために使われます. 計算効果とは,計算の失敗や状態,I/O などのことを指します. 関数 f: A -> BA 型のデータから B 型のデータを計算するものであるとするなら, 計算に付随して発生する何か をモナド T で表すことにすると,その計算全体を f: A -> T B と表現することができるんです. そして,計算効果の種類が一つでも,複数の計算を行えば計算効果は複数発生します.さらにそういった場合,計算には順番があり,その順番にしたがって計算効果が発生します. このとき,連なる計算効果を纏めることができるというのがモナドの特徴なのですが,モナド則はこの性質の成立を保証しているものなんです.

「最後,韻を踏んでましたね」

知りません.えっと,こんな感じでいいですか.

「まくしたてられた感はあるけど,進行の問題もあるし,うん,おっけー」

……はい.では進めましょう.

さて, Monad にはモナド則が成り立つことが 期待されている と言いました.これがどういう意味かわかりますか.

「んー,期待されているってことは Monad だったとしても,常にモナド則が成り立っているとは限らないってことかなー」

そういうことです. Monad のインスタンスを作るとき,モナド則が成り立つことは,作る人が保証しなければいけないことであって,インスタンスを作れたからといってモナド則が満たされていることが自動的に保証されることはない,ということです.

「じゃぁそのさっき言ってた計算効果を纏められるっていう特徴が,もしかしたら無いかもしれない Monad があるってことでいいんですか」

厳密に言えばそうなりますね.もっとも, Haskell で使われているモナドの大半はモナド則が成り立つことが保証されています.

「どうやってですか」

実際に証明をして,です.各 Monad のインスタンスの定義を見て,モナド則の 3 つの等式が成り立つことを証明すればいいんです.むしろ,モナド則が成り立つことが証明されたからこそ,大手を振るってそのインスタンスが使われるようになったと考えた方が自然ですけれど.

「証明かー」

はい,証明です.

「なんとなく話の展開が見えてきましたー.この話だいぶ長くなってきたので巻きで行きましょー」

(……進行役は私じゃないのか……)

「どうかしましたか」

いえ.確かに長くなってきましたから,テンポよく進めましょうか.

Monad を使うと,純粋な文脈のもとで計算効果を明示的に扱えるようになります.そのためにはモナド則と呼ばれる 3 つの等式が成り立つことが不可欠でした.そしてモナド則の成立を保証するのは Monad のインスタンスを作る人であり, Monad のインスタンスが作られたからといって自動的に保証されるものではありません.

実はここ,少し危うい瞬間がありますよね.

「モナド則が成り立つからこそ Monad なのに,成り立つかどうかわからないまま Monad のインスタンスとしてしまえるってところですか」

そうです.最初の方にお話したように,本来であれば Monad とは,型変換子 m, 関数 >>=, 関数 return だけではなく モナド則が成り立つという事実 も含めて構成されるべきものです. Monad を使うときはモナド則が成り立つという事実を使う場合がほとんどなわけですから,これは自然な話です.

「それなんですけど,例えば論文か何かでモナド則が成り立つぞーって証明されたものを実際に Monad のインスタンスにした場合は,その瞬間って存在しないですよね」

そうとも限りません.例えば,モナド則が成り立つことがわかったある対象を Haskell のコードへと変換する際,それが意味を変えていないかどうかは注意が必要ですよね.

「証明を与えたそれと,Haskell のコードにしたこれが本当に同じかどうか,注意が要るよ,と」

えぇ.とはいえ実際にはあまり気にしなくても良いことかもしれません.元々はある挙動をさせたくて Haskell のコードを記述,つまりプログラムを書いているんですから,その挙動に注意を向けていれば変換で意味を変えてしまうという事態はそうそう起こらないと思います.証明を与えられる程度に理解を深めているのであれば尚更です.

「そんなもんなんですかねー」

ですが,それらの道具を使って記述されたプログラムについて様々な性質を証明したいと思った時には,少し話が変わってきます.

「様々な性質というと,停止性とか計算量とかですか」

そうですね.あとは計算結果の細かな仕様の検証とか,えぇ,本当に色々と考えられると思います.そういった時,証明の対象となるのはそこに書かれているコードそのものになります.ですから,先ほど言った変換の際の意味の変化にはより注意が必要になってくるんです.

「なんか,重箱の隅をつつきまくってる感じだなー.やたらと細かいことを気にしてませんか」

その細かいことを気にしないと,しっかりとした証明が与えられないんです.細かい部分を無視したら,それはもはや証明ではないですし.

「証明するっていうのがそもそもオーバーな要求だったりするんじゃないのかなー」

……話を根からひっくり返しかねないことはあまり言わないでください.それに,案外そうでもないですよ.例えばモナド則がそうですけど,使う側からすれば, Monad のインスタンスについてはモナド則が成り立っていて当然なわけです.そして仮に細かい話になってきたとしても,モナド則が成り立つと信じていますから,使うことを躊躇う理由はありませんよね.でも,もしそのインスタンスを作った人が細かい部分を避けて通っていたとしたら,さて,何が起こるでしょうね.

「案外なんとかなるんじゃないかなー.証明はしていなかったけど,実は成り立つので問題なかったーとか」

えぇ,その可能性は大いにあります.でも,それを保証するものはどこにもないんです.それが 1 つ 2 つであれば大きな問題になることはないでしょうけれど,そういった塵が積もって山となったら,ちょっとその山には近づきたくないですよね.

「なんだか感覚に訴える感が強くなってきてるけど,なんとなくはわかります」

こういった細かな問題を解決するには,プログラムを書いたらその環境の上で証明をしてしまえばいい,つまり,定理証明系を使ってプログラムを書き,証明をすればいいのです. Coq では証明の対象となるのは Coq 上で記述されたプログラムですから,先ほどの要求は満たせます.

「数学的対象をコードへ変換する際の変化を気にするなら,そもそもその数学的対象をコーディングしてしまえばいい,ということですか」

そういうことです.そして,例えば Monad は圏論に於けるモナドに由来する構造です.正確には Kleisli triple と呼ばれる構造ですが,そこは気にしないでおきましょう.重要なのは次の事実です.

  1. Monad を使って プログラムが記述できる こと
  2. Monad圏論を下敷きにした概念である こと

「そして Monad を使って記述されたプログラムを定理証明系で扱うためには……」

はい.まずは定理証明系で Monad を定義する必要がありますね. さて,このときモナド則はどう扱われると思いますか.

「 Curry-Howard 対応に則れば,直接 Monad の構成要素としてに モナド則が成り立つという事実を組み込むことができる んですね」

はい.すると Monad のインスタンスを構成するにはモナド則が成り立つという事実も必要となります.つまり,証明を行う必要があるわけです.

「さっき言ってた危うい瞬間が,これでなくなるってことかー」

はい.そして Monad は圏論を下敷きにした概念でした. 時折『モナドは自己函手の圏に於けるモノイド対象』というフレーズを耳にしますね.となると Monad を定理証明系で定義するためには,先立って必要になるものがありますね.自己函手とかモノイド対象とか,そういう言葉が並んではいますけれど,まずはなにより……

圏を定義しなければいけない ってことですねー」

えぇ,そういうことです.モナドによって計算効果が扱えるようになりました,これは Coq に於いてもそうです.すると,モナドを用いて記述されたプログラムというものが証明の対象となっていきます.モナドが絡む以上,証明をするにはモナド則が重要な位置を占めることは想像に難くないと思います.ですが,そもそもモナドは圏論的な概念であり,モナドを構成する各要素もそれぞれが色んな性質を持っています.函手や自然変換といったもの達ですね.これらが持つ性質あってこそのモナドですから,厳密に扱うためには当然,函手や自然変換も定理証明系の上で定義しなければなりません.そうやって突き詰めていくと,結果として 定理証明系の上で圏論を展開する という話になるのです.

「圏論を展開するその第一歩が」

はい.圏を定義することです.

3 To be conituned

「というわけで,長くなってしまいましたので今回はここまでにしたいと思います.圏をつくっていく話は,また別の日にすることにしましょう」

「Coq よりも Haskell の方が出番多かったねー」

「……次回はちゃんと Coq がメインですよ」

「Coqの上で圏を定義する話ですから,そうじゃないと困っちゃいますねー」

「少しだけ中身を予告しておきますと, SSReflect, というか Packaging Mathematical Structures を参考にして圏をつくっていこう,というお話です」

「その論文読み切れてないんじゃなかったっけ」

「次回の話をする分には大丈夫です」

「へー」

「……たぶん」

つづく

日付: 2013-12-08T15:57+0900

著者: mathink

Validate XHTML 1.0