今日の昼前に投稿した記事「評価シーケントの論理計算と操作的意味論」において、操作的意味論に基づいた意味記述方式を提案してます。これは、CatyScript2.0を記述する目的で考えたのですが、なぜ操作的意味論を採用したかを書いておきます。
CatyScriptの意味を表示的（denotational）に記述することも出来なくはないでしょう。しかし、簡単な仮想機械を想定して操作的（operational）に書くほうが次の点で有利なように感じました。
- 処理系実装の方針を立てやすい。
- コンパイル方式のヒントになる。
- スコープ／可視性の定義が容易。
- 細かい振る舞いまで記述できる。
細かい振る舞いが書けるということは、煩雑で抽象度が低いという欠点でもあります。しかし、表示的には書きにくいことがあるとき、自然言語で注記するくらいなら操作的に書いたほうがマシだと思います。
操作的な記述をシーケント計算と組み合わせると、次のメリットがあるように思います。
- 評価方式が正しいことを形式的に証明できる（あくまで原理的なハナシですが）。
- 推論図と証明図を使って型推論が出来るかもしれない（確証はありません）。
それと、評価シーケントの証明図と実際の評価手続きとの対応関係が、LKとNKとの関係に似てる気がします。ある種のカリー／ハワード対応があるんじゃないのかなぁ？ あったら面白いですね。
もちろん、表示的意味論がダメとか嫌いとかでは全然ないので、デカルト半環圏ベースの表示的意味論も並行的に使います！
