Luna Flow
日本語

internal API

internal は数値コアが共有する厳密な整数・有理数のヘルパーを収めています。内容は、2・5・10 のべき、桁数の計算、末尾の因数の除去、明示的な丸めモードによる整数除算、10 進文字列の分割器、既約有理数、2 進有理数（dyadic）による包含区間、および認証付き初等関数の精緻化予算です。bin_float、decimal、decimal_gda、ball_float、semantic、および consistency のテストがこれを利用します。これは内部パッケージであり、Luna-Flow/floating の外部からはインポートできず、インターフェースは変更される可能性があります。そのため、例はコンパイルされません。丸めと包含の不変条件は設計ページで証明し、コアがヘルパーをどう使うかはチュートリアルで示します。

インポート（モジュール内部からのみ）：

import {
  "Luna-Flow/floating/internal",
}

@bigint.BigInt は moonbitlang/core/bigint です。インターフェースは Luna-Flow/arithmetic を @arithmetic（RoundingMode、ArithmeticError、CertificationStage、CertificationFailureReason）として表示し、@def.Sign を使います。

整数の基本

bigint_zero, bigint_one

これらの関数は BigInt の定数 00 と 11 を返します。

pub fn bigint_zero() -> @bigint.BigInt
pub fn bigint_one() -> @bigint.BigInt

abs_bigint, sign_of_bigint, compare_abs

abs_bigint(x) は ∣x∣|x|、sign_of_bigint(x) は Negative、Zero、Positive のいずれか、compare_abs(a, b) は ∣a∣|a| と ∣b∣|b| を比較します（負・ゼロ・正の Int を返します）。

pub fn abs_bigint(@bigint.BigInt) -> @bigint.BigInt
pub fn sign_of_bigint(@bigint.BigInt) -> @def.Sign
pub fn compare_abs(@bigint.BigInt, @bigint.BigInt) -> Int

べき

pow2, pow5, pow10

これらの関数は 2n2^n、5n5^n、10n10^n を返します。

pub fn pow2(Int) -> @bigint.BigInt
pub fn pow5(Int) -> @bigint.BigInt
pub fn pow10(Int) -> @bigint.BigInt

n<0n < 0 のときは異常終了します。pow2 はシフトです。pow5 と pow10 はプロセス全体で共有されるキャッシュを参照します。キャッシュは n≤18n \le 18 から始まり、必要に応じて n=4096n = 4096 まで拡張されます。それより大きいべきは毎回キャッシュせずに計算されます。

digits10

digits10(x) は ∣x∣|x| の 10 進桁数で、digits10(0) == 1 です。

pub fn digits10(@bigint.BigInt) -> Int

x≠0x \ne 0 に対しては 10d−1≤∣x∣<10d10^{d-1} \le |x| < 10^{d} を満たす唯一の dd を返します。ビット長に基づく推定値から出発し、10 のべきとの比較で補正します（10 進文字列は構築しません）。

末尾の因数

remove_factor2

remove_factor2(sig, exp) は sig から因数 2 をすべて取り除き、2 進指数を調整します。

pub fn remove_factor2(@bigint.BigInt, Int) -> (@bigint.BigInt, Int)

sig≠0\mathit{sig} \ne 0 に対しては (sig/2t,exp+t)(\mathit{sig}/2^t, \mathit{exp} + t) を返します。ここで tt は ∣sig∣|\mathit{sig}| の末尾のゼロビットの数であり、sig⋅2exp\mathit{sig} \cdot 2^{\mathit{exp}} は変わらず、新しい仮数は奇数になります。sig=0\mathit{sig} = 0 に対しては (0,0)(0, 0) を返します。

remove_factor10

remove_factor10(coeff, exp) は coeff から因数 10 をすべて取り除き、10 進指数を調整します。

pub fn remove_factor10(@bigint.BigInt, Int) -> (@bigint.BigInt, Int)

値 coeff⋅10exp\mathit{coeff} \cdot 10^{\mathit{exp}} は保たれ、新しい係数は 10 で割り切れません。ゼロに対しては (0,0)(0, 0) を返します。

trim_trailing_decimal_zeros

trim_trailing_decimal_zeros(coeff, exp, max_drop?) は末尾の 10 進のゼロを最大 max_drop 個まで取り除きます。

