`def` の設計

設計目標

def は、floating の四つの表現（二進の BinFloat、IEEE 十進の @decimal.Decimal、GDA 十進の @decimal_gda.Decimal、区間の BallFloat）に対し、それらに共通する事柄のための一つの語彙を与えます。すなわち、値がどのクラスに属するか、符号は何か、どの精度で格納されているか、別の精度へどう移すか、そしてその値のどの代表元であるか、です。また IEEE 比較の結果に名前を与え、Luna-Flow/arithmetic のコンテキスト型とエラー型を再エクスポートします。このパッケージは意図的に薄く作られており、契約を述べるだけで数値アルゴリズムは一切含みません。項目の一覧は API ページに、使用例はチュートリアルにあります。

数学的背景

値とその意味

基数 $\beta$ （BinFloat では $\beta = 2$ 、二つの十進型では $\beta = 10$ ）の有限スカラーは、符号ビット $s$ 、係数 $c \in \mathbb{N}$ 、指数 $e \in \mathbb{Z}$ の三つ組であり、次の実数を表します。

[\![x]\!] = (-1)^{s}\, c\, \beta^{e}.

複数の三つ組が同じ実数を表すことがあります。基数 10 では $(0, 15, -1)$ と $(0, 150, -2)$ はどちらも $1.5$ を表し、 $(0, 0, e)$ と $(1, 0, e)$ はどちらも $0$ を表します。有限でないスカラーは $\pm\infty$ を表すか NaN であり、NaN はいかなる数も表しません。端点 $\ell \le u$ を持つ空でない BallFloat は閉集合 $X = \{\, t \in \mathbb{R} : \ell \le t \le u \,\}$ を表し（無限大の端点はその側が非有界であることを意味します）、空区間は $\varnothing$ を表します。

精度 $p \ge 1$ に対して

\mathbb{F}_{\beta,p} = \{\, (-1)^{s} c\, \beta^{e} : s \in \{0,1\},\ 0 \le c < \beta^{p},\ e \in \mathbb{Z} \,\}

を、有効な基数 $\beta$ の桁が高々 $p$ 桁で指数が非有界な数の集合とします。方向 $m$ （RoundingMode）の丸め関数 $\circ_{m,p} : \mathbb{R} \to \mathbb{F}_{\beta,p}$ は、実数を $\mathbb{F}_{\beta,p}$ の隣接する元に写します。 $\nabla$ （TowardNegative）は $\le t$ である最大の元へ、 $\Delta$ （TowardPositive）は $\ge t$ である最小の元へ、TowardZero はこの二つのうち絶対値の小さい方へ、AwayFromZero は大きい方へ、ToNearestEven は近い方へ写し、同距離の場合は係数が偶数の方を選びます。¹1 IEEE 754-2019, 4.3 節（丸め方向属性）。AwayFromZero は IEEE の二進属性ではなく、GDA の丸め Up に対応します（Cowlishaw, General Decimal Arithmetic Specification）。

IEEE の比較関係

IEEE 754 は、任意の浮動小数点データの組についてちょうど四つの関係 less than、equal、greater than、unordered のうち一つが成り立つように比較を定義しています。²2 IEEE 754-2019, 5.11 節（比較述語の詳細）および表 5.1。quiet な述語と signaling な述語の違いは quiet NaN のオペランドが無効演算を通知するかどうかだけであり、そのため bin_float は関係を BinaryFlags とともに返します。拡張実数上では最初の三つは通常の三分律であり、 $-0 = +0$ かつすべての有限な $t$ について $-\infty < t < +\infty$ です。unordered は少なくとも一方のオペランドが NaN であるとき（両方が同じ NaN である場合も含む）に限って成り立ちます。PartialOrder はこの四値の関係をデータ型にしたものです。

設計上の判断

数値の階層ではなく小さな開いたトレイト

問題。 ジェネリックなコードはどの表現に対してもいくつかの問いを発せられなければなりませんが、表現どうしは算術法則を共有していません。二進と十進の演算は異なる基数で丸め、GDA の演算はスティッキーなコンテキストを受け渡し、区間演算は丸められた点ではなく包含区間を返します。

選択肢。 (a) 算術・順序・パースを備えた広い「実数」トレイト。(b) 表現に依存しない観測と精度変更だけを持つトレイト。(c) 共有トレイトを設けない。

