ホーア論理とシーケント計算を混ぜたような意味記述構文

CatyScript2.0の言語仕様を検討してまして、その意味論をどうやって記述しようか？ と考えています。意味論の記述言語にCatyScript自体を使うという方法があります。次の記事で断片的にそれを試みています。

• CatyScriptで記述するCatyシェル
• CatyScriptで記述するCatyのリクエスト処理

CatyScript2.0によりCatyScript2.0の仕様を書くのは割と容易で楽しい（やってみた）のですが、循環論法なのは確かです（意図的に循環させているのですがね）。やはり意味論には、もっと形式化された記述言語がふさわしいでしょう。

以前、CatyScript1.0（現状のCatyScrip)の意味論を表示的意味論風に書いたことがあります。

• Catyのインタプリタ＝評価関数の表示的意味論

これは、数学的な関数概念を使って次のEval関数を定義する方法です。

• Eval(x, E, p) （xが入力データ、Eが式、pがパラメータ）

この方法により、評価された結果である値を記述することはできるのですが、Eval関数の定義を推論の道具には使えません（使えたとしても使いづらいでしょう）。そこで次のようなこともやりました。

• Catyの論理的意味論：ホーア論理からはじめよう

しかし、表示的意味論と論理的意味論を2回書くのは面倒です。一回で済ませたい。そこで、評価の規則と推論の方法を一度に書けるような記述方法を考えることにしました。

内容：

1. 今回使うホーアトリプルの定義
2. 束縛の表現
3. 束縛の演算
4. クロージャの表現
5. 推論規則
6. 束縛の列に関する参照と代入
7. 参照と代入の意味記述
8. 見通しと妄想

今回使うホーアトリプルの定義

「Catyの論理的意味論：ホーア論理からはじめよう」では、データの集合A, Bと式Eから、ホーアトリプル A{E}B を作っています。今回は、集合ではなくて値x, yを使って x{E}y という形のホーアトリプルにします*1。x{E}y の意味は次のとおりです。

• 入力をxとして式Eを評価したら、結果（出力）はyとなる。

これなら、Evalによる評価 Eval(x, E) ⇒ y を、x{E}y の形式で書けます。ただし、パラメータpが考慮されてません。

CatyScript2.0では、パラメータ以外に一般的な変数概念も導入する予定なので、変数の束縛環境（値割り当て）を考慮することにします。変数の束縛環境をσ, γ, δ, などのギリシャ文字小文字で表します。以下、変数の束縛環境を単に束縛（bindings）と呼ぶことにします。束縛を考慮して拡張したホーアトリプル σ;x{E}γ;y は、次の意味を持つとします。

• 束縛がσ、入力をxとして式Eを評価したら、評価後の束縛はγ、結果（出力）はyとなる。

束縛は入れ子になることがあるので、入れ子の束縛を σ1, σ2, ..., σn のように表します。左側のσ1が一番外側の束縛で、σnが一番内側の束縛です*2。入れ子の束縛を認めると、さらに拡張したホーアトリプルは次の形になります。

• σ1, .., σn; x {E} γ1, ..., γm; y

これは、論理的には一種の含意命題なので、その点を強調したいときは次の形で書きます。

• σ1, .., σn; x {E} → γ1, ..., γm; y

矢印を加えるとシーケンとのような気もします。束縛をカンマで区切って並べたモノは、Σ、Γなどのギリシャ文字大文字で表現することにすると、ホーアトリプルは次のようにも書けます。

• Σ; x {E} Γ; y （オリジナルのトリプル形式）
• Σ; x {E} → Γ; y （シーケント風）

束縛の表現

変数の名前と値の対応をここでは束縛と呼ぶことにしましたが、束縛以外に様々な呼び名があります。

• 値割り当て（valuation）
• 状態（state）
• 環境（environment）
• ストア（store）

なお、束縛では表現できないもっと外側の環境はアンビエント環境（ambient environment）、あるいは単にアンビエントと呼ぶことにしています。いずれ、アンビエントの話もします。

