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

AIコーディングエージェントの登場により、“狭い意味でのコーディング”はAIに任せられるようになりました。しかし、次の作業はまだ人間がやったほうがよさそうです。

1. プログラムの仕様の記述
2. テストの設計・計画

人間が、プログラムの仕様を記述して、テストの設計・計画も準備すれば、あとはAIコーディングエージェントがやってくれるでしょう、たぶん、だいたいは。

プログラムの仕様／テストの背景となる理論で定番中の定番といえば、ホーア論理です。よく知られたホーア論理を、現実のプログラミング／ソフトウェアプロジェクトに適用するための手法・定式化とはどんなものでしょうか？ このテの話は、四半世紀以上ずっと考え込んでいたネタです。が、2026年、またあらためて考えてみようか、と。

タイトルに 1/n と付けたのは、続きものにするつもりだからです。何回になるかはわかりません。記事の切れ目はあまり気にしないで、日記風に書きます。つまり、中途半端なところでも「今日はここまで」と終わりにするかも知れません。$`\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\HoareAutom}{\mathbf{HoareAutom}}
`$

内容：

• 文字の色の約束
• 概要と予告
• プログラムの正しさを信じられる、とは？
• 今日はここまで

シリーズ内の記事：

1. ホーア論理とホーアオートマトン 1/n （この記事）
2. ホーア論理とホーアオートマトン 2/n
3. ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語
4. ホーア論理とホーアオートマトン 4/n ： 隠蔽
5. ホーア論理とホーアオートマトン 5/n ： 整理と注意
6. ホーア論理とホーアオートマトン 6/n ： 記号バンドルの力学
7. ホーア論理とホーアオートマトン 7/n ： 自由記号列の力学
8. ホーア論理とホーアオートマトン 8/n ： ローヴェア、ゴグエン、ホーア、メイヤー

文字の色の約束

テクニカルタームの初出または定義のとき、色を付けたテキストで書きます。よく知られた用語は青い文字です。この記事内では定義・説明しない場合もあります（調べれば分かるので）。多くの場合、このブログの検索ボックスで青い文字を検索すると関連記事が出てきます。必要なら、既存の用語（青い文字）の定義を記事内で繰り返し書くこともあります。

この記事で導入・定義する用語は赤い文字です。赤い文字が新規の用語、あるいは既存の用語でも意味を少し変えて使用する場合があります。赤い文字がよく知られた既存の用語のこともあります。特に話題にしたい用語が赤い文字、ということです。

マゼンタの文字は、この記事の後方または引き続く記事内で定義・説明される概念・用語です。

概要と予告

ラベル付き遷移系〈labeled transition system | LTS〉やオートマトン〈automaton〉を若干一般化した概念としてホーアオートマトン〈Hoare automaton〉を定義します。

ホーアオートマトン達は、圏 $`\HoareAutom`$ を形成します*1。ホーアオートマトンが対象なのではなくて、射になります。圏 $`\HoareAutom`$ の対象はホーア指標〈Hoare signature〉です。つまり、圏 $`\HoareAutom`$ は、ホーア指標を対象として、ホーアオートマトンを射とする圏です。圏 $`\HoareAutom`$ を定義することがとりあえずの目標になります。

圏 $`\HoareAutom`$ は局所小圏〈locally small category〉ではありません。$`\Sigma, \Gamma`$ をホーア指標（圏の対象）として、ホムセット $`\HoareAutom(\Sigma, \Gamma)`$ は小さい集合〈small set〉になるとは限りません。ホムセット $`\HoareAutom(\Sigma, \Gamma)`$ は、ホーアオートマトンのあいだの準同型射〈homomorphism〉や双模倣〈bisimulation〉により（必ずしも小さくない）圏になります。その意味で、$`\HoareAutom`$ は単なる圏ではなくて2-圏です。が、当面は2-圏の構造は無視して単なる圏として扱うでしょう。

圏 $`\HoareAutom`$ に定義を追加してリッチな構造を持たせることが出来ます。2つのモノイド積〈monoidal product〉 $`\boxtimes, \boxplus`$ を導入できます。これらのモノイド積は、集合圏の直積と直和、あるいは論理のANDとORに似たものです。また、圏 $`\HoareAutom`$ を拡張変形して複圏〈multicategory | operad〉や多圏〈polycategory〉にすることもできます。複圏化した $`\mbf{MultiHoareAutom}`$ は実用上便利なものです。

