floating_vs_decmial_x の設計

設計目標

このパッケージは同じ入力で moonbitlang/x/decimal(X)と Luna-Flow/floating/decimal_gda@0.7.1(GDA)を比較します。二つのライブラリの算術は同じではありません。X は小数部を最大 28 桁保持して切り捨て、GDA はコンテキストが選ぶ有効桁数の精度に丸めます。したがって公平な比較には、まず意味論的な契約を定め、両ライブラリにそれを満たさせ、満たすことを証明し、そのうえで計測する必要があります。

API ページが各項目を挙げ、チュートリアルがそれらを実行し、計測値は性能の章にあります。DzmingLi ベンチマークと共通の手法(オラクルによる判定、正準形、対応のある統計)は dzmingli_vs_floating の設計ページで導出しており、このページでは違いを述べます。

数学的背景

二つの十進モデル

X の十進数は 0≤s≤280 \le s \le 28 を満たす組 (c,s)(c, s) で、c⋅10−sc \cdot 10^{-s} を表します。Decimal::new は他のスケールを拒否します。演算は次のとおりです。

a⋅b=trunc⁡28(cℓcr10−(sℓ+sr))(exact when sℓ+sr≤28),a/b=⌊ ⁣⌊cℓ10 28−sℓ+srcr⌋ ⁣⌋⋅10−28,\begin{aligned} a \cdot b &= \operatorname{trunc}_{28}\bigl(c_\ell c_r 10^{-(s_\ell + s_r)}\bigr) \quad\text{(exact when } s_\ell + s_r \le 28\text{)}, \\ a / b &= \Bigl\lfloor\!\Bigl\lfloor \frac{c_\ell 10^{\,28 - s_\ell + s_r}}{c_r} \Bigr\rfloor\!\Bigr\rfloor \cdot 10^{-28}, \end{aligned}

ここで ⌊ ⁣⌊⋅⌋ ⁣⌋\lfloor\!\lfloor \cdot \rfloor\!\rfloor は 0 方向に切り捨てる整数除算、trunc⁡k\operatorname{trunc}_k は小数 kk 桁への 0 方向の切り捨てで、DzmingLi の設計ページで定義したものです。加算、減算、比較は厳密です。sℓ≤28s_\ell \le 28 なので指数 28−sℓ+sr28 - s_\ell + s_r は負にならず、したがって

a/b=trunc⁡28(a/b)a / b = \operatorname{trunc}_{28}(a / b)

が厳密に成り立ちます。X の商は真の商を小数 28 桁に切り捨てたものです。

精度 pp、丸め Down のコンテキストでの GDA 演算は round⁡p(x)\operatorname{round}_p(x)、すなわち厳密な結果を有効 pp 桁に切り捨てたものを返します。同じコンテキストでの quantize(y, 10^{-28}) は、結果が pp 桁に収まるとき trunc⁡28(y)\operatorname{trunc}_{28}(y) を返します。

入れ子の切り捨て

以下の証明は切り捨てに関する二つの事実に基づきます。

補題 1。 t≥kt \ge k と任意の実数 xx について trunc⁡k(trunc⁡t(x))=trunc⁡k(x)\operatorname{trunc}_k(\operatorname{trunc}_t(x)) = \operatorname{trunc}_k(x)。

証明。 x≥0x \ge 0(負の場合は対称)とし、Gj=10−jZG_j = 10^{-j}\mathbb{Z} とします。trunc⁡j(x)\operatorname{trunc}_j(x) は xx を超えない GjG_j の最大の点です。Gk⊆GtG_k \subseteq G_t なので点 z=trunc⁡k(x)z = \operatorname{trunc}_k(x) は GtG_t に属し z≤xz \le x、よって z≤trunc⁡t(x)≤xz \le \operatorname{trunc}_t(x) \le x です。したがって trunc⁡t(x)\operatorname{trunc}_t(x) 以下の GkG_k の最大の点は zz 以上であり、かつ xx 以下の GkG_k の最大の点、すなわち zz 以下です。□\square

補題 2。 整数 NN と A,B>0A, B > 0 について ⌊ ⁣⌊⌊ ⁣⌊N/A⌋ ⁣⌋/B⌋ ⁣⌋=⌊ ⁣⌊N/(AB)⌋ ⁣⌋\lfloor\!\lfloor \lfloor\!\lfloor N / A \rfloor\!\rfloor / B \rfloor\!\rfloor = \lfloor\!\lfloor N / (AB) \rfloor\!\rfloor。

