プログラム意味論の書き方サンプル： UMiToL - 檜山正幸のキマイラ飼育記 (はてなBlog)

プログラミング言語／プログラム実行の意味論を記述するには、ある程度決まったやり方（定石）があります。それを紹介します。単に書き方のルールを並べるのでは退屈ですから、具体的な例を使って説明します。その例に使う言語の名前がUMiToL（ウミトル） -- "Ultimately Minimum Toy Language"（究極的に最小なオモチャ言語）のアクロニム -- です。

UMiToL言語は超簡単で、UMiToL自体の学習負担はほぼゼロなので、その分、“プログラム意味論の書き方”のほうに集中できると思います。細かい定義を積み重ねて、最終的にUMiToLの意味論は関手として記述されます。

内容：

UMiToL言語の構文
変数の構文
リテラルの構文と意味
演算子記号の解釈
- plus(x, y)の値
- minus(x, y)の値
状態、状態空間、式の意味
コンパイル時のチェック
コンパイラが見る文／式
文のプロファイル
文の意味の定め方
宣言文の意味
代入文の意味
プログラムの圏論的意味
おわりに

UMiToL言語の構文

UMiToLはプログラミング言語なので、まずはその構文を定義しましょう。通常のプログラミング言語同様に、リテラル（値を直接に表す表現）と変数があります。演算子記号はプラス記号とマイナス記号の2つ、文は（変数の）宣言文と代入文と空文。これで全てです。

念のために、構文をBNF〈バッカス／ナウア形式〉記法で定義しておきます。とても短い構文定義です。リテラルと変数については、後で詳しく述べます。EMPTYは、何もないことを示す目印です。

式 ::= リテラル | 変数 | '(' 式 ')' | 式 '+' 式 | 式 '-' 式
宣言文 ::= 'var' 変数
代入文 ::= 変数 ':=' 式
空文 ::= EMPTY
文 ::= 宣言文 | 代入文 | 空文
プログラム ::= 文 | プログラム ';' 文

BNFや正規表現に馴染みがない方は次の記事を読んでみてください。

変数の構文

変数はプログラミング言語において非常にポピュラーな概念です。ほとんどのプログラミング言語は変数を持つでしょう。しかしながら、変数はけっこう複雑で難しい概念で、きちんと理解してない方もいるのではないでしょうか。この記事の主たる目的は「変数とは何か？」に答えることです。

構文上は、変数は単なる名前または記号です。名前または記号であることを強調するときは、変数名（variable name）、変数記号〈variable symbol〉と呼びます。

UMiToLの構文を確定するには、変数名〈変数記号〉全体の集合をハッキリさせます。例えば：

英字（ラテン文字）小文字の集合を変数名の集合とする。

この約束だと、変数名は1文字で、全部で26個の変数しか使えません。もちろん実用性はありませんが、これはこれでハッキリとした定義です。別な定義として：

英字（ラテン文字）小文字の後に、アラビア数字を好きなだけ（0個でもよい）並べた文字列の集合を変数名の集合とする。

これだと、'a', 'a1', 'a2', 'a12' などの名前を変数名に使えます。いま、文字列をシングルクォートで囲んだのは、それが具体的な名前〈記号〉であることを明示するためです。変数を表す変数としては、v, wなどを使います。

念のために注意しておくと、上の段落において出現したvは、英小文字'v'という名前の変数そのものではありません。構文論／意味論では、記号の集合の上を走る変数が登場します。“記号そのもの”と、それらの“記号を表す変数”にたまたま同じ記号が使われることはあります。これが混乱の原因となることがしばしばありますので注意してください。

UMiToLでは、変数構文を決めないでおきます。変数〈変数名 | 変数記号〉の集合は、後からカスタマイズ可能としておきます。Vを変数〈変数名 | 変数記号〉の集合として、Vにより変数構文を確定したUMiToL言語をUMiToL(V)とします。

