ひとつ前の記事「Propositions-As-Typesを曲解しないで理解するために」の最初の節や最後の節で、同義語・曖昧多義語を話題にしました。
曖昧さは色々な形で現れます。なにごとかを正確に理解するには、曖昧さを処理していくことが必要です。まー、曖昧に書く・言うほうが悪いのですが、曖昧さのない表現は至難の業です。発信側は曖昧性の少ない表現につとめ、受信側〈解釈側〉は曖昧性の解決につとめることが必要となります。
単に「努力しよう」では精神論になってしまうので、工夫と道具について考えます。$`\newcommand{\mrm}[1]{\mathrm{#1} }
%\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mbf}[1]{\mathbf{#1} }
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
\require{color}
\newcommand{\format}[1]{\textcolor{blue}{\text{#1}}}
`$
内容：
曖昧さ
曖昧多義語では、ひとつの言葉に対して、指す対象物〈モノ〉がたくさんあります。同義語では、モノ（概念的事物かも知れない）に対してそれを指す言葉がたくさんあります。たくさんの候補〈選択肢〉があるので、それらからひとつ選択する作業が発生します。曖昧多義語においては、当該文脈における意味の決定が（解釈側の）選択行為； 同義語においては、当該文脈における適切な表現の決定が（発信側の）選択行為です。
言葉だけではなくて、書き方〈notation〉でも曖昧性はあります。例えば、$`f`$ が $`\mbf{R}\to\mbf{R}`$ という関数だとして、右肩に小さく $`-1`$ を乗せた書き方 $`f^{-1}`$ の意味・用法はたくさんあります。
- 逆関数（$`f`$ が可逆なとき）
- 点〈要素〉の逆像
- 部分集合の逆像
- 逆数関数（$`f`$ の値がゼロにならないとき）
- 部分関数〈partial function〉と考えた逆数関数
1から5のそれぞれの用法に対する定義を書き下すと次のようです。
$`\text{case 1}\\
\quad f^{-1} : \mbf{R} \to \mbf{R}\\
\quad \text{where }f^{-1}(y) = x \Iff f(x) = y\\
\text{case 2}\\
\quad f^{-1} : \mbf{R} \to \mrm{Pow}(\mbf{R})\\
\quad f^{-1} := \lambda\, y\in \mbf{R}. \{x\in \mbf{R}\mid f(x) = y \}\\
\text{case 3}\\
\quad f^{-1} : \mrm{Pow}(\mbf{R}) \to \mrm{Pow}(\mbf{R})\\
\quad f^{-1} := \lambda\, Y\in \mrm{Pow}(\mbf{R}). \{x\in \mbf{R}\mid f(x)\in Y \}\\
\text{case 4}\\
\quad f^{-1} : \mbf{R} \to \mbf{R}\\
\quad f^{-1} := \lambda\, x\in \mbf{R}. \frac{1}{f(x)}\\
\text{case 5}\\
\quad f^{-1} : \mbf{R} \to \mbf{R}\cup \{\bot \}\\
\quad f^{-1} := \lambda\, x\in \mbf{R}.(\text{if } f(x) \ne 0 \text{ then }\frac{1}{f(x)}
\text{ else } \bot)
`$
例えば、逆関数の微分公式を次の形に書いたとき、用法その1〈case 1〉と用法その4〈case 4〉が混じっています。
$`\quad (f^{-1})' = (f'\circ f^{-1})^{-1}`$
もうひとつよく使う $`f^{-1}`$ の用法がありました。一点の逆像とほぼ同じなんですが、逆像を部分集合（ベキ集合の要素）ではなくて、集合の宇宙（$`|\mathbf{Set}|`$）の要素とみる場合です。この場合のプロファイルは：
$`\quad f^{-1} : \mathbf{R} \to |\mathbf{Set}| \text{ in } \mathbf{SET}`$
つまり、実数の集合をインデキシング集合とする集合族〈indexed family of sets〉です。
一点の逆像をファイバーとも呼ぶので、これは、関数〈写像〉 $`f`$ のファイバー・ファミリーと呼ぶと紛れが少ないでしょう。僕は、ファイバー・ファミリーに $`f^{-1}`$ は使わず（あまりにも多義的過ぎるので）、$`f_{@}`$ を使っています。が、世間的多数派は $`f^{-1}`$ です。
[/追記補足]
フォーマット、言語
画像ファイルというのは、結局のところはビット列に過ぎません。これは何も画像に限らず、どんなファイル（デジタルデータ）もビット列なわけですが、特に画像ファイルに注目しましょう。
単なるビット列をどうして我々は視覚的に認識できるのかというと、ビット列を視覚化するやり方が約束として決まっているからです。ビット列の画像としての解釈の約束は画像フォーマット〈graphics {file}? format〉と言います。JPEG、PNG、GIF、WebP などの画像フォーマットはよく知られています。
画像ファイルがあるとき、その画像フォーマットはファイル名拡張子で判断できます。皆さんそうしていると思います。HTTPでデータを転送するときは、メタデータとして、Content-TypeヘッダーにMIMEメディアタイプが指定されます。例えば次のようです。
Content-Type: image/jpeg
ファイル名もメタデータもないときは、ビット列のパターン（特に先頭部分）を見て推測するしかないです。「16進ダンプを見ておまえが推測しろ」と言われるとけっこう困ります（慣れていると出来たりしますが）。
別な話として、日本語と英語とフランス語とドイツ語が混じった文章があったとします。語学が達者な人は、どの部分がどの言語で書かれているかを判断できるでしょうが、僕は、日本語とそれ以外の区別しか出来そうにありません。語学が達者な人でも、一単語、二単語だけを出されると、何語かの判断は難しいでしょう。例えば、「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」」で出した "habitat" はフランス語でも英語でも綴りは同じです。発音は違うでしょう、フランス語だと "h" は発音しないのかな。
画像フォーマットでも自然言語テキストでも、メタデータなしに短いデータ（データの一部）を見せられると、ナンダカヨクワカラナイとなります。
関数を記述するフォーマット
中学・高校の習慣では、2次関数を次のように記述します。
$`\quad y = x^2 + 1`$
これは等式です。等式なので、方程式とも解釈できます。実際、同じ等式が、別な場面では放物線（図形）の方程式として登場します。文脈（あるいはメタデータ）なしでは、それが記述しているモノが関数だか図形だかわかりません。
ラムダ項〈lambda term〉による関数の表現なら、上記の2次関数は次のように書けます。
$`\quad \lambda\, x\in \mbf{R}.\, x^2 + 1`$
図形の方程式だと誤解されるリスクはありませんが、メタデータとしてプロファイル（関数の域と余域）は書いておいたほうがいいでしょう。
$`\quad f: \mbf{R} \to \mbf{R}\\
\quad f := \lambda\, x\in \mbf{R}.\, x^2 + 1
`$
関数を記述するために、等式を使うかラムダ項を使うかは、フォーマット（あるいは言語、構文）の選択の問題です。どれかひとつに決めろ、というのは難しいし、理不尽でもあるので、どんなフォーマットを使ってもいいとしましょう。ただし、MIMEメディアタイプのようなメタデータにより、どのフォーマットを使っているかを明示することにします。
例えば、次のような書き方はどうでしょう。青い文字列は、フォーマットの名前です。
高校方式：
$`\quad f: \mbf{R} \to \mbf{R}\\
\quad f := \\
\quad \text{expression in }\format{high-school-style-function-def}\\
\qquad y = x^2 + 1\\
\quad \text{ end}
`$
ラムダ項：
$`\quad f: \mbf{R} \to \mbf{R}\\
\quad f := \\
\quad \text{expression in }\format{lambda-term}\\
\qquad \lambda\, x\in \mbf{R}.\, x^2 + 1\\
\quad \text{ end}
`$
日本語：
$`\quad f: \mbf{R} \to \mbf{R}\\
\quad f := \\
\quad \text{expression in }\format{informal-Japanese}\\
\qquad \text{二乗して 1 を足す}\\
\quad \text{ end}
`$
等式で放物線を記述するなら、同じ式ですが記述フォーマットの指定を変えます。
$`\quad P\subseteq \mbf{R} \times \mbf{R}\\
\quad P := \\
\quad \text{expression in }\format{high-school-style-subset-def}\\
\qquad y = x^2 + 1\\
\quad \text{ end}
`$
割と多くのケースで、プロファイルやフォーマットのようなメタデータが、暗黙の文脈に隠されるので、暗黙の文脈がうまく読み取れないとナンダカヨクワカラナイとなるのでしょう。暗黙の情報を明示化する書き方は必要だと思います。
型を記述するフォーマット
とりあえず、「型とは集合だ〈types as sets / sets as types〉」と考えることにして、$`\mbf{N}`$ は自然数の型、$`\mbf{String}`$ は文字列の型だとします。次の表現が、なにかしらの複合的型を定義しているとして、解釈できるでしょうか？
$`\quad (\\
\qquad (a, \mbf{N}),\\
\qquad (b, \mbf{String})\\
\quad )
`$
「たぶん ～～ かなー？」という程度の推測しか出来ませんよね。しかし、次のように書くと、推測が容易で、推測に確信も持てるでしょう。
$`\quad (\\
\qquad (\text{age}, \mbf{N}),\\
\qquad (\text{mail-address}, \mbf{String})\\
\quad )
`$
データベースについて知識を持っているなら「これは、$`\text{age}, \text{mail-address}`$ という2つのカラムを持つテーブルスキーマのようなもんだろう」と推測できます。が、その推測と確信の根拠は $`\text{age}, \text{mail-address}`$ という2つの名前の英語辞書的意味です。実際とのところ、そういう推測はよくするのですが、ヨクナイヨナー。
名前を次のように変えたらどうでしょう？
$`\quad (\\
\qquad (\text{id-number}, \mbf{N}),\\
\qquad (\text{mail-address}, \mbf{String})\\
\quad )
`$
同じ推測をするかも知れませんが、「人を一意に特定する情報として、ID番号またはメールアドレスを使う」ってことかも知れません。
実は、複合的型としてのパイ型とシグマ型は似たような形になりがちです（どちらも型ファミリーを素材として作る型だからです）。パイ型は、もっと馴染みがある言い方をすれば構造体型とかレコード型です。シグマ型は、タグ付きユニオン型といえば少し分かりやすいでしょう。
見た目は同じ式を使うとして、構造体型／レコード型を定義する形式なら $`\format{record-type-def}`$ 、タグ付きユニオン型を定義する形式なら $`\format{tagged-union-type-def}`$ とします。構造体型／レコード型なら、2つのフィールドのどちらも必要です。タグ付きユニオン型なら、2つの選択肢〈case | option〉のどちらか一方だけのデータとなります。
構造体型／レコード型を定義：
$`\quad \text{type }\text{Person} := \\
\quad \text{expression in }\format{record-type-def}\\
\quad (\\
\qquad (\text{age}, \mbf{N}),\\
\qquad (\text{mail-address}, \mbf{String})\\
\quad )\\
\quad \text{ end}
`$
タグ付きユニオン型を定義：
$`\quad \text{type }\text{Person} := \\
\quad \text{expression in }\format{tagged-union-type-def}\\
\quad (\\
\qquad (\text{id-number}, \mbf{N}),\\
\qquad (\text{mail-address}, \mbf{String})\\
\quad )\\
\quad \text{ end}
`$
もちろん、フォーマット指定だけでなくて、区切り記号／囲み記号を“それらしく”して誤認を避けるような工夫も併用すべきでしょう。
構造体型／レコード型を定義：
$`\quad \text{type }\text{Person} := \\
\quad \text{expression in }\format{record-type-def}\\
\quad \{\\
\qquad \text{age} : \mbf{N},\\
\qquad \text{mail-address} : \mbf{String}\\
\quad \}\\
\quad \text{ end}
`$
タグ付きユニオン型を定義：
$`\quad \text{type }\text{Person} := \\
\quad \text{expression in }\format{tagged-union-type-def}\\
\quad (\\
\qquad \text{id-number} \Rightarrow \mbf{N}\\
\qquad |\, \text{mail-address}\Rightarrow \mbf{String}\\
\quad )\\
\quad \text{ end}
`$
法則を記述するフォーマット
次のような二項演算 $`m`$ があるとします。
$`\quad m : A\times A \to A \text{ in }\mbf{Set}`$
$`m`$ が可換であることを幾つかの記述フォーマット〈記述構文 | 記述言語〉で書いてみましょう。
古典論理の論理式：
$`\text{expression in }\format{classical-logic}\\
\quad \forall x, y\in A.\, m(x, y) = m(y, x)\\
\text{end}
`$
圏論的等式（等式を2-射と解釈）：
$`\text{expression in }\format{categorical-equation}\\
\quad \mrm{comm} :: m \Rightarrow \sigma_{A, A} ; m : A\times A \to A \text{ in }\mbf{Set}\\
\text{end}
`$
可換図式：
$`\text{expression in }\format{commutative-diagram}\\
\quad \xymatrix{
{A\times A} \ar[r]^{\sigma_{A, A}} \ar[d]_m
&{A\times A} \ar[d]^m
\\
A \ar@{=}[r]
& A
}\\
\quad \text{commutative in }\mbf{Set}\\
\text{end}
`$
ペースティング図（「構造記述のための指標と名前 1/n 基本 // 図式による法則の記述」参照）：
$`\text{expression in }\format{pasting-diagram}\\
\quad \xymatrix{
{A\times A} \ar[r]^{\sigma_{A, A}} \ar[d]_m
\ar@{}[dr]|{\underset{\nearrow}{=}}
&{A\times A} \ar[d]^m
\\
A \ar@{=}[r]
& A
}\\
\quad \text{in }\mbf{Set}\\
\text{end}
`$
書き方の違いは、背後の発想の違いを反映はしているのですが、でも、言いたいことは同じです。事実は語り方に依存しないのです。どのような言葉・絵図でどのように語ろうが、言いたいことは同じです。
おわりに
暗黙の文脈から情報を読み取るスキルは重要なんですが、とはいえですね、あまりにも多くの情報が暗黙化されると解釈側の負担が大きくなってシンドイってこともあります。今日述べた工夫は実はひとつだけで、記述フォーマット〈記述構文 | 記述言語〉が何であるかを明示的に書いたらいいよ、ってことです。
$`\quad \text{expression in }\format{フォーマット}\\
\qquad \text{ナンタラカンタラ}\\
\quad \text{end}
`$
これだけでも、誤解・曲解を避けるために、かなりの効果を見込めると思います。
