情報数学講座 (第7巻)

著者 : 横内寛文

• 共立出版 (1994年6月7日発売)

感想・レビュー・書評

[bugyoさんの感想 · 2015年4月29日]

形無しラムダ計算、型付きラムダ計算、表示的意味論、操作的意味論、実際の関数型言語への意味付けと一通り解説する。後半は圏論を導入し、領域方程式の方法で、ラムダ計算に意味を与える。積み上げる形式なので、続けて読んだ方が良い、間を空けると記法など忘れる。

[exphenomenologueさんの感想 · 2014年8月28日]

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

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

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