GAT〈ガット〉の構文： スターリングの論文から

過去記事「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

6月にチラ見しただけなので、もう一度読んでみようとしたら、ド頭から読めない！ アレレ？

「あっ、そういえば」と思い出しました。この論文は、型理論界隈の因習的な語法・記法を使っていて、読みやすいものではないのでした。以前、語法・記法の解読をしたのですが、記録してなかったのですっかり忘れました。

今回は記録しておくことにします。記録（＝この記事）は、GAT〈generalized algebraic theory〉の構文解説にもなるでしょう。$`\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} }
`$

内容：

因習的な語法・記法

スターリング論文の最初にGAT〈ガット | generalized algebraic theory | 一般化代数セオリー〉の構文の説明があります。型理論界隈では普通の書き方で説明されています。“普通”ということは、次のような困った伝統〈因習〉に沿っているということです。

1. メタレベルの構文とオブジェクトレベルの構文を（一部だが）区別しない。
2. 同義語／多義語を気まぐれに使う。
3. コロンとターンスタイル記号（'$`\vdash`$'）を矢鱈に（過剰に）使う。
4. 演算子記号と区切り記号を区別しない（オーバーロードする）。
5. 所属記号 '$`\in`$' を所属とは別な意味で使う。
6. 空リストに混乱しやすい変わった記号を使う。
7. 構文定義〈文法規則〉と実際に使う構文は別物（建前と本音は違う）。

スターリング論文には、まったく説明されてない構文的メタ変数がいきなり出てきます（これはさすがに伝統ではないけど）。

構文的要素の名前	構文メタ変数	実際に使う構文
ソート名またはオペレーション名	$`\vartheta`$	ボールド体ラテン文字の文字列
変数	$`x, y`$	イタリック体ラテン文字一文字

構文メタ変数 $`\vartheta`$ が表す実際の名前は $`\mbf{ob}, \mbf{id}`$ のようなボールド体ラテン文字の文字列です。構文メタ変数 $`x`$ が表す実際の名前は $`x, y`$ のようなイタリック体ラテン文字一文字*1で、構文メタ変数と実際に使われる変数の区別は付きません。が、構文定義用メタ構文と実際に使う構文が見た目では区別できないことはままあります（文脈で区別）。

ソート{名 | 記号}とオペレーション{名 | 記号}を表すメタ変数の区別がないのも分かりにくいです。この記事の説明では、ソート名の構文メタ変数は $`\sigma`$ 、オペレーション名の構文メタ変数は $`\vartheta`$ とします（詳細後述）。

構文定義（文法）で定義される構文的対象物〈syntactic object〉の呼び名は次のようです。

スターリングの呼び名	その他の呼び名
セオリー	指標、ベースコンテキスト
公理	等式的法則、等式、法則
テレスコープ	局所〈ローカル〉コンテキスト、コンテキスト
ソート	型{項}?
オペレーション	関数、オペレーター
項	インスタンス項、オペレーション項、関数項
代入	コンテキスト射

「セオリー」は、ローヴェアの意味だとある種の圏だし、論理では演繹で閉じた論理式／シーケントの集合の意味で使ったりするので、（それと僕は「セオリー」は出来るだけ避けたいので）「指標〈signature〉」にします。

指標とコンテキストは同じモノです。が、指標の圏とコンテキストの圏は互いに反対圏なので（「 指標の圏はコンテキストの圏の反対圏 」参照）、区別する意味はあります。

依存型理論に現れるコンテキストの圏はファイバー付き圏〈圏のファイブレーション〉なので、ベース圏の対象であるコンテキストと、トータル圏またはファイバー〈局所圏〉の対象であるコンテキストは区別しないと混乱します。ここでは、ベースコンテキスト〈base context〉と局所コンテキスト〈local context〉として区別します（「GAT〈ガット〉」参照）。「コンテキスト」と「指標」が同義なので、ベース指標と局所指標の区別があります。

