僕は、ストリング図やペースティング図が好きです。数式（論理式も含む）や自然言語文より、絵図〈picture | diagram | figure | graph〉による表現を好むという意味で絵図主義者です。絵図によって伝えたいことは、なんらかの形式のテキストでも表現できま…

用語・用法図と知識グラフは、以下の過去記事で導入し説明しました。 パンダ用法と用語・用法図 用語・用法図から知識グラフへ 知識グラフ 2： 直感的かつ正確な伝達のために 用語・用法図は、用語の用法（使用法、運用法）を視覚的に説明する道具でした。そ…

圏を一般化した様々な代数系を総称的に呼ぶ名前がなくて困るのですが、この記事ではとりあえず一般化圏としておきます。同様に、グラフを一般化した様々な構造を総称的に一般化グラフと呼ぶことにします。一般化圏と一般化グラフ、それらに関係する概念・用…

コラージュ図式は、通常のペースティング図に“通常とは違う矢印”を混ぜた図式です。以下の過去記事で導入しました。 コラージュ図式： 圏論的判断計算の主要な道具 コラージュ図式でもっともよく使うものは、ファイバー付き圏に関連する図式（「関手のデカル…

Diag構成（「Diag構成： 圏論的構成法の包括的フレームワークとして」、「Diag構成の現状 2025」参照）の主役である図式という概念はかなり複雑です。そればかりではなく、「図式」という用語や関連する用語達が曖昧多義語で、大変ややこしいことになってい…

前回の記事「用語・用法図から知識グラフへ」で、言いたいことはまとめたつもりになったのですが、しばらくすると言い残しに気付いたので続きを書きます。主な話題は、知識グラフに対して、集合論・圏論・依存型理論を用いた形式意味論を構成する話です。完…

用語・用法図は「パンダ用法と用語・用法図」で導入した図／図解法です。この記事で、用語・用法図の辺に付けるラベルを増やすことにより、用語・用法図を知識グラフにまで拡張します。知識グラフはその名の通り、知識の記述や分析に効果的に使用できます。…

依存型理論にストリング図が効果的に使えることが分かりました。このときストリング図の形状である半グラフに、型・名前・番号など様々な属性を考える必要があります。つまり、属性付き半グラフを使うわけです。そこで、属性付きグラフ／属性付き半グラフに…

「パンダ用法と用語・用法図」で導入した用語・用法図は、用語のあいだの相互関係や曖昧多義語の状況を記述するための図です。これはなかなかに有効な分析装置／説明装置で、その応用例は以下の記事にあります。 用語・用法図の応用： 「関係」、「グラフ」 …

Propositions-as-Types は、幾度となく話題にしています。ブログ記事だけでなく、口頭での説明もけっこうな回数おこなっています。これがうまく説明できないのですわ。説明が困難な主たる原因は、用語の対応があまりにもグジャグジャで混乱必至なことです。…

この記事ではラムダ計算におけるアノテーションを取り上げます。「アノテーション」という同じ呼び名ですが、異なる2つのアノテーションがあります。型アノテーションとアノテーション属性です。型アノテーションは、型推論のヒントや可読性向上のために付け…

「パンダ用法と用語・用法図」で用語・用法図を導入しました。用語に関する問題の分析装置／説明装置を手に入れたので、よく見る問題を分析／説明してみましょう。「単項式は多項式か？」が今回取り上げる“よく見る問題”です。$`%\newcommand{\cat}[1]{\math…

「パンダ用法と用語・用法図」で、用語の用法を図解する用語・用法図を導入しました。この記事では、厄介な曖昧多義語である「関係」と「グラフ」の明瞭化〈clarification〉を通じて、用語・用法図の応用事例を紹介します。また、用語・用法図に若干の機能追…

シリーズの第6回で「大枠と方針」とは、だいぶ話が前後してますが、ここであらためて述べておきます。短い記事です。ハブ記事： 宇宙のラムダ計算 宇宙のラムダ計算の大枠と方針に関するキーワード〈重要語句〉は次です。 型付きラムダ計算 依存型理論 集合…

ラムダ抽象や（ラムダ抽象とは限らない）ラムダ式は、環境のなかに置かれます。環境無しに存在できるラムダ式は稀なので、「ラムダ式には環境がある」と思っていいです。ラムダ式の環境は、実は外側にあるラムダ式のスコープのことです。つまり、ラムダ式の…

「パンダ用法： 流転する呼称」において、「パンダ」という言葉の解釈がややこしいことを説明しました。「パンダ」のようにややこしい言葉は他にもあります。過去記事では「非可換環」を挙げました。「大きい集合」や「境界付き多様体」なども同様にややこし…

宇宙のラムダ計算による記述例を幾つか紹介します。宇宙のラムダ計算は、宇宙規模／ラージスケールの計算でも記述できるのがウリですが、日常的な計算でも普通に使えます。なので、前半では、普通の関数や集合を扱います。後半の例は宇宙規模の関数です。こ…

この記事は、「宇宙のラムダ計算」「宇宙のラムダ計算 2： 構文」の続きです。ラムダ抽象の仮引数リストを独立させた、“依存性を持つ（かも知れない）型リスト”について述べます。$`%\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} …

「宇宙のラムダ計算」の続きです。宇宙のラムダ計算にはどんな構文がいいでしょうか？ 構文の決定には、心理的・感情的エルゴノミクスも考慮する必要があります。違和感がないか、気持ちよく書けるか？ といった問題です。可読性とタイピング量の節約も考慮…

グロタンディーク宇宙は、フォン・ノイマン宇宙（ZFC集合論の宇宙）のなかの“ある種の代数系（演算を備えた集合）”だと考えられます。代数系としてのグロタンディーク宇宙での計算には、通常のラムダ計算が使えます。なぜなら、外側のフォン・ノイマン宇宙か…

「根本的誤解： 集合論、圏論、型理論」で「信仰」という言葉を使ったのですが、これはやっぱり語弊があるな、と思いました。宗教的信仰と理性的判断は切り分けられるし、共存も可能です。「信仰」とは別な言葉を整備しましょう。（空集合以外の）アトムを信…

「根本的誤解： 集合論、圏論、型理論」より： 集合論的型理論では、「ほとんど同じだが微妙に違う」がけっこうな頻度で出てきます。同一視可能だが、ほんとに同一視してしまうと辻褄が合わなくなるのです。これは、「奇妙な感じ」や「モヤモヤした気分」に…

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

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

集合圏のなかで、“掛け算の結合法則”や“累乗の指数法則”の公式が成立します。$`\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集合論に宇宙公理を加えた体系内で解釈可能な、より使い勝手を良くした集合論です。タルスキー／グロタンディーク集合論は、圏論や依存型理論の基盤と…