コンテキスト、判断、指標、シーケントなどのゴチャゴチャを整理

圏論、型理論（型付きラムダ計算含む）、論理は、カリー／ハワード／ランベック対応により、同種の構造（例えばデカルト閉圏）を扱っていると理解することが出来ます。しかし、用語法・記法はバラバラです。このバラバラさゆえに、対応関係を捉えられなかったり、混乱したりする人もいそうです。整理しておきましょう。$`\newcommand{\cat}[1]{ \mathcal{#1}}
\newcommand{\mrm}[1]{ \mathrm{#1}}
\newcommand{\In}{ \text{ in }}
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\Iff}{\Leftrightarrow}
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
%`$

内容：

圏論、型理論、論理
圏、複圏、多圏
方言対応表
圏／複圏／多圏の可達性述語
指標の理論や依存型理論の場合

圏論、型理論、論理

圏論、型理論、論理は「似てるな」という印象を持ちますが、それは印象だけではなくて、キチンと対応付けることが出来ます。多少乱暴ではありますが、「表層が違うだけで内容的には同じ」と言っていいでしょう。

「内容的には同じ」であっても、異なる分野なので、異なる用語法・記法を持ちます。それは、地方ごとに方言があるのと似た状況です。「郷に入っては郷に従え」なので、特定の分野について語るときはその分野の用語法・記法を使うのが望ましいでしょう。

しかし、方言の違いを内容的な違いと誤認するのは困ったことだし、方言の違いを超えた共通概念を認識するのは知的節約術になります。

以下では、圏論、型理論、論理の方言（それぞれの用語法・記法）を比較・整理します。

圏、複圏、多圏

型理論や論理では、通常の圏〈ordinary category〉だけではなく、複圏〈オペラッド〉、多圏をよく使います。複圏／多圏については次の記事にまとめてあります。

述語論理：様々な多圏達の分類整理

通常の圏の対象と射を、“通常”であることを強調して、ここでは単純対象〈simple object〉、単純射〈simple morphism〉とも呼びます。

複圏／多圏では、単純対象のリスト $`(A_1, \cdots, A_n)`$ を対象として使います。リストの項目に名前を付けた名前付きリスト〈レコード〉 $`(a_1:A_1, \cdots, a_n:A_n)`$ などを使うときもあるので、一般的状況でも使える単純対象のコレクション〈collection of simple objects〉という呼び名を採用しましょう*1。

圏／複圏／多圏とその構成素は次のようにまとめられます（整理されてない現実の呼び名は「述語論理：様々な多圏達の分類整理」参照）。

圏	対象〈単純対象〉	域：単純対象	余域：単純対象	射〈単純射〉
複圏	複対象と単純対象	域：複対象	余域：単純対象	複射
多圏	多対象	域：多対象	余域：多対象	多射

複対象と多対象は（実体としては）どちらも単純対象のコレクションです。

射〈単純射〉／複射／多射の域と余域の情報をプロファイル〈profile〉と呼びます。コレクションとしてリストを使う場合のプロファイルは次のように書きます。

射のプロファイル： $`A \to B`$
複射のプロファイル： $`(A_1, \cdots, A_n) \to B`$
多射のプロファイル： $`(A_1, \cdots, A_n) \to (B_1, \cdots, B_m)`$

リストの囲み括弧はしばしば省略されます。

複射のプロファイル： $`A_1, \cdots, A_n \to B`$
多射のプロファイル： $`A_1, \cdots, A_n \to B_1, \cdots, B_m`$

括弧を省略すると、空リストのある場所には何も書かないことになります。

域が空リストの複射のプロファイル： $`\to B`$
余域が空リストの多射のプロファイル： $`A_1, \cdots, A_n \to`$

これは紛らわしいので僕は使いません（世間では使っています）。

通常の圏と同様に、複圏／多圏のホムセット（複ホムセット〈multi-homset〉と多ホムセット〈poly-homset〉）があり、次のように書きます。$`\cat{C},\cat{M},\cat{P}`$ はそれぞれ、圏, 複圏, 多圏です。

$`\quad f\in \cat{C}(A , B)\iff f:A \to B \In \cat{C}\\
\quad m\in \cat{M}( (A_1, \cdots, A_n) , B) \iff m:(A_1, \cdots, A_n) \to B \In \cat{M}\\
\quad p\in \cat{P}( (A_1, \cdots, A_n) , (B_1, \cdots, B_m) ) \iff \\
\qquad p:(A_1, \cdots, A_n) \to (B_1, \cdots, B_m) \In \cat{P}
%`$

