「ものが等しい」ということ

最近、「ものの等しさ」について思うところが何点かあるので書き殴っておく。

数学での「等しさ」

ものを数学的な議論に載せる上で、「等しさ」というのは基本的な概念だと思われる。扱う対象の「等しさ」について合意ができない人と数学的な議論はできない。

述語論理では

まず、述語論理で等号がどう扱われているかについて見ておく。

述語論理では、等号\(=\)はいくつかの規則(公理)を満たすことになっている(等号公理)。いくつか挙げておく:

  • \(t=t\)はいつでも成り立つ。
  • 述語\(P\)について\(P(t)\)かつ\(t=s\)ならば\(P(s)\)が成り立つ。
    • 特に、\(s=t\)かつ\(t=u\)ならば\(s=u\)である。
    • また、\(t=s\)ならば\(s=t\)である。
  • \(t=s\)ならば、任意の(\(t\)に対して定義された)関数\(f\)について\(f(t)=f(s)\)が成り立つ。

まあ、なんというか、「\(s\)と\(t\)が等しければ\(s\)と\(t\)は入れ替えても同じ役割を果たさなければならない」とでも言えるだろうか。

数学では「等号に似た性質を持つ」関係がよく登場する。関係\(\sim\)が以下の3つの性質を満たす時、これを同値関係という:

  • \(t\sim t\)(反射律)
  • \(s\sim t\)かつ\(t\sim u\)ならば\(s\sim u\)(推移律)
  • \(s\sim t\)ならば\(t\sim u\)(対称律)

これらは「等号がどういう性質を満たすべきか」という話であり、具体的な対象(自然数や集合)についての等号はそれぞれの対象が満たす公理やら何やらで議論することになる。

例えばZF集合論であれば、外延性公理によって「集合は所属関係\(\in\)によって等しさが決まる」ことが言える。「この集合\(\{1,2,3\}\)は昨日作ったけどこっちの集合\(\{2,3,1\}\)は今日作ったから別物」みたいなことはないわけだ。

別の例として、自然数を扱うペアノの公理系では自然数に関する等式や「等号の否定\(\neq\)」の公理がいくつかあり、帰結として「\(2\times 3=6\)」や「\(3\neq 4\)」が言える。

「等しさ」の取り替え

数学では、異なる対象を同一視したいことがよくある。例えば、「7で割った余り」を計算したい場合、3と17は7で割った時の余りが同じだから計算の上では同一視できる。有理数の集合から実数を構成するときは、有理数列\(a_n=1-1/n\)と\(b_n=1+2^{-n}\)は何らかの良い条件を満たすから同一視したい。

こういう場合に数学で標準的に使われる構成が、商集合だ。つまり、集合\(A\)とその上の同値関係\(\sim\)があった時に、新たな集合\(A/{\sim}\)を作ることができる。標準的な全射\(p\colon A\to A/{\sim}\)があって、\(x\sim y\)を満たす元は商集合に移すと本物の等式\(p(x)=p(y)\)を満たすようになる。

これは「等しさ」の取り替えと思うこともできるかもしれないが、同じ集合に複数の「等しさ」があってはいけない。ここでは、\(A\)の「等しさ」はそのままであり、\(A\)と\(A/{\sim}\)は別物なのだ。

ところで。商集合が構成できれば良いのだが、プログラミングで出てくるようなだとそういう構成ができないことがある。そういう場合に使われるのがsetoid(セトイド、セットイド、亜集合)だ。

setoidは集合\(A\)とその上の同値関係\(\simeq_A\)の組\(\langle A,\simeq_A\rangle\)である。まあ、数学的な構造にはよくある話だ。数学に慣れた読者なら「はいはい、『良い感じの性質を満たす写像』を考えて圏にするんだね」とか言い出すだろう。

ここでの「良い感じの性質を満たす写像」は、もちろんsetoidに備わった同値関係をリスペクトする写像のことである。\(\langle A,\simeq_A\rangle\)から\(\langle B,\simeq_B\rangle\)へのsetoidの射とは、(集合としての)写像\(f\colon A\to B\)であって、「\(x\simeq_A y\)ならば\(f(x)\simeq_B f(y)\)」を満たすもののことである。

このほか、setoid \(\langle A,\simeq_A\rangle\)について述べるときは備わった同値関係をリスペクトするようにしなければならない。

