「マイヤースのシステム理論への違和感と代替案」で述べたIOCシステム〈入力・出力・制御付きシステム〉と、制御インターフェイスへのラッパーについて、具体的な定義を提示します。背景となる圏は集合圏としますが、デカルト圏や対称モノイド圏への拡張は難…

思いつきのメモ。7月22日の記事「状態遷移系達の二重圏の直接的定義」において、マイヤース〈David Jaz Myers〉の圏論的システム理論〈categorical systems theory〉を紹介しました。7月22日記事において、「違和感／ズレ」という言葉を何度も使っています。…

状態遷移系に関する補足小ネタ その1：「状態遷移系達の二重圏の直接的定義」において、状態遷移系をバンドルのあいだのレンズ射として定式化しました。状態遷移系（＝レンズ射）を図式に描くとき、野球のホームベース形に描くと具合がいいです。$`%\newcomm…

ジャズ・マイヤース〈David Jaz Myers〉が、Categorical Systems Theory のなかで、「アリーナの二重圏」という概念を定義しているのですが、なんだかピンとこない。実例を考えてみました。具体的な状態遷移系をタイト射とする二重圏です。この具体的な状態…

簡単な呼び名・言い回しで実は複雑な内容を語っていることがあります。簡単な呼び名・言い回しを、ドリルダウン（だんだん詳細化する）方式で分析してみましょう。例えば「小さな圏の圏の2-圏」は、けっこう複雑な内容を表しています。$`\newcommand{\cat}[1…

「判断的セオリーと判断計算」で紹介したコラリア／ディ-リベールティの論文 "Context, Judgement, Deduction" は、「演繹〈deduction〉とは何なのか？」をテーマにしています。「メリス／ジルバーガーの圏論的判断計算」で紹介したメリス／ジルバーガーの論…

「属性付き2-グラフのスノーグローブ現象」に書いたように、属性付き2-グラフではメタ巡回〈循環〉的状況が生じます。しかし、これは困ったことではなくて、むしろ望ましいことである気がします。「属性付き2-グラフのスノーグローブ現象 // おわりに」より…

「属性付き2次元グラフ： 図式言語の基本」において、図式、形状、テンプレートについて説明しました。次のように述べました。 形状と図式は違う概念である。 テンプレートは、特別な場合として形状も図式も含む一般的概念である。 ところが次も言えます。 …

「コラージュ図式： 圏論的判断計算の主要な道具 // コラージュ図式」より： コラージュ図式〈collage diagram〉は、ここでの判断計算の主役です。通常の図式と同様に、形状〈shape〉である図形の各セルにターゲット・ドクトリン内のモノを割り当てます。た…

「判断的セオリーと判断計算」においてコラリア／ディ-リベールティの判断計算を、「メリス／ジルバーガーの圏論的判断計算」においてメリス／ジルバーガーの判断計算を紹介しました。コラリア／ディ-リベールティはちょっと複雑過ぎる印象で、メリス／ジル…

メリス／ジルバーガーの次の論文をチラ見・拾い読みしました。 [MZ13-][MZ15] Title: Functors are Type Refinement Systems Authors: Paul-André Melliès, Noam Zeilberger Year: 2015 Pages: 14p URL: https://www.irif.fr/~mellies/papers/functors-are-t…

「判断形式を普通に書く」より： 型理論の判断形式を使うと、非常に簡潔に書けます。しかし、簡潔さの代償として、多くの情報を暗黙化します。コラリア／ディ-リベールティも簡潔な記述を目指しているので、えげつない「記号の乱用、短縮記法、完全な省略」…

前回の記事「判断形式を普通に書く」で、コラリア／ディ-リベールティの次の論文を参照しました。 [CL21-24] Title: Context, Judgement, Deduction Authors: Greta Coraglia, Ivan Di Liberti Submitted: 17 Nov 2021 (v1), 1 Nov 2024 (v3) Pages: 61p URL…

型理論の人々は「判断形式で書かないと死んでしまう」のでしょうか？ そして、判断形式にターンスタイル（'$`\vdash`$'）とコロン（'$`:`$'）以外使ったら死んでしまう」のでしょうか？ターンスタイルとコロンへの執着は、もはや「好みの問題」の域を超えて…

圏論的概念は、可換図式やペースティング図を使って定義や記述がされます。テキスト構文で書けないわけではないですが、矢鱈に煩雑になります。現実的には、図式なしではやっていけません。この記事では、図式による定義を、明確かつ簡潔に書くためのフォー…

ヒルベルトのイプシロン記号は、集合からその要素を気まぐれに（まったく予測できないスタイルで）取り出す操作です。ヒルベルトのイプシロン記号が便利な場面や必須な場面があります。しかし、ヒルベルトのイプシロン記号に空集合を渡したときの挙動がよく…

形式化された議論であれ非形式的〈インフォーマル〉な議論であれ、命題と規則を区別する必要はあります。「型理論と論理： 非形式シーケント記法 // 規則は命題ではないのだが」において、規則は命題ではないと言ったのですが、混同されるのはそれなりの理由…

あー、そういうことかぁ！僕は、用語の語源にあまりこだわらないので、「包括圏」の語源は知らなかったし、調べることもしませんでした。「なんでか知らんけど、『包括圏』って呼ぶのね」で済ませていました。語源や逸話を知らないと概念を理解できないわけ…

「型理論周辺、何で混乱するのか？」において： 型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです 地雷原になってしまう大きな理由に、ターンスタイル記号 '$`\vdash`$'、二重矢印 '$`\R…

どこに引っ越すのか？ それは“コンテキスタッドの世界”への引っ越しです。コンテキスタッドが型理論／論理／インスティチューション理論に対して、統合的・整合的な枠組みを与えるだろう、と思っています。それは、最近の記事達の内容や動機になっています。…

型理論周辺の用語・記法・説明が混乱誘発的〈confusing〉で、それは僕の長年の悩みの種です。型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです*1。最近、包括コンテキスタッド（「型理論…

包括圏とコンテキスタッドの組み合わせは、型理論やインスティチューション理論に向いているようです（「型理論とコンテキスタッド： コンテキストフル射」参照）。この記事では、包括コンテキスタッド（包括圏とコンテキスタッドの組み合わせ）を定義し利用…

集合 $`X`$ 上の方程式が与えられたとき、その解集合（空集合でも $`X`$ 全体でも、なんであれ）は一意に決まると我々は信じています。しかし、トポスのなかで方程式を考えると、解集合（に相当する解対象）は一意に決まることは保証されません。これって、…

圏の恒等射だけで部分圏ができます。が、この部分圏はファイブレーションクラスにはなりません。包含的圏（「色々な包含的圏」参照）の包含射達は部分圏を形成しますが、これもファイブレーションクラスにはなりません。圏のファイブレーションクラスの定義…

「名前の解釈： 正確なコミュニケーションのために」、「名前の解釈 その2」の続きです。$`\newcommand{\In}{\text{ in }} \newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] } \newcommand{\hyp}{ \text{－} } \newcommand{\mbf}[1]{ \mathbf{#1}…

「名前の解釈： 正確なコミュニケーションのために」の続きです。$`\newcommand{\In}{\text{ in }} \newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] } \newcommand{\hyp}{ \text{－} } \newcommand{\mbf}[1]{ \mathbf{#1} } \newcommand{\mrm}[1…

名前の解釈をちゃんとしよう -- と、口頭では何百回も言った気がするのですが、ちゃんと書いたことはなかったので、この記事にまとめておきます。名前を正確に解釈せずにボヤッとした印象で済ませてしまう癖を矯正するのは難しいですね。それが、何百回も言…

カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッド（「コンテキスタッド、包括圏、ハイパードクトリン」参照）は、型理論と思いのほか相性がいいようです。ちょっと驚いています。型理論的概念である包括圏を、テレスコープ構成によ…

「色々な包含的圏」において、包含的圏の変種を6種類定義しました。圏の対象達全体の集合に載る大域的な構造と、各対象ごとに構成できる局所的な構造の2つの観点から分類しています。この記事では、包含的圏（の変種）の事例であり、同時に誤解しやすい点に…

包含的圏〈inclusive category〉の定義は人により色々です。型理論やインスティチューション理論に使うことを目的にして、包含的圏に関して整理しておきます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]…