BCDE〈Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó〉などの用語法だと、ベースコンテキスト＝ベース指標を単に指標、局所指標＝局所コンテキストを単にコンテキストと省略しています。スターリングは別な論文で、逆な省略法（コンテキスト＝ベースコンテキスト、指標＝局所指標）を採用していました。ここでは、指標＝ベース指標＝ベースコンテキストとして、局所コンテキストの「局所」は省略しない方針にします。

「ソート＆オペレーション」か「型＆関数」かは好み・流儀の違いで、良し悪しを議論してもしょうがないのでスターリングが使っていた「ソート＆オペレーション」を使います*2。「ソート＝ソート項、項＝オペレーション項」というアンバランスな省略も多数派の用法なので、今回はケチを付けずに使います。ここでの「ソート」は構文的なので、意味論的ソートを表す予定の記号表現〈項〉のことです。「代入〈substitution〉」も多数派なのでそのまま使います。

スターリングの用語とこの記事で説明に使う用語の対応は：

スターリングの呼び名	この記事の呼び名
セオリー	指標
公理	等式
テレスコープ	局所コンテキスト
ソート	ソート
オペレーション	オペレーション
項	項
代入	代入

この節冒頭に箇条書きで挙げた因習的な語法・記法の残りは、後で触れます。

GAT指標の構文

GATと呼ばれる形式的体系の中核となる構文的対象物は、（GATの）指標です。指標を構成するため、あるいは指標を利用するために判断〈judgement〉と導出規則〈推論規則〉があります。

GATの指標は、通常の指標の拡張になっていて、もちろん通常の指標もGATの指標とみなせます。次は、半群の通常の指標です。

$`\T{signature }\msf{Semigroup}\:\{\\
\quad \T{sort }\msf{U} \In \mbf{Set}\\
\quad \T{operation }\msf{op} : \msf{U}\times\msf{U} \to \msf{U} \In \mbf{Set}\\
\quad \T{equation }\msf{assoc} : \\
\quad \: \top \to \forall (x, y, z\in \msf{U}).\, \msf{op}(\msf{op}(x, y), z) = \msf{op}(x, \msf{op}(y, z)) \In \mbf{Logic}\\
\}
`$

（スターリングの）GAT指標の構文では、上記のような通常の指標とは違った発想と書き方をします。オペレーション〈関数〉のプロファイル〈入出力の仕様〉は、直積型を使わずに、引数変数を伴う多変数関数の形で書きます。引数変数は沿えますが、戻り値変数（出力結果を表す変数）は使いません。

$`\quad \T{operation }\msf{op} : (x\in \msf{U}, y\in \msf{U}) \to \msf{U} \In \mbf{MSet}`$

$`\mbf{MSet}`$ は、射〈複射〉が多変数関数であるような複圏〈オペラッド〉です。複圏を知らなくてもあまり気にしなくていいです。タプル単一引数ではなくてほんとの多引数を考えることが重要な点です。

もとの指標の $`\msf{U} \In \mbf{Set}`$ の意味は $`\msf{U}\in |\mbf{Set}|`$ と同じです。これを次のように解釈し直します。

$`\quad \T{sort }\msf{U} : \mbf{1} \to |\mbf{Set}| \In \mbf{SET}`$

さらに、単元集合 $`\mbf{1}`$ からの関数は0引数の多変数関数だ考えて次のように書きます。

$`\quad \T{sort }\msf{U} : () \to |\mbf{Set}| \In \mbf{MSET}`$

もとの指標の結合律 $`\msf{assoc}`$ は、当該の命題が成立していることを主張しています。命題（「「命題」の曖昧性から前層意味論へ」参照）を対象とする圏 $`\mbf{Logic}`$ のなかで、真を表す対象 $`\top`$ から当該命題への射 $`\mbf{assoc}`$ が存在すれば、その射は当該命題（結合律）成立の証拠となります。

（スターリングの）GATでは、等式的法則に関して別な発想をして別な書き方をします。次のようです。

$`\quad \T{equation }\msf{assoc} :\\
\quad \: (x, y, z\in \msf{U}) \to (\msf{op}(\msf{op}(x, y), z) \equiv \msf{op}(x, \msf{op}(y, z)) \In \msf{U}) \In \mbf{MSet}
`$

