Catyの意味論を少しずつ書いていきます（あんまりタラタラはしてられないけどね）。
タラタラはしてられないので、やれるところまで今日やっちゃいますよ、意味論。
「Catyのインタプリタ＝評価関数の表示的意味論」において、Catyスクリプトの表示的意味論と操作的意味論の中間みたいな形で、インタプリタの記述をしました。続いて、論理的意味論（公理的意味論）を組み立てましょう。論理的意味論の、いや、形式手法すべての原点といえばホーア論理です。ホーア論理のスタイルにより、Catyスクリプトのための演繹系を定義します。これは、インタプリタのみならずコマンドやファシリティの、仕様記述とテストの枠組みを与えます。
念のため注意しておきますと； ホーア論理は「枠組みを与えます」が、機械的推論アルゴリズムに向いているとは言えません。アルゴリズムはまた別に考える必要があります。
内容：
- ホーア・トリプル
- 基本的な式に関する推論規則
- 包含関係式に関する推論規則
- 式の構成に沿った推論規則
- 簡単な派生推論規則の例
- 証明図の例
- あと、それから
ホーア・トリプル
p, qを論理式、Sをプログラムコードとして、p{S}q の形をホーア・トリプルと呼びます。ホーア・トリプル p{S}q の意味は、「プログラムの実行前にpが成立しているならば、コードSを実行した後でqが成立する」ということです。
ここでは、命題p, qとしては、次の形のものに限定します。
さらに、EはCatyスクリプトの式だとして、(x∈A){y := Eval(x, E)}(y∈B) の形を考えることにします（「:=」は代入）。この形しか考えないので、これを再び A{E}B の形で略記し、Catyにおけるホーア・トリプルとして扱います。ホーア・トリプルの意味を述語論理の論理式で書けば、次のようになります。
- A{E}B ⇔ ∀x.[x∈A ⊃ (Eval(x, E))∈B]
ホーア・トリプル A{E}B 以外に、次の形の命題（論理式）も使います。
- A⊆B （A, BはJsonの部分集合）
A⊆B の形の論理式を包含関係式と呼ぶことにします。0は空集合、1は特定された単元集合*2を表す定数として使います。次の命題は1つの包含関係式で表せます。
- a = b
- a∈A
- A = 0
それぞれ：
- {a}⊆{b}
- {a}⊆A
- A⊆0
基本的な式に関する推論規則
式Eが定数リテラル（スカラーだと思ってよい）のとき、E = c (c∈A) のように書くことにします。式Eがコマンド呼び出しのとき、E = f (f::A->B) のように書くことにします。A->B はコマンド呼び出しfのプロファイルです。
まず、2つの基本的な推論規則を導入します。
Eが定数、つまり、E = c、c∈A のとき、次の推論ができます。
-----------[定数]
1{c}A
Eがコマンド呼び出しfで、f::A->B のときは次の推論ができます。
-----------[呼び出し]
A{f}B
これらの推論規則の仮定（横棒の上側）がカラッポなので、1{c}A と A{f}B は公理だとも言えます。定数リテラルcごとに[定数]-規則、コマンド呼び出しfごとに[呼び出し]-規則があります。
[定数]と[呼び出し]は、推論規則としては仮定を持たないのですが、便宜上、(c∈A)、(f::A->B) というアノテーションを横棒の上に書くことにします。
(a∈A)
------------[定数]
1{c}A(f::A->B)
------------[呼び出し]
A{f}B
包含関係式に関する推論規則
ホーア・トリプルと包含関係式が混じった推論を2つ導入します。
X⊆A A{E}B
--------------[左包含]
X{E}B
A{E}B B⊆Y
--------------[右包含]
A{E}Y
式の構成に沿った推論規則
式の構成方法には次がありました。
| 番号 | 構成方法 | 式の形 | 圏論的な解釈 |
|---|---|---|---|
| 1 | パイプ | E | F | 射の結合 |
| 2 | 配列 | [E, F] | デカルトペア（名前なし） |
| 3 | オブジェクト | {α:E, β:F} | デカルトペア（名前あり） |
| 4 | 分岐 | when {α=>E, β=>F} | 余デカルトペア |
| 5 | 繰り返し | each {E} | 圏論的クリーネスター |
それぞれの構成方法ごとに推論規則を導入します。∩ は集合の共通部分です。[U, V], {α:U, β:V}, (@α A), List(A) などは型構成子ですが、その意味は容易に想像できるでしょう。
A{E}B B{F}C
---------------[パイプ]
A{E | F}C
A{E}U B{F}V
---------------------[配列]
(A∩B){[E, F]}[U, V]
A{E}U B{F}V
--------------------------------[オブジェクト]
(A∩B){{α:E, β:F}}{α:U, β:V}
A{E}U B{F}V
------------------------------[分岐]
(@α A){when {α=>E, β=>F}}UA{E}B
-----------------------[繰り返し]
List(A){each{E}}List(B)
[追記]もう1つ鬱陶しい推論規則があったのだった。「コイツをなくせないかなー」と思っていたせいか、入れ忘れました。なくせればそれでハッピー。やっぱり必要だと判明すれば次の機会に触れます。[/追記]
簡単な派生推論規則の例
今までに述べた推論規則を組み合わせると、派生推論規則（マクロ推論規則）が作れます。例えば、次の規則は便利です。
A{E}B B⊆B' B'{F}C
---------------------[ゆるいパイプ]
A{E | F}C
この[ゆるいパイプ]-規則は、[右包含]-規則（[左包含]でもよい）と[パイプ]-規則の組み合わせです。
A{E}B B⊆B'
------------[右包含]
A{E}B' B'{F}C
----------------------[パイプ]
A{E | F}C
when {α=>E, β=>F} と when {β=>F, α=>E} を構文的には区別しないことを利用すれば、次の規則も派生規則として得られます。
A{E}U B{F}V
-----------------------------[分岐 2]
(@β B){when {α=>E, β=>F}}V
[分岐 2]-規則の展開形は次のとおりです。
A{E}U B{F}V
-----------------------[交換]
B{F}V A{E}U
-----------------------------[分岐]
(@β B){when {β=>F, α=>E}}V
-----------------------------[構文的同値]
(@β B){when {α=>E, β=>F}}V
“構文的同値”なんて概念を使いたくないなら、[分岐 2]-規則を（マクロではなく）組み込みの推論規則に最初から入れておいてもいいでしょう。
証明図の例
次のことを“事実”として仮定します。
- a∈X
- f::A->U
- g::B->V
- h::C->W
この状況で、1{a | f | [g, h]}[V, W] を適当な論理的仮定から証明します。下の証明図で「*」が付いている論理式は証明における仮定です。
(a∈X) (f::A->U) (g:B->V) (h::C->W)
-------[定数] -----------[呼び出し] ------[呼び出し] -------[呼び出し]
1{a}X * X⊆A A{f}U B{g}V C{h}W
--------------------------[ゆるいパイプ] -----------------------[配列]
1{a | f}U * U⊆(B∩C) (B∩C){[g, h]}[V, W]
-----------------------------------------------------------[ゆるいパイプ]
1{a | f | [g, h]}[V, W]
この証明図の存在は、いま定義した演繹系で次が成立することを意味します。
- X⊆A, U⊆(B∩C) |- 1{a | f | [g, h]}[V, W]
連言（and, conjunction）と含意（implication）があって、演繹定理を仮定するなら、次のように言い換えることもできます。
- |- X⊆A∧U⊆(B∩C) ⊃ 1{a | f | [g, h]}[V, W]
いずれにしても、X⊆A と U⊆(B∩C) が静的または動的に確認できるなら、1{a | f | [g, h]}[V, W] が保証できることになります。これは、次の意味論的な事実を保証することにつながります。
- Eval('a | f | [g, h]') ∈ [V, W]
あるいは、2項Evalに関して：
- Eval(a, 'f | [g, h]') ∈ [V, W]
あと、それから
表示的（操作的っぽい表示的だが）意味論はアレで終わりだし、ホーア論理風演繹系もコレで終わりです。今回定義した演繹系は、古典論理の演繹系NKに、ホーア・トリプルとその推論を突っこんだようなシステムですね。手と紙で証明するぶんには、この演繹系けっこう使いよい。が、あんまりコンピュータ向きじゃないので、次はコンピュータ向きの演繹系を考えることになります。でもその前に、もう少しチャントした形に整理したほうがいいかもな。
