「判断的セオリーと判断計算」においてコラリア／ディ-リベールティの判断計算を、「メリス／ジルバーガーの圏論的判断計算」においてメリス／ジルバーガーの判断計算を紹介しました。コラリア／ディ-リベールティはちょっと複雑過ぎる印象で、メリス／ジルバーガーは単純過ぎる印象を持ちました。中庸の圏論的判断計算とはどのようなものでしょう。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\In}{\text{ in }}
\newcommand{\twoto}{\Rightarrow }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{ \text{－} }
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\incto}{\hookrightarrow }
%
\newcommand{\Over}{\sqsubset }
\newcommand{\VRule}{\downdownarrows}
\newcommand{\HRule}{\rightrightarrows}
\require{color} % Using
\newcommand{mag}[1]{\textcolor{magenta}{#1}}
`$
内容：
判断計算のモデル
コラリア／ディ-リベールティとメリス／ジルバーガーは、似たようなアイディアで似たような話題を扱ってますが、用語法がだいぶ食い違っているので調整しておきます。
| コラリア／ディ-リベールティ | メリス／ジルバーガー | この記事 |
|---|---|---|
| 判断的セオリー | 型詳細化システム | ターゲット・ドクトリン |
| コンテキスト | 型 | |
| 判断、カインド | 型達の圏 | カインド |
| 判断、{判断}?分類子 | 型詳細化システム | 粗視化 |
| 規則 | 型詳細化システム | 粗視化 |
| ポリシー | ポリシー | |
| 演繹規則 | 推論規則 | 導出ステップ |
| 判断 | 判断、問題図式 | |
| 導出 | 根拠、解図式 | |
| 判断的構造 |
判断計算はある種の形式体系とします。その圏論的モデルが判断的セオリーや型詳細化システムですが、ここでは特別な構造を準備しないで、既存のドクトリンをモデルだとします。ここでのドクトリン〈doctrine〉とは、対象が圏類似構造である圏類似構造です。具体的には以下のようなドクトリンを考えます。
| $`\text{small size}`$ | $`\text{large size}`$ |
|---|---|
| $`\mbf{Cat}`$ | $`\mbf{CAT}`$ |
| $`\mbf{Prof}`$ | $`\mbf{PROF}`$ |
| $`\mbf{ProfDC}`$ | $`\mbf{PROFDC}`$ |
| $`\mbf{MultiCat}`$ | $`\mbf{MultiCAT}`$ |
| $`\mbf{SymMonCat}`$ | $`\mbf{SymMonCAT}`$ |
| $`\mbf{DblCat}`$ | $`\mbf{DblCAT}`$ |
それぞれのドクトリンの対象〈0-射〉、射〈1-射〉、2-射は：
- 圏、関手、自然変換
- 圏、プロ関手、自然変換
- 圏、関手とプロ関手、自然変換
- 複圏、複関手〈複圏の射〉、複自然変換〈複関手の自然変換〉
- 対称モノイド圏、対称モノイド関手、対称モノイド自然変換
- 二重圏、二重関手、2-射は不明
これらはいずれも具体的に与えられるドクトリンです。判断的セオリーのような、新しい抽象的構造を定義することはしません -- その必要性を感じないので。
既存のドクトリンからひとつを選んで、それを判断計算のターゲット・ドクトリン〈target doctrine〉とします。形式体系としての判断計算は、ターゲット・ドクトリンに対して意味解釈をします。
ターゲット・ドクトリンの対象〈0-射〉をカインド〈kind〉、ターゲット・ドクトリンの射〈1-射〉を粗視化〈coarsening〉と呼びます。粗視化の実体は関手、プロ関手、複関手、対称モノイド関手、二重関手など、ターゲット・ドクトリンにより変わります。ターゲット・ドクトリンの2-射はポリシー〈policy〉です。
ターゲット・ドクトリンの0-射、1-射、2-射に独特の名前を与えるのは、0-射〈カインド〉の0-射、1-射、2-射との混同を避けるためです。「カインド」「ポリシー」はコラリア／ディ-リベールティから、「粗視化」は、メリス／ジルバーガーの「詳細化」の反対語にしました。実際の例では、ターゲット・ドクトリンの1-射として忘却関手やファイブレーションを使うことが多いので、情報の一部を落としている感じがしたからです。とはいえ、「粗視化」は単なる呼び名なので、関手、プロ関手、複関手、対称モノイド関手、二重関手などが粗視化の実体になり得ます。
「カインド ＝ ターゲット・ドクトリンの0-射」「粗視化 ＝ ターゲット・ドクトリンの1-射」「ポリシー ＝ ターゲット・ドクトリンの2-射」という呼び名は一般論で使用するだけで、個別の事例ではそれぞれ別な呼び名を使うでしょう。
コラージュ図式
コラージュ図式〈collage diagram〉は、ここでの判断計算の主役です。通常の図式と同様に、形状〈shape〉である図形の各セルにターゲット・ドクトリン内のモノを割り当てます。ただし、割り当てるモノはカインド内の対象・射に限りません。
まずはコラージュ図式の形状ですが、これは2次元のグラフです。通常の有向グラフに、多辺形を境界とする多角形を貼り付けた組み合わせ幾何的図形です。2次元グラフの頂点〈0-セル〉、辺〈1-セル〉、多角形〈2-セル〉には、属性〈attribute〉を付けることができます。属性により、セルに割り当て可能なモノを制限します。
例えば、メリス／ジルバーガーの割り当て計算を再現するには、次の属性値を使います。
| セル | 属性値 |
|---|---|
| 頂点 | object |
| 辺 | morphism, valuation |
| 四角形 | commutative, lift |
属性値の意味は次のようです。
- object ： ターゲット・ドクトリン内のカインドの対象
- morphism ： ターゲット・ドクトリン内のカインドの射
- valuation ： ターゲット・ドクトリン内の粗視化（関手など）の値割り当て〈value assignment | valuation〉
- commutative ： 可換多角形、境界の辺はすべて morphism である必要がある。
- lift ： 2本のmorphism辺と2本のvaluation辺からなる四角形でmorphism達が粗視化で対応している。
使用例は「メリス／ジルバーガーの圏論的判断計算」にあります。
他の属性値としては：
- 2-morphism ： ターゲット・ドクトリン内のカインドの2-射
- component ： ターゲット・ドクトリン内のポリシー（自然変換など）の成分である1-射
- pullback ： プルバック四角形
- pushout ： プッシュアウト四角形
- cartesian-lift ： 関手のデカルト持ち上げになっている四角形
- hetero-morphism ： プロ関手のヘテロ射（「これは良い！ プロ関手の代替としての混合圏」参照）
ここまでの例では、属性値は単なる名前ですが、もっと複雑なデータを属性にしてもかまいません。形状に付けられた属性は、その形状のコラージュ図式を制約〈constrain〉します。
$`\msc{T}`$ をターゲット・ドクトリンとします。$`S`$ を、セルに属性値が割り当てられた2次元グラフとします。属性による制限を守って、セルにターゲット・ドクトリン内のモノを対応させる写像がコラージュ図式〈collage diagram〉です。コラージュ図式 $`D`$ は次のように書きます。
$`\quad D:S \leadsto \msc{T}`$
グニグニの矢印記号 '$`\leadsto`$' は、「関手のデカルト射とファイバー付き圏」で使っています。上記過去記事で導入した関手ターゲットの図式〈functor-targeted diagram〉は、コラージュ図式の典型例です。
コラージュ図式を話題にしている文脈では、コラージュ図式を単に「図式〈diagram〉」とも呼びます。なお、「コラージュ」は、プロ関手のコグラフ〈cograph of a profunctor〉とは直接の関係はありません。普通の辞書的意味である「異なる素材を組み合わせて一つのものを作る技法」にちなみます。
コラージュ図式の形状（属性付きの2次元グラフ）達は圏を形成するとします。その圏を $`\cat{S}`$ とします。圏 $`\cat{S}`$ は充分モノ包含的圏〈adequate monic inclusive category〉（「包含的圏の事例と反例」参照）であることを要求します。そうでないと、コラージュ図式のテンプレートをうまく定義できません。
$`S, T\in |\cat{S}|`$ として、圏 $`\cat{S}`$ の射 $`i`$ が包含射であることを次のように書きます。
$`\quad i: S \incto T \In \cat{S}`$
包含射の定義は、2次元グラフ $`S`$ が2次元グラフ $`T`$ の（属性も含めて）部分グラフであることだとして定義します。図式達の圏 $`\cat{S}`$ の射で必要なものは包含射なので、なんなら、すべての射が包含射である（包含射しかない）圏でもかまいません。
2つのコラージュ図式 $`D, E`$ のあいだの射は、通常の流儀のとおり、ベースパートとファイバーパートの組み合わせで定義します。今回は、話を簡単にするために、ファイバーパートは恒等に限ることにします。つまり、コラージュ図式 $`D, E`$ のあいだの射はベースパートだけで決まります。以下の図のようです。
$`\quad \xymatrix@C+1pc{
S \ar@{~>}[dr]^{D} \ar[dd]_{\varphi}
\ar@{}@/^1.5pc/[dd]|{\text{comm.}}
&{}
\\
{}
&{\msc{T}}
\\
T \ar@{~>}[ur]_{E}
&{}
}
`$
三角形内の $`\text{comm.}`$ は可換であることを示します。形状達の圏 $`\cat{C}`$ の射 $`\varphi`$ による $`E`$ のプレ結合引き戻し〈pre-composition pullback〉を $`\varphi^*(E)`$ として、上の図式は次の等式を意味します。
$`\quad D = \varphi^*(E) : S \leadsto \msc{T}`$
この等式は、$`D \to E`$ という図式のあいだの射も定義します。図式の射は、形状の射 $`\varphi: S \to T`$ と余域の図式 $`E`$ のペア $`(\varphi, E)`$ で決まります。なぜなら、域の図式は $`\varphi^*(D)`$ として求めることができるからです。$`(\id_S, D)`$ は図式 $`D`$ の恒等射です。
形状（属性付き2次元グラフ）達の圏 $`\cat{S}`$ とターゲット・ドクトリン $`\msc{T}`$ が決まると、コラージュ図式達の圏も決まります。それを次のように書きます。
$`\quad \mrm{ColgDiag}^{\cat{S}}(\msc{T})`$
単一のコラージュ図式だけではあまり面白いことは出来ません。コラージュ図式のテンプレートを次節で定義します。
テンプレート、問題図式、解図式
ストリング図やペースティング図をテンプレート化して使うことは重要です。テンプレートやテンプレート充填問題（当初はフレーム充填問題と呼んでいた）については、以下の過去記事に書いています（「メリス／ジルバーガーの圏論的判断計算」でも挙げた過去記事リストです）。
- モノイド圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈
- オペラッドと型付きラムダ計算
- 圏論におけるフレーム充填問題
- 1-圏でもフレーム充填問題、因子分解と比較子
- フレーム充填問題と解空間関手
- ストリング図、ストリング図動画が“使える”とは？
ここから先、$`S, T`$ などは、形状達の圏 $`\cat{S}`$ の対象ではなくて、包含射を表わすとします。包含射は、域と余域から一意的に決まってしまうので、次のように書けます。
$`\quad S = (\mrm{dom}(S) \incto \mrm{cod}(S)) \In \cat{S}`$
今の文脈では、次の記法を使います。
$`\quad S_\mrm{giv} := \mrm{dom}(S)\\
\quad S_\mrm{tot} := \mrm{cod}(S)
`$
包含射 $`S`$ の域 $`S_\mrm{giv}`$ を、$`S`$ の所与パート〈given part〉または既知パート〈known part〉、余域 $`S_\mrm{tot}`$ を、$`S`$ の全体パート〈total part〉と呼びます。形状のあいだの包含射の別名としてテンプレート形状〈template shape〉を使います。
テンプレート形状 $`S = (S_\mrm{giv}\incto S_\mrm{tot})`$ の所与パートに属するセルは所与セル〈given cell〉または既知セル〈known cell〉と呼びます。所与セル〈既知セル〉ではないセルは不定セル〈indeterminate cell〉または未知セル〈unknown cell〉と呼びます。
$`S = (S_\mrm{giv}\incto S_\mrm{tot})`$ をテンプレート形状として、部分形状〈subshape〉 $`S_\mrm{giv}`$ にだけターゲット・ドクトリンのモノ（意味的実体）が割り当てられたコラージュ図式をコラージュ図式テンプレート〈collage diagram template〉と呼びます。コラージュ図式テンプレートは以下のように書けます。
$`\quad \xymatrix@C+1pc{
{S_\mrm{giv}} \ar@{~>}[dr]^{G} \ar@{_{(}->}[dd]_S
&{}
\\
{}
&{\msc{T}}
\\
{S_\mrm{tot}}
&{}
}
`$
$`G`$ は所与パートでのみ定義されたコラージュ図式です。
コラージュ図式テンプレートを実際に描くときは、未知パート〈不定パート〉のセルには疑問符、または先頭が疑問符である名前でラベルすることにします。例えば次がその例です。
$`\quad \xymatrix{
X \ar[r]^{?} \ar@{|->}[d]
\ar@{}[dr]|{?\, \text{lift}}
&Y \ar@{|->}[d]
\\
A \ar[r]_f
&B
}
`$
$`X, Y, A, B, f`$ は疑問符が付いてないので、所与パートへの実体の割り当てです。'$`\mapsto`$' の形の矢印（関手の値割り当て〈付値〉）も所与〈既知〉だとします。$`\text{lift}`$ は、四角形が関手の持ち上げ四角形であることを表わす属性です。$`X`$ から $`Y`$ への射と、四角形が実際に持ち上げであることが未知パートとなります。
コラージュ図式テンプレートを話題にしている文脈では、コラージュ図式テンプレートを単にテンプレート〈template〉とも呼びます。問題図式〈problem diagram〉はテンプレートの別名です。
問題図式〈コラージュ図式テンプレート〉$`(S, G)`$ に対して、以下の $`E = (S_\mrm{tot}, E)`$ を解図式〈solution diagram〉と呼びます。
$`\quad \xymatrix@C+1pc{
{S_\mrm{giv}} \ar@{~>}[dr]^{G} \ar@{_{(}->}[dd]_S
\ar@{}@/^1.5pc/[dd]|{\text{comm.}}
&{}
\\
{}
&{\msc{T}}
\\
{S_\mrm{tot}} \ar@{~>}[ur]_{E}
&{}
}
`$
つまり、問題図式の未知セル〈不定セル〉にも意味的実体を割り当てたコラージュ図式が解図式です。解図式は、“テンプレートの穴を埋めたもの”と言えます。
今定義した解図式は、“すべての穴を完全に埋めたもの”ですが、一部の穴だけを埋めた部分解図式〈partial solution diagram〉も考えることができます。とりあえずは、完全な解図式だけを扱うことにします。
判断と根拠
問題図式を判断〈judgement〉とも呼びます。問題図式に対する解図式を（判断に対する）根拠〈evidence〉とも呼びます。以下の用語達はすべて同義語ということです。
- 判断
- 問題図式
- テンプレート
- コラージュ図式テンプレート
同一の概念にたくさんの同義語が出現してしまうのは、習慣・伝統と折り合いを付ける都合からです。
言い回しとして； 図式 $`E = (S_\mrm{tot}, E)`$ が判断〈問題図式〉 $`(S, G)`$ の根拠〈解図式〉であるとき、
判断 $`(S, G)`$ は、根拠 $`E`$ により正当化〈justify〉される。
根拠 $`E`$ は、判断 $`(S, G)`$ を正当化〈justify〉する。
と言います。
判断 $`(S, G)`$ が根拠 $`E`$ により正当化されることを、次の記法で書くことにします。
$`\quad \vdash (S, G) \text{ by } E`$
$`\text{ by } E`$ の部分を書かない場合は、次の存在命題だと解釈します。
$`\quad \exists E.(\vdash (S, G) \text{ by } E)`$
正当化〈justification〉に関する命題には、判断と根拠が出現します。判断と根拠は、ターゲット・ドクトリン $`\msc{T}`$ と形状達の圏 $`\cat{S}`$ がないと定義できません。したがって、正当化に関する命題の背後には、必ず $`\msc{T}`$ と $`\cat{S}`$ があります。$`\msc{T}`$ と $`\cat{S}`$ のペア $`(\msc{T}, \cat{S})`$ を判断的構造〈judgemental structure〉と呼ぶことにします。
判断的構造は、コラリア／ディ-リベールティの判断的セオリーに相当するとも言えますが、コラージュ図式の形状達の圏 $`\cat{S}`$ に注目するので、その点では判断的セオリーとは違います。
判断的構造があれば、判断〈問題図式〉、根拠〈解図式〉、正当性〈可解性〉などの概念が定義可能です。ターゲット・ドクトリン $`\msc{T}`$ と形状達の圏 $`\cat{S}`$ が持つ構造と性質に基づいて、根拠構成子〈evidence constructor〉（解構成子〈solution constructor〉と同義）も定義可能です。
判断、根拠（メリス／ジルバーガーの用語では導出）、根拠構成子〈解構成子〉の概念があれば、判断計算〈judgement calculus〉の形式体系を構成可能です。判断計算の作り方のおおよそは、「メリス／ジルバーガーの圏論的判断計算」に書いています。
判断と根拠のテキスト化
判断はコラージュ図式テンプレートであり、根拠はコラージュ図式のことでした。どちらも図式です。コラリア／ディ-リベールティでもメリス／ジルバーガーでも、図式のテキスト化に労力が注がれるのですが、原則としてテキスト化はしないことにします。
テキスト化には多くの流儀・手法があり、テキスト化は大変です（「メリス／ジルバーガーの圏論的判断計算 // 圏論的意味論が鬱陶しい事情」参照）。テキスト化にエネルギーを奪われて消耗します。テキスト化の結果であるテキスト表現は、曖昧で不正確で、混乱と間違いを誘発します。何もいいことがありません。
テキスト化する場合でも、分野固有の特別な書き方はしないで、圏論の標準的記法を使います。ひとつだけ、非標準的な記法を導入するなら、「判断形式を普通に書く // ファイバーへの制限と依存ペア」で説明した縦棒記号があると便利です。縦棒記号は色々な用途がありますが、ファイバーへの制限の意味で使う縦棒記号はフェンス記号〈fence symbol〉と呼ぶことにします。
フェンス記号さえあれば、様々な意味で使うターンスタイル（'$`\vdash`$'）は不要です。ターンスタイルは、前節の正当性〈可解性〉命題だけに使用を限定できます。オーバーロードされたターンスタイルの解釈に悩むこともなくなります。
判断はシーケントと言っても同じことです。論理では「シーケント」という言葉が好まれる、というだけのことです。であるなら、論理のシーケントも論理固有の書き方はやめて、圏論の標準的記法にしてしまえば幸せになれそうです。今まで、各分野の習慣・伝統に配慮して、様々なテキスト化を尊重してきたつもりです -- オーバーロードとコンフリクトに苦しみながら。けど、なんだか疲れた。不毛な気がしてきた。バカバカしくなってきた。もう、やめようかな。
そしてそれから
コラージュ図式の形状は、属性付きの2次元グラフでした。これは、ペースティング図とだいたい同じです。ペースティング図ではなくてストリング図を使う方式も考えられます。以下の過去記事達で紹介したレイヤー化ストリング図がヒントになるかも知れません。
判断〈コラージュ図式テンプレート〉や根拠〈コラージュ図式〉の記述にテキスト形式を避けたいなら、テキスト言語に変わる図式言語が必要なわけです。図式言語を読み書きする環境がほとんど無いなかで、工夫と妥協でやりくりする、ってことになりますね。これはこれで茨の道かも。
