https://m-hiyama.hatenablog.com/entry/2026/02/28/173445

「ホーア論理とホーアオートマトン 1/n」の続きです。文字の色の約束は前回と同じです。「ホーア論理とホーアオートマトン 1/n // 文字の色の約束」を確認してください。$`\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{\T}[1]{ \text{#1} }
\newcommand{\HoareAutom}{\mathbf{HoareAutom}}
\newcommand{\SimpleHoareAutom}{ \mathbf{SimpleHoareAutom} }
`$

内容：

シリーズ・ハブ記事

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

ラベル付き遷移系とオートマトン

ラベル付き遷移系とオートマトンを（定義だけ）ザッと復習しておきましょう。この節で述べるラベル付き遷移系／オートマトンは決定性〈deterministic〉なものです。決定性ではないラベル付き遷移系／オートマトンについては後の節で述べます。

ラベル付き遷移系〈labeled transition system | LTS〉とは、以下の3つの構成素〈constituents〉からなる構造です。

状態空間〈state space〉 $`S`$
$`S`$ は集合
ラベル達の集合〈set of labels〉 $`A`$
$`A`$ は集合
遷移写像〈transition map〉 $`\tau`$
$`\tau : S\times A \to S`$ は写像

$`S`$ の要素は、状態点〈state point〉、あるいは単に状態〈state〉と呼ばれます。$`A`$ の要素は、ラベル〈label〉、アクションラベル〈action label〉、アクション〈action〉などと呼ばれます。記号〈symbol〉、名前〈name〉は（今の文脈では）ラベルと同義語なので、アクション記号〈action symbol〉、アクション名〈action name〉などの言葉も使われます。ラベル達の集合 $`A`$ はアルファベット〈alphabet〉ともいいます。

集合 $`A`$ のリストの集合 $`\mrm{List}(A)`$ を $`A^*`$ とも書きます。リストの連接〈concatenation〉演算を $`\#`$ 、空リスト〈空列〉を $`\varepsilon`$ として、$`(A^*, \#, \varepsilon)`$ はモノイドになります。遷移写像 $`\tau`$ は、次の写像 $`\widetilde{\tau}`$ に持ち上げ〈拡張〉できます。

$`\quad \widetilde{\tau} : S\times A^* \to S \In \mbf{Set}`$

$`\widetilde{\tau}`$ は、モノイドの（集合への）右作用〈right action〉になります。これは、次の法則を満たします。

$`\text{For }s \in S,\; a, b\in A^* \\
\quad \widetilde{\tau}(\widetilde{\tau}(s, a), b) =
\widetilde{\tau}(s, a\mathop{\#} b) \\
\quad \widetilde{\tau}(s, \varepsilon) = s
`$

ここで、言葉に関して注意しておきます。「アクション」は曖昧多義語になります。文脈により次のような複数の意味を持ちます。

集合 $`A`$ の要素、ラベルと同義
$`a\in A`$ に対して、$`S\ni s \mapsto \tau(s, a)\in S`$ で定義される写像
遷移写像 $`\tau`$ をアクション〈作用〉と呼ぶこともある。
拡張された遷移写像 $`\widetilde{\tau}`$ をアクション〈作用〉と呼ぶこともある。$`\widetilde{\tau}`$ は右作用だが左作用もある。
$`a\in A^*`$ に対して、$`S\ni s \mapsto \tilde{\tau}(s, a)\in S`$ で定義される写像

オートマトン〈automaton〉は、ラベル付き状態遷移系 $`(S, A, \tau)`$ に、2つの部分集合 $`I, F\subseteq S`$ を追加した構造 $`(S, A, \tau, I, F)`$ です。

始状態〈initial state〉の集合 $`I`$
一点だけの集合 $`\{i\} \subseteq S`$ のことが多い。空集合を許すことも稀にある。
終状態〈final state〉の集合 $`F`$
$`S`$ の、空ではない任意の部分集合。

