ラムダ計算の勉強のしかた、プログラム意味論

先日のエントリで手続きを記述するという側面と、式を記述するという2つの側面があるということを書きました。
プログラムの理論とはなにか

そして、手続きの性質として代表的な、アルゴリズムについての勉強のしかたについてまとめてみました。
アルゴリズムの勉強のしかた

そこで、今回は、式を記述するという側面の勉強のしかたと、あとこの分野は自分でもまだ全然勉強してなかったので、これからどういう本を読もうと思っているかをまとめてみます。

プログラム意味論

プログラムは必ずプログラム言語、少なくとも記号で記述します。*1
そこで、プログラムの勉強という点では、どのように動くかというアルゴリズムの勉強だけではなく、どのように書けるか、書いたものにどのような性質があるのかということも知る必要があります。

例えば、2005年あたりからRubyのような動的型付け言語が流行りだし、Javaなどの静的型付けの言語との比較が行われ、昨年2010年あたりからScalaのような強力な型推論を使うと静的型付け言語でも動的型付け言語のような記述が行えることが認知されてきました。ここで、言語の型システムというのが注目されるようになってきている気がします。
この型システムのような、プログラムをどのように書けるかという観点での勉強も必要になるということです。

こういった分野の基礎になるのがプログラム意味論のようです。
プログラム意味論はマイナーです。アルゴリズムや計算理論が書名についた本はたくさんありますが、プログラム意味論の本はそれがそのまま書名になった唯一の本が絶版という状況です。
プログラム意味論 (情報数学講座)

それでも型システムのように、プログラム意味論の方面も徐々に注目されている気がします。
なぜ今までプログラム意味論は注目されず、いま注目されはじめてきたかというと、プログラムの意味を扱う余裕がでてきたこと、プログラムの作成にプログラムの記述能力の助けが必要になってきたことがあるのではないかと思います。

というのも、これまでのコンピュータはプログラムの処理を行うのが手一杯で、プログラムの意味まで扱ってられなかったのです。スクリプト言語の実行には時間がかかります。Scalaは推論が多くコンパイルには時間がかかります。それがCPUや最適化、コンパイラの技術の進化で実用になってきました。
また、並列実行のプログラムが重要になると、動かしてから動作を検証することが難しくなり、プログラム言語での記述によって動作を保証するということが大事になっているように思います。

あと、どういう記号で書くとどういう計算量になるかが結構対応するという記述的計算量の話もおもしろそうです。
Logic ∩ CS | d.y.d.

ということで、プログラム意味論を勉強する必要があるなと思っているのですが、そのとっかかりとしてラムダ計算は必要なので、まずはラムダ計算を勉強するための本をまとめてみます。

ラムダ計算の勉強の準備

いきなり「論理と計算のしくみ」を読んでもいいのですが、命題論理・述語論理の部分を読みやすい入門書で勉強しておくほうが楽なので、まずは論理学の勉強をするのをおすすめします。
いつも、論理学を勉強しましょうという文脈では入門!論理学 (中公新書)を勧めるのですが、ラムダ計算への過程としての論理学の入門ではちゃんと記号で勉強しておく必要があるので、この本が一番よいと思います。

論理学

ラムダ計算とかプログラム意味論とか勉強しなくても、論理学は勉強しておくべきです。

手も動かしておきましょう

やはり、勉強するときはプログラムを書いて確認するほうが楽だし、せめてプログラムコードで想像できるようにしておくほうがいいです。
そこで、この本です。
今回のエントリは、プログラムの「式を記述する」という側面を勉強しましょうという趣旨なのですが、式は関数で記述するのであり、つまり関数型言語が「式を記述する」というアプローチでのプログラム言語なので、関数型言語を知っておく必要があるということです。

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

