…たのですが、ここではインスティチューション理論にならって文〈sentence〉と呼ぶことにします。「文とは何か？」には答えず、演繹系を構成する集合 $`S`$ の要素だと位置付けます。演繹系の演繹ステップ $`s`$ は、適当な自然数 $`n`$ に対して次のように書けます。$`\quad s = ((s_1, \cdots, s_n), s_0) \in S^n \times S`$$`n`$ 個の文の並び $`(s_1, \cdots, s_n)`$ がステップの仮説〈h…

…数学〉／モデル理論／インスティチューション理論の「指標」は同じモノである。 コンテキストを対象としてコンテキスト射を射とする圏がある。それが型理論で扱う圏〈型理論的圏〉である。正確に言えば： 型理論的圏の公理系が幾つかある。「ダラッっと依存型理論・インスティチューション // 色々な型理論的圏」参照。 公理系で規定される型理論的圏の対象を習慣として「コンテキスト」と呼ぶ。 公理系で規定される型理論的圏の射を「コンテキスト射」と呼ぶ。 コンテキストを対象としてコンテキスト射を射…

…ラッっと依存型理論・インスティチューション // 色々な型理論的圏」参照）ので、特にカートメル／ヴォエヴォドスキー／パルムグレンの型理論ではどう解釈するかを次節で説明します。コンテキスト拡張前節で指摘したように、型理論、圏論、集合論、論理を一緒に語る際の困難は、記号法・用語法がグチャグチャになってしまうことです。記号法・用語法は圏論のものを使って整理することにします。他の分野の記号法・用語法としては奇妙になってしまうかも知れません。「0-圏または1-圏」を「(0|1)-圏」の…

…グレンの包括圏 ν-インスティチューション ダラッの続きは？ 色々な型理論的圏タイトルに「依存型理論」と書きましたが、現在の型理論は、マーチンレフ〈Per Erik Rutger Martin-Löf | マルティンレーフ〉に端を発する依存型理論の系譜上にあり、単に「型理論」と言ってもそれは依存型理論のことでしょう。依存性を扱わない型理論が無意味というわけではないですが、現実的問題だと依存性無しでは表現力が不足なことが多いです。依存型理論を圏論ベースで展開するとして、どんな方…