オートマトンでは、オートマトンにより受理される言語〈language accepted by automata〉という概念が定義できます。例えば、有限オートマトンで受理される言語は正規言語〈regular language〉です。

単純ホーアオートマトン

一般的なホーアオートマトンの定義の前に、単純ホーアオートマトンを定義しておきましょう。単純ホーアオートマトンは、通常のオートマトン（前節）を僅かに拡張したものです。

単純ホーアオートマトン〈simple Hoare automaton〉は、以下の5つの構成素からなる構造です。

状態空間〈state space〉 $`S`$
$`S`$ は集合
アクションラベル達の集合〈set of action labels〉 $`A`$
$`A`$ は集合
遷移写像〈transition map〉 $`\tau`$
$`\tau : S\times A \to S`$ は写像
述語ラベル達の集合〈set of predicate labels〉 $`P`$
$`P`$ は集合
観測写像〈observation map〉 $`\omicron`$
$`\omicron : S\times P \to \mbf{B}`$ は写像（'$`\omicron`$' はラテン文字オーではなくて、ギリシャ文字オミクロン）
$`\mbf{B}`$ は二値の真偽値の集合 $`\mbf{B} = \{\mrm{T}, \mrm{F}\}`$

$`P`$ の要素は、述語ラベル〈predicate label〉、または単に述語〈predicate〉と呼ばれます。「述語」も曖昧多義語になります。次の複数の意味を持ちます。

$`P`$ の要素のこと、述語ラベルと同義
$`p\in P`$ に対して、$`S\ni s \mapsto \omicron(s, p)\in \mbf{B}`$ で定義される写像

これらは、論理における「述語記号〈predicate symbol〉」「述語」と同じです。

単純ホーアオートマトンは、特別な場合としてラベル付き遷移系／オートマトンを包摂します。まず、単純ホーアオートマトンの述語ラベル達の集合 $`P`$ を空集合にしてみましょう。すると、観測写像 $`\omicron`$ は次の形になります。

$`\quad \omicron : S\times \emptyset \to \mbf{B} \In \mbf{Set}`$

$`S\times \emptyset = \emptyset`$ なので、$`\omicron`$ は空集合から $`\mbf{B}`$ への唯一の写像になります。これは無視してかまいません。結局、述語ラベルがひとつもない単純ホーアオートマトンはラベル付き遷移系と同じことです。

次に、述語ラベル達の集合 $`P`$ が二元集合 $`\{i, f\}`$ の場合を考えます。2つの集合 $`I, F`$ を次のように定義します。

$`\quad I := \{s\in S \mid \omicron(s, i) = \mrm{T} \}`$
$`\quad F := \{s\in S \mid \omicron(s, f) = \mrm{T} \}`$

すると、$`(S, A, \tau, I, F)`$ はオートマトンになります。これで、単純ホーアオートマトンは（通常の）オートマトンを包摂することも分かりました。

モノイド付きモノイド圏のなかの単純ホーアオートマトン

単純ホーアオートマトンに関して何かを議論すれば、特別な場合としてラベル付き遷移系／オートマトンにもその議論は適用できます。この節では、単純ホーアオートマトンを、集合圏以外の圏のなかで定義してみます。

単純ホーアオートマトンの定義を、圏論を前提とした指標〈signature〉で書いてみます。指標については、（必要があれば）以下の過去記事を参照してください。

単純ホーアオートマトンの指標は：

$`\T{signature }\mrm{SimpleHoareAutom}\: \{\\
\quad \T{sort } S \In \mbf{Set}\\
\quad \T{sort } A \In \mbf{Set}\\
\quad \T{operation }\tau : S\times A \to S \In \mbf{Set}\\
\quad \T{sort } P \In \mbf{Set}\\
\quad \T{operation }\omicron : S\times P \to \mbf{B} \In \mbf{Set}\\
\}
`$