pub fn trim_trailing_decimal_zeros(@bigint.BigInt, Int, max_drop? : Int) -> (@bigint.BigInt, Int, Int)

c=c′⋅10kc = c' \cdot 10^{k}、e′=e+ke' = e + k を満たし、k≤k \le max_drop の制約のもとで kk が最大となる (c′,e′,k)(c', e', k) を返します。負の max_drop（デフォルトは −1-1）は無制限を意味します。ゼロに対しては (0,0,0)(0, 0, 0) を返します。上限を設けると、decNumber 流の理想指数への末尾除去のように、呼び出し側が目標の指数で止めることができます。

exact_divide_by_power_of_ten

exact_divide_by_power_of_ten(coeff, shift) は、除算が割り切れる場合は Some(coeff / 10^shift)、そうでなければ None です。

pub fn exact_divide_by_power_of_ten(@bigint.BigInt, Int) -> @bigint.BigInt?

符号は保たれます。ゼロはどの shift に対しても Some(0) になります。非ゼロの係数に対して負の shift を与えると異常終了します。

整数商の丸め

round_positive_div

round_positive_div(n, d, negative, mode) は商 n/dn/d を整数の絶対値に丸めます。

pub fn round_positive_div(@bigint.BigInt, @bigint.BigInt, Bool, @arithmetic.RoundingMode) -> @bigint.BigInt

n≥0n \ge 0 かつ d>0d > 0 が必要です（そうでなければ異常終了します）。negative は絶対値が n/dn/d である実数の商の符号であり、結果は ∣∘mode((−1)negative n/d)∣|\circ_{\text{mode}}((-1)^{\text{negative}}\, n/d)| です。ここで ∘\circ は整数への丸めを表します。

moden=qd+rn = qd + r、0≤r<d0 \le r < d に対する結果
TowardZeroqq
TowardPositiveq+[r>0∧¬negative]q + [r > 0 \wedge \neg\text{negative}]
TowardNegativeq+[r>0∧negative]q + [r > 0 \wedge \text{negative}]
AwayFromZeroq+[r>0]q + [r > 0]
ToNearestEvenq+[2r>d∨(2r=d∧q odd)]q + [2r > d \vee (2r = d \wedge q \text{ odd})]

結果が厳密（n/dn/d に等しい）であるのは、ちょうど r=0r = 0 のときです。

round_shift

round_shift(m, s, negative, mode) は、シフトで計算した round_positive_div(m, 2^s, negative, mode) です。

pub fn round_shift(@bigint.BigInt, Int, Bool, @arithmetic.RoundingMode) -> @bigint.BigInt

mm は非負であるべきです（検査されません）。s≤0s \le 0 の場合は mm をそのまま返します。

10 進文字列

split_decimal_string

split_decimal_string(text) は有限の 10 進リテラルを符号、数字列、指数に分割します。

pub fn split_decimal_string(String) -> (Bool, String, Int)?

受け付ける文法は次のとおりです。

[+|-] digit* [. digit*] [(e|E) [+|-] digit+]     with at least one mantissa digit

結果 (neg,D,q)(\mathit{neg}, D, q) は value=(−1)neg⋅D⋅10q\text{value} = (-1)^{\mathit{neg}} \cdot D \cdot 10^{q} を満たします。ここで DD は仮数部のすべての数字からなる文字列（先頭のゼロも保持）であり、qq は記述された指数から小数部の桁数を引いたものです。記述された指数は減算の前に ±1 500 000 000\pm 1\,500\,000\,000 で飽和するため、巨大な指数でも Int はオーバーフローしません。inf や nan を含め、それ以外はすべて None になります。

///|
test "split decimal string" {
  debug_inspect(@internal.split_decimal_string("-12.50e3"), content="Some((true, \"1250\", 1))")
  debug_inspect(@internal.split_decimal_string(".5"), content="Some((false, \"5\", -1))")
  debug_inspect(@internal.split_decimal_string("1e"), content="None")
}

Result のコンビネータ

result_lift2, result_lift2_checked

これらの関数は 2 つの Result を組み合わせ、最初のエラーを返します。

pub fn[A, B, E, C] result_lift2(Result[A, E], Result[B, E], (A, B) -> C) -> Result[C, E]
pub fn[A, B, E, C] result_lift2_checked(Result[A, E], Result[B, E], (A, B) -> Result[C, E]) -> Result[C, E]

