去年「指標から名前の削除」という短い記事を書きましたが、その続きです。名前の削除に関して、いつだったかどこかで見た方法を紹介します。“いつどこか”を忘れてしまったので出典不明です。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\In}{ \text{ in } }
\newcommand{\id}{\mathrm{id} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\T}[1]{\text{#1} }
`$
「指標から名前の削除」から、名前を削除した指標を再掲します。
$`\T{signature }\T{Semigroup} \:\{\\
\quad \_ \In \mbf{Set}\\
\quad \_ : a1\times a1 \to a1 \In \mbf{Set}\\
\quad \_ ::
(a2\times \id_{a1}); a2 \twoto \alpha_{a1,a1,a1} ; (\id_{a1} \times a2); a2
\In \mbf{Set}\\
\}
`$
集合圏で考えるのを前提とすると、$`\In \mbf{Set}`$ はすべて省略できます。念の為、アンダースコアの後に番号を添えます。すると：
$`\T{signature }\T{Semigroup} \:\{\\
\quad \_1 \\
\quad \_2 : a1\times a1 \to a1\\
\quad \_3 ::
(a2\times \id_{a1}); a2 \twoto \alpha_{a1,a1,a1} ; (\id_{a1} \times a2); a2\\
\}
`$
これと同じ内容を、3カラムの表〈テーブル〉の形に書きます。3つのカラム〈欄〉は、番号、ラムダ式、ラムダ式への引数指定です。
$`\begin{array}{|l|l|l|}
\hline
1 & &
\\
2 & \lambda\, X.\, [X\times X, X] & 1
\\
3 & \lambda\,(X, f).\, \left( (X\times \id_X); f = \alpha_{X,X,X} ; (\id_{X} \times f); f \right)
& 1, 2
\\
\hline
\end{array}
`$
第二カラム（中央）のラムダ式は型付きラムダ式ですが、型宣言／型注釈は省略して、次の約束がされているとします。
- $`X`$ は集合を表す変数、$`f`$ は関数を表す変数
ラムダ抽象の形をしたラムダ式は、型構成子、命題構成子になっています。第三カラム〈左〉の引数を適用すると、ベータ変換によりラムダ記号 $`\lambda`$ は消えます。ただし、番号そのものを代入すると奇妙なので、接頭辞 $`a`$ を付けてベータ変換の計算をしてみます。イコールを使うと混乱しそうなところは $`\twoto`$ を使っています。
$`\quad (\lambda\, X.\, [X\times X, X])(a1)\\
\twoto [a1 \times a1 , a1]\\
\:\\
\quad (\lambda\,(X, f).\, \left( (X\times \id_X); f = \alpha_{X,X,X} ; (\id_{X} \times f); f \right) )(a_1, a_2)\\
\twoto (a1\times \id_{a1}); a_2 = \alpha_{a1,a1,a1} ; (\id_{a1} \times a2); a2
`$
テーブルの各行を、臨時の名前 $`a1, a2`$ を使って書けば：
- $`a1`$
- $`a2 : [a1 \times a1 , a1]`$
- $`a3 : (a1\times \id_{a1}); a_2 = \alpha_{a1,a1,a1} ; (\id_{a1} \times a2); a2`$
ここでのコロンは、圏論のプロファイル・コロンではなくて、型理論の居住関係〈inhabitation relation〉のコロンです。居住関係のコロンは、集合論と論理をミックスして解釈します。
- $`a1`$ は、集合（宇宙の要素）である。
- $`a2`$ は、コロンの右の集合の要素である。
- $`a3`$ は、コロンの右の命題の証明である。
テーブルの罫線をやめて、行列風に書くことにして、入れ子の名前無し指標を書いてみます。以下は、半群の指標を埋め込んだモノイドの指標です。
$`\begin{bmatrix}
1 & \begin{bmatrix}
1 & &
\\
2 & \lambda\, X.\, [X\times X, X] & 1
\\
3 & \lambda\,(X, f).\, (X\times \id_X); f = \alpha_{X,X,X} ; (\id_{X} \times f); f
& 1, 2
\end{bmatrix}
&
\\
2 & \lambda\, X.\, [\mbf{1}, X]
& 1.1
\\
3 & \lambda\,(X, f, e).\, (e\times \id_X) ;f = \ell_X
& 1.1, 1.2, 2
\\
4 & \lambda\,(X, f, e).\, (\id_X \times e) ;f = r_X
& 1.1, 1.2, 2
\end{bmatrix}
`$
左単位律子〈left unitor〉がラムダ記号とかぶるので、単位律子は $`\ell, r`$ としました。$`1.1, 1.2`$ などは、入れ子の内側の構成素を参照するためのパス式です。入れ子がいくら深くなってもパス式で構成素にアクセスできます。
この書き方から、指標を書くのに名前は不要なのがハッキリとわかるでしょう。ラムダ式では名前を使ってますが、使っている名前はラムダ変数（例： $`X, f, e`$ ）か外部で定義済みの名前（例： $`\mbf{1}, \ell, r`$）です。ラムダ変数はアルファ変換〈リネーミング〉でいかようにでも変えることが出来るし、なんならド・ブラウン・インデックス（「ラムダ式のド・ブラウン・インデックス」参照）でラムダ変数を消してしまってもいいです。
外部で定義済みの大域的名前にしろ、合意された番号や番号パスを使って参照してもかまいません。
なぜにここまで名前の削除にこだわるのかと言うと、人は名前に意味を込める行為をしてしまうからです。それをやられると、構文論と意味論の議論が台無しになってしまいます。番号もある種の名前〈識別子〉ですが、意味を込める行為を防止できます。
また、番号は明示的に書かなくても、リスト内の出現位置で代用できます。そして番号は、コンピュータの内部では扱いやすいというメリットもあります。