記号 '$`\equiv`$' は、二項述語としての等号ではなくて、両辺が等しいことの証拠あるいは保証としての等号です。言い方を変えれば、'$`\equiv`$' は、両辺が等しい保証込みなのです。「『述語としての等号を含む命題がすべての $`x, y, x`$ に対して真』である保証がある」と「すべての $`x, y, x`$ に対して、『等号が真である保証』が対応している」は、内容的には同じですが、発想が違います。

集合 $`\msf{U}`$ における「等号が真である保証」が何であるか気になるなら、集合 $`\msf{U}`$ を離散圏とみなしたときの射だと捉えればいいでしょう。つまり、要素 $`x \in |\msf{U}|`$ に対する $`\id_x\in \mrm{Mor}(U)`$ が $`x \equiv x`$ です。

ここで、簡潔に書けるような書き方の約束を導入します。キーワード sort, operation, equation はなくても困らないので省略します。$`|\mbf{Set}|`$ を $`\mbf{Sort}`$ と書きます。すると、半群の指標は次のように書けます。

$`\T{signature }\msf{Semigroup}\:\{\\
\quad \msf{U}: () \to \mbf{Sort} \In \mbf{MSET}\\
\quad \msf{op} : (x, y\in \msf{U}) \to \msf{U} \In \mbf{MSet}\\
\quad \msf{assoc} : \\
\quad \: (x, y, z\in \msf{U}) \to (\msf{op}(\msf{op}(x, y), z) \equiv \msf{op}(x, \msf{op}(y, z)) \In \msf{U}) \In \mbf{MSet}\\
\}
`$

さらに、それぞれのプロファイル宣言を“どこで考えているか？”を示す行末の $`\In \cdots`$ も推測可能だとして省略します。

$`\T{signature }\msf{Semigroup}\:\{\\
\quad \msf{U}: () \to \mbf{Sort} \\
\quad \msf{op} : (x, y\in \msf{U}) \to \msf{U} \\
\quad \msf{assoc} : \\
\quad \: (x, y, z\in \msf{U}) \to (\msf{op}(\msf{op}(x, y), z) \equiv \msf{op}(x, \msf{op}(y, z)) \In \msf{U}) \\
\}
`$

“どこで考えているか？”の情報は、名前 $`\msf{U}, \msf{op}, \msf{assoc}`$ で表されるモノが住んでいる場所〈生息地 | 居住地〉のことです。この情報を省略してしまうのはいかがなものか？ と僕は思います。伝統としては、生息地は意味論で考えることで、構文側では明記しないことになっています。

GAT指標で圏を定義する

GAT指標の特徴とウリは、ソート〈型項〉が、関数と同様に引数〈パラメータ〉を持てることです。前節のソート $`U`$ も引数を持っていたのですが、0引数なので引数渡しは省略していたのです。

引数付きソート〈パラメータ付き型項〉を使った例として、小さい圏の指標を書いてみます。ホムセットを使った定義で、ホムセットは“対象をパラメータとするソート”になります。

$`\T{signature }\msf{Category}\:\{\\
\quad \msf{O}: () \to \mbf{Sort} \\
\quad \msf{H}: (x, y\in \msf{O}) \to \mbf{Sort} \\
\quad \msf{cmp} : (x, y, z\in \msf{O}, f\in \msf{H}(x,y), g\in \msf{H}(y, z)) \to \msf{H}(x, z) \\
\quad \msf{assoc} : \\
\quad \: (x, y, z, w\in \msf{O}, f\in \msf{H}(x, y), g\in \msf{H}(y, z), h\in \msf{H}(z, w) ) \\
\quad \: \to (\msf{cmp}(\msf{cmp}(f, g), h) \equiv \msf{cmp}(f, \msf{cmp}(g, h)) \In \msf{H}(x, w)) \\
\quad \cdots (省略) \cdots\\
\}
`$

