判断的セオリーと判断計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)

前回の記事「判断形式を普通に書く」で、コラリア／ディ-リベールティの次の論文を参照しました。

[CL21-24]
Title: Context, Judgement, Deduction
Authors: Greta Coraglia, Ivan Di Liberti
Submitted: 17 Nov 2021 (v1), 1 Nov 2024 (v3)
Pages: 61p
URL: http://arxiv.org/abs/2111.09438

この論文は、圏論的構造である判断的セオリー〈judgemental theory〉と、形式体系である判断計算〈judgement calculus〉を定義して、その理論と応用を述べています。

コラリア／ディ-リベールティ論文の主題である判断的セオリーと判断計算について簡単に紹介します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\twoto}{\Rightarrow }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in }}
\newcommand{\On}{\text{ on }}
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{ \text{－} }
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\Rule}{\rightrightarrows}
`$

内容：

判断的セオリー
ベースと判断
呼び名の問題
判断関手と判断形式
おわりに

判断的セオリー

判断的セオリーは、2-圏に近い圏類似構造〈category-like structure〉です。0-射、1-射、2-射から構成されます。0-射達と1-射達で圏〈1-圏〉が構成されますが、これはちゃんとした圏であり、タチの良い圏です。しかし、2-射達を含めても2-圏にはなりません。判断的セオリーの用途から言って、2-圏でなくてもかまわないのです。

判断的セオリーの0-射は圏であり、1-射は関手で、2-射は自然変換です。つまり、小さいとは限らない圏達の2-圏 $`\mbf{CAT}`$ の部分2-圏もどきが判断的セオリーです。

判断的セオリー〈judgemental theory〉を、筆記体〈スクリプト体〉大文字の $`\msc{A}, \msc{B}`$ などで書くことにします。一般にn-圏 $`\cat{K}`$ の$`i`$-射達の集合を $`|\cat{K}|_i`$ と書きます。判断的セオリー $`\msc{A}`$ に対しても同じ記法を使います。すると：

$`\quad |\msc{A}|_0 \subseteq |\mbf{CAT}|_0`$
$`\quad |\msc{A}|_1 \subseteq |\mbf{CAT}|_1`$
$`\quad |\msc{A}|_2 \subseteq |\mbf{CAT}|_2`$

$`|\msc{A}|_0, |\msc{A}|_1`$ は、$`\mbf{CAT}`$ から誘導される圏構造により圏〈1-圏〉になります。これを $`\msc{A}_{\le 1}`$ と書くことにします。$`\msc{A}_{\le 1}`$ は、圏達を対象とする圏です。単なる圏ではなくて、有限完備圏です。つまり、終対象があるし、直積も自由に作れるし、イコライザーもプルバック四角形も自由に作れます。

判断的セオリーの2-射は自然変換ですが、特殊な形の自然変換だけを許します。関手〈1-射〉$`F, G, H`$ は $`\msc{A}_{\le 1}`$ に属するものだとして、次の形の $`\alpha, \beta`$ です。

$`\quad \xymatrix{
{}
&{\cdot} \ar[dr]^G
\ar@{}[d]|{\alpha \Downarrow}
&{}
\\
{\cdot} \ar[ur]^F \ar[rr]_H
&{}
&{\cdot}
}\\
\quad \In \mbf{CAT}
`$

$`\quad \xymatrix{
{}
&{\cdot} \ar[dr]^G
\ar@{}[d]|{\beta \Uparrow}
&{}
\\
{\cdot} \ar[ur]^F \ar[rr]_H
&{}
&{\cdot}
}\\
\quad \In \mbf{CAT}
`$

テキストで書くときは次のようにしましょう。

$`\quad \alpha :: (F, G)\twoto H \In \msc{A}`$
$`\quad \beta :: H \twoto (F, G) \In \msc{A}`$

コラリア／ディ-リベールティは、$`\alpha`$ の形を反変〈contravariant〉、$`\beta`$ の形を共変〈 covariant〉と呼んでいます。要は二種類あるというだけです。どちらを共変（あるいは反変）と呼ぶかは、コイントスで決めるようなものなので気にしてもしょうがないです。根拠のない呼び名は憶えにくいですが、忘れても別にかまいません。

判断的セオリー $`\msc{A}`$ は、2-射〈自然変換〉と1-射〈関手〉のヒゲ結合〈whiskering〉に対して閉じていますが、2-射どうしの縦結合や横結合は定義されていません。よって、2-圏とは言えないのです。

2-射〈自然変換〉と1-射〈関手〉の組み合わせからの構成として、ヒゲ結合以外にシャープ持ち上げ〈sharp lifting | #-lifting〉があります。聞いたことがない構成ですが、実際、前例はないようです。

Remark 1.0.13. We could not find any precise instance of #-liftings in the literature, our construction seems original.
備考 1.0.13. 既存の文献の中では、シャープ持ち上げの事例を見つけることができませんでした。我々の構成は独自のものであるようです。

これ以上シャープ持ち上げには踏み込みませんが、判断的セオリーはちょっと珍しい構成を持っているわけです。

判断的セオリーの定義はまだ終わってません。続きは節を改めます。

ベースと判断

判断的セオリー $`\msc{A}`$ には、2-圏もどきの構造以外に、特別な0-射（圏）と1-射（関手）達が指定されています。$`|\msc{A} |_0`$ のなかの特別な要素〈0-射 | 対象〉がただひとつ特定されていて、それをベース〈base〉と呼びます。$`|\msc{A} |_1`$ のなかの特別な要素〈1-射 | 射〉達が特定されていて、それらを判断〈judgement〉と呼びます。

判断的セオリー $`\msc{A}`$ のベースを $`\mrm{Base}_\msc{A}`$ 、判断達の集合を $`\mrm{Judge}(\msc{A})`$ と書くことにします。

$`\quad \mrm{Base}_{\msc{A}} \in |\msc{A}|_0`$
$`\quad \mrm{Judge}(\msc{A}) \subseteq |\msc{A}|_1`$

次の条件は（判断的セオリーの公理として）要求します。

$`\quad F \in \mrm{Judge}(\msc{A}) \Imp \mrm{cod}(F) = \mrm{Base}_\msc{A}
`$

つまり、判断の余域は必ずベース（特定されている圏）です。

他に次のような条件が考えられます。

判断はファイブレーション（の射影）でなくてはならない。
$`\forall \cat{C}\in |\msc{A}|_0.\exists F\in \mrm{Judge}(\msc{A}).\, \mrm{dom}(F) = \cat{C}`$
$`\forall F, G\in \mrm{Judge}(\msc{A}).\, \mrm{dom}(F) = \mrm{dom}(G) \Imp F = G`$
$`\forall F\in |\msc{A}|_1.\, \mrm{dom}(F) = \mrm{Base}_\msc{A} \Imp F \in \mrm{Judge}(\msc{A})`$

2番目の条件は、判断的セオリーの任意の0-射から出る判断があることです。3番目の条件は、判断的セオリーの任意の0-射から出る判断はたかだか1つ〈無いか、ただ1つ〉であることです。4番目の条件は、余域がベースである1-射は判断に限る（判断以外の1-射の余域はベースではない）ことです。

コラリア／ディ-リベールティは、2番目と4番目を仮定しているようです。が、4番目は邪魔になるときがあります。例えば、コンテキスタッド（「型理論とコンテキスタッド：コンテキストフル射」参照）と判断的セオリーを一緒に考えるときは4番目は邪魔です。1番目の条件が必要になる場合（たぶん多くの場合）もあるでしょう。

とりあえずここでは、2番目の条件だけを要求して、他の条件は必要に応じて追加することにします。

判断的セオリー $`\msc{A}`$ の構成素をまとめると：

$`\mbf{CAT}`$ の部分1-圏（部分2-圏ではない） $`\msc{A}_{\le 1}`$
2-射（実体は自然変換）達の集合 $`\msc{A}_2`$
特定された0-射 $`\mrm{Base}_{\msc{A}} \in |\msc{A}|_0`$
1-射達の集合 $`\mrm{Judge}(\msc{A}) \subseteq |\msc{A}|_1`$

$`\msc{A}_{\le 1}`$ は有限完備圏で、$`\msc{A}_2`$ は幾つかの構成に関して閉じていて、$`\mrm{Base}_{\msc{A}}`$ と $`\mrm{Judge}(\msc{A})`$ はこの節で述べた条件を満たします。

呼び名の問題

コラリア／ディ-リベールティは、判断的セオリーのベースをコンテキスト達の圏〈category of contexts〉と呼んでいます。この呼び名は、型理論での呼び名を借用しています。判断的セオリーは型理論以外でも使えそうなので、一般論ではベースと呼んでおいて、個別な具体例ではそれぞれに相応しい呼び名にするのが良いかと思います。型理論ならもちろん「コンテキスト達の圏」が相応しいでしょう。

“圏達の圏”を扱うときはいつでも生じる問題なのですが、「対象」や「射」が何を表わすかよく分からなくなります。例えば、ベースは圏 $`\msc{A}_{\le 1}`$ の対象なので、「ベースと呼ばれる対象」だから「ベース対象」と呼んでよさそうです。一方で、ベースの実体は圏なので「ベース圏」と呼んでもいいでしょう。ベース圏の対象は「ベース対象」と ‥‥ あれれ、ダメだ。こういうことがしょっちゅう起きて、こんがらかるのです。

判断的セオリーの0-射、1-射、2-射には、それと分かる呼び名を与えておいたほうがよさそうです。コラリア／ディ-リベールティは、次のような方針を採用しています。

$`|\msc{A}|_0`$ の要素（0-射、実体は圏）を判断と呼ぶ。
$`\mrm{Judge}(\msc{A})`$ の要素（特別な1-射、実体は関手）も判断と呼ぶ。
1-射（関手）であることを強調したいときは、判断分類子〈judgment classifier〉と呼ぶ。
判断分類子（単に「分類子」とも呼ぶ）の域のことも（分類子の）判断と呼ぶ。

「判断」が0-射（圏）なのか、1-射（関手）なのかはあえて曖昧にする、ということです。

We will often blur the distinction between the classifier and its judgement.
我々はしばしば、分類子とその判断の区別を[意図的に]曖昧にします。

これに限らず、用語・記法は意図的に曖昧にする方針で、それが論文を難読にしています。僕は曖昧さ解決にエネルギーを使いたくないので、「判断」の意味は曖昧性なく一意的に決めます。

$`\mrm{Judge}(\msc{A})`$ の要素（特別な1-射、実体は関手）だけを判断と呼ぶ。

となると、$`|\msc{A}|_0`$ の要素（0-射、実体は圏）の呼び名が別に必要です。論文内では使ってませんが、コラリアのトーク動画のなか（下例えば1分50秒くらい）では、0-射を「カインド」と呼んでいました。

https://www.youtube.com/watch?v=lfm8HH5gLyU (2022/01/15)

というわけで、$`|\msc{A}|`$ の要素（0-射、実体は圏）をカインドと呼びましょう。型理論では、カインドの対象は型項やインスタンス項です。論理では、カインドの対象は論理式です。

コラリア／ディ-リベールティによれば、判断に限らない $`|\msc{A}|_1`$ の要素は「規則〈rule〉」で、$`|\msc{A}|_2`$ の要素は「ポリシー〈policy〉」です。困ったことに、この意味の規則（1-射）は判断計算の規則に対応しません。むしろ、ポリシーが判断計算の規則に対応します。このへんも、規則とポリシーを意図的に曖昧にして、ポリシーのことも規則と呼ぶような曖昧用法を使ってます。これもけっこうシンドイ。

コラリア／ディ-リベールティの意味の規則の具体例は、型理論ならインスタンス項への型割り当て、論理なら限量子です（あくまで一例ですが）。つまり、判断計算の判断形式〈judgement form〉のなかで使う（広い意味の）演算記号に相当する圏論的実体を「規則」と呼んでいることになります*1。判断計算の規則形式〈rule form〉とはズレています（ズレの解消は曖昧用法で行うお約束）。

ここでは、$`|\msc{A}|_1`$ の要素は演算記号に対応する実体だから演算〈operator〉にします -- 曖昧用法はカンベンして欲しいので。

曖昧性を少なくした用語は次のようです。

コラリア／ディ-リベールティ	この記事
判断(1)	カインド
判断(2)	判断
規則(1)	演算
規則(2)＝ポリシー	ポリシー

判断関手と判断形式

「判断形式を普通に書く」から引用すると：

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

個人的な感覚と価値観では、「記号の乱用、短縮記法、完全な省略」のワザを使いまくるのが良いことだとは思えないんだよな－。もちろん、記述と計算が迅速になるメリットは承知しています。が、そういう速記術、計算術は別にしてくれないかなー、と。

判断計算〈judgement calculus〉は、判断的セオリーという圏類似構造に対応する形式的計算系〈formal calculus〉です。言い方を換えると、判断的セオリーは判断計算の圏論的モデルです。ただし、モデルは構文論的意味論（「型理論周辺、何で混乱するのか？ // 構文論的意味論と意味論的意味論」参照）のモデルなので、構文構造を表わす圏類似構造です。

モデル側の概念である「判断」と、形式的計算系に関わる概念である「判断」も区別しないで曖昧に語ることは、ある意味普通ですが、区別したいときは、モデル側なら「判断関手」、計算系側なら「判断形式」とします。判断的セオリーの判断関手を、判断計算の判断形式によって書き記すことになります。

以下のような判断関手があったとします。

$`\quad F : \cat{C} \to \mrm{Base}_\msc{A} \In \mrm{Judge}(\msc{A})`$

このとき、判断計算側では、次のパターンの判断形式が使えます。

$`\text{For }X\in |\mrm{Base}_\msc{A}|\\
\quad X \mid_F \cdots
`$

判断形式の詳細と事例は「判断形式を普通に書く」を見てください。

型理論の場合ならば、ベースは（型理論の意味での）コンテキスト達の圏 $`\mbf{Ctx}`$ とします。習慣に従い、圏 $`\mrm{Ctx}`$ の対象はギリシャ文字大文字で書きます。すると、判断形式のフォーマットは次のようです。

$`\text{For }\Gamma \in |\mbf{Ctx}|\\
\quad \Gamma \mid_\pi \cdots
`$

判断関手 $`\pi`$ は、型項にそのコンテキストを対応させる射影だとしましょう。

$`\quad \pi : \mbf{Type} \to \mbf{Ctx}`$

型項 $`A`$ がコンテキスト $`\Gamma`$ に対して整形式〈well-formed〉であることを表わす判断形式は次のようになります。

$`\text{For }\Gamma \in |\mbf{Ctx}|\\
\quad \Gamma \mid_\pi A \In \mbf{Type}
`$

論理の場合ならば、ベースの対象は、論域〈domain of discourse〉に対応する型付き変数達の集合です。ベースの射は、変数のあいだを結ぶ式（代入〈substitution〉と呼ばれることがある）のインデックス付き集合（これも代入〈substitution〉と呼ばれることがある）です。ベースを、型理論のときと同じく（名前をオーバーロードして） $`\mbf{Ctx}`$ とします。判断形式のフォーマットは次のようです。

$`\text{For }\Gamma \in |\mbf{Ctx}|\\
\quad \Gamma \mid_\pi \cdots
`$

判断関手 $`\pi`$ は、論理式にコンテキスト（型付き変数達の集合）を割り当てる関手だとします。

$`\quad \pi : \mbf{Formula} \to \mbf{Ctx}`$

ただし、コンテキスト $`\Gamma`$ に含まれる変数名〈ラベル〉達を $`\mrm{Var}(\Gamma)`$ 、論理式 $`A`$ に現れる変数名達を $`\mrm{Var}(A)`$ としたとき：

$`\quad \mrm{Var}(A) \subseteq \mrm{Var}(\pi(A))`$

論理式 $`A`$ がコンテキスト $`\Gamma`$ に対して整形式（色々な構文的整合性を満たす）であることを表わす判断形式は次のようになります。

$`\text{For }\Gamma \in |\mbf{Ctx}|\\
\quad \Gamma \mid_\pi A \In \mbf{Formula}
`$

“型理論の型項”と“論理の論理式”の扱い方が同じになることは、Propositions-as-Types / Types-as-Propositions というキャッチフレーズのひとつの表現になっています。

おわりに

形式的計算系の構文論的モデルとして圏類似構造を使うことは、有効で面白い方法だと思います。その意味で、コラリア／ディ-リベールティの判断的セオリー／判断計算も有効で面白そうです。が、「用語・記法は意図的に曖昧にする」とか「記号の乱用、短縮記法、完全な省略のワザを駆使する」とか、悪しき伝統にこだわるのはいかがなものか？とは思います。概念の記述・定義・説明には、できるだけ普通の書き方・言い回しを使い、それとは別に速記術・計算術を導入する、という方策だと、だいぶアクセスしやすくなるでしょう。

*1:[追記]論理の場合、論理演算子〈結合子〉ごとに推論規則があります（論理演算子と無関係な規則もありますが）。これを参考に、「演算が規則をパラメトライズするから、演算を規則と呼ぶ」ということらしいです。たぶん。[/追記]