… algebra〉やインスティチューション理論の意味の指標です。ただし、指標の記述に依存型が使えます。つまり、依存指標〈dependent signature〉ということになります。モノイドの指標は依存型なしで書けますが、ホムセットベースの小さい圏の指標は依存型がないとうまく書けません。その意味で、GATのベース指標はLATの指標（単ソート代数的指標）に比べて記述力が向上しています。ベース対象〈ベースコンテキスト | ベース指標〉 $`\Gamma \in |\cat{B}|…

インスティチューション理論の骨組みに、型理論やモナドを使って肉付けしようという目論見（「構文付き変換手インスティチューション 1/n」における“半具象インスティチューション”）は、型理論的圏の反対圏が指標の圏として使えることが分かってちょっと進捗しました（「型理論とインスティチューション理論が繋がるぞ！」参照）。このタイミングで、型理論的圏について再確認しておきます。型理論的圏 -- つまり型理論／型システムの圏論的モデル*1は、色々と提案されています。カートメルのコンテキス…

ビンゴ！ 「インスティチューションの“指標の圏”の具体化として、型理論的圏の反対圏をとればいいだろう」と見当をつけていたのですが、アタリだったようです。型理論的圏は、拡張包括構造を持ちます。拡張包括構造を持つ圏上の、プルバック四角形（コスパンの極限）を保つ余インデックス付き圏は、自動的に、反対圏上にインスティチューション構造をもたらします。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}…

…帰納」参照 *2:パルムグレンは "multivariable presheaf" と呼んでますが、"variable" は不要でしょう。 *3:パルムグレンは「直接拡張関係」を使っています。 *4:"connecting map" は、「型理論とインスティチューションの周辺」で引用した論文[Sub21-]で使われていた用語、"canonical projection", "canonical pullback square" は[AENR23-24]で使われていた用語です。

…ド 構文論と形式言語インスティチューションは、構文論と意味論の枠組みを与えます。抽象的な枠組みだけで、中身はありません -- それが悪いってことではないです。が、より詳細で具体的な構造も付け足したいとは思います。「構文付き変換手インスティチューション 1/n」で出した言葉「半具象インスティチューション〈semi-concrete institution〉」は、インスティチューションの大枠（いわば骨）に、より詳細で具体的な構造（いわば肉）も付け足したものを意味します。インスティ…

「構文付き変換手インスティチューション 1/n」において、半具象インスティチューション〈semi-concrete institution〉という言葉を出しました。インスティチューション理論における指標の圏〈category of signatures〉やモデル関手〈model functor〉は、公理的・天下りに与えられるので、まったく具体性を持ちません。（完全に具体的でなくても）もうちょっと具体的に規定されたインスティチューション、という意味で「半具象インスティチューショ…

…ては、構文付き変換手インスティチューション（「構文付き変換手インスティチューション 1/n」参照）のフレームワークが使えるでしょう。ファイブレーションの扱いは、ファイブレーション達を射のクラス（「射のクラスと制約付きスパン」）と考えたほうが良さそうです。‥‥ 続きはまた。 *1:Graphvizで描いたのですが、アルファベットが逆順に並ぶのを調整できませんでした。どうやるんかな？ *2:「フレーム付き指標の充填問題」が適切でしょうか？ *3:いつでもこの用法で「空間」を使うわ…

…antics〉とは、インスティチューション理論において抽象的・公理的に要請されるモデル関手を、具体的に構成するための手法です。また、ローヴェア〈William Lawvere〉の関手意味論〈functorial semantics〉の拡張でもあります。全般的な枠組みの解説は以下の過去記事にあります。 構文付き変換手インスティチューション 1/n まずは、指標という概念を具体化します。具体的に定義された指標を（抽象的・公理的な場合と対比して）具象指標〈concrete sign…

…論は「構文付き変換手インスティチューション 1/n」から始まる一連の記事達（まだ途中）で書こうとしています。実際的な指標とその使い方の例は「構造記述のための指標と名前 1/n 基本」に書いています。また、指標は「圏論におけるフレーム充填問題」とも密接に関係します。インスティチューション理論で出てくる指標は、まったく抽象的な存在物です。指標の実体・正体は何もなくて、単に“指標の圏”の対象を「指標」と呼ぶだけのことです。“指標の圏”も具体物ではなくて、インスティチューションの公理…

…とめんどくさくて‥。 *2:名前の細かい種別は、多くの場合、名前を圏のk-射と解釈したときの次元 k です。二重圏では、1-射がさらにタイト1-射、プロ1-射に分類されます。「二重圏、縦横をもう一度」参照。 *3:指標拡大は、構文付き変換手インスティチューション（「構文付き変換手インスティチューション 1/n」参照）では、非常に重要です。 *4:僕は、テキストによる記述は“必要悪”だと捉えています。「「コミュニケーションの多次元化」という革命に立ち会っているのだと思う」参照。

「構文付き変換手インスティチューション 2/n 実例：モノイド」でモノイドに関する実例を出しました。この記事では別な実例、多項式に関わるインスティチューションを紹介します。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\op}{ \mathrm{op} } \newcommand{\In}{\text{ in }} \newcommand{\u}[1…

「構文付き変換手インスティチューション 1/n」で言い残していることはあるのですが、いったんそれは棚上げにして構文付き変換手インスティチューションの実例を挙げます。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\op}{ \mathrm{op} } \newcommand{\In}{\text{ in }} %\newcommand{\u}[1]{\…

…Burstall〉のインスティチューションが優れたフレームワークです。が、上記のような構造を扱うには幾つかの問題があります。 抽象的過ぎる。 構文を表現する手段が貧弱。 高次元のサポートがない。 そこで、具象的で構文を表現できて高次元（当面は2次元）を扱えるインスティチューションを考えようと思い立つわけです。もう何年も前からそう思っています。が、なかなかうまくいかない。素材がうまく噛み合ってくれないのですよ。最近になって、「なにがマズいのだろう？」とかえりみると、次元・サイズ…

…らの事例を確認かな。インスティチューション（抽象モデル理論）からも事例が作れそうな気がしますが、気がするだけで（現時点では）それ以上わかりません。依存アクテゴリーを定義する環境となる二重圏（いわば、外の二重圏）についても調べる必要があります。環境の二重圏はサイズが大きくて緩い構造なので、扱うのは大変です。うまい計算法を選ばないと一貫性地獄で苦しむことになりそう。 *1:バエズ〈John C. Baez〉が説明に使っていた絵、出典不明。 *2:画像は https://www.a…

…13 演繹系と閉包系インスティチューション〈institution〉は、論理の意味論〈モデル論〉を抽象化した構造です。論理の構文論〈証明論〉を抽象化した構造としてπ-インスティチューションがあります。π-インスティチューションについては、例えば次の論文など： Title: Refinement by interpretation in π-institutions Authors: César Rodrigues, Manuel A. Martins, Alexandre M…

…tor〉と呼びます。インスティチューション理論ではリダクト関手〈reduct functor〉と言います*2。言いやすいというだけの理由（他意はない）で、「リダクト関手」を使うことにします。リダクト関手は $`g^*`$ と略記されることがあります（もちろん、$`\cat{P}`$ は周知として）。トータル圏に埋め込まれた局所圏 $`\cat{P}[X]`$ は、ファイブレーション射影の逆像とみなせます。$`\quad P^{-1}(X) \cong \cat{P}[X] \…

