学部生向けなのでさくさく読めてよい。
カバーしているのは操作的意味論*1で、序盤から中盤にかけて単純な自然数の和積算の意味論をベースに徐々に盛りつけてMLライクな言語の意味論を作り上げる。letや関数、再帰関数の意味をどう与えることができるのかはこの辺りを読めば分かる。
後半これに型をつけていくのだが、型を仕様記述言語として説明しているのは面白かった。型のない言語にそれとは別で型付けの意味を与えたときに、「評価できない式(実行時エラーが出る)⊂型付けできない式」ということを述べている。つまり、型付けできればエラーは起きない、と。そして、型付けの仕方を工夫することでこれらの集合がイコールになるよう近づけて仕様記述言語としての精度を上げることができる、という文脈で多相型を持ってきている。
最後は型推論を解説しているが、こちらもアルゴリズムをなるべく平易にさっくり解説している。全体的にあっさり目な印象もあるけれど、話の流れに飛躍がなく重要なポイントも押さえているので、操作的意味論ってどういうものなんだろうって人は読んでみるといいと思う。
【9/1追記】忘れてたけど帰納法周りをなんとなくではなくきちんと解説しているので、そこも他の本にないすごく良い部分だと思う。特に構造と導出の帰納法が自分の中ではごっちゃになっていたので、そこが整理できたのは嬉しい。
*1:表示的意味論と操作的意味論の違いはm-hiyamaさんのエントリがわかりやすい