UMiToLの実際の構文は、変数の集合Vがハッキリしないと確定しません。その意味で、UMiToLはプログラミング言語そのものというより、プログラミング言語フレームワークです。変数の集合というパラメータを渡されて具体的な言語を作り出す装置のようなものです。

変数の集合V |→ プログラミング言語UMiToL(V)

実際の（オモチャでない）プログラミング言語でも、隅々までカッチリ構文を決めないで、後で決める部分を構文的パラメータにしていることもあります。構文的パラメータを具体化すると、その言語ファミリーの特定のバージョン〈具体例 | インスタンス〉が定義できます。

例えば、UMiToLのパラメータである変数集合を、英字小文字の集合だと決めると：

{'a', 'b', ..., 'z'} |→ プログラミング言語UMiToL({'a', 'b', ..., 'z'})

となり、UMiToL言語ファミリーの特定バージョンであるUMiToL({'a', 'b', ..., 'z'})が定義できます。UMiToL({'a', 'b', ..., 'z'})が使いにくいと感じるなら、別な変数集合を準備して、UMiToL言語フレームワーク（具体的UMiToL言語の生成装置）に渡せばいいのです。

リテラルの構文と意味

文字列'12'は、数値十二を表すための記号です。値を直接的に表す記号をリテラル〈literal〉と呼びます。'12'は12を表すリテラルです。

リテラルとそれが表す値を区別することは滅多にありませんし、通常は区別する必要がありません。しかし、プログラム意味論では、（少なくとも一旦は）リテラルと値を区別します。

いま、「リテラルは値を表す」と言いました。ということは、リテラルと値は密接に関連しています。値が何であるかをハッキリさせないとリテラルもハッキリしません。

そこで、値の集合Xを考えます。この集合Xをどう決めるかもカスタマイズ項目、つまり言語フレームワークUMiToLのパラメータです。例えば、X = (10未満の自然数 *1) と決めてもかまいません。言語フレームワークUMiToLのパラメータを2つに増やして、値の集合も指定すると：

{'a', 'b', ..., 'z'}と{0, 1, ..., 9} |→ プログラミング言語UMiToL({'a', 'b', ..., 'z'}, {0, 1, ..., 9})

このケースでは、リテラルは '0', '1', ..., '9' の10個です。シングルクォートにより、値そのものとリテラルを区別しています。値とリテラルは1：1に対応しているとします。今の場合は、0←→'0', 1←→'1', ..., 9←→'9' です。値は、数学的・概念的存在物であり、リテラルは構文的・記号的存在物です。

もう少し詳しく言うと、リテラルを導入するには、次の3つの構成素が必要です。

値の集合 X
リテラルの集合 L
写像 val:L→X

写像valは何でもいいのですが、話を簡単にするために双射〈全単射〉であることを要求しましょう*2。具体例を挙げれば：

値の集合 X = {0, 1, ..., 9}
リテラルの集合 L = {'0', '1', ..., '9'}
写像 val:L→X は、val('0') = 0, val('1') = 1, ..., val('9') = 9,

値の集合Xと写像 val:L→X は、構文論というより、もはや意味論に入り込んでいます。なので、リテラルの導入では、構文論と意味論が混じった話をしています。構文論と意味論が混じらないようにキッチリ分けることも可能ですが、いずれは混ぜちゃう（一緒に考える）ので神経質になっても意味がありません。

リテラルの話を単純化するために、次のような方法をとることがあります。

値の集合Xを決める。
リテラルの集合Lを L = X と決める。
写像 val:L→X は、val = id_X = (Xの恒等写像) と決める。

要するに、値とリテラルをまったく区別しない立場です。こうしても、理論上の不都合は起きないので、値とリテラルを同一視してもかまいません。

演算子記号の解釈

前節の設定を引き継いで：

変数の集合 V = {'a', 'b', ..., 'z'} （26文字）
値の集合 X = {0, 1, ..., 9} （10個の自然数）

とします。また、値とリテラルを同一視します。つまり、いちいち'3'のようにクォートせずに、3はリテラルでもあり値でもあるとします。

