北海道苫小牧市出身の初老PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

「論理と計算のしくみ」が大変ためになった

読み終わったので感想です。他の方々からも良書だ良書だと勧められましたが、結論から言うとやはり買いです。

論理と計算のしくみ
萩谷 昌己 西崎 真也
4000061917

前半は論理学から話を初めてゲーデル不完全性定理までを論じます。後半はλ計算型理論についての内容です。カリー・ハワード対応がわからなくてもいいのであれば、後半のλ計算の部分だけ読むこともできます。

読み切れば、例えば、本物のプログラマはHaskellを使うの連載に出てくる次のような単語の意味は理解できるようになるでしょう。

  • reduction
  • call-by-name
  • call-by-value
  • Weak Head Normal Form
  • 型推論
  • 依存型
  • 多相型

他にも以下のような聞いたことあるけどなんだろこれって知識が補完されます。

なお、話の中身はプログラミングというよりは数学です。難解なものを除き、事実だけでなく証明まできっちりと述べています。集合論について基礎的なことは1章にまとまっていますが、大学の教養部で身につける程度の集合論の知識はあったほうが読みやすいでしょう。自信がない方は読書会を主催するなどして、そのような素養のある方を騙して巻き込みに参加して頂き、レクチャーしてもらえば安心して読み進められると思います。

余談:この本に載ってないもの