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

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

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

参照用 記事

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

Catyの意味論を少しずつ書いていきます(あんまりタラタラはしてられないけどね)。

タラタラはしてられないので、やれるところまで今日やっちゃいますよ、意味論。

「Catyのインタプリタ=評価関数の表示的意味論」において、Catyスクリプトの表示的意味論と操作的意味論の中間みたいな形で、インタプリタの記述をしました。続いて、論理的意味論(公理的意味論)を組み立てましょう。論理的意味論の、いや、形式手法すべての原点といえばホーア論理です。ホーア論理のスタイルにより、Catyスクリプトのための演繹系を定義します。これは、インタプリタのみならずコマンドやファシリティの、仕様記述とテストの枠組みを与えます。

念のため注意しておきますと; ホーア論理は「枠組みを与えます」が、機械的推論アルゴリズムに向いているとは言えません。アルゴリズムはまた別に考える必要があります。

内容:

  1. ホーア・トリプル
  2. 基本的な式に関する推論規則
  3. 包含関係式に関する推論規則
  4. 式の構成に沿った推論規則
  5. 簡単な派生推論規則の例
  6. 証明図の例
  7. あと、それから

ホーア・トリプル

p, qを論理式、Sをプログラムコードとして、p{S}q の形をホーア・トリプルと呼びます。ホーア・トリプル p{S}q の意味は、「プログラムの実行前にpが成立しているならば、コードSを実行した後でqが成立する」ということです。

ここでは、命題p, qとしては、次の形のものに限定します。

  • x∈A (xは自由変数、AはJsonの部分集合*1

さらに、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つの包含関係式で表せます。

  1. a = b
  2. a∈A
  3. A = 0

それぞれ:

  1. {a}⊆{b}
  2. {a}⊆A
  3. 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}}U

A{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]-規則を(マクロではなく)組み込みの推論規則に最初から入れておいてもいいでしょう。

証明図の例

次のことを“事実”として仮定します。

  1. a∈X
  2. f::A->U
  3. g::B->V
  4. 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に、ホーア・トリプルとその推論を突っこんだようなシステムですね。手と紙で証明するぶんには、この演繹系けっこう使いよい。が、あんまりコンピュータ向きじゃないので、次はコンピュータ向きの演繹系を考えることになります。でもその前に、もう少しチャントした形に整理したほうがいいかもな。

*1:正確に言えば、Jsonの部分集合を表すつもりの記号や記号列です。有り体にいってこの記事では、構文的対象と意味的対象をテキトーに混同しているのです。

*2:実際のCatyでは、1 = {null} です。