OCamlという言語を使っていて、OCamlを実用で使うシチュエーションはあまりないので、関数型言語をすでに使っている場合には読まなくていいかなと思います。
ただ、あとの「プログラミング言語の基礎概念」でもOCamlが使われているし、本の構成としてもつながりやすいので、おさらいとして目を通すのもいいと思います。
あと、プログラム理論の説明にOCamlが使われていることが多いという空気をなんとなく感じるので、一応OCamlは やっておくほうが教養としてよさそうです。

ラムダ計算の本

さて、ラムダ計算の勉強です。
ぼくの知ってる中では、この本が一番よいです。
ラムダ計算は、だいたい集合論→命題論理→一階述語論理→高階述語論理→ラムダ計算という順に発展してきたものなのだと思うのですが、この順番自体が「論理と計算のしくみ」に載っていて、こういう順番にかかれています。

論理と計算のしくみ

この本に書かれている式を、プログラム言語で書いてみて、実際に動かしてみるといいと思います。

たとえばぼくはこういう感じでGroovyで書いています。
おとうさん、ぼくにもYコンビネータがわかりましたよ！
Javaでも書けなくはないのですが、Javaにはラムダ構文がなく必要以上に煩雑なコードになってしまうので、Javaに近いGroovyで記述しています。

π計算

ラムダ計算の並行版としてパイ計算というのがあります。
並行環境でのプログラムを記述することはどんどん重要になってくるので、パイ計算も大事になる気がします。
で、それを勉強しようと思っているのですが、日本語での本がみあたりません。英語だとこの本があって、以前うっかりポチって手元にあるので、いまの仕事が一段落したら読もうかと思ってます。

Communicating and Mobile Systems: The Pi-Calculus

ブクマコメントで解説を教えてもらいました。
http://kaiya.cs.shinshu-u.ac.jp/pub/pi/

他に、こういう本をkoichikさんから教えてもらいました。
The Pi-Calculus: A Theory of Mobile Processes
A Distributed Pi-Calculus

プログラム意味論へ

ほかに、こういう本を読もうと思っているものをまとめてみます。

ラムダ計算からプログラム言語に近づいていくための本も探さないとなーと思っていたら、昨日よさげな本をみつけました。
パターンマッチング、型システム、型推論までコンパクトに書かれています。いま読んでる本が終わったら次に読む予定。

プログラミング言語の基礎概念 ((ライブラリ情報学コア・テキスト))

あと、やはりこの本は手元に置いておいたほうがよさそう。大きめの本屋の在庫にあったりするんだろうか。

プログラム意味論 (情報数学講座)

と思ったら復刊ドットコムで扱っているとコメントで教えていただきました。
『プログラム意味論（情報数学講座）（横内寛文）』 販売ページ | 絶版・レア本を皆さまの投票で復刻 復刊ドットコム

それと、やっぱ圏論もやっておく必要がありそう。この本をうっかりポチって手元にあるので、がんばって読もうかと思っています。

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

圏論の本では、層・圏・トポス―現代的集合像を求めてのほうが人気がありそうですが。

あと、このブログで取り上げられてた本がおもしろそうです。*2
http://www.funclang.net/cruel/?p=218

記号と再帰: 記号論の形式・プログラムの必然

ブログの締めの「目の前にあるソースコードのコピーではなく、数学からアイディアを借りましょう」が刺さります。

最後に、プログラム言語の理論としては、この本もあてはまるのだと思います。これはなぜかTSUTAYAの本屋に売ってたので買ってかえってて、20ページくらい読んで止まってます。全部で1000ページ近くあるのだけど。

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

いろいろ勉強することがたくさんありそうです。

追記(10/1)
プログラム言語の理論だとこの本が定番みたいですね。

Types and Programming Languages (The MIT Press)

Types and Programming Languages
2018/4/5 訳本も出てます
型システム入門 −プログラミング言語と型の理論−

*1:記述しているからにはその記述のための要素があって、その要素のことを記号というので、これはトートロジーなのだけど

*2:ブクマコメントにバカ本とあったけど、取り上げてたブログをひととおり見る限り、一部に議論の甘い部分はありそうだけど、よい評価のようだ