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

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

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

［参照用 記事］

非決定性写像の圏におけるホーア式のモデル

雑記／備忘

「FIT/FitNesseと多重マークアップ／多重データ構造」にチラッと書いたのですが、カニンガムのFITに似たCaty向けテストシステムを作成中です。

基本的な構文要素は、エクスペクテーション、エクスペクテーションの列、ホーア・トリプルです。これらは、次の形でWiki文書として記述されます。

構文要素 Wiki記法
エクスペクテーション テーブルの1行
エクスペクテーションの列 テーブル
ホーア・トリプル 見出しで識別された3つのセクション

トリプルは、事前条件、実行部、事後条件の3つの部分からなりますが、事前条件と事後条件は省略可能です。条件が省略されていても、常に真となる条件がそこにあると思えば「トリプル（三つ組）」です。

さて、エクスペクテーションは、論理式と実行文を兼ねた構文要素で、その意味論が問題になります。こんなときは、ある程度は形式的（フォーマル）に記述した方が手っ取り早いし正確さも担保できるので、遠慮なしに圏論や代数の言葉を使うことにします。今回はまず、かなり退屈なんですが、諸々の定義を羅列します。例と証明は付けませんが、例を探して細部を埋めるのは練習問題ということで。

この記事で導入した概念を使ってエクスペクテーションのモデルを構成するのは次回（続き）にします。

内容：

  1. 非決定性写像の圏
  2. 非決定性写像に関する用語と記法
  3. ベキ等な足し算構造
  4. ベキ等半環（ISR）
  5. ブール代数
  6. 可換なベキ等演算と順序
  7. ガード演算
  8. ホーア式
  9. 等式的な表現
  10. まとめと予告

全体：

  1. 非決定性写像の圏におけるホーア式のモデル
  2. 非決定性写像の圏におけるホーア式のモデル 踊り場・編
  3. 非決定性写像の圏におけるホーア式のモデル いちおう完結・編

非決定性写像の圏

プログラムの挙動は状態遷移で表現できますが、決定性の遷移だけだと何かと不便なので、非決定性遷移を使うことにしましょう。S, Tが集合のとき、fがSからTへの非決定性写像だとは、通常の写像としては f:S→Pow(T) と書けることです。Pow(T)は、Tの部分集合全体からなる集合、つまりTのベキ集合です。非決定性写像の結合（合成）を定義できるし、s∈S に対して、s|→{s} で定義される非決定性写像が恒等を与えるので、非決定性写像の圏ができます。

モナドをご存知なら、次の説明がスッキリするでしょう； 集合圏Set上に、共変ベキ関手Pow*を考えます。下付きの星は、共変であることを強調するためです。次のような、モナド乗法とモナド単位で共変ベキ関手はモナドになります。

  • flattenS : Pow*(Pow*(S)) → Pow*(S)
  • singletonS : S → Pow*(S)

この共変ベキ・モナドのクライスリ圏 Kl(Set, Pow*) を作ると、それが非決定性写像の圏NDMapになっています。

  • NDMap = Kl(Set, Pow*)

圏NDMapは抽象的な圏ではなくて、集合圏から具体的に構成された圏であることに注意してください。集合と要素を使っていくらでも手でいじることができます。

非決定性写像に関する用語と記法

圏NDMap内で考えることにして、f:S→T は非決定性写像とします（集合圏では f:S→Pow(T) です）。Sをfの始域、Tをfの終域と呼ぶことにして、次の定義をします。

  • fの定義域 = Def(f) = {s∈S | f(s) ≠ 空集合}
  • fの像 = Im(f) = {t∈T | t∈f(s) となるsが存在する}

fのグラフを、{(s, t)∈S×T | t∈f(s) } とすると、Def(f)とIm(f)はグラフを2方向に射影した影＜かげ＞のことです。

A⊆S, B⊆T として、fの制限とマスキングを次のように定義しましょう。

  • fのAへの制限 = f|A = λs.[if (s∈A) then f(s) else 空集合]
  • fのBによるマスキング = f∩B = λs.[f(s)∩B]

また、f, g:S→T の和を次のように定義します。

  • (f + g) = λx.[f(s)∪g(s)]

f + g より f∪g と書いた方が自然ですが、他の記法との兼ね合いでプラス記号を使うことにします。

I（大文字アイ）とO（大文字オー）は次の意味で用いることにします。

  • IS = idS = λs.({s})
  • OS→T = λs.(空集合)

OS→S は、OS と略記し、さらに混乱の心配がないなら下付きのSとかS→Tを省略します。

ベキ等な足し算構造

圏NDMapのホムセット HomNDMap(S, T) = NDMap(S, T) に注目してみます。f, g ∈NDMap(S, T) に対して、足し算（和） f + g を定義しましたが、この足し算は次を満たします。

  1. (f + g) + h = f + (g + h)
  2. f + O = O + f = f
  3. f + g = g + f

つまり、NDMapのホムセットは必ず可換モノイドになっています。この可換モノイドは次の等式も成立するという意味で特殊なものです。

  • f + f = f （ベキ等性）

