圏の次元調整〈dimension adjustment〉という概念を出したのは次の記事でした。 圏の離散化、切り捨て、次元調整（MathJax数式がうまくレンダリングされないときは、ページリロードで表示されると思います。） まず前提として、すべての圏は無限次元圏だと考…

項・式など（と呼ばれる記号的存在物）の生成や操作に関連してモナドが現れることがあります。この種のモナドについて述べておきます。「構文論 vs. 意味論」という文脈で、構文機構の扱いやすい定式化が必要になりますからね。$`\newcommand{\cat}[1]{\math…

モナドに関して： モナドの単位自然変換は、成分ごとにモノ射だろう。 とか予想しがちですが、これは違います。よく見かけるモノドの単位がモノ射成分なだけです。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\id}{\mathrm{id} } \newcommand{\In}{\te…

一連のシリーズ記事（最初の記事は「最近の型理論： 宇宙と世界、そして銀河」）を始めた目的は、最近のプログラミング言語・証明支援系 Lean、Agda、Coq などが備えている型システムの背景となっている「階層化された宇宙達を備えた型理論」を調べて紹介す…

ひと月以上前（4月6日）「自然言語混じり形式証明の意味論」という記事を書きました。そこに、5つの過去記事へのリンクがあります。それら一群の記事で、「自然言語文がコメントや補足説明ではなくて、形式証明の正式な一部となるような証明記述言語が使える…

前回の記事「最近の型理論： 外部化手法のもとでのパイ型と指数型」で、次のようなことを書きました。 対象を圏の外部に取り出す方法を外部化手法〈externalization〉と呼ぶとして、...[snip]... 「集合圏と似てないデカルト閉圏に対しては、外部化手法は有…

一連のシリーズ記事として、「階層化された宇宙達を備えた型理論」について述べてきました。最初の記事がハブ記事（他の記事へのリンク集）にもなっています。 最近の型理論： 宇宙と世界、そして銀河 「階層化された宇宙達を備えた型理論」は依存型理論でも…

「依存型理論で述語論理が出来てしまう理由」において、2つの圏をもとにしてハイパードクトリンを構成する方法の概略を示しました。このハイパードクトリンは、依存型理論と述語論理のどちらも記述できる汎用的な機構になっています。銀河（型をホストする圏…

タイトルの件に関して、とりあえず概要だけ述べます。おおよそのストーリーを語るので、細部の抜けやギャップはあります。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\J}{\mathrm{J}} \newcommand{\In}{\text{ in…

記事タイトルの「最近の」は、「理論的には古くから知られていても、実用的利用は最近になって出てきた」といった意味です。さらに具体的な特徴として、「階層化された宇宙達を備えた型理論」のことです。そのような型理論は、Lean, Agda, Coq などの型シス…

インデックス付けられた集合の族〈indexed family of sets〉を単にファミリーと呼びます。ファミリーにはたくさんの同義語があります； コンテナ、多項式、（集合論的な）バンドル、ファイバー付き集合、アリーナ、メニューなど。同義語がたくさんあるのは、…

先週の記事「最近の型理論： 宇宙・世界・銀河 もう少し」では、型理論をホストする圏について考えてみました。ある程度の極限・余極限を持つデカルト閉圏があれば、そこで型理論を展開できそうです。が、対象のあいだの包含関係が欲しくなることがあります…

前回（昨日）の記事「最近の型理論： 宇宙と世界、そして銀河」で説明した世界構造に関して、少し補足します。$`\newcommand{\Imp}{\Rightarrow} \newcommand{\Iff}{\Leftrightarrow} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}}…

Lean（最新版はLean 4）は強力な型システムを備えた汎用プログラミング言語です。そればかりではなくて、証明支援系としての機能も同一の型システムをベースにして実現しています。AgdaやCoqもまた、型システムに基づく証明支援系／プログラミング言語です。…

必ずしも関手や自然変換にならないような写像や部分写像も積極的に使うべきだ、ということは何度か言っています。そのことに関するブログ内検索は： 「非自然」を検索 「圏論的コンストラクタ」を検索 ひとつだけ記事を挙げるなら： 圏論的コンストラクタと…

