トレース意味論とゲーム意味論

トレース意味論とは、プログラムの意味を「実行したときに起きるイベントの列」として表現したものです。イベントとして何を考えるかは目的次第ですが、例えば「入出力」や「関数へ引数を渡す」などといったものが考えられます。以下でポイントになるのは、トレースは「列」だということです。トレースが持っている情報はイベント発生の時間的前後関係だけであって、因果関係などのイベント同士の依存関係は表現されません。

ゲーム意味論*1の基本的な考察対象は「プレイ」と「相互作用列（interaction sequence）」と呼ばれるものですが、これは本質的にはトレースにイベント同士の依存関係の情報が加わったものです。

トレース意味論の方が素朴で直観的に分かりやすい面もあると思うのですが、僕はゲーム意味論の方が好きです。僕がこうした意味論を使うのはプログラム検証のための性質を定義する場面になるのですが、トレース意味論は情報が多すぎて、定義した性質が実は検証できないという事態に陥りやすいと思うからです。一方ゲーム意味論では、イベント列から「使っても良い情報」を切り出す方法が確立されています。「View」と呼ばれる概念がそれです。「View」しか見られないというのは、はっきり言って不便なのですが、それと引き換えに「View」だけから定義できる性質はプログラムの構文との相性が良いです。

こういった理由で、僕にはトレース意味論は素朴すぎるように感じられます。もちろん用途次第ではトレース意味論の方が適している場合もあるはずですが。

*1:ここではHO/N styleのゲーム意味論を考えています。AJM styleのものは趣が異なります。