numeric_expr の設計

設計目標

floating の適合性フロントエンドは、まったく異なる 4 つのコーパス形式（GDA .decTest、IEEE 1788 .itl、MPFR のデータファイル、Berkeley TestFloat のベクトル）を読み込み、それらを 4 つの数値型に対して実行します。numeric_expr は、「これらのオペランドにこの演算を適用する」ための共有された型付きの中間表現と 1 つの評価器を提供し、解析・数値の意味論・エラー報告を分離します。

フロントエンドはテキストを Expr に変換し、ソース位置を保持します。
バックエンドは 2 つのコールバックとして与えられ、リテラルと演算の意味を定めます。
evaluate はそれらを組み合わせ、どのノードで失敗したかを報告します。

パッケージ自体は、算術演算、数値の解析、IO、グローバル状態のいずれも含みません。

数学的背景

syntax

$L$ をリテラル（スパン付きの生のテキスト）の集合、 $O$ を演算（スパン付きの名前）の集合とします。公開コンストラクタは、次の文法の項をちょうど生成します。

e \;::=\; \mathsf{lit}(\ell) \;\mid\; \mathsf{op}(o)(e_1, \dots, e_n), \qquad \ell \in L,\; o \in O,\; n \ge 0 .

内部的には、項は Luna-Flow/type_theory パッケージの @tt_syntax.Term[Atom] として格納されます。ここで Atom は、リテラルの場合とプリミティブ演算の場合を持つ非公開の列挙型です。Expr::literal(ℓ) は Value(LiteralAtom(ℓ)) であり、Expr::invoke(o, args) は Apply(Value(PrimitiveAtom(o)), args) です。一般の Term 型には Variable と Bind の形もあり、関数の位置に任意の項を置けますが、公開コンストラクタがそれらを作ることはありません。

意味

値の集合 $V$ 、エラーの集合 $E$ 、および 2 つのコールバックを固定します。

d : L \to V + E, \qquad i : O \times V^{*} \to V + E .

EvalError[E] のエラー集合 $L \times E \;+\; O \times E \;+\; \mathrm{Span}$ を $\mathrm{Err}$ と書きます。意味 $[\![e]\!] \in V + \mathrm{Err}$ は構造的再帰によって定義されます。

\begin{aligned} [\![\mathsf{lit}(\ell)]\!] &= \begin{cases} v & \text{if } d(\ell) = v,\\ \mathsf{LiteralFailure}(\ell, x) & \text{if } d(\ell) = \mathrm{err}\ x, \end{cases}\\[4pt] [\![\mathsf{op}(o)(e_1, \dots, e_n)]\!] &= \begin{cases} [\![e_k]\!] & \text{if } [\![e_1]\!], \dots, [\![e_{k-1}]\!] \in V \text{ and } [\![e_k]\!] \in \mathrm{Err},\\ v & \text{if all } [\![e_j]\!] = v_j \in V \text{ and } i(o, v_1 \dots v_n) = v,\\ \mathsf{OperationFailure}(o, x) & \text{if all } [\![e_j]\!] = v_j \in V \text{ and } i(o, v_1 \dots v_n) = \mathrm{err}\ x . \end{cases} \end{aligned}

これは、エラーモナド $V \mapsto V + \mathrm{Err}$ における構文木の畳み込み（カタモルフィズム）であり、引数は左から右へ順に評価されます。評価器はこれをそのまま書き写したものです。evaluate_term は 3 つの形にマッチし、for ループで引数を評価し、最初の Err で返ります。

設計上の判断

数値トレイトではなくコールバック

問題。 同じ行形式が複数の数値型に対して実行され、各フロントエンドは独自の値型を必要とします。gda_expr は、10 進数・整数・真偽値・文字列からなる列挙型に評価され、それぞれが 13 個の GDA ステータスフラグを持ちます。

選択肢。 「V はリテラルを解析し演算を適用できる」といったトレイト、すべてのフロントエンドで共有する固定の値の列挙型、または 2 つの単純な関数引数。

選択。 2 つの関数引数です。MoonBit のトレイトは Self パラメータしか持たないため、トレイトは演算表をデータとして受け取れず、1 つの値型が 2 つの解釈（たとえば、同じ Decimal を IEEE のコンテキストと GDA のコンテキストで読むこと）を持つこともできません。関数は行ごとの状態も捕捉できます。gda_expr は行の GdaContext を閉包に取り込むので、同じリテラルのテキストが、それが現れるディレクティブブロックの精度と丸めで読み取られます。

`type_theory` の構文の上の不透明な `Expr`

問題。 呼び出し側は、木の格納方法に依存せずに式を構築・評価できるべきであり、パッケージは後で変数や束縛子を追加できるべきです。

選択。 Expr は非公開の @tt_syntax.Term[Atom] をラップします。type_theory は組織の構文木に対する束縛と置換を担っているので、変数と Bind は 2 つ目の木の型を作らずにそれを再利用して後から追加できます。フィールドが非公開であるため、後でコンストラクタを追加しても、Expr::literal、Expr::invoke、evaluate だけを使う呼び出し側は壊れません。

左から右への即時失敗（fail-fast）評価

