文系プログラマでもコンピュテーションをアンダースタンディングできた！！１ - 書評『アンダースタンディングコンピュテーション』

タイトルは煽りです。

『アンダースタンディングコンピュテーション―単純な機械から不可能なプログラムまで』をご恵贈いただきました。ありがとうございます。

作者: Tom Stuart,笹田耕一(監訳),笹井崇司
出版社/メーカー: オライリージャパン
発売日: 2014/09/18
メディア: 大型本
この商品を含むブログ (2件) を見る

本書の扱う計算理論と呼ばれる分野には、前職の同僚たちがそういうのに詳しかったこともあってずっと興味を持ってはいたものの、いくつかの教科書的な本を繙いては読み進めずに挫折することを繰り返していました。その意味で、監訳者あとがきの「これなら私でも読める」という言葉は、自分自身の思いでもあると感じました(もちろん、笹田さんの「私でも」と、僕のそれとではおおいに異なることはいうまでもありませんが)。

計算とは何か？それはつまり「コンピュータの行うこと」であるのは間違いないことではあるものの、私たちプログラマが日々書いているプログラムが、どのような意味を持ち、どういう過程を経てその「計算」にたどり着くのかについて、すらすらと答えられるひとは多くはないでしょう。もちろん、そのようなことを知らずとも優れた仕事を行うことは可能でしょうけれども、いったんひっかかった疑問に、なにかしらの答えを見出したいと思うのもまた、自然なことです。

本書ではそれを、以下の題材を取り上げつつ、プリミティブなところからひとつづつ積み上げて解説していきます。

プログラミングの意味についてのふたつの意味論(semantics): 操作的意味論と表示的意味論
限られた機能を持つ小さな「機械」: 決定性有限オートマトン、非決定性有限オートマトン、プッシュダウン・オートマトン
「究極の機械」としてのチューリングマシン
プログラミングによってチューリングマシンをシミュレートする: 型なしラムダ計算、SKIコンビネータ計算、Iota、etc.
決定不可能性問題と、その近似的な解決としての抽象解釈

扱われている内容自体は、教科書的な書籍をいくつか組み合わせればカバーされるようなものであるかもしれませんが、本書はそうした教科書たちとは異なり、内容を形式的に述べるよりもむしろ、Rubyのコードで直接的に示すことでわかりやすさを採っているというのが特徴でしょう。たとえば、操作的意味論について

操作的意味論とは、プログラミングがある種の装置上でどのように実行されるのか、その規則を定義することによって、プログラミング言語の意味を記述する方法です。

と述べつつも、その「規則」を形式的に説明するよりもむしろ、

1つの方法は、構文を小さなステップ(スモールステップ)で繰り返し簡約(reduce)することによって、プログラムを評価する機械を考えることです。ステップを経るたびに、プログラムは最終結果、最終的にそれが意味するものへと近づいていきます。

と、SIMPLEという単純なプログラミング言語を元に、その抽象構文木(Abstract Syntax Tree)がどのように簡約されていくかの規則を簡単なRubyプログラムで書き表すことによって、「プログラムの意味」を直感的に理解させてくれます。

また、簡単な機械から説き起こし、そうした「別の仕事をやりたくなるたびに新しい機械を設計するのではなく、入力からプログラムを読み込んで、そこに書かれた仕事をやるような単一の機械」としての万能性を持つ、チューリングマシンと等価である計算能力を持つシステムを示す第6章では、

変数の参照
procの生成
procの呼び出し

のみ、すなわち、型なしラムダ計算と同様のスタイルのRubyプログラムによって説明することで、個人的には、これまでどうやっても理解にいたらなかったラムダ計算というものが、少なくとも記述についていくことによってなんとなくはわかるものになったという意味で、非常にありがたいものでした。

さらに、そのラムダ計算同様の「万能性」を持つ様々な「規則のシステム」が紹介されるわけですが(そこには、ライフゲームなども含まれる)、ラムダ計算よりもさらにシンプルに見えるSKIコンビネータ計算やIotaが、ラムダ計算と等価である(すなわち、それらを使ってラムダ計算の表示的意味論を与えることができる)というのは、我々の(？)行っている計算というものは、畢竟、ある構造をいかに簡約するかという規則と、その実行にまでシンプルにできるのか！と衝撃を覚えました。

ところで昨今は、JavaScriptに静的型付けをサポートするタイプのaltJSが多数出てきていたり、RubyやPythonにおいて型注釈の導入が議論されていたり(Ruby、Python)など、いわゆる動的言語のコミュニティにおいても静的型付けに対する関心が高まっているように見受けられます。本書では、決定不可能性問題を近似的に解決する手法としての抽象解釈、その具体的な方法としての静的意味論について述べられており、その方面への関心からも興味深い内容が語られています。

変数に静的な型を付けることのメリットというのはいろいろあるのでしょうが、その中でもここで述べられるのは、あるプログラムがどのように実行されるのかは、実行してみなければわからない、すなわち静的解析によっては決定不可能であるという根本的な不可能性に対して、我々人間が、現実の世界を抽象化した地図によっておおいに恩恵を受けるのと同じように、静的型付けによる近似的な計算により、プログラムを実行せずともある範囲での安全性を確かめられるということです。極端にいえば、IDEの支援を受けられるとかコンパイル時に型チェックできるのは便利だなぐらいにしか思ってなかったので、蒙きを啓かれました。

そういったわけで、ごく限られた機能を持つ小さな機械から始まって、一般的なプログラムを実行できるという万能性を持つ機械と、それと等価なプログラムによるシステム、そしてそれらが本質的に抱えている計算不可能性を通じて、型理論のさわりにまでいたる本書は、幅広い内容を扱いつつも、単にそうした分野に興味を持っているだけの初学者を過度に恐れさせる形式性を避け、ある程度までの理解へとすんなり導いてくれるという、稀有な本であるように思えました。僕と同じように、計算理論について知ってみたくていろいろ挑戦したけど挫折しまくってきた人々に、間違いなくおすすめしたい本です。

アンダースタンディングコンピュテーション―単純な機械から不可能なプログラムまで