…前に「型理論／論理／インスティチューション理論の引っ越し準備」という記事を書きました。その冒頭に曰く： どこに引っ越すのか？ それは“コンテキスタッドの世界”への引っ越しです。 引っ越し先である“コンテキスタッドの世界”について、十分に調査したわけではないです。もう少し調べてみよう、とふと思い立ちました。1回の記事で書き切れるかどうかわからないので、*/n という番号を付けます。今回はその1回目でさえなくて 0 回、つまり前置きの回です。雑多なことを散文的に書きます。記事内で…

…は論理／依存型理論／インスティチューション理論などに登場します。従来のイントラ形状射／インター形状射を各種コンマ射に変えた事例は今後出てくるでしょう。付録：リンク集この記事内に出現した過去記事へのリンクを、古い順にリストします。 最近の型理論： デカルト閉圏の外部化・内部化とスノーグローブ現象 // メタ巡回性と外部化・内部化 依存アクテゴリーに向けて // スノーグローブ現象／マイクロコスモ原理 変換手意味論とブラケット記法 // 「空間」という言葉 曖昧性を減らす： Di…

…指標の具体例： ν-インスティチューションのために 「指標」という語を含むすべての過去記事は： 指標 の検索結果: 半群の指標は、例えば次のように書けます。$`\T{signature Semigroup}\: \{\\ \quad \T{sort } U\\ \quad \T{operation } m : U\times U \to U\\ \quad \T{equation } \mrm{assoc} :: (m\times \id_U);m = \alpha_{U,U…

…理論のコンテキスト、インスティチューション理論の指標の類似物です。類似物というより、コンテキスト／指標の別表現と言ったほうがいいかも知れません。ところで、束縛子 $`\tau`$ の直後の束縛変数リストは、型リストに出現する名前〈ラベル〉と同じで冗長です。次の書き方を許すとします。$`\mrm{UnitalSemigrp} := \tau(*).\{\\ \quad A:|\mbf{Semigrp}|\\ \quad C: \PR{\mrm{HasUniqueUnit}(A)…

…論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです 型理論に関する誤解について書くと長くなってしまうので、「型理論のジャングルに踏み込むための心構えと装備 1/2 // 型理論は集合論ではない」でも触れた話題をまた取り上げます。集合 $`A`$ の要素 $`a\in A`$ を取ったとき、$`a\in X`$ となる集合 $`X`$ は $`A`$ 以外にもいくらでもあります。一方で、型理論のインスタンスは一意的な型を持っ…

…蔽の教義 ゴグエンのインスティチューションの教義 ホーアのオートマトンの教義 メイヤーの良い指標の教義 これらの教義をうまいことブレンドすることによって、ソフトウェアシステムの意味論を構成します。この記事では、まだ厳密には定義してない用語を遠慮なく使っているので、そこは気にしないでアウトラインを掴む目的で読み進めることをおすすめします。記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{…

…指標の具体例： ν-インスティチューションのために 「指標」という語を含むすべての過去記事は： 指標 の検索結果: 「ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語 // オブジェクト指向風の指標」において、「オブジェクト指向風の指標」という言葉を使いました。この記事では、オブジェクト指向風の指標が何であるかを正確に記述することにします。半決定性写像達の圏 $`\mbf{SDet}`$（「ホーア論理とホーアオートマトン 2/n // 決定性、非決定性、半決定…

…l theory〉、インスティチューション理論〈institution theory〉、形式セオリーの理論〈theory of formal theories〉などでは普通に使われていますが、人により若干定義が違います。ソート〈型＠お馴染み〉宣言とオペレーション〈関数・メソッド＠お馴染み〉宣言の部分（法則は入れない）を指標と呼ぶ人がいます。稀に、ソート宣言も外してオペレーション宣言の部分だけを指標と呼ぶ人もいます。僕は、ソート宣言・オペレーション宣言・法則をすべて入れたものを…

…指標の具体例： ν-インスティチューションのために 単純ホーアオートマトンの指標は：$`\T{signature }\mrm{SimpleHoareAutom}\: \{\\ \quad \T{sort } S \In \mbf{Set}\\ \quad \T{sort } A \In \mbf{Set}\\ \quad \T{operation }\tau : S\times A \to S \In \mbf{Set}\\ \quad \T{sort } P \In \mb…

…す。「型理論／論理／インスティチューション理論の引っ越し準備 // 依存ペア」「型理論とコンテキスタッド： コンテキストフル射 // 依存ペアと作用演算」に書いたように、依存ペアの書き方はイッパイありますが、ここでは $`(k \mid \sigma)`$ を使います。$`k\in |\mbf{ss}|`$ で $`\sigma\in G_k`$ です。$`\int G`$ の射は、3つ組 $`\A{\tau, \sigma, \varphi}`$ で書くことにします。ここで…

「型理論／論理／インスティチューション理論の引っ越し準備」の続きです。タイトルが長いので少し短くしました。「型理論など」は「型理論／論理／インスティチューション理論」のことです。包括圏の変種（ある種の双対）や包括圏に対する付加的構造について述べて、インスタンス概念を表すハープーン射にも触れます。最後に、包括圏の使い方を示します。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \new…

…hism〉と呼ぶ。 インスティチューション理論では、$`\cat{C}`$ の反対圏 $`\cat{S} := \cat{C}^\op`$ が出てくる。 $`\cat{S}`$ の対象を指標〈signature〉、射を指標射〈signature morphism〉と呼ぶ。 型理論とインスティチューション理論では、興味の中心や手法は違いますが、扱っているモノ自体は同じです。以下、インスティチューション理論の指標達の圏 $`\cat{S}`$ について述べます。 圏 $`\cat…

…igma)`$ は、インスティチューション理論におけるモデル圏 $`\mrm{Model}(\Sigma)`$ と同一視可能でしょう。おわりにこの記事で定義した $`\mrm{Sys}`$ は、複圏〈オペラッド〉をインデキシング空間とするインデックス付きシステム空間でした。マイヤースは、グロタンディーク二重構成の後で、できた二重圏上の二重インデックス付き圏を定義しています。「状態遷移系達の二重圏の直接的定義」より： なお、マイヤースは、二重圏上の二重インデックス付き圏〈dou…

…論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです 地雷原になってしまう大きな理由に、ターンスタイル記号 '$`\vdash`$'、二重矢印 '$`\Rightarrow`$'、上段・下段を区切る横棒などの記号が多義的に使われ、その意図・意味・使用法が読み取りにくいことがあります。型理論の判断〈judgement〉に使われるターンスタイル記号と、演繹系〈演繹システム〉に対するメタ命題で使われるターンスタイル記号と、シーケン…

…ッドが型理論／論理／インスティチューション理論に対して、統合的・整合的な枠組みを与えるだろう、と思っています。それは、最近の記事達の内容や動機になっています。 コンテキスタッド、包括圏、ハイパードクトリン 型理論とコンテキスタッド： コンテキストフル射 包括コンテキスタッドに向けて 型理論周辺、何で混乱するのか？ 型理論、論理、インスティチューション理論をすべて、コンテキスタッドの枠組みで定式化して同時に扱いたいのです。現状の用語・記号のコンフリクトや不整合をある程度は解消し…

…論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです*1。最近、包括コンテキスタッド（「型理論とコンテキスタッド： コンテキストフル射」「包括コンテキスタッドに向けて」参照）を使えば、型理論周辺をうまく整理できるのではないかと思っています。しかし、仮にうまく整理できたとして、それでも混乱をまねく要因は取り除けないでしょう。そもそも、以下に挙げるダイコトミー〈概念の二分法〉による区分けが難しいのです。その難しさが混乱の要因とな…

…み合わせは、型理論やインスティチューション理論に向いているようです（「型理論とコンテキスタッド： コンテキストフル射」参照）。この記事では、包括コンテキスタッド（包括圏とコンテキスタッドの組み合わせ）を定義し利用するために必要な諸々の準備的事項をバラバラと記します。コンテキスタッドのための用語集〈グロッサリー〉といった趣です。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newc…

…。「リダクト関手」はインスティチューション理論で使われる言葉です。「$`\cat{C}`$ の対象 $`\mapsto`$ ファイバー〈局所圏〉」「$`\cat{C}`$ の射 $`\mapsto`$ リダクト関手」という対応は反変関手ですが、この反変関手は、ファイブレーション〈ファイバー付き圏〉 $`\pi: \cat{E}\thto \cat{C}`$ から逆グロタンディーク構成（「グロタンディーク構成・逆構成と同値対応」参照）で得られたインデキシング〈インデックス付き圏…

…り色々です。型理論やインスティチューション理論に使うことを目的にして、包含的圏に関して整理しておきます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} %\newcommand{\msf}[1]{\mathsf{#1}} \newcommand{\twoto}{\Rightarrow } %\newcommand{\…

…か？ 型理論／論理／インスティチューション理論の引っ越し コンテキスタッドと特殊ケース達コンテキスタッド〈contextad〉はある種のモナド（正確にはスード高次モナド）です。モナドなので、台の上に単位と乗法が載った代数構造（モノイド構造）になります。コンテキスタッドの台はスパンです。次の形に書きます。$`\quad \cat{C}\overset{\pi}{\ot}\cat{E} \overset{\odot}{\to}\cat{C}`$ このスパンは、一般的にはパラダイス…

…ら特性関手へ型理論とインスティチューション理論で共通に登場する関手をエス関手〈ess functor〉と呼んだのは、関手の値である集合の要素が「型理論では sort」、「インスティチューション理論では sentence」、「拡張包括構造としては拡張の step」なので、どれもエスだからです。論理まで考えると、エス関手の値である集合の要素は、「proposition〈命題〉」、「predicate〈述語〉」、「property〈性質〉」などと呼ばれます。それじゃピー関手か？ と…

…ート、論理では命題、インスティチューション理論では文と呼ばれているもの（「コンテキストの圏と指標の圏と限量子 // エス関手」参照）。 射影〈projection〉： クランのファイブレーションクラスの要素である射。ファイブレーション、ディスプレイ射とも呼ぶ。 コンテキスト拡張〈context extension〉： コンテキスト $`\Gamma`$ と拡張ステップ $`A\in |\msc{S}(\Gamma)|`$ から新しいコンテキスト $`\Gamma\cdot A…

…理論〈依存型理論〉／インスティチューション理論／論理の圏論的定式化において、かなり使いやすい圏（のドクトリン）です。例1： 集合達の包括クラン最初の具体例は、依存性を持たない包括クランです。包括クランの各構成素を次のように決めます。 台圏： 空集合を除いた集合圏 $`\mbf{Set}_+`$ 終対象： 単元集合 $`\mbf{1} = \{\emptyset\}`$ （要素が空集合であるのは別にかまわない） ファイブレーションクラス： すべての全射からなるクラス エス関手：…

…導入して、“型理論／インスティチューション理論のための圏論”のツールボックスに付け加えます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\msc}[1]{\mathscr{#1}} \newcommand{\u}[1]{\underline{#1}} %\newcommand{\id}{\…

「ν-インスティチューションでは健全性の定義と証明が出来る」で述べた「ν-インスティチューションの健全性」が示せるのは、充足関係の定義がうまいこと働くからです。では、充足関係の定義がどこから来たのでしょうか？ これは具体例を見たり触ったりしていれば思い至るものです。逆に、具体例がなかったら実験・観察ができないので、何もわからないし何も思いつかないでしょう。ν-インスティチューションやC-システムの具体例として僕がよく見たり触ったりしているのは、集合圏で解釈する等式的指標達の圏…

…l `$内容： ν-インスティチューション 包括圏とデカルト関手 エム関手、モデル関手 ν-インスティチューションの健全性 ν-インスティチューション「ダラッっと依存型理論・インスティチューション // ν-インスティチューション」において、「ν-インスティチューション」〈nu-institution〉という言葉を出したんですが、それ以前に「半具象インスティチューション〈semi-concrete institution〉」と呼んでいたものに別名を与えただけです。「半具象イン…

…024年の「型理論とインスティチューションの周辺」、「カートメル／ヴォエヴォドスキー／パルムグレンの型理」でも引用しています。相対随伴〈relative adjunction〉という概念は、1968年にウルマー〈Friedrich Ulmer〉が提案しているようで、随分と古いのですが、相対モナドとしてリバイバルさせたのはアルテンキルヒ／チャップマン／ウウスタルです。 [ACU14-] Title: Monads need not be endofunctors Authors…

…の反対圏」「型理論とインスティチューション理論が繋がるぞ！」「指標の圏に対する余ディスプレイ包含構造」で述べたように、コンテキストの圏と指標の圏は互いに反対圏です。この事実を利用することにより、型理論とインスティチューション理論を密接に結びつけることができます。また、ローヴェア流の限量子の定式化をコンテキストの圏（指標の圏でもある）に組み込むことができます。このとき、コンテキストの圏の構造の一部は、ハイパードクトリンとしての役割りを持ちます。$` \newcommand{\m…

…の反対圏」「型理論とインスティチューション理論が繋がるぞ！」で述べたように、指標の圏とコンテキストの圏は互いに反対圏です。まさに表裏一体の関係にあります。となると、コンテキストの圏に関する知見を用いて指標の圏を調べる、あるいは逆に、指標の圏に関する知見を用いてコンテキストの圏を調べることが出来ることになります。指標の圏には包含構造を載せることが多いです。包含構造には幾つかの種類があるのですが、コンテキストの圏のディスプレイクラスを双対化して新種の包含構造を定義してみます。$`…

… 意味論的構造（例：インスティチューション）における、構文的対象の妥当性〈validity〉の（メタレベルの）宣言 4番の意味でターンスタイルを使うのは見たことないですが、ないとも言い切れません。プロファイル宣言は、圏論の意味での射の域・余域の仕様です。高次圏〈n-圏〉の高次射〈k-射〉、複圏〈オペラッド〉の複射、多圏の多射のプロファイルもあります。構文的対象が整形式〈well-formed〉だとは、コミュニケーションに使われる記号的・図形的表現がデタラメではなくて（真偽はと…