$`\msf{O}`$ は圏の対象の集合を表す名前〈記号〉です。$`\msf{H}`$ は圏のホムセットを表す名前〈記号〉ですが、2つのパラメータを持ち、パラメータは $`\msf{O}`$ の要素です。$`\msf{cmp}`$ は圏の結合〈composition〉演算を表すオペレーター名〈オペレーター記号〉です。$`\msf{cmp}`$ は5つの引数〈パラメータ〉を持つオペレーターですが、視認性などを考慮して便宜上次のように書くことが多いでしょう。

$`\quad \msf{cmp}_{x, y, z}(f, g)`$

下付きにした3つの引数は推測可能なので省略してかまいません。さらに中置演算子記号 '$`;`$' を使うとかは記法規約〈notational conventions〉の問題となり、理論上はどうでもいいところなので踏み込みません。

圏の指標で省略した部分は、恒等〈identity〉の宣言と、等式的法則である左単位律と右単位律です。

上に書いた指標による圏の定義は、可読性も悪くなく、意味もまーまー取りやすいと思います。これは、可読性のための省略をしているからです。省略しないでマジメに書くとして：

1. $`\msf{O}`$ に引数（0個だけど）をチャンと渡して $`\msf{O}()`$ と書く。
2. $`(x, y\in \msf{O})`$ のようなまとめて宣言をせずに、ひとつずつバラして書く。
3. $`\msf{cmp}`$ の引数を省略しないで書く。

やってみます。

$`\T{signature }\msf{Category}\:\{\\
\quad \msf{O}: () \to \mbf{Sort} \\
\quad \msf{H}: (x\in \msf{O}(), y\in \msf{O}()) \to \mbf{Sort} \\
\quad \msf{cmp} : (x\in \msf{O}(), y\in \msf{O}(), z\in \msf{O}(), f\in \msf{H}(x,y), g\in \msf{H}(y, z)) \to \msf{H}(x, z) \\
\quad \msf{assoc} : \\
\quad \: (x\in \msf{O}(), y\in \msf{O}(), z\in \msf{O}(), w\in \msf{O}(), f\in \msf{H}(x, y), g\in \msf{H}(y, z), h\in \msf{H}(z, w) ) \\
\quad \: \to (\msf{cmp}_{x,z,w}(\msf{cmp}_{x,y,z}(f, g), h) \equiv \msf{cmp}_{x, y, w}(f, \msf{cmp}_{y,z, w}(g, h)) \In \msf{H}(x, w)) \\
\quad \cdots (省略) \cdots\\
\}
`$

マジメ・律儀な感じはしますが、視認性・可読性は劣化しました。構文におけるマジメさ・律儀さと視認性・可読性はトレードオフの関係にあるんですね。ただし、適切な省略の程度があり、省略や乱用をやり過ぎるとまたワケワカメになります。

スターリングの構文定義

前節の最後の圏の指標は、視認性・可読性が悪いですが、スターリングのオリジナルの構文定義を守った書き方だとこんなもんじゃないです。地獄のような視認性・可読性になります。地獄のような構文を定義する構文定義も色々と地獄だし ‥‥

まず、指標は宣言達をならべたリストです。リストは、丸括弧囲み、カンマ区切りとします。視認性・可読性のために、インデントして1行に1項目ずつ縦に並べる書き方をします。リストの区切りカンマと、項目〈宣言〉内に出現するカンマが紛らわしいので、項目〈宣言〉をブラケットで囲むことにします。

前節の最後の圏の指標の本体部分だけをリストとして書くと：