まあ私もsetoid周辺にはそこまで詳しくないのでこの辺にしておくが、setoidはモロに「等しさ」の概念を取り替えている感じがする。もちろん、台集合が同じでも備わった同値関係が異なれば異なるsetoidであるが。

掛け算の順序

話は変わるが、「掛け算の順序」はSNSで人気の話題だ。普段数学界隈にいない人がうっかり言及して、界隈の人々が群がってくる光景は何回か見た気がする。

小学校での指導方法やテストの採点についてはここでは論じない。私が気になっているのは、SNSで見かける論者の中に「等しさ」の概念を履き違えている輩がいることである。つまり、「\(2\times 3=3\times 2\)である」と言ったときにケチをつけてくるような輩のことである。

無論、字面だけを見れば「\(2\times 3\)」と「\(3\times 2\)」は異なる見た目をしているが、数学での「\(=\)」は字面だけを見るものではない。計算過程が違っても構わない。そういう、「可換性を認められない人」はこの記事の冒頭に書いた「扱う対象の『等しさ』について合意ができない人」であり、まともな議論は成り立たない。

もちろん、「字面が同じ」「計算過程や計算量が同じ」ことを意識する議論があっても良いが、通常の意味の「\(=\)」と混同させてはならない。議論の際に「等しさ」の概念をわざと混同させているならその者は悪質な詭弁家であるし、無理解ゆえに混同させているならばその者は数学的な議論の土俵に立てない阿呆である。

参考:https://togetter.com/li/2331626

元々頭のおかしな人が掛け算の順序にのめり込んだ結果ああなったのか、それとも掛け算の順序には人を狂わせる魔力があるのか、謎である。

プログラミングにおける「等しさ」

プログラミングにおいても「等しさ」は大事だ。多くのプログラミング言語には「等しさ」を判定する == のような演算子があるし、マップや集合のようなデータ構造を作るには「等しさ」を判定しないといけないし、「等しさ」はコンパイラーの最適化にも関わってくる。

これらの「等しさ」は同じものだろうか?そうではない。まず、== のような演算子は、所詮はただの演算子・関数であって、言語設計者や(演算子オーバーロードのできる言語なら)プログラマーが自由に設定できる。例えば、浮動小数点数について NaN == NaN が成り立たないのは有名な話だ。0.0 == -0.0 なのに 1.0/0.0 != 1.0/(-0.0) という話もある。JavaScriptでは [] == "" が成り立つ。つまり、== は一般には数学的な「等しさ」(等しければ振る舞いは完全に同一)とは別の概念であることがわかる。もちろん、== が数学的な「等しさ」となるべく一致するように作るのが良い言語・良いプログラマーの務めであろう。

話は変わるが、世の中にはオブジェクト指向という考えに影響された言語が多い。「オブジェクト指向」を構成する要素は多くあるだろうが、「オブジェクト」という概念があることは共通しているだろう。ならば「オブジェクト」の「等しさ」を考えなくてはならない。

例えば、JavaScriptで const a = {foo: 123, bar: "A"} で作ったオブジェクトと、const b = {foo: 123, bar: "A"} で作ったオブジェクトは「等しい」だろうか?

const a = {foo: 123, bar: "A"};
const b = {foo: 123, bar: "A"};
// aとbは「等しい」か?

abJSON.stringify のような関数に与えて中身を見ると、同じ結果を返すだろう。では ab は「等しい」と言って良いだろうか?

否である。=== 演算子で ab を比較すると、false が返ってくる。オブジェクトには自己同一性 (identity) があり、異なる瞬間に作られたオブジェクトは自己同一性の意味で異なる、というのが多くのオブジェクト指向言語で一致するところだろう。参照の等価性と呼ばれることもある。

自己同一性を手軽に判定できる言語としては、Java(==)、JavaScript(===)やPython(is)がある。

オブジェクト指向の信者であれば自己同一性はあって当たり前のものだと思うかもしれない。しかし、実際のところ自己同一性は何の役に立つのだろうか?Javaで文字列を == で比較しようとしたプログラマーを罠に嵌めるためだろうか?

一つの答えは、可変なオブジェクトを区別するため、となる。先ほどのJavaScriptの例で言うと、ab を構築した直後は同じ内容のオブジェクトに見えるかもしれないが、

a.foo = 456;

