frontend/itl_expr の設計

設計目標

ITF1788 プロジェクトは、IEEE 1788-2015¹1 IEEE Std 1788-2015, IEEE Standard for Interval Arithmetic。ここで検証されるのは、集合ベースのフレーバー、装飾（decoration）（第 8 節）、およびオーバーラップ関係（第 10.6.4 節）です。の区間テストケースを ITL という小さな言語で公開しています。このパッケージはそれらのケースを ball_float に対して実行し、ball_float 適合性ページにある区間に関する主張が、外部の固定（pin）されたコーパスに裏付けられるようにします。他のフロントエンドと同様に純粋であり、テキストを受け取って結果を返すだけで、IO は行いません。

数学的背景

区間と最狭結果

集合ベースのモデルでは、区間は $\mathbb{R}$ の閉かつ連結な部分集合、すなわち空集合、実数直線全体、または $-\infty \le a \le b \le +\infty$ を満たす $[a, b]$ です（無限大の端点は開いています）。演算 $f$ と区間 $X_1, \dots, X_n$ に対し、値域は $f$ が定義される点全体にわたる $f(X_1, \dots, X_n) = \{ f(x_1, \dots, x_n) : x_i \in X_i \}$ です。数値形式 $\mathbb{F}$ （ここでは binary64）における最狭結果とは、値域の凸包を含む最小の $\mathbb{F}$ 区間です。

\operatorname{tight}_{\mathbb{F}}(f, X) = \Bigl[\, \max\{ a \in \mathbb{F} : a \le \inf f(X) \},\; \min\{ b \in \mathbb{F} : b \ge \sup f(X) \} \,\Bigr].

ITF1788 のケースは、IEEE 1788 が最狭であることを要求する演算について、この最狭区間を期待値として記載しています。したがって、端点の等価性を比較するテストは一度に 2 つのことを検査します。包含性（結果が値域を包含すること）と最狭性（どの端点も 1 ulp 以上広すぎないこと）です。

装飾

装飾付き区間とは組 $(X, d)$ であり、 $d$ は全順序 $\mathsf{com} > \mathsf{dac} > \mathsf{def} > \mathsf{trv} > \mathsf{ill}$ の要素で、 $X$ を生成した評価について分かっていることを記録します（たとえば $\mathsf{com}$ は、有界なボックス上で定義かつ連続であり、結果も有界であることを表します）。NaI（「区間ではない」）は $\mathsf{ill}$ を持つ装飾付き空集合です。演算は、入力の装飾と、そのボックス上での演算自体の装飾との最小値をとることで装飾を伝播します。

オーバーラップ状態

2 つの区間のオーバーラップ関係は 16 個の値をとります。2 つの空でない区間に対する Allen の区間代数の 13 個の関係（before、meets、overlaps、starts、containedBy、finishes、equals とそれらの逆関係）と、空の引数に対する 3 個の値です。このパッケージは、さらに NaI の引数を undefined に対応させます。

合格規則

区間値のケースで、実際の結果が $(A, d_A)$ 、期待値が $(E, d_E)$ のとき、ケースが合格するのは次の場合です。

\bigl(A = \text{NaI} \wedge E = \text{NaI}\bigr) \;\vee\; \Bigl( \operatorname{sets}(A, E) \wedge \bigl(\text{no `\_` in the expected text} \vee d_A = d_E\bigr) \Bigr),

ここで $\operatorname{sets}(A, E)$ は、両方が空であるか、両方が空でなく $\inf A = \inf E$ かつ $\sup A = \sup E$ のときに成り立ちます。端点は数値として比較します（BinFloat::compare == 0。したがって $-0 = +0$ であり、区間を実数の集合とみなす IEEE 1788 と同じです）。数値のケースは実際の数が期待される端点と等しいときに、真偽値のケースは真偽値が等しいときに、オーバーラップのケースは状態名が等しいときに合格します。

設計上の判断

公開されている `ball_float` API に対して実行する

各 ITL 演算は @ball_float.BallFloatDecorated の 1 つの公開メソッドに対応し（たとえば add は + に、sqrt は sqrt_interval に、pown は pown に、overlap は overlap_state に）、結果は BallContext::binary64() で丸められます。公開 API を通してテストすることで、コーパスは装飾のロジックを含め、ユーザーが実際に呼び出すものをそのまま検査します。