さて、プログラミング言語UMiToL（のコア部分）で演算子が決められています。'+'と'-'が演算子記号で、これはカスタマイズの余地がありません（演算子は決め打ち）。プラス記号'+'とマイナス記号'-'を見れば、誰でもそれは足し算と引き算だろうと連想します。それが暗黙の了解、あるいは常識というもんです。

だがしかし、暗黙の了解や常識に頼ることは、プログラム意味論では一番やってはいけない行為です。暗黙の了解や常識は完全に明白ではないので、定義が曖昧になり、その後の議論もイイカゲンでグダグダになります。

実際のところ、UMiToL({'a', 'b', ..., 'z'}, {0, 1, ..., 9})における'+'や'-'は暗黙の了解や常識では決めかねます。'5 + 8'や'2 - 5'はUMiToLの構文で許された式ですが、その意味はハッキリしません。5 + 8 = 13, 2 - 5 = -3 に決っているだろうって？いえ、13も-3もUMiToL({'a', 'b', ..., 'z'}, {0, 1, ..., 9})では扱えない値です。

では、上記の設定（変数の集合 V = {'a', 'b', ..., 'z'}、値の集合 X = {0, 1, ..., 9}）のもとで、演算子記号'+'、'-'の意味を確定しましょう。事前準備として、エラー／未定義を表す特別な値として、ボトムと呼ばれる記号'⊥'を導入して、次のように定義します。

X_⊥ = {0, 1, ..., 9}_⊥ = {0, 1, ..., 9, ⊥}

数学的な関数〈写像〉 plus, minus を定義します。

plus:X_⊥×X_⊥→X_⊥
minus:X_⊥×X_⊥→X_⊥

plus(x, y), minus(x, y)の一覧表を作ってしまいましょう。

plus(x, y)の値

x＼y	0	1	2	3	4	5	6	7	8	9	⊥
0	0	1	2	3	4	5	6	7	8	9	⊥
1	1	2	3	4	5	6	7	8	9	⊥	⊥
2	2	3	4	5	6	7	8	9	⊥	⊥	⊥
3	3	4	5	6	7	8	9	⊥	⊥	⊥	⊥
4	4	5	6	7	8	9	⊥	⊥	⊥	⊥	⊥
5	5	6	7	8	9	⊥	⊥	⊥	⊥	⊥	⊥
6	6	7	8	9	⊥	⊥	⊥	⊥	⊥	⊥	⊥
7	7	8	9	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥
8	8	9	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥
9	9	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥

minus(x, y)の値

x＼y	0	1	2	3	4	5	6	7	8	9	⊥
0	0	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥
1	1	0	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥
2	2	1	0	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥
3	3	2	1	0	⊥	⊥	⊥	⊥	⊥	⊥	⊥
4	4	3	2	1	0	⊥	⊥	⊥	⊥	⊥	⊥
5	5	4	3	2	1	0	⊥	⊥	⊥	⊥	⊥
6	6	5	4	3	2	1	0	⊥	⊥	⊥	⊥
7	7	6	5	4	3	2	1	0	⊥	⊥	⊥
8	8	7	6	5	4	3	2	1	0	⊥	⊥
9	9	8	7	6	5	4	3	2	1	0	⊥
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥

基本は普通の足し算と引き算です。うまく定義できないときは⊥にしてしまう方針です。

plus:X_⊥×X_⊥→X_⊥, minus:X_⊥×X_⊥→X_⊥ をキチンと定義した上で、演算子記号'+'の意味は関数plus、演算子記号'-'の意味は関数minusと定めます。

状態、状態空間、式の意味

UMiToLの実行とは、破壊的代入により変数の値を変えることです。UMiToLは極小な言語ですが、典型的な手続き型言語です。手続き型言語の意味論では、状態と状態空間を使うのが定石ですから、その説明をします。

Vは変数全体の集合です。集合Vは構文的なカスタマイズ項目で、今考えている事例では V = = {'a', 'b', ..., 'z'} でした。26個の変数があり、それ以上の変数を使うことはできません。不便ですが、それはいいとします。必要なら、別なVを採用することもできます。

