オーバーロード解決のために、振り仮名風アノテーション - 檜山正幸のキマイラ飼育記 (はてなBlog)

ここ数年、オーバーロード（言葉・記号の多義的使用）の問題にひどく悩まされています。僕ひとりの問題というよりは、コミュニケーションの障害となるので困っているのです。

言葉・記号をオーバーロードしてしまうと、オーバーロード解決（曖昧性をなくして一義化すること）には何らかの付加情報が必要です。この付加情報は、多くの場合、暗黙の前提とか以心伝心みたいになっていて、共通前提・共通スキルを持ってないコミュニケーション参加者に誤解・混乱・ストレスを与えます。

文字コミュニケーション（音声コミュニケーションではない）の場合に限りですが、オーバーロード解決の手段を考えてみます。

内容：

一休さんと逆ルビ
タイプアノテーションを振り仮名風に
幾つかの例
おわりに

ほのめかし

一休さんと逆ルビ

「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」という記事で、オーバーロードの例として、一休さんのトンチの話をしました。一休さんは、「このハシわたるべからず」という文内の語「ハシ」の曖昧性（同音異義語の存在）を利用して、橋の真ん中を渡った、という逸話です。

この場合、「橋」と「端」は、同音異義語です。したがって、読み〈音〉「ハシ」が与えられても、その意味を一意的に決定できません。「ハシ」の曖昧性を除去する（オーバーロードを解決する）ために、“逆ルビ”（すぐ後で説明）を使ってみます。

このハシ（橋）わたるべからず

通常のルビ（振り仮名付け）は、「橋（ハシ）」「端（ハシ）」のように使いますが、親文字〈ruby base〉と振り仮名〈ruby text〉を逆にします。逆ルビでは、読みを親文字として、意味〈語義〉を示す情報を振り仮名として添えます。

逆ルビの例をもう少し。振り仮名は小さな文字になるので、目を凝らして見てください。

ニハ（庭）ニハニハ（二羽）、ウラニハ（裏庭）ニハニハ（二羽）、ニハトリ（鶏）
ここではきもの（履物）を脱いでください。
ここではきもの（着物）を脱いでください。

タイプアノテーションを振り仮名風に

掛け算と足し算に関する分配法則を等式で書けば次のようになります。

a(x + y) = ax + ay

アルファベット先頭の小文字'a'を別な文字'f'に置き換えます。

f(x + y) = fx + fy

アルファベット文字の置き換えが、記述している法則の内容に影響を与えるとは思えません。しかし、文字'f'を使うと「んっ？ fは関数かな？」とか思います。すぐ上の等式は、関数〈写像〉fの線形性を主張しているような気がしなくもない雰囲気がただよいます。

上記の等式を書いた当人が、文字'f'により関数〈写像〉を意図している場合、このテのコミュニケーション手法を僕は“ほのめかし”と呼んでいます。相手（解釈者）が、“ほのめかし”に敏感に反応できればコミュニケーションが成立し、そうでないならコミュニケーションは失敗します。失敗のリスクが大きい“ほのめかし”を僕はやめたいんだよ！

分配法則の場合、文字 a, x, y のタイプは、a∈R, x∈R, y∈R です（実数の話をしている前提で）。一方、fの線形性を述べたいなら、f:V→W, x∈V, y∈V （V, Wはベクトル空間）となるでしょう。この事情をハッキリさせるために、文字のタイプ情報〈type informtion〉を逆ルビと同様なレイアウトで付加してみます。

$\overset{\in {\bf R}}{a}(\overset{\in {\bf R}}{x} + \overset{\in {\bf R}}{y}) = \overset{\in {\bf R}}{a}\,\overset{\in {\bf R}}{x} + \overset{\in {\bf R}}{a}\,\overset{\in {\bf R}}{y} \\ \:\\ \overset{V \to W}{f}(\overset{\in V}{x} + \overset{\in V}{x}) = \overset{V \to W}{f}\, \overset{\in V}{x} + \overset{V \to W}{f}\, \overset{\in V}{y} \\$

