このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

指標から名前の削除

指標は宣言文の集まりです。各宣言文は、順番〈位置番号〉でも名前でも一意識別できます。実用上は、(順番は覚えにくいので)名前が使われます。が、理論上は名前が邪魔になることがあるので、ときに、名前を削除する必要があります。

名前の削除方法の記述が意外に見つからないので、ここに記しておきます。事例で示します。$`\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 \T{sort } U \In \mbf{Set}\\
\quad \T{operationt } m : U\times U \to U \In \mbf{Set}\\
\quad \T{equation }\mrm{assoc} ::
(m\times \id_U); m \twoto \alpha_{U,U,U} ; (\id_U \times m); m
\In \mbf{Set}\\
\}
`$

このなかで、$`\mrm{assoc}`$ は、等号を集合圏の2-射とみなして書いた等式的法則です。以下の可換図式とまったく同じことです。

$`\quad \xymatrix{
(U\times U)\times U \ar[r]^{\alpha_{U,U,U}}
\ar[d]_{m \times \id_U}
& U\times (U\times U)
\ar[d]^{\id_U \times m}
\\
U\times U \ar[d]_{m}
& U\times U \ar[d]^{m}
\\
U \ar@{=}[r]
& U
}\\
\quad \text{commutative }\In \mbf{Set}
`$

指標内に出てくる名前 $`U, m, \mrm{assoc}`$ を、適当な接頭辞(ここでは文字 'a')と位置番号から作った $`a1, a2, a3`$ に置き換えます。すると:

$`\T{signature }\T{Semigroup} \:\{\\
\quad \T{sort } a1 \In \mbf{Set}\\
\quad \T{operationt } a2 : a1\times a1 \to a1 \In \mbf{Set}\\
\quad \T{equation } a3 ::
(a2\times \id_{a1}); a2 \twoto \alpha_{a1,a1,a1} ; (\id_{a1} \times a2); a2
\In \mbf{Set}\\
\}
`$

宣言文先頭のキーワードは無くてもいいので省略します。名前も位置番号(出現の順番)からわかるので省略、ただし構文の都合で場所取りのアンダースコアを書いておきます。すると:

$`\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}\\
\}
`$

接頭辞 'a' は別になんでもよくて、特に意味はありません。つまり、名前ではなくて位置番号 $`1, 2, 3`$ が識別子になっています。これで、名前は削除できました。

名前の削除は、しばしば暗黙に(なにも言わずに)行われます。「あれっ、名前はどうした?」と思ったら、暗黙に削除されたのかも知れません。名前を削除すると、指標のあいだのリネーム同値〈アルファ同値〉が等値〈イコール〉に変わります。名前の削除は、リネーム同値の同値類を取ることと同じ効果があります。

なお、名前の削除のためには、指標の宣言文のあいだに全順序〈total order〉が必要です。順番がなくて名前だけで識別されている場合は、名前の削除ができません。