ずーっと前から読みたかったけど絶版になってしまって読めなかった本が復刊。
プログラム意味論 (情報数学講座)
横内 寛文
最初はラムダ計算とコンビネータ理論から入り、3章で領域理論について解説する。posetの取り扱いとか最小不動点定理とかまともに学んだことなかったので、すごくためになった。
そして型付きラムダ計算を元に関数型言語の操作的意味論と表示的意味論の比較。正格性の話にもページを割いている。この辺もあまり区別できずにいたのでありがたい解説。
5章は圏論で、随伴は出てこないけど必要な話はだいたい入ってる印象。6章は逆極限法で、型無しラムダ計算の意味論に必要な同型である X≃X^X を満たすXを調べる。圏論で一般化して始代数の存在の話とか最小不動点定理の言い換えとか、ここも非常に面白い内容。
最後の章で、CCC(Cartesian Closed Category)で型無しλ計算の意味論を構成する。この辺はそのままCLTTに読み繋げたいところ。この結果を元にSKIとは違うコンビネータ理論を構成するが、この辺は心が折れたので読み流した。
昔見かけたときは圏論が載っているということで興味を持ったのだけど、不動点の話とか領域理論とか大変楽しく読めてよかった。CCCでの形式化もCLTT読む前の準備運動になるのかなあと思ったので、表示的意味論に興味がある人は買って損はない内容かなと思う。