選択: (b)。 Floating が持つのはちょうど classify、sign、precision、with_precision、normalized だけです。算術は MoonBit の演算子トレイトと Luna-Flow/arithmetic の能力トレイト（SqrtChecked、AddContextual、…）から得られ、各型はその法則を守れる場合にのみそれを実装します。単一の広いトレイトは四つの領域すべてに一つの法則を強いることになります。例えば区間は、重なり合うオペランドについて偽ることなしにスカラーの compare を実装できません。これは、コードはその要件を述べる最小のトレイトの組み合わせに依存すべきだという Luna-Flow の原則に従ったものです。

`Sign` は二つのゼロを統合する

sign が答えるのは「値はゼロのどちら側にあるか」であって、「符号ビットは何か」ではありません。 $-0$ と $+0$ を Zero に統合することで sign は表される値の関数となり、表現間で一致し、また符号付きゼロを同じく区別しない semantic の射影とも一致します。符号ビットは具体的なパッケージを通じて引き続き観測できます。NaN は数直線上に位置を持たないので、スカラーの実装は NaN に対して Zero を返します。これを気にする呼び出し側は先に is_nan を調べてください。

区間 $X = [\ell, u]$ に対しては、同じ問いに三つの正直な答えがあり、BallFloat::sign はそれらを次のように返します。

\operatorname{sign}(X) = \begin{cases} \texttt{Positive} & \text{if } \ell > 0 \quad(\text{every member is positive}),\\ \texttt{Negative} & \text{if } u < 0 \quad(\text{every member is negative}),\\ \texttt{Zero} & \text{if } \ell \le 0 \le u \quad(0 \in X). \end{cases}

$\ell \le u$ であるため、空でない $X$ に対してこの三つの場合は網羅的かつ互いに排他的です。 $\ell > 0$ でも $u < 0$ でもなければ、 $\ell \le 0 \le u$ となります。したがって区間における Zero は「ゼロを含む」を意味し、sign を通じて定義される is_zero もその意味を受け継ぎます。

`PartialOrder` は IEEE の四通りの関係である

問題。 比較結果は NaN のオペランドに対しても表現できなければなりません。

選択肢。 (a) MoonBit の Compare を通じて Int を返す。(b) Option[Int] を返す。(c) 四値の列挙型を返す。

選択: (c)。 浮動小数点データ上の「以下」を $\preceq$ とします。これは集合全体の上の順序ではありません。

\begin{aligned} &\text{reflexivity fails:} && \mathrm{NaN} \preceq \mathrm{NaN} \text{ is false, since the pair is unordered;}\\ &\text{totality fails:} && \text{neither } 1 \preceq \mathrm{NaN} \text{ nor } \mathrm{NaN} \preceq 1;\\ &\text{antisymmetry fails on data:} && -0 \preceq +0 \text{ and } +0 \preceq -0, \text{ but } -0 \ne +0 \text{ as data.} \end{aligned}

NaN でないデータに制限すると $\preceq$ は反射的・推移的・全域的であり、したがって全前順序であって、「等しい」による商は拡張実数の全順序になります。NaN を含めると前順序ですらないので、Int 値の Compare インスタンスでは法則を守ってこれを表現できません。順序付けられない組にどの整数を選んでも、それに基づくソートは NaN を比較可能なものとして扱ってしまいます。明示的な Unordered を持つ列挙型は情報を保持し、呼び出し側に match でそれを処理することを強制します。Option[Int] も同じ情報を運べますが、「答えなし」に不在という一般的な意味を与えてしまい、名前も失われます。

具体的なパッケージは、それを必要とする用途のために、全順序である関係も追加で提供しています。BinFloat::total_order は IEEE の totalOrder 述語（5.10 節）を実装し、BinFloat::compare（Compare インスタンス）はすべての NaN をすべての数より上に置く全前順序です。これらは PartialOrder とは異なる関係であり、呼び出し箇所ごとに選択します。

算術型の再エクスポート

ArithmeticContext、ArithmeticError、RoundingMode、FpClass および認証の型は Luna-Flow/arithmetic が所有しており、同パッケージは floating が実装する contextual トレイトと checked トレイトを定義しています。def はそれらに似たものを定義するのではなく pub using で再エクスポートするので、@def.RoundingMode の値はそのまま @lf_arith.RoundingMode の値であり、二つのリポジトリの間に変換層は存在しません。

正しさ／不変条件

`Floating` の法則

