`semantic` の設計

設計目標

semantic は表現に依存せずに一つの問いに答えます。このデータはどの数を表すのか？ 二進浮動小数点数、IEEE 十進数、区間の端点を、厳密な有理数、符号付き無限大、NaN、閉区間に写すことで、異なるパッケージ、異なる精度、異なる基数で計算された値を厳密に比較できるようにします。同じ目的のために、checked のエラーも小さな共通の語彙に写されます。このパッケージはテスト、診断、プロトコルのための境界であり、算術は一切行いません。項目の一覧は API ページに、使用例はチュートリアルにあります。

数学的背景

浮動小数点数は有理数である

符号ビット $s$ 、整数係数 $c \ge 0$ 、指数 $e$ を持つ有限の二進浮動小数点数は $(-1)^{s} c\, 2^{e}$ を表し、有限の十進数は $(-1)^{s} c\, 10^{q}$ を表します。 $m = (-1)^{s} c$ と書けば、どちらも整数 $m$ 、基数 $r \ge 2$ 、整数 $k$ による $m\, r^{k}$ という形をしており、これは有理数です。

m\, r^{k} = \begin{cases} \dfrac{m\, r^{k}}{1}, & k \ge 0,\\[2ex] \dfrac{m}{r^{-k}}, & k < 0. \end{cases}

したがって有限の二進値はちょうど二進有理数 $\mathbb{Z}[1/2] = \{\, a/2^{j} : a \in \mathbb{Z}, j \in \mathbb{N} \,\}$ であり、有限の十進値はちょうど $\mathbb{Z}[1/10] = \{\, a/10^{j} \,\}$ であって、どちらも $\mathbb{Q}$ の部分環です。これが ExactRational::from_scaled_integer が計算する写像であり、 $r^{|k|}$ は BigInt で厳密に評価されます。

既約形は標準形である

すべての有理数 $x$ は、次を満たす表現 $n/d$ をちょうど一つ持ちます。

d > 0, \qquad \gcd(|n|, d) = 1 \qquad (\text{and } 0 = 0/1).

存在性。 $d' \ne 0$ である任意の $n'/d'$ から、分子と分母に $\operatorname{sgn}(d')$ を掛け、両方を $g = \gcd(|n'|, |d'|)$ で割ればよい。一意性。 両方の組が既約で $d, d' > 0$ のとき $n/d = n'/d'$ と仮定する。すると

