佐藤　雅彦，桜井　貴文：プログラムの基礎理論

概要

プログラムの性質を検証するにはどうしたらいいか。これが本書の出発点である。 より定式化したことばでいえば、ある論理体系のなかで、プログラムが正しいかどうかを証明するにはどうしたらよいか。 この証明を遂行するためには、計算とは何か、推論とは何かということを形式化することから始めないといけない。 そして続けて、式に対する操作を定義する必要がある。 そのあとで、ある関数型プログラミング言語と論理体系を導入して、プログラムの性質が厳密に論じられることを示す。

感想

筒井康隆

p.2 に次のように書かれていて驚いた。たとえば，「筒井康隆」という漢字（記号）列はとある著名な作家（対象）の名前であり， 「UNIX」という英字（記号）列は AT&T が開発してライセンスしているとある有名なオペレーティングシステム（対象）の名前である． ここで筒井康隆がわかっても後の同書の理解には関係がないのがつらい。

それでもあるとすれば、p.4 で次のように言及されていることである。 ところで，一つの表記体系が一つの対象を表現しているとは限らない． 「筒井康隆」という記号列が「文学部唯野教授」の著者以外の人物（つまり同姓同名の他人）を指していることがありえたり， 「UNIX」という記号列がとあるオーディオ機器を指していることがあるように、（後略） 冒頭に「筒井康隆」が出てきたので、何か最後にオチがあるのかと期待したが、なかった。

なお、「UNIX」という名前の美容院があることを、数年前知った。

記号

正直いって難しい。ただ、何もできないと思われるのは癪だから、ちょっとだけ記号の書き方を練習しておく。

p.49 で、項 `a` に対して M 式 〚`a`〛を以下のように定めるとある。 〚〛は、たまたま「かっこ」と打って変換したら出てきたのだが、変換時に「環境依存」と表示されたので、どんな Web のページでも表示できるかどうか不安である。 TeX ならばそれぞれ \lBrack と \rBrack とするか、\double[ と \double] とするかなのだろうが、どちらも MathJax では出てこない。 したがって、自分で勝手に記号を追加できる ASCIIMathML.js を使うことにした。[|a|] と打つと `[|a|]` と表記される。

図に乗ってもう一つ。p.41 の練習問題２の 2.3 では、2つのリスト `l, m` の非重複和 `l u+ m` を以下のように定義する． とある。 この ⊎ はなかなか出ないだろうな。

数式

数式表示には、ASCIIMathMLを使っている。

まりんきょ学問所 ＞ コンピュータの部屋 ＞ コンピュータの本 ＞ 佐藤　雅彦，桜井　貴文：プログラムの基礎理論