また、j:R→S, k:T→U とすると、次の分配法則も成立します。

  1. j;(f + g) = j;f + j;g
  2. (f + g);k = f;k + g;k

特に、EndNDMap(S) = NDMap(S, S) では、射の結合「;」を掛け算と考えると、足し算／掛け算が、割と普通に／かなり自由に遂行できる計算体系になっています。でも、引き算はうまく定義できないし、足し算はベキ等、掛け算は可換とは限らないことには注意しましょう。

ベキ等半環（ISR）

前節で述べた、NDMap(S, S)は、プログラムが引き起こす状態遷移を計算するための代数構造として適切なものです。

f, g∈NDMap(S, S) を、状態空間Sに作用するプログラム（のdenotation）だとみなせば、NDMap(S, S)が持つ演算／定数と、プログラムの構成は次のように対応します。

演算／定数 プログラムの構成
掛け算 ; 順次実行
足し算 + 非決定性の選択
零 O 常に失敗するプログラム
単位 I 何もしないプログラム

「;」と「I」で可換とは限らないモノイド、「+」と「O」で可換なベキ等モノイドになっています。さらに次の分配法則が成立します。

  • (f + g);h = f;h + g;h
  • h;(f + g) = h;f + h;g

今述べた計算法則を満たすような代数系はベキ等半環（ISR; idempotent semiring）と呼ばれます。さらに、クリーネスターとそれに関する公理を付け加えると、クリーネ代数の定義になります。でも、今回はクリーネスターは不要なので、ベキ等半環の範囲内で話をします。

ブール代数

Ωを二値ブール代数とします。 Ω = {0, 1} で、1が真で0が偽とします。ブール演算の記号は ∧、∨、¬ を使うことにします。Sを集合として、Ω(S) = ΩS としましょう。ここで、ΩS は普通の指数べきで、ΩS = {f | f:S→Ω という写像} です。Ω(S)も自然にブール代数となります。Ω(A)においても、定数0, 1、演算記号∧、∨、¬を使います。

p∈Ω(S) とは、p:S→Ω （ただし、集合圏で）のことです。つまり、pは二値真偽値を値とする関数です。このような関数を述語（predicate）とか性質（property）とか呼びますが、ここでは条件とか命題という言葉を使います。pがS上の条件であるとき、条件を満たす点の全体はSの部分集合になります。それを [p] と書くことにします。

  • [p] = {s∈S | p(s) = 1}

次の法則が成立します。

  1. [p∧q] = [p]∩[q]
  2. [p∨q] = [p]∪[q]
  3. [¬p] = [p]c

上付きのcは集合の補集合を表します。

∧を掛け算、∨を足し算とみなすと、ブール代数Ω(A)はベキ等半環（ISR）でもある点に注意してください。単にベキ等半環であるだけでなく、Ω(A)は可換（掛け算が交換する）ベキ等半環になっています。

可換なベキ等演算と順序

ホムセットNDMap(S, T)における足し算+、ブール代数Ω(A)における∧と∨は、いずれも可換なベキ等演算です。可換なベキ等演算があると、それから順序を定義することができます。演算記号は + を使うことにして：

  • x≦y ⇔ x + y = y

演算 + が可換でベキ等なことを使えば次の性質を導くことができます。

  1. x≦x
  2. x≦y かつ y≦z ならば x≦z
  3. x≦y かつ y≦x ならば x = y

NDMap(S, T)の場合は、+から定義される順序は、∀s.(f(s)⊆g(s)) として定義される順序と一致します。Ω(A)では、∧が定義する順序と∨が定義する順序が一致して、常識的な順序の定義になります。順序から演算を定義することもできますが、後で使う予定がないので省略します。

ガード演算

p∈Ω(S)、f:S→T とします。fはNDMap(S, T)の射です。p・f:S→T を次のように定義します。

  • p・f = f|[p]

ここで、[p]は条件pの外延である集合（[p]⊆S）、縦棒記号は制限を表します。具体的に書き下すと：

  • (p・f)(s) = (if p(s) then f(s) else 空集合)

p・f を、fをpによりプレガードした射と呼びます。記号「・」で表される演算はプレガード演算です。プレガード演算は次のような性質を持ちます。

  1. p・(f + g) = p・f + p・g
  2. (p∨q)・f = p・f + q・f
  3. (p∧q)f = p・(q・f)

∨を+、∧を併置に置き換えてみると：

  1. p・(f + g) = p・f + p・g
  2. (p + q)・f = p・f + q・f
  3. (pq)f = p・(q・f)

そうです。スカラー乗法の公理と同じですよね。ブール代数Ω(S)をスカラーの半環と考えて、ホムセットNDMap(S, T)は、可換半環の上の加群になっているのです。ただし、引き算は定義できない点には注意してください。単に「加群」ではなくて、半加群と呼ぶほうが混乱がないような気がしますが、用語「半加群」はあまり使われてないようです。

f:S→T、q∈Ω(T) に対して、ポストガード f・q:S→T は次のように定義します。

  • f・q = f∩[q]

