dzmingli_vs_floating の設計
設計目標
このパッケージは DzmingLi/decimal@0.2.2 と Luna-Flow/floating/decimal_gda@0.7.1 について二つの問いに答えます。同じ厳密な十進結果を計算するか、そして係数が数千桁に伸びたときどれだけ速く計算するか。速度は両方の答えが正しい場合にだけ報告するので、設計の中心には、ライブラリ同士が一致しているだけでは騙されない正しさの検査があります。
API ページが各項目を挙げ、チュートリアルがそれらを実行します。計測値は性能の章にあります。
数学的背景
十進値
有限の十進数とは組 (c,s)∈Z×Z で、次を表します。
v(c,s)=c⋅10−s.
写像 v は単射ではありません。(c,s) と (10c,s+1) は同じ数を表します。GDA 算術はこうした組を区別します(指数は結果の一部です)が、ベンチマークが比べるのは数です。そのため各同値類の正準な代表が必要で、このパッケージは s≥0 かつ c の末尾の 0 が最も少ない組を使います。
c=0 について ∣c∣ の十進桁数を d(c) と書くと、
10d(c)−1≤∣c∣<10d(c).
working_precision は d を ∣c∣ の十進文字列の長さとして計算するので、d(0)=1 です。
精度と 0 方向への丸め
精度 p の GDA コンテキストは、∣c∣<10p かつ e が指数範囲内にある数 c⋅10e をちょうど表現します。演算は厳密な結果 x を計算し、それをこうした数に丸めます。丸めモード Down(0 方向)では結果は次のとおりです。
roundp(x)=sgn(x)⌊∣x∣⋅10p−E(x)⌋⋅10E(x)−p,E(x)=⌊log10∣x∣⌋+1,
したがって ∣roundp(x)∣≤∣x∣ で、等号は x の有効桁数が p 以下のときに限り成り立ちます。小数部を固定の k 桁で同様に切り捨てる操作を次のように書きます。
trunck(x)=sgn(x)⌊∣x∣⋅10k⌋⋅10−k.
参照オラクルを用いた差分テスト
I1,I2 を検査対象の実装、O をオラクル、κ を等価が判定可能な集合への正準化写像とします。入力 x に対する実装 k の判定は次のとおりです。
validk(x)⟺κ(Ik(x))=κ(O(x)).
ペアごとの差分テストは κ(I1(x))=κ(I2(x)) だけを検査します。この検査は両実装が同じ誤った結果を返す共通モードの誤りを見逃し、失敗してもどちらが間違っているかを示しません。オラクルがあれば各実装を個別に判定でき、二つの不一致も判定結果で説明できます。
設計上の決定
三つの実装、計測するのはそのうち二つ
課題。 ベンチマークは「速い」と「速いが間違っている」を区別しなければなりません。選択肢。 ライブラリ間のペアごとの一致、一方のライブラリを他方の参照とする、独立したオラクル。決定。 計時の外で全データセットに対して実行する、BigInt 上の独立した厳密なオラクル(ValidationCoverage::EveryDataset)。理由。 オラクルは一行ずつ確認できるほど小さく、どちらのライブラリともコードを共有せず、4,096 桁以降の DzmingLi の 108 件の失敗を見つけました。ペアごとの一致では「ライブラリが食い違う」としか報告できなかったはずです。あるサイズが速度比のプロットに入るのは、そのサイズで両実装のすべての検証が通った場合だけです。
中立な表現と許容誤差ゼロ
課題。 二つのライブラリは結果の表記(指数表記、末尾の 0、0 の符号)が異なり、近似的な比較では本物の誤りが隠れてしまいます。決定。 すべての結果を DecimalValue に解析し、canonical_string の等価、つまり許容誤差ちょうど 0 で比較します。理由。 後述の精度契約のもとでは、ベンチマーク対象のすべての演算の結果が厳密に表現できるので、正しい実装はそれを一桁ずつ再現しなければなりません。健全性の議論は正しさと不変条件にあります。代償として、比較は指数のコホートとステータスフラグを無視します。それらは公式の decTest 監査(tools/run_dzmingli_dectest_audit.sh)がカバーします。
厳密有限オラクル
オラクルは係数に対する整数演算だけを使います。
加算と減算は両オペランドを s=max(sℓ,sr) に揃えます:
cℓ10−sℓ±cr10−sr=(cℓ10s−sℓ±cr10s−sr)10−s.
乗算は係数を掛け、スケールを足します。除算は商を整数の分数として書き、約分します。
cr10−srcℓ10−sℓ=MN,N=cℓ10sr, M=cr10sℓ,N′=gN, M′=g∣M∣, g=gcd(N,M),
そして M′ が 2 と 5 以外の素因数を持たない場合にだけ受け入れます。次に M′∣N′10k を満たす最小の k を求め、(N′10k/M′, k) を返します。整数除算、剰余、べき乗、完全平方数の平方根、FMA、単項演算はこれらの規則から導かれます。一覧はAPI ページの表にあります。
切り捨て系の規則(DivideInteger、Quantize、Rescale、ToIntegralExact、ToIntegralValue)が 0 方向に切り捨てるのは、BigInt の除算がそうだからです。GDA の quantize、rescale、to_integral_* はコンテキストのモードで丸めるので、両方のコンテキストで Down を使います。他のモードではこれらの演算でオラクルが誤ります。なお公開されたフィクスチャでは、これらの演算はいずれにせよ厳密です(次の決定を参照)。
精度契約
課題。 すべての演算は厳密な結果を保持できる精度 p で実行しなければなりません。そうすれば丸めは決して起きず、許容誤差 0 も公平になります。大きな p はただではありません。GDA の除算の仕事量は精度とともに増えうるので、過大な p は結果に不要な仕事まで計時しかねません。決定。 p はフィクスチャごとにオペランドから計算し、厳密な結果の桁数に対する最小の単純な上界にガード桁を足したもの、すなわち working_precision(op, ℓ, r) + 2 とし、Power と Fma は上書きします。理由。 以下の導出は、この上界がランナーの生成するすべてのオペランドクラスで成り立ち、さらに各オペランドも厳密に保持できるので、p での解析が丸めを起こさないことを示します。
オペランドの桁数を dℓ,dr,dt、m=max(dℓ,dr)+∣sℓ−sr∣ と書きます。ランナーが使うオペランドは次のとおりです。Add、Subtract、Multiply、Fma、Quantize、Compare はスケールがプロファイル (0,2)、(8,18)、(28,0) から来る生成オペランドを取ります。Divide、DivideInteger、Remainder はスケール 0、8、28 の生成オペランドを 2、8、25 で割ります。Power は二乗(指数 2)、SquareRoot は生成した整数の二乗を取ります。Quantize は量子 10−sℓ、Rescale は指数 −sℓ、ScaleB はシフト 0 を使い、残りの単項演算は整数を取ります。
Add/Subtract:Multiply:Power (n=2):Fma:Divide (b∈{2,8,25}):DivideInteger:Remainder:SquareRoot:Unary group:Compare:∣cℓ10s−sℓ±cr10s−sr∣<10m+10m≤10m+1∣cℓcr∣<10dℓ+dr∣cℓ2∣<102dℓ∣cℓcr10σ−sℓ−sr+ct10σ−st∣<10m′+1, m′=max(dℓ+dr,dt)+∣sℓ+sr−st∣21=5⋅10−1, 81=125⋅10−3, 251=4⋅10−2∣trunc(a/b)∣≤∣a∣<10dℓ−sℓ∣r∣≤∣a∣, scale(r)=sℓcℓ=g2, d(g)≤⌈dℓ/2⌉∣result coefficient∣≤∣cℓ∣result∈{−1,0,1}⇒ ≤m+1 digits, p=m+4⇒ ≤dℓ+dr, p=dℓ+dr+4⇒ ≤2dℓ, p=2dℓ+4⇒ p=dℓ+dr+dt+∣sℓ+sr−st∣+4≥m′+1⇒ ≤dℓ+3, p=dℓ+dr+4≥dℓ+5⇒ ≤dℓ⇒ ≤dℓ⇒ p=dℓ+4⇒ ≤dℓ, p=dℓ+4⇒ p=max(dℓ,dr)+3
表のどの p も max(dℓ,dr,dt) 以上なので、オペランド自体は厳密に解析されます。Power と Fma を上書きするのは、working_precision だけでは dℓ+dr+2、指数 2 では dℓ+3 となり、二乗を保持するには小さすぎるからです。
この契約が証明されているのはこれらのオペランドクラスについてであり、任意の入力についてではありません。一般の有限小数を与える除数 q=2α では商の係数は cℓ⋅5α で約 dℓ+0.699α 桁ですが、上界は dr≈0.301α+1 しか増えません。α=13 で上界は破れます。1/8192=0.0001220703125 は 10 桁必要ですが、p=1+4+4=9 です。このようなフィクスチャが黙って受け入れられることはなく、次節で示すとおりオラクルとの比較で拒否されます。
計時範囲
OperationOnly(arithmetic_only)は計時前に解析したオペランドに対する公開演算一回を計時します。FullPath(full_path)は加えて準備済みのコンテキストで正準オペランド文字列を解析します。これはテキストを受け取る呼び出し側が払うコストです。両範囲は同じフィンガープリントの同じデータセットを実行するので、数値は同じ入力を表します。コンテキストの構築、正準化、検証、レポートはどちらの範囲にも含まれません。
対応のある統計
Mare Mark はデータセット j、繰り返し r、ブロック b ごとに、実装ごとの較正済みレイテンシを一つ記録します。パッケージは (j,r,b) を共有する DzmingLi と GDA のサンプルを対にし、差をとります。
Δi=tiGDA−tiDZ.
サンプルを t=μimpl+βb+ε(βb はブロックに共通のドリフト。周波数の変化やキャッシュ状態など)とモデル化すると、Δi=μGDA−μDZ+(ε−ε′) となり、ブロック効果は打ち消されます。BalancedBlocks は先に走る実装を交互に入れ替えるので、順序の効果も平均すれば打ち消されます。報告される量は次のとおりです。
δ=100⋅medianitiDZmedianiΔi %,speedup=medianitiDZmedianitiGDA,
判定は δ≤−3 なら gda_faster、δ≥3 なら dzmingli_faster、それ以外は equivalent です。中央値の破綻点は 50 % なので、Mare Mark が報告はするが除去しない外れ値によって大きく動くことはありません。3% のしきい値は実用上の有意性の目安であって仮説検定ではなく、レポートには信頼区間はありません。11 Mare Mark の compare_paired は Δi の四分位範囲を区間として保存します。これは対応差のばらつきを表すもので、中央値の不確かさではありません。
サイズごとに 3 データセット、それぞれ確認用の繰り返し 20 回なので、有効なサイズには 60 組があります。
演算ごとのサイズ上限
DzmingLi の digit_count は bit_length * 30103 を 32 ビットの Int で評価します。積は次の条件でオーバーフローします。
bit_length>30103231−1≈71337⟺digits≳71337⋅log102≈21475.
n 桁のオペランド二つの積は最大 2n 桁なので、乗算、FMA、二乗は n≈10738 から限界を超えうります。そのためスケーリング用ランナーはすべての演算を 10,000 桁で止め、16,384 桁と 20,000 桁では add、subtract、divide、compare だけを実行します。これらはオーバーフロー条件から得た解析的な上界で、32,768 桁と 65,536 桁での実行では中断が再現しました。
正しさと不変条件
正準形。 c=0 について、normalize は s′≥0 かつ(s′=0 または 10∤c′)を満たす (c′,s′) を返し、各ステップは (10q,s) を (q,s−1) に置き換えるだけなので v(c′,s′)=v(c,s) です。このような二つの組が同じ数を表すのは、両者が等しいときに限ります:
c110−s1=c210−s2, s1<s2 ⇒ c2=c110s2−s1 ⇒ 10∣c2 and s2>0,
これは (c2,s2) の正規形に矛盾し、s1=s2 なら c1=c2 となります。canonical_string は符号、∣c′∣ の各桁、小数点の位置 s′ を書きますが、これらはすべて数によって決まるので、文字列の等価は数の等価です。
オラクルの除算。 N′/M′ は既約分数です。M′∣N′10k なら gcd(M′,N′)=1 より M′∣10k=2k5k なので、M′ は 2 と 5 以外の素因数を持ちません。逆に M′=2α5β なら、そのような最小の k は max(α,β) です。オラクルはループの前に因数分解を確認するのでループは停止し、返すスケールは最短の厳密なスケールです。
整数平方根。 オラクルは次を反復します。
xk+1=⌊2xk+⌊n/xk⌋⌋,x0=10⌈D/2⌉>n,
ここで D は n の桁数です。相加相乗平均の不等式 (x+n/x)/2≥n より、各反復値は ⌊n⌋ 以上です。xk>⌊n⌋ の間は n/xk<xk なので xk+1<xk です。列は ⌊n⌋ に達するまで狭義単調に減少し、そこでループが止まります。その後オラクルは x2=n を要求するので、平方数でない入力は丸めた根を出すのではなく中断します。
許容誤差 0 の健全性。 x を厳密な結果、p をフィクスチャの精度とします。
- x の有効桁数が p 以下なら、規格に準拠した GDA 演算は x に等しい数を返します。x はどの丸めモードでも自分自身が正しく丸めた値だからです。よって κ(I(x))=κ(O(x)) で、正しい実装が拒否されることはありません。
- x が p 桁を超えるなら、0 方向への丸めは ∣roundp(x)∣<∣x∣ を与えるので正準文字列が異なり、検証は失敗します。精度不足が受け入れられることはありません。
- 正準文字列の等価は数の等価なので、誤った結果が受け入れられることはありません。
精度契約は生成されるすべてのオペランドクラスについて (1) の前提を確立します。それらのクラスの外でも (2) は成り立つので、検査はフェイルクローズドになります。
決定性。 オペランドは Mare Mark のシード付き derive_seed(seed, "<operation>:<digits>", profile) から導かれ、時計は使わないので、同じシードは同じコーパスと同じフィンガープリントを再現します。generate_decimal は数字 1..9 だけを使うので、生成された係数は要求どおりの桁数を持ち、末尾に 0 を持ちません。
オラクルのコスト。 n 桁の係数では、加算は 10∣sℓ−sr∣ を掛ける桁揃えが、乗算は BigInt の積一回が、除算は GCD 一回と 10 倍 max(α,β) 回(M′=2α5β)が支配的です。いずれも計時領域の外で実行されます。
却下した代替案
- ペアごとの一致だけ。 却下:不一致の原因を特定できず、共通の誤りを見逃します。
- 一方のライブラリを他方のオラクルにする。 却下:GDA ライブラリ自体が検査対象の一つであり、ベンチマークが見つけた DzmingLi の失敗を GDA の失敗と区別できなくなります。
- 許容誤差付きの比較(ulp や相対誤差)。却下:ベンチマーク対象の結果はすべて十進で厳密なので、0 でない許容誤差は誤りを隠すだけです。
- 固定の大きな精度(105 桁など)。却下:除算の仕事量を結果に必要な分以上に増やしうるうえ、計時を任意の定数に結び付けてしまいます。
- 実行ごとにランダムなオペランド。 却下:結果は再現可能でなければならず、フィンガープリントも計時範囲をまたいで安定している必要があります。
exp、ln、log10 のスケーリングベンチマーク。 却下:恒等的なフィクスチャではアルゴリズムを動かせず、一般の結果には独立した高精度の超越関数オラクルが必要です。これらは decTest 監査だけでカバーします。
境界
- このパッケージが検査するのは数値だけです。指数のコホート、結果の末尾の 0、ステータスフラグ、NaN、無限大、符号付きゼロは比較の対象外で、decTest 監査がカバーします。
- 除算は有限小数になる除数 2、8、25 だけで試験します。循環小数の商や大きな分母はベンチマークせず、オラクルも循環小数の商を拒否します。
Parse と Format は恒等パスです。GDA の書式化は試験せず、DzmingLi の 329 件の toSci 失敗は decTest 監査が別に記録しています。
OperandShape はラベルにすぎません。コーパスはサイズごとに三つの決定的なスケールプロファイルで、ランダムな分布ではありません。
- 精度契約が証明されているのは上に挙げた生成オペランドクラスについてであり、任意の入力についてではありません。
- 実行ファイルは
native ターゲットでだけ動作し、他のターゲットではメッセージを表示して終了します。
DzmingLi/decimal@0.2.2 は非推奨となり moonbit-community/decimal に移行しています。ベンチマークは歴史的な比較のためにこれを固定しています。