この指標を、集合圏 $`\mbf{Set}`$ とは限らない圏 $`\cat{C}`$ における指標に書き換えます。ただし、圏 $`\cat{C}`$ が何でもいいわけではありません。直積 $`\times`$ に相当するモノイド積 $`\otimes`$ を持っているとします。つまり、$`\cat{C} = (\cat{C}, \otimes, \mbf{I})`$ はモノイド圏〈monoidal category〉です。また、二値真偽値の集合 $`\mbf{B}`$ に相当する対象が固定されている必要があります。$`\mbf{B}`$ に相当する対象を $`M \in |\cat{C}|`$ とします。後々の都合から、$`M`$ は $`\cat{C}`$ 内のモノイド対象〈monoid object〉だと仮定します。

まとめると：

圏 $`\cat{C}`$ はモノイド圏である。
$`\cat{C}`$ 内のモノイド $`(M, \cdot, e)`$ が固定されている。

モノイド圏 $`\cat{C}`$ とモノイド対象 $`M = (M, \cdot, e) \In \mrm{Mon}(\cat{C})`$ の組み合わせ $`(\cat{C}, M)`$ をモノイド付きモノイド圏〈monoical category with a monoid〉と呼ぶことにします。

$`(\cat{C}, M)`$ がモノイド付きモノイド圏だという前提で、圏 $`\cat{C}`$ 内の単純ホーアオートマトンの指標は次のように書けます。

$`\T{signature }\mrm{SimpleHoareAutom}\: \{\\
\quad \T{sort } S \In \cat{C}\\
\quad \T{sort } A \In \cat{C}\\
\quad \T{operation }\tau : S\otimes A \to S \In \cat{C}\\
\quad \T{sort } P \In \cat{C}\\
\quad \T{operation }\omicron : S\otimes P \to M \In \cat{C}\\
\}
`$

この形に書いてしまえば、単純ホーアオートマトンのあいだの準同型射〈homomorphism〉の定義は容易です。ローヴェア〈William Lawvere〉の関手意味論〈functorial semantics〉の流儀に従えばいいのです。

$`F = (S, A, \tau, P, \omicron)`$ と $`F' = (S', A', \tau', P', \omicron')`$ を2つの単純ホーアオートマトンだとして、そのあいだの準同型射は次のような射達です。

$`f: S \to S' \In \cat{C}`$
$`g: A \to A' \In \cat{C}`$
$`h: P \to P' \In \cat{C}`$

以下の図式達の可換性を要求します。

$`\quad\xymatrix{
{S\otimes A} \ar[r]^{\tau} \ar[d]_{f\otimes g}
& S \ar[d]^f
\\
{S'\otimes A'} \ar[r]^{\tau'}
& S'
}\\
\quad \text{commutative }\In \cat{C}
`$

$`\quad\xymatrix{
{S\otimes P} \ar[r]^{\omicron} \ar[d]_{f\otimes h}
& M \ar@{=}[d]
\\
{S'\otimes P'} \ar[r]^{\omicron'}
& M
}\\
\quad \text{commutative }\In \cat{C}
`$

こうして作った単純ホーアオートマトン達の圏を $`\SimpleHoareAutom_{(\cat{C}, M)}`$ とします。モノイド付きモノイド圏を $`(\mbf{Set}, \mbf{B})`$ に具体化すれば、集合圏と二値真偽集合 $`\mbf{B}`$ （論理ANDでモノイドとみなす）に関する単純ホーアオートマトン達の圏ができ上がります。

$`\cat{D}, \cat{E}`$ を $`\cat{C}`$ の部分圏とします。単純ホーアオートマトン達の圏 $`\SimpleHoareAutom_{(\cat{C}, M)}`$ の定義において、以下の制限を付けてでき上がる圏を $`\SimpleHoareAutom_{(\cat{C}, M)}^{\cat{D}, \cat{E}}`$ と書きます。

単純ホーアオートマトンの構造射（上の定義の $`\tau, \omicron`$）を $`\cat{D}`$ の射に制限する。
準同型射の成分達（上の定義の $`f, g, h`$）を $`\cat{E}`$ の射に制限する。

