型理論とインスティチューションの周辺

紹介している資料は、「依存型理論の圏論的セマンティクスの資料」と一部重複しています。$`\newcommand{\cat}[1]{\mathcal{#1}}`$

構文論と形式言語

インスティチューションは、構文論と意味論の枠組みを与えます。抽象的な枠組みだけで、中身はありません -- それが悪いってことではないです。が、より詳細で具体的な構造も付け足したいとは思います。「構文付き変換手インスティチューション 1/n」で出した言葉「半具象インスティチューション〈semi-concrete institution〉」は、インスティチューションの大枠（いわば骨）に、より詳細で具体的な構造（いわば肉）も付け足したものを意味します。

インスティチューションの構文側を具象化することは、なんらかの形式的体系〈formal system〉（「球体集合達の圏の構文表示 2/2 // 形式的体系」参照）について考えることです。形式的体系には形式言語〈formal language〉が付随します。というか、形式言語を定義するための仕掛けが形式的体系だと言っていいでしょう。

形式言語を定義するには、語彙〈vocabulary〉と文法〈grammar〉が必要です。語彙は、基本的〈basic | primitive | atomic | builtin〉な構文的データ〈syntactic data〉の集合のことです。基本的な構文的データをどう組み合わせてより複雑な構文表現を構成するか、その規則を与えるのが文法です。

型理論のコンテキストや、一般代数学〈universal algebra〉／論理の指標は、形式言語の語彙を定義する手段〈defining {device | method}〉です。型理論と一般代数学／論理では、呼び名の食い違いがあります。が、概念的には同様な対象物を扱っています。

型理論	一般代数学／論理
コンテキスト	指標
型	ソート
型なし〈untyped | unityped〉	単ソート〈single-sorted〉
単純型つき〈simply typed〉	多ソート〈many-sorted〉
依存型つき〈dependently typed〉	依存ソート〈dependently sorted〉
型項〈type term〉	？
インスタンス項〈instance term〉	{演算 | 関数}記号／述語記号
？	式〈expression〉

形式言語の語彙は単なる集合以上の構造を持つので、コンテキスト／指標も構造を持つことになります。型理論では、コンテキストの構造を記述する手法が色々あります（「指標の圏はコンテキストの圏の反対圏」参照）。

型理論と一般代数学の相互関係のモダンな記述は、次の論文の "Part 1 Dependently sorted algebraic theories" がいいかも知れません。

• [Sub21-]
• Title: From dependent type theory to higher algebraic structures
• Author: Chaitanya Leena Subramaniam
• Submitted: 6 Oct 2021
• Pages: 155p
• URL: https://arxiv.org/abs/2110.02804

ファミリー付き圏〈category with families〉を中心とした視点からの概観は次のスライドで手っ取り早く知ることができます。

• [Dyb19-]
• Title: Categories with Families: Unityped, Simply Typed, Dependently Typed
• Author: Peter Dybjer
• Date: December 2019
• Pages: 25p（スライド）
• URL: https://cj-xu.github.io/faum/dybjer.pdf

スライドに対応する論文は次です。

• [CCD19-20]
• Title: Categories with Families: Unityped, Simply Typed, and Dependently Typed
• Authors: Simon Castellan, Pierre Clairambault, Peter Dybjer
• Submitted: 1 Apr 2019 (v1), 7 Jul 2020 (v2)
• Pages: 46p
• URL: https://arxiv.org/abs/1904.00827

構文モナド

形式言語の語彙は、コンテキスト／指標として表せます。これらは圏の対象です。語彙から言語の文・式を生成するメカニズムである文法は、コンテキスト／指標の圏の上のモナドにエンコードされます。語彙と文法を表現するモナドを構文モナド〈syntax monad〉と呼ぶことにします。例えば、グラフの圏を指標の圏と考えて、グラフから“パスのグラフ”を作るモナドが構文モナドの例です。

モナドは随伴系に分解することができます（「モナドの分解の比較定理」参照）。アイレンベルク／ムーア分解とクライスリ分解が典型的な分解です。コンピュータッドの圏は、構文モナドの分解のひとつとして登場するのでしょう。

