ホーア論理とホーアオートマトン 4/n ： 隠蔽

「ソフトウェア・システムの正しさをテストと証明で示したい」という願望が、一連の記事の動機です。この願望は、ソフトウェアを作る人は誰でも持っている願望でしょう。しかし、徳目主義・根性主義で「やるべきだ、頑張ろう」と言ってみても埒が明きません。「正しさをテストと証明で示す」方法論、あるいは方法論の背景・基盤となる理論がないとハナシになりません。

ここで提示する理論は新しいものではありません。ホーア論理は、ソフトウェアの記述と証明の方法として最も古く最もよく知られたものでしょう。ホーア論理以外に、ゴグエン〈Joseph Goguen〉の隠蔽仕様／隠蔽代数〈hidden specification / hidden algebra〉*1が非常に有用なので今回紹介します。

ゴグエンが使った用語「隠蔽〈hidden〉」は、今さら変えるわけにもいきませんが、安易な連想からの誤認・誤解を誘発しやすいので、その点は丁寧に説明・注意します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\twoto}{\Rightarrow}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\o}[1]{\overline{#1} }
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
\newcommand{\In}{\text{ in } }
%\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
\newcommand{\tto}{ \mathrel{!\!\!\to} }
\newcommand{\T}[1]{ \text{#1} }
\newcommand{\vinfer}{ \downdownarrows }% vertical meta rule (infer)
`$

内容：

• 文字の色の約束（追加あり）
• 隠蔽状態ソート付き指標
• 隠蔽状態ソート
• メソッド
• メソッドの単純化表示
• 様々なメソッドとその単純化表示
  • コマンド
  • コンストラクタ
  • 静的メソッド
• プロファイルの書き換え、ホムセット間対応、推論
• メイヤー指標

シリーズ・ハブ記事

• ホーア論理とホーアオートマトン 1/n

文字の色の約束（追加あり）

記事内で使う文字の色に関する約束は「ホーア論理とホーアオートマトン 1/n // 文字の色の約束」に書いています。要約すると：

• 青い文字 ： よく知られた用語
• 赤い文字 ： そこで定義される用語
• マゼンタの文字 ： 記事の後方または引き続く記事内で定義・説明される用語

もうひとつ色を追加します。茶色の文字は、記事の前の部分、またはシリーズ内の過去記事で既に定義済みの用語です。過去記事を読んでいるなら“知られた用語”のはずですが、注意を促したほうがよさそうなときに茶色の文字を使用します。過去記事で定義済みの用語をすべて茶色にするのは現実的でないし、煩雑になるので、あくまで注意を促したい場合だけ茶色です。

隠蔽状態ソート付き指標

ここから先、指標の概念を全面的に使います。指標については、「ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語」の2つの節「指標、シグニチャ、プロファイル、インターフェイス」「指標」で説明しています。より詳しくは次の過去記事を参照してください。

• 構造記述のための指標と名前 1/n 基本 （続きの記事あり）
• インターフェイスとしての指標、設計者と利用者と実装者
• 指標から名前の削除 （続きの記事あり）
• 指標の具体例： ν-インスティチューションのために

「指標」という語を含むすべての過去記事は：

• 指標 の検索結果:

「ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語 // オブジェクト指向風の指標」において、「オブジェクト指向風の指標」という言葉を使いました。この記事では、オブジェクト指向風の指標が何であるかを正確に記述することにします。

半決定性写像達の圏 $`\mbf{SDet}`$（「ホーア論理とホーアオートマトン 2/n // 決定性、非決定性、半決定性」参照）における指標は、次の3つの部分からなります。

1. ソート〈型 | 集合 | 圏 $`\mbf{SDet}`$ の対象〉の宣言（0個以上任意個）
2. オペレーション〈{半決定性 | 部分}{関数 | 写像} | 圏 $`\mbf{SDet}`$ の射〉の宣言（0個以上任意個）
3. 法則〈公理 | 制約 | 条件〉の宣言（0個以上任意個）

法則はホーアトリプルにより記述すると仮定します。法則が無い指標は無法則指標と呼ぶのでした。

ゴグエン〈Joseph Goguen〉達の用語法では、オブジェクト指向風の指標を隠蔽仕様〈hidden specification〉と呼びます。

「ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語 // 指標」で述べたように、「指標〈signature〉」という言葉は人により意味が変わります。ゴグエンは指標に法則を含めません。法則を含めたものは仕様〈specification〉と呼びます。つまり（'＠'、'≡' については「
ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語 // 曖昧多義語、同義語・類義語」参照）：

　　指標＠檜山 ≡ 仕様＠ゴグエン
　　無法則指標＠檜山 ≡ 指標＠ゴグエン

僕の用語法（僕一人ってことじゃないですよ！）で言えば：

　　オブジェクト指向風指標 ≡ 隠蔽指標

ただし、「隠蔽」という形容詞を付けただけでは意味不明あるいは誤解されそうなので、より説明的に言えば：

　　オブジェクト指向風指標 ≡ 隠蔽状態ソート付き指標

指標に現れるソートのひとつに（ひとつだけに）、「これは隠蔽状態のソートですよ」と示すマークを付けます。すると、その指標は隠蔽状態ソート付き指標になります。言い換えると、ソートのひとつ（ひとつだけ）に、隠蔽状態ソート〈hidden state sort〉のマークが付いた指標が隠蔽状態ソート付き指標〈signature with hidden state sort〉です。次節でより詳しく説明します。

隠蔽状態ソート

オブジェクト指向では、オブジェクトの内部構造に関する情報は外部に公開しないことが推奨されています。この方針・原則・技法を情報隠蔽〈information hiding〉と呼びます。ゴグエンの隠蔽は、（おそらく）情報隠蔽から来ているのでしょう。外部に見せてはいけないソート〈型 | 集合〉を hidden とマークします。hidden とマークされたソートは、オブジェクトの内部状態を表します。ここでは、隠蔽されるだけでなくて状態でもあることを強調して、隠蔽状態ソート〈hidden state sort〉という言葉を使います。

「ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語 // オブジェクト指向風の指標」で例にした IntStack で、隠蔽状態ソートを明示すると次のようになります。

$`\T{signature }\mrm{IntStack} \In \mbf{SDet}\: \{\\
\quad \T{hidden state sort }S\\
\quad \T{operation }\mrm{isEmpty} : S \tto \mbf{B}\\
\quad \T{operation }\mrm{top} : S \to \mbf{Z}\\
\quad \T{... 以下省略 ...}\\
\}
`$

実在のプログラミング言語のオブジェクト指向風指標〈インターフェイス〉では、隠蔽状態ソートは暗黙化されることが多いです。指標〈インターフェイス〉に必ず1個だけ隠蔽状態ソートがあるなら、省略してしまっていいだろう、ということです。

この暗黙化（明示的には書かないこと）は、書く手間を減らす効果はありますが、書いてないので認識出来ない事態をもたらします。隠蔽状態ソートを認識できないことは、たいへんに非常にとってもマズイので、僕の一連の記事では、隠蔽状態ソートを絶対に省略しないことにします*2。

指標内に、隠蔽状態ソート以外のソートが現れることもあります。例えば、スタックに積む値を整数ソート〈整数型 | 整数達の集合〉の値に固定せずに、不定の（固定してない）ソート $`V`$ を許すことにします。すると、スタックの指標は次のようになります。

$`\T{signature }\mrm{Stack} \In \mbf{SDet}\: \{\\
\quad \T{hidden state sort }S\\
\quad \T{sort }V\\
\quad \T{operation }\mrm{isEmpty} : S \tto \mbf{B}\\
\quad \T{operation }\mrm{top} : S \to V\\
\quad \T{... 以下省略 ...}\\
\}
`$

不定のソート〈型 | 集合〉 $`V`$ は、ジェネリックスの型パラメータと同じことです。指標内に不定のソートを許す事と、ソート〈型 | 集合〉の引数渡しを導入する事はメカニズムとしては違います*3。が、得られる効果は事実上同じです。

ゴグエン達の用語法では、隠蔽状態ソートではないソートは可視ソート〈visible sort〉と呼びます。が、「可視」は誤解をまねきやすいので使わないことにします。

「隠蔽 ←→ 可視」は反対語のペアですが、多くの人は名前〈識別子〉の public〈公開 | 可視〉と private〈内部専用 | 非公開 | 不可視 | 隠蔽〉を連想するでしょう。しかし、ソートが可視であること（隠蔽状態ソートではないこと）は、名前の可視性とは直接的な関係はありません。「隠蔽状態ソートではない」の意味で「可視」という形容詞を使わずに、「隠蔽状態ソートではないソート＝通常ソート〈ordinary sort〉」と呼ぶことにします。「可視」を使うのは、名前〈識別子〉の public/private と関連する場合にします。

指標に現れるソートは、最大で1個（0個または1個の）の隠蔽状態ソートと、任意個数（0個でもよい）の通常ソートです。「隠蔽状態ソート」「通常ソート」という2つの用語はバランスが悪くぎごちないですが、別の文脈で現れる「不可視ラベル」「可視ラベル」と混同されるとエライこと（話がグチャグチャ）になるので、用語のコンフリクトを避けることを最優先します。

「隠蔽状態ソート」が長ったらしくてイヤなら、「隠蔽ソート」と省略するのは許します。「隠蔽状態ソート付き指標」が長ったらしくてイヤなら、「隠蔽指標」と省略するのも許します。が、省略することによって本来の定義を見失わないように注意してください。

隠蔽状態ソート付き指標は、ただひとつのソートが隠蔽状態ソートだとマークされた指標ですが、指標に含まれるオペレーションがすべてメソッド〈method〉であることも要求します。となると、メソッドの正確な定義が必要になります。次節で定義しましょう。

メソッド

オペレーション〈{半決定性 | 部分}{関数 | 写像}〉がメソッドであることは、隠蔽状態ソートに対して相対的に決まります。以下、$`S`$ が隠蔽状態ソートだとします。

オペレーション $`m`$ がメソッド〈method〉であるのは、次のプロファイルを持つときです。

$`\quad m : S\times A \to S \times B \In \mbf{SDet}`$

$`S`$ は隠蔽状態ソートだとマークされたソート〈型 | 集合〉でした。$`A`$ は（メソッド $`m`$ の）入力ソート〈input sort〉、または引数ソート〈{parameter | argument} sort〉と呼びます。$`B`$ は（メソッド $`m`$ の）出力ソート〈output sort〉、または戻り値ソート〈return-value sort〉と呼びます。

メソッドの入力ソート／出力ソートは、まったく任意の（勝手に選んだ）ソート〈型 | 集合〉が許されるわけではありません。次の制約があります

• 入力ソートと出力ソートは、既知基本ソート〈known basic sort〉、または指標の通常ソート〈ordinary sort〉の積〈product〉でなければならない。

上の制約内に未定義の言葉（マゼンタ色）が出てきているし、日本語もやや曖昧なので、以下で説明を追加します。

既知基本ソート〈knwon basic sort〉とは、指標を定義する前に、具体的にハッキリと定義されているソート〈型 | 集合〉のことです。数学の習慣だと、既知基本ソート（のラベル〈記号 | 名前〉）は太字の名前にします。例えば、$`\mbf{B}, \mbf{Z}`$ などです。暗黙に $`\mbf{1}`$ （特定されたシングルトン集合 ≡ ユニット型）と $`\mbf{0}`$ （空集合 ≡ ネバー型）は既知基本ソートに入れます。既知基本ソートは必要に応じて増やしてかまいません。例えば、実数の集合である $`\mbf{R}`$ を既知基本ソートに入れてかまいません。特定の時点で、既知基本ソートがどれだけあるかがハッキリしていることが重要です。

ソートの積〈product〉とは、集合の直積のことです。既知基本ソートの積として書けるソート〈型 | 集合〉は既知〈known〉と考えます。既知基本ソートが事前に具体的にハッキリと定義されているソートなので、それらの直積もよく分かっているソートとみなします。

既知ソート（既知基本ソートの直積）から既知ソートへの関数〈写像〉を幾つか選んで、それらを既知基本オペレーション〈known basic operation〉と決めます。既知基本ソートや既知基本オペレーションは、決めること／約束することで定義される概念で、ソート〈型 | 集合〉やオペレーション〈{半決定性 | 部分}{関数 | 写像}〉が生まれつき持っている性質ではありません。

既知基本ソート達と既知基本オペレーション達*4は、暗黙に前提されることが多いです。既知基本ソートと既知基本オペレーションは数が多いこともあるので、全部を列挙したり説明したりするのは大変です。なので「みんながよく知っているヤツだよ」で済まされて暗黙化・省略されます。暗黙化・省略は、（それを認識できなくなる人がいるので）諸悪の根源です。指標を定義する際には、既知基本ソート達と既知基本オペレーション達が事前に決まっていることを強く意識しましょう。

メソッドの入力ソートと出力ソートは、事前に決まっている既知基本ソート（幾つか）と、指標内で宣言された通常ソート（幾つか）の積で書ける必要があります。$`A_1, \cdots, A_n`$ と $`B_1, \cdots, B_m`$ を既知基本ソート／通常ソート（同じものが重複して現れてもよい）として、メソッドのプロファイルは以下の形です。

$`\quad m : S \times (A_1\times \cdots \times A_n) \to S\times (B_1\times \cdots\times B_m) \In \mbf{SDet}`$

$`A := A_1\times \cdots \times A_n,\; B := B_1\times \cdots\times B_m`$ と置いて、次の形に書きます。

$`\quad m : S \times A \to S\times B \In \mbf{SDet}`$

次節以降で、メソッドとその入力ソート／出力ソートの具体例を挙げます。

メソッドの単純化表示

以下は、ソート〈型 | 集合〉 $`V`$ の値を積むスタックの指標です。（決定性〈全域性〉を表す矢印「$`\tto`$」は使わずに、決定性は法則で記述してもかまいません。）

$`\T{signature }\T{Stack}\In \mbf{SDet} \:\{\\
\quad \T{hidden state sort }S\\
\quad \T{sort }V\\
\quad \T{operation }\mrm{isEmpty} : S \tto \mbf{B}\\
\quad \T{operation }\mrm{top} : S \to V\\
\quad \T{operation }\mrm{push} : S \times V \tto S\\
\quad \T{operation }\mrm{pop} : S \to S\\
%
\:\\
\quad \T{... 法則は省略 ...}\\
\}
`$

この指標に出てくるオペレーションはメソッドでしょうか？ 初見では、前節で定義したメソッドの形をしてないように思えます。が、ちょっとした細工でメソッドとみなすことが出来ます。

上記スタックの指標の $`\mrm{isEmpty}, \mrm{top}`$ のように、$`S \to B`$ の形をしたプロファイルを持つオペレーションをクエリー〈query〉と呼びます。$`\mrm{push}`$ のように $`S \times A \to S`$ の形をしたプロファイルを持つオペレーションはコマンド〈command〉と呼びます。

コマンド／クエリーはメイヤー〈Bertrand Meyer〉によるオペレーションの分類です。メイヤーは、隠蔽状態ソート付き指標（オブジェクト指向風のインターフェイス）は、コマンドとクエリーから構成されるべきだ（Command-Query分離の原則〈principle of Command-Query separation〉）と主張しています。以下の過去記事を参照してください。

• メイヤー先生の偉大さとCommand-Query分離

さて、「初見ではメソッドの形をしてないオペレーションを、ちょっとした細工でメソッドとみなす」方法を説明しましょう。基本的なアイディアは、ある条件〈制約〉を満たすメソッドに対して、単純化表示〈simplified presentation〉を見つけることです。

最初の例として、状態を動かさない決定性メソッドを考えます。決定性メソッド $`m`$ が状態を動かさない〈does not move state〉とは、以下の図式が可換となることです。

$`\quad \xymatrix {
{S\times A} \ar[r]^m \ar[d]_{\pi_1}
& {S\times B} \ar[d]^{\pi_1}
\\
S \ar[r]_{\id_S}
&S
}\\
\quad \text{commutative }\In \mbf{Det}
`$

圏が $`\mbf{SDet}`$ ではなくて $`\mbf{Det} = \mbf{Set}`$ であることに注意してください。メソッド $`m`$ が決定性〈全域〉なので、$`\mbf{Det} = \mbf{Set}`$ で考えています。

$`\pi_1`$ は第一射影です。上記可換図式は、メソッド $`m`$ の第一成分（状態遷移パート〈state-transition part〉は恒等写像だと言っています。要素を追いかけると次のようになります。

$`\quad \xymatrix {
{(s, a)} \ar@{|->}[r]^-m \ar@{|->}[d]_{\pi_1}
& {(m_1(s, a), m_2(s, a))} \ar@{|->}[d]^{\pi_1}
\\
s \ar@{|->}[r]_-{\id_S}
&{s = m_1(s, a)}
}
`$

第一成分は $`m_1(s, a) = s`$ で決まってしまうので、第二成分（戻り値パート〈return-value part〉 $`m_2`$ を $`q`$ と置くと、メソッド $`m`$ は $`q`$ だけで決まります。

$`\quad q: S\times A \to B \In \mbf{Det}`$

「決定性の $`m`$ が状態を動かさない」という条件のもとでは、次の一対一対応があります。

$`\quad (m : S\times A \to S\times B)\longleftrightarrow(q : S\times A \to B)`$

これは、条件付きのメソッド $`m`$ がより単純な形の表示 $`q`$ を持つ例です。この場合、$`q`$ は $`m`$ の単純化表示〈simplified presentation〉と呼ぶことにします。単純化表示を持つのはメソッドに条件があるからで、任意のメソッドが単純化表示を持つわけではありません。

上記の指標 $`\mrm{Stack}`$ のオペレーション $`\mrm{isEmpty}`$ は、メソッド $`\mrm{isEmpty0}`$ の単純化表示と解釈できます。

$`\quad (\mrm{isEmpty0} : S\times \mbf{1} \to S\times \mbf{B})\longleftrightarrow( \mrm{isEmpty} : S \to \mbf{B} )`$

単純化表示をもとの形に戻せば、オペレーション $`\mrm{isEmpty}`$ は前節の意味でのメソッドだと言えます。

オペレーション $`\mrm{isEmpty}`$ は決定性〈全域〉でしたが、オペレーション $`\mrm{top}`$ は決定性ではありません。決定性ではない場合の「$`m`$ は状態を動かさない」の定義はちょっと面倒になります。$`\bot`$ を未定義を表す値として、$`\bot = \{\bot\}`$ という略記（記号の乱用）を使うとして、以下の図式の可換性が「$`m`$ は状態を動かさない」ことになります。

$`\quad \xymatrix {
{S\times A} \ar[r]^-m \ar[d]_{\pi^m_1}
& {S\times B + \bot} \ar[d]^{\pi_1 + \id_\bot}
\\
{S+\bot} \ar[r]_{\id_{S + \bot}}
&{S + \bot}
}\\
\quad \text{commutative }\In \mbf{Det}
`$

ここで、$`\pi^m_1`$ は次のように定義されます。

$`\quad \pi^m_1(s,a) := \T{if } m(s, a) = \bot \T{ then }\bot \T{ else } s
`$

決定性のときと同じように、状態を動かさない $`m`$ に対して、$`q:S\times A \to B + \bot`$ が決まります。$`m`$ は単純化表示 $`q`$ を持ち、$`q`$ により $`m`$ を一意的に表示できます（詳細は割愛）。

様々なメソッドとその単純化表示

前節で述べたことは、$`q: S\times A \to B`$ のようなプロファイルのオペレーションは、$`m: S\times A \to S\times B`$ というメソッドの単純化表示とみなせるということでした。ただし、メソッド $`m`$ は「状態を動かさない」という前提が付きます。

他にも、あるオペレーションが別のメソッドの単純化表示とみなせるケースはあります。もちろん、メソッドに条件が必要です。条件としては、次がよく使われます。

1. メソッドが状態を動かさない。（既出）
2. メソッドの状態遷移パートが状態に寄らない。
3. メソッドの戻り値パートが状態に寄らない。

これらの条件を満たすメソッドは単純化表示を持ちます。そして、単純化表示によりメソッドを一意的に表示できます。

もっとも、単純化表示は技巧的なコジツケのような印象もあります。熱心に追求すべき話題でもないので、ここでは、決定性〈全域〉のメソッドに限って説明します。決定性でない場合は、話が面倒になります（ここでは扱いません）。