$`\SimpleHoareAutom_{(\cat{C}, M)}^{\cat{D}, \cat{E}}`$ の具体例はすぐ後で出します。

決定性、非決定性、半決定性

$`M = (M, \mu, \eta)`$ を集合圏 $`\mbf{Set}`$ 上のモナド〈monad〉とします。モナドのクライスリ圏〈Kleisli category〉を $`\mrm{Kl}(M/\,\mbf{Set})`$ と書くことにします。

$`\mrm{Pow}_* = (\mrm{Pow}_*, \mu, \eta)`$ を、共変のベキ集合関手〈covariant powerset functor〉 $`\mrm{Pow}_*:\mbf{Set} \to \mbf{Set}`$ に、通常のモナド乗法〈monad multiplication〉とモナド単位〈monad unit〉を一緒にしたモナドとします。

$`\mbf{NDet} := \mrm{Kl}(\mrm{Pow}_*/\,\mbf{Set})`$ と定義します。つまり、圏 $`\mbf{NDet}`$ は：

$`|\mbf{NDet}| = |\mbf{Set}|`$
$`\mbf{NDet}`$ の射 $`f:A\to B`$ は、$`f:A \to \mrm{Pow}(B) \In \mbf{Set}`$ （クライスリ射〈Kleisli morphism〉）のこと
結合と恒等は、クライスリ射のクライスリ結合〈Kleisli composition〉とクライスリ恒等〈Kleisli {identity | unit}〉

圏 $`\mbf{NDet}`$ の射を非決定性写像／非決定性関数〈nondeterministic {map | function}〉と呼びます。

$`\mrm{Maybe} = (\mrm{Maybe}, \mu, \eta)`$ を、メイビーモナド〈Maybe monad〉とします。メイビーモナドの台関手〈underlying functor〉は、おおよそ $`X \mapsto X + \{\bot\}`$ という対応です。$`\bot`$ は関数〈写像〉が未定義であることを表す記号です。

$`\mbf{Partial} := \mrm{Kl}(\mrm{Maybe}/\,\mrm{Set})`$ と定義します。つまり、圏 $`\mbf{Partial}`$ は：

$`|\mbf{Partial}| = |\mbf{Set}|`$
$`\mbf{Partial}`$ の射 $`f:A\to B`$ は、$`f:A \to \mrm{Maybe}(B) \In \mbf{Set}`$ （クライスリ射）のこと
結合と恒等は、クライスリ射のクライスリ結合とクライスリ恒等

圏 $`\mbf{Patial}`$ の射を部分写像／部分関数〈partial {map | function}〉と呼びます。

用語のフレーバーを揃えるために、次の別名を導入します。

圏 $`\mbf{Partial}`$ を $`\mbf{SDet}`$ とも呼ぶ。
圏 $`\mbf{SDet}`$ の射を半決定性写像／半決定性関数〈semi-deterministic {map | function}〉とも呼ぶ。

同様に、記法・用語を揃えるために、$`\mbf{Set}`$ を $`\mbf{Det}`$ とも書き、その射を決定性写像／決定性関数〈deterministic {map | function}〉とも呼びます。決定性関数とは単なる関数のことです。

$`\mbf{Det}\subseteq \mbf{SDet}\subseteq \mbf{NDet}`$ （部分圏の系列）とみなします。関係達の圏 $`\mbf{Rel}`$ は $`\mbf{NDet}`$ と同一視できますが、ここでは、$`\mbf{Rel} \cong \mbf{NDet}`$ （圏同型）とみなします。いずれにしても、$`\mbf{Rel}`$ と $`\mbf{NDet}`$ は事実上同じ圏です。

単純ホーアオートマトンの変種達

前々節と前節で述べたことを利用すると、単純ホーアオートマトンの変種達と変種達からなる圏を定義できます。

$`\SimpleHoareAutom_{(\mbf{Set}, \mbf{B})}^{\mbf{Set}, \mbf{Set}}`$ は、最初に述べた単純ホーアオートマトン達の圏になります。この圏は：