指標の圏（言語の語彙の圏）を $`\cat{S}`$ として、$`\cat{S}`$ 上の構文モナドを分解した随伴系が次の形だとします。

$`\quad \xymatrix@C+1pc{
\cat{S} \ar@/^1pc/[r]^F \ar@{}[r]|\bot
& \cat{C} \ar@/^1pc/[l]^U
}\\
\quad \text{in }{\bf CAT}
`$

とある帰納的・再帰的手順で構成される、随伴系の構成素である $`\cat{C}`$ をコンピュータッドの圏〈category of computads〉と呼び、その圏の対象をコンピュータッド〈computad〉と呼ぶことになります。コンピュータッドは、指標とアイレンベルク／ムーア代数の中間に位置する構造だと言えます。

構文モナドは、単一・一枚岩〈monolithic〉とは限りません。複数のモナド達により文法が提供されるかも知れません。複雑な文法を、より単純な文法を組み合わせて作ることになります。単純な文法はモナドにエンコードされ、ベックの分配法則が組み合わせる手段となるでしょう。文法を組み合わせる規則としてのメタ文法が必要そうです。

メタ文法がどんなものか？ ハッキリとはわからない*1のですが、例えば次の論文はヒントになりそうです。

• [BMW11-]
• Title: Monads with arities and their associated theories
• Authors: Clemens Berger, Paul-André Melliès, Mark Weber
• Submitted: 16 Jan 2011 (v1), 10 Feb 2011 (v2)
• Pages: 30p
• URL: https://arxiv.org/abs/1101.3064

より新しいものは：

• [BG18-20]
• Title: Monads and theories
• Authors: John Bourke, Richard Garner
• Submitted: 11 May 2018 (v1), 2 Jun 2020 (v2)
• Pages: 41p
• URL: https://arxiv.org/abs/1805.04346

相対モナド

前節で出したバーガー／メリス／ウェバーの論文は、アリティ付き圏／アリティ付き関手とアリティ付きモナドを使っています。圏 $`\cat{C}`$ のアリティとは、$`\cat{C}`$ の部分圏 $`\cat{A}`$ で、包含関手 $`\cat{A} \to \cat{C}`$ が稠密関手〈dense functor〉となるものです。アリティ付き関手〈functor with arities | arity-respecting functor〉の定義は少し複雑です（割愛）。アリティ付きモナドは、アリティ付き圏／アリティ付き関手／自然変換の2-圏のなかのモナドです。

アリティ付きモナドは、相対モナドで置き換えられないでしょうか？ アリティ付きモナドより相対モナドのほうが使い勝手が良さそうに思えます。最近、仮想設備〈virtual equipment〉を使った相対モナドの形式論も出てきました。

• [AM23-24]
• Title: The formal theory of relative monads
• Authors: Nathanael Arkor, Dylan McDermott
• Submitted: 27 Feb 2023 (v1), 1 Apr 2024 (v3)
• Pages: 91p
• URL: https://arxiv.org/abs/2302.14014

相対モナドが有望そうな気がするのは、ヴォエヴォドスキー〈Vladimir Voevodsky〉が相対モナドを使っていたからです。

• [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

ヴォエヴォドスキーは、型理論の理論〈theory of type theories〉を構築しようとしてましたが、志半ばでこの世を去りました。ヴォエヴォドスキーのプロジェクトは後継者達により進行しているようです。

• [AENR23-24]
• Title: Algebraic Presentations of Dependent Type Theories
• Authors: Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke
• Submitted: 27 Feb 2023 (v1), 1 Apr 2024 (v3)
• Pages: 63p
• URL: https://arxiv.org/abs/2111.09948

ボンヤリした印象に過ぎないのですが、アリティ付きモナドや相対モナドを使った型理論〈構文論〉の定式化は、モナド／ローヴェア圏／ナーブ定理〈脈体定理〉（「「代数」への三種のアプローチと回路代数」参照）を結びつける形になるのではないでしょうか。

*1:ストリート〈Ross Street〉がリース〈wreath | 花輪〉と呼んでいたものがメタ文法かも知れません。「複合モナドから花輪積へ」参照。