…ナド 構文モナド をインスティチューション理論の意味での指標の圏だとします。対象 は指標です*1。なにかしら「指標から項を生成するメカニズム」があるとします。そのメカニズムは文法／構文生成規則と言っていいかも知れません。指標 から生成された項の集合を とします。 は単なる集合ではなくて何らかの構造を持つかもしれません。その構造込みで だとしましょう。 は圏 の射（指標射）にも定義できて、 は圏 上の自己関手になるとします。つまり： が大きい圏である可能性も考えて （小さい圏達…

…プログラム意味論（のインスティチューション理論）ではリダクト関手〈reduct functor〉、インデックス付き圏の文脈では再インデキシング関手〈reindexing functor〉とも呼ばれます。モデル移行関手を使えば、異なる統計セオリー上の統計モデルを比較することができます。パターソンは、モデル移行関手の実例も出しています。例えば、線形モデルが一般化線形モデルの特殊例であることは直感的には当たり前そうですが、厳密な記述と証明は出来るでしょうか？ パターソンの動画でこの…

…つも助けてくれるのはインスティチューション理論です。インスティチューション理論をベースに考えるのが良さそうです。少なくとも僕にとっては、インスティチューション理論が一番頼りになる足場です。インスティチューション理論の基礎概念に指標〈signature〉があります。指標をモジュールと考えることもできますが、規模が小さすぎるので、幾つかの指標をまとめたグループをモジュールと考えるのが良いでしょう。つまり、「モジュールとは何か？」に対しては「指標の集まりがモジュールだ」と答えること…

…性だけを要求します。インスティチューション理論（そういう理論がある）では、左単位律のような条件〈公理〉は指標とは切り離しますが、「何を条件として切り離すか？」の基準がハッキリしないので（「指標と仕様」参照）、ここでは条件〈公理〉も指標内に記述します*1。指標内のキーワードを変える「多相関数の「パラメトリック性 vs 満足性」」にて： 標準的なキーワードは、type, function ではなくて、sort, operation ですが、キーワードに違和感を持つ人が多いので t…

…。満足性の定義には、インスティチューション理論の道具立てを使います。が、インスティチューション理論を知っている必要はありません。Xさんは「lengthらしさ」を内心期待してましたが、3人に伝えてません。「lengthらしさ」を何個かの文として言語化しなくてはなりません。実際の関数fが、文sで記述された性質を実際に持つとき、次のように書きます。 f |= s 記号'|='（TeXだと \vDash ''）は、満足関係〈充足関係 | satisfaction relation〉の…

…情です。「等式的関手インスティチューション（概要）」で述べたように、等式的関手インスティチューションでは、指標Σに対するモデル圏*1 Model[Σ] を、関手圏*2として具体的に構成するのでした。 Model[Σ] := [Σ◇, Set] 上記の右辺によりモデル圏が定義されますが、右辺に登場する (-)◇ と [-, -] の意味がハッキリしないと定義したことになりません。実際、これじゃ全然ハッキリしてません。モデル圏の定義をハッキリさせようとすると、圏論では常につきまと…

…Burstall〉のインスティチューション〈institution〉を少し具体的に考えたい、ってことでした。どのように具体化したいかと言うと： 使う論理を、等式的論理と一階述語論理に固定する。 指標Σに対するモデルの圏を、Model[Σ] := [FreeCat(Σ), Set]CAT と具体的に与える。 指標圏を固定する気はないのですが、当座の指標圏としては、有向グラフの圏を採用します。ただし、単に「有向グラフ」と言ってしまうと誤解をまねきそうです。通常の有向グラフGと、両…

…Burstall〉のインスティチューション〈institution〉は、論理やプログラムの構文論と意味論〈モデル論〉の抽象的枠組みを提供します。抽象度が高いゆえに、一般的で汎用性が高いのですが、ちょっと掴みどころがない感じもします。そこで、抽象的インスティチューションの一部を具体化します。 使う論理を固定する： 抽象的インスティチューションは論理非依存〈logic nutral | logic agnostic〉がウリなんですが、使う論理を等式的論理と一階述語論理に固定します…

…指標とモデルの理論（インスティチューション理論含む）と、ローヴェア理論（ちゃんと言うと、「ローヴェア理論」の理論）と、形状圏を使ったホモロジー／コホモロジーが扱っているモノ達は、酷似しているのでしょう、おそらく。書き方に関する注意：ある言葉の同義語がある場合は、山形括弧（'〈'と'〉'）で囲んで示します。内容： モノイド対象 モノイドの指標 集合圏において具体化 順序集合の圏において具体化 ベクトル空間の圏において具体化 ローヴェア圏 モノイドの指標のローヴェア圏 ローヴェア…

…〉と呼ぶ人もいます。インスティチューションの理論などでは、法則が入ってない指標と、法則を入れた仕様を区別したほうが確かに分かりやすいです。なんでもかんでも指標で済ませると、区別したいときに困るような気がします。多パート指標トム・レンスター〈Tom Leinster〉は（例えば https://arxiv.org/abs/math/9810017 で）、指標をデータ・パートと公理パートに分けて書いています（書き方はインフォーマルですが*1）。モノイドの指標をパート分けして書き直…