最近の記事「GAT〈ガット〉の構文： スターリングの論文から」で、スターリング〈Jonathan Sterling〉によるGAT構文を紹介しました。そのままではとても実用にならないシロモノですが、理論的には扱いやすく優れたアイディアが含まれていると思います。
スターリングは、型理論界隈の伝統と習慣〈ありていに言って因習〉に従って彼の構文を記述していて、スターリング独自の奇妙な規則もあって、スターリング論文はとっつきにくいものとなっています。内容は良いのにもったいない。
スターリング構文にシンタックスシュガーをまぶして、実用にも使える構文にします。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\M}{\text{-} }
%\newcommand{\T}[1]{\text{#1} }
\newcommand{\id}{\mathrm{id} }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\rev}{\mathop{\triangleleft} }
\newcommand{\snoc}{\mathop{\blacktriangleleft} }
\require{enclose}
`$
内容：
大枠、基準
2012年に「型理論ってば」という記事を書きました。型理論の用語法が錯綜していてヤンナッチャウという話です。12年以上経過した今でも（12年くらいじゃ変わらんわな）型理論の語法・記法はグチャグチャで相変わらず困っています。型理論を、集合論、圏論、論理などと一緒に論じると状況はさらに悪化します。
まずは、次のことを心に留めておきましょう。
- 型理論の「コンテキスト」と、一般代数学〈universal algebra | 普遍代数学〉／モデル理論／インスティチューション理論の「指標」は同じモノである。
- コンテキストを対象としてコンテキスト射を射とする圏がある。それが型理論で扱う圏〈型理論的圏〉である。正確に言えば：
- 型理論的圏の公理系が幾つかある。「ダラッっと依存型理論・インスティチューション // 色々な型理論的圏」参照。
- 公理系で規定される型理論的圏の対象を習慣として「コンテキスト」と呼ぶ。
- 公理系で規定される型理論的圏の射を「コンテキスト射」と呼ぶ。
- コンテキストを対象としてコンテキスト射を射とする圏の反対圏の対象（これもコンテキストなのだが）を習慣的に「指標」とも呼ぶ。指標の圏の射は「指標射」。「指標射」は、「コンテキスト射」の向きを形式的に逆にしたもの。「指標の圏はコンテキストの圏の反対圏」参照。
- 依存型理論では、型理論的圏としてファイバー付き圏〈fibered category〉が使われる。ファイバー付き圏のベース圏の対象を「ベースコンテキスト」、ファイバー〈局所圏〉またはトータル圏の対象を「局所コンテキスト」と呼ぶ。「GAT〈ガット〉」参照。
- 依存型理論における「型」と「インスタンス」の定義は人・場合により異なり複雑である。
型理論の語法・記法は錯綜していますが、上記の“事実”は、さまざまな語法・記法の相互翻訳の基準を与えてくれるでしょう。
スターリングの語法・記法・アイディア
スターリングの論文を再掲しておくと：
- [Ste19-]
- Title: Algebraic Type Theory and Universe Hierarchies
- Author: Jonathan Sterling
- Submitted: 23 Feb 2019
- Pages: 25p
- URL: https://arxiv.org/abs/1902.08848
使う用語と記号に関しては（「GAT〈ガット〉の構文： スターリングの論文から」にも記述あり）：
| スターリング | 多数派 | ここで使うのは |
|---|---|---|
| セオリー $`\mathbb{T}`$ | 指標 $`\Sigma`$ | 指標 $`\Sigma`$ |
| テレスコープ $`\Psi`$ | ？ | 局所コンテキスト $`\Psi`$ |
| ソート記号 $`\vartheta`$ | 型名 | ソート名 $`\sigma`$ |
| オペレーション記号 $`\vartheta`$ | 関数名 | オペレーション名 $`\theta`$ |
| 変数（メタ変数） $`x`$ | ？ | 変数{名} $`\xi`$ |
| 適用 $`\vartheta\langle \varphi \rangle`$ | 適用 $`f(\varphi)`$ | 適用 $`\varphi\rev\varphi`$ |
| ソート $`A`$ | 型 $`A`$ | ソート{項}? $`A`$ |
| 項 $`M`$ | 項 $`t`$ | {オペレーション}?項 $`M`$ |
| 代入 $`\varphi`$ | 代入 $`\sigma`$ | 代入〈局所コンテキスト射〉$`\varphi`$ |
スターリングは、ソート記号〈ソート名〉とオペレーション記号〈オペレーション名〉を構文的には区別してません。ここでは、ソート名の集合、オペレーション名の集合、変数{名}?の集合は、互いに無交差〈disjoint〉な3つの集合として準備します。実際の変数としてイタリック体ラテン文字を使うので、変数の集合を走る変数（メタ変数）にはギリシャ文字を使うことにします。
「型」と「ソート」、「関数」と「オペレーション」は同義語として、特に区別はしないで使います。
スターリングの構文の特徴は、関数の定義として引数変数の名前と順番を指定して、それを公開することです。関数の利用者〈呼び側〉は、公開された関数の引数変数名と順番を正確に知っていて、それを使って関数を呼び出します。関数の宣言時の仮引数リスト〈formal parameter list〉は、構文的には局所コンテキスト〈local context〉と呼びます。呼び出し時に使われる実引数リスト〈actual argument list〉は、構文的には代入〈substitution〉と呼びます。
- 局所コンテキストは、関数の宣言時の仮引数リストに使う。
- 代入は、関数の呼び出し時の実仮引数リストに使う。
引数変数名が関数の一部なので、引数変数名をリネームすると別な関数になります。関数を特定するには、引数変数名のリストの情報が必要です。このことは、実用的な見地からは困った仕様ですが理論的にはメリットもあります。
構文定義
スターリングのオリジナルの構文（をわずかに変えたもの）の定義は、「GAT〈ガット〉の構文： スターリングの論文から」を見てください。
ここでの構文は次のように定義します。$`\varepsilon`$ は等式の名前〈ラベル〉です。記号 '$`\snoc`$' は構文的なスノック演算（「GAT〈ガット〉の構文： スターリングの論文から」参照）です。
指標 $`\Sigma ::= () \mid \Sigma \snoc (\mathscr{S} \mid \mathscr{O} \mid \mathscr{E})`$
ソート宣言 $`\mathscr{S} ::= \sigma : \Psi \to \mbf{Sort}`$
オペレーション宣言 $`\mathscr{O} ::= \theta : \Psi \to A`$
等式 $`\mathscr{E} ::= \varepsilon : \Psi \to \text{holds }M = N : A`$
局所コンテキスト $`\Psi ::= () \mid \Psi \snoc \xi : A`$
ソート $`A ::= \sigma \rev \varphi`$
項 $`M ::= \xi \mid \theta\rev \varphi`$
代入 $`\varphi ::= () \mid \varphi \snoc \xi := M`$
上の構文定義は、やっぱり内輪の人間なら分かるジャーゴン〈隠語〉による記述ですね。
昔風の文字種・フォントを使わないプレーンテキストによる記述ならば、文法の終端記号と非終端記号の区別は引用符を使えば済むのですが、色々な文字種・フォントを使うと、どれが終端記号か分からなくなります。内輪の人間なら分かりますが。
終端記号を明示的に識別する方法を幾つか試してみたのですが、LaTeX〈MathJax〉だと引用符はどうもウマくない。終端記号を四角枠で囲んでみましょう。例えば：
等式 $`\mathscr{E} ::= \varepsilon \enclose{box}{:} \Psi \enclose{box}{\to} \enclose{box}{\text{holds }} M \enclose{box}{=} N \enclose{box}{:} A`$
局所コンテキスト $`\Psi ::= \enclose{box}{()} \mid \Psi \snoc (\xi \enclose{box}{:} A)`$
四角枠で囲った部分は終端記号なので、そのまま書きます。スノック演算を表す '$`\snoc`$' は、構文生成規則内で使う演算子記号で、終端記号ではないので、オブジェクトレベル構文に現れることはありません。
ツリーの絵に描くともっともっと分かりやすくなりますが、描くのが面倒なので、構文定義にはほとんど使われていません。自分でツリーを描くといいですよ。
[/追記]
シンタックスシュガー
スターリングの構文を実用的に使える程度に改善するため、理論的構造はそのままにシンタックスシュガーを構成します。シンタックスシュガーは、構文的な妖精さん（マクロメカニズムとか）が面倒を見てくれると想定します。
妖精さんがやってくれること、つまりスターリングの構文からの表面的変更点は以下です。
- 引数渡しのとき、引数変数名を省略できる。
- 仮引数リスト／実引数リストを分割してよい。
- 指標のなかの等式に名前を付ける。
- オペレーションの宣言に、記法の規約〈notational conventions〉を書けるようにする。
- 記法の規約から、暗黙引数〈implicit arguments〉が推測できるようにする。
- 固有名 $`\mbf{Sort} := |\mbf{Set}|`$ を導入する。
- その他、馴染みやすいキーワードや構文に変更する。
例題としては、「GAT〈ガット〉の構文： スターリングの論文から // GAT指標で圏を定義する」で述べた、GAT指標による小さい圏の定義を使います。
スターリングのオリジナルの構文にはあまり触れません。「GAT〈ガット〉の構文： スターリングの論文から // スターリングの構文定義」と原論文を参照してください。
指標の書き方は、「曖昧性を減らす： Diag構成を事例として // 指標の書き方」で述べた書き方を使います。プレーンテキストのなかにLaTeX〈MathJax〉数式をインラインで混ぜて書きます。例えば：
signature $`\msf{Semigroup}`$ {
sort $`\msf{U}`$ in $`\mbf{Set}`$
operation $`\msf{op}`$ : $`(\msf{U}, \msf{U})\to \msf{U}`$ in $`\mbf{Set}`$
equation $`\msf{assoc}`$ : $`\top \to \forall(x, y, z \in \msf{U}). \msf{op}(\msf{op}(x,y), z) = \msf{op}(\msf{op}(x, y), z)`$ in $`\mbf{Logic}`$
}
この記事だけの話ですが、指標で導入される名前はサンセリフ体ラテン文字列の名前とします。
圏の指標
この節は、内容としては「GAT〈ガット〉の構文： スターリングの論文から // GAT指標で圏を定義する」と同じです。
型理論の習慣として次があります。
- コロンとターンスタイル記号（'$`\vdash`$'）を矢鱈に（過剰に）使う。
コロンは使うことにしますがターンスタイルは使わないことにします。関数を表す通常の矢印を使います。
小さい圏の指標は次のように書きます。
signature $`\msf{Category}`$ {
sort $`\msf{O}`$ : $`()\to \mbf{Sort}`$
sort $`\msf{H}`$ : $`(x, y:\msf{O})\to \mbf{Sort}`$
operation $`\msf{cmp}`$ : $`(x, y, z: \msf{O})(f: \msf{H}(x, y), g: \msf{H}(y, z)) \to \msf{H}(x,z)`$
...(省略)...
}
普通の書き方に見えますが、けっこうシンタックスシュガーを使っています。
- 冗長な（なくてもいい）キーワード sort, operation を使って読みやすくしている。
- $`\msf{O}`$ は0引数のソートなので、スターリング記法では $`\msf{O}\langle \cdot \rangle`$ 。ここでの構文だと、$`\msf{O}\rev()`$ だが、0引数のソート／オペレーションでは、引数渡しを完全に省略していいとする。
- 0引数でなくても、引数渡し〈評価 | 適用〉の演算子 $`\rev`$ は省略していいとする。
- 引数渡しの実引数リストの引数変数名は省略していいとする。引数の順番があるので、引数変数名は再現できる。
- $`(x:\msf{O}, y:\msf{O})`$ を $`(x, y:\msf{O})`$ とまとめて宣言していいとする。
- $`\msf{cmp}`$ の5つの引数を3個と2個に分割して宣言していいとする。気持ちとしてはカリー化なのだが、正式なカリー化は導入せずに、単に構文的に仮引数リストも実引数リストも分割（グループ化）していいとする。
もっと説明的な書き方をしてみます。
signature $`\msf{Category}`$ {
sort $`\msf{O}`$ :
for $`()`$
$`\msf{O} : \mbf{Sort}`$
sort $`\msf{H}`$ :
for $`(x, y:\msf{O})`$
$`\msf{H}(x, y) : \mbf{Sort}`$
operation $`\msf{cmp}`$ :
for $`(x, y, z: \msf{O})`$
for $`(f: \msf{H}(x, y), g: \msf{H}(y, z))`$
$`\msf{cmp}(x, y, z)(f, g) : \msf{H}(x,z)`$
...(省略)...
}
sort 宣言は $`\msf{O} : \mbf{Sort}`$ と略記してもいいでしょう。丸括弧は適宜省略していいとします。
オペレーション $`\msf{cmp}`$ に関する等式的法則を記述してみます。
signature $`\msf{Category}`$ {
sort $`\msf{O}: \mbf{Sort}`$
sort $`\msf{H}`$ :
for $`(x, y:\msf{O})`$
$`\msf{H}(x, y) : \mbf{Sort}`$
operation $`\msf{cmp}`$ :
for $`(x, y, z: \msf{O})`$
for $`(f: \msf{H}(x, y), g: \msf{H}(y, z))`$
$`\msf{cmp}(x, y, z)(f, g) : \msf{H}(x,z)`$
equation $`\msf{assoc}`$ :
for $`(x, y, z, w:\msf{O})`$
for $`(f :\msf{H}(x, y),g :\msf{H}(y, z),h :\msf{H}(z, w) )`$
holds $`\msf{cmp}(x,z,w)( \msf{cmp}(x,y,z)(f, g), h) =`$
$`\msf{cmp}(x,y,w)(f, \msf{cmp}(y, z, w)(g, h)) :\msf{H}(x, w)`$
...(省略)...
}
キーワード holds は、直後の等式が実際に成立していることを強調しています。
上記のような記述なら、まずまずの可読性で理解もしやすいと思います。が、$`\msf{cmp}`$ に引数が5つも付いているのが煩雑ではあります。もう少し工夫しましょう。
記法の規約
通常の圏論においては、$`\msf{cmp}(x, y, z)(f, g)`$ のような煩雑な書き方はしないで、$`f;g`$ とか $`g\circ f`$ と書きます。中置演算子記号を使っていると同時に、一部の引数を省略しています。このような記法の規約〈notational conventions〉も書き込むことにします。
signature $`\msf{Category}`$ {
sort $`\msf{O}: \mbf{Sort}`$
sort $`\msf{H}`$ :
for $`x, y:\msf{O}`$
$`\msf{H}(x, y) : \mbf{Sort}`$
operation $`\msf{cmp}`$ :
for $`x, y, z: \msf{O}`$
for $`f: \msf{H}(x, y), g: \msf{H}(y, z)`$
$`f;g ::= \msf{cmp}(x, y, z)(f, g) : \msf{H}(x,z)`$
equation $`\msf{assoc}`$ :
for $`x, y, z, w:\msf{O}`$
for $`f :\msf{H}(x, y),g :\msf{H}(y, z),h :\msf{H}(z, w)`$
holds $`(f;g);h = f;(g;h) :\msf{H}(x, w)`$
...(省略)...
}
'$`::=`$' を使った記法の規約により、次のことを宣言しています。
- $`\mbf{cmp}`$ を中置演算子記号 $`;`$ で表すこと。
- 引数 $`(x, y, z)`$ は省略していいこと。
$`\mbf{cmp}`$ の最初の3つの引数は暗黙引数〈implicit arguments〉として扱われます。暗黙引数は省略していいし、省略しても他の引数から再現できます。
上で使った '$`::=`$' は、オブジェクトレベル構文に出現する記号です。たまたま、構文定義のためのメタレベル構文であるBNF〈Backus–Naur form〉の記号とコンフリクトしてますが、別物です。「左辺は右辺で定義される」という意味では、BNF構文生成規則の '$`::=`$' と少し似てますが、オブジェクトレベルとメタレベルなので別物です。
[/追記]
おわりに
スターリングの構文にシンタックスシュガーをまぶしましたが、もとの構文・アイディアを本質的に変えたわけではなくて、単なる表層的な変更です。見た目が変わるだけのことなので、理論的なメリットはそのまま残されています。
シンタックスシュガー付きスターリング構文は、依存型理論とGATの説明に有効に使えると思います。