Vの部分集合をA, Bなどで表します。X_⊥^Aで、AからX_⊥への写像全体の集合を表します（指数記号に慣れてない方は「なんでソコに、足し算、掛け算、累乗の記号を使うのですか？」参照）。Xは変数の値の集合、⊥は未定義を表す記号でしたね。

UMiToLにおける状態空間〈state space〉とは、A（A⊆V）に対するX_⊥^Aという形の集合のことです。状態空間X_⊥^Aの要素を状態点〈state point〉、または単に状態〈state〉と呼びます。A, B⊆V として、写像 f:X_⊥^A→X_⊥^B は2つの状態空間のあいだの写像です。このような写像を状態遷移〈state transition〉と呼びます。状態空間に構造（順序構造、位相構造など）を入れたり、状態遷移として許される写像を制限したりもしますが、今は単なる集合と写像でいいとします。状態、つまり状態空間の要素をρ, τのようなギリシャ文字小文字で表すことにします。

式の意味を定めるには状態が必要です。なぜなら、式は特定の状態においてはじめて値が定まるからです。eが式のとき、状態ρにおける式eの意味を〚e〛_ρ と書きます。白抜きの太いブラケットは、スコット・ブラケット〈Scott brackets〉、表示ブラケット〈denotation brackets〉、セマンティック・ブラケット〈semantic brackets〉、オックスフォード・ブラケット〈Oxford brackets〉など、色々な名前で呼ばれてますが、意味写像を表す記号です。

スコット・ブラケットを使って式の意味を記述*3すると次のようになります。

cがリテラル（c∈X）のときは、〚c〛_ρ = c
vが変数（v∈V）のときは、〚v〛_ρ = ρ(v)
〚(e)〛_ρ = 〚e〛_ρ
〚e + e'〛_ρ = plus(〚e〛_ρ, 〚e'〛_ρ)
〚e - e'〛_ρ = minus(〚e〛_ρ, 〚e'〛_ρ)

補足説明をすると：

値とリテラルを区別しないことにしたので、リテラルcの値はcそのものです*4。リテラルの意味は状態ρと無関係です。
変数の意味は、そのときの状態ρにより決定されます。ρ:A→X_⊥ で、v∈A のときだけ意味を持ちます。v∈A でないときには〚v〛_ρは定義できません。
式を括弧で包んでも意味に影響はありません。
演算子'+'の意味は、写像 plus:X_⊥×X_⊥→X_⊥ で記述されるのでした。前節を参照。
演算子'-'の意味は、写像 minus:X_⊥×X_⊥→X_⊥ で記述されるのでした。前節を参照。

状態は、式が評価されるときの環境を与えるので、評価環境〈evaluation environment〉、または単に環境〈environment〉と呼ばれることもあります。

コンパイル時のチェック

構文的に正しいプログラムは、BNFだけで定義することはできません。UMiToLのような単純な言語でも次の点を考えなくてはなりません。

式のなかに宣言してない変数が出現したらどうするか。
式のなかに初期化（最初の代入）してない変数が出現したらどうするか。
代入文の左辺が宣言してない変数だったらどうするか。
既に宣言済の変数をもう一度宣言したらどうするか。

ここでは、実行の前にUMiToLコンパイラが動くとして、コンパイラが次の動作をするとします。

式のなかに宣言してない変数が出現したらコンパイルエラーとする。
代入文の左辺が宣言してない変数だったらコンパイルエラーとする。

実行できるプログラムは、コンパイラのチェックをパスしているので、実行時に次のことを前提できます。

式のなかに宣言してない変数は出現しない。
代入文の左辺が宣言してない変数であることはない。

しかし、次は保証されません。

式のなかに初期化（最初の代入）してない変数は出現しない。
既に宣言済の変数をもう一度宣言することはない。

言い方を換えると：

式のなかに初期化（最初の代入）してない変数が出現するかもしれない。
既に宣言済の変数をもう一度宣言するかもしれない。

