「同じ」という言葉は何を意味するのか？

あるものAとあるものBが「同じ」だというのは、何を意味するのだろう。

もしも、AとBが数字なら、その意味ははっきりわかる。
例えば、A=1でB=1なら、AとBが「同じ」だということになる。それは、1=1のことだ。

もしも、AとBが集合なら、AとBが同じだということは、Aに含まれる要素がBに含まれる要素が全て等しいということだ。集合 A={ りんご、みかん、バナナ } は、集合 B = { バナナ,  みかん. りんご } と「同じ」である。

もしも、AとBが三角形なら、二つの三角形の二辺の長さが等しく、その二辺が作る角度が等しい場合、三角形Aと三角形Bは、「同じ」だと言える。

これらの例でわかることは、あるものとあるものが「同じ」だというためには、それぞれが、同じ種類のものでなければならないということ。数字と三角形は、「同じ」にはなれない。

ここでの「同じ種類」というものを、「同じ型を持つ」ということにすれば、あるものAとあるものBが「同じ」だというためには、AとBは、「同じ型」を持っていなければいけないということになる。

このあたりのことを、数学者のドリーニュが例を挙げて丁寧に説明しているビデオがある。"What do we mean by "equal" " https://goo.gl/nXhqmb
今年の9月にプリンストンの高等研究所で開催された "Vladimir Voevodsky Memorial Conference" https://www.math.ias.edu/vvmc2018 での、彼の講演である。

ドリーニュは、若くして、グロタンディックを出し抜いて「ヴェーユ予想」を解いた有名な数学者なのだが、不思議なことに、彼が説明していることは、コンピュータでプログラミングをしたことがある人は、よくわかっていることだということである。

整数 A=1 と浮動小数点実数 B=1.0 とは、コンピュータ内部での扱いは違うものである。もしも、あるプログラミング言語が、整数型・実数型の他に複素数型をサポートしているとすると、A=1, B=1.0, C=1.0+0.0i は、皆、違うものである。

数字の場合いずれの型にも、加減乗除の演算は定義される。複数の型に適用可能な演算子は、「ポリモーフィズム」と言われるのだが、このあたりの扱いも、必要なら「キャスト」で型変換することを含めて、プログラマはよく知っていると思う。

ここでは、もう一つ別のことを確認しておこう。

同じ型に属するA, Bに対して、「AとBは同じ」だということとは、別の「同じ」があるのだ。それは、二つの型が同じことを意味する「同じ」だ。前者は、ある型に属するインスタンスが等しいことを述べているのだが、後者は、型のシステムの中で、二つの型が等しいことを述べている。

このことを、初めて明確な形で定式化したのは、マーティン＝レフである。
Martin-Löfの型の理論は、次のことを示す四つの形式で記述される。

　ある対象aが、型であること
　　α : Type
　ある表現式 aが、型 αの要素であること
　　 a : α
　二つの表現式が、同じ型の内部で、等しいこと
　　a = b : α
　二つの型が、等しいこと
　　α = β　: Type

マーティン＝レフの「型の理論」は、関数型言語の基礎を与えている。

実は、現代数学の重要な流れの一つである Univalent Theory は、数学の新しい基礎づけを探していたVoevodskyが、思いもかけず身近なところ、学生たちのコンピュータ実習室で、マーティン＝レフの「型の理論」を再発見したときに始まるのだ。