集合論、圏論、型理論において、基本的なところで根本的誤解をしているのではないかと思える事態にたまに遭遇します。僕の個人的な経験・観察なので、そのような誤解が多いのかどうか、正確にはわかりません。が、少数でも事例はあるので、注意喚起しておく…

圏論（高次圏論含む）において出現する概念や状況を正確に記述するのは容易ではありません。ネーミングルールを工夫することによって、多少なりとも記述の正確性や情報量を増やすことを考えてみます。ここでの“工夫”とは、集合、圏、関数、関手などの名前に…

集合圏のなかで、“掛け算の結合法則”や“累乗の指数法則”の公式が成立します。$`\quad (X\times Y) \times Z \cong X\times (Y \times Z)`$ $`\quad Z^{X\times Y} \cong (Z^Y)^X`$ 集合圏のなかの集合の計算は、集合論的単純型理論における型の計算と同じこ…

「型理論のジャングルに踏み込むための心構えと装備 1/2」において、次の基本概念を説明しました。 単純型 単純型のインスタンス 依存性を持つ型 シグマ型形成子 シグマ型 シグマ型の標準射影 依存性を持つ型のインスタンス パイ型形成子 パイ型 これらの集…

依存型理論に関する記事を書き始めたのですが、「うーむ、こりゃダメだ」と。型理論の用語法が混乱していて、警告や注意事項を適宜挿入するレベルでは対応できないな、と思いました。型理論を語る言葉・言い回し・記法は、極めて曖昧です。その曖昧さを解決…

「ホーア論理とホーアオートマトン 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…

「ソフトウェア・システムの正しさをテストと証明で示したい」という願望が、一連の記事の動機です。この願望は、ソフトウェアを作る人は誰でも持っている願望でしょう。しかし、徳目主義・根性主義で「やるべきだ、頑張ろう」と言ってみても埒が明きません…

ホーアオートマトンは、“状態ソートを含む指標のモデル”となるものです。今言った「状態ソートを含む指標のモデル」は、ホーアオートマトンの手短〈てみじか〉な説明になっています。が、これだけでは通じないでしょう。通じないだけならいいのですが、言葉…