という文を実行してしまうと ab は内容が異なるオブジェクトとなる。こういう破壊的更新を気軽に行える言語では、自己同一性が重要となる。

逆に言うと、不変な(immutableな)オブジェクトについては自己同一性はそれほど重要ではない。むしろ、なるべく隠したほうが「Javaで String== で比較してしまった」というような事故を防げるだろう。

実際、Standard MLやHaskellのような関数型言語では、ほとんどの値は不変であり、内容に基づいて == (SMLの場合は =)の判定が行われる。例外は参照セル(ref 型や IORef 型)や可変な配列(SMLの array 型)であり、これらは破壊的更新が行われるため、自己同一性に基づいて等価性が判定される。

関数型言語であっても、実装依存の手段で不変な値の「参照の等価性」を判定できることがある。ただ、そういうのはプログラマーの責任で行うものであって、コンパイラーが最適化によって「2箇所で生成された同じ内容の値」を「1箇所で生成された値」にまとめる可能性を考慮しなくてはならない。

プログラミング言語を設計する者は、安易に「全てはオブジェクトだ!!!」と主張する前に、値の同一性についてよく考えるべきである。値に自己同一性を持たせることは何の役に立つのか?そして、どういう最適化を阻害するのか?

最後に、コンパイラーにとっての「等しさ」について触れておく。コンパイラーは原則として、言語仕様で定められたプログラムの振る舞いを変えてはならない。しかし、計算にかかるコストを削減することは認められる。

ab が整数型なら a * bb * a は値が同じなので、これらを同一視して共通部分式削除などの最適化の対象にできる。もっと複雑な例として、次のコード

int sum = 0;
for (int i = 0; i < n; ++i) {
    sum += i;
}

は、オーバーフローが起こらなければ sum = n * (n - 1) / 2 と等価である。なので、オーバーフローが起こらないと仮定できる状況(C言語の符号付き整数など)ではコンパイラーは前者を後者に書き換えて良い。コンパイラーにとってこれらは値が等しく、計算コストは後者の方が低いからだ(CPUに乗算命令があればの話だが)。

オブジェクトの例で言うと、JavaScript処理系は

const a = {foo: 123, bar: "A"};
const b = {foo: 123, bar: "A"};

const a = {foo: 123, bar: "A"};
const b = a;

に最適化することは基本的にできない。ab が破壊的更新されたり、自己同一性のテストが行われたりすると挙動が変わるからだ(逆に言うと、これらが起こらないことを確認できれば最適化しても良い)。一方、Standard MLでは

val a = {foo = 123, bar = "A"}
val b = {foo = 123, bar = "A"}

というコードを

val a = {foo = 123, bar = "A"}
val b = a

に最適化することができる。レコードは不変(immutable)で、レコードの自己同一性をテストする手段は通常のStandard MLにはないからだ。

浮動小数点数の話をすると、a * bb * a はNaNを無視すれば値が同じなのでコンパイラーはこれらを等価だと判断する(トンデモ系の人は「消費電力が違うかもしれない」と言い出すのだが、違いがあったとしても微々たるものだろうし、コンパイラーにとってはどうでも良いことである)。一方、a + 0.0a は同一視できない。a-0.0 の場合に前者は(通常の丸めモードでは) 0.0 となり、後者は -0.0 となるからだ。0.0-0.0== の意味では等しくても、逆数や atan2 を計算したときに振る舞いの違いが観測できるため、コンパイラーはこれらを別物だと考えなければならない。コンパイラーにとって重要なのは「値が同じように振る舞うか」という意味での「等しさ」であり、「== 演算子が true を返す」という意味での「等しさ」ではない。

まあ「NaNのビットパターンについての違いは無視するけど0の符号は無視しないのかよ」みたいな話になるのだが、それは言語仕様との兼ね合いになるのだろう。言語仕様が認めていればコンパイラーは最適化によって振る舞いを変えても良い。一方、x86の機械語(これもプログラミング言語と考えられる)では浮動小数点数はNaNのビットパターンも含めてほぼ完全に挙動が規定される(一部の近似命令や乱数命令は除く)。言語仕様は「認められる振る舞いの集合」を指定する、と考えれば良いのだろうか。

ぐだぐだと書いたが、「プログラミングでは一つの型に複数の『等しさ』(っぽい概念)が紐づくことがあるから気をつけろ」というのが教訓になるだろうか。

Spread the love