以下の法則はトレイトの契約です。値 $x$ 、精度 $p$ 、方向 $m$ について述べ、 $q = \max(1, p)$ とします。このリポジトリの四つの実装はこれらを満たしており、下流の実装も満たすことが期待されます。

\begin{aligned} &\textbf{(F1) partition} && \text{exactly one of } \texttt{is\_finite}(x),\ \texttt{is\_infinite}(x),\ \texttt{is\_nan}(x) \text{ holds;}\\ &\textbf{(F2) sign} && \texttt{classify}(x) \ne \texttt{NaN} \implies \texttt{sign}(x) \text{ is given by the side of } 0 \text{ on which } [\![x]\!] \text{ lies;}\\ &\textbf{(F3) precision} && \texttt{precision}(x) \ge 1;\\ &\textbf{(F4) re-precision} && \texttt{precision}(\texttt{with\_precision}(x, p, m)) = q;\\ &\textbf{(F5) rounding} && x \text{ a finite scalar} \implies [\![\texttt{with\_precision}(x,p,m)]\!] = \circ_{m,q}([\![x]\!]);\\ &\textbf{(F6) enclosure} && x \text{ an interval} \implies [\![x]\!] \subseteq [\![\texttt{with\_precision}(x,p,m)]\!];\\ &\textbf{(F7) normal form} && [\![\texttt{normalized}(x)]\!] = [\![x]\!],\quad \texttt{normalized}(\texttt{normalized}(x)) = \texttt{normalized}(x). \end{aligned}

有限でないスカラーに対しては、with_precision はクラスと符号を保ち、格納される精度だけを変えるので、(F4) は引き続き成り立ちます。区間に対する (F2) は上で導いた三つの場合の規則です。スカラーに対しては、 $[\![x]\!] = 0$ のとき「 $0$ のどちら側か」は Zero です。

BallFloat で (F6) が成り立つ理由。 中心 $c$ 、半径 $r$ の有界なボールに対し、with_precision は $\tilde c = \circ_{m,q}(c)$ を計算し、誤差 $|c - \tilde c|$ と半径を上向きに丸めて $\tilde e \ge |c-\tilde c|$ と $\tilde r \ge r$ を得て、それらを上向き丸めで加えて $R \ge \tilde r + \tilde e$ とし、 $[\nabla(\tilde c - R), \Delta(\tilde c + R)]$ を格納します。 $|t - c| \le r$ を満たす任意の元 $t$ について、

|t - \tilde c| \le |t - c| + |c - \tilde c| \le r + |c - \tilde c| \le \tilde r + \tilde e \le R,

したがって $\nabla(\tilde c - R) \le \tilde c - R \le t \le \tilde c + R \le \Delta(\tilde c + R)$ です。方向 $m$ は中心を動かすだけであり、包含はすべての $m$ について成り立ちます。非有界な区間は下端を下向きに、上端を上向きに丸めるので、自明に包含します。

(F5) の帰結

丸めはその値域上で恒等写像です。 $t \in \mathbb{F}_{\beta,q}$ ならば、 $t$ は自分自身の隣接元なので、すべての方向について $\circ_{m,q}(t) = t$ です。したがって

[\![x]\!] \in \mathbb{F}_{\beta,q} \implies [\![\texttt{with\_precision}(x, p, m)]\!] = [\![x]\!],

であり、特に $p \le p'$ のとき $\mathbb{F}_{\beta,p} \subseteq \mathbb{F}_{\beta,p'}$ なので、精度を上げても値は決して変わりません。

一般には、精度を二段階で下げることは一度に下げることと同じではありません。方向付き丸めモードでは同じになります。 $q \le p$ かつ $m =$ TowardZero とし、 $\circ_{m,k}$ を $\circ_k$ と書き、 $a = \circ_q(t)$ 、すなわち $t$ と同じ符号を持ち絶対値が $|t|$ を超えない最大の $\mathbb{F}_{\beta,q}$ の元とします。このとき

\begin{aligned} a \in \mathbb{F}_{\beta,q} \subseteq \mathbb{F}_{\beta,p},\ |a| \le |t| &\implies |a| \le |\circ_p(t)| \le |t| && \text{(definition of } \circ_p\text{)}\\ b \in \mathbb{F}_{\beta,q},\ |b| \le |\circ_p(t)| &\implies |b| \le |t| \implies |b| \le |a| && \text{(definition of } a\text{)}\\ &\implies \circ_q(\circ_p(t)) = a = \circ_q(t). \end{aligned}