result_lift2(Ok(a), Ok(b), f) は Ok(f(a, b)) です。result_lift2_checked は f(a, b) そのものを返します。left が Err ならそのエラーが返され、そうでなければ right の Err が返されます。

厳密な有理数

ExactRat

ExactRat は既約の有理数です。

pub struct ExactRat {
  // private fields
} derive(Eq)

ExactRat::new, ExactRat::numerator, ExactRat::denominator

ExactRat::new(n, d) は n/dn/d を正の分母を持つ既約分数にします。アクセサは既約化された各部分を返します。

pub fn ExactRat::new(@bigint.BigInt, @bigint.BigInt) -> Self
pub fn ExactRat::numerator(Self) -> @bigint.BigInt
pub fn ExactRat::denominator(Self) -> @bigint.BigInt

d=0d = 0 のときは異常終了します。ゼロは 0/10/1 として格納されます。形が正準なので、ExactRat に対する == は有理数としての等しさです。

ExactRat::equal, ExactRat::not_equal

これらのメソッドは正準形を比較します。== と != を使ってください。

pub fn ExactRat::equal(Self, Self) -> Bool
pub fn ExactRat::not_equal(Self, Self) -> Bool
///|
test "exact rational" {
  let r = @internal.ExactRat::new(-6N, -8N)
  inspect(r.numerator(), content="3")
  inspect(r.denominator(), content="4")
  inspect(r == @internal.ExactRat::new(9N, 12N), content="true")
}

2 進有理数による包含区間

CertifiedDyadic

CertifiedDyadic は 2 進有理数 n⋅2−sn \cdot 2^{-s} です。ここで nn は numerator_、スケール ss = scale_ は非負です。

pub struct CertifiedDyadic {
  numerator_ : @bigint.BigInt
  scale_ : Int
}

フィールドは読み取り可能です。値は new または from_int で構築してください。

CertifiedDyadic::new, from_int, numerator, scale

new(n, s) は n⋅2−sn \cdot 2^{-s}（s<0s < 0 なら異常終了）、from_int(k) は k⋅20k \cdot 2^{0} です。アクセサはフィールドを返します。

pub fn CertifiedDyadic::new(@bigint.BigInt, Int) -> Self
pub fn CertifiedDyadic::from_int(Int) -> Self
pub fn CertifiedDyadic::numerator(Self) -> @bigint.BigInt
pub fn CertifiedDyadic::scale(Self) -> Int

表現は正規化されていません。2⋅2−12 \cdot 2^{-1} と 1⋅201 \cdot 2^{0} は同じ数を表す、構造体としては異なる値です。

CertifiedDyadic::add, sub, mul, neg, compare

これらのメソッドは 2 進有理数の厳密な算術と比較です。

pub fn CertifiedDyadic::add(Self, Self) -> Self
pub fn CertifiedDyadic::sub(Self, Self) -> Self
pub fn CertifiedDyadic::mul(Self, Self) -> Self
pub fn CertifiedDyadic::neg(Self) -> Self
pub fn CertifiedDyadic::compare(Self, Self) -> Int

add と sub は大きい方のスケールに揃え、mul はスケールを加算し、compare は（表現ではなく）数を比較します。

CertifiedDyadic::round_down, CertifiedDyadic::round_up

x.round_down(s) と x.round_up(s) は、スケール ss を持つ ≤x\le x の最大の 2 進有理数と ≥x\ge x の最小の 2 進有理数、すなわち ⌊x⋅2s⌋⋅2−s\lfloor x \cdot 2^{s} \rfloor \cdot 2^{-s} と ⌈x⋅2s⌉⋅2−s\lceil x \cdot 2^{s} \rceil \cdot 2^{-s} です。

pub fn CertifiedDyadic::round_down(Self, Int) -> Self
pub fn CertifiedDyadic::round_up(Self, Int) -> Self

s<0s < 0 なら異常終了します。ss が現在のスケール以上であれば、値は厳密に表し直されます。

CertifiedInterval

CertifiedInterval[T] は包含区間として使われる順序対 lower <= upper です。

pub struct CertifiedInterval[T] {
  lower_ : T
  upper_ : T
}
pub fn[T] CertifiedInterval::new(T, T, (T, T) -> Int) -> Result[Self[T], @arithmetic.ArithmeticError]
pub fn[T] CertifiedInterval::lower(Self[T]) -> T
pub fn[T] CertifiedInterval::upper(Self[T]) -> T