ホーア論理〈Hoare logic〉は、論理とプログラムを一緒に扱える形式体系〈formal system〉です。論理パートもプログラムパートもある種の代数構造を定義します。最初の段階では、論理代数〈logic algebra〉として、古典論理〈classical logic〉にボトム（$`\bot`$）を追加したボトム付き古典論理〈bottomed classical logic〉を採用します。プログラム代数〈program algebra〉としては単なるモノイドを扱います。つまり、プログラムの順次実行だけをモデル化します。後々、もう少し複雑な論理代数／プログラム代数を扱うかも知れません。例えば、テスト付きクリーネ代数〈Kleene algebra with test | KAT〉とか。

プログラムの仕様記述にホーアトリプル〈Hoare triple〉を使うつもりですが、ホーアトリプルの解釈としては軌道集合意味論〈trajectory-set semantics〉を使うつもりです。軌道集合意味論は、2005年（20年以上前）の記事で名前を出した（しかも「よくわからんなー」という文脈で）だけで放置していたものです。

• while文は難しい：軌道集合意味論？ (2005-07-22)

ホーア論理とホーアオートマトンの文脈で、適切な意味論は何だろう？ と考えてみると「やっぱりコレだろ」という感じがするので、軌道集合意味論を、記憶の瓦礫の中から掘り起こすことにします。

プログラムの正しさを信じられる、とは？

「このプログラムはバグがない」とか「この関数はちゃんと動く」とか言うのは簡単です。言うだけなら誰でもいつでも言えます。しかし、そのような発言が信じられるかというと、何らかの証拠・保証がないと信じられませんよね。

発言（主張、命題）が妥当であると論理的に認められる方法は二種類あります。

• モデル論的妥当性〈model-theoretic validity〉： 命題が、特定のモデルにおいて、あるいはすべてのモデルにおいて真になること。$`P`$ を命題、$`M`$ をモデルとして、$`M \models P`$ （特定のモデルにおいて真）、$`\models P`$ （すべてのモデルにおいて真）と書かれる。
• 証明論的妥当性〈proof-theoretic validity〉： なんらかの演繹システム〈{deduction | deductive} system〉において命題が証明されること。$`P, Q_1, \cdots , Q_n`$ を命題、$`S`$ を演繹システムとして、$`Q_1, \cdots Q_n \vdash_S P`$ は「演繹システム $`S`$ において、$`Q_1, \cdots Q_n`$ を仮定して、$`P`$ を証明できることを表す。

モデル論的妥当性を単に妥当性〈validity〉、証明論的妥当性を証明可能性〈provability〉と呼ぶこともあります。

論理では認められないが、現実生活では使っている妥当性 -- 非論理的妥当性*2には次のようなものがあります。

• 信念妥当性〈validity by belief〉： 自分が“そう思っている”ことを根拠とした妥当性。
• 伝聞妥当性〈validity by hearsay〉： 誰かが“そう言った”ことを根拠とした妥当性。
• 経験的妥当性〈empirical validity〉： 過去の（有限個の）実例で正しかったことを根拠とした妥当性。

例えば、「ボクがすごく注意深く頑張って作ったんだから、このプログラムはバグはない」という発言は信念妥当性に基づき主張しています。「先輩が、この関数はちゃんと動くと言っていたから大丈夫」は、伝聞妥当性に基づく主張です。「このライブラリは評判がいいから大丈夫」も伝聞妥当性の主張と言えるでしょう。「この関数はたくさんテストをしたから大丈夫」は典型的な経験的妥当性の主張です。「このライブラリは評判がいいから大丈夫」も、「多くの人が使っていて目立った瑕疵がない」ということであれば経験的妥当性が含まれるでしょう。

論理的妥当性であるモデル論的妥当性も証明論的妥当性も、現実に確認するのは困難または不可能です。なので、現実世界では非論理的妥当性、特に経験的妥当性で“ヨシとしている”ことが多いですね。これは致し方ないです。しかし、できるだけ論理的妥当性に近付けようと頑張ることに意義はあります。

ホーア論理＋ホーアオートマトン＋軌道集合意味論の枠組みは、経験的妥当性（テストによる妥当性）も論理的妥当性と一緒に扱えるので、かなり忠実な現実世界のモデル化として使えると思います。

今日はここまで

冒頭に書いたように、このシリーズ（予定）は日記風に書くつもりなので、「今日はここまで」で終わりにします。全然まとまりがついてないけど。

最近ブログ記事を書いてないけど、これには理由があります。僕が一日にキーボードを叩く量はだいたい決まっているようです。ブログ記事以外でタイピング量を消費してしまうと、ブログ記事は書かないことになります。最近、AIチャットボットやAIエージェントとの対話で一日のタイピングが尽きてしまうのです。

ブログ記事を投稿するには、長さやまとまりを気にしないで、その日のタイピング量で賄える長さで切ってしまうのがいいかも、と考えた次第です。