束縛は名前・値ペアの集合なので、{名前1 : 値1, 名前2 : 値2, ..., 名前n : 値n} の形で書きます。名前の重複は許しません。名前は、コンピュータのなかでは文字列データなので、束縛をJSONオブジェクトと思ってかまいません。入れ子になった束縛 σ1, ..., σn はJSONオブジェクトの配列 [σ1, ..., σn] で表現できます。単一の束縛σは、長さ1の配列 [σ] とみませます。よって、束縛の列 Σ, Γ などはJSONオブジェクトの配列で表現可能です。

aが変数名（の文字列）だとして、束縛σにおけるaの値を σ[a] と書きます*3。束縛σのなかに名前aがないときは、σ[a] = ⊥ だとして、⊥（ボトム）の処理は後で考えることにします。

aが変数名、xが値のとき、束縛σに対して σ{x/a} という記法も使います*4。σ{x/a} の意味は次のとおり。

• 名前aがσに含まれてないときは、a : x という名前・値ペアをσに付け加えたモノ
• 名前aがσに含まれるときは、aに対する値をxにセットしたモノ

σ{x/a} は、束縛σのもとで破壊的代入文 a := x を実行した後の束縛だと思えばいいでしょう。

束縛の演算

2つの束縛に対する演算（二項演算）として、++、+<, >+ の3つの演算を導入します。σ, γが束縛とのとき、σ++γ、σ+<γ、σ>+γ は次のように定義されます。

1. σ++γ は、σとγに含まれる名前に共通部分がないときだけ定義される。σに含まれる名前・値ペアと、γに含まれる名前・値ペアを合併した集合となる。
2. σ+<γ は、σに含まれる名前・値ペアと、γに含まれる名前・値ペアを合併した集合だが、同じ名前があれば、γの値を採用する。
3. σ>+γ は、σに含まれる名前・値ペアと、γに含まれる名前・値ペアを合併した集合だが、同じ名前があれば、σの値を採用する。

この定義から、σ+<γ = γ>+σ であり、σとγに含まれる名前に共通部分がないときは σ++γ = σ+<γ = σ>+γ であることは明らかです。

εを空な束縛とすると、ε+<σ = σ+<ε = σ であり、束縛の二項演算+<はεを単位元とするモノイド演算となります。二項演算>+も同様です。二項演算++は部分演算ですが、部分的（partial）な可換モノイド演算となります。

[追記]ここで導入した3つの演算 ++、+<、>+ は、束縛に限らず、JSONオブジェクトのようなレコード型データ構造に対する演算として便利に使えます。知っておくと利用場面は多いと思います。[/追記]

クロージャの表現

「CatyScriptで記述するCatyのリクエスト処理」において、CatyScriptにおけるクロージャを次のように定義しました。

/** クロージャ

 */ 

type Closure = {

 /** 入力 */

 @[default(null)]

 "input" : any?,
 /** 変数束縛 */

 @[default({})]

 "vars" : object?,
 /** オプションパラメータ */

 @[default({})]

 "opts" : object?,
 /** 引数パラメータ */

 @[default([])]

 "argv" : array?,
 /** 実行すべきスクリプトコード */

 @[default("")]

 "code" : (string | binary)?

};

このなかで、オプションパラメータ（名前付きパラメータ）と引数パラメータ（位置パラメータ）は、入れ子の変数束縛で表現可能です。オプションパラメータはそもそも名前・値ペアの集合なので、そのまま束縛とみませます。引数パラメータは配列値なので、"_ARGV"とか"$ARGV"とかの普通は使わない（あるいは使えない）名前の値としてオプションパラメータに混ぜてしまえばいいでしょう。

具体的には、--num=25 --flag=true hello world のようなコマンドラインパラメータは次の束縛になります。

{

  "num" : 25,

  "flag" : true,

  "_ARGV" : ["", "hello", "world"]

}

_ARGVの0番項目はシステム側でセットするものです。

