core の設計

設計目標

core は luna-poly のすべての表現が共有する意味を定めます。すなわち、単項式とは何か、単項式をどの順序で並べるか、名前付き変数とは何か、そして汎用アルゴリズムがストレージを知らずに多項式について何を観測してよいか、です。密、項配列、疎、コンテキスト束縛の多項式は、イミュータブルでもミュータブルでも、すべてこれらの定義の上に構築されるため、等価性、順序、命名について慣習ではなく構成によって一致します。

数学的背景

多項式環

$R$ を可換環 (加法演算だけを考える場合は可換モノイド) とします。変数 $x_0, \dots, x_{n-1}$ の多項式とは、有限台の関数 $f : \mathbb{N}^n \to R$ であり、次のように書きます。

f = \sum_{\alpha \in \mathbb{N}^n} f_\alpha \, x^\alpha, \qquad x^\alpha = x_0^{\alpha_0} x_1^{\alpha_1} \cdots x_{n-1}^{\alpha_{n-1}} .

$x^\alpha$ が単項式、 $\alpha$ が指数ベクトルです。多項式は点ごとの加法と次の畳み込み積によって環 $R[x_0, \dots, x_{n-1}]$ をなします。

(fg)_\gamma = \sum_{\alpha + \beta = \gamma} f_\alpha \, g_\beta ,

これは $x^\alpha x^\beta = x^{\alpha + \beta}$ の双線形拡張です。言い換えると $R[x_0, \dots, x_{n-1}]$ はモノイド環 $R[\mathbb{N}^n]$ であり、単項式に関することはすべて加法モノイド $\mathbb{N}^n$ についての命題です。

固定のアリティを持たない指数ベクトル

ExponentVector は $n$ を保持しません。次の集合の元を表します。

\mathbb{N}^{(\infty)} = \{\, \alpha : \mathbb{N} \to \mathbb{N} \mid \alpha_i = 0 \text{ for all but finitely many } i \,\},

これは可算無限個の変数上の自由可換モノイドです。零による埋め込み $\iota_n(\alpha_0, \dots, \alpha_{n-1}) = (\alpha_0, \dots, \alpha_{n-1}, 0, 0, \dots)$ は単射なモノイド準同型 $\mathbb{N}^n \to \mathbb{N}^{(\infty)}$ なので、

R[x_0] \subset R[x_0, x_1] \subset \cdots \subset R[x_0, x_1, \dots] = R[\mathbb{N}^{(\infty)}]

であり、2 変数で書かれた多項式は、最後の変数を使わない 3 変数で書かれた多項式と文字どおり同じ元です。

$\alpha \neq 0$ にはそれぞれ最後の非零位置 $\ell(\alpha) = \max\{ i \mid \alpha_i \neq 0 \}$ があり、有限語 $(\alpha_0, \dots, \alpha_{\ell(\alpha)})$ が $\alpha$ を決定します。この語が ExponentVector に格納される正規形であり、単位元 $0$ は空の語として格納されます。ここから直ちに次の 2 つが従います。

正規形は一意であるため、格納された語の構造的等価性は $\mathbb{N}^{(\infty)}$ における等価性と一致します。[1, 0] == [1] となるのはこのためです。
多項式の アリティ (各項の格納長の最大値) は、 $f \in R[x_0, \dots, x_{n-1}]$ となる最小の $n$ です。

全次数 $|\alpha| = \sum_i \alpha_i$ はモノイド準同型 $\mathbb{N}^{(\infty)} \to \mathbb{N}$ であり、 $|\alpha + \beta| = |\alpha| + |\beta|$ です。ベクトルの構築時に一度だけ計算され、指数と並べて格納されます。

設計上の判断

すべての表現に共通の単項式型

問題。 密な一変数ストレージには整数のべきしか必要ありませんが、項配列、疎、コンテキスト束縛の多項式はいずれも、指数ベクトル、その上の順序、そしてハッシュを必要とします。

選択肢。 各表現が独自のキー型を定義することもできますし、1 つの共有型を core に置くこともできます。

選択。 ExponentVector は core に置かれ、両方のファサードから再エクスポートされます。そのため immut と mutable の多項式は変換なしで項をやり取りでき、等価性と順序についても一致します。ベクトルはイミュータブル (永続的な @immut/vector.Vector をラップしている) であり、そのためミュータブルなコンテナの内部でもキーとして安全に使えます。

単項式順序

