「デジタル語彙目録:: 名前の管理」において、次のように書きました。
ありていに言って、デジタル語彙目録作成は、
$`\qquad`$ひたすら名前との戦い
です。
名前をソフトウェアを使ってキチンと管理しようとすると、その名前が何を指すのか？ どんな種類の名前なのか？ どの名前空間に入れるべきか？ などをマジメに考えなくてはなりません。
常に名前をマジメに考える必要はあるのですが、特にデジタル語彙目録を作る過程では、名前をシリアス／シビアに扱う作業が発生します。
「名前をマジメに考える」とはどういうことなのかを、ひとつの具体例を使って説明します。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\doct}[1]{\mathbb{#1}}
%\newcommand{\M}{\text{-} }
\newcommand{\T}[1]{\text{#1} }
\newcommand{\id}{\mathrm{id} }
%\newcommand{\dimU}[2]{{#1}\!\updownarrow^{#2}}
\newcommand{\ClassOf}[1]{ \{\!| {#1} |\!\} }
\newcommand{\CatOf}[1]{ \langle\!| {#1} |\!\rangle }
%\newcommand{\Opt}[1]{ \{\!/ {#1} /\!\} }
`$
内容：
省略可能フィールド
「リスト」、「タプル」、「ディクショナリ」、「構造体」、「配列」、「シーケンス」、「オブジェクト」、「テーブル・ロー」など、大差ない概念に言葉が矢鱈に溢れかえっていて、まったくウンザリしますが、ここでは「レコード」という言葉を使います。レコードを構成する成分はフィールドです。フィールドはフィール名とフィールド値のペアです。フィールドのあいだには順番があるとします。つまり、「3番名のフィールド」という言い方は意味があります。
関数の引数が省略可能〈optional〉な場合があります。前もってデフォルト値が決まっていたり、他の引数と内部の情報から計算可能だったりすれば、引数は省略できます。同様に、なんらかの事情でレコードのフィールドが省略可能なとき、そのフィールドを省略可能フィールド〈optional field〉ということにします。ときに、省略可能フィールド、あるいは省略されてしまったフィールドを暗黙フィールド〈implicit field〉と小むずかしげに呼ぶこともあります。
レコードの省略可能フィールドが省略されてしまう理由は色々あります。レコードを見たら、フィールドが省略されてないか？ 省略されているとしたらどのような理由で省略されているのか？ 省略を補完したらどうなるのか？ -- これらを必ずシッカリ考えましょう。
「名前をマジメに考える」ことと、「省略をマジメに考える」ことは似た行為で、密接な関係があります。
単射
写像〈関数〉 $`f:X \to Y \In \mbf{Set}`$ が単射であることを表す論理式は次のようです。
$`\quad \forall x, x'\in X.\, f(x) = f(x') \Imp x = x'`$
変数 $`x, x'`$ は全称限量子で束縛された束縛変数なので、この論理式に登場する自由変数は $`X, Y, f`$ です。$`Y`$ は出てきてないように見えますが、等号が集合ごとに決まっているとして書き換えてみると次のようです。論理式に $`Y`$ も含まれます*1。
$`\quad \forall x, x'\in X.\, \mrm{eq}_Y(f(x), f(x')) \Imp \mrm{eq}_X(x, x')`$
この論理式の自由変数〈プレースホルダー〉$`X, Y, f`$ に具体的な集合と写像を代入すれば真か偽が決まります。論理式を、真偽値をとる関数とみなせるのですが、その関数をラムダ式で書けば次のようです。
$`\quad \lambda\, f \in \mbf{Set}(X, Y).\, \forall x, x'\in X.\, \mrm{eq}_Y(f(x), f(x')) \Imp \mrm{eq}_X(x, x')`$
上記の関数の余域は何でしょうか？ $`\mrm{True}`$ と $`\mrm{False}`$ の二値からなる二元集合だと考えてもいいですが、Propositions-As-Types の立場では、圏 $`\mbf{Logic}`$ に値をとると考えたほうが好都合です。圏 $`\mbf{Logic}`$ については「Propositions-As-Typesを曲解しないで理解するために」を見てください。
Propositions-As-Types の立場（のひとつ）では、先の「真偽値をとる関数」とは次のプロファイルの関数です。
$`\quad \mbf{Set}(X, Y) \to \mbf{Logic}`$
実は、上記プロファイルの書き方も記号の乱用、あるいは雑な書き方で、ほんとは次のようです。
$`\quad \mbf{Set}(X, Y) \to |\mbf{Logic}| \In \mbf{SET}`$
今後、論理式は全体をブラケットで囲みます。これには2つの意図があります。
- 論理式を、Propositions-As-Types の立場で解釈することを示す。論理式を評価〈evaluate〉したときの値は $`\mrm{True}`$ と $`\mrm{False}`$ だとは限らない。
- 全体をブラケットでまとめると視認性がよくなる。
例えば、先のラムダ式を使った関数は次のように書きます。
$`\quad \lambda\, f \in \mbf{Set}(X, Y).\, [\forall x, x'\in X.\, \mrm{eq}_Y(f(x), f(x')) \Imp \mrm{eq}_X(x, x')]\\
\qquad : \mbf{Set}(X, Y) \to |\mbf{Logic}| \In \mbf{SET}
`$
集合 $`|\mbf{Logic}|`$ に値をとる関数を述語〈predicate〉と呼びます。述語は関数の特別なモノに過ぎません。
単射の指標と実例
「単射」という名前で呼ぶ概念を形式的に定義するために次の指標を使います。指標の書き方は「曖昧性を減らす： Diag構成を事例として // 指標の書き方」で述べた書き方を使います。プレーンテキストのなかにLaTeX〈MathJax〉数式をインラインで混ぜて書きます。
signature $`\mrm{Injection}`$ {
$`X \in |\mbf{Set}|`$
$`Y \in |\mbf{Set}|`$
$`f: X \to Y \In \mbf{Set}`$
$`\text{injectivity} : \mbf{1} \to [\forall x, x'\in X.\, \mrm{eq}_Y(f(x), f(x')) \Imp \mrm{eq}_X(x, x')] \In \mbf{Logic}`$
}
この指標の実例〈example〉とは、具体的な2つの集合（同じ集合でもよい）とそのあいだの写像、そして、単射であることを表す論理式に対する証明の4つ組です。例えば：
- $`X := \mbf{Z}`$
- $`Y := \mbf{R}`$
- $`f := \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R})`$
- $`\text{injectivity} := \text{👌}`$
最後のOKマーク 👌 は、「曖昧性を減らす： Diag構成を事例として」に説明があります。「証明があると思ってね」といったマークです。
この実例を、フィールド名は省略したレコードとして書けば：
$`\quad (\mbf{Z}, \mbf{R}, \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}), 👌)`$
長さ 4 のレコードです。ところが、最初の2つのフィールドは、3番目のフィールドから確実に推測できます。つまり冗長です。省略します。
$`\quad (\lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}), 👌)`$
これで、長さ 2 のレコードになりました。しかし、単射の実例だと言っているので、単射性の証明・証拠はあるに決まっているだろうから、最後のフィールドも“あらずもがな”なので省略します。
$`\quad (\lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}) )`$
長さ 1 のレコードになりました。長さ 1 のレコードは、その唯一のフィールド値と同一視可能なのでカッコは省略して：
$`\quad \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R})`$
このような省略により、もともと4つの構成素を宣言していた指標 $`\mrm{Injection}`$ の実例として、裸のラムダ式だけの $`\lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R})`$ が実例だと主張できることになります。
定義や宣言と、その実例の形式にズレがあって辻褄があってないときは省略がされているのです。
指標の名前、型の名前、集合の名前
前節で出てきた指標の名前 $`\mrm{Injection}`$ は、いったい何に付けられた名前でしょうか？ もちろん、指標に付けられた名前ですが、指標は構文的対象物〈syntactic object〉で、指標が記述するセマンティクスがあります。指標の名前とは、指標が記述するセマンティクスに付けた名前とも解釈できます。
型理論で言えば、指標は複合型（より正確に言えば依存レコード型）を定義します。つまり、型理論的には、指標のセマンティクスは型です。型の実例を集めると集合になります。集合論的には、指標のセマンティクスは実例達の集合です。
名前 $`\mrm{Injection}`$ の解釈の可能性として：
- 名前 $`\mrm{Injection}`$ は、構文的対象物に付けられた名前である。
- 名前 $`\mrm{Injection}`$ は、型に付けられた名前である。
- 名前 $`\mrm{Injection}`$ は、集合に付けられた名前である。
ひとつの名前を3つのモノにオーバーロード〈多義的使用〉するのは辛い！ 次の約束にしましょう。
- 指標の名前は型の名前と考える。ここはオーバーロード。
- 指標の名前を集合の名前とは考えない。オーバーロードしない。
指標／型の名前から集合を作るには、「指標とヒルベルト・イプシロン記号を利用しよう」で導入した $`\ClassOf{\hyp}`$ を使います。
- 名前 $`\mrm{Injection}`$ は、指標の名前である。
- それと同時に、名前 $`\mrm{Injection}`$ は型の名前でもある。
- $`\ClassOf{\mrm{Injection}}`$ は、型 $`\mrm{Injection}`$ の実例の集合を表す。
型理論では、$`x`$ が 型 $`T`$ の実例であることを $`x:T`$ と書くのですが、コロンは他の用法もあって混乱のリスクがあるので、コロンとまったく同義ですが、次も使います。
- $`x \text{ is-a }T`$
- $`x \text{ inhabits }T`$
inhabits〈居住する〉という語を使う事情は、「実用圏論： 2-圏、居住関係、プロファイリング」を見てください。
今の事例で言うと、以下の書き方はすべて同義です。
- $`(\mbf{Z}, \mbf{R}, \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}), 👌) \text{ is-a } \mrm{Injection}`$
- $`(\mbf{Z}, \mbf{R}, \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}), 👌) \text{ inhabits } \mrm{Injection}`$
- $`(\mbf{Z}, \mbf{R}, \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}), 👌) : \mrm{Injection}`$
- $`(\mbf{Z}, \mbf{R}, \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}), 👌) \in \ClassOf{\mrm{Injection}}`$
書き方が違うだけで同じです。
ここで、集合 $`\ClassOf{\mrm{Injection}}`$ に名前〈固有名〉を与えましょう。
$`\quad \mrm{Inj} := \ClassOf{\mrm{Injection}}`$
これで、この時点での名付けの状況は以下のように変わります。
- 名前 $`\mrm{Injection}`$ は、指標の名前である。
- 名前 $`\mrm{Injection}`$ は、型の名前でもある。
- 名前 $`\mrm{Inj}`$ は、集合の名前である。
次の書き方もできるようになりました。
- $`(\mbf{Z}, \mbf{R}, \lambda\, n\in \mbf{Z}.(2n\; \in \mbf{R}), 👌) \in \mbf{Inj}`$
述語の名前
単射であることを表す述語（関数の特別なモノ）は、次のラムダ式で書けました。
$`\quad \lambda, f \in \mbf{Set}(X, Y).\, [\forall x, x'\in X.\, \mrm{eq}_Y(f(x), f(x')) \Imp \mrm{eq}_X(x, x')]\\
\qquad : \mbf{Set}(X, Y) \to |\mbf{Logic}| \In \mbf{SET}
`$
この述語（である関数）に名前を付けましょう。実際は、集合 $`X, Y`$ ごとに関数が在るので次のような命名になります。
$`\text{For }X, Y \in |\mbf{Set}|\\
\quad \text{is-injective}_{X, Y} := \\
\qquad \lambda, f \in \mbf{Set}(X, Y).\, [\forall x, x'\in X.\, \mrm{eq}_Y(f(x), f(x')) \Imp \mrm{eq}_X(x, x')]\\
\quad : \mbf{Set}(X, Y) \to |\mbf{Logic}| \In \mbf{SET}
`$
$`X, Y`$ ごとに述語が決まるので、次のような状況です。
$`\quad |\mbf{Set}|^2 \ni (X, Y) \mapsto \text{is-injective}_{X, Y} \in \mbf{SET}(\mbf{Set}(X, Y), |\mbf{Logic}|)`$
つまり、下付きの $`X, Y`$ がない $`\text{is-injective}`$ は、以下のごとくパイ型（の集合）に所属しています。
$`\quad \text{is-injective} \in \prod_{(X, Y)\in |\mbf{Set}|^2} \mbf{SET}(\mbf{Set}(X, Y), |\mbf{Logic}|)`$
$`\text{is-injective}_{X, Y}(f)`$ は次のように書いても同じ（書き方の変更だけ）です。
$`\quad \text{is-injective}_{X, Y}(f) \\
= \text{is-injective}( (X, Y), f ) \\
= \text{is-injective}( ((X, Y), f) )
`$
$`((X, Y), f)`$ は、次のごとくシグマ型（の集合）に所属しています。
$`\quad ((X, Y), f) \in \sum_{(X, Y)\in |\mbf{Set}|^2} \mbf{Set}(X, Y)`$
なので、関数 $`\text{is-injective}`$ のプロファイルは次のようにも解釈できます。
$`\quad \text{is-injective} :
\sum_{(X, Y)\in |\mbf{Set}|^2} \mbf{Set}(X, Y) \to |\mbf{Logic}| \In \mbf{SET}
`$
たくさんの名前を準備するのは鬱陶しいので、ひとつの名前 $`\text{is-injective}`$ を場面ごとにちょっとずつ違った意味で使うのが現実的でしょう。この運用法は、オーバーロードというより、コアージョン（「曖昧性を減らす： Diag構成を事例として // 具体例、記号の乱用、コアージョン」参照）を前提とした名前の運用法です。
$`\text{is-injective}(X, Y, f)`$ という、3つの引数をフラットに並べて渡すことも許す（意味は変わらず）とすると、例えば、$`\mrm{Injection}`$ の指標は次のように書けます。
signature $`\mrm{Injection}`$ {
$`X \in |\mbf{Set}|`$
$`Y \in |\mbf{Set}|`$
$`f: X \to Y \In \mbf{Set}`$
$`\text{injectivity} : \mbf{1} \to \text{is-injective}(X, Y, f) \In \mbf{Logic}`$
}
論理式を繰り返し書く必要がなくなるので、記述が楽になります。
名前の種別
ここまで、数式のなかで使う名前、つまりシンボルとして
$`\quad \mrm{Injection}`$
$`\quad \text{injectivity}`$
$`\quad \mbf{Inj}`$
$`\quad \text{is-injective}`$
という4つの名前が登場しました。そろぞれの名前の意味と運用法について説明しました。
これらのシンボル（LaTeXコードで表現される名前）に対して、管理名（「デジタル語彙目録:: 名前の管理」参照）としてプレーンテキストの名前も与えます。例えば次のように決めます。
| $`シンボル`$ | テキストの名前 |
用語（日本語） |
|---|---|---|
| $`\mrm{Injection}`$ | Injection |
単射 |
| $`\text{injectivity}`$ | injectivity |
単射性 |
| $`\mbf{Inj}`$ | Inj |
単射の集合 |
| $`\text{is-injective}`$ | is-injective |
単射である |
テキストの名前は、名前空間ツリーに配置されてソフトウェアにより管理されるとします。名前の種別は次のようです。
- 名前
Injection： 指標の名前、型の名前と解釈 - 名前
injectivity： 指標のなかの構成素宣言のラベル名、証明・証拠の名前と解釈 - 名前
Inj： 集合の名前 - 名前
is-injective： 述語の名前、プロファイルの違いによる多義性はコアージョンで実現
名前を正確に使うということは、概念を精密に分析して記述することに繋がります。
*1:含まれてなきゃないで、別にかまわないのですけどね。