方言対応表

方言（各分野の用語法）の対応（カリー／ハワード／ランベック対応）は基本的に次の表で与えられます。

圏論	単純対象	単純対象のコレクション	単純射／複射／多射	プロファイル
型理論	型	型コンテキスト	項	型判断
論理	命題	命題コレクション	証明	シーケント

幾つかの注意事項を以下に述べます。

型理論の文脈では、型コンテキスト／型判断を単にコンテキスト〈context〉／判断〈judgment〉と略称します。用語「判断」は論理でも使うことがあります。

型判断／シーケントは、単なるプロファイルとはちょっと違った意味合いで使われることがあります。それについては次節で述べます。

プロファイル記述に使う矢印記号は、$`\to`$ 以外に $`\vdash,\, \Rightarrow`$ も使います。使い分けは習慣と趣味の問題です。また、プロファイルとしての型判断は、圏論のプロファイルと違った書き方をします。

$`\quad \text{圏論風記法 } m:(A_1, \cdots, A_n) \to B \\
\quad \text{型理論風記法 } (A_1, \cdots, A_n) \vdash m:B
`$

古典論理のシーケント〈LKシーケント〉の場合、矢印の左側と右側では解釈が異なります。このことを明示するために、命題のリストの左肩にマーカーを付けてみましょう。

$`\quad p: {^\land (A_1, \cdots, A_n)} \to {^\lor (B_1, \cdots, B_m) }`$

あるいは、区切り記号を変えて：

$`\quad p: (A_1, \cdots, A_n) \to (B_1\mid \cdots\mid B_m)`$

しかし、実際のシーケントではこのような区別はされずに、分かりにくくなっています。古典論理のシーケント（より一般に、矢印の左右で解釈が変わるシーケント）は話がややこしいので、使わないで済むなら使わないほうが吉です。

圏／複圏／多圏の可達性述語

$`\cat{C}`$ を圏として、2つの対象を引数とする述語 $`\mrm{Reachable}_\cat{C}(-, -)`$ を次のように定義します。

$`\For A, B \in |\cat{C}|\\
\quad \mrm{Reachable}_\cat{C}(A, B) :\Iff \cat{C}(A, B) \ne \emptyset
`$

ホムセットが空でないことを、言い方を変えれば：

$`\For A, B \in |\cat{C}|\\
\quad \mrm{Reachable}_\cat{C}(A, B) :\Iff
\exists f \in \mrm{Mor}(\cat{C}).( \mrm{dom}(f) = A \land \mrm{cod}(f) = B)
`$

二項述語 $`\mrm{Reachable}_\cat{C}`$ を、圏 $`\cat{C}`$ の可達性述語〈reachability predicate〉と呼びます。

特に、$`G`$ が有向グラフで、有向グラフから作った自由圏を $`\mrm{FreeCat}(G)`$ とするとき、圏 $`\mrm{FreeCat}(G)`$ の可達性は、有向グラフ $`G`$ におけるパス可達性です。

複圏／多圏に対しても、ホムセットが空でないことによって可達性を定義できます。複圏／多圏の単純対象の集合を $`\mrm{Obj}(-)`$ として、コレクションとしてリストを使う場合に、可達性を記述しましょう。以下、$`\cat{M}`$ は複圏、$`\cat{P}`$ は多圏とします。

$`\For A_1,\cdots,A_n, B \in \mrm{Obj}(\cat{M})\\
\quad \mrm{Reachable}_\cat{M}( (A_1, \cdots, A_n), B) :\Iff \cat{M}( (A_1, \cdots, A_n), B) \ne \emptyset
`$

$`\For A_1,\cdots,A_n, B_1, \cdots, B_m \in \mrm{Obj}(\cat{P})\\
\quad \mrm{Reachable}_\cat{P}( (A_1, \cdots, A_n), (B_1, \cdots, B_m ) ) :\Iff\\
\qquad \cat{P}( (A_1, \cdots, A_n), (B_1, \cdots, B_m )) \ne \emptyset
`$

$`\cat{X}`$ は圏または複圏または多圏だとして、可達性 $`\mrm{Reachable}_\cat{X}(-, -)`$ を中置関係記号 $`\vdash_\cat{X}`$ を使って表すことにします。例えば複圏の場合なら：