\begin{aligned} n d' &= n' d &&\text{(cross-multiplying)}\\ d \mid n d',\ \gcd(d, n) = 1 &\implies d \mid d' &&\text{(Euclid's lemma)}\\ d' \mid n' d,\ \gcd(d', n') = 1 &\implies d' \mid d\\ d, d' > 0 &\implies d = d' \implies n = n'. \end{aligned}

ExactRational::new はまさにこの形を確立し（符号を分子に移し、gcd にはユークリッドの互除法を用い、ゼロは $0/1$ に正規化します）、フィールドは非公開なので、すべての ExactRational は既約です。その結果、二つの BigInt フィールド上の導出された構造的等価性は、そのまま有理数の等価性です: $n/d = n'/d' \iff (n, d) = (n', d')$ 。

異なる基数の値の比較

射影された二つの値の等価性は標準形によって判定されます。順序はパッケージでは提供されていませんが、この表現により 2 回の乗算で判定できます。 $b, d > 0$ である既約な $a/b$ と $c/d$ について、

\frac{a}{b} < \frac{c}{d} \iff \frac{a}{b} - \frac{c}{d} < 0 \iff \frac{ad - cb}{bd} < 0 \iff ad - cb < 0 \quad (\text{since } bd > 0),

これはチュートリアルが numerator() と denominator() を使って実装しているものです。

標準的な分母は、どの十進数が二進表現を持つかも説明します。既約な二進値の分母は $2^{j}$ であり、既約な十進値 $a/10^{j}$ は分母 $2^{u} 5^{v}$ に約分されます。既約形の一意性により、十進値が（十分な精度の）ある有限の二進浮動小数点数に等しいのは、その既約な分母が因数 $5$ を持たないとき、かつそのときに限ります。十分の一は $1/(2 \cdot 5)$ に約分されるので、それに等しい二進浮動小数点数は存在せず、binary64 の 0.1 の射影は $3602879701896397/2^{55}$ という別の数になります。¹1 Goldberg, “What every computer scientist should know about floating-point arithmetic”, ACM Computing Surveys 23(1), 1991, 基数変換の節; Knuth, TAOCP vol. 2, 4.4 節。

///|
test "a decimal has a binary equal iff its denominator has no factor 5" {
  let denominator = fn(s : @semantic.SemanticScalar) {
    match s {
      Rational(q) => q.denominator().to_string()
      _ => "none"
    }
  }
  let d = fn(text : String) {
    @semantic.SemanticScalar::from_decimal(@decimal.Decimal::from_string(text).unwrap())
  }
  let b = fn(x : Double) {
    @semantic.SemanticScalar::from_bin_float(@bin_float.BinFloat::from_double(x))
  }
  inspect(denominator(d("0.375")), content="8")
  inspect(d("0.375") == b(0.375), content="true")
  inspect(denominator(d("0.1")), content="10")
  inspect(denominator(b(0.1)), content="36028797018963968")
}

拡張有理数の組としての区間

空でない BallFloat は、 $\mathbb{Z}[1/2] \cup \{-\infty, +\infty\}$ の端点 $\ell \le u$ に対して $X = \{\, t \in \mathbb{R} : \ell \le t \le u \,\}$ を表します。IEEE 1788-2015 の集合ベースの区間と同様に、無限大の端点はその側が非有界であることを意味します。²2 IEEE 1788-2015, Standard for Interval Arithmetic, 7 節（集合ベースのフレーバー）: 区間は $\mathbb{R}$ の閉連結部分集合であり、非有界または空であってもよい。 SemanticInterval::from_ball_float は $\ell$ と $u$ をそれぞれ独立に from_bin_float で射影するので、この組は $X$ を厳密に決定します。空区間は ball_float によって $\ell = +\infty$ 、 $u = -\infty$ として格納され、射影もその逆転した組を保持します。拡張された順序において、lower > upper が成り立つのはちょうど空集合の場合です。有理数 $t$ に対する所属判定 $t \in X$ は、上で導いた種類の比較 2 回で行えます。

設計上の判断

共通の浮動小数点形式ではなく厳密な有理数

問題。 二進値と十進値を比較するには共通の領域が必要です。

選択肢。 (a) 両方を Double または幅の広い二進浮動小数点数に変換する。(b) 両方を十進文字列に変換する。(c) 両方を $\mathbb{Q}$ に射影する。

選択: (c)。 浮動小数点数への変換は丸めを伴うので、異なる二つの値が変換後に等しいと判定されることがあります（binary64 の 0.1 と十進の 0.1 はどちらも同じ Double に丸められます）。文字列比較は書式とコホートに依存します。 $\mathbb{Z}[1/2]$ と $\mathbb{Z}[1/10]$ はどちらも情報を失わずに $\mathbb{Q}$ に埋め込まれ、既約形により等価性はフィールドの比較になります。代償はサイズで、 $r^{|k|}$ は約 $|k| \log_2 r$ ビットになります。

射影が捨てるもの

射影は表される値だけを保持します。精度、十進の量子（コホート）、ゼロの符号、NaN のペイロード、符号と signaling 状態、区間の装飾、そしてすべてのフラグとコンテキストの状態を捨てます。これらは表現や計算の性質であり、具体的なパッケージが公開しています。そのいずれかを保持すると、異なるパッケージ由来の等しい二つの数が等しくないと判定されることになり、このパッケージの目的が損なわれます。

構造的等価性を持つ単一の値としての NaN

SemanticScalar は Eq を導出するので、NaN == NaN です。この型は「この計算は数を生成しなかった」を他と並ぶ一つの結果として扱うモデルであり、テストでは二つのパッケージがともにそれを生成することを表明する必要があります。NaN が自分自身と順序付けられない IEEE の比較は、具体的なパッケージと PartialOrder に残されています。

独立したエラー語彙

ArithmeticError はメッセージを持ち、認証の失敗に対しては精度や精緻化回数を含む詳細レコードを持ちますが、これらは同じ数学的失敗に対してもパッケージごとに異なります。SemanticError は種類だけを保持するので、semantic_scalar_result によって結果をパッケージ間で比較可能になります。この写像は種類の述語を固定された順序で調べ、どれにも該当しなければ UnsupportedOperation にフォールバックします。すべての ArithmeticErrorKind コンストラクタには専用の述語があるので、各種類は同じ名前の SemanticError に写されます。

単純な関数としての射影

semantic_scalar_result はトレイトでディスパッチするのではなく、射影を引数として受け取ります。 $\mathrm{Res}(T) = T + E$ 、 $\mathrm{Sem}(S) = S + E'$ とすると、この関数は

\texttt{semantic\_scalar\_result}(\cdot, f) = f + \texttt{from\_arithmetic} : T + E \longrightarrow S + E',

二つの写像の余積であり、左の被加数には $f$ を、右にはエラー写像を適用します。これは関手則 $\texttt{semantic\_scalar\_result}(r.\texttt{map}(g), f) = \texttt{semantic\_scalar\_result}(r, f \circ g)$ を満たすので、呼び出し側は一つの射影をすべてのパイプラインで再利用できます。

正しさ／不変条件

既約形。 すべての ExactRational は $d > 0$ 、 $\gcd(|n|, d) = 1$ 、 $n = 0 \Rightarrow d = 1$ を満たします。new は $d = 0$ で異常終了します。
厳密性。 有限の $x$ について $\texttt{from\_bin\_float}(x) = \texttt{Rational}([\![x]\!])$ かつ $\texttt{from\_decimal}(x) = \texttt{Rational}([\![x]\!])$ であり、何も丸められません。
等価性の健全性と完全性。 対応する二つのスカラー型のいずれかの有限な $x$ 、 $y$ について、射影が等しいのは $[\![x]\!] = [\![y]\!]$ のとき、かつそのときに限ります。これは既約形の一意性によります。
クラスの保存。 無限大は同じ符号の Infinity に、すべての NaN は NaN に、有限値は Rational に射影されます。
区間。 from_ball_float は端点の射影の組です。実数直線全体は $(-\infty, +\infty)$ を、空区間は $(+\infty, -\infty)$ を与えます。
コスト。 from_scaled_integer は厳密なべき乗を 1 回、負の指数の場合には gcd を 1 回行います。どちらもオペランドのビット長 $O(|k| \log r + \log |m|)$ の多項式時間です。

却下した代替案

ExactRational に算術を実装する。 厳密な有理数算術は別のライブラリの領分です。ここで実装すると射影を数値型として使うことを誘発しますが、射影は数値型ではありません。
SemanticScalar への Ord 風のインスタンス。 NaN と逆転した空区間は全順序の中に居場所がありません。呼び出し側が有理数を明示的に順序付けます。
符号付きゼロを保持する。 同じ数を表しているにもかかわらず、-0.0 と十進の 0 が等しくなくなってしまいます。
@decimal_gda.Decimal の射影。 現在のブランチでは提供されていません。GDA の値は文字列形式か @decimal.Decimal を経由してこのパッケージに到達します。

境界

算術、丸め、パース、書式化、交換形式へのエンコード、区間の縮小は行いません。
意味値の順序付けは行わず、等価性のみを扱います。
表現の詳細（精度、量子、符号付きゼロ、NaN のペイロードと signaling、装飾、フラグ、コンテキスト）は意図的に保存しません。
射影を持つのは BinFloat、@decimal.Decimal、BallFloat だけです。
非常に大きな指数を持つ値の射影は厳密であるがゆえに大きくなります。パッケージはそのコストに対する防御を行いません。

Goldberg, “What every computer scientist should know about floating-point arithmetic”, ACM Computing Surveys 23(1), 1991, 基数変換の節; Knuth, TAOCP vol. 2, 4.4 節。 ↩
IEEE 1788-2015, Standard for Interval Arithmetic, 7 節（集合ベースのフレーバー）: 区間は $\mathbb{R}$ の閉連結部分集合であり、非有界または空であってもよい。 ↩

semantic の設計