型理論では、「代入〈substitution〉」という言葉を幾つかの意味で使います。この記事では複数の意味を切り分けて別な呼び名を与えることにします。
ある人々にとっては、いちいち呼び分けることは鬱陶しくてバカバカしいことに思えるでしょう。しかし、誰もが曖昧多義語を自力で難なく解釈できるわけでもなくて、混同・混乱・誤解してしまうこともあります。「代入」の曖昧性を一度は分析しておく意義はあるでしょう。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\hyp}{\text{-} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{ \text{ in } }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\ot}{\leftarrow}
\newcommand{\op}{\mathrm{op}}
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Ent}{ \sqsubseteq }
%\newcommand{\hinfer}{ \rightrightarrows }% horizontal meta rule (infer)
%\newcommand{\vinfer}{ \downdownarrows }% vertical meta rule (infer)
%%
%\require{color} % Using
%\newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name
%\newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression
%\newcommand{\T}[1]{\text{#1} }
`$
内容:
型理論を語ることの難しさ
集合論は、そんなにたくさんはありません。有名どころは:
ツェルメロ/フレンケル集合論が圧倒的多数派で、事実上の独占状態になっています。通常の用途では、「集合論 = ツェルメロ/フレンケル集合論」だとしてかまいません。
論理も、古典論理が圧倒的多数派なので、「論理 = 古典論理」で問題ありません。
しかし、型理論は何百もあり、圧倒的多数派は存在せず、現状は群雄割拠の時代です。「型とはなんぞや?」に対しても、それぞれの型理論がそれぞれの答を準備しています。「集合論・圏論 vs. 型理論」から再掲すると:
- Sets-as-Types
- Algebras-as-Types
- Coalgebras-as-Types
- Propositions-as-Types
- Categories-as-Types
- Logical Relations-as-Types*1
- ‥‥
この記事で想定してる型理論は、カートメル/ヴォエヴォドスキー/パルムグレンの型理論(「 カートメル/ヴォエヴォドスキー/パルムグレンの型理論」参照)です。カートメル/ヴォエヴォドスキー/パルムグレンの型理論のキャッチフレーズは次です。
- Families-as-Types
- Functors-as-Types
一般的には「関手が型だ」と考えますが、特に関手の域が離散圏のときは「ファミリーが型だ」となります。
型理論の構文としては、スターリングのGAT構文(「GAT〈ガット〉の構文: スターリングの論文から」「実用になる型理論の記法」参照)を念頭に置いています。
「代入」の意味
とりあえず見渡すと、「代入」が6種類くらいの意味で使われているようです。それぞれの意味ごとに別な呼び名を用意しましょう。
- 代入文〈substitution statement〉 : $`\xi := M`$ という形式の構文的対象物
- 代入レコード〈substitution record〉 : 代入文の順序付き名前付きのコレクション
- 代入作用〈substitution action〉 : 代入レコードの項に対する作用
- 構成手続き〈construction procedure〉としての代入レコード : コンテキスト射の構文的表現(それが構成手続き)としての代入レコード
- 還元手続き〈reduction procedure〉としての代入レコード : 指標射の構文的表現(それが還元手続き)としての代入レコード
- 代入結合〈substitution composition〉 : 構成手続きまたは還元手続きに対する二項演算
これらを理解するには、さらに次の用語の理解が必要です。
- 構文的対象物〈syntactic object〉*2
- 順序付き名前付きのコレクション
- 項
- 作用
- コンテキスト射
- 指標射
- 構文的表現
- 結合
これらの用語も解説していきます。
型理論と圏論の記法
型理論と圏論では、記法のコンフリクト(競合/かち合い)が起きているので、そのことをハッキリさせておきます。
まず、「圏」という言葉は、1-圏に限らず2-圏、3-圏などの高次圏をも意味するとします。また、0-圏(つまり、単なる集合)かも知れません。任意の n に対して、n-圏は、高次の恒等射を追加して考えれば(n + 1)-圏とみなせます。とはいえ、「圏 = 1-圏」の場合が多いですが。
$`\cat{C}`$ を圏(つまり、n-圏)だとして、次の左右は同じ意味です。
$`\quad A\In \cat{C} \iff A \in |\cat{C}|`$
$`\quad f : A \to B \In \cat{C} \iff f\in \cat{C}(A, B)`$
$`\quad \alpha :: f \twoto g: A\to B \In \cat{C} \iff \alpha\in \cat{C}(A,B)(f, g)`$
このとき使われているコロンは、プロファイルコロン〈profile colon〉と呼ぶことにします。
一方、型理論の居住関係〈inhabitation relation〉を表すコロンは居住記号〈inhabitation symbol〉と呼ぶことにします。
圏論における内部ホムを構成する演算子記号は $`[\hyp,\hyp]`$ が多数派ですが、型理論では矢印 $`\hyp\to\hyp`$ が演算子記号に使われます。ここでは、折衷案で $`[\hyp \to \hyp]`$ を内部ホムの記号とします。
圏論のプロファイル記述と型理論の居住記号を区別して書きたいときは、居住記号に $`\in:`$ を使います。多くのケースで、次の左右は同じ意味です。右が型理論、左が圏論です。
$`\quad a \in: A \iff a : \mbf{1} \to A \In \cat{C}`$
$`\quad f \in: A \to B \iff f:\mbf{1} \to [A\to B]\In \cat{C}`$
型理論では圏 $`\cat{C}`$ が暗黙化されます。集合圏を想定しているなら、次のようです。
$`\quad a \in: A \iff a : \mbf{1} \to A \In \mbf{Set}`$
$`\quad f \in: A \to B \iff f:\mbf{1} \to [A\to B]\In \mbf{Set}`$
さらに、ポインティング写像と要素を同一視して、集合論の記法で書くなら:
$`\quad a \in: A \iff a \in A`$
$`\quad f \in: A \to B \iff f \in \mrm{Map}(A, B)`$
以下では、プロファイルコロンと居住記号が紛らわしいときは、居住記号に上記のように $`\in:`$ を使います。型理論的文脈だとハッキリわかるときは、居住記号にコロンを使います。内部ホムは常に $`[\hyp \to\hyp]`$ を使います。
構文か意味か
以下は同義語で、どっちを使うかは好みの問題です。
- ソート = 型
- オペレーション = 関数
圏論的解釈をするなら、ソートは圏の対象であり、オペレーションは特別な射のことです。このように、ソート/オペレーション(型/関数 と言っても同じ)を意味的対象物〈semantic object〉と解釈する場合、その意味的対象物を表現する構文的対象物〈syntactic object〉を「項〈term〉」と呼びます。
- ソートを表現する構文的対象物はソート項〈型項〉
- オペレーションを表現する構文的対象物はオペレーション項〈関数項〉
論理では、項〈個体項〉と式〈論理式〉を区別することがありますが、ほとんどの分野・場合で、項〈term〉と式〈expression〉は同義語です。
型理論ではしばしば、ソート項〈型項〉を単にソート〈型〉とも呼び、オペレーション項〈関数項〉を単にオペレーションとも呼びます。構文論中心に考えるなら、そういう呼び方になります。しかしそうなると、意味的対象物をなんて呼ぶか? ここでは、ソート実体〈sort entity〉、オペレーション実体〈operation entity〉と呼ぶことにします。
構文論中心 | 意味論中心 |
---|---|
ソート = ソート項 | ソート = ソート実体 |
オペレーション = オペレーション項 | オペレーション = オペレーション実体 |
型理論は構文論の議論が多いので、ソートがソート項を意味し、オペレーションがオペレーション項を意味する場面が多いです。さらに、次のようなアンバランスな規約が多数派です。
- 「ソート〈型〉」はソート項〈型項〉を意味する。
- 単に「項」と言ったら、それはオペレーション項〈関数項〉を意味する。
- 「ソート」が(文脈により)ソート実体を意味することもある。
- 「項」が(文脈により)オペレーション実体を意味することもある。
オペレーション項をインスタンス項と呼ぶこともあります(僕はけっこう使います)が、「インスタンス」がこれまた曖昧多義語なので(「型理論のインスタンスとは」参照)、「インスタンス」は使わないほうが吉かも知れません。
型理論の構文圏
なにか(意味)を表す予定の記号的な構造が構文的対象物〈syntactic object〉です。構文的対象物は、文字・記号・名前などを基本データとして形式文法〈formal grammar〉を使って定義されます。
型理論に出てくる構文的対象物達を編成して圏に仕立てることが出来ます。そのような圏を(型理論の)構文圏〈{syntax | syntactic} category〉と呼ぶことにします。習慣として、構文圏の対象をコンテキスト〈context〉、射をコンテキスト射〈context morphism〉と呼びます。コンテキスト射の別名が“代入”ですが、この意味での代入は、用語「代入」の4番目の用法である「構成手続きとしての代入レコード」のことです。
コンテキストと指標〈signature〉は同義語です。この2つの言葉が指すモノはまったく同じです。指標については「構造記述のための指標と名前 1/n 基本」「インターフェイスとしての指標、設計者と利用者と実装」を参照してください。
コンテキストと指標は同じモノですが、コンテキストの圏〈category of contexts〉 $`\cat{C}`$ と指標の圏〈category of signatures〉 $`\cat{S}`$ は違います(同じ圏ではない)。互いに反対圏なのです。次の関係が成立しています。
- $`|\cat{S}| = |\cat{C}|`$
- $`\cat{C}^\op = \cat{S}`$
- $`\cat{S}^\op = \cat{C}`$
詳しくは次の過去記事に書いています。
$`\cat{C}`$ を型理論の構文圏だとして、次のような事情です。
- $`\Gamma\in |\cat{C}|`$ をコンテキストと呼ぶ。(ギリシャ文字大文字を使うのは習慣)
- 同じ $`\Gamma`$ を $`\Gamma \in |\cat{C}^\op|`$ とみなしたモノを指標と呼ぶ。
- $`\varphi : \Gamma \to \Delta \In \cat{C}`$ をコンテキスト射と呼ぶ。
- 同じ $`\varphi`$ を $`\varphi : \Delta \to \Gamma \In \cat{C}^\op`$ とみなした射を指標射と呼ぶ。
コンテキスト/指標は、宣言文を並べた構文的対象物ですが、コンテキスト射/指標射もまた構文的対象物です。コンテキスト射/指標射に関わる諸々の構文的対象物を(多義的に)「代入」と呼ぶのです。
様々な代入
やっと本題の「代入」の話です。
構文的メタ変数に関しては「実用になる型理論の記法」とだいたい同じ約束を採用します。
- 指標を表すメタ変数は $`\Sigma,\Gamma`$ など
- 名前を表すメタ変数は $`\xi, \eta`$ など
- ソート項を表すメタ変数は $`A, B`$ など
- オペレーション項を表すメタ変数は $`M, N`$ など
なんらかのモノを順序付きで並べたコレクション型データをリスト〈list〉と呼びます(普通どおり)。順番は一切なくて、名前〈キー〉で識別するコレクション型データをディクショナリ〈dictionary〉と呼びます。
成分〈component | item〉に順番(あるいは順序位置)があり、名前〈キー〉でも参照できるコレクション型データは、ここではレコード〈record〉と呼ぶことにします。レコードは、リストとディクショナリの両方に性格を持つので、囲み記号は丸括弧でも波括弧でもどっちでもいいとします。成分の区切り記号はカンマか改行とします。レコードは、名前とナニカのペアのコレクションですが、以下の表現はどれもレコードとして許容します。
$`( (\xi, X), (\eta, Y) )`$
$`\{ (\xi, X), (\eta, Y) \}`$
$`( \\
\quad (\xi, X)\\
\quad (\eta, Y)\\
)`$
$`\{\\
\quad (\xi, X) \\
\quda (\eta, Y) \\
\}`$
指標内に出現する宣言文では、ペア $`(\xi, X)`$ を $`x : X`$ と書きます。コロンは型理論の居住記号なので、そのことを明示したいなら $`\xi : X`$ です。
代入文では、ペアの区切りに '$`:=`$' を使います。以下が代入文の構文です。
$`\quad \xi := M`$
ここで、$`\xi`$ は名前、$`M`$ はオペレーション項です。名前 $`\xi`$ は、前もって次の形の宣言文で宣言されているとします。
$`\quad \xi \in: A`$
宣言文の右辺 $`A`$ はソート項です。
代入文を幾つか並べたレコード(リストでもディクショナリでもなくてレコード!)が代入レコードです。代入レコードは、単なる構文的対象物のことであり、用途や意味については何も言ってません。
代入レコードが、オペレーション項に作用するときは代入作用(構文的な作用素)であり、代入レコードをコンテキスト射の表現と捉えれば構成手続き、指標射の表現と捉えれば還元手続きです。(いずれも後述。)
*1:"Logical Relations as Types: Proof-Relevant Parametricity for Program Modules", Jonathan Sterling, Robert Harper
*2:生成文法の用語ではなくて、一般的な構文論/意味論に関する用語です。