“
たかが論理、されど論理
私は生涯一プログラマでありたいと思っているものである。
私の得意とする言語はＣである。
Ｃ以外のプログラミング言語では、
本物のプログラムは書けないとさえ思っている。
Ｃにはモジュールの機能がないとか、
並行処理のためのプリミティブがないとか言いながらも、
実は内心では、
Ｃよりすぐれたプログラミング言語を設計することなど不可能だと思っている。
時たま Common Lisp などという言語を使うこともあるが、
それは単なるプロトタイピングだと割り切っている。
Lisp で書かれたシステムはすべてプロトタイプであり、
本物のシステムにするためにはＣで書きかえなければならないと思っている。
なぜＣが優れているのかといえば、
フォン・ノイマン型アーキテクチャにベッタリしているからである。
つまり、私は何を隠そう、
フォン・ノイマン型以外のコンピュータは実用にはなり得ないと
信じているものの一人である。
表向きはデータ・フローとかリダクション・マシンに興味のある bit の読者を
装ってはいるが、
ハードウェアの進歩とは、単なるメモリ量の増加、
単なる CPU クロックの高速化、単なる CPU 数の増加、
単なるディスクの巨大化と高速化、単なるネットワークの高速化 ... 等々
であると思っている。
そして、表向きは関数型言語や論理型言語に興味のある bit の読者を
装ってはいるが、
その実情は、Ｃ言語しかまともに使ったことがないのである。
というのは実は嘘で、
かつては FORTRAN で腕ならぬカードパンチャをならしたこともあるし、
Pascal で助かる夢を見たこともあったが、
結局こうしてＣに静かに落ち着いているのである。
それは、一つには、
Ｃプログラマに与えられる仕事の中には、
FORTRAN プログラマに対する仕事のように簡単ではなく、
Pascal プログラマに対する仕事のように退屈ではなく、
十分難しくて、
十分汚らしくて、
十分ワクワクするものがあるからなのだろう。
そのような私も、かつて、論理学というものを学んだことがある。
論理学はロジックともいう。
ロジックをよくするもののことをロジシャンという。
英語の職業の名前には「イシャン」という語尾がつくものがいくつかあるが、
どうも、どれもこれも一癖か二癖あるイカガワシイ職業のようである。
その最たるものがポリティシャンであるが、
その他にも、マジシャン、テクニシャン (?) というように、
口八丁手八丁の手合が揃っている。
例えば、外科医はサージオンであるが内科医はフィジシャンである。
また、芸術家はアーティストなのに音楽家はミュージシャンである
(これは音楽家がラッパを吹くからだという説がある)。
そして、科学者はサイエンティスト、物理学者はフィジシストであるのに、
数学者はマセマティシャン、
論理学者はロジシャンというのはどうしたことであろうか。
まあ、そんなことは大したことではない。
ここで述べようと思うのは、
そのようなロジックの素養が
現在のプログラマ生活にどのように役立っているかという、
非常に真面目な話である。
つまり、コンピュータ・サイエンスと呼ばれる学問の中で、
論理学に基礎を置いている分野の素養が、
プログラムを書く上でどのように役立っているのかを述べたいと思うのである。
私のような一介のＣプログラマから見た、
それらの分野の存在価値というものについて述べてみたいのである。
* 検証論
ロジックとコンピュータ・サイエンスといえば、
最初に思い浮ぶのは、Floyd と Hoare に始まるプログラムの検証論である。
例えは、Hoare の推論体系では、
| {P} S {Q}
という形の式を証明の対象とする。
これをアサーション (assertion) という。
ここで、S はプログラム、P は入力条件、Q は出力条件で、
{P} S {Q} は、
「P が成立しているときに S を実行して停止したら Q が成り立つ」と読む。
例えば、
| {x は偶数} x:=x+1 {x は奇数}
はアサーションである。
x が偶数のとき x を一増やせば (x:=x+1) x は奇数になるので、
これは正しいアサーションである。
Hoare の体系では、
いくつかの (正しい) アサーションから
別の新しい (正しい) アサーションを得る推論規則によって
プログラムの検証を行うようになっている。
一つ一つの推論規則は、プログラミング言語のオペレータに対応している。
例えば、
| {P} S {Q} {Q} T {R}
| --------------------------
| {P} S;T {R}
という規則がある。
---- の上が前提で下が結論である。
この規則は ; (逐次実行) というオペレータに対応するものである。
例えば、上の例のアサーションと、
| {x は奇数} x:=x+1 {x は偶数}
というこれも正しいアサーションと、上の ; に関する規則を使えば、
| {x は偶数} x:=x+1;x:=x+1 {x は偶数}
というこれも正しいアサーションが導かれる。
さて、
バグのないプログラムを作ったり
自分のプログラムにバグのないことを人に納得させたりするのに、
Hoare の体系が実際に役に立つのだろうか。
Hoare の体系の一つ一つの規則は極めて当たり前のことである。
およそプログラムの書ける者なら、つまり、
プログラムがどう走るかわかっている者なら、
誰でも簡単に Hoare の体系の規則を再構成することができる。
往々にしてロジックというものは、そのように当たり前であることが多い。
だから、ロジックに親しみを感じるような「ロマンチスト」でない人々は、
なんでこんな当たり前のことを仰々しく説教するんだ、
帰ってローグでもしよう、
と怒り出してしまったりするのである。
その上、Hoare の規則を一つ一つ律義に追いかけて
プログラムの検証を行うのは全く非現実的なことである。
世の中にはプログラムの検証を支援してくれるシステムがここかしこに
いろいろとあるようだが、
一介のＣプログラマである私にとっては高嶺の花である。
しかも、聞くところによれば、
そのようなシステムのどれ一つをとっても実際の役には立っていないようである。
では、Ｃプログラマの私にとって、
Hoare の体系を学ぶということにいったいどのような意義があるというのだろう。
二つあると思う。
一つはアサーションという「概念」にある。
Hoare の体系を学べば、
少なくとも、
プログラムの正しさは {P} S {Q} というアサーションと呼ばれる概念によって
定式化できるのだということがわかる。
Hoare の規則は誰でも再構成できると述べたが、
それはもちろん、アサーションという概念を知っていればの話である。
アサーションという概念を知っているかいないかで、
プログラムの正しさに関する考えや感覚が違ってくるのではないだろうか。
例えば、プログラムの内部仕様書を書くときでも、
このプログラムはこういう入力条件の下で働き、
その結果、こういう出力をする、
というような定式化が自然に行えるようになる。
しかし、概念を学ぶということは、
方程式とかアルゴリズムとかを学ぶとことに比べて、
非常に弱々しいことである。
その弱々しさは、まさに「教養学部」的知識の持つ脆弱さといえよう。
つまり、アサーションという概念を知っているからといって、
それが直接にプログラムの信頼性や生産性の向上に結びつくわけではない。
そこには個人差というものがある。
例えば、bit に FFT (fast Fourier transform) の記事が載っていたとしよう。
その記事を読んで理解した人は、
FFT という確実な知識を確実に得る。
もし FFT を使わなければならない事態が生じた場合、
FFT を知っているかいないかは白か黒かである。
それに対して、bit に Hoare の体系の記事が載っていたとしよう。
その記事を読んで理解した人の中には、
何だ当たり前のことじゃないか、読んで損をした、と思う人もいるだろうし、
フムなるほど、と思うがすぐに忘れてしまう人もいるだろう。
アサーションという言葉と概念に魅せられるキトクな人も何人かはいるに違いない。
要するに、読んだ結果は人それぞれなのである。
また、アサーションという概念を使わなければならないと
どうしようもないような事態などあるのだろうか。
たとえそのような事態があったとしても、
bit の記事のことを思い出す人がいるのだろうか。
自力で似たような概念をあみだしてしまう人もいるかもしれない。
この場合、
アサーションを知っているかいないかは、せいぜい薄い灰色と濃い灰色である。
従って、そのような教養学部的知識というのは、個々人に向けられるというより、
社会全体に対して向けられていると考えるべきではないだろうか。
社会全体に浸透したとき、
つまり、世間一般の常識となったときに、
社会全体として何らかの効果が見えてくるのである。
それは一つには個人差というものがあるためだが、個人差だけの問題ではない。
社会の人々全員が同じ概念に慣れ親しんだとき、
そこにコミュニケーションというものが生じるのである。
もしも bit のその記事を皆が (いやいやながらも) 読んで、
皆がアサーションという概念を理解しアサーションという言葉を覚えたならば、
そこに会話が生まれるのである。
(ハー、教養学部的議論は疲れるものである。)
数学に「必要十分条件」という概念がある。
別にこの概念を知らなくても数学に不自由はしないだろう。
というより、このような概念は知らず知らずのうちに誰もが使っているものである。
しかし、必要十分条件という言葉があるのとないのでは、
「社会全体の効率」が大分と違うのではないだろうか。
ただし、必要十分条件とアサーションは若干状況が異なっている。
やはり、アサーションという概念を把握するためには、
Hoare の体系を一度はチャンと勉強せねばならないのである。
先に、Hoare の体系を学ぶは意義は二つあるといったが、
その二つ目とは、
Hoare の体系がブログラムの意味論を定めているということである。
Hoare の体系はプログラムの検証のための推論規則を与えているのだが、
逆に、Hoare の体系の推論規則を通してプログラミング言語の意味を
正確に把握できるというのである。
そこで次にプログラミング言語の意味論について述べよう。
* 意味論
プログラミング言語に厳密な意味論を与えようという努力は数多く行われてきた。
上述の推論規則による意味論は
公理的意味論 (axiomatic semantics) と呼ばれるものである。
この他に、仮想機械による操作的意味論 (operational semantics)、
λcalculus への翻訳による表示的意味論 (denotaional semantics) がある。
つまり、プログラミング言語の形式的意味論には
三つの流派 (家元) があるといえる。
私のようなＣプログラマには操作的意味論はよくわかるのであるが、
その他の意味論はどのような意義があるのかよくわからない。
公理論的意味論については上で検証の話をしたので、
以下では表示的意味論と操作的意味論について少しみてみよう。
表示的意味論では、
プログラムにλcalculus という形式体系のλ項というものを
対応させることによって、
プログラムの意味を定義する。
一般にλ項は関数を表現するのだが、
この場合、プログラムに対応づけられるλ項は、
プログラムの初期状態に対してプログラムの終了状態を与える関数になる。
例えば、プログラム S に対するλ項を [S]、
プログラム T に対するλ項を [T] とすると、
プログラム S;T に対応するλ項は [T]・[S] となる。つまり、
| [S;T] = [T]・[S]
ただし、・は関数の合成を表わす演算子である。
表示的意味論によってプログラミング言語の意味論を与える場合、
上ような等式 (といっても上の等式は余りにも簡単なものであるが) が、
山のように続く。
どのように山のように続くのかというと、
例えば Algol68 では電話帳が 2 冊埋ってしまっている。
また、かつて Ada の表示的意味論を同様にして与えるという企てがあったらしいが、
その後、何の音沙汰もないから、きっと挫折してしまったんだろう。
Ｃプログラマとしては、
Ｃの表示的意味論だけは書かないで欲しいと思うのである。
本当のことをいえば、
λcalculus への翻訳だけが表示的意味論の本質ではない。
翻訳の対象となっているλcalculus の厳密なモデルを定式化することが、
数学的な見地からいうと最も重要な問題なのであるが、
そこまでいくと、もはや一介のＣプログラマとしては手が届かないので、
もはやコレマデ。
仮想機械による操作的意味論とは、
仮想機械の定義と、
プログラムから仮想機械のコードへの変換規則
(早い話がコンパイルのし方) を定め、
それでプログラミング言語の意味論が定義されたとしてしまう、
全く節操のない意味論である。
これは、
Pascal の P-code インタープリタと P-code へのコンパイラを読んた人が、
「これで遂に Pascal という言語がわかったぞ」と叫ぶのに似ており、
Lisp で書かれた eval がマニュアルの最後のアペンディックスにないと
我慢できない Lisp ブログラマのことでもある。
Lisp の場合、
eval が仮想機械であり、
仮想機械コードへの変換には強いていえば昔懐かしい MS 変換があたる。
操作的意味論は節操のない意味論ではあるが、
数多くの長所をもっている。
まず、仮想機械の効率がよければ、
つまり、仮想機械の構造が
フォン・ノイマン型のコンピュータで高速に実行できるようなものであれば、
それをそのままインプリメントしても
十分に実用的な処理系ができるということである。
また、プログラミング言語の意味論で問題になる部分は、
実際の計算機の影響を受けている汚らしい部分であることが多く、
その場合、仮想機械というのは何の理論的な制約も受けないから、
汚いものは汚いものとして定義することができる。
では、他の意味論、
つまり、公理的意味論と表示的意味論にはどのような意義があるのだろうか。
仮想機械による操作的意味論と同様に、
公理的意味論ならば適当な自動証明系によって、
表示的意味論ならばλcalculus のインタープリタによって、
意味論から直接に処理系を実現できると主張する人々がいる。
しかし、そのような方法で実用的な効率のよい処理系を得るのは難しい。
従って、公理的意味論と表示的意味論の最大の利点は、
その「わかりやすさ」ということになる。
確かに、仮想機械による意味論は、
詳細すぎるためにわかりにくい
(と公理的意味論や表示的意味論の支持者はいう)。
しかし、だからといって、
公理的意味論や表示的意味論の方がわかりやすいとどうしていえるのだろう。
確かに公理的意味論と表示的意味論においては
不必要な詳細さはある程度は排除されるけれども、
プログラミング言語が現存の計算機の上で効率よく走ることを想定して
設計されているとするならば、
どうしても「機械」というものの呪縛から逃れられず、
操作的意味論と同等の複雑さを持たざるを得ないはずである。
また、操作的意味論においても、
不必要な詳細さを排除しつつ、
なるべく抽象的に仮想機械のアーキテクチャを設計すれば、
公理的意味論や表示的意味論に劣らぬわかりやすい定義を与えることができる。
つまり、私のようなＣプログラマから見ると、
抽象的な (?) 操作的意味論と、
具体的な (?) 公理的意味論もしくは表示的意味論は、
機能的には全く同じものに思えるのである。
実際、各々の意味論は、
適当な制限のもとで互いに変換し合うことができるだろう。
プログラミンク言語の意味論の差は宗教の差だという意見がある。
私としては宗教戦争には参加したくないので、コノヘンデ。
プログラマとは技術者である。
技術者に意味のあるのは技術の有効性である。
技術には正義も悪もない。
だから、
操作的意味論が好きだとかは、表示的意味論の方が好きだとか、
そういう好き嫌いをいうべきではない。
操作的意味論に合ったところには操作的意味論を使い、
表示的意味論に合ったところには表示的意味論を使い、
どちらでもいいところでは、どちらを使ってもよいのである。
いうまでもなく、Ｃプログラマである私は、
フォン・ノイマン型のアーキテキチャが至上のものであると信じている。
しかし、多くの bit の筆者のように、
フォン・ノイマン型のアーキテキチャは決して至上のものではなく、
とてつもなくアド・ホックでいい加減なもので、
もっと「計算というものの本質」に則したアーキテクチャがあるはずだと
考える人々がいる。
そして、その「計算というものの本質」は、
論理学などによる基礎的な考察から出てくると考えられている。
そのような人々にとって、
公理的意味論や表示的意味論は頼るべき大樹である。
実際、少し乱暴な言い方かもしれないが、
公理的意味論から論理型言語、
表示的意味論から関数型言語が生まれたと見ることもできる。
つまり、論理型言語は公理的意味論を直接実行するための言語であり、
関数型言語は表示的意味論を直接実行するための言語と考えられるのである。
そこで、論理型言語と関数型言語について少し述べたく思う。
* 論理型言語と関数型言語
私のようなＣプログラマにとって、
論理型言語と関数型言語は中途半端な存在に思えてしかたがない。
現在の論理型言語や関数型言語は、
ロジックにその基礎を置きながらも、
フォン・ノイマン型のアーキテクチャに色気を使っていて、
まったくもって男らしくないのである。
そのような色気を使うならなぜにＣを使わないのかといいたくなってしまう。
確かに、関数型言語や論理型言語はＣ言語の思いもよらない機能を生み出してきた。
しかし、関数型言語や論理型言語がフォン・ノイマンの機械の上で動いている以上、
効率というものを考えたとき、
いつもフォン・ノイマンの亡霊がいうのである。
「お前、高階関数は便利やけど、クロージャは高うつくんやで。
コンビネータも同じや」
とか「そこは論理的にはそれでええが、
カットをぎょうさん入れへんと速ならんで」
とかいわれてしまうのである
(なぜかフォン・ノイマンの亡霊は大阪弁である)。
そして、
フォン・ノイマンの亡霊のいわれるままに、
せっかくの機能を使うのをやめたり、
ひどいときには、
効率のために言語自体を歪めてしまうことになる。
しかし、いくらそのようなことをしても、
Ｃ言語より速くなるはずがない (フッフッフッ)。
ロジックの基礎を欠き、たいして効率もよくない言語は、
よっぽど便利なことでもない限り使う気にならない。
例えば Common Lisp は、
無節操と思われるくらいのデータ型を持ち、
余計なお世話と思えるくらい関数が多いので、
ついその便利さゆえに使いたくなってしまう。
聞くところによると、
Prolog も大変無節操な言語だそうだ。
いつか機会があれば使ってみようかとも思ってたりもする。
しかし、ロジックはその素性からして、
プログラミングにおいてではなく、
仕様記述において本領を発揮するものではないだろうか。
プログラミングにおいては、
目の前に種も仕掛けもある計算機というものが
白日のもとにさらけ出されてしまっているので、
なかなか「イシャン」の出番がないのである。
それにひきかえ、仕様記述という荒唐無稽の世界では、
「イシャン」たちが華々しく活躍してくれそうである。
* 仕様記述
プログラミング言語の意味論も、
プログラミング言語の意味を記述するのであるから、
仕様記述の一例ということができる。
しかし、プログラミング言語の意味論には仕様記述の醍醐味が余り感じられない。
なぜなら、プログラミング言語の意味は、
卑しくもプログラマと呼ばれるものならば、
大抵の場合わかり過ぎるくらいにわかり切ったことだからである。
つまり、プログラマにとってプログラミング言語もその意味も身内のものなのである。
それに対して、仕様記述というものは、
外から与えられた問題の仕様をいかに厳密に記述するかということではないだろうか。
形式的仕様記述の方法は数多く開発されている。
思いつくだけでも、
代数的仕様記述、
一階述語論理による仕様記述、
時相論理による仕様記述、
集合論を用いた仕様記述 ... 。
しかし、残念ながら、
本物のプログラマたちによって用いられているのは、
自然言語と図式による仕様記述である。
しかし、検証論のところで述べた意味で、
たとえ実際に使われなくても、
それぞれの記述方法が提示している概念には貴重なものが多い。
また、形式的仕様記述は、
仕様を書けばそれで一応の目的が達せられるので、
プログラムの検証に比べれば支援システムの可能性が大きい。
仕様記述と大きく関連するが、
抽象データ型に代表される大規模プログラムを作るための技術にも、
ロジックを基礎としているものがある。
これらの技術に現われる「概念」の中には、
大規模プログラムを開発するのに欠かせないものが多い。
まさにロジックの面目躍如たるところである。
しかし、ここでも、
「そんなこと知らなくても、
チャンとプログラムを書いて、
チャンとバグをとって、
チャンと仕様書を出せばいいんだろ。」
といわれてしまえば、グーの音もでないのである。
そこは、やはり、これは教養学部的知識なのだから、
教養として知っておいても損はないと開き直るしかない。
しかし、一介のプログラマとしては少々辛いところもあるが、
プログラマにプログラムを書かせる上司の立場に立ってみると、
また新たな視点が出てくる。
有象無象のプログラマたちに「チャンと」やるといわれても、
上司の方としては「チャンと」の意味をハッキリさせたいのである。
それには、帰りに一杯飲みながら腹を割って話すのが一番であるかもしれないが、
部下が、「ここは代数的に記述してみよう」とか、
「この問題は述語的な仕様の方が合っている」とかいっているのを聞けば、
「おおっ、チャンとやっているな」と安心することこの上ないのである。
ところで、そのような仕様記述の技術に現われる概念の中には、
既にロジシャンたちが大昔に発見しているものが多い。
そのような概念を応用して、
コンピュータ・サイエンティストたちが
得意満面になっているのを見ると、
今ではＣプログラミングを生業としているが
ロジックに造詣の深い (と自分では思っている) 私は、
ガクッときてしまうことがある。
しかしガクッとくるのは間違いだと思う。
別にロジシャンたちは、
そのような概念が計算機の世界で実際に使えるなどとは夢にも思わなかったわけで、
最初に発見した人も偉いが、
最初に使った人も偉いのである。
コンピュータ・サイエンスにおけるロジックの役割は、
やはり、長いロジックの歴史の中で蓄積された概念を、
コンピュータ・サイエンスの要所要所で次々と披露してくれたことではないだろうか。
それはこれからも続くことだろう。
つまり、コンピュータ・サイエンスにとってロジックは道具の一つなのである。
だから、便利なものは無節操にどしどしもらってきて使う。
それがロジックに対する正しい接し方なのだと思う。
* されど
しかし、私の中にはロジックを単なる道具と割り切れない心がある。
それは、今ではＣプログラマをやっているこの私にも、
From Froge to Godel などという本の中にある Godel の論文のコピーを
大事そうにかかえていた頃があったからである。
「たかが論理、されど Prolog」の筆者氏と同様、
私は東京で生まれ育ったのであるが、
「たかが論理、されど Prolog」の筆者氏とは異なり、
私は都立高校へ入学した。
やはり、ロジックを愛するロマンチストは、
都立高校へ行かねばならなかったのである。
ちょうどその頃「ゲーデルの証明」という本が出た。
これはゲーデルの不完全性定理を解説した本であり、
ロマンチストである私はこの本によってロジックの不可思議な世界に
魅せられていったのであった ...
いやいや、そのような 60 年代的感傷は 80 年代には似合わないのでやめよう。
今や世界は情報化社会。
日本にも JUNET などという大規模ネットワークが張り巡らされ、
毎日何キロバイトという情報が、
2400 baud という恐るべきスピードで飛び交っている。
そして、JUNET の fj ニュースグループには、
多くの人々が様々な意見を交換し合い、
毎日読むのが楽しみである。
さて、今日も楽しくニュースを読んだ私は、
踊る指先も軽やかに、エディタを呼び起こすのである。
と、画面には何やら漢字の文章が。
何々、「されど論理、たかが論理」？
どうやら、誰かが私のパスワードを盗んで
このようなザレ文を私の大事なディレクトリの下に入れたようである。
なにしろ、
生涯一プログラマでありたいと思っている私が、
こんなザレ文を書くはずがないのだからして。