「 $\le t$ である最大の元」を用いた同じ議論は $\nabla$ と $\Delta$ にも通用します。ToNearestEven ではこの恒等式は成り立ちません（二重丸め）。³3 Muller et al., Handbook of Floating-Point Arithmetic, 2nd ed., 2018, 3.2 節（二重丸め）; Goldberg, “What every computer scientist should know about floating-point arithmetic”, 1991. 二進で $t = 1.0100001_2 = 161/128$ を考えます。 $p = 3$ では隣接元は $1.25$ と $1.5$ であり、 $t$ は $1.25$ に丸められますが、これは $q = 2$ の隣接元 $1$ と $1.5$ のちょうど中間です。同距離なので係数が偶数の $1$ が選ばれます。一方、 $t > 1.25$ なので $t$ を直接 2 ビットに丸めると $1.5$ になります。

///|
test "double rounding to nearest differs from one rounding" {
  let t = @bin_float.BinFloat::from_double(1.2578125)
  let nearest = @lf_arith.RoundingMode::ToNearestEven
  let twice = @def.Floating::with_precision(
    @def.Floating::with_precision(t, 3, nearest),
    2,
    nearest,
  )
  let once = @def.Floating::with_precision(t, 2, nearest)
  inspect(twice.to_string(), content="1p0")
  inspect(once.to_string(), content="3p-1")
  let toward_zero = @lf_arith.RoundingMode::TowardZero
  let twice_rz = @def.Floating::with_precision(
    @def.Floating::with_precision(t, 3, toward_zero),
    2,
    toward_zero,
  )
  let once_rz = @def.Floating::with_precision(t, 2, toward_zero)
  inspect(twice_rz.to_string() == once_rz.to_string(), content="true")
}

述語

四つの述語は classify と sign の射影なので、その正しさは (F1) と (F2) に帰着します。is_zero は先に classify を評価し、短絡評価の && を使います。そのため NaN クラスの値に対して sign を呼ぶことはなく、BallFloat::sign が空区間で異常終了するにもかかわらず、空区間上でも全域的です。

コスト

def のすべての項目は、委譲先の実装を除けば定数時間です。with_precision と normalized のコストは、具体的なパッケージの丸めまたは末尾ゼロ除去のコストに等しく、十進では係数の桁数に、二進では係数のビット長に線形です。

却下した代替案

算術を備えた Real スーパートレイト。 丸め算術や区間算術が満たさない法則（結合則、全順序）を主張することになり、厳密・丸め・包含の各演算の違いを隠してしまいます。
IEEE 比較に Compare を使う。 Int の結果では unordered を表現できません。上の導出を参照してください。
NegativeZero / PositiveZero という別々の符号。 sign が値ではなく表現に依存するようになり、区間の符号には対応するものがありません。
RoundingMode と ArithmeticContext のローカルなコピーを定義する。 Luna-Flow/arithmetic とのあらゆる境界で変換が必要になります。

境界

ここでは算術、パース、書式化、比較のいずれも実装しません。def は結果（Sign、PartialOrder）に名前を付け、契約を述べるだけです。
Floating は、体、全順序、IEEE 形式、厳密な算術、あるいはいかなるエラー挙動も含意しません。ジェネリックなコードは、使用する追加の能力トレイトを要求しなければなりません。
with_precision は指数の境界を守らず、フラグも報告しません。コンテキストとフラグは、具体的なパッケージの *_ctx API と Luna-Flow/arithmetic の contextual トレイトの役割です。
Sign はゼロや NaN の符号ビットを公開しません。
法則は文書化され、実装によってテストされていますが、トレイトが下流の実装に対してそれを強制することはありません。

IEEE 754-2019, 4.3 節（丸め方向属性）。AwayFromZero は IEEE の二進属性ではなく、GDA の丸め Up に対応します（Cowlishaw, General Decimal Arithmetic Specification）。 ↩
IEEE 754-2019, 5.11 節（比較述語の詳細）および表 5.1。quiet な述語と signaling な述語の違いは quiet NaN のオペランドが無効演算を通知するかどうかだけであり、そのため bin_float は関係を BinaryFlags とともに返します。 ↩
Muller et al., Handbook of Floating-Point Arithmetic, 2nd ed., 2018, 3.2 節（二重丸め）; Goldberg, “What every computer scientist should know about floating-point arithmetic”, 1991. ↩

def の設計