「ホーア論理とシーケント計算を混ぜたような意味記述構文」で述べた記述言語はマー悪くない感じです。ですが、使いやすい記述言語にするにはまだ拡張と改善が必要です。記述言語も記述される対象も、より精密にしたいですね。
気が付いたところを早速に拡張・改善します。
内容：
評価シーケント
現状のシーケントの形式は Σ;x{E} → Γ;y です。もともとがホーア論理から出発したので、矢印「→」を取り除くと Σ;x{E}Γ;y というトリプルになります。しかし、もうトリプル形式にはこだわらないでシーケントとして扱うことにします。シーケントの左右が異なる形なのは扱いにくいので、左右とも同じ形式とします。その形は、Σ;x{E1, E2, ...} です。
- Σは束縛の列 σ1, σ2, ..., σn です。それぞれの束縛はスコープオブジェクトとみなされ、束縛の列はスコープのスタックまたはチェーンを意味します。
- x は値（リテラル）です。式に対する入力ですが、それ以前の計算の結果でもあるので、「カレントの値」とみなすのがふさわしいでしょう。
- {E1, E2, ...} は式（項）の列。左から順に評価されることを想定しています。
Σ;x{E1, E2, ...} は計算の状況を表現していて、ハードウェア的な比喩を使うなら：
- Σは、引数とローカル変数を累積するスタック
- xは、レジスタの値
- {E1, E2, ...} はコード領域
Σ;x{E1, E2, ...} → Γ;y{F1, F2, ...} というシーケントは、評価計算の実行により、計算状況が変化したことを表します。こうなると、論理的な意味は薄くなり、記号的な仮想計算機を使った操作的意味論をやることになります。シーケント計算の証明図は、一連の評価計算の計画（未来のこと）または評価計算の履歴（過去のこと）を表します。
gotoによる制御を扱うには、コードを一時的に保存する制御スタック（コードスタック）も必要になりますが、今回は制御スタックは入れないことにします。Σ;x{E1, E2, ...} → Γ;y{F1, F2, ...} という形のシーケントを評価シーケントと呼ぶことにしましょう。
今まで（って、たいした期間じゃないが）使ってきたシーケント Σ;x{E} → Γ;y は、Σ;x{E} → Γ;y{} とみなすことによって、新しいタイプのシーケント内に埋め込めます。今までの書き方をそのまま使えるように、式の列が空のときは、{}を省略してもいいとします。
推論規則、公理、証明
評価シーケントは、文字通り式を評価して計算を進行させることを表します。評価シーケントを上下に並べた図形を推論規則と呼びます。図形であることを強調するときは推論図ともいいます。推論規則の意味は、上段にある評価シーケントが正しい（その評価計算が可能である、合法である）ならば、下段の評価シーケントも正しい、ということです。
上段がカラッポである推論規則を公理規則あるいは単に公理と呼びます。公理規則の上段は空なので、下段に現われるシーケントのことを公理と呼ぶこともあります。公理は、無条件にいつでも正しい評価方法のことです。
推論規則の実例を3つ挙げます。規則[id]は公理です。1個の星印はカラッポであることの目印です。規則[comp]の上段は2つの評価シーケントを横に並べたものですが、横幅が広くなりすぎるので二行に書いています。
*
----------------------------------------[id]
Σ;x{E1, E2, ...} → Σ;x{E1, E2, ...}
Σ;x{E1, E2, ...} → Γ;y{F1, F2, ...}
Γ;y{F1, F2, ...} → Δ;z{G1, G2, ...}
-----------------------------------------[comp]
Σ;x{E1, E2, ...} → Δ;z{G1, G2, ...}
Σ;x{E1} → Γ;y
------------------------------------[first]
Σ;x{E1, E2, ...} → Γ;y{E2, ...}
推論図を積み重ねた図形が証明図です。証明図についてこれ以上は説明しませんが、論理と同じ概念と用語法を使います。
束縛列の操作
シーケントの左右は、計算状況の記号的な表現です。そのなかで束縛列は、引数とローカル変数を蓄えるスタック、ないしはスコープチェーンの役割を果たすものです。変数の可視性は、束縛列の操作で表現されます。
束縛σ, γ、変数名a、値xに対して、次のような操作が定義されました（「ホーア論理とシーケント計算を混ぜたような意味記述構文」参照）。
- σ[a] -- 変数値の取り出し
- σ{x/a} -- 変数値の追加または置き換え
- σ+<γ -- γを優先させた束縛のマージ
- σ++γ -- 名前の共通部分がない場合のマージ
σ++γ が定義できるとき、σとγは直交していると言い、σ⊥γ と書くことにします。
- σ⊥γ ⇔ (σに含まれる名前の集合とγに含まれる名前の集合に共通部部がない)
束縛の列Σ, Γに対しても同様な概念をこれから定義します。それらは次の記法で表されるものですね。
- Σ[a]
- Σ{x/a}
- Σ+<Γ
- Σ++Γ
束縛列の直交性は、「Σ⊥Γ ⇔ Σ++Γ が定義できる」となるように（すぐ後で）定義します。
Σ[a] と Σ{x/a} は「ホーア論理とシーケント計算を混ぜたような意味記述構文」で既に定義しているのでソチラを参照してください。Σ{x/a} はシャドーイングありの単一代入です。現在の（一番内側の）スコープ（束縛）に変数の追加はできますが、既存の変数を書き換えることはできません。
Σ+<Γ と Σ++Γ は次の節で定義しましょう。
束縛列のマージ
ΣとΓが束縛の列のとき、カンマを置いて並べた形 Σ,Γ は、ΣとΓの連接だとします。カンマを連接の中置演算子に使っているわけですが、混乱しやすいので良い記法とは言えませんねー。が、abuse of notation ということでご勘弁を。
さて、Σ+<ΓとΣ++Γはどちらも Σ,Γ のことだとします。ただし、Σ++Γが定義できるためには条件が必要です。その条件は次のように述べられます。
- Σ = (σ1, ..., σn)、Γ = (γ1, ..., γm) とする。
- σ = σ1+< ... +<σn、γ = γ1+< ... +<γm と定義する。つまり、σはΣの成分をすべて+<演算したもの、γはγの成分をすべて+<演算したもの。ΣやΓが空のときは、「すべて+<演算したもの」はε（空な束縛）とします。
- このようにして作ったσとγに、同じ名前が出現しないときに限り Σ++Γ が定義できる。
Σ、σ、Γ、γ を上で述べた意味だとして、次の条件は同値です。
- σとγに名前の共通部分がない。
- σ⊥γ
- σ++γが定義できる。
- Σ++Γが定義できる。
Σ++Γが定義できるとき、ΣとΓは直交していると言い、Σ⊥Γ と書きます。
Σ+<ΓもΣ++Γも単なる連接ですが、次の性質が成立します。（σとγは上で定義した意味を持つとします。）
- (Σ+<Γ)[a] = (σ+<γ)[a]
- (Σ++Γ)[a] = (σ++γ)[a]
- (Σ+<Γ)[a] が未定義のときは、(Σ+<Γ){x/a} = (σ+<γ){x/a}
- (Σ++Γ)[a] が未定義のときは、(Σ++Γ){x/a} = (σ++γ){x/a}
これらの性質により、束縛列は単一の束縛と同じように扱えることになります。
評価シーケント計算のまとめ
1つの評価シーケントは、式の評価方法を記述しています。シーケントの左右は、評価計算の前と後の計算状況の記号的表現です。推論規則は、一連の評価計算をどのように進めるかを表しています。
評価シーケント、推論規則、証明図は、記号的仮想機械により操作的な解釈ができて、呼び出しスタック（あるいはスコープチェーン）、値レジスタ、コード領域のそれぞれが変化していく様子として捉えることが可能です。
