コンパイラについて始めて聞いた時は、かなり感動した ものである。プログラ ムを解析して、それと同等の動作をする機械語コードを自動生成するなんて、 一体どういう仕組みになってるんだろうかと大いに興味を持った。結局今日 に至るまで、コンパイラの教科書をまじめに読んだ事はないのだが、コンパイ ラと同等のものを独自に作った事はある。

      プログラムというのは論理的な構造と意味を持ったものであって、プログ ラムが間違っていない事を確かめる作業も、一つのプログラムを書き換えてよ り性能の良いプログラムや、似て非なるプログラムを作る際にも、その論理的 構造や意味を理解しない限り、作業は何ひとつ進まない。例えば、数値解析の 理論を作って、理論の正当性が数学者達によって確認されたとしても、それは その理論に基づいて作成されたとされる数値解析プログラムが、理論通り正確 に作られている事を意味しない。やはりプログラムと理論を見比べてチェック する必要があるわけである。結局、プログラムを「ちゃんと理解する」という 作業が必要になるわけだ。小さなプログラムを扱う限りでは、人間が頑張れば 良い事だが、大きなプログラムや大量のプログラムについて、上のような作業 をするとなると、当然人手だけに頼るのは大変で、コンピュータに任せようと いうことになる。そうなると、コンピュータがプログラムの論理を理解できる か？という問題になる。

      数理論理学はこの問題にある程度答える事ができる。つまり、数理論理学の新 しい理論を作る事によって、コンピュータがプログラムの論理を理解するメカ ニズムを明らかにする事ができるわけだ。私はこの理論を研究した結果、「証明 コンパイラ」という概念にたどりついた。例えば数値解析の理論を人間がプログ ラム化するからミスが発生するのであって、数値解析の理論をそのままコンピュー タに入力して、コンピュータがその理論の正当性の確認をした後にプログラム を自動生成してしまえば問題は無いわけである。そこで証明コンパイラの理論 を使って実際に上のような処理をするシステムを作ろうということになった。 勿論そのシステムが理論通りに作られているか、という問題は残るのだが、一 つのシステムについて一度限りしっかりチェックしておけば良いのである。証 明コンパイラ・システムなるものを、どうやって作れば良いかは、コンパイラ についてのいくらかの耳学問と、自分の理論をより精密に考えていくことによ り、自ずとわかってくる。結局、字句解析、構文解析、エラー処理、コード生成処 理を行う通常のコンパイラと同じようなものが出来上がった。 しかし、通常のコンパイラと違う部分もかなりある。それについて一言で説明 するのは難しいが、通常のコンパイラはプログラムの論理的「構造」(つまり 文法構造)については十分に解析するが、プログラムの論理的「意味」につい ては、ほとんど解析していない。しかし、証明コンパイラは、数理論理学の理 論に基づいて、プログラムの論理的「意味」まで解析する。この結果、入力文 の「文法的には正しいが意味は通らない」部分も正確に見つけ出し、さらにプ ログラムの表面的な形だけではなく、意味も考えないとできないようなプログ ラムの修正もある程度はできる。このような事は通常のコンパイラではほとん どできない。 結局証明コンパイラの理論は、コンパイラ技術を飛躍的に発展させるための理 論の一つだったわけである。

      コンピュータの概念がどう発展しても、人間の指 示を一切受けずに全く独自に思考・判断して動き回るという事は、あってもらっ ては困る。そうなったら、まさに人間の言う事に聞く耳を持たない、 刃物を持った狂人がその辺をウロウロして いるようなものだろう。 何らかの形で、人間の意図や指示をコンピュータに 伝えるための「言語」が必要になる。 その言語をコンピュータが理解できる形 に変換するものがコンパイラ技術である。およそ高等動物の「言語」には論 理が内在するから、人間とコンピュータを論理を媒介として結びつける技術の 重要性は変わらない。感性や感情のコミュニケーションも大切だが、それだけ で良いというのなら、我々の生活は犬や猫と同じなのか、ということになる。 そして、心ある計算機科学者は、コンパイラ技術が理論と実践が理想的な形で 融合している極めて良いお手本であり、プログラム言語の処理系にとどまらず、 人間とコンピュータの間を媒介する数多くの技術に応用できることを知ってい る。 コンパイラの理論には、古典的なオートマトン理論、文脈自由文法理論にとど まらず、広く数理論理学や計算理論等も関連してくる。数理科学的にも極めて 興味深い分野であり、それらの理論は実践家が開発したさまざまな技術と深く 係わってくる。新しい理論を使って技術を向上させたり、実践家が個々のコン パイラについて開発した技術を、理論的に裏付けすることにより、より普遍的 な技術に高めたりできるのである。