new(lower, upper, compare) は、compare(lower, upper) > 0 のとき、段階 EnclosurePropagation、理由 InvalidEnclosure の認証失敗エラーを返します。

certified_dyadic_fraction

certified_dyadic_fraction(n, d, s) は n/dn/d をスケール ss の 2 つの 2 進有理数で挟みます。

pub fn certified_dyadic_fraction(@bigint.BigInt, @bigint.BigInt, Int) -> Result[CertifiedInterval[CertifiedDyadic], @arithmetic.ArithmeticError]

結果は [⌊n2s/d⌋2−s, ⌈n2s/d⌉2−s][\lfloor n 2^{s}/d \rfloor 2^{-s},\ \lceil n 2^{s}/d \rceil 2^{-s}] です。これは n/dn/d を含み、幅は 00 または 2−s2^{-s} であり、点区間になるのはちょうど d∣n2sd \mid n 2^{s} のときです。正でない dd は定義域エラーになります。

certified_dyadic_div

certified_dyadic_div(a, b, s) は 2 つの 2 進有理数の商 a/ba/b をスケール ss で挟みます。

pub fn certified_dyadic_div(CertifiedDyadic, CertifiedDyadic, Int) -> Result[CertifiedInterval[CertifiedDyadic], @arithmetic.ArithmeticError]

b=0b = 0 はゼロ除算エラーになります。それ以外の場合、結果は a/ba/b を正の分母で書いたものに certified_dyadic_fraction を適用したものです。

///|
test "one third at scale 8" {
  let third = @internal.certified_dyadic_div(
    @internal.CertifiedDyadic::from_int(1),
    @internal.CertifiedDyadic::from_int(3),
    8,
  ).unwrap()
  inspect(third.lower().numerator(), content="85") // 85/256 <= 1/3
  inspect(third.upper().numerator(), content="86") // 86/256 >= 1/3
}

精緻化予算

CertifiedRefinementBudget

CertifiedRefinementBudget は、Ziv 流の評価ループの作業精度と精緻化の回数を追跡します。

pub struct CertifiedRefinementBudget {
  work_precision : Int
  refinements_ : Int
  limit_ : Int
}

CertifiedRefinementBudget::new, next, available, precision, refinements

new(p, limit?) は作業精度 max⁡(1,p)\max(1, p)、精緻化 0 回、精緻化回数の上限 max⁡(1,limit)\max(1, \mathit{limit})（デフォルト 12）で開始します。next() は精度を max⁡(32,⌊p/2⌋)\max(32, \lfloor p/2 \rfloor) だけ増やし、精緻化を 1 回数えます。available() は精緻化の回数が limit 未満の間は真です。

pub fn CertifiedRefinementBudget::new(Int, limit? : Int) -> Self
pub fn CertifiedRefinementBudget::next(Self) -> Self
pub fn CertifiedRefinementBudget::available(Self) -> Bool
pub fn CertifiedRefinementBudget::precision(Self) -> Int
pub fn CertifiedRefinementBudget::refinements(Self) -> Int

例えば 64→96→144→21664 \to 96 \to 144 \to 216 となります。

certified_failure

certified_failure(operation, stage, reason, target_precision, budget) は、認証付き演算が断念したときに返す ArithmeticError を構築します。

pub fn certified_failure(String, @arithmetic.CertificationStage, @arithmetic.CertificationFailureReason, Int, CertifiedRefinementBudget) -> @arithmetic.ArithmeticError

エラーの詳細には、演算名、段階、理由、目標精度、および予算の現在の作業精度と精緻化回数が記録されます。

公開インターフェース全体

このスナップショットは、パッケージの生成された pkg.generated.mbti です。説明文とインターフェースが食い違う場合は、こちらが正となります。

// Generated using `moon info`, DON'T EDIT IT
package "Luna-Flow/floating/internal"

import {
  "Luna-Flow/arithmetic",
  "Luna-Flow/floating/def",
  "moonbitlang/core/bigint",
}

// Values
pub fn abs_bigint(@bigint.BigInt) -> @bigint.BigInt

pub fn bigint_one() -> @bigint.BigInt

pub fn bigint_zero() -> @bigint.BigInt