コンパイラが見る文／式

前節で述べたように、UMiToLにはコンパイラがあるとします。コンパイラは構文解析〈パージング〉や実行可能コード生成を行いますが、今は変数の出現チェックに注目しましょう。これは前節で述べた「宣言してない変数の出現はコンパイルエラーにする」機能です。

例として次のUMiToLプログラムを考えます。（このプログラムはコンパイルエラーしません。）

var a;
a := 1;
var b;
b := 3;
a := a + b

コンパイラは、上から順に変数宣言と変数使用を追いかけます。宣言済み変数の集合〈有効な変数の集合〉は、1行ごとに次のように変化します。

{} → {'a'} → {'a'} → {'a', 'b'} → {'a', 'b'}

各行に書いてある文が（変数使用に関して）適正であるかどうかは、そのときの宣言済み変数の集合に依存します。コンパイラは、単に注目している1つの文を見ているのではなく、そのときの宣言済み変数の集合も一緒に見ています。

コンパイラが見ている宣言済み変数の集合を、プログラム・コードに記入してみます。縦棒'|'の左に変数の集合を添えます。

({} | var a);
({'a'} | a := 1);
({'a'} | var b);
({'a', 'b'} | b := 3);
({'a', 'b'} | a := a + b)

(変数の集合 | 文) の形を“コンパイラが見る文”と考えましょう。同様に、(変数の集合 | 式) が“コンパイラが見る式”です。コンパイラが見る文／式が適正〈suitable〉であるとは次のことだとします。

宣言文 (A | var v) はAが何であっても適正
代入文 (A | v := e) が適正である ⇔ ({v}∪Var(e))⊆A
空文 (A |) はAが何であっても適正

ここで、Var(e)は式eに出現する変数の集合で、次のように定義されます。

cがリテラルのとき、Var(c) = {}
vが変数のとき、Var(v) = {v}
Var(eを括弧で包んだ式) = Var(e)
Var(e + e') = Var(e)∪Var(e')
Var(e - e') = Var(e)∪Var(e')

コンパイラが見る式 (A | e) が適正であることはもちろん：

(A | e) が適正 ⇔ Var(e)⊆A

適正という概念は、構文的に整形式〈well-formed〉であることと、意味的に妥当〈valid〉であることの中間的な“正しさ”概念です。

[補足]
プログラムの“正しさ”について補足しておきます。プログラムの構文はBNFのような文法記述言語で記述されます。文法に対して“正しい”とは構文解析木が作れることです。しかし、“整形式＝構文解析木が作れた”だけでは実行時に問題がある（ことが多い）ので、コンパイラは追加のチェックをします。このチェックを通ったプログラムは適正ということにします。

実行時の“正しさ”は妥当性と呼びましょう。例えば、次の条件を満たすとき妥当だとします。

プログラムが停止する。
停止したときの変数の値に未定義（⊥）がない。

UMiToLの場合、そもそも繰り返し構文がないので、すべての適正なプログラムは停止します。しかし、変数の値が未定義でないことは保証されません。例えば、var a という宣言文だけのプログラムは妥当ではありません（宣言されただけでは、変数の値は⊥）。

理想的なコンパイラにおいては、適正なプログラム＝妥当なプログラムです。つまり、コンパイラを通ったプログラムは実行時に問題を起こしません。この理想を実現するのはなかなか難しいですが、邪悪な挙動を制限することにより理想に近づけることはできます。
[/補足]

文のプロファイル

ここから先では、単に文と言ったら、コンパイラが見る文であって適正なものです。Aは変数の集合、つまり A⊆V だとして：

宣言文 (A | var v) Aは何でもよい
代入文 (A | v := e) {v}∪Var(e))⊆A を仮定する
空文 (A |) Aは何でもよい

それぞれの文に対してプロファイル〈profile〉というものを考えます。文のプロファイルは、2つの変数の集合のあいだに矢印を入れた記号です。具体的には：

