人間と証明とプログラム: 『コンピュータは数学者になれるのか？』を読んだ

ウィッシュリストに入れていたのを知人に頂いた。数学基礎論とコンピュータ科学をつなぐ啓蒙書、という立ち位置の本なのだけど、自分はコンピュータ科学のバックグラウンドとしての数学基礎論、というとらえ方で読んでいった。専門的な概念とか簡単な証明とかはバンバン出てくるので基礎を抑えておかないと読むのには難儀しそう。以下、おもしろかった部分を整理がてらかいつまんで説明してみる。あまり丁寧ではないけど、間違っていたら教えてください。

書名にもある「数学者」とは真理を追い求める人のことで、ひいては与えられた命題に対する定理を証明するものである、と最初に位置づけられる。なので人間の証明能力をどのようにして・どこまで機械化できるのか、というところからこの本の話は始まる。

形式系

第1章は数学的な準備の章。まず、証明のための言語と推論規則からなる形式系を定める。自然数について語れるよう定義された形式系 が、本書の出発点となる仮想の数学者になる。形式系は拡大していくことができ、 に一部の文に対する数学的帰納法の能力を与えてより高度な 、さらにすべての文に解放して （ペアノ算術） ……と、能力や表現力を高めながら形式系を積み上げていくことができる。また、形式系の推論規則を組み合わせて論理式の証明図を書きあげられるとき、形式系は論理式を証明できる、という。

ゲーデルの不完全性定理とゲンツェンの無矛盾性証明

続く第2章から第5章まではそれぞれ、数学基礎論の否定的・肯定的結果、コンピュータ科学の否定的・肯定的結果の章になっている。数学基礎論の否定的結果といえば、無矛盾な形式系がそれ自身の無矛盾性を証明できない*1というゲーデルの（第二）不完全性定理。2章はこの結果に向かってほぼ一本道に突き進んでいく。ちなみに「はじめに」を読み直していたら、とあるメタ的な理由により、本書第1、2章は中高生程度の数学知識を持つ読者を対象にしています。とあって、はてどういうことだろう、と思ったことを思いだした。種明かしはちゃんとしてあった（忘れてたけど）。

というのが数学基礎論における「できない」だったわけだけど、逆に「できる」は何なのか、という話が第3章で続く。ここではゲンツェンの無矛盾性証明が紹介されている。ゲンツェンは にちょうど という順序数についての超限帰納法を加えると、 の無矛盾性を証明できることを示した。ゲーデルの結果に対し、具体的にどんな能力を与えたら無矛盾性を証明できるようになるのか？ を明らかにしているわけだ。

対角線論法

本書を貫く重要なワードのひとつが対角線論法。自然数の集合と実数の集合の濃度を分離するのに登場したあと、これが何度も、いろいろな場所で登場する。自己言及の匂いのあるとき対角線論法が現れるという感じか。実際強力な道具であることを見せつけられるが、後半第4章でこれまた有名な P 対 NP 問題が登場したときには力を発揮できない。 であることが知られている問題のクラスの関係において、 と は対角線論法によって分離できるが、肝心の と に関してはうまくいかない。対角線論法は量的な違いに対しては効くが、質的な違いに対しては有効でなく、それ以外にも P 対 NP 問題へのアタックはこれまでの数学基礎論の方法を応用してさまざまに試みられるが、どうも上手くいかない、という話で、これが面白い。

論理式の不動点

2.2 節で論理式の不動点を見つける過程でも対角線論法が使えるという話が出てきたけど、図式的にどういう対角線になるのか分からなかったので厳密さはともかく自分で書いてみた。

1変数論理式 に対して、操作 の不動点を見つけたい。ゲーデル数 を持つ1変数論理式を とおき、表の縦と横に並べる。表の中で行 と 列 が出会うところには、 を埋める。対角線の各要素に対して を適用し、 を得る。ここである行 が存在し、 が成立するはずである。このとき行 k と対角線の交わるところに注目すると であり、 は の不動点になっている。

			…
	︙
︙	︙	︙	⋱
			…

ラムダ式の不動点

同じように定理 5.1 のラムダ式の不動点も図式的に発見できる。ラムダ式 の不動点を発見したいのだとする。すべてのラムダ式に番号をふって（ゲーデル化とかでできると思う） とし、表の縦と横に並べる。表の中で行 と列 が出会うところは とおく。対角線の各要素に を適用し、 を得る。ここである行 が存在し、 が成立するはずである。このとき、この行と対角線が交わるところに注目すると であり、 が の不動点になっている。これは とβ同値。なるほど自分で書いてみるとこの謎の形の式も理解できるような気になる……。

			…
	︙
︙	︙	︙	⋱
			…

構成的証明

もう一つおもしろかったのが、構成的な証明と非構成的な証明の話。構成的な証明というのは具体的に証拠を提示する手続きになっていて、背理法はこの証拠を提示できないから構成的な証明には含まれない。これまで扱ってきたペアノ算術などは推論規則に背理法を許す古典論理にもとづいているが、これを除いた直観主義論理という論理体系もある。直観主義論理における証明は構成的であり、その証明図のひとつひとつのステップはラムダ項を構築したりバラしたりする操作とぴったり対応する。そしてこのことから、論理式を型と、その証明をプログラムと対応づけることのできるというカリー・ハワード対応が導かれる。