ほんとは、「・」とは別な記号を使ったほうがいいのでしょうが、スカラー（ブール代数の要素）が左にくるか右にくるかで区別ができるのでいいとしましょう。このポストガードは、右からのスカラー乗法の公理を満たします。

結局、ホムセットNDMap(S, T)は、プレガードにより左Ω(S)-加群、ポストガードにより右Ω(T)-加群の構造を持ちます。特に、エンドォセットNDMap(S, S)は、両側Ω(S)-加群の構造を持ちます。次の等式に注目 -- これは直接的に確認できます。

  • (f・q);g = f;(q・g)

ホーア式

さて、いよいよホーア式（ホーア・トリプル）の登場です。今回は、構文論と意味論をあまり区別しないで、モデル領域のなかでホーア式を定義してしまいましょう。非決定性写像の圏NDMapの各対象S（Sは集合）にはブール代数Ω(S)が付随している状況で考えます。

p∈Ω(S)、f:S→T, q∈Ω(T) があるとき、これらを組にした (p, f, q) がホーア式です。通常ホーア式は、{p}f{q} または p{f}q と記されます。ここでは、p{f}q を採用します。ホーア式の伝統的・標準的な解釈は知っているものとして、圏NDMap（とブール代数の集まり）のなかにホーア式をエンコードすることにします。

NDMapは具体的な圏なので、p{f}q のエンコードは、集合や要素を切った張ったすれば何種類もできます。例えば、次のような定式化があるでしょう。

  • Im(p・f) ⊆ [q]

fの逆像（写像の場合と類似の定義）をf-1とすると、次のようにも書けます。

  • [p]⊆f-1([q])

ただし、これらは代数的に扱いやすいとは言えないので、p{f}q の表現としては次がいいと思います。

  • p・f ⊆ f・q

形が単純なのがいいでしょ。

この「⊆」による不等式は、NDMap(S, T) の上で解釈されて、次の意味を持ちます。

  • 任意の s∈S に対して、(p・f)(s) ⊆ (f・q)(s)

プレガードとポストガードの定義を思い出して (p・f)(s) ⊆ (f・q)(s) を書き換えれば：

  • (f|[p])(s) ⊆ f(s)∩[q]

(f|[p])(s) を、p(s) = 0 のときと p(s) = 1 のときに分けてみます。

  1. p(s) = 0 のとき： 空集合 ⊆ f(s)∩[q]
  2. p(s) = 1 のとき： f(s) ⊆ f(s)∩[q]

上は常に成立するので、下のほうだけが問題になります。一般に、A ⊆ A∩B とはどういうことか？ と考えてみると、それは A ⊆ B ってことですから、f(s) ⊆ [q] が出てきます。

以上をまとめると、(f|[p])(s) ⊆ f(s)∩[q] であるとは：

  1. p(s) = 0 のときは、成り立つ
  2. p(s) = 1 のときは、f(s) ⊆ [q] のこと

もう少しプログラムっぽい表記で書いてみると：



if (p(s)) {

  return q(f(s))

} else {

  return true;

}

はい、ホーア式に関する判定条件そのものですね。q(f(s)) の正確な意味は、「t∈f(s) である任意のtに関して q(t)」です。

等式的な表現

p・f ⊆ f・q は十分に美しい表現だと思いますが、「不等式の形をしているのが気に入らない」という人がいるかもしれません。等式的な定義に直してみます。

プレガード演算もポストガード演算も順序を保存します。これは、足し算を保存することと、順序が足し算から誘導されることからわかります（直接確認してもいいです）。また、次の不等式／等式も心にとめておいてください。

  1. p・f ⊆ f
  2. f・q ⊆ f
  3. p・(p・f) = p・f
  4. (f・q)・q = f・q

それで、示すべき等式は p・f・q = p・f です。

仮定である p・f ⊆ f・q の両辺に p をプレガードして、すぐ上の等式を使うと p・f ⊆ p・f・q がでます。いつでも成立している f・q ⊆ f の両辺に p をプレガードすれば、p・f・q ⊆ p・f 。この2つの不等式から p・f・q = p・f が出ます。

逆も簡単です。まず、p・(f・q) ⊆ f・q は常に成立します。等式 p・f・q = p・f を使って不等式の左辺を置き換えると、p・f ⊆ f・q が出ます。

まとめと予告

ホーア式を非決定性写像の圏NDMapで定式化しました。圏の対象Sにはブール代数Ω(S)が付随していて、ブール代数係数の両側加群がたくさん集まった構造を持っています。

この定式化では、条件（命題）はΩ(S)、Ω(T)のなかに入っていて、実行文は S→T の射により意味付けされます。条件と実行文はまったくの別物です。これは、とてもスッキリしているのですが、現実には条件と実行文を完全に区別できないこともあります。条件（論理式）の評価が副作用を持ったり、実行文の成功・失敗が真偽として評価されるようなことがあるからです。

次回（続き）では、条件と実行文をあまり区別しない方法を紹介します。エクスペクテーションの定式化では、条件と実行文を区別しません。