公理

この章では、関数が呼出されたとき動作の定義を行う前提となる公理を定める。

これらは実行環境の動作を厳密に定めるために導入するものであり、多くの読者にとってこの章の内容は退屈なものだろう。

公理に基づく処理

この仕様書において実行環境の動作が公理に基づいて定められている場合は、実行環境はその裁量によって、その動作で定められた結果そのものの代わりに、公理によってその結果と等しいと導かれる結果を用いても良い。

動作が公理を満たしていると見なしてという制約付きで定められている場合は、実際に公理が満たされているかどうかに関わらず、公理が満たされていれば正しい結果が得られるような一定の手順によって処理を行わなければならない。すなわち、実際には公理が満たされていなくても、処理を行うのに支障がない限り、公理が満たされている場合と同様の処理を行わなければならない (そしてその結果は本来の結果に等しくなくても良い)。実際には公理が満たされておらず、そのために処理の継続に支障がある場合は、エラーとする。特に、結果が正常終了となることが公理によって保証される部分の結果が正常終了でなかった場合は、直ちにその結果を公理に基づく処理全体の結果として返す。

相等関係の公理

オブジェクトの集合 S が相等関係の公理を満たしているとは、S に属する任意のオブジェクト a, b, c が以下の条件を全て満たすことである。

式 !!(a == a) の評価結果は [[初期の Boolean.true]] である。
式 !!(a == b) === !!(b == a) の評価結果は [[初期の Boolean.true]] である。
式 !!(a == b && b == c) の評価結果が [[初期の Boolean.true]] ならば、式 !!(a == c) の評価結果も [[初期の Boolean.true]] である。
式 !!(a == b) === !(a != b) の評価結果は [[初期の Boolean.true]] である。
オブジェクト a, b が等しいことと式 !!(a == b) の評価結果が [[初期の Boolean.true]] であることは同値である。

相等関係の公理は、== 演算子が同値関係であることを表している。

関数の公理

オブジェクト F が関数の公理を満たしているとは、以下の条件を満たすことである。

F は関数として呼出し可能である。
n を 1 以上の自然数とし、a₁, a₂, …, a_n および b₁, b₂, …, b_n をそれぞれオブジェクトとする。1 以上 n 以下の任意の自然数 i について a_i と b_i が等しいとき、式 F[a₁, a₂, …, a_n] と F[b₁, b₂, …, b_n] の評価結果は等しい。

関数の公理は、関数として呼出し可能なオブジェクトが (プログラミングにおける手続きとしての関数ではなく) 数学的な意味での関数であることを表す。

マグマの公理

マグマとは、特定の二項演算が定義されたオブジェクトの集合である。

加法に関するマグマ

オブジェクトの集合 S が加法に関するマグマの公理を満たしているとは、以下の条件を全て満たすことである。

S は相等関係の公理を満たしている。
S に属する任意のオブジェクト a, b に対し、式 a + b の評価結果は正常終了であり、その値もまた S に属する。

乗法に関するマグマ

オブジェクトの集合 S が乗法に関するマグマの公理を満たしているとは、以下の条件を全て満たすことである。

S は相等関係の公理を満たしている。
S に属する任意のオブジェクト a, b に対し、式 a * b の評価結果は正常終了であり、その値もまた S に属する。

半群の公理

半群とは、演算に結合法則が成り立つマグマである。

加法に関する半群

オブジェクトの集合 S が加法に関する半群の公理を満たしているとは、以下の条件を全て満たすことである。

S は加法に関するマグマの公理を満たしている。
S に属する任意のオブジェクト a, b, c に対し、式 (a + b) + c と a + (b + c) の評価結果は等しい。

乗法に関する半群

オブジェクトの集合 S が乗法に関する半群の公理を満たしているとは、以下の条件を全て満たすことである。

S は乗法に関するマグマの公理を満たしている。
S に属する任意のオブジェクト a, b, c に対し、式 (a * b) * c と a * (b * c) の評価結果は等しい。

モノイドの公理