では構成的な証明だけがプログラムに対応するのか？ というとそんなことはなくて、面白いことに論理における背理法が（Scheme で言うところの）call/cc に対応することから、カリー・ハワード対応は古典論理にも拡張できる。また、古典論理における証明を直観主義論理における証明に翻訳する方法と、call/cc を含む関数型プログラムを CPS 変換によって純粋関数型プログラムに変換する方法とが対応する！ これは10年くらい前にウェブで見て面白かったやつ（Curry-Howard Isomorphism - d.y.d.）だなー。と思って調べてみたら本当に10年前だった。

感想

見知ったワードが幾つか出てくるけど、それぞれお話程度の理解しかなかったので、その関係も含めてもう一歩踏み込んだ数学的詳細を追うことができてよかった。面白かった大きなトピックを拾ってここには書いてみたけれど、本の中での議論はとうぜんもっと詳細だし他の話もいろいろ出てくるので、興味を持ったらちゃんと読むといいと思います。

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-

その他の資料

• 直観主義論理への招待 著者による数学基礎論サマースクール講義資料
• 計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座) ラムダ計算について詳しく。領域理論の話もあったけどよく分かってなかった……
• 情報科学における論理 (情報数学セミナー) sequent 計算という自然演繹とはまた違った形式系を主にしている

*1:もちろん本ではもっとちゃんと述べてある

Router::Simple::Reversible という Perl モジュールを書いた

https://metacpan.org/pod/Router::Simple::Reversible

だいぶ昔に書いていたのを shipit しました。tokuhirom さんの Router::Simple に、いわゆるリバースルーティングを足しただけのモジュール。Router::Simple を継承しているので、bless しなおすなりして使えばよいかと思います。

新しく生えるメソッド $router->path_for に $router->match で返ってくるような hashref を渡すと、いい感じにルーティングのルールが具体化されたかたちで文字列が返ってくるシンプルな API です。テスト を見るとだいたい使い方がわかります:

my $router = Router::Simple::Reversible->new;

# from Router::Simple's pod
$router->connect('/', {controller => 'Root', action => 'show'});
$router->connect('/blog/{year}/{month}', {controller => 'Blog', action => 'monthly'});
$router->connect('/wiki/:page', { controller => 'WikiPage', action => 'show' } );
$router->connect('/download/*.*', { controller => 'Download', action => 'file' } );

is $router->path_for({ controller => 'Root', action => 'show' }),
   '/';

is $router->path_for({ controller => 'Blog', action => 'monthly' }, { year => 2015, month => 10 }),
   '/blog/2015/10';

is $router->path_for({ controller => 'WikiPage', action => 'show' }, { page => 'HelloWorld' }),
   '/wiki/HelloWorld';

is $router->path_for({ controller => 'Download', action => 'file' }, { splat => [ 'path/to/file', 'xml' ] }),
   '/download/path/to/file.xml';

is $router->path_for({ controller => 'NoSuchController', action => 'show' }),
   undef;

何か変なところがあったら GitHub リポジトリ のほうまでお知らせください。

A Tour of Go のその先: 『みんなのGo言語【現場で使える実践テクニック】』

著者の一人であり、同僚でもある songmu さんに『みんなのGo言語』をいただきました。Go言語界隈の有名人がずらりと顔を並べていて豪華。拙作のツールも大きく取りあげていただいて、ありがたいです。

自分もGoという言語が好きで、趣味ではよく書いている（最近はおろそかだけど）んだけど、執筆陣はリアルワールドでGoを使いこなしている歴歴。オムニバス形式の各章がそれぞれの著者の背景を反映してバラエティに富んでおり、A Tour of Go、Effective Goを終えた人が、入門一歩先のGoをつまみ食いするのにとても良い本だと思った。

思ってみれば、Goは簡素な文法をもつようデザインされていて、要所を押さえた標準のツーリング等々を見ても、その使用者に与えられている道具というのが意図的に限られている言語だった。そしてそのことが、コードだとかプロジェクトの構成だとかの、書かれたものとしてのGo言語全体の複雑度を下げることに貢献しているのだけれど、一方でGoはさまざまの実用的な目的のために使われる言語でもあり、使用者はその乏しい表現力の中でいかに現実的な課題を解くのか、という問題に直面することにもなる。

そこでGoで本格的なプログラムを書くには、言語そのものへの知識に加えて、その周辺に醸成されているイディオム的な語彙を身につけることが他の言語に比較して重要になると思う。そういうものってのは常にドキュメントされているものではないわけで、Go的なやり方を知るためには例えば自分はGo公式のソースコードを読んできた（この本でも何人かの著者が紹介している）けれど、今回この本が登場したことで、より分かりやすい形での指南役が増えたのは喜ばしいことだと思う（あと『Go言語によるWebアプリケーション開発』の鵜飼さんによる巻末付録とかもいい）。

すでに語られているし、個別の内容にはあまり触れる必要はなさそうだけど……、songmu さんによる1章、fujiwara さんによる3章、suzu_v さんによる6章はGoを書く人なら全員読む価値があり、mattn さんによるマルチプラットフォーム、deeeet さんによるコマンドラインツール、lestrrat さんによる reflect パッケージはそれぞれ各論のすばらしい解説になっている。自分はLL的なバックグラウンドをもっているのだけれど、そういう観点から見たGoというのも各所で語られていてよかった。

今後Goの入門系の書籍であればウェブアプリケーションとか、並行処理に特化した話題も気になってくるところですね。読みたい〜。

みんなのGo言語【現場で使える実践テクニック】