bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

解釈次第で!(1)

1.あなたは何を

この文章はキーボード上のキーを打ちながら作成している。でも、もし、ワープロのプログラムではなく、ゲームのプログラムが動いていたなら、敵の攻撃をかわすべく、シューティングに夢中になっているかも知らない。このシューティングもキーを打ち込むことには変わりはない。同じキーの打ち込みが、解釈を変えるだけで、全く別の世界を作り出してくれる。

このような仕組みをHaskellで作れないのだろうか?最近、これが現実となった。アプフェルマス(Apfelmus)が開発したオペレーショナル・モナド(Operational Monad)である。また、そのもとになっているのは操作的意味論である。
オペレーショナル・モナド(Operational Monad)の数学的な背景は圏論(Category Theory)である。Haskellそのものが、圏論(Category Theory)をベースとしているので、時間があれば、少し手ごわいが、勉強してみるとよい。手始めにその神髄の話をする。

2.赤ちゃんと大人の会話

圏論の一つ目の目的は、数学的な構造が似ているものをカテゴリーとしてまとめることである。二つ目の目的は、異なるカテゴリーの間を結びつけることである。最後の、そして、最も重要な三つめの目的は、二つのカテゴリー間での随伴性(Adjunction)である。ここまで勉強が進めば、圏論での議論はおよそ理解できるようになる。随伴性とは何かを数学の概念を使わずに次に紹介する。

圏論の世界はカテゴリーの構造とカテゴリー間の関係を述べることなので、ここでは、意味の分からない言葉を発する赤ちゃんの世界と単語にちゃんとした意味がある大人の世界との二つのカテゴリー考えることにする(圏論の若き研究者であるスピバック(Spivak)が、Category Theory for the Sciencesという本を書いたが、「赤ちゃんと大人の会話」の話はこの本の中で紹介されているはずである。この本は、正式には、この秋出版される予定なので、楽しみに待つとよい)。

赤ちゃんの世界では、音の列が生成される。これは、大人は理解することはできないが、赤ちゃんはそれなりに意味のあることを言っている。そこで、赤ちゃんが発した音の列を大人の世界に移す。大人の世界に移した音の列と大人が発する単語の列で言っていることが同じであれば、この二つの間で(大人の世界での)写像が存在することになる。

逆に、大人が発する単語の列も赤ちゃんの音の列に移せるはずである。そうすると、赤ちゃんの音の列と赤ちゃんの世界に移した大人の単語の列には、言っていることが同じであれば、この二つの間で(赤ちゃんの世界での)写像が存在することになる。

ここで出てきた二つの写像、大人の世界での写像と赤ちゃんの世界での写像は、証明するのは難しそうだが、直感的に同じと感じられる。完全に一致していなくても、番号を入れ替えれば同じになる程度のものを、圏論の世界では、自然な同型と言っている。先ほどの二つの写像が自然な同型であるとき、二つの世界は同じような構造を持っていると考えてよい。これが成り立つとき、これらの世界での現象を調べるとき、都合の良い世界に移して考えればよいということになる。とても便利な道具である。

3.米田の補題

随伴性の証明には、米田の補題が利用される。数学的な言葉を抜きにして説明すると、ある条件の下では、自然変換(写像)が集合と一対一に対応すると述べている。この性質をHaskellに応用すると、命令のセット(集合)を定めると、それらの命令の解釈(自然変換)を定めることができる。また、その逆も真であるとなる。冒頭で述べた話は、キーを命令と考え、ワープロであればこのキーに対して編集用の操作が定義され、ゲームのプログラムであればこのキーに対して物体の移動が定義されていると考えると、オペレーショナル・モナドで実現できそうな気がする。