所属記号'∈'は、省略してもいいでしょう。関数の適用〈application〉は、右から左への方向（反図式順）なので、矢印も逆向きのほうが自然に感じるでしょう。

$\newcommand{\from}{\leftarrow}% % \overset{{\bf R}}{a}(\overset{ {\bf R}}{x} + \overset{ {\bf R}}{y}) = \overset{ {\bf R}}{a}\, \overset{ {\bf R}}{x} + \overset{ {\bf R}}{a}\, \overset{ {\bf R}}{y} \\ \:\\ \overset{W \from V}{f}(\overset{ V}{x} + \overset{ V}{x}) = \overset{W \from V}{f}\, \overset{ V}{x} + \overset{W \from V}{f}\, \overset{ V}{y} \\$

TeX（このブログではMathJax）による数式レンダリングにおいては、ルビ〈振り仮名〉風のレイアウトに \overset コマンド〈コントロールシーケンス〉を使っています。

毎回タイプ情報をルビで添えるのは煩雑に過ぎますが、“ほのめかし”を使いたいタイミングで、せめて最初の一回はルビでタイプ情報を注釈〈アノテート〉すれば、“ほのめかし”による誤解・混乱・ストレスを削減・軽減できると思います。

幾つかの例

図式順／反図式順による適用／結合〈合成〉の書き方は次のようになります（檜山の流儀）。

	図式順	反図式順
適用	$x.f$	$f(x)$
結合	$f;g$	$g\circ f$

これを、タイプアノテーション付きで書けば分かりやすさが向上するでしょう。

	図式順	反図式順
適用	$\overset{A}{x}.\overset{A \to B}{f}$	$\overset{B \from A}{f}(\overset{A}{x})$
結合	$\overset{A \to B}{f};\overset{B \to C}{g}$	$\overset{C \from B}{g}\circ \overset{B \from A}{f}$

「関手と自然変換の計算に出てくる演算子記号とか」で「酷い話だなー」と嘆いたような、演算子記号なしの併置がいきなり出てくると、ほんとに困ります。併置"εη" を次のようにタイプアノテーション付きで書いてもらえば判読可能になります。

$\overset{H \Leftarrow G}{\epsilon} \; \overset{G \Leftarrow F}{\eta}$

この場合、矢印の向きから反図式順記法だとわかります。η::F⇒G, ε::G⇒H なので、演算子記号なしの併置は自然変換の縦結合だと推測できます。

最初のお約束として、あるいは、紛らわしい場面での補足情報としてタイプアノテーションを付けてもらえれば助かりますよね。矢印の向きで、図式順／反図式順も分かります。

もうひとつ、 $\frac{\partial}{\partial x}$ の解釈の例を挙げましょう。これは、「さまざまな関手／オペレータと微分の表示」の最後で触れた例です。多様体上の微分の知識が必要なので、ご存知なければ無視してください。

$\frac{\partial}{\partial x} f$ または $\frac{\partial}{\partial x}\cdot f$ の3種類の用法を、次のようにアノテーションで区別します。

$\overset{C^\infty({\bf R}^2) \leftarrow C^\infty({\bf R}^2)}{\frac{\partial}{\partial x}} \;\overset{C^\infty({\bf R}^2)}{f} \\$
$\overset{C^\infty(U)_m \leftarrow C^\infty(U)}{\frac{\partial}{\partial x}} \; \overset{C^\infty(U)}{f} \\$
$\overset{\Gamma_M(U, TM) \leftarrow C^\infty(U)^m}{\frac{\partial}{\partial x}} \,\cdot\, \overset{C^\infty(U)^m}{f} \\$

最初の例は、初等的な微分の話です。二変数関数 f を、第一方向（変数 x の方向）に偏微分しています。この意味での偏微分記号に、変数 x を付けるのは実はよろしくないことは「微分計算、ラムダ計算、型推論 // 何がダメなのか」を参照してください。

