読み終わったので感想です。他の方々からも良書だ、良書だと勧められましたが、結論から言うとやはり買いです。
論理と計算のしくみ
萩谷 昌己 西崎 真也
前半は論理学から話を初めてゲーデルの不完全性定理までを論じます。後半はλ計算と型理論についての内容です。カリー・ハワード対応がわからなくてもいいのであれば、後半のλ計算の部分だけ読むこともできます。
読み切れば、例えば、本物のプログラマはHaskellを使うの連載に出てくる次のような単語の意味は理解できるようになるでしょう。
- reduction
- call-by-name
- call-by-value
- Weak Head Normal Form
- 型推論
- 依存型
- 多相型
他にも以下のような聞いたことあるけどなんだろこれって知識が補完されます。
- 命題論理、述語論理、様相論理、時相論理、直観論理
- ゲーデルの不完全性定理
- チューリングマシンの停止性問題
- λ計算、α簡約、β簡約、η簡約
- Yコンビネータ
- 型付きλ計算、型理論
- シーケント計算、自然演繹
- カリー-ハワードの対応
なお、話の中身はプログラミングというよりは数学です。難解なものを除き、事実だけでなく証明まできっちりと述べています。集合論について基礎的なことは1章にまとまっていますが、大学の教養部で身につける程度の集合論の知識はあったほうが読みやすいでしょう。自信がない方は読書会を主催するなどして、そのような素養のある方を騙して巻き込みに参加して頂き、レクチャーしてもらえば安心して読み進められると思います。
