プログラミング理論
河野真治 @ 琉球大学情報工学です。
学部は化学だったので、コンピュータ関係の理論をしっかり勉強
したのは大学院からです。
哲学には興味があったし、当時、東工大には吉田夏彦先生と前原
昭二先生がいたので、否応なく記号論理学も勉強してたんですが...
高校時代に島内剛一の「数学の基礎」に手を付けて挫折した記憶
があって、実は結構、苦手な意識があった。あれじゃなくて、前
原先生の「数学基礎論入門」を読んでいれば、かなり違っていた
んじゃなかろうか。群論も、岩波の「代数学」じゃなくて、アル
ティンの「ガロア理論入門」から読んでいればなぁ...
でも、東大だと、ちゃんと勉強している先輩がいたので、良い本
を読めたと思います。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
河野真治 @ 琉球大学工学部情報工学科
Fnews-brouse 1.9(20180406) -- by Mizuno, MWE <mwe@ccsf.jp>
GnuPG Key ID = ECC8A735
GnuPG Key fingerprint = 9BE6 B9E9 55A5 A499 CD51 946E 9BDC 7870 ECC8 A735