宣言文 (A | var v) のプロファイルは A→(A∪{v})
代入文 (A | v := e) のプロファイルは A→A
空文 (A |) のプロファイルは A→A

文とそのプロファイルをまとめて書けば：

(A | var v):A→(A∪{v})
(A | v := e):A→A
(A |):A→A

書き方だけ見ると、写像の域・余域〈始域・終域〉と同じですが、とりあえず単なる記号だと思ってください。気持ちの上では次のように解釈します。

(A | var v) の実行前に有効な変数の集合はA、実行後に有効な変数の集合は(A∪{v})
(A | v := e) の実行前に有効な変数の集合はA、実行後に有効な変数の集合はA
(A |) の実行前に有効な変数の集合はA、実行後に有効な変数の集合はA

文の意味の定め方

前節に述べたように、文には変数の集合をくっつけて考えます。そして、文にはそのプロファイルが一意的に決まります。

文の意味もスコット・ブラケットで書くことにします。スコット・ブラケットのなかに書く文では丸括弧を省略します。次のように書きます。

宣言文 (A | var v) の意味は〚A | var v〛
代入文 (A | v := e) の意味は〚A | v := e〛
空文 (A |) の意味は〚A |〛

まず、変数の集合Aに対してスコット・ブラケット〚A〛を次のように定義します。

〚A〛 = X_⊥^A

〚A〛はA上の状態空間です。Aが空集合 $\emptyset$ 、単元集合{v}のときは次のようになります。

〚 $\emptyset$ 〛 $\stackrel{\sim}{=}$ 1
〚{v}〛 $\stackrel{\sim}{=}$ X_⊥

1は特定された単元集合ですが、1 = $\emptyset$ _⊥ = {⊥} と定義しておけばいいでしょう（何でもいいんだけどね）。

実は、文とプロファイルの記法 (A | v := e):A→A などは、スコット・ブラケットと相性が良いように決めたものです。文の意味は、状態空間のあいだの写像なので、集合と写像の意味で次が成立します。

〚A | var v〛:〚A〛→〚A∪{v}〛
〚A | v := e〛:〚A〛→〚A〛
〚A |〛:〚A〛→〚A〛

空文の意味は簡単で、次のように定義できます。

〚A |〛 = id_〚A〛（A上の状態空間の恒等写像）

宣言文と代入文の意味は節を改めて定義します。

宣言文の意味

UMiToLのプログラムは、その実行中に必ず状態を持ちます。実行に伴い状態が変化します。その状態は、変数の集合A（A⊆V）を使って ρ:A→X^⊥ と書けるのでした。ここで、Aは、有効な変数の集合です。有効とは、宣言済みであることです。

宣言済み変数の集合 = 有効な変数の集合 = dom(ρ)

宣言文 (A | var v) は、有効な変数の集合〈宣言済み変数の集合〉Aに、変数vを追加します。追加直後のvの値は⊥（未定義）とします。vが既に宣言済み、つまり v∈A ならば何も起こりません。

以上に述べた宣言文 (A | var v) の効果〈作用 | effect〉は、次のような写像として定式化できます。

X_⊥^A→X_⊥^A∪{v}

前節で定義した記法を使えば：

〚A | var v〛:〚A〛→〚A∪{v}〛

この写像〚A | var v〛を具体的に定義します。まず、v∈A の場合は：

〚A | var v〛 = id_〚A〛 :〚A〛→〚A〛

つまり、変数vが既に宣言済みのときは、A∪{v} = A で、〚A | var v〛は何もしない写像（恒等写像）です。次に、v∈A でない場合： ρ∈〚A〛（〚A〛 = X_⊥A）に対して、〚A | var v〛(ρ) = ρ' と置くと、

w∈A ならば ρ'(w) = ρ(w)
ρ'(v) = ⊥

A上ではρをそのまま、vの値は⊥とした新しい状態ρ'が〚A | var v〛(ρ) です。この場合は〚A〛と〚A∪{v}〛は違う集合なので、〚A | var v〛:〚A〛→〚A∪{v}〛 ρ|→ρ' は異なる状態空間のあいだを飛び移る状態遷移となります。

