操作的意味論 vs 表示的意味論

http://d.hatena.ne.jp/ranha/20090615
(via http://d.hatena.ne.jp/yad-EL/20090615/p2)

「諸君らの愛した表示的意味論(R5RS)は死んだ。なぜだ?」

う、これは私も(というか私ごときでは)迂闊に発言できないテーマです…。Scheme (R5RS → R6RS)に固有の事情は知らないので、(もしあれば)メーリングリストなどでの議論を検索したほうが詳しいかもしれません。追記:R5RSの操作的意味論と、その表示的意味論に対するメリットに関しては論文があるようです。

迂闊に発言すると、(一般論としては)「操作的意味論のほうが理論が簡単だから」だと思います。要するにプログラムの「意味」というより「動作」を状態遷移(式の書き換え)で表しているだけなので…。歴史的には、操作的意味論も(仮想機械やインタプリタによる定義から)項の書き換えによる定義に洗練されていって、特にScheme的には継続を文脈(context)として(継続渡し形式を使わないで)ダイレクトに表せたり、関数引数の評価順序の非決定性を簡単に表現できることが大きかった…のかもしれません。追記:上述の論文によると、この推測でほぼアタリのようです。

表示的意味論は、順序集合上の連続関数とかカテゴリーの射とか、(教科書的定義ですが)プログラムを「数学的対象に対応」させるので、その数学的対象の意味がわかれば、より深い理解が可能になるのだと思います。ただ、Schemeλ計算はまだ良いのですが、より複雑な言語(π計算とか)になると、より高度な数学的理論が必要になったり、うまく対応する数学的対象が見つかっていなかったりするようです。…ボロが出ていたら突っ込んでください>詳しい方