証明。 N≥0N \ge 0 について N=qA+rN = qA + r(0≤r<A0 \le r < A)、q=uB+vq = uB + v(0≤v<B0 \le v < B)と書きます。すると N=uAB+(vA+r)N = uAB + (vA + r) かつ 0≤vA+r≤(B−1)A+A−1<AB0 \le vA + r \le (B-1)A + A - 1 < AB なので u=⌊N/(AB)⌋u = \lfloor N/(AB) \rfloor です。0 方向の切り捨ては NN について奇関数なので、負の場合も従います。□\square

設計上の決定

二つの意味論グループ

課題。 乗算と除算では、結果に小数 28 桁を超える桁が必要になった時点で両ライブラリの本来の結果は食い違い、異なる計算を計時しても何も分かりません。選択肢。 両方が厳密になる入力にベンチマークを限る、GDA に X のポリシーを再現させる、X に GDA のポリシーを再現させる。決定。 二つのグループを別々に報告します。ExactOverlap は入力を制限し、XCompatible は追加の quantize で GDA に X のポリシーを再現させます。理由。 X には設定できるコンテキストがないので適応できるのは GDA 側だけであり、その適応のコストは GDA の利用者が X の意味論のために払うものの一部です。二つのグループは異なる計時範囲 arithmetic_only と semantic_equivalent_pipeline を持ち、決して合算しません。

両グループに共通の一つのオラクル

オラクルは X のポリシーを実装します。加算、減算、比較は厳密、厳密な積のスケールが 28 を超えるときはその trunc⁡28\operatorname{trunc}_{28}、商は trunc⁡28\operatorname{trunc}_{28} です。除算では k=28+sr−sℓk = 28 + s_r - s_\ell として、k≥0k \ge 0 のとき ⌊ ⁣⌊cℓ10k/cr⌋ ⁣⌋\lfloor\!\lfloor c_\ell 10^{k} / c_r \rfloor\!\rfloor、そうでなければ ⌊ ⁣⌊⌊ ⁣⌊cℓ/10−k⌋ ⁣⌋/cr⌋ ⁣⌋\lfloor\!\lfloor \lfloor\!\lfloor c_\ell / 10^{-k} \rfloor\!\rfloor / c_r \rfloor\!\rfloor を返し、これは補題 2 により(crc_r の符号を NN に移せば)⌊ ⁣⌊cℓ/(10−kcr)⌋ ⁣⌋\lfloor\!\lfloor c_\ell / (10^{-k} c_r) \rfloor\!\rfloor に等しくなります。どちらの場合も trunc⁡28(a/b)⋅1028\operatorname{trunc}_{28}(a / b) \cdot 10^{28} です。

ExactOverlap では生成されるすべての結果に対して切り捨ては恒等なので、同じオラクルが厳密な値を返します:

  • 乗算のフィクスチャは sℓ+sr=14≤28s_\ell + s_r = 14 \le 28 を満たすスケールの組を使う。
  • 除算のフィクスチャは整数を 22、44、55、88、2525 で割り、その逆数 5⋅10−15 \cdot 10^{-1}、25⋅10−225 \cdot 10^{-2}、2⋅10−12 \cdot 10^{-1}、125⋅10−3125 \cdot 10^{-3}、4⋅10−24 \cdot 10^{-2} の小数部は高々 3 桁。
  • 加算、減算、比較は定義により厳密。

精度契約

GDA の精度 pp は working_precision(op, ℓ, r, semantics) で、ガード桁は足しません。dℓ,drd_\ell, d_r を係数の桁数、m=max⁡(dℓ,dr)+∣sℓ−sr∣m = \max(d_\ell, d_r) + |s_\ell - s_r| とすると:

Add/Subtract:result<10m+1⇒p=m+2Multiply:∣cℓcr∣<10dℓ+dr⇒p=dℓ+dr+1Divide, ExactOverlap:∣cℓ∣⋅{5,25,2,125,4}<10dℓ+3⇒p=dℓ+dr+2≥dℓ+3Compare:operands only⇒p=max⁡(dℓ,dr)+1\begin{aligned} \textbf{Add/Subtract:}\quad & \text{result} < 10^{m+1} &&\Rightarrow p = m + 2 \\ \textbf{Multiply:}\quad & |c_\ell c_r| < 10^{d_\ell + d_r} &&\Rightarrow p = d_\ell + d_r + 1 \\ \textbf{Divide, ExactOverlap:}\quad & |c_\ell| \cdot \{5, 25, 2, 125, 4\} < 10^{d_\ell + 3} &&\Rightarrow p = d_\ell + d_r + 2 \ge d_\ell + 3 \\ \textbf{Compare:}\quad & \text{operands only} &&\Rightarrow p = \max(d_\ell, d_r) + 1 \end{aligned}

