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

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

カートメル／ヴォエヴォドスキー／パルムグレンの型理論

雑記／備忘

型理論／型システムは何十種類、いや何百種類もあるのですが、そのなかで、「今のイチ推しは何ですか？」と聞かれれば、カートメル／ヴォエヴォドスキー／パルムグレンの型理論を挙げます。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
`$

内容：

カートメル、ヴォエヴォドスキー、パルムグレン

カートメル〈John Cartmell〉は、彼の学位論文と関連する論文のなかで、属性付き圏〈category with attributes | CwA〉、コンテキスト圏〈contextual category〉、一般化代数理論〈generalized algebraic theory〉などの新しい概念を型理論に導入しました。

カートメルの学位論文は、タイプライターと手書きの紙をスキャンしたデータとして公開されています。

これはちょっと読みにくい。後になって"Annals of Pure and Applied Logic"に掲載された要約のほうが（これもスキャンデータですが）読みやすいです。

ヴォエヴォドスキー〈Vladimir Voevodsky〉は、型理論の厳密な定式化の基礎としてカートメルのコンテキスト圏を採用しました。ただし、C-システム〈C-system〉と名前を変えています。ヴォエヴォドスキーは、「コンテキスト圏は圏とは言えない」と考えていたようです。そのことは「パチモンの圏 ＝ システム」に書いています。

C-システムに関するヴォエヴォドスキーの論文を幾つか挙げると：

  • [Voe14-16]
  • Title: Subsystems and regular quotients of C-systems
  • Author: Vladimir Voevodsky
  • Submitted: 28 Jun 2014 (v1), 15 Mar 2016 (v3)
  • Pages: 12p
  • URL: https://arxiv.org/abs/1406.7413

  • [Voe14-15]
  • Title: A C-system defined by a universe category
  • Author: Vladimir Voevodsky
  • Submitted: 28 Sep 2014 (v1), 29 Jul 2015 (v3)
  • Pages: 33p
  • URL: https://arxiv.org/abs/1409.7925

  • [Voe16-]
  • Title: C-system of a module over a Jf-relative monad
  • Author: Vladimir Voevodsky
  • Submitted: 1 Feb 2016
  • Pages: 32p
  • URL: https://arxiv.org/abs/1602.00352

ヴォエヴォドスキーがC-システムを探求していたときと同時期にパルムグレン〈Erik Palmgren〉は次の論文を発表しています。

ヴォエヴォドスキーとパルムグレンは、お互いに参照がまったくないので、同じ時期の独立した仕事でしょう。が、ヴォエヴォドスキーの抽象的な定式化を、パルムグレンが具体的に解説しているかのごとき内容になっています。このことは「ヴォエヴォドスキーの宇宙圏とパルムグレンの複前層」に書いています。

カートメル、ヴォエヴォドスキー、パルムグレンの系譜に属する型理論をカートメル／ヴォエヴォドスキー／パルムグレンの型理論〈Cartmell-Voevodsky-Palmgren type theory〉と呼ぶことにします。

型とは何なのか？

型理論は何百種類もあるので、「型」をどう捉えるかで大雑把に分類します。この分類を、 ◯◯◯s-as-Types とか Types-as-◯◯◯s とかのキャッチフレーズで表します。以下は「集合論・圏論 vs. 型理論」からの再掲です。

  • Sets-as-Types（集合が型だ）
  • Algebras-as-Types（代数が型だ）
  • Coalgebras-as-Types（余代数が型だ）
  • Propositions-as-Types（命題が型だ）
  • Categories-as-Types（圏が型だ）
  • Logical Relations-as-Types（論理関係が型だ）*1
  • ‥‥

Propositions-as-Types（命題が型だ）は有名なキャッチフレーズですが、「命題」が曖昧多義語なので（「Propositions-As-Typesを曲解しないで理解するために // 「命題」を排除したい！」参照）意味不明です。もう少し分かりやすく言い直すなら：

  • Formulae-as-TypeTerms（論理式が型項だ）

論理で使う論理式を型項（型を表す記号表現）だと解釈しよう、ということです。この立場により、真偽値や述語も型理論のなかで議論できるようになります（「「命題」の曖昧性から前層意味論へ」参照）。

もう少し ◯◯◯s-as-Types の例を挙げましょう。

  • Objects-as-Types（対象が型だ）
  • Families-as-Types（ファミリーが型だ）
  • Presheaves-as-Types（前層が型だ）
  • Copresheaves-as-Types（余前層が型だ）
  • Functors-as-Types（関手が型だ）

Objects は“圏の対象”のことです。Objects-as-Types はかなり広い概念です。Sets は集合圏の対象だし、Algebras は代数の圏の対象、Coalgebras は余代数の圏の対象です。Categories でさえ、圏達の2-圏の対象ですから、Objects-as-Types に含まれると言えます。

Functors-as-Types も、広い範囲の型理論を包摂できるキャッチフレーズです。Families, Presheaves, Copresheaves は、いずれも Functors の特殊ケースです。

カートメル／ヴォエヴォドスキー／パルムグレンの型理論は、基本的には Presheaves-as-Types の立場の型理論です。が、Propositions-as-Types（Formulae-as-TypeTerms）も扱えるように配慮しています。また、グロタンディーク構成を繰り返し適用することにより、カートメルツリー構造（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）を実現しています。

カートメルツリー構造を持つことから、Presheaves-as-Types の立場の型理論を、抽象的な構造であるC-システムとみなすことが出来ます。つまり、カートメル／ヴォエヴォドスキーの一般論を適用できます。

単純型理論 vs. 依存型理論

あまたある型理論を分類する基準として、単純型理論と依存型理論という二分法を採用することもあります。

型理論を圏論的に解釈するとして、単純型理論〈simple type theory〉は Objects-as-Types で考えるだけです。例えば、型理論特有の型付け判断〈type juedgedment | typing judgement | 型付け判断〉
$`\quad C \vdash t:A`$
は次のように圏論的に解釈できます。

  • $`C, A`$ は、（なんか適当な）圏 $`\cat{C}`$ の対象である。
  • $`t`$ は、$`C`$ から $`A`$ への射である。

つまり、上記の型判断は次の圏論的な主張と同じことです。

$`\quad t : C \to A \In \cat{C}`$

また、$`C \vdash t: A\to B`$ の圏論的解釈は次です。

$`\quad t : C \to [A, B] \In \cat{C}`$

型理論の矢印は、圏論（のデカルト閉圏）では角括弧〈ブラケット〉です。ちなみに、型理論の型判断の記号 '$`\vdash`$' *2は論理の証明可能性の記号と同じですが、違う意味です。ややこしいのは、十分に抽象化すると「やっぱり同じ意味」になったりすることです。

この事例からうかがえるかも知れませんが、型理論、圏論、集合論、論理を一緒に語るときは、括弧・カンマ・コロン・矢印などの基本的な記号が奪い合いになって、記号法（用語法もだけど）はカオスになります。呼び名や書き方の泥沼状態の説明や言い訳に矢鱈に時間を取られます。この泥沼がなければ、かなり明快な話なのですがねぇ‥‥

さて、依存型理論〈dependent type theory〉ですが、単純型理論と比べてだいぶ複雑です。Objects-as-Types と考えていてはウマくいきません。型とは別にコンテキスト〈context〉という概念を導入して、Objects-as-Contexts（対象がコンテキストだ）と考えます。型は、圏の対象とは別なナニカになります。

依存型理論における型判断は次の形です。

$`\quad \Gamma \vdash t: A`$

$`\Gamma`$ がコンテキスト（圏の対象）です。ギリシャ文字大文字なのは単なる習慣で、僕はラテン文字もよく使います。$`A`$ は型です。型はコンテキストとは別物なので、コンテキスト達の圏の対象ではありません。

ここから先の解釈は、依存型理論ごとに差があります。圏論ベースの依存型理論だけでもたくさんある（「ダラッっと依存型理論・インスティチューション // 色々な型理論的圏」参照）ので、特にカートメル／ヴォエヴォドスキー／パルムグレンの型理論ではどう解釈するかを次節で説明します。

コンテキスト拡張

前節で指摘したように、型理論、圏論、集合論、論理を一緒に語る際の困難は、記号法・用語法がグチャグチャになってしまうことです。記号法・用語法は圏論のものを使って整理することにします。他の分野の記号法・用語法としては奇妙になってしまうかも知れません。

「0-圏または1-圏」を「(0|1)-圏」のように書くことにします。インデックス付けられた集合族と前層と余前層をひっくるめて「ファミリー」と呼びます。集合圏のアロー圏の対象（単なる写像）と圏のファイブレーション〈ファイバー付き圏〉をひっくるめて「バンドル」と呼びます。

$`X`$ が(0|1)-圏で、$`F`$ が $`X`$ 上のファミリーのとき、次のように書きます。

$`\quad F:X^\bullet \to \mbf{Set} \In \mbf{CAT}`$

$`F`$ が反変関手のときは黒丸の位置に $`{^\mathrm{op}}`$ が入ります。$`F`$ が共変関手なら黒丸の位置はカラッポです。$`X`$ が0-圏（集合）のときは反変・共変の別は無意味です。しかし、0-圏 $`X`$ を1-圏とみなして考えます。

(0|1)-圏 $`X`$ 上のすべてのファミリーの集合（圏ではない）を次のように書きます。この書き方は圏論の標準的記法です。

$`\quad |[X^\bullet, \mbf{Set}]|`$

型理論の習慣に従い、(0|1)-圏をコンテキストと呼び、ギリシャ文字大文字 $`\Gamma`$ などで書きます。「コンテキストとはなんぞや？」という問〈とい〉は無意味です。「(0|1)-圏 $`X`$」の別な呼び方・言い回しとして「コンテキスト $`\Gamma`$」を導入しただけで、コンテキストという新しい概念を定義したわけではありません。

同様に、別な呼び方・言い回しとして、$`|[\Gamma^\bullet, \mbf{Set}]|`$ の要素を「コンテキスト $`\Gamma`$ 内の型」という呼び方・言い回しもします。

コンテキスト（つまり(0|1)-圏） $`\Gamma`$ と、$`\Gamma`$ 内の型（つまりファミリー） $`A`$ に対して、そのグロタンディーク構成を「コンテキスト $`\Gamma`$ の、型 $`A`$ による拡張〈extension〉」と呼び、$`\Gamma\cdot A`$ と書きます。

$`\quad \Gamma\cdot A := \int_\Gamma A`$

グロタンディーク構成の標準射影を $`\rho^{\Gamma, A}`$ と書きます。

$`\quad \rho^{\Gamma, A}: \Gamma\cdot A \to \Gamma \In \mbf{CAT}`$

型理論の言葉でも、$`\rho^{\Gamma, A}`$ はやはり標準射影〈canonical projection〉と呼びます。

カートメル／ヴォエヴォドスキー／パルムグレンの型理論は、グロタンディーク構成によるバンドル-ファミリー対応を基本的な道具として使います。型理論的内容を、圏論の手法で展開します。型理論の言葉と圏論の言葉の対応は以下のようです。

型理論 圏論
コンテキスト 0-圏または1-圏
型 ファミリー（前層、余前層含む）
コンテキスト拡張 グロタンディーク構成
標準射影 （バンドルの）標準射影
インスタンス セクション

インスタンスは、以下の型判断に出てくる $`t`$ のことです。

$`\quad \Gamma \vdash t: A`$

上記の型判断を圏論の記法に翻訳すると：

$`\quad t : \Gamma \to \Gamma\cdot A \In \mbf{CAT}\\
\quad \text{where }t * \rho^{\Gamma,A} = \mrm{Id}_\Gamma
`$

$`t`$ も $`\rho^{\Gamma,A}`$ も関手なので、結合〈合成〉の図式順記号として $`*`$ を使いました。

おわりに

前節のように、圏論の記法・用語法で概念を定義すると、「型理論をやっている気がしない」と感じる人がいるかも知れません。内容は確実に型理論です。言葉・言い回し・書き方が違うだけです。

しかし、文化・言語が異なる分野・コミュニティのあいだで翻訳をすると、翻訳後のものはオリジナルとは違うとみなされるかも知れません。確かに違ってしまうでしょう。しかし、違いの部分は心理的・情緒的なもので、論理的・構造的な違いがあるとは思えません。

カートメル／ヴォエヴォドスキー／パルムグレンの型理論は、文化的・言語的な食い違いに悩まされる話題ではありますが、僕のイチ推しの型理論です。

*1:"Logical Relations as Types: Proof-Relevant Parametricity for Program Modules", Jonathan Sterling, Robert Harper

*2:記号の名前はターンスタイル記号です。型判断に使うときは特に判断ストローク〈judgement stroke〉と呼んだりします。