型と名前によるGoのコード探索 ― gofind

思いつきでツールを作ってはリスのように忘れ、再発見しては新鮮な気持ちで便利に使う日々です。

一般にプログラミングにおいては、ソースコードを読むことに意外とばかにならない時間を使うもの。特に Go ではデフォルトで標準ライブラリのソースコードが手元にあり、コードを書く際よい教科書になるので、これを読むことも多いはず。

Go は静的に型付けされる言語なのでその点コードは読みやすいけれど、データ構造が不変ではないので、ある構造体のフィールドがどこで書き換わるのかを知るには、処理を追っていくしかない。名前で grep するのもひとつの手ではあるけど、精度はあまり期待できない。

そこで gofind。簡単に言うと、型やパッケージを含めた名前でもって Go のソースコードを検索するツールです。

go get github.com/motemen/gofind/cmd/gofind

使い方は以下の通り。

gofind <pkg>.<name>.[<field>] <pkg>...

コードを読んで型付けまで行うので、実行には少し時間がかかる。

第一引数が、コード中の出現を見つけたい型や関数のパッケージ名で修飾された名前。型が構造体である場合には、フィールド名をオプショナルにつけることができる。指定できるものは以下のようなところ。

• 型名
• 関数名
• （構造体型の）フィールド名
• メソッド名

以降の引数は検索対象のパッケージで、普通にインポートパスを指定してもいいし（net/http とか）、ディレクトリでもいい（./lib/web とか）。

すると、指定された型や名前を持つ変数とかメソッドの出現をハイライトしてくれる。

利用例

実例を見るのが早いので、以下でいろいろ検索してみます。

構造体型のフィールド

このフィールド、どこで更新・参照されるんだろう？ というときに。gofind のもともとの動機です。

% gofind crypto/tls.Config.ServerName net/http
...
net/http/transport.go:1015:             if cfg.ServerName == "" {
net/http/transport.go:1016:                     cfg.ServerName = cm.tlsHost()
net/http/transport.go:1039:                     if err := tlsConn.VerifyHostname(cfg.ServerName); err != nil {
net/http/transport.go:2081:             ServerName:                  cfg.ServerName,
net/http/transport.go:2114:             ServerName:                  cfg.ServerName,

面白いのは、構造体リテラルのフィールド名も発見できること。画像で見るとわかりますが、ServerName: もハイライトされている。

構造体の無名初期化も検出できるのが便利。これは grep では発見しづらいところ。

% gofind go/ast.Package.Imports go/ast
go/ast/resolve.go:173:  return &Package{pkgName, pkgScope, imports, files}, p.errors.Err()

関数

go list std は標準パッケージの一覧。こうやって公式にどういう使い方がされているか発見できるので、生きたサンプルとして役立つ。

% gofind strings.Split $(go list std)
archive/tar/reader.go:781:      sparseMap := strings.Split(extHdrs[paxGNUSparseMap], ",")
crypto/tls/common.go:597:       labels := strings.Split(name, ".")
...

型

変数や構造体のフィールドで、指定された型を持つものを検索。

% gofind golang.org/x/tools/cmd/stringer.Package golang.org/x/tools/cmd/stringer
golang.org/x/tools/cmd/stringer/stringer.go:133:        g.Printf("package %s", g.pkg.name)
golang.org/x/tools/cmd/stringer/stringer.go:170:        pkg *Package     // Package we are scanning.
...

gofind sync.Mutex $(go list std) などとすれば、公式のソースコードでこの型がどういう名前付けをされているかわかるわけです（Go 言語における並行処理の構築部材 - 詩と創作・思索のひろば）。

メソッド

% gofind encoding/json.Encoder.Encode golang.org/x/tools/cmd/godoc
golang.org/x/tools/cmd/godoc/handlers.go:146:   json.NewEncoder(w).Encode(resp)

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

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

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

形式系

第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 リポジトリ のほうまでお知らせください。