pub fn certified_dyadic_div(CertifiedDyadic, CertifiedDyadic, Int) -> Result[CertifiedInterval[CertifiedDyadic], @arithmetic.ArithmeticError]

pub fn certified_dyadic_fraction(@bigint.BigInt, @bigint.BigInt, Int) -> Result[CertifiedInterval[CertifiedDyadic], @arithmetic.ArithmeticError]

pub fn certified_failure(String, @arithmetic.CertificationStage, @arithmetic.CertificationFailureReason, Int, CertifiedRefinementBudget) -> @arithmetic.ArithmeticError

pub fn compare_abs(@bigint.BigInt, @bigint.BigInt) -> Int

pub fn digits10(@bigint.BigInt) -> Int

pub fn exact_divide_by_power_of_ten(@bigint.BigInt, Int) -> @bigint.BigInt?

pub fn pow10(Int) -> @bigint.BigInt

pub fn pow2(Int) -> @bigint.BigInt

pub fn pow5(Int) -> @bigint.BigInt

pub fn remove_factor10(@bigint.BigInt, Int) -> (@bigint.BigInt, Int)

pub fn remove_factor2(@bigint.BigInt, Int) -> (@bigint.BigInt, Int)

pub fn[A, B, E, C] result_lift2(Result[A, E], Result[B, E], (A, B) -> C) -> Result[C, E]

pub fn[A, B, E, C] result_lift2_checked(Result[A, E], Result[B, E], (A, B) -> Result[C, E]) -> Result[C, E]

pub fn round_positive_div(@bigint.BigInt, @bigint.BigInt, Bool, @arithmetic.RoundingMode) -> @bigint.BigInt

pub fn round_shift(@bigint.BigInt, Int, Bool, @arithmetic.RoundingMode) -> @bigint.BigInt

pub fn sign_of_bigint(@bigint.BigInt) -> @def.Sign

pub fn split_decimal_string(String) -> (Bool, String, Int)?

pub fn trim_trailing_decimal_zeros(@bigint.BigInt, Int, max_drop? : Int) -> (@bigint.BigInt, Int, Int)

// Errors

// Types and methods
pub struct CertifiedDyadic {
  numerator_ : @bigint.BigInt
  scale_ : Int
}
pub fn CertifiedDyadic::add(Self, Self) -> Self
pub fn CertifiedDyadic::compare(Self, Self) -> Int
pub fn CertifiedDyadic::from_int(Int) -> Self
pub fn CertifiedDyadic::mul(Self, Self) -> Self
pub fn CertifiedDyadic::neg(Self) -> Self
pub fn CertifiedDyadic::new(@bigint.BigInt, Int) -> Self
pub fn CertifiedDyadic::numerator(Self) -> @bigint.BigInt
pub fn CertifiedDyadic::round_down(Self, Int) -> Self
pub fn CertifiedDyadic::round_up(Self, Int) -> Self
pub fn CertifiedDyadic::scale(Self) -> Int
pub fn CertifiedDyadic::sub(Self, Self) -> Self

pub struct CertifiedInterval[T] {
  lower_ : T
  upper_ : T
}
pub fn[T] CertifiedInterval::lower(Self[T]) -> T
pub fn[T] CertifiedInterval::new(T, T, (T, T) -> Int) -> Result[Self[T], @arithmetic.ArithmeticError]
pub fn[T] CertifiedInterval::upper(Self[T]) -> T

pub struct CertifiedRefinementBudget {
  work_precision : Int
  refinements_ : Int
  limit_ : Int
}
pub fn CertifiedRefinementBudget::available(Self) -> Bool
pub fn CertifiedRefinementBudget::new(Int, limit? : Int) -> Self
pub fn CertifiedRefinementBudget::next(Self) -> Self
pub fn CertifiedRefinementBudget::precision(Self) -> Int
pub fn CertifiedRefinementBudget::refinements(Self) -> Int

pub struct ExactRat {
  // private fields
} derive(Eq)
pub fn ExactRat::denominator(Self) -> @bigint.BigInt
pub fn ExactRat::equal(Self, Self) -> Bool
pub fn ExactRat::new(@bigint.BigInt, @bigint.BigInt) -> Self
pub fn ExactRat::not_equal(Self, Self) -> Bool
pub fn ExactRat::numerator(Self) -> @bigint.BigInt

// Type aliases

// Traits