$`(\\
\quad [\msf{O}: () \to \mbf{Sort}], \\
\quad [\msf{H}: (x\in \msf{O}(), y\in \msf{O}()) \to \mbf{Sort}], \\
\quad [\msf{cmp} : (x\in \msf{O}(), y\in \msf{O}(), z\in \msf{O}(), f\in \msf{H}(x,y), g\in \msf{H}(y, z)) \to \msf{H}(x, z)], \\
\quad [\msf{assoc} : \\
\quad \: (x\in \msf{O}(), y\in \msf{O}(), z\in \msf{O}(), w\in \msf{O}(), f\in \msf{H}(x, y), g\in \msf{H}(y, z), h\in \msf{H}(z, w) ) \\
\quad \: \to (\msf{cmp}_{x,z,w}(\msf{cmp}_{x,y,z}(f, g), h) \equiv \msf{cmp}_{x, y, w}(f, \msf{cmp}_{y,z, w}(g, h)) \In \msf{H}(x, w))\\
\quad ],\\
\quad \cdots (省略) \cdots\\
)
`$

ここで、次の習慣を適用します。

• コロンとターンスタイル記号（'$`\vdash`$'）を矢鱈に（過剰に）使う。

また、二項述語としての等号と等式成立の保証を含む等号の区別もやめます。すると次のようになります。

$`(\\
\quad [\msf{O}: () \vdash \mbf{Sort}], \\
\quad [\msf{H}: (x : \msf{O}(), y : \msf{O}()) \vdash \mbf{Sort}], \\
\quad [\msf{cmp} : (x: \msf{O}(), y: \msf{O}(), z: \msf{O}(), f: \msf{H}(x,y), g: \msf{H}(y, z)) \vdash \msf{H}(x, z)], \\
\quad [\msf{assoc} : \\
\quad \: (x: \msf{O}(), y: \msf{O}(), z: \msf{O}(), w: \msf{O}(), f: \msf{H}(x, y), g: \msf{H}(y, z), h: \msf{H}(z, w) ) \\
\quad \: \vdash (\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))\\
\quad ],\\
\quad \cdots (省略) \cdots\\
)
`$

さらに、スターリングのオリジナル構文では：

• $`\mbf{Sort}`$ をなぜかイタリックの $`sort`$ と書く。$`sort`$ は実体を指さない単なるキーワードかも。
• 名前はボールド体小文字の文字列。
• $`\mbf{H}: (x : \mbf{O}(), y : \mbf{O}()) \vdash {sort}`$ なら、 括弧の種類と位置を変えて $`\mbf{H}: [x : \mbf{O}(), y : \mbf{O}() \vdash {sort}]`$ のように書く。
• 空リストの $`()`$ は $`\cdot`$ と書く。（空リストに混乱しやすい変わった記号を使う。）
• 余分な丸括弧は付けない。
• 等式的法則には名前を付けない。

次のようになります。

$`(\\
\quad [\mbf{o}: [\cdot \vdash {sort}] ], \\
\quad [\mbf{h}: [x : \mbf{o}\cdot, y : \mbf{o}\cdot \vdash {sort}] ], \\
\quad [\mbf{cmp} : [x: \mbf{o}\cdot, y: \mbf{o}\cdot, z: \mbf{o}\cdot, f: \mbf{h}(x,y), g: \mbf{h}(y, z) \vdash \mbf{h}(x, z)] ], \\
\quad [ \\
\quad \: x: \mbf{o}\cdot, y: \mbf{o}\cdot, z: \mbf{o}\cdot, w: \mbf{o}\cdot, f: \mbf{h}(x, y), g: \mbf{h}(y, z), h: \mbf{h}(z, w) \\
\quad \: \vdash \mbf{cmp}_{x,z,w}(\mbf{cmp}_{x,y,z}(f, g), h) = \mbf{cmp}_{x, y, w}(f, \mbf{cmp}_{y,z, w}(g, h)) : \mbf{h}(x, w)\\
\quad ],\\
\quad \cdots (省略) \cdots\\
)
`$

だいぶ難読化できました ‥‥ って、難読化が目的じゃないんだけどなー。

実は極め付きの難読化（目的じゃないんだけど）構文があります。それは次節にして、次のことに触れておきます。

• 演算子記号と区切り記号を区別しない（オーバーロードする）。
• 所属記号 '$`\in`$' を所属とは別な意味で使う。
• 空リストに混乱しやすい変わった記号を使う。

スターリングのGAT指標の、BNF記法による構文生成規則は次のようです（原論文と僅かに変えています）。