スピヴァック〈David I. Spivak〉が、集合圏上の多項式関手に関して使用している $`y^A`$ のような記法を「米田テンソル計算 3： 米田の「よ」、米田の星、ディラックのブラケット 再論 // スピヴァックの指数記法」で紹介しました。指数記法はとても具合が…

昨日の記事「述語論理： 二重圏的ハイパードクトリン」で、二重圏的ハイパードクトリンという概念を出しました。二重圏的ハイパードクトリンを定義するために、シード付き二重圏を定義したのですが、どうも安直過ぎました。シード付き二重圏を再定義します。…

ハイパードクトリンのベース圏はデカルト圏を仮定するのが普通です。が、デカルト圏の代わりに二重圏をベース圏として採用してみると、これはこれで使いやすい気がします。述語論理系やベック／シュバレー条件が比較的素直に定義できます。[追記]シード付き…

圏論の基本事項解説、割と久しぶり。ファイバー積はオーバー圏の直積であり、余ファイバー和〈融合和〉はアンダー圏の直和です。$`\newcommand{\cat}[1]{\mathcal{C} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } \newcommand{\fpr…

型理論、ラムダ計算、論理、形式証明などの話をするときは、表題にあるような基本概念を使いたいのですが、基本概念を説明するほうも／されるほうも消耗しがち、色々と障害があるので。この記事で、なるべく苦労なく手っ取り早く基本概念に馴染めるような説…

一連の話の“流れ”（以下の記事群参照）として、自然言語混じり形式証明の意味論に少し触れておきます。昨日の記事への追記・補足の位置付けです。 チャットAIで形式証明も自然言語混じりで書ける（はず） 自然言語証明から形式証明を抽出できる（はず） 証明…

「証明支援系がダメだった理由と、AIでブーストする理由 // 人間可読証明」において次のように書きました。 人類がテキスト言語から絵図言語に乗り換えられないのは、文字・活字・組版文化の歴史的惰性だと思いますが、このような歴史的惰性を変化させるのは…

考える圏は小さい圏にします。小さい圏とは、集合圏 $`{\bf Set}`$ の内部圏〈圏対象〉です。こう仮定したからと言って、サイズの問題を完全に無視してるわけでもありません。集合圏のベースになるグロタンディーク宇宙を一レベル上げれば、大きい圏も扱えま…

Coq、Agda、Idris、Lean などの証明支援系は、型付きラムダ計算と帰納的構成計算に基いています。ベースに強力な型システムを持ったプログラミング言語があり、型システムの型チェッカーを利用して証明チェックも行います。証明記述と証明チェックは、ラムダ…

「チャットAIで形式証明も自然言語混じりで書ける（はず）」と「自然言語証明から形式証明を抽出できる（はず）」で述べたように、自然言語を使って形式証明が書けるようになるだろうと予測（むしろ期待）してます。しかし、自然言語であろうが形式言語であ…

コンテナ＝1-コンテナ という概念の次元を1つ上げて2-コンテナを定義します。取り急ぎ。$`\newcommand{\s}[1]{\mathrm{s}{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\In}{\text{ in }} \newcommand{\hyp}{…

記号の乱用〈記法の{乱用 | 濫用} | abuse of notation〉は、ものごとを分かりにくくして誤解と混乱のもとになります。しかし、非常に広く使われていて、使わないで済ますことが困難です。人間にとってだけではなく、プログラミング言語や証明支援系などのソ…

不満があっても、「言ってもどうせ何も変わりはしない」という諦めがあればあえて不満を口に出すことはないでしょう。願望があっても、「どうせ叶わぬ夢だし、言ったところで虚しくなるだけ」と断念しているなら語ることはないでしょう。僕は今から不満と願…

「チャットAIで形式証明も自然言語混じりで書ける（はず）」と「自然言語証明から形式証明を抽出できる（はず）」において、形式証明と自然言語証明はかなりの程度相互翻訳可能になるはず、という予測（というか期待・願い）を述べたのですが、自然言語ヒン…

「チャットAIで形式証明も自然言語混じりで書ける（はず）」において、形式証明のなかに自然言語によるヒント／キューが書けたら証明記述作業が格段に楽になる、と書きました。この方法を少し推し進めれば、書籍や論文の自然言語証明から形式証明を生成でき…