今回は、ホーア論理とホーアオートマトンに関するビッグピクチャー（俯瞰的に見た全体像）について語ります。その際、ローヴェア〈Francis William Lawvere〉、ゴグエン〈Joseph Amadee Goguen〉、ホーア〈Charles Antony Richard Hoare〉、メイヤー〈Bertra…
次のような会話を考えてみます。 Aさん「‥‥て何のことだろう？」 Bさん「ちょっと待って、Chat GPT に聞いてみる。」 Bさん「Chat GPT によると ～～ だってさ。」 この質疑応答では、Bさんはいなくてもいいでしょう。 Aさん「‥‥て何のことだろう？ Chat GPT…
前回、古典解析力学とオートマトン理論のアナロジーを話題にしました。軌道集合意味論は、このアナロジーに依拠しています。が、力学系とオートマトンでは、だいぶ違った側面もあります。今回は、物理起源の力学系と、プログラムの意味論としてのオートマト…
このシリーズでやりたいことは、ホーア論理（ホーアトリプルに基づく論理）によりソフトウェアシステムの振る舞いを記述・制約することです。実際に動くソフトウェアシステムは、ホーアオートマトンによりモデル化します。ホーア論理の（あるいはホーアトリ…
過去4回の記事を読み直してみると、ここいらで整理しておいたほうがいいことや、注意事項などがあることに気付きました。今回はそれらについて書きます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\mrm}[1]{\mat…
「ソフトウェア・システムの正しさをテストと証明で示したい」という願望が、一連の記事の動機です。この願望は、ソフトウェアを作る人は誰でも持っている願望でしょう。しかし、徳目主義・根性主義で「やるべきだ、頑張ろう」と言ってみても埒が明きません…
ホーアオートマトンは、“状態ソートを含む指標のモデル”となるものです。今言った「状態ソートを含む指標のモデル」は、ホーアオートマトンの手短〈てみじか〉な説明になっています。が、これだけでは通じないでしょう。通じないだけならいいのですが、言葉…
「ホーア論理とホーアオートマトン 1/n」の続きです。文字の色の約束は前回と同じです。「ホーア論理とホーアオートマトン 1/n // 文字の色の約束」を確認してください。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcomman…
AIコーディングエージェントの登場により、“狭い意味でのコーディング”はAIに任せられるようになりました。しかし、次の作業はまだ人間がやったほうがよさそうです。 プログラムの仕様の記述 テストの設計・計画 人間が、プログラムの仕様を記述して、テスト…
最近の証明支援系／プログラミング言語では、通常の型システムの上位に宇宙システム（ソートシステムともいう）を備えたものがあります。2023年の記事「最近の型理論： 宇宙と世界、そして銀河」の冒頭を引用すると： Lean（最新版はLean 4）は強力な型シス…
古典論理では、命題「Pでない ならば Qでない」の対偶である「Q ならば P」は、もとの命題と同値であり意味は変わらないとされます。しかし、対偶命題がもとの命題と同値なことは日常直感と合わない、とも言われます。そのとき出される実例のひとつに「言わ…
Lean のコード生成に関しては、GitHub Copilot の補完AIやエージェントはほとんど役に立ちません（むしろ、邪魔しやがる）。コーディングAIの利用は現実的でないので諦めました。とはいえ、Lean の複雑な言語仕様や巨大な Mathlib ライブラリを理解・把握で…
2025年内にもう一本ブログ記事を（間に合った）。「生成AIとしゃべる」のは、何かを生成させたいからしゃべるわけです。チャットボットなら会話の応答文を生成させたいし、画像生成AIなら画像を生成させたい、と。目的のモノ、意図したモノを生成させるには…
「AI支援形式証明への道 報告-3 圏論のプラグイン化」への補足記事です。AIに Lean 4 のコードを生成してもらう作業は、通常のプログラミング言語（Python、TypeScript、C++ など）のコード生成とはだいぶ様子が違います。通常のプログラムコード生成に有用…
「AI支援形式証明への道」を書いた頃（2025年11月末）から、AIチャットボットに手伝ってもらって、Lean 4 により定義や定理を記述することを試しています。今のAIは高性能で速いですが、それを使っている僕が低性能で遅いので、全体の進捗は「遅々としている…