したがって ExactOverlap のすべての結果と、量子化前の XCompatible の積は GDA で厳密です。XCompatible の積は sℓ+sr>28s_\ell + s_r > 28 のとき 10−2810^{-28} に量子化されます。量子化後の係数は厳密な係数より桁数が少ないので quantize は成功し、厳密な積の trunc⁡28\operatorname{trunc}_{28}、すなわち X の積を返します。

XCompatible の除算では精度は次のとおりです。

p=max⁡(1,I)+30,I=dℓ−sℓ−dr+sr+1.p = \max(1, I) + 30, \qquad I = d_\ell - s_\ell - d_r + s_r + 1 .

II は商の整数部の桁数の上界です:

∣a∣<10 dℓ−sℓ,∣b∣≥10 dr−1−sr⇒∣a/b∣<10 dℓ−sℓ−dr+sr+1=10I.|a| < 10^{\,d_\ell - s_\ell}, \quad |b| \ge 10^{\,d_r - 1 - s_r} \quad\Rightarrow\quad |a / b| < 10^{\,d_\ell - s_\ell - d_r + s_r + 1} = 10^{I} .

divide は round⁡p(a/b)\operatorname{round}_p(a/b) を返します。∣a/b∣≥1|a/b| \ge 1 なら整数部は高々 II 桁なので、少なくとも p−I≥30p - I \ge 30 桁の小数が残ります。∣a/b∣<1|a/b| < 1 なら残る桁はすべて小数で、少なくとも p≥31p \ge 31 桁が残ります。いずれの場合も t≥30t \ge 30 の格子で round⁡p(a/b)=trunc⁡t(a/b)\operatorname{round}_p(a/b) = \operatorname{trunc}_t(a/b) となり、補題 1 から次が得られます。

quantize⁡(round⁡p(a/b), 10−28)=trunc⁡28(trunc⁡t(a/b))=trunc⁡28(a/b).\operatorname{quantize}\bigl(\operatorname{round}_p(a/b),\ 10^{-28}\bigr) = \operatorname{trunc}_{28}\bigl(\operatorname{trunc}_t(a/b)\bigr) = \operatorname{trunc}_{28}(a/b) .

量子化後の係数は高々 I+28≤p−2I + 28 \le p - 2 桁なので、quantize が無効演算を起こすことはありません。28 桁を超える 2 桁はガード桁です。補題 1 には不要ですが、商の最後の桁の作られ方に契約が左右されないようにしています。

この導出は divide が厳密なオペランド aa と bb を受け取ることを前提にしています。次節では、フィクスチャがこの前提を破る場合を示します。

既知の制限:X 互換除算でのオペランドの丸め

prepare_fixture は GDA のオペランドを Decimal::from_string(text, precision=p) で解析し、これは有効 pp 桁に偶数丸めします。XCompatible の除算では pp はオペランドの長さではなく桁数の差 II で決まるので、pp 桁より長いオペランドは計時される除算の前に丸められます。ここから二つの帰結が生じます。

  1. 正しさは構成によっては保証されない。 各オペランドが相対誤差 12101−p\tfrac12 10^{1-p} 以内に丸められると、計算される商は a/ba/b から最大で約 ∣a/b∣⋅101−p<10I+1−p≤10−29|a/b| \cdot 10^{1-p} < 10^{I + 1 - p} \le 10^{-29} ずれ、商が 10−2810^{-28} の倍数をまたぐことがあります。たとえば a=49⋯9⏟59a = 4\underbrace{9\cdots9}_{59}、b=1060b = 10^{60} では p=31p = 31 となり、GDA は aa を 5⋅10595 \cdot 10^{59} と解析して 0.50.5 を返しますが、X とオラクルは 0.49999999999999999999999999990.4999999999999999999999999999 を返します。公開されたコーパスが検証を通るのは商がそうした境界から離れているからであり、記録されたシードについての経験的な結果です。
  2. 計時される仕事量が異なる。 フィクスチャは桁数 DD が等しいオペランドを組にし、p≤51p \le 51 なので、D=64D = 64 以降 GDA は高々 51 桁のオペランドを割り、X は DD 桁のオペランド全体を割ります。そのため 64 桁以上の x_compatible 除算の計時は同じ仕事量を比べていません。一般的な桁数の実行(D≤28<pD \le 28 < p)は影響を受けません。