二番目の例のセッティングを述べます； Uは多様体M（dim(M) = m）上の開集合で、局所座標 x の定義域です x:M⊇U→R^m 。 $\frac{\partial}{\partial x}$ は、 $\frac{\partial}{\partial x} = (\frac{\partial}{\partial x^1}, \cdots, \frac{\partial}{\partial x^m})$ と、座標成分ごとの微分作用素を横に並べたものです。 $\frac{\partial}{\partial x}$ のプロファイル（域と余域）は $\frac{\partial}{\partial x}: C^\infty(U) \to C^\infty(U)_m$ で、 $C^\infty(U)_m$ は関数を横に並べたタプルの空間です（縦タプルと横タプルを区別します）。

以上の状況設定のもとで、二番目の $\frac{\partial}{\partial x} f$ は解釈可能だと思いますが、一番目の例とはだいぶ違います。でも、記号はオーバーロードされています。

次は三番目の例。ここでの $\frac{\partial}{\partial x}$ は、局所座標 x に伴うフレームを意味します（「接バンドルのホロノーム座標」の言葉で言えば、ホロノームフレームです）。 $\frac{\partial}{\partial x}$ は、 $\frac{\partial}{\partial x} = (\frac{\partial}{\partial x^1}, \cdots, \frac{\partial}{\partial x^m})$ なのは二番目の例と同じですが、各 $\frac{\partial}{\partial x^i}$ は局所ベクトル場と解釈されるので、 $\frac{\partial}{\partial x}$ は、m個のベクトル場を横に並べたタプルとみなし、さらには $\Gamma({{\bf R}^m}_U) \to \Gamma_M(U, TM)$ というセクション空間間の写像とみなします。ここで、R^m_U は、ファイバーがR^mであるU上の自明ベクトルバンドルです。

この状況に $\Gamma({{\bf R}^m}_U) \cong C^\infty(U)^m$ という同型をかますと、 $\frac{\partial}{\partial x} : C^\infty(U)^m \to \Gamma_M(U, TM)$ という解釈が可能となります。三番目の例の $\frac{\partial}{\partial x}$ は、f∈C^∞(U)^m に微分作用素として作用しているわけではないので、併置ではなくて中置演算子記号' $\cdot$ 'を入れています*1。当然ながら、一番目とも二番目ともまったく違います。

まったく違うものに、どうして同じ記号を使うのか？と僕に聞かれても困ります。実際に使っているから使うのだ、としか答えようがないです。多くの場合、オーバーロードされる記号には、なにかしらの共通点や関連性があります。しかし、オーバーロードがエスカレートすると、この共通点・関連性が希薄、ときに行方不明になってしまうこともあるのです。（それとは別に、まったくの偶然によるコンフリクトもあります。）

おわりに

オーバーロードや記号の乱用〈abuse of notation〉は、やめるわけにはいきません。現状、夥〈おびただ〉しく使われていますし、オーバーロード／記号の乱用なしで書くのは煩雑すぎて現実的じゃないです。

一方で、コミュニケーション参加者に誤解・混乱・ストレスを与えているのも事実です。折り合いをつけるひとつの方法として、オーバーロード解決のヒントをルビ風アノテーションとして付けるのはアリだと思います*2。対話的デジタルテキストにおいて、必要に応じてアノテーションを展開・折りたたみできたりすると使い勝手がよいと思いますが、非対話的〈静的〉テキストでもルビ風アノテーションはけっこうな効果があるでしょう。

*1:通常は、f を左側に書きますが、そうすると、行列計算との整合性がなくなります。

*2:「テンソル記法の「意味不明問題」は解決した」で採用した方法は、タイプアノテーション〈型情報注釈 | プロファイル情報注釈〉を、ルビ風レイアウトではなくて、右側上下添字で付加するものです。i, j が V, W のマーカーだとして、 $x^j_i = \overset{W \from V}{x}$ です。