対象は、決定性単純ホーアオートマトンである。つまり、遷移写像も観測写像も決定性である。
射は、決定性準同型射である。つまり、準同型射のすべての成分は決定性である。

$`\SimpleHoareAutom_{(\mbf{NDet}, \mbf{B})}^{\mbf{Det}, \mbf{NDet}}`$ は：

対象は、決定性単純ホーアオートマトンである。つまり、遷移写像も観測写像も決定性である。
射は、非決定性準同型射である。つまり、準同型射のすべての成分は非決定性である。

ここから先、主に扱う圏は $`\SimpleHoareAutom_{(\mbf{SDet}, \mbf{B})}^{\mbf{SDet}, \mbf{Det}}`$ です。この圏は：

対象は、半決定性単純ホーアオートマトンである。つまり、遷移写像も観測写像も半決定性である。
射は、決定性準同型射である。つまり、準同型射のすべての成分は決定性である。

半決定性は決定性を含むので、次のような部分圏の関係があります。

$`\quad \SimpleHoareAutom_{(\mbf{Det}, \mbf{B})}^{\mbf{Det}, \mbf{Det}} \subseteq
\SimpleHoareAutom_{(\mbf{SDet}, \mbf{B})}^{\mbf{SDet}, \mbf{Det}}
`$

$`\SimpleHoareAutom_{(\mbf{SDet}, \mbf{B})}^{\mbf{SDet}, \mbf{Det}}`$ を、単純ホーアオートマトンの圏の“デフォルト”と考えます。なので、次のような記法の約束をします。

$`\quad \SimpleHoareAutom :=
\SimpleHoareAutom_{(\mbf{SDet}, \mbf{B})}^{\mbf{SDet}, \mbf{Det}}
`$

今後、何の断りもなく「単純ホーアオートマトンの圏」と言った場合、$`\SimpleHoareAutom_{(\mbf{SDet}, \mbf{B})}^{\mbf{SDet}, \mbf{Det}}`$ を意味します。

ホーアオートマトンの圏に向けて

単純ホーアオートマトン達の圏 $`\SimpleHoareAutom`$ は、ラベル付き遷移系達の圏や（通常の）オートマトン達の圏を含みます（そう考えてよい）。十分一般的な圏のように思えますが、プログラムの実行やテストをモデル化するには不十分です。単純ホーアオートマトンより一般的な構造であるホーアオートマトンと、ホーアオートマトン達の圏を考える必要があります。

ホーアオートマトンは単純ホーアオートマトンの一般化、ホーアオートマトンのなかでも単純なものが単純ホーアオートマトンという関係です。しかし、単純ホーアオートマトンの圏とホーアオートマトンの圏はまったく違います。圏の作り方の発想が別物です。

単純ホーアオートマトン達の圏 $`\SimpleHoareAutom`$ では、対象が単純ホーアオートマトンでした。ホーアオートマトン達の圏 $`\HoareAutom`$ では、単純ホーアオートマトンの一般化であるホーアオートマトンが射です（対象ではない！）。対象はホーア指標〈Hoare signature〉と呼ぶ記号的／ラベル的な存在物です。

$`\Sigma, \Gamma, \Delta`$ を、ホーア指標（圏 $`\HoareAutom`$ の対象）として、$`F, G`$ をホーアオートマトン（圏 $`\HoareAutom`$ の射）とします。

$`\quad F:\Sigma \to \Gamma, \: G: \Gamma \to \Delta \In \HoareAutom`$

ならば、射の結合〈composition〉（図式順） $`F\rhd G`$ を定義できます。$`F\rhd G`$ はまたホーアオートマトンです。圏論的な結合 $`\rhd`$ は、ソフトウェア・コンポネントの結合として現実によく使われている方法のモデルになっています。逆に言うと、結合 $`\rhd`$ がないと現実のモデル化が難しいのです。

と、ホーアオートマトン達の圏 $`\HoareAutom`$ の存在を匂わせたところで、今日はここまで（「今日はここまで」参照）。