• 指標 $`\mathbb{T} ::= \emptyset \mid \mathbb{T}, (\sigma : \mathscr{S}\mid \vartheta : \mathscr{O}) \mid \mathbb{T}, \mathscr{E}`$
• ソート宣言本体 $`\mathscr{S} ::= [\Psi \vdash sort]`$
• オペレーション宣言本体 $`\mathscr{O} ::= [\Psi \vdash A]`$
• 項の等式 $`\mathscr{E} ::= [\Psi \vdash M = N : A]`$
• 局所コンテキスト $`\Psi ::= \cdot \mid \Psi, x : A`$

上記の構文生成規則の右辺には出てきてない構文要素は以下のとおり。

構文要素の名前	構文メタ変数
ソート名	$`\sigma`$
オペレーション名	$`\vartheta`$
ソート〈型項〉	$`A`$
項〈関数項・値項〉	$`M,N`$
変数（の名前）	$`x`$

習慣・伝統〈因習〉も含めて慣れてないと、なかなか解読できないですよね。

1. $`::=`$, $`|`$, $`(\:)`$, はBNF構文生成規則の記号。
2. さまざまな文字種・フォントの構文メタ変数〈非終端記号〉が出てくる。
3. $`\emptyset`$ と $`\cdot`$ は空リスト $`()`$ を表す記号。（空リストに混乱しやすい変わった記号を使う。）
4. コロン $`:`$、ターンスタイル $`\vdash`$、ブラケット $`[\:]`$、イコール $`=`$ は実際にそのまま使うリテラル〈終端記号〉。
5. $`sort`$ も実際にそのまま使うリテラル。
6. カンマは区切り記号のリテラルではない。リストの最後に項目（リストの成分）を追加する構文的な演算子記号。

カンマをリスト演算の記号として使うのは非常に一般的です。この演算を snoc〈スノック〉と呼んだりするのですが、Lispのリスト演算である cons（リストの先頭に項目を追加する）の逆綴りです。つまり、「構文生成規則内のカンマはスノックを表す」と。ほんとに隠語と因習の世界。

構文生成規則の補足的条件に $`\sigma \in \mathbb{T}`$ とか $`(\vartheta : \mathscr{O})\in \mathbb{T}`$ のような表現が出てきますが、これは集合の所属関係ではありません。次の意味です。

• 指標 $`\mathbb{T}`$ のなかに、ソート名 $`\sigma`$ が出現する。
• 指標 $`\mathbb{T}`$ のなかに、オペレーション宣言 $`\vartheta : \mathscr{O}`$ が出現する。

[追記]
BNF記法を使う場合、「リテラル〈終端記号〉は必ずクォートする」という規則を守るだけで、構文メタ変数〈非終端記号〉かリテラル〈終端記号〉か分からないという問題は解決します。なのに、実際に行われないのは、実はリテラルを決める気がないからかも知れません。一見リテラルのように書いてあっても、その綴りに決めたいわけではないので、実は変数なのです。
[/追記]

引数渡し

「極め付きの難読化」について説明します。GAT指標では、ソートもオペレーションも引数〈パラメータ〉を持ちます。ソート名（を表すメタ変数）を $`\sigma`$ 、オペレーション名（を表すメタ変数）を $`\vartheta`$ とするとき、これらの名前〈記号〉への引数渡しの正式な構文は次の形になります。

• $`\sigma\langle \psi \rangle`$
• $`\vartheta\langle \psi \rangle`$

つまり、引数を山形括弧のなかに入れます。山形括弧のなかの $`\psi`$ は代入を表します。

代入〈substitution〉とは、変数への値の割り当てを表す記号的表現です。代入の構文は以下のように決めます。

• $`\psi ::= \cdot \mid \psi, x := M`$

隠語・因習を使って構文生成規則を書いています。

