プログラムの書き方の本

今回は、プログラムの書き方の本。プログラムの宣言的な側面を扱うための本とでも言うか。id:t_yanoおまたせ。
ただ、こっち側はほんとに勉強を始めたばっかりなので、ちょっと目を通しただけで読んでない本もばかりだし、自分でもちゃんとわかってない部分も多い。そういうのを割り引いて見てもらえれば。

で、まずは、論理。プログラム書かなくても読んでほしい。

論理学

これは全部読んだ。
この本読むと、かしこさが15くらいあがる。日本語がうまくなる。考えるとき、間違った結論をださなくなる。議論するとき、議論の骨子をみつけて、議論からそれる部分を省くことができるようになる。
1章「命題論理」2章「述語論理」を読めば、あとはヤル気があれば読めばいいと思う。「様相論理」はあとで必要なのでがんばったほうがいいかも。
もう、「論理学」だけ読んでもらえばいいので、ここから先はオマケだ。

つぎに、集合論。論理と集合は深い関係がある。このブログを見てくれてる人なら、最近集合で遊んでたのを見たかもしれないけど、まあ「←いまココ」という感じ。そのときに買った集合論の本。

新装版 集合とはなにか―はじめて学ぶ人のために (ブルーバックス)

ただ、これも2章までは読むとして、3章をがんばって読むところまででいい気がする。測度とか位相空間とかは面白そうではあるけども。

さて、この集合論とか論理がプログラムにどうつながるか、ということになる。
もちろん、集合論はリレーショナル代数となって、みんな大好きRDBMSにつながる話ではあるけど、今回はプログラムの書き方なので、データベースの話はやめておく。データベースよく知らないし。データベースは、セルコとかデイトで検索して出てくる本を読めばいいんじゃなかろうか。

ということで本題に戻って、この本。いま読み始めたところ。

論理と計算のしくみ

集合から始まって、上の論理学の内容をもっと形式的になぞって、計算可能性を論理学的に説明して、ラムダ計算で終わる。計算論での計算可能性は、グラフ理論をベースとしたオートマトンから進めてると思うんだけど、こちらは論理から出発して、同じ結論にたどりつくというのが面白い。

あとは、圏論とかか。

圏論による論理学―高階論理とトポス

本だけ買ってまだ全然読んでないのだけど、「テンプレート処理が、もろにモナドになっている」とかいうのを納得できるようになれるとカッコイイ。
圏論やモナドが、どうして文書処理やXMLと関係するのですか？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
ごめんなさい、圏論って言ってみたかっただけです。

と、まあ、論理をつきつめると、こうやってラムダまで来ますよって言ってもなんだかピンと来ないという感じもするし、なにより、こちらの道は険しそう。なので、集合論や論理をプログラムの書き方につなぐ方法としては、仕様記述とかモデリング手法のほうが実際のプログラムの書き方へのイメージがつきやすそう。
そこで、形式仕様言語のZ言語の解説書が手元にあったので紹介しようと思ったのだけど、残念ながら絶版。

ソフトウェア仕様記述の先進技法 Z言語

集合・論理から始まってるし、きれいに仕様記述につながると思ったのだけど、(出版社の)トッパンがつぶれてしまってどこにも引き継がれなかったんだろう。もったいない。
Z言語は、ゼッドと発音するようだ。
で、このZ言語のZは、ZF集合論のZということなんだけど、ZF集合論はツェルメロ-フレンケル集合論なのだから、フレンケルがかわいそうなのではないだろうか。

まあ、ないものねだりをしても仕方がないので、形式仕様記述のほかの本を探してみたんだけど、荒木先生の本は形式的手法が主目的じゃなかったらなんだか難しそう。
プログラム仕様記述論 (IT Text)
この本は近くの本屋になかったのでわからない。
ソフトウェア開発のモデル化技法
他には、Bメソッド、VDMという仕様記述言語の解説書みたいなのしか見あたらなかった。

読むといいよ、というわけではないし、実物を見たこともないんだけど、こういう、形式仕様言語からJavaで記述するまでの本もあって、集合論・論理→形式仕様言語→プログラム言語という流れをきれいにつなぐことができる。
Formal Software Development: From VDM to Java
ところで、Amazonでは400ページと書いてあるのに、目次みると237ページまでしかないのは、なんでだぜ？

