「型理論のジャングルに踏み込むための心構えと装備 1/2」において、次の基本概念を説明しました。
- 単純型
- 単純型のインスタンス
- 依存性を持つ型
- シグマ型形成子
- シグマ型
- シグマ型の標準射影
- 依存性を持つ型のインスタンス
- パイ型形成子
- パイ型
これらの集合論的単純型理論／集合論的依存型理論の概念に基づき、この記事では、型理論の語彙・用語法が“どんなことになっちゃっているか”を分析しましょう。
型理論の語彙・用語法で困ることは、頻繁に使われる基本用語の意味が曖昧なことです。ここで取り上げる基本用語は次の言葉達です。
- 依存型
- 依存積型
- 項
- 構成子
- 命題
内容：
そもそも「依存型」が意味不明
依存型理論（ここでは集合論的依存型理論）では、「依存」という言葉を多用しますが、場面ごとに意味は違います。
- 「依存性を持つ型」の場合： パラメータ〈インデックス〉に依存して関数値である型が変わる。
- 「依存ペア」の場合： 第一成分に依存して第二成分の型が決まる。
- 「依存関数」の場合： 引数値に依存して戻り値型が決まる。
これらの場合、「ナニカは、ナニカに依存する」構造があります。
- 関数〈族〉の値は、パラメータに依存する。
- 第二成分の型は、第一成分に依存する。
- 戻り値の型は、引数値に依存する。
しかし、形容詞「依存」が、「なにかしら『依存』と関係しそう」とか、「依存型理論に出てくる」という程度の意味で使われることがあります。
例えば、「シグマ型は依存型である」という言い方に目くじらを立てる人はあまりいません。言いたいことは「シグマ型は、依存型理論に出てくる特徴的な型である」とか「シグマ型は、単純型理論ではお目にかからない型である」でしょう。
しかし、シグマ型は単純型です。シグマ型形成子は、集合族〈依存性を持つ型〉に単一の集合〈単純型〉を対応させるので、シグマ型形成子で作られたシグマ型は単純型です。
ややこしいのは、「シグマ型は単純型」であっても、「シグマ型は依存性を持たない〈依存性を持つ型ではない〉」とも言い切れないことです。集合 $`X`$ と集合族 $`X^\sim`$ は一対一に対応する*1ので、単純型と“自明な依存性を持つ型”はしばしば同一視されます。そうなると、「シグマ型は自明な依存性を持つ型である」は言えます。
自明な依存性であっても依存性に違いはないから、「シグマ型は依存性を持つ型」は正しいことになります。しかし、「シグマ型は依存型である」と発言した人がそのように考えているケースは少ないでしょう。また、「いやっ、シグマ型は依存型ではない」と反論する人がいれば、その人の気持ちは「シグマ型は非自明な依存性を持たない」ということでしょう。
次の3つを区別しないとナニガナニヤラ？の議論になります。
- なんらかの依存性を持つ型（集合族）
- 自明な依存性を持つ型（単元集合上で定義された集合族）
- 非自明な依存性を持つ型（2個以上の要素を持つ集合上で定義された集合族）
シグマ型は単純型（単なる集合）だと言うと、シグマ型には標準射影が組み込まれているので「単なる集合ではなくて構造物〈structure〉ではないか」といぶかしく思う人もいるでしょう。確かにシグマ型は構造を持ちます。しかし、集合は構造を持てないわけではないです。タルスキー／グロタンディーク集合論、あるいはその元になっているZFC集合論では、単なる集合でも極めて複雑な構造を持てます。「単純型（単なる集合）だから構造を持てない」は誤りです。
「依存型」は依存型理論の主題のはずですが、その主題を表す言葉が意味不明な状態なのです。
「依存積型」はトラブルメーカー
「依存積型〈dependent product type〉」という言葉があります。これは、ひどい曖昧多義語です。
- シグマ型を、依存積型と呼ぶことがある。
- パイ型を、依存積型と呼ぶことがある。
Aさんが「依存積型」をシグマ型の意味で使っていて、Bさんが「依存積型」をパイ型の意味で使っていたなら、AさんとBさんのコミュニケーションはどこかで破綻するでしょう。
どうしてこんな事態になったのかと言うと：
- 発想-1 ： シグマ型 $`\sum_X F`$ は、直積型〈単純積型〉 $`X\times Y`$ の一般化だから「依存積型」と呼ぼう。そして、パイ型 $`\prod_X F`$ は指数型〈単純関数型〉$`[X, Y]`$ の一般化だから「依存指数型」または「依存関数型」と呼ぼう。
- 発想-2 ： シグマ型 $`\sum_X F`$ は、総和記号を使っているから「依存和型」と呼ぼう。そして、パイ型 $`\prod_X F`$ は総積記号を使っているから「依存積型」と呼ぼう。
それぞれの発想は合理性がありますが、一緒にすると、ひどい曖昧多義語「依存積型」が誕生します。
実際僕は「依存積型」で混乱した経験があります。その記録が残っています。
- 「依存型とΣ-Δ-Π随伴、そしてカン拡張」の冒頭
- 「リスト、タプル、タグ付きデータ、関数、依存関数」の冒頭
「項」は嫌い
「型理論のジャングルに踏み込むための心構えと装備 1/2」では「インスタンス」という言葉を使いました。インスタンスの定義は、シグマ型の標準射影のセクションでした。
型理論では、「インスタンス」という言葉をあまり使いません。「インスタンス」ではなくて「項〈term〉」が多数派です。しかし僕は、「項」にはどうにも馴染めません。このことは「型理論へのファイブレーション的アプローチ： インスタンスとは // 「インスタンス」を「項」と呼ぶのはやめよう」で詳しく書いています -- 過去記事を読んでみてください。
ジョイアル〈Andre Joyal〉は、項と呼ぶのは“間違いだ〈is incorrect〉”とまで言っています。しかし、ジョイアルの呼び名は「要素〈element〉」で、「それじゃ集合論の要素と混同するだろ」と。そんなこんなで「インスタンス」を使っています。
「項」という呼び名のまずいところは、言葉自体が構文論的なので、そうじゃなくても曖昧な構文論と意味論の区別をさらに曖昧にしてしまうことです。僕の対策は：
- 「インスタンス」は、意味論実体を指すと約束する。
- 構文論的である場合はインスタンス項〈instance term〉と呼ぶ。
- 意味論的であることを強調したいならインスタンス実体〈instance entity〉と呼ぶ。
ちなみに、デ・ブール〈Menno de Boer〉の対策は：
- 構文論的である場合は項式〈term expression〉と呼ぶ。
- 意味論的である場合は項〈term〉と呼ぶ。
しかし、term と expression は同義語または類義語として使うので、term expression はどうかな？ と感じます。
「インスタンス」に代わる言葉として「住人〈inhabitant〉」があります。型理論で使われているコロンは居住関係〈inhabitation relation〉の記号ということになります。住人が存在する型は被居住〈inhabited〉な型*2です。
「インスタンス」「住人」を、型の値〈value〉とかデータ〈data〉と呼ぶ場合もあります。が、「値／データ」はポピュラー過ぎる多義語なので、あまり推奨はできません。ただし、単純型のインスタンスを「値」と呼ぶのは悪くないと思っています。
いずれにしても、構文論と意味論の区別もなしにインスタンス項／インスタンス実体を「項」と呼ぶのはやめたほうがいいと思います。と、僕が言ったところで何の効果もないでしょうが。
なお、型理論では、そもそも「構文論と意味論の区別が難しい」ことは「型理論周辺、何で混乱するのか？ // 構文論的意味論と意味論的意味論」に書いています。
微妙な言葉「構成子」
「型理論のジャングルに踏み込むための心構えと装備 1/2」とこの記事では、「型形成子〈type former〉」を使っています。普段僕は、「型構成子〈type constructor〉」を使うことが多いのですが、「構成子」が微妙な言葉なので今回は避けました。
通常、「型構成子」は「型形成子」と同義だと思っていいでしょう。あえて区別するなら、「型構成子」が意味論的、「型形成子」は構文論的です。しかし、単に「構成子」と言うと、ほとんどの場合「型形成子」の意味はなくなります。
型理論における「構成子」は「データ構成子」のことで、帰納的に定義される型のデータ〈インスタンス | 値〉を定義するモノです。つまり、次が同義語だということです。
- 構成子
- データ構成子
- インスタンス構成子
- 値構成子
ある型が帰納的に定義されたとき、付随するデータ構成子は「その型の構成子」です。例えば Planetmath の説明 では the type’s constructors という言い方をしています。the type’s constructors を日本語にすれば「型の構成子」で、「の」を省略すると「型構成子」になります。
もちろん、シッカリした文脈（事前の約束事）のもとで「型構成子」「構成子」を使うぶんには何の問題もないのですが、文脈が薄い状況では迂闊に使えない言葉です。
「命題も型」と言うけれど
Propositions-as-Types の立場、あるいはカリー／ハワード／ランベック対応の観点から言えば、「命題は型だ」と言えます。もう少し分かりやすい言い方をするなら； 単純型理論のなかで命題論理は展開できるし、依存型理論のなかで述語論理は展開できる、ということです。
そういうことであれば、型理論の言葉と論理の言葉が揃っていてくれたら嬉しい。実情はどうでしょうか？
| 型理論 | 論理 |
|---|---|
| 型 | 命題 |
| 単純型 | 真偽値（単純命題とは言わない） |
| 依存型 | 述語（依存命題とは言わない） |
| 単純型のインスタンス | 真（インスタンスという言葉は使わない） |
| 依存型のインスタンス | ？？ |
| 単純型のインスタンス項 | 命題論理の証明 |
| 依存型のインスタンス項 | 述語論理の証明 |
「？？」は適当な言葉がないということです。個人的には、単純型／依存型のインスタンスに相当する論理的概念は「証拠〈witness〉」と呼んでますが、一般的とは言えません。
構造的には綺麗な対応があるのですが、用語のうえではあまり綺麗な対応はしていません。そればかりか、「型」という用語の曖昧性に引きずられて、「命題」も曖昧に使用されます。「命題」の意味は：
- 真偽値（単純型に相当）
- 真（単純型のインスタンスに相当）
- 述語（依存型に相当）
- 論理式（型項／型式に相当）
論理では、構文論と意味論をシッカリ分ける習慣がありますが、型理論のなかで展開された論理は、構文論・意味論の区別が曖昧化される傾向があるようです。
おわりに
この記事で取り上げたのは、集合論的単純型理論／集合論的依存型理論に限って、特に目立って理不尽な曖昧多義語や歪んだ用語体系です。これ以外にも、混乱誘発的〈confusing〉な用語法・記法や、誤認・誤解をまねくハマリ所はたくさんあります。
注意力を研ぎ澄まして、落とし穴に落ちないようにしましょう。
*1:「型理論のジャングルに踏み込むための心構えと装備 1/2 // 依存性を持つ型のインスタンス」参照。
*2:口頭で「ひきょじゅう」と言うと「非居住」という否定の意味に取られかねないので、「居住された型」と言う方が無難です。