問題。 複数のオペランドが不正な場合、どのエラーを報告し、処理を続行するのか。

選択。 引数は左から右へ評価され、最初のエラーが残りを評価せずに返されます。したがって報告されるエラーは決定的であり（後行順で最も左にある失敗した葉またはノード）、破棄される値に対してコールバックが実行されることはありません。ドキュメントのすべての診断を必要とするフロントエンドは、このリポジトリのフロントエンドがそうしているように、評価前の解析中にそれらを収集します。

エラーは構文ノードを保持する

LiteralFailure と OperationFailure は、メッセージだけでなく Literal や Operation そのものを保持します。ノードは生のテキストまたは名前とスパンを持ち、それがコーパスランナーの出力する内容です。コールバックのエラー E は変更されずに保持されるため、型付きのエラーが評価を経ても失われません。

正しさ／不変条件

命題 1（閉じた形）。 公開 API で構築されたすべての Expr は、Value(LiteralAtom(ℓ)) であるか、args のすべての要素が同じ 2 つの形のいずれかである Apply(Value(PrimitiveAtom(o)), args) です。したがって、そのような木に対して evaluate が UnsupportedExpression を返すことはありません。

証明。 構築に関する帰納法による。Expr::literal は 1 つ目の形を生成します。Expr::invoke(o, args) は 2 つ目の形を生成し、その引数は Expr 値の項であり、帰納法の仮定により所定の形を持ちます。evaluate_term が UnsupportedExpression を返すのは、部分項の根にある Value(PrimitiveAtom(_))、Variable、Bind、または先頭が Value(PrimitiveAtom(_)) でない Apply の場合のみであり、これらはいずれも現れません。 $\square$

命題 2（後行順の接頭辞）。 $u_1, u_2, \dots, u_N$ を木のノードを後行順（子を左から右へ、その後に親）に並べたものとします。evaluate が行うコールバック呼び出しの列は $c(u_1), c(u_2), \dots, c(u_m)$ です。ここで $c$ はリテラルに対しては decode、演算ノードに対しては invoke であり、

m = \begin{cases} N & \text{if evaluation succeeds,}\\ \min\{\, k : c(u_k) \text{ returns } \mathrm{Err} \,\} & \text{otherwise.} \end{cases}

証明の概略。 木に関する帰納法による。葉はちょうど 1 回の呼び出しを行います。 $\mathsf{op}(o)(e_1, \dots, e_n)$ に対する後行順は、 $e_1, \dots, e_n$ の後行順を連結し、その後にノード自身を続けたものです。ループは $e_1, \dots, e_n$ を順に評価します。帰納法の仮定により、それぞれは自身の後行順の呼び出しを行って最初に失敗した呼び出しで停止し、ループは子が 1 つでも失敗するとただちに返ります。すべての子が成功すれば、そのノードに対して invoke が 1 回呼び出されます。これらを連結すると主張が得られます。 $\square$

系：成功時には、decode はリテラルごとに 1 回、invoke は呼び出しノードごとに 1 回実行されます。同じノードに対してコールバックが 2 回実行されることはありません。返されるエラーはノード $u_m$ に属し、ちょうど 1 回だけラップされます（子のエラーは変更されずに返され、祖先によって再ラップされることはありません）。

命題 3（純粋性と決定性）。 evaluate は木を読み取り、2 つのコールバックを呼び出すだけです。コールバックが決定的な関数であれば、evaluate も決定的です。

計算量。 ノード数 $N$ 、高さ $h$ の木に対し、評価は高々 $N$ 回のコールバック呼び出しを行い、呼び出しノードごとに引数配列を 1 つ割り当て（合計サイズは高々 $N - 1$ ）、再帰の深さは $h$ です。Expr::invoke による構築は引数配列をコピーし、 $n$ 個の引数に対して $O(n)$ です。

却下した代替案

Expr を公開の列挙型にすること。 呼び出し側は木をパターンマッチできるようになりますが、新しい構文形式（変数、束縛子）を追加するたびに呼び出し側が壊れます。不透明な構造体はその自由を保ちます。
評価中にすべてのエラーを収集すること。 エラーの後も続行するアプリカティブな評価器は、失敗したオペランドの値をでっち上げるか演算をスキップしなければならず、後続のエラーの意味が不明確になります。代わりに、フロントエンドは評価前に解析診断を収集します。
Operation にアリティを持たせること。 宣言されたアリティは、バックエンドがいずれにせよ行わなければならない検査（オペランドの種類も検査する必要がある）を重複させるだけであり、可変長引数の演算には使えません。
再帰の代わりに明示的なスタックを使うこと。 コーパスの行は浅い（リテラルに対する 1 つの演算）ため、より単純な再帰的な畳み込みを維持しています。

境界

トークナイザ、パーサー、プリティプリンタはありません。フロントエンドがテキストを Expr に変換します。
数値型、丸め、精度、フラグ、コンテキストはありません。数値の意味論はすべてコールバックが担います。
演算のアリティや型の検査は行いません。
内部表現は保持できるものの、変数、束縛子、共有、ユーザー定義関数はまだ公開されていません。
IO、ログ出力、グローバル状態はありません。ソースのスパンは単なるデータです。
式全体の等価性判定や出力はありません。