このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

操作的意味論と、不純な表示的意味論

雑感を記すだけですが:

1年ほど前に、「なぜ僕は操作的意味論に傾いたか」という記事を書いたことがあります。もともと、ナントカ意味論という分類には拘ってはいないのですが、できることなら表示的(denotational)にやりたいな、という希望はあります。ですが、「表示的」を狭義に考えると「どうも無理があるよなー」というのが僕の感想です。

集合と関数(写像)という枠組みでプログラムの意味を記述するのはなかなかうまくいきません。無限走行、部分性に関しては、ボトム、順序、位相といった構造を導入してきれいにマトメることができます。非決定性も、ベキ集合モナド(とその変種)や関係圏を使えば定式化できます。しかし、並列プログラムやリアクティブシステムになると辛い感じがします。時間の概念が陽に絡んでくると、表示的(外延的)な記述が難しくなります。

そもそも「表示的」って何なんだ?ってハナシがあるのですが、その前に「表示的ではない」とされる操作的意味論に触れておきます。操作的意味論では、記号的な抽象機械を設計して、その抽象機械の動作によってプログラムの意味を説明します。「機械の動きを、別な機械の動きで説明するだけ」という批判もありますが、「説明する側の機械」が「説明される側の機械」より解析しやすいなら十分意義があると思います。

抽象機械の抽象度はさまざまですが、いずれにしても「実行のステップ」という概念があります。計算状況がステップごとに移り変わるわけです。したがって、抽象機械は書き換え系(rewriting system)、状態遷移系といえます。入力と出力との関係がいきなり記述されるのではなくて、初期状態から終状態に至る経路(軌道、軌跡)として計算手順が示されます。計算手順を捨象してない点において「表示的ではない」とされるのでしょう。

抽象機械のステップを考えることは離散時間を入れていることです。おそらく、「表示的」とは時間概念を陽に入れず、入れるにしても時間軸全体を俯瞰して(空間化して)構造に取り入れるのでしょう。一方の「操作的」は、時間に沿って遂行される手順が主題となります。こんな分類でいいのかどうか自信はないのですが、僕はそんなふうに捉えています。

さて、冒頭の「どうも無理があるよなー」とは、ステップ/時間を陽に扱わない方法が苦しい、ということです。ステップ/時間を考慮すると、確かに手順中心で「操作的」となります。しかし、ステップ/時間を入れたら表示(denotation)を諦めるべきかというと、そうでもないと思っています。表示(モデル)として、前もって時間概念を含む対象物を取ればいいのです。

と、こう言うと単に言葉の遊びみたいですが、「モデル=圏」と考えると、時間概念を含むか含まないかは、モデル圏*1の特性として記述できると思われます。典型的な例は共有メモリにアクセスする2つのプロセスです。アクセスの順序、つまりタイミングにより結果が変わります。タイミングの影響は、モノイド積の交替性(interchangeability)を壊す形で現れます。つまり、時間概念を取り入れるひとつの(あくまで「ひとつ」の)方法は、非交替的な積を持つ圏を考えることです。

交替的な積と非交替的な積は分離しているわけではなくて、非交替的な積を持つ圏のなかに交替的な部分圏が入り込んでいます。交替的な部分圏(純部分圏や中心)だけを考えれば、本来の表示的意味論が展開できます。つまり、「表示的」を「積が交替的=タイミングの影響がない」と捉えれば、非表示的なモデル内に表示的モデルも入り込んでいることになります。

非交替的な積を持つ圏では、関数適用やタプリングのような計算は成立しません。当面我々が使える計算手法は抽象機械のステップを追いかけることです。抽象機械が十分に抽象的に洗練されれば、それはラムダ計算やシーケント計算に匹敵するモニになるかもしれません。なるといいな。

関連記事:

*1:ホモトピーにモデル圏という概念がありますが、それとは関係ありません。計算モデルとなる圏という意味です。