オペランドを max⁡(dℓ,dr)\max(d_\ell, d_r) 以上の精度で解析し、精度 pp のコンテキストで割れば、両方の影響はなくなります。このブランチではベンチマークのコードは変更しておらず、制限はここと性能の章に記録しています。

計時から除外されるフィクスチャ

X と GDA の値への変換、10−2810^{-28} の量子、コンテキスト、検証、正準化はすべて計時の外で構築または実行されます。計時される本体は run_x または run_gda で、公開演算一回と、XCompatible のパイプラインでは quantize のステップです。

対応のある統計

対応付け、相対差 δ\delta(ここでは X の中央値に対する)、3 %3\,\% の判定しきい値、速度比は DzmingLi ベンチマークと同じで、X を基準とします。x_speedup_vs_gda が 11 を超えれば X が速いことを意味します。

正しさと不変条件

  • 正準形と許容誤差 0 の健全性は DzmingLi の設計ページで証明しています。中立モデルのコードは同一です。
  • ExactOverlap:精度表と、それらの結果に対する trunc⁡28\operatorname{trunc}_{28} の恒等性により、生成されるすべての結果は両ライブラリで厳密であり、オラクルと一致します。
  • XCompatible の乗算:X、GDA、オラクルはいずれも厳密な積の trunc⁡28\operatorname{trunc}_{28} を返します。
  • XCompatible の除算:X とオラクルはすべての入力で trunc⁡28(a/b)\operatorname{trunc}_{28}(a/b) を返します。GDA もオペランドの有効桁数が pp 以下なら同じです(補題 1)。それより長いオペランドは上の既知の制限に当たります。
  • 比較:X の Compare::compare は共通のスケールでの係数比較の符号を返し、normalize_order がそれを {−1,0,1}\{-1, 0, 1\} に写します。GDA の compare は同じ値を十進数として返します。

却下した代替案

  • すべての演算に単一の「公平な」意味論。 却下:小数 28 桁を超える積と商について、両ライブラリが本来実装している意味論は存在しません。
  • X に GDA を真似させる。 却下:X には精度や丸めのコンテキストがないので、公開 API の外で追加のスケール調整が必要になります。
  • 小数 28 桁目の 1 単位を許容誤差として比較する。 却下:両側とも決定的に切り捨てるので、厳密な一致が必要であり、実現もできます。
  • 演算ごとに一つの合算スコア。 却下:arithmetic_only と semantic_equivalent_pipeline は異なる仕事を計時しています。

境界

  • 計測するのは add、subtract、multiply、divide、compare だけです。X にはコンテキスト、フラグ、特殊値、指数のコホートがないので、それらはいずれも比較しません。
  • XCompatible の除算の契約は、GDA が厳密に解析できるオペランドについてだけ成り立ちます。既知の制限を参照してください。
  • HTML のコーパス要約は総数を validation_count + failed_count、合格を validation_count と報告します。Mare Mark の validation_count はすでに失敗を含むので、失敗のある実行では要約は両方の数を過大に示します。公開された実行には失敗はありませんでした。
  • Mare Mark の実装レコードには moonbitlang/x@0.4.46 と記されていますが、モジュールは現在 moonbitlang/x@0.5.5 に依存しています。公開された計測は 0.4.46 で行われました。
  • 現在の moonbitlang/core の wasm-gc ターゲットでは、BigInt::from_string が長い入力に対して誤った値を返します。9 を 3,584 個並べた文字列ですでに誤って解析され、9 を 4,096 個並べると 4,094 桁の数になります。このパッケージは使っていませんが、テスト division precision follows the requested semantic contract は使っており、その期待値 4097 はこの誤った解析から記録されたものです。正しい値は 4099 で、native と js ターゲットはこれを計算します。
  • 実行ファイルは native ターゲットでだけ動作し、異なるターゲットの結果を合わせることはしません。