横内寛文『プログラム意味論』

この分野の入門書として名高い本だが、これはとても面白い。昔（１０年くらい前）にいくつかの章を読んだが、今回は通読してみた。λ計算とその意味論を扱った本。λ計算の構文論（型なしも型付きも）から始まり、その意味論として操作的意味論と表示的意味論を導入。表示的意味論ではCPOを使って、まず型付きλ計算のモデルを提示する。λ計算を拡張したPCFで自然数論の初めの方。圏論をメインに導入して、領域方程式の理論でCPOでの構成と圏論での構成を述べる。最後に、λモデル、λ代数、カテゴリカル・コンビネータを軽く扱って終わる。

だいたい違和感なく読めて行ったのだが、定義7.2.4(p.228)以降のcccとλ代数の関係を扱うあたりからきつかった。総じて説明は上手で、直観的なイメージの与え方もよい。CPOや圏論の道具立ても導入するものが限られていて、無用な混乱を生まないようになっている。以前D∞はCPOで学んだことがあったので、これを圏論で構成し、必要十分な条件を求めていく逆極限法の話を記した領域方程式のところが一番面白かった。

それにしても対象とその上の関数空間が同型になるという型なしλ計算のモデルは面白い。とても楽しかった。GunterかMitchellでも本棚から引っ張り出してくるかな。