🚀 go-pugleaf

河野真治 @ 琉球大学情報工学です。

学部は化学だったので、コンピュータ関係の理論をしっかり勉強
したのは大学院からです。

哲学には興味があったし、当時、東工大には吉田夏彦先生と前原
昭二先生がいたので、否応なく記号論理学も勉強してたんですが...
高校時代に島内剛一の「数学の基礎」に手を付けて挫折した記憶
があって、実は結構、苦手な意識があった。あれじゃなくて、前
原先生の「数学基礎論入門」を読んでいれば、かなり違っていた
んじゃなかろうか。群論も、岩波の「代数学」じゃなくて、アル
ティンの「ガロア理論入門」から読んでいればなぁ... 

でも、東大だと、ちゃんと勉強している先輩がいたので、良い本
を読めたと思います。D ate のDabase とか、Ulman のAutomaton,
Compiler とか。Manna の Mathematical Theo ry of Computation
も、その一つ。

当時、大学には海賊版の書籍を売る業者が出没していて、手のこ
の本が安く買えたんだよな～ 取り締まりでなくなってしまいまし
たが。日本コンピュータ協会が極悪で、基本的な入門書を超高額
のハードカバーで売っていた。あんなの買えないよ。日本のコン
ピュータ文化の発展を阻害した協会だと思う。

最近、貧乏なので、また本を買えなかったりするんだよな。でも、
プログラミング理論の本って、Manna のが現状でも一番良いんじ
ゃなかろうか? 網羅的だし、わかりやすいし。しかも、あまり役
に立たない理論は無視しているし。

言っちゃ悪いけど、λ計算の理論の大半は役に立たないと思う。
特にCCC系か。合流性とかは面白いけど実用性はないしな～ Fixed
point 系もだめだと思う。

Model checking は「状態の数え上げ」で、つまりは「しらみつぶ
し」なのでわかりやすい。それで、何を調べるかと言うことにな
ると、やっぱり、

　論理学、(特に時相論理)

に戻ることになります。状態の入口と出口に論理式を張り付けて
いくのがホーア理論なので、それもわかりやすい。ソフトウェア
工学的に、もっと注目されるべきだと思うが. .. 

　最終的に要求される出力を論理式で表して、
　それをプログラムの実行とは逆方向に推論して行って、
　ループの部分を「不変式」で乗り越える

ってのは、微妙にダメだと思う。やってみるとわかるんだけど、
これで要求される論理式の大きさって、プログラムの大きさの2-4
乗ぐらいになる。

プログラムの正しさを記述すると言うのは、そういうことなんだ
けど、そもそもプログラミング出来る人間が100人に一人ぐらいし
かいないのに、プログラムの正しさの記述となると、1000人に一
人。しかも、記述量は膨大... 

プログラムと、その正しさの記述が1対1ぐらいでないと勝負にな
りません。もっとも、要求される正しさにもよる。モデル検証が
広がったおかげで「正しさを記述する重要性」つまり、形式的仕
様記述の重要性が広まっていることは確か。でも、それは、

　モデル検証で検証するべきプロパティって何ですか?

という質問だったりするんだよな。それがわかってないと言うこ
とは「何をプログラミングしているのかわかってない」というこ
となんだが... 

モデル検証用の複雑なBrancing Temporal Logic 式を集めたサイ
トとかを見ると、なんか本末転倒だと感じる。なんで、ものごと
を複雑にしたがる... 

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科