$`\quad (A_1, \cdots, A_n) \vdash_\cat{M} B \iff \mrm{Reachable}_\cat{M}( (A_1, \cdots, A_n) , B)`$

今話題にしている圏／複圏／多圏 $`\cat{X}`$ が明らかなら、$`\vdash_\cat{X}`$ の下付き $`\cat{X}`$ は省略して単に $`\vdash`$ と書きます。

結局、記号 $`\vdash`$（ターンスタイル記号）はプロファイル矢印以外に可達性述語記号（中置関係記号）としても使われます。可達性述語記号を使った命題は、型理論／論理のメタ命題になります。

型理論の場合、可達性は、特定の型を持つ項 $`t`$ の存在を主張します。

$`\quad (A_1, \cdots, A_n) \vdash B\\
\iff \exists t .\, (A_1, \cdots, A_n) \vdash t: B
`$

上記の上段の $`\vdash`$ は可達性述語記号で、下段の $`\vdash`$ はプロファイル矢印です。記号のオーバーロードが分かりにくい理由ですから、分かりやすく書くなら：

$`\quad \mrm{Reachable}_{\cat{M}} ( (A_1, \cdots, A_n), B)\\
\iff \exists t .\, t: (A_1, \cdots, A_n) \to B \In \cat{M}
`$

上段のメタ命題〈判断〉に対して、項 $`t`$ が証拠〈witness〉となります。

論理の場合、可達性は、命題の証明可能性〈provability〉を主張します。

$`\quad (A_1, \cdots, A_n) \vdash B\\
\iff \exists p .\, p : (A_1, \cdots, A_n) \to B \In \cat{M}
`$

上段のメタ命題〈証明可能性判断〉に対して、実際の証明 $`p`$ が証拠となります。

「判断」という言葉が、メタ命題／メタ述語記号の意味と、証拠のプロファイル／プロファイル矢印記号の意味でオーバーロードされています。強く関連しているからオーバーロードされているのですが、いったんは区別して理解しないと混乱するでしょう。

指標の理論や依存型理論の場合

[追記]あっ、タイトルに「指標」を入れていたのに、「指標」に触れてなかった。書き足します。[/追記]

以下は、「型クラス述語とイプシロン型」で事例に使ったモノイドの指標です。

// モノイドの指標
signature Monoid {
  sort U
  operation m : U×U → U
  operation e : 1 → U
laws:
  ∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
  ∀x∈U. m(e(), x) = x
  ∀x∈U. m(x, e()) = x
}

指標を、改行の代わりにカンマで区切ったリストとして表してみます。キーワードは省略します。

// モノイドの指標
signature Monoid := (U, m : U×U → U, e : 1 → U,
  ∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z)),
  ∀x∈U. m(e(), x) = x,
  ∀x∈U. m(x, e()) = x)

改行もありますが、区切りの意味はなくて、単にレイアウト調整の改行です。

指標を表すリストは、項目（成分、要素）の種類がバラバラで、出現する項目が前の（左の）項目に依存します。従って、項目を自由に並べ替えることはできません。

型理論の型コンテキストも、項目を自由に並べ替えられないことがあります。項目のあいだに、右のものが左側に依存する依存性がある場合です。

項目の順序交換ができない（対称性を持たない）コレクションを使っても、複圏／多圏を定義できます。指標の理論や依存型理論では、そのような非対称な複圏／多圏を使うことがあります*2
。

豆知識ですが、「項目の順序交換ができない、項目のあいだに依存性があるコレクション」をテレスコープ〈telescope〉と呼ぶことがあります。

https://www.pls-lab.org/en/telescope
https://ncatlab.org/nlab/show/type+telescope
https://www.win.tue.nl/automath/archive/pdf/aut103.pdf ド・ブラウン〈N.G. de Bruijn〉の "Telescopic mappings in typed lambda calculus" 、おそらくテレスコープの起源
https://leanprover.github.io/reference/declarations.html#contexts-and-telescopes Leanにおけるテレスコープ

テレスコープ、指標、コンテキストは（内容的には）同義語です。

*1:$`\cat{C}`$ がデカルト閉圏で、$`\cat{C}`$ のなかでは“複雑な”対象、例えば $`A\times[ B\times C, C]`$ も、通常の圏の対象なので単純対象です。

*2:「述語論理：様々な多圏達の分類整理」の分類で「対称 vs. 非対称」という基準を出しましたが、項目の順序交換できない場合が非対称です。