1. $`::=`$, $`|`$ はBNF構文生成規則の記号。
2. $`\psi`$ は、代入を表す構文メタ変数〈非終端記号〉。
3. $`\cdot`$ は空リスト $`()`$ のこと。（空リストに混乱しやすい変わった記号を使う。）
4. カンマはスノック演算を表す（演算子記号と区切り記号を区別しない）。
5. $`x`$ は、変数を表す構文メタ変数〈非終端記号〉。実際に使う変数〈終端記号〉と区別が付かない。
6. $`M`$ は、項〈関数項・値項〉を表す構文メタ変数〈非終端記号〉。
7. := は、実際にそのまま使うリテラル〈終端記号〉。（スターリングの原論文ではスラッシュを使っていて、左右は逆です。）

例えば、$`()`$ とか $`(x := 1)`$ とか $`(x := 1, y := a + 2)`$ とかは算術定数・演算が使える場合の代入の例です。

引数渡しには、山形括弧のなかに代入を入れるので、$`f`$ がオペレーション名〈関数記号〉だとして、次のような形になります。

• $`f\langle () \rangle`$
• $`f\langle (x := 1) \rangle`$
• $`f\langle (x := 1, y := a + 2) \rangle`$

空リストは $`\cdot`$ と書くので、一番目は $`f\langle \cdot \rangle`$ が正式です（空リストに混乱しやすい変わった記号を使う）。

代入に出現する変数（の名前）は重複してはダメです。順序は場合により変えても良さそうですが、スターリングは順序も定義された順番を守る前提のようです。だったら、「変数の名前は不要だろう」と思うでしょ。が、「変数の名前も定義された順番で書く」のがオフィシャルな構文定義です。これはかなり面倒です。例えば：

• $`f()`$ は $`f\langle \cdot \rangle`$ と書く。
• $`f(1)`$ は $`f\langle (x := 1) \rangle`$ と書く。
• $`f(1, 2)`$ は $`f\langle (x := 1, y := 2) \rangle`$ と書く。
• $`f(x, g(3))`$ は $`f\langle (x := x, y := g \langle (x := 3) \rangle ) \rangle`$ と書く。

ソートやオペレーションに関して、「定義時の引数変数名を、呼び出しのたびに繰り返し間違いなく記述する」は、現実には耐えられない仕様ですが、理論上の取り扱いが若干簡単になるメリットがあります。

要するに、現実に使うことは想定してないのですが、試みに、圏の定義に出てきた引数渡しの一部を、オフィシャルな構文で書いてみましょう。

• $`\mbf{o}\cdot`$ は $`\mbf{o}\langle \cdot\rangle`$
• $`\mbf{h}(x, z)`$ は $`\mbf{h}\langle (x := x, y:= z) \rangle`$
• $`\mbf{cmp}_{y, z, w}(g, h)`$ は $`\mbf{cmp}\langle (x := y, y:= z, z := w, f := g, g := h) \rangle`$
• $`\mbf{cmd}_{x, y, w}(f, \mbf{cmp}_{y, z, w}(g, h))`$ は
  $`\mbf{cmd}\langle (x := x, y:= y, z := w, f := f, g := \mbf{cmp}\langle (x := y, y:= z, z := w, f := g, g := h) \rangle )\rangle`$

オフィシャルな引数渡し構文を使って圏を定義する指標を書くと、普通の人ではまず読めないシロモノが出来上がります。当然に使い物になりません。次の了解事項があるのです。

• 構文定義〈文法規則〉と実際に使う構文は別物（建前と本音は違う）。

おわりに

スターリングが定義しているGAT指標の構文は、理論的な取り扱いが目的なので、「可読性が悪い」だの「使い物にならない」だのと文句をつけるスジアイはありません。ただ、「実際に使う気なんてない」ことを最初に表明したほうが誤解は招かないとは思います。そして、諸々の奇妙な約束事と暗黙の了解事項も部外者にはなかなか想像できないので、出来るだけ明示的に書いたほうがいいと思います。「面倒くさくてやってられん」という事情も察しは付くけど。

*1:形式的定義では変数が無限にあるとするので、文字が無限にあると想定します。

*2:証明支援系においては、「ソート」は型ではなくて、宇宙の意味で使うことが多いようです。