「ホーア論理とホーアオートマトン 8/n ： ローヴェア、ゴグエン、ホーア、メイヤー // 造花は花か？」にて： レッドヘリングを口頭で説明するために、僕はパンダの話をしたり（昔は「パンダ＝レッサーパンダ」だった、とか）するのですが、今回は「花と造花…
「贅沢なタルスキー／グロタンディーク集合論」で言い残した幾つかの論点に対して、この記事でより詳しい説明を与えます。記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcomman…
タルスキー／グロタンディーク集合論〈Tarski-Grothendieck set theory〉は、現在の標準的集合論であるZFC集合論に宇宙公理を加えた体系内で解釈可能な、より使い勝手を良くした集合論です。タルスキー／グロタンディーク集合論は、圏論や依存型理論の基盤と…
今回は、ホーア論理とホーアオートマトンに関するビッグピクチャー（俯瞰的に見た全体像）について語ります。その際、ローヴェア〈Francis William Lawvere〉、ゴグエン〈Joseph Amadee Goguen〉、ホーア〈Charles Antony Richard Hoare〉*1、メイヤー〈Bert…
次のような会話を考えてみます。 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 ライブラリを理解・把握で…