端点の読み取り

16 進数の端点 0x…p… は、整数の仮数部と 2 進指数として正確に解析され、その後作業精度に丸められます。10 進数の端点は $2p + 16$ 桁の 10 進数として解析され、 $p$ ビットへの 1 回の最近接偶数丸めで 2 進数に変換されます。有効数字が高々 $2p + 16$ 桁のリテラルでは 10 進数の解析は正確なので、端点は 1 回だけ丸められます。外向きではなく最近接に丸めるのは簡略化です。binary64 の数である端点では正確ですが、0.1 のような 10 進数の端点は最も近い binary64 の数として読まれ、それはリテラルが表す区間の内側にも外側にもなり得ます。

装飾はケースが明示する場合にのみ比較する

ITL は、集合ベースのテストには装飾なしの期待値（[4.0,6.0]）を、装飾のテストには装飾付きの期待値（[4.0,6.0]_com）を書きます。実行器は装飾なしのリテラルを $\mathsf{com}$ として解析しますが、装飾を比較するのは期待値のテキストに _ が含まれる場合のみです。そのため、集合ベースのケースが実装の付与する装飾によって不合格になることはありません。

3 種類の処理区分と厳格なサマリー

Unsupported は、ライブラリが実装していないケース（逆演算 mulRevToPair などの未知の演算や、signal 注釈付きの期待値）を表します。Diagnostic は、データを読み取れないケースを表します。RunSummary::success は、不合格のケースがある場合および診断がある場合に失敗します。固定されたコーパス中の読み取れないデータは、除外された機能ではなく、パーサーまたはコーパスの欠陥だからです。Unsupported のケースは success を失敗させません。CLI の --strict-supported は、完全なサポートを主張するフェーズについて、それらを失敗の終了コードに変えます。

正しさ／不変条件

カウンタの恒等式。 すべての結果はちょうど 1 つの処理区分を持つため、 $\text{total} = \text{executable} + \text{unsupported} + \text{diagnostic}$ かつ $\text{executable} = \text{passed} + \text{failed}$ が成り立ちます。

合格の健全性。 区間値のケースが合格すれば、実際の端点は期待される端点と等しくなります。期待値が最狭の binary64 包含区間であれば、実際の結果は値域の包含区間であり、かつ最狭でもあります。コーパスが包含のみを約束する場合（最狭ではなく accurate な演算）、合格は実装が同じ端点に到達したことを示します。

決定性。 解析と実行はテキストと precision のみに依存します。結果はケースを実行する順序に依存しないため、呼び出し側はケースを自由にフィルタリングしたり並べ替えたりできます。

全域性。 完結したすべての文はケースまたは解析診断になり、execute_case はケースの内容によって中断（abort）することはありません。読み取れない入力はすべて処理区分を通じて報告されます。

却下した代替案

包含のみの検査（ $E \subseteq A$ ）。何 ulp も広すぎる結果を受け入れてしまい、精度の退行を隠してしまいます。
常に装飾を比較すること。 集合ベースのケースは装飾について何も主張していないにもかかわらず、既定の装飾によってそれらを不合格にしてしまいます。
シグナルを合格として扱うこと。 IEEE 1788 のシグナル（たとえば UndefinedOperation）は現在の API では観測できないため、そのようなケースは黙って合格とするのではなく、未実行として報告されます。

境界

逆演算、mulRevToPair、文字列変換、例外シグナルは実行されません。
10 進数の端点は外向きではなく最近接に丸められます。
区間の結果は常に binary64 に丸められます。precision は端点の読み取り方にのみ影響します。
ブロックコメントは /* が行頭にある場合にのみ認識されます。
ファイル IO や演算のフィルタリングは行いません。どちらも cli/itl_expr_cli にあります。

IEEE Std 1788-2015, IEEE Standard for Interval Arithmetic。ここで検証されるのは、集合ベースのフレーバー、装飾（decoration）（第 8 節）、およびオーバーラップ関係（第 10.6.4 節）です。 ↩