問題。 項配列ストレージは項をソートされた状態に保つ必要があり、疎ストレージのソート済みマップにはキーの順序が必要です。また、先頭項が代数的に意味を持つように、その順序は 単項式順序 であるべきです。

選択。 ExponentVector::compare は次を実装します。

\alpha \prec \beta \iff |\alpha| < |\beta| \;\text{ or }\; \bigl( |\alpha| = |\beta| \text{ and } \alpha_k < \beta_k \text{ for } k = \max\{ i \mid \alpha_i \neq \beta_i \} \bigr).

全次数が等しい場合は、異なる変数のうち 添字が最大の もので決着をつけます。これは変数の優先順位 $x_0 \prec x_1 \prec x_2 \prec \cdots$ に対する次数付き辞書式順序であり、次数付き逆辞書式順序ではありません。¹1 Cox、Little、O’Shea の Ideals, Varieties, and Algorithms §2.2 では、 $x_1 > x_2 > \cdots > x_n$ に対して $\alpha - \beta$ の 最も左の 非零成分によって grlex を定義しています。ベクトルを右から読むことは、変数を逆順に並べた同じ順序になります。例えば 3 変数の次数 $2$ では、 $(1,0,1) - (0,2,0) = (1,-2,1)$ の最後の非零成分が正なので $x_0 x_2 \succ x_1^2$ となりますが、 $x_0 > x_1 > x_2$ とした次数付き逆辞書式順序では $x_1^2$ が先に来ます。

この順序は単項式順序に必要な 4 つの性質を持ちます。以下で $\mathbb{N}^{(\infty)}$ に対して導出します。

全順序である。 $\alpha \neq \beta$ かつ $|\alpha| = |\beta|$ ならば、両ベクトルとも有限台なので集合 $\{ i \mid \alpha_i \neq \beta_i \}$ は空でない有限集合であり、その最大値 $k$ が存在して $\alpha_k \neq \beta_k$ によって決まります。

乗法と両立する。 任意の $\gamma$ に対して、

\begin{aligned} |\alpha + \gamma| - |\beta + \gamma| &= |\alpha| - |\beta|, \\ (\alpha + \gamma)_i - (\beta + \gamma)_i &= \alpha_i - \beta_i \quad \text{for every } i, \end{aligned}

したがって次数の比較、異なる位置の集合、その最大値 $k$ 、および $k$ における符号はすべて変わりません。すなわち $\alpha \prec \beta \Rightarrow \alpha + \gamma \prec \beta + \gamma$ です。

単位元が最小である。 $|0| = 0 \le |\alpha|$ であり、等号は $\alpha = 0$ のときに限ります。

整列順序である。 変数が無制限に多くても成り立ちます。無限列 $\alpha^{(1)} \succ \alpha^{(2)} \succ \cdots$ が存在したと仮定します。次数は自然数の非増加列をなすので、ある $N$ 以降は定数 $d$ に等しくなります。 $m = \ell(\alpha^{(N)})$ とします。 $|\beta| = d$ かつ $\beta \prec \alpha^{(N)}$ を満たす後続の $\beta$ は、すべての $i > m$ で $\beta_i = 0$ となります。そうでなければ $\beta_j > 0$ となる最大の添字を $j > m$ とすると、2 つのベクトルは $j$ より上で一致し (どちらも零)、 $\beta_j > 0 = \alpha^{(N)}_j$ なので $k = j$ かつ $\beta \succ \alpha^{(N)}$ となり矛盾します。よって鎖の末尾は $\binom{d+m}{m}$ 個の元からなる集合 $\{ \beta \in \mathbb{N}^{m+1} \mid |\beta| = d \}$ に含まれ、有限集合内の狭義減少列は有限です。

この順序を選ぶ理由。 全次数で次数付けすると、項配列多項式の最初の項がその最高次部分になり、読み手が最初に見たいものと一致します。また、最後の変数で決着をつけることは、2 つの短いベクトルを後ろから一度走査するだけで済みます。各表現が依存しているのは乗法との両立性です。TermPolynomial::scale はすべての項に同じ単項式を掛け、配列を再ソートせずにそのまま保ちます。 $\alpha \mapsto \alpha + \gamma$ が狭義単調増加だからです。

等価性、順序、ハッシュの一致

compare が $0$ を返すのは、次数が等しくかつ異なる位置がないとき、すなわち正規形の語が等しいときに限り、これは equal と同じです。hash は次数と格納された指数を組み合わせますが、どちらも正規形の語の関数なので、等しいベクトルは等しいハッシュ値を持ちます。したがって、ソート済みマップ (compare で順序付け) とハッシュマップ (hash と equal をキーとする) は同じ単項式を同一視します。