もしコンパイラが、重複した変数の宣言をチェックするなら、宣言文の意味は常に異なる状態空間のあいだの写像となります。今の前提では重複した宣言文をチェックしてないので、宣言文の意味が恒等写像になることもあります。ここらは大した問題ではありません。

代入文の意味

UMiToLの唯一の実行文は代入文です。

〚A | v := e〛:〚A〛→〚A〛

ρ∈〚A〛に対して、〚A | v := e〛(ρ) を定義しましょう。〚A〛 = X_⊥^A だったので、ρ∈〚A〛とは ρ:A→X_⊥ のことです。次の3つの命題は同じ意味です。

ρ∈〚A〛
ρ∈X_⊥^A
dom(ρ) = A, cod(ρ) = X_⊥

ρ∈〚A〛に対して、〚A | v := e〛(ρ) = ρ' と置くと、

w∈A、w ≠ v ならば、ρ'(w) = ρ(w)
ρ'(v) = 〚e〛_ρ

代入文 (A | v := e) の作用〈効果 | effect〉は、変数vの値を式eを評価した結果で置き換えること（その他の変数の値は変えない）です。

〚e〛_ρは既に定義した式の意味ですが、式eに変数集合Aを添えたほうが明確・正確です。また、下付きのρを丸括弧に入れても同じことですから：

〚A | e〛_ρ = 〚A | e〛(ρ) （ρ∈〚A〛）

〚A | e〛は、〚A〛の要素（状態）ρを引数にしてX_⊥の値を返すので、写像〚A | e〛:〚A〛→X_⊥ です。ところで、X_⊥ $\stackrel{\sim}{=}$ 〚単元集合〛なので、〚A | e〛:〚A〛→〚単元集合〛とみなせます。この形から、変数集合Aを添えた式 (A | e) のプロファイルは、r∈V を選んで次のように決めてかまいません。

(A | e):A→{r}

ハードウェアで例えれば、rは式の評価値を入れる役割のレジスタです。

プログラムの圏論的意味

いままでに述べた話を圏論を使って整理しましょう。プログラム意味論を圏論なしで行うのは辛いものがあるので、圏論の基礎知識は仮定します。圏論に馴染みがない方は、次の記事からのリンクを辿ってみてください。

2017年圏論に関する参考文献の案内（無料オンライン版含む）

いまここで必要なのは圏の定義だけなので、次の記事を読むだけで十分かも知れません。

はじめての圏論その第1歩：しりとりの圏

今回は、集合圏Setをベースにします。より精密な議論をするには、順序集合の圏Ordや位相空間の圏Topを使います。部分写像の圏Partialを使うと⊥（ボトム）の扱いが少しスマートになります。

変数の集合Vと値の集合X、それと写像 plus, minus:X_⊥×X_⊥→X_⊥ を固定します。以下では、plus, minusも“込み”でXと書くことにします（記号の乱用 X = (X, plus, minus)*5）。このセッティングにより、UMiToL言語ファミリーの特定インスタンスUMiToL(V, X)を考えます。具体的な事例としては、V = {'a', 'b', ..., 'z'}, X = {0, 1, ..., 9}。

さて、UMiToL(V, X)のプログラムの全体を圏として定義します。その圏をPorgとしましょう。圏Progは以下の通り。

Obj(Prog) = |Prog| = Pow(V) （Pow(V)はVのベキ集合）
Mor(Prog) = (適正な全ての文)
dom, cod, idはすぐ下に記述
圏の結合〈composition〉もすぐ下に記述

dom, codは文の種類ごとに定義します。

宣言文 dom(A | var v) = A, cod(A | var v) = A∪{v}
代入文 dom(A | v := e) = A, cod(A | v := e) = A
空文 dom(A |) = A, cod(A |) = A

idは、

id_A = (A |) （空文）

結合の定義は次のようです。

(A | α);(B | β) = (A | α;β)

これにはちょっと説明が必要でしょう。

