---
tags: TrRun4
id: Theo-D03_monogusa.md
---
<style>
div.def {
border-left: 5px solid skyblue;
padding-left: 1em
}
</style>

# 檜山トレラン4 D03 モノグサ原則と混乱への対策

$\newcommand{\In}{\text{ in } }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\twoto}{\Rightarrow}
%
\require{color}%
\newcommand{\Keyword}[1]{ \textcolor{green}{ \bf \text{#1} } }%
\newcommand{\For}{\Keyword{For }}%
\newcommand{\Variable}{\Keyword{Variable }}%
\newcommand{\WeWillDefine}{\Keyword{WeWillDefine }}%
\newcommand{\WeDefine}{\Keyword{WeDefine }}%
\newcommand{\Justification}{\Keyword{Justification }}%
\newcommand{\WeAssert}{\Keyword{WeAssert }}
%$

書き言葉であれ話し言葉であれ、数学を語るときの大原則はモノグサ原則である。モノグサ原則への対策をしておかないと、混乱や誤解へと陥る。

関連する文書：

- [/2 B07 数学のための文法講座](https://hackmd.io/@m-hiyama/ryND05Bgu)

## モノグサ原則

数学は**モノグサ原則**で支配されている。モノグサ原則とは、次の2つの選択肢があったとき「2番目を選ぶべし」という原則である。

1. 省略せずに丁寧に書けば、明確で誤解が少なくなる。
2. 省略して雑に書けば、短く楽に書ける。

つまり、文脈から推測可能な情報は書かずに、読者（情報の受け手）の推測に“任せる”（あるいは“頼る”）。

しかし、読者が常にうまく推測できるとは限らない。推測に失敗すると混乱や誤解に陥る。モノグサ原則は弊害が大きい。

「諸悪の根源」とも言えるモノグサ原則だが、==極めて広く一般的に強く浸透している==ので、読者が混乱・誤解への対策をするしかない。

## 何が省略されるのか

よくある典型的な省略を挙げる。

1. ラムダ記号の省略
2. 限量子（特に全称限量子）の省略
3. 型／変域（の宣言）の省略
4. 引数の省略
5. 判断記号の省略
6. イプシロン記号の省略

これらの省略で引き起こされる混乱と、それへの対策を述べていく。

<!--
は：

1. 値と関数の混乱 ← ラムダ記号の省略
2. 真偽判断の混乱 ← 限量子の省略
3. 真偽判断の混乱 ← 型／変域の省略

命題と主張の混乱 ← 判断記号の省略
プロファイルと射の混乱 ← イプシロン記号の省略

空集合と単元集合の混乱 ← 引数値の省略

プロファイル
射
ホムセット

-->

## 値と関数の混乱

$x, y$ は実数変数だとして、裸の式 $x^2 + y + 1$ を考える。次のどちらが成り立つだろうか？

1. $x^2 + y + 1 \in {\bf R}$
2. $x^2 + y + 1 \in \mrm{Map}({\bf R}^2, {\bf R})$

何とも言えない、関数を表すラムダ記号（'$\lambda$'）を使えば明確になる。

$\For x, y\in {\bf R}\\
\WeAssert x^2 + y + 1 \in {\bf R}$

$\WeAssert \lambda\, (x, y)\in {\bf R}^2.(\, x^2 + y + 1 \;\in {\bf R}) \in \mrm{Map}({\bf R}^2, {\bf R})$

関数を表すラムダ式内で '$\in$' を使うと視認性が悪くなるのと、型理論／プログラミング言語などと習慣が合わないことから、'$\in$' の代わりにコロンを使ってもよい。

$\WeAssert \lambda\, (x, y): {\bf R}^2.(\, x^2 + y + 1 \;: {\bf R}) \in \mrm{Map}({\bf R}^2, {\bf R})$

ラムダ記号が省略されてしまう原因は、関数を表すラムダ式を書くのが==確かに面倒==だからだろう。思い切って簡略な書き方を採用しよう。

$\WeAssert \lambda[x^2 + y + 1] \in \mrm{Map}({\bf R}^2, {\bf R})$

ラムダ記号 '$\lambda$' を前置したブラケットで囲むだけ。負担が少ない。

ただし、ラムダ変数〈引数変数 \| ラムダ束縛変数〉の宣言がないと困ることがある。毎回変数の型宣言は面倒なので、事前にラムダ変数の宣言を書くことにする。CafeOBJ や Mizar で採用されている方式である。

$\Variable x, y:{\bf R}\\
\WeAssert \lambda[x^2 + y + 1] \in \mrm{Map}({\bf R}^2, {\bf R})\\
\WeAssert \lambda[x] \in \mrm{Map}({\bf R}, {\bf R})$

ラムダ変数の個別宣言は省略しているので、次の3つの区別はできなくなっている。まー、しゃーない、==諦めよう==。必要ならちゃんと書けばいい。

1. 恒等関数： $\lambda\,x:{\bf R}.(\, x\;:{\bf R}) \in \mrm{Map}({\bf R}, {\bf R})$
2. 第一射影関数： $\lambda\,(x, y):{\bf R}^2.(\, x\;:{\bf R}) \in \mrm{Map}({\bf R}^2, {\bf R})$
3. カリー化した第一射影関数：
$\lambda\,x:{\bf R}.(\, \lambda\, y:{\bf R}.(\, x\;:{\bf R})\; :\mrm{Map}({\bf R}, {\bf R}) ) \in \mrm{Map}({\bf R}, \mrm{Map}({\bf R}, {\bf R}))$

## 真偽判断の混乱

$(U, (*), e)$ がモノイドだとして、変数は $U$ 上の変数として次の等式を考える。

$\quad x * y = y * x$

「あ、交換法則だ」と反応するかも知れないが、これだけでは何とも言えない。交換法則を主張するには、全称限量子が必要で、別な限量子を付ければ別な意味になる。

1. $\forall x\in U.\,\forall y\in U.(\, x * y = y * x \,)$
2. $\forall x\in U.\,\exists y\in U.(\, x * y = y * x \,)$
3. $\exists x\in U.\,\forall y\in U.(\, x * y = y * x \,)$
4. $\exists x\in U.\,\exists y\in U.(\, x * y = y * x \,)$

$+$（足し算）、${^2}$（二乗）は半環の演算として常識的に解釈するとして、次は成立するだろうか？

$\quad \forall x, y.(\, (x + y)^2 = x^2 + y^2 \,)$

半環が何であるか、変数の変域を明示しないと何とも言えない。

1. 成立しない：$\forall x, y\in {\bf R}.(\, (x + y)^2 = x^2 + y^2 \,)$
2. 成立する：$\forall x, y\in \{0, 1\}.(\, (x + y)^2 = x^2 + y^2 \,)$ （半環演算はブール代数のものとする）

限量子が省略されてしまう理由もラムダ記号の省略と同じだろうから、これも負担が少ない略記を導入する。

$\Variable x, y:U\\
\WeAssert \forall[x * y = y * x]$

$\Variable x, y:\{0, 1\}\\
\WeAssert \forall[(x + y)^2 = x^2 + y^2]$

ラムダ記法の簡略化と同じく、述語（ブール値関数）の域やカリー化の情報などは失われるが、まー、しゃーない、==諦めよう==。必要ならちゃんと書けばいい。

## 命題と主張の混乱

高校くらいで「命題とは、真偽が判断できる文である」と習ったはず。「命題とは、正しい文である」とは==習ってない==はずだし、それは間違い。偽な命題も、もちろん在る。

だが、「命題 ＝ 正しい文」という用法は多い、数学書でさえ「定理 3.2」の代わりに「命題 3.2」と書いて、「命題」が正しい文であるかのごとき印象を強めている。

提示された文を即座に正しい文だと思いこむのは現実世界／日常生活でも極めて危険な行為だ。

- [フェイク情報に騙されないために](https://hackmd.io/@m-hiyama/ryND05Bgu#%E3%83%95%E3%82%A7%E3%82%A4%E3%82%AF%E6%83%85%E5%A0%B1%E3%81%AB%E9%A8%99%E3%81%95%E3%82%8C%E3%81%AA%E3%81%84%E3%81%9F%E3%82%81%E3%81%AB) 参照。命題を目にすることと、その命題が真であることはまったく別！

ファクトチェックの後で、「『～』という文は正しい」と述べるメタな文は<strong style="color:crimson">判断</strong>〈judgement〉とか<strong style="color:crimson">主張</strong>〈assertion〉とかステートメントと呼ぶ。「‥‥は正しい」に相当する記号は '$\vdash$' である。数理論理学では、 '$\vdash$' と '$\models$' を使い分け、厳しく区別しているが、我々はそこまで厳密な議論はしないので、'$\vdash$' だけを使い、この記法を<strong style="color:crimson">判断記号</strong>〈judgement symbol〉と呼ぶことにする。

「モノイドが可換である」と主張するには、$\forall x, y\in U.(\,x*y = y*x\,)$ でも不十分で、それが真であることまで言わなくてはならない。

$\quad \vdash \forall x, y\in U.(\,x*y = y*x\,)$

変数の型が事前に了解されているなら、次のように書くこともある。

$\quad \vdash \,x*y = y*x$

これは全称限量子の省略以外に、ラムダ記号の省略とも解釈できる。

$\quad \vdash \,\lambda\, x, y\in U.(\, x*y = y*x\,)$

ラムダ式が表すブール値関数が「正しい」とは、次のような2-射が存在することである。

$\quad \mrm{True}_X \twoto \lambda\, x, y\in U.(\, x*y = y*x\,) : U\times U \to {\bf B} \In {\bf Set}$

圏論的には、'$\vdash$' が '$\mrm{True}_X \twoto$' の略記だと思うと具合がいい。

多くの場合、「書いた／言った文は正しいことにしよう」という暗黙の了解のもとで、「‥‥は正しい」は省略する。この習慣が悪いわけではないが、「‥‥は正しい」まで含めて定式化や分析をする必要がある場面も多い。命題と主張〈判断〉を区別できない／ゴッチャにするのは、==なかなかにマズイ==。色々とマズイ。

## 空集合と単元集合の混乱

空集合と単元集合が区別できてない事例は、意外に多く見受けられる。

“引数無しの関数”は、$f()$ の形で呼び出すが、このことから、$f$ のプロファイルを、

$\quad f:\emptyset \to Y \In {\bf Set}$

と思い込んでいる人が意外に多い。

上記プロファイルの関数は存在するが、それと引数無しの関数は==まったく別物！== 引数無しの関数のプロファイルは、

$\quad f:{\bf 1} \to Y \In {\bf Set}$

例えば、${\bf 1} = \{*\}$ ならば、$f()$ は $f(*)$ の略記（モノグサしてるだけ）。

悪いことに単元集合型をvoid型と呼ぶ。'void'の英語辞書的意味は'empty'と同義。だが、void type = empty set ではなくて、void type = singleton set 。

プログラミング言語の幾つかは、単元集合型の唯一の要素を空リスト $()$ に設定している。

$\quad {\bf 1} = \{()\}$

関数への引数渡しを $f\; x$ と書く構文を使うと、

$\quad f( () ) = f\; ()$

となり、“引数無しの関数”の呼び出し形式を構文的に合理化できる。うまい工夫だが、余計に誤解と混乱を助長している気もする。

## 単元集合と要素の混乱

単元集合とその唯一の要素をオーバーロードすることは割と多い。

$\quad \text{null} = \{\text{null}\}\\
\quad 1 = \{ 1 \}$

$A$ が単元集合のとき、その要素はイプシロン記号 $\varepsilon!$ で明示的に取り出したほうがよい。例えば“ルート2”の定義は：

$\WeDefine \sqrt 2 := \varepsilon! \{x\in {\bf R} \mid x^2 = 2 \land x \ge 0\}$

単元とは限らない集合とビックリが付いてないイプシロン記号の組み合わせ $\varepsilon A$ は、どの要素を選ぶか分からないので使いにくい。

イプシロン記号の別な使用例として、写像 $f:A \to B\In {\bf Set}$ が全単射のとき、逆写像 $g$ の定義は次のようにする。

$\WeWillDefine g:B \to A \In {\bf Set}\\
\For y \in B\\
\WeDefine g(y) := \varepsilon!\{x \in A\mid f(x) = y\}\\
\Justification\\
\quad \forall y\in B.\, \mrm{IsSingletonSet}(\{x \in A\mid f(x) = y\})$

必要な場面ではイプシロン記号を使ったほうが議論が明確になる。逆に言うと、イプシロン記号を使わないと曖昧模糊になるリスクがある。

## プロファイル、ホムセット、射の混乱

プロファイル、ホムセット、射は別な概念である。「そんなことは承知している」と思うかも知れないが、やせた圏〈thin category〉では混乱する。

プロファイル（域・余域の指定） $A \to B$ に対して、ホムセット $\cat{C}(A, B)$ は必ず定まる。が、ホムセットがどんな集合かは分からない。

- ホムセット $\cat{C}(A, B)$ は空集合かも知れない。
- ホムセット $\cat{C}(A, B)$ は単元集合かも知れない。
- ホムセット $\cat{C}(A, B)$ は2個以上の要素を持つかも知れない。
- ホムセット $\cat{C}(A, B)$ は無限集合かも知れない。

何とも言えない。

ホムセットが空集合または単元集合である圏をやせた圏と呼ぶ。やせた圏では：

- 指定されたプロファイルの射は存在しないかも知れない。
- 指定されたプロファイルの射が存在するなら、ひとつしかない。

このため、やせた圏でのプロファイル／ホムセット／射が==ゴッチャになりがち==。

混乱予防のために、指定したプロファイルの射があれば、それを $![A \to B]$ と書くことにする。

- プロファイル： $A \to B \In \cat{C}$
- 単元ホムセット： $\cat{C}(A, B) \In {\bf Set}$
- 唯一の射： $![A \to B] \in \cat{C}(A, B)$

この記法は、やせた圏でなくても、ホムセットが単元集合のときなら使える。例えば、終対象への唯一の射は：

$\quad !_X = \,![X \to {\bf 1}] \in \cat{C}(X, {\bf 1})$

ただし、$![A \to B]$ が意味を持つのは、ホムセットが単元集合のときだけなので注意。集合圏で $![{\bf 1} \to \emptyset]$ と書いても意味がない（そんな射は存在しないから）。

2-射の場合でも同様にする。

- プロファイル： $f \twoto g \In \cat{C}$
- 単元ホムセット： $\cat{C}(?, ?)(f, g) \In \cat{C}$
- 唯一の2-射： $![f \twoto g] \in \cat{C}(?, ?)(f, g)$

疑問符のところは適当な対象〈0-射〉が入るが、

$\quad A := \mrm{dom}(f) = \mrm{dom}(g)\\
\quad B := \mrm{cod}(f) = \mrm{cod}(g)\\
\quad \alpha:: f \twoto g: A \to B \In \cat{C}$

ならば、

- 唯一の2-射： $\alpha = \,![f \twoto g] \in \cat{C}(A, B)(f, g)$

## 構文と意味の混乱

構文領域にある構文的対象〈syntactic object〉と意味領域にある意味的対象〈semantic object〉の区別は難しい。これは、モノグサ原則に起因するとは言いにくいので、別な機会に論じる。

次のような関係があるとだけ言っておく。

digraph {
    concept[label="抽象的概念"]
    subgraph cluster_dom {
      syn[label="構文\n(ラベル,コンビネーション)"]
      sem[label="意味\n(シング)"]
      syn -> sem[label="意味割り当て"]
      sem -> syn[label="構文化\n 引用"]
    }
    concept -> syn[label="構文的側面"]
    concept -> sem[label="意味的側面"]
}