哲学には興味があったし、当時、東工大には吉田夏彦先生と前原昭二先生がいたので、否応なく記号論理学も勉強してたんですが... 高校時代に島内剛一の「数学の基礎」に手を付けて挫折した記憶があって、実は結構、苦手な意識があった。あれじゃなくて、前原先生の「数学基礎論入門」を読んでいれば、かなり違っていたんじゃなかろうか。群論も、岩波の「代数学」じゃなくて、アルティンの「ガロア理論入門」から読んでいればなぁ...
でも、東大だと、ちゃんと勉強している先輩がいたので、良い本を読めたと思います。Date のDabase とか、Ulman のAutomaton, Compiler とか。Manna の Mathematical Theory of Computation も、その一つ。
当時、大学には海賊版の書籍を売る業者が出没していて、手のこの本が安く買えたんだよな〜 取り締まりでなくなってしまいましたが。日本コンピュータ協会が極悪で、基本的な入門書を超高額のハードカバーで売っていた。あんなの買えないよ。日本のコンピュータ文化の発展を阻害した協会だと思う。
最近、貧乏なので、また本を買えなかったりするんだよな。でも、プログラミング理論の本って、Manna のが現状でも一番良いんじゃなかろうか? 網羅的だし、わかりやすいし。しかも、あまり役に立たない理論は無視しているし。
言っちゃ悪いけど、λ計算の理論の大半は役に立たないと思う。特にCCC系か。合流性とかは面白いけど実用性はないしな〜 Fixed point 系もだめだと思う。
Model checking は「状態の数え上げ」で、つまりは「しらみつぶし」なのでわかりやすい。それで、何を調べるかと言うことになると、やっぱり、
論理学、(特に時相論理)
に戻ることになります。状態の入口と出口に論理式を張り付けていくのがホーア理論なので、それもわかりやすい。ソフトウェア工学的に、もっと注目されるべきだと思うが...
最終的に要求される出力を論理式で表して、
それをプログラムの実行とは逆方向に推論して行って、
ループの部分を「不変式」で乗り越える
ってのは、微妙にダメだと思う。やってみるとわかるんだけど、これで要求される論理式の大きさって、プログラムの大きさの2-4乗ぐらいになる。
プログラムの正しさを記述すると言うのは、そういうことなんだけど、そもそもプログラミング出来る人間が100人に一人ぐらいしかいないのに、プログラムの正しさの記述となると、1000人に一人。しかも、記述量は膨大...
プログラムと、その正しさの記述が1対1ぐらいでないと勝負になりません。もっとも、要求される正しさにもよる。モデル検証が広がったおかげで「正しさを記述する重要性」つまり、形式的仕様記述の重要性が広まっていることは確か。でも、それは、
モデル検証で検証するべきプロパティって何ですか?
という質問だったりするんだよな。それがわかってないと言うことは「何をプログラミングしているのかわかってない」ということなんだが...
モデル検証用の複雑なBrancing Temporal Logic 式を集めたサイトとかを見ると、なんか本末転倒だと感じる。なんで、ものごとを複雑にしたがる...
No comments:
Post a Comment