左辺の';'は、圏の結合を表す記号（図式順結合記号）です。
αとβは、BNFで定義した文を表します。
右辺の';'は、2つの文を構文的に繋ぐときに使う分離子記号〈セパレータ〉です。

圏の演算記号と文の分離子に同じセミコロンが使われているので紛らわしいのですが、一方で、これは便利な記法でもあります。

Progにおける結合律と単位律は簡単そうですが、実際は「文が同じ」であることを正確に定義しないといけなくて、けっこう難しいです。今回は割愛します。

先に導入したプロファイル (A| v := e):A→A などは、実は圏Progにおける射を表す記法だったのです。Progが圏であることが分かれば、スコット・ブラケットで表された意味写像が関手であることも分かります。

〚-〛は、プログラムの圏Progから集合圏Setへの関手なのです。次が成立します。

対象 A∈|Prog| に対して、〚A〛は集合、つまりSetの対象である。
射 (A | α):A→B in Prog に対して、〚A | α〛は写像、つまりSetの射である。
dom(〚A | α〛) = 〚dom(A | α)〛, cod(〚A | α〛) = 〚cod(A | α)〛
id_〚A〛 = 〚id_A〛 = 〚A |〛
〚(A | α);(B | β)〛 = 〚A | α〛;〚B | β〛（右辺の';'は写像の結合）

UMiToLの意味論は、関手〚-〛:Prog→Set により完全に記述できます。

おわりに

超簡単な手続き型言語UMiToLに対して、圏論的意味論を与えました。UMiToLの実行文は代入文だけであり、代入文は変数の値を変えるものです。したがって、UMiToLの意味論は変数の意味論だと言ってもいいでしょう。

現在では、表示的意味論〈denotational semantics〉と操作的意味論〈operational semantics〉の境界は曖昧です。UMiToLの意味論は、集合と写像（集合圏）を意味とするので表示的意味論のようではあります。しかし、代入文の意味は状態遷移系であり、一種の抽象機械を考えていることになり操作的ともいえます。もはや、意味論の分類を云々してもしょうがない気がします。計算現象をキチンと写し取れるモデルが作れればそれでいいのです。

いずれにしても、手続き型言語の意味論には状態概念が必要でしょう。状態は純関数的ではないので嫌う人もいますが、そういう拘りはナンセンスに思えます。仮にプログラミング言語に状態も副作用もなくても、ファイルシステムやデータベースを扱えば状態が入り込んでしまいます。ファイルシステムもデータベースも一切触らない、というのは現実性がないでしょう。

UMiToLは状態と副作用（実は主作用）を扱う最も簡単なモデルですが、その意味論はそれなりに複雑な構造を持ちます。構文的パラメータである変数集合Vや、意味的パラメータである値の集合X（plus, minusを含む）などのメカニズムをチャンと分析すると、もっと複雑な構造（たぶんインスティチューション）が現れます。また、条件分岐や繰り返しの制御構造を入れれば、それも複雑さにつながります。

オモチャでない実用的プログラミング言語の意味論が随分と複雑そうなことは想像できるでしょう。しかし、その複雑さのなかに面白くて深い構造が潜んでいると期待もできるのです。

*1:0は自然数に含めます。

*2:valが何でもいいときは、違うリテラルが同じ値を指すことがあり、また、リテラルでは表現できない値も存在します。リテラルで表現できなくても、リテラルから作った式で表現できれば、値を指すことができます。式でも表現できない値があっても別にかまいません。

*3:厳密に言えば、文字列／トークン列としての式に意味を定めるのではなくて、構文解析後の構文解析木に対して意味を定めます。UMiToLの場合、構文解析は非常に簡単なので、構文解析木を引き合いに出す必要はないでしょう。

*4:⊥を表すリテラルはないことに注意してください。

*5:Xにplus, minusを加えた構造は、特に演算法則を要求していません。何の法則性もない二項演算を持つ代数系をマグマと呼びます。(X, plus, minus)は、二項演算を2つ持つマグマと言えます。