名前はコンテキストに、位置はベクトルに

問題。 ユーザーは名前付き変数 ( $x$ 、 $y$ 、 $t$ ) で考えますが、算術には位置が必要です。

選択肢。 すべての単項式の中に名前を格納するか、単項式は位置ベースのままにして名前を別の表に置くかです。

選択。 単項式は位置ベースのままにします。VariableContext は互いに異なる名前のリスト $\Gamma = (s_0, \dots, s_{k-1})$ であり、変数 $s_i$ は組 $(s_i, i)$ です。名前が互いに異なるので、写像 $i \mapsto s_i$ と $s_i \mapsto i$ は $\{0, \dots, k-1\}$ と $\Gamma$ の名前との間の互いに逆な全単射であり、コンテキストは名前付きの項と指数ベクトルとを双方向に変換します。

添字はコンテキストの先頭から数えた位置であり、de Bruijn レベル に似ています。 $\Gamma$ を新しい名前で拡張すると末尾に追加され、既存の変数の番号が付け替えられることはありません。 $\Gamma$ から得た変数は、 $\Gamma$ のどの拡張においても意味を保ちます。

コンテキストは構造的に比較されます。同じ名前から別々に構築された 2 つのコンテキストは等しく、それらの変数は互換に使えます。これにより、コンテキストは同一性やアロケーションの追跡を必要としない単純な値のままでいられます。

`type_theory` の名前への橋渡し (構文への依存ではなく)

Luna-Flow/type_theory は、名前、束縛、代入に関する共通語彙を担っています。Variable::to_type_theory_name は変数をその名前に写し、添字を忘れます。VariableContext::variable_by_type_theory_name はコンテキスト内で名前を変数に解決し直します。前者の写像を $N(v)$ 、後者を $L_\Gamma$ と書きます。 $\Gamma$ のすべての変数 $v$ に対して、

\begin{aligned} L_\Gamma(N(v)) &= \text{the variable of } \Gamma \text{ named } v.\text{name} && \text{(definition of } L_\Gamma) \\ &= \Gamma[v.\text{index}] && \text{(names are unique, and } v \in \Gamma) \\ &= v , && \text{(}\texttt{contains}\text{ means } \Gamma[v.\text{index}] = v) \end{aligned}

であり、逆に $L_\Gamma(t)$ が定義されるときは常に $N(L_\Gamma(t)) = t$ です。したがって 1 つのコンテキスト内では名前と変数は互換であり、名前ベースの代入 API はまず名前を解決し、変数ベースの API をそのまま再利用できます。

多項式には束縛子がありません。コンテキストのすべての変数は、その上のすべての多項式において自由です。type_theory における代入の難所である捕獲回避代入は、ここでは自明になります。置換結果を捕獲しうる束縛変数が存在しないからです。そのため luna-poly は type_theory から Name だけを取り込み、項構造と正規形は独自のものを保ちます。

能力は観測であり、代数ではない

問題。 汎用コードは、ストレージ型に依存せずに「変数はいくつか、項はいくつか、零か」を問い合わせる必要があります。一方で、代数構造には luna-generic に既に独自の語彙があります。

選択。 Has* トレイトはそれぞれ 1 つの観測を公開し、バンドル UnivariatePolynomial、MultivariatePolynomial、ContextualPolynomial、MutablePolynomial がそれらを族ごとにまとめます。環演算は、具体型が実装する標準の Add、Mul、Neg、Sub、Zero、One トレイトに残します。トレイトは pub(open) なので、下流のパッケージが独自の表現に対して実装できます。