形式仕様記述がやりたいわけではないので、もうすこし別の本としてこういう本をみつけた。

ソフトウェア科学基礎―最先端のソフトウェア開発に求められる数理的基礎 (トップエスイー基礎講座)

集合論や論理から出発して、ソフトウェアのモデル化、検証につながる本。簡単な本ではないのだけど、上にあげた「論理学」と「集合とはなにか」を読んだ後なら、あまり読むのに苦労はしないと思う。
時系列の論理モデルについて書いてあるのが興味深い。

同じような目的・同じ金額で読みやすいのはこの本。

形式手法モデル理論アプローチ―情報システム開発の基礎

論理・集合・オートマトン(グラフ)でモデル化し、プログラムに落とし込んでいくという流れが書いてある。酒問屋のシステムみたいな実例も載ってるので、具体的にわかりやすいんじゃないだろうか。
ちなみに、この「酒問屋のシステム」というのは、モデリング技法を検証するためのベンチマークとして使われる問題。「酒屋の倉庫問題」「酒屋の在庫問題」でググると結構出てくる。

実は今回のエントリを書くために本を調べたり実際に見てみたりしたんだけど、本当にプログラムを書くことに論理と集合論が直接かかわっていることを実感した。
ぼくはオブジェクト指向とかあんまり興味がなくてよくわからないし、個々のオブジェクト指向技法には適用できるところとできないところがあると思っている。集合論や論理は普遍的なもので、プログラムを書く上ではいつでもどこでも重要になると言えるし、集合論や論理を押さえておけば、オブジェクト指向だったりモデリング技法だったり検証技法が、集合論や論理に何を付け加えて何を狙っているかがわかりやすくなると思う。基礎になる集合論や論理との差分を勉強すればいいだけなので、楽だろうしね。

さて、形式仕様記述に触れたんだから、プログラムの書き方の本としてはプログラミング言語の本にも触れねばなりますまい。ぼくはプログラミング言語は苦手なので、参考になるかどうかはわからないけど、70ページくらいにシオリが挟まったままのこの本をちゃんと読もうかと思ってる。

コンピュータプログラミングの概念・技法・モデル (IT Architects' Archiveクラシックモダン・コンピューティング)

並列(Parallel)と平行(concurrent)が逆に訳されているという話もあるので、そのあたりは注意が必要らしい。
CTM/CTMCP/ガウディ本で気になった訳語その２: ホットコーナー
この本が読み進んでないのは分厚くて持ち運べないというのがあるんだけど、自分で3分冊にするという勇気もなく。分解するべきかな。
CTMと呼ぶらしい。ガウディ本でも通じるのかな？ガウディ本と言い出したのは中村さんらしい。
http://iiyu.asablo.jp/blog/2006/06/11/401548

で、最後。
プログラムの書き方と、プログラムの動かし方を統合する本が必要になりますよね。
そこで、みんな大好きSICP。もう手元にありますよね。

計算機プログラムの構造と解釈

読み返すといいと思います。
ぼくは、まだ最初のほうしか読んでないので、またちゃんと読みます。*1

あと、形式手法の本を探してるときに、こんな本をみつけた。SICPの代わりにいいかもしれない。

プログラミングの基礎 ((Computer Science Library))

この本も狙ってるところはSICPと同じ方向と言えそう。本もコンパクトだし日本語も読みやすいし微分とかの数学は出てこないし、サンプルのカッコの嵐もないから読みやすそう。といっても言語はOCamlだけど。SICP1冊分の金額で、2冊買えるのもお得。
SICPの3章までに対応する感じなので、SICPの2章くらいで記号微分とか出てきたころに挫折するくらいなら、この本を一冊やったほうがいい。こっちを先にやろうかな。

ということで、ほとんど読んでない本だったのだけど、こんな感じで勉強すれば、プログラムがちゃんと書けるようになるんじゃないかなぁと思っています。

*1:2009/3/20 追記 もう「プログラミングの基礎」を読めばSICPは読まなくていいと思います