クロージャ内に含まれる入力をx、もとの変数束縛をσ、オプションパラメータと引数パラメータを一緒にした束縛をα、スクリプトコードの式をEとすると、クロージャは σ, α; x {E} の形になります。つまり、ホーアトリプルを含意命題（あるいはシーケント）の形に書いたときの前提部分がクロージャとなります。表にまとめると次のとおりです。

クロージャ	ホーアトリプル
input	入力 x
vars	束縛 σ
opts	束縛 α の一部
argv	束縛 α の一部
code	式 E

クロージャの評価規則は、σ, α; x {E} → Γ; y というホーアトリプル（あるいはシーケント）で表現できます。Γは評価後の束縛、yは評価した結果の値です。

推論規則

ホーアトリプルは論理式なので、推論ができないと面白くありません。いくつかの推論規則を導入してみます。ただし、推論規則の雰囲気を伝える程度にして、CatyScript2.0における実際の推論規則は別な記事で述べます。

まずは、一種の構造規則である「束縛の水増し規則」です。

      Σ; x {E} → Γ; y

 ----------------------------[Thinning]

  Δ, Σ; x {E} → Δ, Γ; y

評価に関係しない束縛がいくらあっても害にはならないことを主張しています。

[追記]次に挙げている「束縛の入れ子規則」は良くない例ですね。 σ+<σ' と σ, σ' を入れ替えることはスコープ構造を壊してしまうので、たちの悪い変形です。一般的な規則としては採用できません。[/追記]

束縛の入れ子の意味を与える推論規則「束縛の入れ子規則」は次です。この規則がほんとに必要かどうかよく分からないのですが、とりあえず例として。

  Σ, σ+<σ'; x {E} → Γ; y

 -----------------------------[Nest]

  Σ, σ, σ'; x {E} → Γ; y