PolynomialShape は観測を比較可能にします。is_compatible_with は同値関係です。反射性と対称性は場合ごとに成り立ち、推移性は「同じコンストラクタ」が推移的であること、そして Contextual についてはコンテキストの等価性が推移的であることから従います。アリティと項数は意図的に無視されます。上述の埋め込みにより、2 つの多変数多項式は常に共通の環 $R[x_0, \dots, x_{\max(n, n') - 1}]$ に属し、2 つの一変数多項式は常に $R[x]$ に属するからです。共通の環を持てないのはコンテキスト束縛の多項式だけで、それはコンテキストが異なる場合です。

多パラメータトレイトの代わりに演算レコード

問題。 「係数 $A$ を持つ多項式型 $P$ 」上の汎用アルゴリズムには、2 つの型パラメータを持つトレイトか、関連係数型が必要です。

制約。 MoonBit のトレイトには Self しかなく、多パラメータトレイトも関連型もありません。

選択。 UnivariateOps[P, A]、MultivariateOps[P, A]、ContextOps[P, A] は関数のレコードであり、各具体型の ops() で構築されて明示的に渡されます (辞書渡し)。レコード型は両方のパラメータに言及するので、fn[P, A] f(ops : MultivariateOps[P, A], ...) のような関数は多項式と係数を関連付けられます。フィールドはプライベートで、アクセサメソッドを通じてのみ到達できるため、呼び出し側を壊さずにレコードのレイアウトを拡張できます。

チェック付き版は `Option` を返す

すべての部分的な演算には、中断 (abort) する形式と、契約違反 (負の添字、重複した名前、未知の変数) に対して None を返す *_checked 形式があります。Option は理由を持たないため、理由が必要な呼び出し側は自分で前提条件を確認します。これは、linear-algebra、arithmetic、type_theory が使う、構造化されたエラー値を持つ Result という Luna Flow の規約より前からのものです。各ページは現在の Option の契約をそのまま記述しています。

正しさ / 不変条件

正規形の指数ベクトル。 格納された語は決して $0$ で終わらず、degree は格納された指数の和に等しくなります。すべてのコンストラクタと with_exponent は切り詰め直します。
順序。 compare は $\mathbb{N}^{(\infty)}$ 上の全単項式順序かつ整列順序であり (上で導出)、equal および hash と整合します。
コンテキスト。 名前は互いに異なり、位置 $i$ の変数の添字は $i$ です。extend_checked と from_names_checked がこれを保証し、それ以外にコンテキストを構築するものはありません。
名前の往復。 $v \in \Gamma$ に対して $L_\Gamma(N(v)) = v$ 、また定義されるときは $N(L_\Gamma(t)) = t$ です。
形状の互換性 は同値関係です。
計算量。 ExponentVector の構築、mul、compare は格納長に対して $O(\ell)$ 、degree は $O(1)$ です。名前によるコンテキスト検索は線形走査で、文字列比較 $O(k)$ 回です。get と contains は、変数 1 つの比較を除いて $O(1)$ です。

採用しなかった代替案

多項式ごとに固定のアリティ。 すべてのベクトルに $n$ を持たせると、[1, 0] と [1] が同じ単項式に対して異なるキーになり、 $R[x_0]$ と $R[x_0, x_1]$ の間で明示的な持ち上げが必要になります。末尾の零を切り詰めれば、包含関係が無償で得られます。
辞書式順序。 素の lex も単項式順序ですが、次数付きではありません。項配列多項式が $x_0^{100}$ より前に $x_1$ を並べることになり、項が次数ごとにまとまりません。
単項式内の名前。 名前を格納すると、単項式の積のたびに文字列を比較することになり、算術が 1 つの命名方式に縛られます。位置ベースのベクトルとコンテキストの組み合わせなら、算術は純粋に数値的なままです。
Polynomial 万能トレイト。 構築、算術、評価をすべて担う 1 つのトレイトは係数型に言及できず、関数が実際にどの演算を必要とするかを隠してしまいます。小さな観測トレイトと明示的な演算レコードの組み合わせなら、要件を正確に表せます。
type_theory の束縛構文の実装。 多項式は何も束縛しないので、束縛の仕組みは意味を加えずに義務だけを増やします。

境界

ストレージ、算術、評価は含みません。それらは表現パッケージに属します。
指数は UInt です。単項式の積や全次数は $2^{32}$ を法として暗黙のうちにラップアラウンドし、そうなると順序はもはや乗法と両立しません。
単項式順序は 1 つしか提供されません。lex、grevlex、重み順序を選ぶ API はなく、Gröbner 基底の仕組みもありません。
コンテキストは同一性ではなく構造的に比較されます。同じ名前を同じ順序で持つ 2 つのコンテキストは同じコンテキストです。
能力トレイトは観測だけを表します。代数法則は持たず、演算レコードも保持する関数が何らかの法則を満たすかどうかを検査しません。
type_theory からは名前だけを使います。luna-poly はその束縛や書き換えのインターフェースを実装しません。

Cox、Little、O’Shea の Ideals, Varieties, and Algorithms §2.2 では、 $x_1 > x_2 > \cdots > x_n$ に対して $\alpha - \beta$ の 最も左の 非零成分によって grlex を定義しています。ベクトルを右から読むことは、変数を逆順に並べた同じ順序になります。 ↩