このシリーズでやりたいことは、ホーア論理（ホーアトリプルに基づく論理）によりソフトウェアシステムの振る舞いを記述・制約することです。実際に動くソフトウェアシステムは、ホーアオートマトンによりモデル化します。ホーア論理の（あるいはホーアトリプルの）意味論には“軌道集合意味論”（と僕が呼んでいる方法）を使う予定です。
ホーアオートマトン／軌道集合意味論は、実は物理的手法です。「物理的手法」が言い過ぎ（物理に失礼）なら、物理的比喩を使う手法と言い換えてもいいです。僕は物理はろくに知らないのですが、それでも物理と計算科学のアナロジーには興味を持ち、そのアナロジーをずっと意識しています。
今回は、記事タイトルにある記号バンドルを準備した後で、物理-計算科学アナロジーに関するラフな説明をします。ラフな説明でも、「どうしてそのように定義するか／定式化するか」の気持ち・ココロを納得するには役に立つと思います。
最後は個人的回想を含めたオシャベリです。なお、記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\twoto}{\Rightarrow}
%\newcommand{\id}{\mathrm{id} }
\newcommand{\In}{\text{ in } }
%\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
\newcommand{\tto}{ \mathrel{!\!\!\to} }
\newcommand{\parto}{\supset\!\to}
\newcommand{\T}[1]{ \text{#1} }
`$
内容：
シリーズ・ハブ記事
オートマトンのアルファベットと指標のアルファベット
ホーアオートマトンの定義はまだしてませんが、「ホーア論理とホーアオートマトン 2/n // 単純ホーアオートマトン」で定義した単純ホーアオートマトンは、ホーアオートマトンのなかで特に簡単な部類のものです。現時点では、ホーアオートマトンとは単純ホーアオートマトンだと思ってかまいません。もっと簡単な例で考えたいなら、ラベル付き遷移系だけを想定してもいいです。以下で「オートマトン」は、単純ホーアオートマトンやラベル付き遷移系の意味です。（将来／未来において）一般的なホーアオートマトンの定義が済んだ後なら、「オートマトン」はホーアオートマトンと解釈することもできます。
オートマトンには、何種類かのラベルがあります。ラベル付き遷移系ではアクションラベルだけですが、単純ホーアオートマトンなら述語ラベルとアクションラベルの二種類のラベルがありました。一般的なホーアオートマトンではさらにコンストラクタラベルとデストラクタラベルも追加されます。
ラベル〈label〉の同義語として、記号〈symbol〉、名前〈name〉、識別子〈identifier〉などがありました。ときに、ラベルを字〈letter〉と呼ぶこともあります。
すべての種類のすべてのラベルを全部寄せ集めた集合を（オートマトンの）アルファベット〈alphabet〉と呼びます。当面、アルファベットは集合と思っていいですが、実際にはアルファベットがけっこう複雑な構造を持つことがあります。ラベルの種類があるなら、その種類が既に構造（アルファベットが単なる集合ではない）になっています。
$`J`$ が（なんらかの意味の）オートマトンのとき、$`J`$ のアルファベットを $`\mrm{Alphabet}(J)`$ と書きます。直前の段落で注意したように、当面 $`\mrm{Alphabet}(J)\in |\mbf{Set}|`$ と考えます。
$`\Sigma`$ が指標（「ホーア論理とホーアオートマトン 5/n ： 整理と注意 // 指標は無名でも無限でもよい」参照）のとき、$`\Sigma`$ に出現するすべてのオペレーション記号〈オペレーションラベル | オペレーション名〉の集合を、（指標の）アルファベット〈alphabet〉と呼びます。メイヤー指標（「ホーア論理とホーアオートマトン 4/n ： 隠蔽 // メイヤー指標」「ホーア論理とホーアオートマトン 5/n ： 整理と注意 // 多パート指標、属性付き指標」参照）のように、アルファベット（オペレーション名達の集合）が何種類かに分けられているかも知れません。
指標 $`\Sigma`$ のアルファベットを $`\mrm{Alphabet}(\Sigma)`$ と書きます。当面 $`\mrm{Alphabet}(\Sigma)\in |\mbf{Set}|`$ と考えます。
オートマトンのアルファベット $`\mrm{Alphabet}(J)`$ と指標のアルファベット $`\mrm{Alphabet}(\Sigma)`$ は、定義上は違うものです。が、「アルファベット」という呼び名を共有しているのは密接に結びついているからです。オートマトン $`J`$ が指標 $`\Sigma`$ のモデルであるためには、$`\mrm{Alphabet}(\Sigma) \subseteq \mrm{Alphabet}(J)`$ である必要があります（いずれちゃんと説明します）。
（[追記]最初、$`\mrm{Alphabet}(\Sigma) = \mrm{Alphabet}(J)`$ と等式で書いてましたが、一般的には包含関係なので、修正しました。[/追記]）
バンドル
集合論的バンドル〈set-theoretic bundle〉とは、単に写像〈関数〉のことです。実体としては写像に過ぎませんが、用途・文脈・解釈などの“態度・気持ち”が単なる写像とは違います*1。そのため、用語法も変えます。
| 写像 | 集合論的バンドル |
| 域 | 全空間〈{total | entire} space〉 |
| 余域 | 底空間〈base space〉 |
| 写像そのもの | 射影〈projection〉 |
全空間、底空間と呼ぶからといって位相があるわけじゃないです。射影と呼ぶからといって全射を要求しているわけじゃないです。
「集合論的」と形容しているのは、幾何の文脈で出てくるバンドルとは別物だからです。しかし、ここでは集合論的バンドルしか出てこないので、集合論的バンドルを単にバンドル〈bundle〉と呼びます。
$`\pi: E \to B \In \mbf{Set}`$ がバンドルのとき、射影 $`\pi`$ の逆像集合を次のように書きます。
$`\quad E_{@b} := \pi^{-1}(b) = \{x\in E \mid \pi(x) = b\}`$
普通はアットマークを付けませんが、下付き添字が色々な意味で多用されるので、念の為アットマークを付けて逆像集合であることを強調します。逆像集合 $`E_{@b}`$ を、このバンドルの $`b\in B`$ におけるファイバー〈fibre | fiber〉と呼びます。
オートマトンの記号バンドル
$`J`$ をオートマトンとします。オートマトン $`J`$ の状態空間を $`S`$ 、遷移写像を $`\tau`$ とします。$`\tau`$ は次のような{半決定性 | 部分}{写像 | 関数}でした。
$`\quad \tau : S\times \mrm{Alphabet}(J) \to S \In \mbf{SDet}`$
$`\mbf{SDet}`$ は、集合と半決定性写像からなる圏でした（「ホーア論理とホーアオートマトン 2/n // 決定性、非決定性、半決定性」参照）。
アルファベット $`\mrm{Alphabet}(J)`$ にはアクションラベルではないラベル（例えば述語ラベル）が含まれるかも知れません。非アクションラベル $`x`$ に対しては $`\tau(s, x)`$ を未定義にすればいいだけです。$`\tau`$ は適切なペア $`(s, a)`$ に対してだけ定義されます。
オートマトン $`J`$ から、以下のようにしてバンドル $`\pi:E \to B \In \mbf{Set}`$ を作れます。
- $`E := \{(s, a)\in S\times \mrm{Alphabet}(J) \mid \tau(s, a) \T{ が定義されている}\}`$
- $`B := S`$ （底空間は状態空間）
- $`\pi := \pi_1|_{E}`$ （射影は、第一射影の $`E`$ への制限）
$`b\in B`$（$`\T{where }B = S`$）に対するファイバー $`E_{@b}`$ は次のようです。
$`\quad E_{@b} := \{ (s, a)\in S\times \mrm{Alphabet}(J) \mid a = b \T{ で } \tau(s, a) \T{ が定義されている}\}`$
バンドルの全空間 $`E`$ 上では、遷移写像 $`\tau`$ は常に定義されます（未定義部分を削り落としているので）。$`E`$ に制限した $`\tau`$ を同じく $`\tau`$ と書くと、その $`\tau`$ （制限した $`\tau`$）は決定性写像〈全域写像〉です。
$`\quad \tau : E \to B \In \mbf{Set}`$
こうして、オートマトン $`J`$ から作ったバンドル $`\pi: E \to B\In \mbf{Set}`$ を、（オートマトンの）記号バンドル〈symbol bundle〉と呼ぶことにします。ファイバー $`E_{@b}`$ は、点 $`b`$ で意味を持つ記号〈ラベル〉達の集合です。
オートマトンを記号バンドルの形にしておくと、物理（力学）との対応関係〈アナロジー〉が分かりやすくなります。
古典解析力学とオートマトン
物理の古典解析力学とオートマトンとの対応関係〈アナロジー〉は以下の表のようになります。
| 配位空間〈configuration space〉 | 記号バンドルの底空間 |
| 位置〈position〉 | 底空間の点〈要素〉 |
| 配位空間の運動〈motion in configuration space〉 | 底空間の点列 |
| 力〈force〉または運動量〈momentum〉 | 全空間の要素（点と記号のペア） |
| 微分方程式〈differential equation〉 | 遷移写像 |
| 相空間〈phase space〉 | 記号バンドルの全空間 |
| 相空間の運動〈motion in phase space〉 | （全空間内の）軌道 |
物理における配位空間とは、位置の空間です。通常我々が“空間”と呼んでいるものは単一粒子の配位空間です。位置の対応物は、記号バンドルの底空間の点、つまりは状態空間の点〈状態点〉です。
配位空間 $`\longleftrightarrow`$ 状態空間
位置 $`\longleftrightarrow`$ 状態点
時間は離散時間で考えるので、運動はステップ〈step〉に刻まれます。つまり、力学系〈dynamical system〉は番号 0, 1, 2, ... に沿って時間発展〈time evolution〉します。配位空間の運動は、底空間〈状態空間〉の点列 $`s_0, s_1, s_2, \cdots`$ に対応します。
配位空間の運動 $`\longleftrightarrow`$ 状態空間内の点列
運動量（または力）が、全空間の要素（点と記号のペア）に対応することには違和感を感じるかも知れません。運動量は、配位空間の一点 $`p`$ と、その点から出る固定ベクトル（束縛ベクトル）*2 $`v`$ とのペア $`(p, v)`$ です。配位空間の一点 $`p`$ は、状態空間の一点（状態点） $`s`$ に対応します。そして、（違和感があるかも知れませんが）運動量のベクトル $`v`$ が記号（アクションラベル）$`a`$ に対応します。したがって、運動量の固定ベクトル $`(p, v)`$ の対応物は、点（状態点）と記号（アクションラベル）のペア $`(s, a)`$ なのです。
運動量 $`\longleftrightarrow`$ 状態点と記号〈アクションラベル〉のペア
運動量 $`(p, v)`$ が点 $`p`$ を通る運動を駆動するのと同様に、ペア $`(s, a)`$ は、状態点からの状態遷移を駆動します。そう考えれば、運動量のベクトル $`v`$ の対応物が記号（アクションラベル） $`a`$ であることも（多少は）納得いくでしょう。
古典力学では、運動は微分方程式で記述されます。無限小時間における無限小運動が法則になります。オートマトンの場合は離散時間なので無限小時間はなくて、最小時間（1ステップ）があります。1ステップの運動とは、状態遷移のことです。$`(s, a) \mapsto s' = \tau(s, a)`$ が、最小時間（1ステップ）に関する法則です。オートマトンの遷移写像は、古典力学の微分方程式に相当するわけです。どちらも運動の法則を与えます。
微分方程式 $`\longleftrightarrow`$ 遷移写像
古典解析力学における相空間の運動とは、配位空間の点と運動量のペア $`(p, v)`$ の（時間パラメータに沿った）連続した連なりです。オートマトンの場合は、離散時間なので、状態点と記号（アクションラベル）が互い違いに出現する列 $`s_0, a_1, s_1, a_2, s_2, \cdots`$ が、相空間の運動の対応物です。
列 $`s_0, a_1, s_1, a_2, s_2, \cdots`$ は次の条件を満たす必要があります。
- $`s_1 = \tau(s_0, a_1)`$
- $`s_2 = \tau(s_1, a_2)`$
- $`\cdots`$
- $`s_{k + 1} = \tau(s_k, a_{k + 1})`$
このような列が、オートマトンの軌道〈trajectory〉です。軌道の長さは有限でも無限でもかまいません（無限軌道を禁止しません）。
相空間 $`\longleftrightarrow`$ 記号バンドルの全空間
相空間の運動 $`\longleftrightarrow`$ 軌道
オートマトンの軌道達の集合が軌道集合〈trajectory set | set of trajectories〉です。オートマトンの振る舞い〈behavior〉は、軌道集合で記述されるとみなします。むしろ、振る舞いと軌道集合を同一視すると言ったほうがいいでしょう。
ソフトウェアシステムに関して言えば、軌道はシステムの実行の履歴になります。可能な〈起こり得る〉すべての軌道達の集合と、期待される軌道集合〈望ましい軌道集合 | 正しい軌道集合〉を比較することが出来れば、ソフトウェアシステムの正しさを検証できます。正しい軌道集合を記述する方法があれば、それは正確な仕様記述の方法になります。
以上が軌道集合意味論のおおざっぱなアイディアです。
マーク・ウィリアム・ホプキンス
軌道集合意味論は、2005年くらいには考えていたようです。ただし、おぼろげなアイディアだけでよく分かってはいなかったですが。
- while文は難しい：軌道集合意味論？ (2005-07-22)
「軌道」という言葉を使っているのは、物理・力学とのアナロジーを想定しているからです。僕が、物理と計算科学のアナロジーを意識するようになったのはマーク・ウィリアム・ホプキンス〈Mark William Hopkins〉の影響です。
M.W.ホプキンスは、2000年前後には学生・研究者で、インターネット上に刺激的な投稿をしていました。いつからか彼はアカデミアを離れたようで、インターネット上のテキストは削除あるいは散逸し、論文を発表するようなこともなくなったようです。
M.W.ホプキンスは物理にも計算科学にも強く、「場の量子論と形式言語理論」のアナロジーを指摘していました。曰く：
- 状態マシンの遷移関係 $`\longleftrightarrow`$ ハミルトニアン
- 2状態間の遷移パスで生成される言語 $`\longleftrightarrow`$ S行列
- クリーネ・スターの定義 $`\longleftrightarrow`$ ダイソンの公式
よく分からなかった（今でもよく分からない）ですが、興味をひかれました。
以下に列挙する過去記事は、M.W.ホプキンスへの言及がある記事です。
- Mark W. Hopkinsは今どこに？ (2005-06-14)
- 信頼できるリソースとリンクの必要性 (2005-06-14)
- Kleene圏のシンクロニシティ (2005-06-15)
- もうひとつのKleene圏：Wolfram Kahlの総括 (2005-06-16)
- 「物理系実務者のための圏論入門」への補遺＋檜山の戯言 (2007-04-06)
- トレース付き対称モノイド圏とはこんなモノ (2010-10-22)
- 計算モデルに使えそうな2次元の圏：フレーム付き双圏 (2012-05-18)
- ジェイコブ・ルーリー ： 同時代の天才 (2012-05-24)
- 形式言語理論のための代数 (2014-08-13)
- 「M.W.ホプキンスの観察」への気長なアプローチ (2014-08-22)
- いろいろな総和可能性 (2014-09-02)
- 畳み込み半環の前送り準同型 -- パリクの定理に向けて (2014-09-25)
以下の2つの記事も、M.W.ホプキンスの物理-計算科学アナロジーに基づく話です。
- 予定： クリーネスター・圏論・計算の離散力学 (2013-09-23)
- 再考： クリーネスター・圏論・計算の離散力学 (2013-10-08)
2014年以来M.W.ホプキンスへの言及はないのですが、物理-計算科学アナロジーを忘れたわけではありません。オートマトンの力学的解釈も軌道集合意味論も、明らかにM.W.ホプキンスの影響下にあります。
今日はここまで（「今日はここまで」参照）。