実際の評価計算では、推論の上下を入れ替えた次の形のほうが便利です。

  Σ, σ, σ'; x {E} → Γ; y

 -----------------------------[Nest']

  Σ, σ+<σ'; x {E} → Γ; y

[追記]良くない例、ここまで。[/追記]

一般に、評価計算で使うときは推論規則の逆を使うことが多いのですが、いちいちそのことには言及しないで、論理的な推論に使う規則を示すことにします。

評価すべき式Eが定数cであるとき、評価の結果はcであるし、束縛に影響を与えません。この事実は次のように書き表します。

 -------------------[const]

 Σ; x {c} → Σ; c

推論規則の上段（前提、仮定）はカラッポです。このとき、下段は公理ですが、公理を特別扱いしないで、上段がカラッポの推論規則として扱います。なお、上段がカラッポであることを明示するために、星印を1つ書いておくと見やすいようです。

           *

 -------------------[const]

 Σ; x {c} → Σ; c

束縛の列に関する参照と代入

1つの束縛は名前・値ペアの集合（ただし名前の重複はない）で、Σ、Γなどは束縛の列を表すのでした。σ, Σ とか Σ, σ のように書いた場合は、束縛の列Σ（空かもしれない）に束縛σを、書かれている順序でアペンドした列を表します。また、Σ, Γ という書き方は、ΣとΓの連接（concatenation）です。カンマをオーバーロードしているので、文脈により適切に解釈する必要があります。

aが名前、xが値のとき、束縛σに対してσ[a]とσ{x/v}を定義しました。束縛の列Σに対しても、Σ[a]とΣ{x/a}を定義します。まずは、Σ[a]から：

1. Σが空のときは、Σ[a] = ⊥
2. Σ = (Σ', σ) のときは、
   1. σ[a] が定義されているなら、Σ[a] = σ[a]
   2. σ[a] が未定義なら、Σ[a] = Σ'[a]

次にΣ{x/a}の定義を2種類示します。それぞれを、浅い代入と深い代入と呼ぶことにします。いずれも破壊的代入です。

浅い代入：

1. Σは空のときは、Σ{x/a} = [{a : x}]
2. Σ = (Σ', σ) のときは、Σ{x/a} = (Σ', σ{x/a})

深い代入：

1. Σが空のときは、Σ{x/a} = [{a : x}]
2. Σ = (Σ', σ) のときは、
   1. σ[a] が定義されているなら、Σ{x/a} = (Σ', σ{x/a})
   2. σ[a] が未定義なら、Σ{x/a} = (Σ'{x/a}, σ)

Catyでは、浅い代入に条件を付けた単一代入*5を採用します。

単一代入：

1. Σが空のときは、Σ{x/a} = [{a : x}]
2. Σ = (Σ', σ) のときは、
   1. σ[a] が定義されているならエラー、
   2. σ[a] が未定義なら、Σ{x/a} = (Σ', σ{x/a})

どのような代入方式を採用するかは目的に応じて選びます。とはいえ、深い代入はやめたほうがいいと思いますけど。

参照と代入の意味記述

Σが束縛の列（空列でもよい）として、名前aと値vに対して Σ[a]、Σ{x/a} が定義されているなら、変数参照と代入の意味論を記述できます。

変数参照の構文が単に変数名aだけで、代入の構文が a := E の場合、それらの意味論は次のように記述できます。

            *

 ------------------------[var]

  Σ; x {a} → Σ; Σ[a]

     Σ; x {E} → Γ; y

 ------------------------------[assign]

  Σ; x {a := E} → Γ{y/a}; y

CatyScript2.0では、変数参照の先頭にはパーセント記号が付き、代入はリダイレクトの構文を使います。よって、変数参照と代入式の意味論は次のようになります。

            *

 ------------------------[var]

  Σ; x {%a} → Σ; Σ[a]

     Σ; x {E} → Γ; y

 ------------------------------[assign]

  Σ; x {E > a} → Γ{y/a}; y

%0, %1, ... のようなパーセント記号に番号を続けた変数の意味は、おそらく次のようになるでしょう。ここで、kは番号で、番号kによる配列へのインデックスアクセスも [k] の形で表しています。

             *

 ---------------------------------[var-pos]

  Σ; x {%k} → Σ; Σ[_ARGV][k]

とまー、こんな感じで意味論を記述していくことになります。

見通しと妄想

以上に概略を述べた方法で、CatyScript2.0の評価の方法と証明の方法を同時に記述できるんじゃないかな、と思っています。ただし、例外処理や大域的制御構造（gotoです）を導入すると、この方法では無理があります。制御スタックや継続のような概念を追加することになるでしょう。

「Catyの論理的意味論：ホーア論理からはじめよう」で述べたように、値ではなくて集合（述語と言っても同じ）を入出力仕様に使って、型推論も行えたらいいなー、とか少し期待してます。例えば、式Eと式Fのパイプライン結合に関する推論規則は次のようですが、値x, y, zを条件に変更するようなことです。

  Σ; x {E} → Γ; y    Γ; y {F} → Δ; z 

 -------------------------------------------[comp]

        Σ; x {E|F} → Δ; z 

x, y, z を P, Q, Q', Rという条件に直して、含意命題 Q⊃Q' を加えると次のような推論規則になります。

  Σ; P {E} → Γ; Q   Q⊃Q'   Γ; Q' {F} → Δ; R 

 --------------------------------------------------[comp]

        Σ; P {E|F} → Δ; R

この図式を眺めていると、Σ → Γ とかがベース圏の射で、Q⊃Q' などがファイバー内の垂直射になっているインデックス付き圏（圏のファイブレーション）になっているような気がするんですが、妄想かも知れません。

*1:将来的に、再び集合に戻すかもしれません。

*2:この順序は、紙や黒板に書くときの順序です。実装上は、σnをスタックトップにしたほうが便利でしょう。

*3:σを関数とみなして σ(a) と書くこともあります。

*4:σ[x/a] と書くことも多いようです。

*5:内側のスコープで外側の束縛を隠すこと（シャドーイング）は許します。