このブログの更新は X（旧Twitter）アカウント @m_hiyama で通知されます。
Follow @m_hiyama

ご連絡は上記 X アカウントに DM にてお願いします。

［参照用 記事］

メリス／ジルバーガーの圏論的判断計算

雑記／備忘

メリス／ジルバーガーの次の論文をチラ見・拾い読みしました。

ジャーナルの出版は2015年ですが、2013年にはインターネット上に公開されていたものです。

メリス／ジルバーガーは、ある種の判断計算〈judgement*1 calculus〉とその圏論的意味論を定義しています。判断計算の圏論的意味を与える圏論的構造を型詳細化システム〈type refinement system〉と呼んでいます。論文タイトルにある通り、型詳細化システムとは単に関手に過ぎません。つまり、単なる関手をモデル（圏論的意味）として判断計算を構成しています。

この記事では、メリス／ジルバーガーのアイディア・発想（の一部）を紹介します。最初のほうに、型理論や論理の圏論的意味論が鬱陶しい事情についても（愚痴を）書きます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#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{\Over}{\sqsubset }
\newcommand{\VRule}{\downdownarrows}
\newcommand{\HRule}{\rightrightarrows}
\require{color} % Using
\newcommand{mag}[1]{\textcolor{magenta}{#1}}
`$

内容：

参考資料

冒頭に挙げた論文以外に、ジルバーガーのスライドがあります。

次の論文は、[MZ15] の続編のようです（読んでないです）。モノイド関手やファイブレーション／双ファイブレーションのような条件付き関手をモデルにした場合の議論のようです。

  • [MZ13B-]
  • Title: Type refinement and monoidal closed bifibrations
  • Authors: Paul-André Melliès, Noam Zeilberger
  • Submitted: 1 Oct 2013
  • Pages: 29p
  • URL: https://arxiv.org/abs/1310.0263

圏論的意味論が鬱陶しい事情

圏論一般がシンドイ理由のかなりの部分が図式のテキスト化のシンドサでしょう。以下の過去記事があります。

ストリング図だけではなく、ペースティング図でもその他の図式でも、テキストに書き下すのは手間がかかり大変です。面倒くさいだけでなくて、「なんでこんなバカバカしい事をせにゃならんのだ？」というストレス／心的ダメージも大きいです。「心が折れる」のですよ。

僕は、「過渡期だからしょうがないんだ」と考えています（以下の過去記事参照）。

次の過去記事達でも愚痴（「疲れる」）やら対処やらを書いています。

さらに以下も関連する話ですが、「テキスト化はめんどくさい、やりたくねー」と言っています。

さて、メリス／ジルバーガーの型詳細化システムですが、冒頭で言ったとおりこれは単なる関手です。「関手」と「型詳細化システム」は完全に同義語です。関手に「型詳細化システム」という別名を与えているのは、圏と関手に関わる概念を判断計算の概念へと翻訳するためです。翻訳の最初の用語対応が「関手 ←→ 型詳細化システム」なのです。

メリス／ジルバーガーの与えた翻訳は見事なもので、その巧みさに関心します。一方で、このテの翻訳を見ると毎度「翻訳する必要があるのか？」という疑問も感じます。圏と関手に関わる概念は、圏の言葉と手法を使って語ればいんじゃないの？ と。

僕の疑問と違和感は、だいぶバイアスがかかったものです。「型理論も論理も最初から圏論の言葉と手法で作ればいんじゃないの」という極論が背景にあるので。現実的には、現状においては、翻訳をしない限り、異なる分野をブリッジすることはできません。型理論は型理論の言葉と手法、論理は論理の言葉と手法で語られているわけですから。

メリス／ジルバーガー論文 [MZ15] は、「判断的セオリーと判断計算」で紹介したコラリア／ディ-リベールティの論文 [CL21-24] から参照されていたものです。コラリア／ディ-リベールティもメリス／ジルバーガーも、判断計算という形式体系を話題にしています。アイディアもけっこう似ています。しかし、用語・記法は腰を抜かすほどに食い違っています。

翻訳のためには、圏論的構造と構成素に、従来からるある伝統的用語・記号を割り当てる必要があります。ちょっと視点が違うと、まったく違った割り当て方になってしまうのです。また、コラリア／ディ-リベールティは、簡潔なテキスト化のために異様に短いテキスト表示を定義しています。テキストの短縮のために過剰なオーバーロードやコアージョンを使っているのです（「簡潔にしないと死んでしまうなら」参照）。こういう現象を見ると、やっぱりテキスト化が諸悪の根源だなー、と思わざるを得ません。

判断計算とは何か？

判断計算〈judgement calculus〉とは導出系〈演繹系〉の一種です。導出系はオペラッドだとみなすといいでしょう。以下の過去記事を参照してください。

いつものことで、導出系〈演繹系〉とオペラッドでは用語法（概念へのラベルの貼り方）が違います。

オペラッド 演繹系
色 項 または 判断
生成オペレーター {演繹}?ステップ
オペレーター {演繹}?ツリー

「演繹〈deduction〉」と「導出〈derivation〉」と「証明〈proof〉」は互いに置き換え可能なので、演繹ステップは、導出ステップ、証明ステップでも同じです。

導出系と呼ばれるオペラッドは、非対称（対称とは限らない、しかし対称でもかまわない）色付きオペラッド〈non-symmetric colored operad〉です。色達の集合とステップと呼ばれる基本オペレーター達から生成されます。色達・ステップ達から自由生成された自由オペラッドに、オペラッドの演算と整合した同値関係（合同〈congruence〉と呼ぶ）により商集合を作るかも知れません。

つまり、導出系と呼ばれるオペラッドは次のモノ達から構成されます。

  1. 色の集合 $`C`$
  2. ステップの集合 $`S`$ 。各ステップのプロファイル（入出力の仕様）は $`\mrm{List}(C)\times C`$ の要素となる。
  3. 集合 $`C`$ と集合 $`S`$ とプロファイル関数 $`\mrm{prof}:S \to \mrm{List}(C)\times C`$ から自由生成された自由オペラッド $`\mrm{FreeOpd}(C, S, \mrm{prof})`$ 上の合同関係 $`E`$

導出系（と呼ばれるオペラッド）は、商オペラッド $`\mrm{FreeOpd}(C, S, \mrm{prof})/E`$ のことです。

では、どんな導出系（と呼ばれるオペラッド）が判断計算なのか？ と言うと、明確な定義はありません。ある人が「‥‥を判断計算と呼ぶ」と言えば、それが（その人の）判断計算の定義になります。ゆるい合意として、論理のシーケント計算や型理論の伝統的形式体系を模倣するような導出系が判断計算です。

メリス／ジルバーガーの判断計算とコラリア／ディ-リベールティの判断計算は別なものですが、どちらも、論理のシーケント計算や型理論の伝統的形式体系を模倣しようとしています。

なお、導出系に関する比較的最近の記事に次があります。

問題図式と解図式

問題の記述として使う図式、あるいは図式により記述された問題を問題図式〈problem diagram〉と呼ぶことにします。図式の描き方としてはペースティング図を使いますが、ストリング図を使ってもかまいません。

問題図式の具体例を挙げます。

$`\quad \xymatrix{
\cdot \ar[r] \ar@[magenta][d]_{?}
\ar@{}[dr]|{? \,\mag{\Downarrow}}
&\cdot
\\
\cdot \ar@[magenta][r]_{?}
&{?} \ar@[magenta][u]_{?}
}\\
\quad \In \cat{C}
`$

これは、圏 $`\cat{C}`$ 内に描かれた図式ですが、疑問符が付いた所には、$`\cat{C}`$ の対象・射・2-射が割り当てられていません。疑問符が付いた頂点、辺〈矢印〉、面はそれぞれ、未知0-セル〈unknown 0-cell〉、未知1-セル〈unknown 1-cell〉、未知2-セル〈unknown 2-cell〉と呼びます。一般的には未知セル〈unknown cell〉です。疑問符が付いてないセル（頂点、辺、面）は既知セル〈{known | given} cell〉です。

方程式の場合と同様に、問題図式は「与えられた既知セルに対して未知セルをすべて求めなさい」という問題を記述しています。わかりやすくするために未知セルの矢印に色を付けています。が、いつでも色を付けるとは期待しないでください。

問題図式をテキスト化するには、既知セルにも未知セルにも名前を付ける必要があります。

$`\quad \xymatrix{
A \ar[r]^{f} \ar@[magenta][d]_{?x}
\ar@{}[dr]|{?\xi\, \mag{\Downarrow}}
&B
\\
C \ar@[magenta][r]_{?y}
&?W \ar@[magenta][u]_{?z}
}\\
\quad \In \cat{C}
`$

名前に関する情報をすべてテキストで書き下します。

  1. $`A\In \cat{C}`$
  2. $`B \In \cat{C}`$
  3. $`f:A \to B \In \cat{C}`$
  4. $`?W \In \cat{C}`$
  5. $`?x : A\to C \In \cat{C}`$
  6. $`?y : C \to {?W} \In \cat{C}`$
  7. $`?z : ?W \to B \In \cat{C}`$
  8. $`?\xi :: f \twoto {?x}; {?y}; {?z} : A \to B\In \cat{C}`$

問題図式の解となる図式を解図式〈solution diagram〉と呼びます。以下は、先の問題図式に対する解図式です。

$`\quad \xymatrix{
A \ar[r]^{f} \ar[d]_{a}
\ar@{}[dr]|{\alpha\, {\Downarrow}}
&B
\\
C \ar[r]_{b}
&D \ar[u]_{c}
}\\
\quad \In \cat{C}
`$

解図式の情報をすべてテキストで書き下します。

  1. $`A\In \cat{C}`$
  2. $`B \In \cat{C}`$
  3. $`f:A \to B \In \cat{C}`$
  4. $`?W := D\; \In \cat{C}`$
  5. $`?x := a\; : A\to C \In \cat{C}`$
  6. $`?y := b\; : C \to D \In \cat{C}`$
  7. $`?z := c\; : D \to B \In \cat{C}`$
  8. $`?\xi := \alpha\; :: f \twoto a; b; c : A \to B\In \cat{C}`$

$`\cat{C}`$ が1-圏の場合、2-射は等式しかないので、$`\alpha`$ は次のような等式です。

$`\quad f = a; b; c : A \to B\In \cat{C}`$

解図式には既知セルも含まれます。問題図式の未知セルを埋めた結果である解図式のセルは解セル〈solution cell〉と呼びます。解図式は、既知セルと解セルから構成されます。

問題図式はテンプレート〈template〉と呼んでもまったく同じです。図式がストリング図である場合は、未知1-セル（0-セルではない）が“テンプレートの穴”で、未知0-セルが“テンプレートのスリット”になります。解セルは、穴やスリットへのフィラー〈filler〉になります。

ストリング図ベースのテンプレートや充填問題については以下の過去記事に書いています。

関手ターゲットの図式

メリス／ジルバーガーの型詳細化システムは関手のことでした。型詳細化システムにおける図式は、関手が絡んだ図式になります。これは、「関手のデカルト射とファイバー付き圏」で導入した関手ターゲットの図式になります。

関手 $`F:\cat{D}\to \cat{C}\In\mbf{CAT}`$ を前提として次の図式を考えます。

$`\quad \xymatrix{
S \ar[r]^g \ar@{|->}[d]
&T \ar@{|->}[d]
\\
A \ar[r]_f
&B
}\\
\quad \In F:\cat{D}\to\cat{C}
`$

この場合、無名の矢印 $`\mapsto`$ は、関手 $`F`$ による対応を示します。図式の内容をテキストに書き下すと次のようです。

  1. $`S \In \cat{D}`$
  2. $`T \In \cat{D}`$
  3. $`g:S \to T\In \cat{D}`$
  4. $`A\In \cat{C}`$
  5. $`B\In \cat{C}`$
  6. $`f:A\to B\In \cat{C}`$
  7. $`A = F(S)`$
  8. $`B = F(T)`$

四角形のなかに $`\text{lift}`$ と書き込んだ場合は、さらに次の条件が付くとします。

  • $`f = F(g)`$

$`\text{lift}`$ と書いてなくても、上記の条件を仮定していることもあります。

さらに、四角形のなかに $`\text{Cart.l.}`$ （Cartesian lift）と書き込んだ場合は、$`g`$ が $`f`$ のデカルト持ち上げ（「関手のデカルト射とファイバー付き圏」参照）であることを示します。次がその例です。

$`\quad \xymatrix{
S \ar[r]^g \ar@{|->}[d]
\ar@{}[dr]|{\text{Cart.l.}}
&T \ar@{|->}[d]
\\
A \ar[r]_f
&B
}\\
\quad \In F:\cat{D}\to\cat{C}
`$

「型理論とコンテキスタッド： コンテキストフル射 // 補足 追記（デカルト持ち上げ、コンテキスト拡張）」で示唆した書き方 $`f^{\Uparrow T}`$ を使うと、上記の図式の内容は次のようです。

  • $`S = f^*(T)`$
  • $`g = f^{\Uparrow T}`$

「包括コンテキスタッドに向けて // ファイブレーション的プルバック四角形」では、$`\text{Cart.l.}`$ である四角形をファイブレーション的プルバック四角形〈fibrational pullback square〉と呼んでいます。プルバック四角形と似た扱いができるからです。

上記のファイブレーション的プルバック四角形（デカルト持ち上げの四角形）を次のようにも書きます。

$`\quad \xymatrix{
S \ar@{|->}[d]
\ar@{}[dr]|{\text{Cart.l.}}
&T \ar@{|->}[d] \ar@{|->}[l]_{f^*}
\\
A \ar[r]_f
&B
}\\
\quad \In F:\cat{D}\to\cat{C}
`$

$`f^*`$ はファイブレーションから誘導される $`f`$ の再インデキシング関手〈re-indexing functor〉を表します。

メリス／ジルバーガーの判断と導出

この節では、メリス／ジルバーガーの用語・記法をそのまま使って、次の概念を説明します。

  • 型詳細化システム〈type refinement system〉
  • 型〈type〉
  • 詳細型〈refinement type〉
  • 詳細化する〈refines〉
  • 型付け判断〈typing judgement〉
  • 部分型付け判断〈subtyping judgement〉
  • 導出〈derivation〉

任意の関手 $`\mbf{U}:\cat{D}\to \cat{T}`$ を型詳細化システム〈type refinement system〉と呼びます。関手の余域圏 $`\cat{T}`$ の対象を型〈type〉、関手の域圏 $`\cat{D}`$ の対象を詳細型〈refinement type〉と呼びます。$`\mbf{U}(S) = A`$ のとき、「$`S`$ は $`A`$ を詳細化する〈refines〉」と言います。

以下の形の問題図式を型付け判断〈typing judgement〉と呼びます。

$`\quad \xymatrix{
S \ar@[magenta][r]^{?} \ar@{|->}[d]
\ar@{}[dr]|{\text{lift}}
&T \ar@{|->}[d]
\\
A \ar[r]_f
&B
}\\
\quad \In \mbf{U}: \cat{D} \to \cat{T}
`$

以下の形の問題図式を部分型付け判断〈subtyping judgement〉と呼びます。

$`\quad \xymatrix{
U \ar@[magenta][r]^{?} \ar@{|->}[d]
\ar@{}[dr]|{\text{lift}}
&V \ar@{|->}[d]
\\
A \ar@{=}[r]_{\mrm{id}}
&A
}\\
\quad \In \mbf{U}: \cat{D} \to \cat{T}
`$

部分型付け判断は次のようにも書けます。

$`\quad \xymatrix{
U \ar@[magenta][d]^{?}
\\
V \ar@{|->}[d]^{\text{lift}}
\\
A
}\\
\quad \In \mbf{U}: \cat{D} \to \cat{T}
`$

型付け判断の解図式を導出〈derivation〉と呼びます。以下は導出の例です。

$`\quad \xymatrix{
S \ar[r]^{\alpha} \ar@{|->}[d]
\ar@{}[dr]|{\text{lift}}
&T \ar@{|->}[d]
\\
A \ar[r]_f
&B
}\\
\quad \In \mbf{U}: \cat{D} \to \cat{T}
`$

解図式内の解セルは1つしかありません。解セル（上記の例なら1-射を表わす $`\alpha`$）を導出〈derivation〉と呼ぶこともあります。導出は曖昧語ですが、この曖昧性はそれほど問題にはならないでしょう。

部分型付け判断は、型付け判断の特別なものなので、その導出は同様に定義できます。次は、部分型付け判断の導出の例です。

$`\quad \xymatrix{
U \ar[d]^{\beta}
\\
V \ar@{|->}[d]^{\text{lift}}
\\
A
}\\
\quad \In \mbf{U}: \cat{D} \to \cat{T}
`$

この節で出現した用語はすべて、圏論的概念に別名を付けただけです。「型」、「詳細化」、「型付け判断」、「部分型」、「導出」といった言葉のなかには、既に知っている言葉があったかも知れません。そして、何か違和感を感じたかも知れません。しかし、用語の定義は、概念へのラベル付けの約束なので、どんなラベルを貼ろうと勝手なのです。とある圏論的概念に「型付け判断」というラベルを貼ったら、それはそう呼ぶだけのことです、約束なのだから。

ひょっとすると、圏論的概念が既に知っている言葉をうまく説明してくれるかも知れません。まったく何の関係もないかも知れません。頑張ったら関係付けることが出来るかも知れません。

テキスト化

前節で導入した圏論的概念を、型理論や論理の伝統的概念・用語・記法に翻訳するには、とりあえずはテキスト化する必要があります。左にテキスト、右にもとの図式を並べます。左のテキストと右の図式が対応します。前提している型詳細化システム（関手）$`\mbf{U}`$ は省略します。

$`\quad S\Over A
\quad \xymatrix{
S \ar@{|->}[d]
\\
A
}
`$

$`\quad S \underset{f}{\twoto} T
\quad \xymatrix{
S \ar@[magenta][r]^{?} \ar@{|->}[d]
\ar@{}[dr]|{\text{lift}}
&T \ar@{|->}[d]
\\
A \ar[r]_f
&B
}
`$

$`\quad U\le V
\quad \xymatrix{
U \ar@[magenta][d]^{?}
\\
V \ar@{|->}[d]^{\text{lift}}
\\
A
}
`$

$`\quad S \overset{\alpha}{\underset{f}{\twoto}} T
\quad \xymatrix{
S \ar[r]^{\alpha} \ar@{|->}[d]
\ar@{}[dr]|{\text{lift}}
&T \ar@{|->}[d]
\\
A \ar[r]_f
&B
}
`$

$`\quad U \overset{\beta}{\le} V
\quad \xymatrix{
U \ar[d]^{\beta}
\\
V \ar@{|->}[d]^{\text{lift}}
\\
A
}
`$

二重矢印記号（'$`\twoto`$'）は、圏の2-射を表わす矢印や論理の含意記号とコンフリクト〈競合 | 衝突〉しますが、致し方ないです。メリス／ジルバーガーが二重矢印記号を使っているので。

テキストは図式と同じことを表します。欠けている（暗黙化されている）情報は自分で補います。例えば $`S\Over A`$ を見たら次の情報をすぐに想起します。

  1. $`S\in |\cat{D}|`$ （$`S`$ は詳細型である）
  2. $`A\in |\cat{T}|`$ （$`A`$ は型である）
  3. $`\mbf{U}(S) = A`$ （$`S`$ は $`A`$ を詳細化する）

可解性命題

$`P`$ が問題図式だとして、$`P`$ が解を持つ（対応する解図式が存在する）ことを、$`\vdash P`$ と書きます。この場合のターンスタイル記号（'$`\vdash`$'）の使い方は、論理（の証明論）と同じです。

具体的に $`P`$ が与えられれば、$`\vdash P`$ は普通の命題として書き下すことができます。例えば、次の問題図式を考えてみましょう。

$`\quad \xymatrix{
{A} \ar[rr]^f \ar@[magenta][dr]_{?g}
&{} \ar@{}[d]|{?{\xi}\, \mag{\Downarrow}}
&{B}
\\
{}
&{?X} \ar@[magenta][ur]_{?h}
&{}
}\\
\quad \In\cat{C}
`$

$`\cat{C}`$ が1-圏だとすると、2-射は等式しかありません。可解性〈solvability〉の命題は、等式を成立させる射の存在を主張することになります。

$`\exists X\in |\cat{C}|.\\
\exists g\in \cat{C}(A, X).\\
\exists h\in \cat{C}(X, B).\\
\quad f = g; h
`$

問題図式 $`P`$ に対して、$`S`$ がその解図式であることを次のように書きましょう。

$`\quad \vdash P \text{ by }S`$

$`S`$ は、$`P`$ が可解〈solvable〉であることの証拠〈witness〉となります。可解であるとは、何かしらの解が在ることなので、次のような同値があります。

$`\quad \vdash P \Iff \exists S.\, \vdash P \text{ by }S`$

可解であることの否定は非可解〈unsolvable〉であり、次のように書きます。

$`\quad \not\vdash P \Iff \lnot \exists S.\, \vdash P \text{ by }S \Iff \forall S.\, \lnot (\vdash P \text{ by }S)`$

前節のテキスト化を使って、可解性命題を書いてみます。

$`\quad \vdash A \underset{f}{\twoto} B`$

これは、以下の問題図式の可解性を主張しています。

$`\quad \xymatrix{
S \ar@[magenta][r]^{?} \ar@{|->}[d]
\ar@{}[dr]|{\text{lift}}
&T \ar@{|->}[d]
\\
A \ar[r]_f
&B
}
`$

$`\alpha`$ が解1-セルである解図式があるなら、次が成立します。

$`\quad \vdash A \underset{f}{\twoto} B \text{ by } A \overset{\alpha}{\underset{f}{\twoto} } B`$

解の構成規則

型詳細化システム（単なる関手）に関して、次の条件付き可解性命題が成立します。

$`\quad (\vdash A \underset{f}{\twoto } B)\land (\vdash B \underset{g}{\twoto } C)
\Imp (\vdash A \underset{f;g}{\twoto } C)
`$

その根拠は、解1-セルを結合すれば、問題図式 $`A \underset{f;g}{\twoto } C`$ の解図式を作れるからです。幾つかの解図式から別の解図式を作り出す手順を解構成子〈solution constructor〉と呼びます。今の場合、次のような解図式を構成する構成子〈コンストラクタ〉が存在するのです。

$`\quad \xymatrix{
S \ar[r]_\alpha \ar@{|->}[d] \ar@/^1pc/[rr]^{\alpha; \beta}
&T \ar[r]_\beta\ar@{|->}[d]
&U \ar@{|->}[d]
\\
A \ar[r]^f \ar@/_1pc/[rr]_{f;g}
&B \ar[r]^g
&C
}\\
\quad \In \mbf{U}:\cat{D}\to\cat{T}
`$

この解の構成子を $`\mrm{Comp}`$ という名前で呼びます。既存の解図式達から、解の構成子 $`\mrm{Comp}`$ を使って新しい解図式を作り出す構成規則〈construction rule〉を次の形式で書きます。

$`\quad \vdash A \underset{f}{\twoto} B \text{ by } A \overset{\alpha}{\underset{f}{\twoto} }B \\
\quad \vdash B \underset{g}{\twoto} C \text{ by } B \overset{\beta}{\underset{g}{\twoto} }C \\
\VRule \mrm{Comp}\\
\quad \vdash A \underset{f;g}{\twoto} C \text{ by } A \overset{\alpha;\beta}{\underset{f;g}{\twoto} }C
`$

一般的な構成規則は次のフォーマットで書きます。

$`\quad \vdash P_1 \text{ by } S_1\\
\quad \cdots\\
\quad \vdash P_n \text{ by } S_n\\
\VRule \Phi\\
\quad \vdash Q \text{ by } \Phi(S_1, \cdots, S_n)
`$

「型理論と論理： 非形式シーケント記法 // 規則は命題ではないのだが」に書いたように、規則と命題は違います。規則は、既存のナニカから新しいナニカを作り出す“やり方”のレシピです。命題は、真偽判定可能なナニゴトかを主張しています。

しかし、「型理論や論理における命題と規則： 混同する事情」で説明したごとく、規則から自明に誘導される命題があります。それは次の命題です。

$`\quad \vdash P_1 \land\\
\quad \cdots \land\\
\quad \vdash P_n\\
\Imp \\
\quad \vdash Q
`$

構成規則と、規則から自明に誘導される命題は似た形をしています。これらは決まった形をしているので、省略をして短く書くことにします。

省略した規則：
$`\quad P_1\\
\quad \cdots\\
\quad P_n\\
\VRule \Phi\\
\quad Q
`$

解図式をすべて省略しています。「書かなくてもまー分かるでしょ」ということです。実際に、この程度の省略は使われるし、困ったことに「書いてないので分からない」こともしばしばあります。

省略した命題：
$`\quad P_1, \\
\quad \cdots,\\
\quad P_n\\
\vdash\\
\quad Q
`$

これは、「$`P_1, \cdots, P_n`$ がすべて可解ならば、$`Q`$ も可解である」と読めます。

型理論や論理は省略が大好きなようです。矢鱈に省略をされると、意味が分からなくなったり、混同・混乱が生じたりします。何がどう省略されたかをシッカリ追跡しましょう。

構成規則から導出ステップへ

問題図式の解の構成規則を横一行で書くときは次のフォーマットを使います。

$`\quad \Phi : P_1, \cdots, P_n \HRule Q`$

こう書くと、オペラッドのオペレーターのように見えます。$`P_1, \cdots, P_n, Q`$ が色で、$`\Phi`$ はオペレーターの名前です。

実際、問題図式（オペラッド用語の色）達の集合と解の構成子（オペラッド用語のオペレーター）達の集合があると、それらからオペラッドを作れます。オペラッドは、用語法（下）以外は導出系〈演繹系〉と同じものでした。

オペラッド 導出系
色 項 または 判断
生成オペレーター {導出}?ステップ
オペレーター {導出}?ツリー

メリス／ジルバーガーが既に「判断」「導出」という言葉を（問題図式と解図式の意味で）使っているので、導出系に関する用語は「項」と「ステップ」にします。

メリス／ジルバーガーの意味の判断を導出系の項（オペラッドの色）として、導出系のステップ（オペラッドの生成オペレーター）を定義しましょう。

ひとつは既に述べた $`\mrm{Comp}`$ によるステップです。次のように簡略に書けます。

$`\quad \mrm{Comp} : S\underset{f}{\twoto} T, T\underset{g}{\twoto} U\HRule
S\underset{f;g}{\twoto} U
`$

もうひとつ、圏の恒等射にあたる構成規則をステップとしておきます。

$`\quad \mrm{Id} : {}\HRule S\underset{id}{\twoto} S
`$

この構成規則の $`\HRule`$ の左は空っぽです。何の原料がなくても、恒等射を構成できます。

ステップ（実体は構成子による構成規則）に出現する $`S, T, U`$ は、型詳細化システム $`\mbf{U}:\cat{D}\to \cat{T}`$ の $`\cat{D}`$ のすべての対象達に渡って動かします。そして $`f, g`$ は、$`\cat{T}`$ のすべての射達に渡って動かします。そうすると、$`\mrm{Comp}_{S, T, U}`$ と $`\mrm{Id}_S`$ というインデックス付けられたステップの族〈indexed family of steps〉ができます。2つの族がステップの2つの種類に対応します。

ステップからオペラッド結合によりツリーが組み立てられます。ツリー達の集合に、圏の結合律と左右の単位律に相当する合同関係 $`\sim`$ を入れます。結合律に相当する合同関係の記述を、メリス／ジルバーガー論文からコピーすると以下のようです。

証明図の図法・レイアウトで描いていますが、言っていることは“圏の射の結合〈合成〉に関する結合律”です。

すべてのツリー達の集合を合同関係で割る（商集合を作る）と、目的の導出系（オペラッド）が出来上がります。

型詳細化システム（実体は単なる関手）の少数の導出（解図式のこと）を選んで、それらをステップとする導出系を構成することが出来ます。型詳細化システム（関手）の域圏や余域圏に構造（例えばモノイド構造）を入れて考えることも出来ます。型詳細化システム（関手）に条件（例えばファイブレーションであること）を課すことも出来ます。

コラリア／ディ-リベールティの判断的セオリーとの関係

メリス／ジルバーガーの論文 [MZ15] とコラリア／ディ-リベールティの論文 [CL21-24] は似た話題を扱っています。しかし、用語・記法はとんでもなく違っています。メリス／ジルバーガーの型詳細化システム（関手）を、コラリア／ディ-リベールティは判断（あるいは判断分類子）と呼んでいます。「判断」「規則」「導出」などが何を意味するかは、もはやカオス状態で、著者ごと・著作ごと・文脈ごとに確認するしかないです。

メリス／ジルバーガーもコラリア／ディ-リベールティも、関手に注目してなにかをしてます。注目すべき関手を、ポール・テイラー〈Paul Taylor〉に倣ってディスプレイ関手（ディスプレイ写像の関手版）と呼ぶことにします。メリス／ジルバーガーは、ディスプレイ関手（型詳細化システム）をひとつだけ固定して議論しています。それに対して、コラリア／ディ-リベールティはたくさんのディスプレイ関手（判断分類子）達を同時に考えて、ディスプレイ関手以外の関手や自然変換までも一緒に考えようとしています。

ディスプレイ関手達、ディスプレイ関手以外の関手達や自然変換達が構成するマクロな構造がコラリア／ディ-リベールティの判断的セオリー〈judgemental theory〉（「判断的セオリーと判断計算」参照）です。特に、ひとつのディスプレイ関手だけから構成される判断的セオリーを考えれば、それはメリス／ジルバーガーのセッティングになります。

いずれの場合でも、判断計算の判断形式〈judgement form〉は、関手ターゲットの問題図式です。問題図式の解の構成規則が導出系のステップになります。判断計算は、判断的セオリーから構成された導出系だと捉えられます。言い方を変えれば、判断計算という形式体系のモデルが判断的セオリーです。

コラリア／ディ-リベールティの判断的セオリーとメリス／ジルバーガーの型詳細化システムを一緒に使いたいなら、分野固有のテキスト化を避けることが肝要だと思います。出来るだけ圏論標準の図式を使って一律に記述するのが望ましい、ということです。そうしないと、記法の管理で疲弊してしまいます。

そしてそれから

[MZ13B-] Type refinement and monoidal closed bifibrations には、注目している圏・関手がモノイド構造やファイバー付き構造を持つ場合が書いてあるようです。構造が載った圏達・関手達の判断的セオリーを考えることになります。ハイパードクトリンの場合などを考えると、ファイバーごとにモノイド構造／モノイド閉構造／デカルト閉構造などを持つファイブレーションが重要そうです。

ファイブレーションに注目するということであれば、包括圏やコンテキスタッドとも関連がでてきそうです。コンテキスタッドをホストする環境であるパラダイス（と呼ばれる2-圏）は、判断的セオリーもホストするのではないか？ と妄想が拡がります。

*1:メリス／ジルバーガーは、'e' を書かない "judgment" を使ってます。