モノイドとは、単位元のある半群である。

加法に関するモノイド

オブジェクトの集合 S が加法に関するモノイドの公理を満たしているとは、以下の条件を全て満たすことである。

S は加法に関する半群の公理を満たしている。
S に属する任意のオブジェクト a は Math$zero という名前のプロパティを持ち、その値もまた S に属する。そして S に属する任意のオブジェクト b について式 a.Math$zero + b および b + a.Math$zero の評価結果は b の評価結果に等しい。

乗法に関するモノイド

オブジェクトの集合 S が乗法に関するモノイドの公理を満たしているとは、以下の条件を全て満たすことである。

S は乗法に関する半群の公理を満たしている。
S に属する任意のオブジェクト a は Math$one という名前のプロパティを持ち、その値もまた S に属する。そして S に属する任意のオブジェクト b について式 a.Math$one * b および b * a.Math$one の評価結果は b の評価結果に等しい。

群の公理

群とは、逆演算の可能なモノイドである。

加法に関する群

オブジェクトの集合 S が加法に関する群の公理を満たしているとは、以下の条件を全て満たすことである。

S は加法に関するモノイドの公理を満たしている。
S に属する任意のオブジェクト a について、式 -a の評価結果は正常終了であり、その値もまた S に属する。そして式 -a + a および a + -a の評価結果は a.Math$zero の評価結果に等しい。
S に属する任意のオブジェクト a, b について、式 a - b と a + -b の評価結果は等しい。

乗法に関する群

オブジェクトの集合 S が乗法に関する群の公理を満たしているとは、以下の条件を全て満たすことである。

S は乗法に関するモノイドの公理を満たしている。
S に属する任意のオブジェクト a について、式 /a の評価結果は正常終了であり、その値もまた S に属する。そして式 /a * a および a * /a の評価結果は a.Math$one の評価結果に等しい。
S に属する任意のオブジェクト a, b について、式 a / b と a * /b の評価結果は等しい。

可換群の公理

可換群とは、演算に交換法則が成り立つ群である。

加法に関する可換群

オブジェクトの集合 S が加法に関する可換群の公理を満たしているとは、以下の条件を全て満たすことである。

S は加法に関する群の公理を満たしている。
S に属する任意のオブジェクト a, b について、式 a + b と b + a の評価結果は等しい。

乗法に関する可換群

オブジェクトの集合 S が乗法に関する可換群の公理を満たしているとは、以下の条件を全て満たすことである。

S は乗法に関する群の公理を満たしている。
S に属する任意のオブジェクト a, b について、式 a * b と b * a の評価結果は等しい。

環の公理

環とは、加法・減法・乗法が定義されたオブジェクトの集合である。環は加法に関する可換群である。また環の加法と乗法には分配法則が成り立つ。

オブジェクトの集合 S が環の公理を満たしているとは、以下の条件を全て満たすことである。

S は加法に関する可換群の公理と乗法に関する半群の公理を満たしている。
S に属する任意のオブジェクト a, b, c について、式 a * (b + c) と a * b + a * c の評価結果は等しく、また式 (a + b) * c と a * c + b * c の評価結果も等しい。

単位的環の公理

単位的環とは、乗法に単位元が存在する環である。

オブジェクトの集合 S が単位的環の公理を満たしているとは、S が環の公理と乗法に関するモノイドの公理の両方を満たしていることである。

斜体の公理

斜体とは、四則演算が定義されたオブジェクトの集合である。加法は可換であるが、乗法は可換とは限らない。

オブジェクトの集合 S が斜体の公理を満たしているとは、以下の条件を全て満たすことである。

S は単位的環の公理を満たしている。
S から、自身の Math$zero プロパティの値と等しいオブジェクトを除いた集合は、乗法に関する群の公理を満たす。

体の公理

体とは、加法だけでなく乗法も可換な斜体である。

オブジェクトの集合 S が体の公理を満たしているとは、S が斜体の公理と乗法に関する可換群の公理の両方を満たしていることである。