immut/context の設計

設計目標

ContextPolynomial[A] を使うと、名前付き変数で多項式を書き、評価・部分評価・代入によって変換できます。一方で算術は位置ベースのままで、項表現と疎表現を再利用します。ここは luna-poly が Luna-Flow/type_theory と接する場所でもあります。代入は type_theory の名前をキーにできますが、正規形、格納、係数の算術はこのパッケージが引き続き担います。

数学的背景

コンテキスト上の多項式

VariableContext $\Gamma = (s_0, \dots, s_{k-1})$ は変数 $x_0, \dots, x_{k-1}$ に名前を付けます。コンテキスト多項式は次を満たす組 $(\Gamma, f)$ です。

f \in R[\Gamma] := R[x_0, \dots, x_{k-1}] .

[(x, 1), (y, 2), (x, 1)] のような名前付きの項は、名前の上の自由可換モノイドの語です。コンテキストは各変数の指数をそのインデックスに加算することで、これを指数ベクトルに写します。この写像はモノイド準同型（語の連結は指数ベクトルの和）なので、同じ変数の繰り返しの因子は $x \cdot x = x^2$ のようにまとまり、因子を並べ替えても同じ単項式になります。

代入は普遍性そのものである

$R$ を可換とします。任意の多項式 $q_0, \dots, q_{k-1} \in R[\Gamma]$ に対し、 $R$ を固定し $x_i \mapsto q_i$ と送る環準同型 $\varphi : R[\Gamma] \to R[\Gamma]$ がちょうど 1 つ存在し、それは次のものです。

\varphi\Bigl(\sum_\alpha c_\alpha x^\alpha\Bigr) = \sum_\alpha c_\alpha \prod_{i} q_i^{\alpha_i} .

準同型であること。 加法性は構成から成り立ちます。単項式については

\begin{aligned} \varphi(x^\alpha x^\beta) = \varphi(x^{\alpha+\beta}) &= \prod_i q_i^{\alpha_i + \beta_i} \\ &= \prod_i q_i^{\alpha_i} \prod_i q_i^{\beta_i} && (R[\Gamma] \text{ is commutative}) \\ &= \varphi(x^\alpha)\,\varphi(x^\beta), \end{aligned}

であり、 $\varphi(fg) = \varphi(f)\varphi(g)$ の両辺は $(f, g)$ について双線形なので、この等式は単項式からすべての多項式に拡張されます。

一意であること。 $R$ を固定する準同型は、 $x^\alpha = \prod_i x_i^{\alpha_i}$ 上では乗法性によって、和の上では加法性によって決まるので、 $x_0, \dots, x_{k-1}$ での値によって決定されます。

代入 $\sigma$ は変数の部分集合 $S \subseteq \Gamma$ に置換先を割り当てます。これにより次の像が決まります。

q_i = \begin{cases} \sigma(x_i) & x_i \in S, \\ x_i & x_i \notin S, \end{cases}

ここでスカラー $a \in R$ は定数多項式 $a$ と見なし、これにより準同型 $\varphi_\sigma$ が定まります。substitute(σ) は式のとおりに項ごとに $\varphi_\sigma(f)$ を計算します。各因子 $x_i^{\alpha_i}$ は $x_i^{\alpha_i}$ （置換なし）、定数 $a^{\alpha_i}$ （スカラー）、または $q_i^{\alpha_i}$ （多項式）になります。

設計上の判断

同時・1 パスの代入

問題。 $\sigma = \{x \mapsto y,\; y \mapsto 2\}$ のとき、 $x + y$ は $y + 2$ になるべきか、 $4$ になるべきか。

選択。 同時代入です。各 $q_i$ は $\sigma$ で与えられたとおりに取り、置換先の多項式自体にはさらに代入しません。これは上の準同型 $\varphi_\sigma$ であり、したがって

\varphi_\sigma(x + y) = q_x + q_y = y + 2 .

逐次的な解釈は 2 つの準同型の合成であり、合成則

\varphi_\tau \circ \varphi_\sigma = \varphi_{\tau \cdot \sigma}, \qquad (\tau \cdot \sigma)(x_i) = \varphi_\tau\bigl(q^\sigma_i\bigr),

が成り立ちます。両辺はいずれも $R$ を固定し、すべての $x_i$ 上で一致する準同型だからです。逐次的に代入するには substitute を 2 回呼びます： $\varphi_{y \mapsto 2}(\varphi_{x \mapsto y}(x + y)) = \varphi_{y \mapsto 2}(2y) = 4$ 。同時代入を基本操作とするのは順序に依存しないからです。 $\sigma$ のエントリを並べ替えても結果は変わりません。

重複エントリは上書きではなくエラー

同じ変数を 2 回写すリストは関数 $\sigma$ を定義しません。最初または最後のエントリを選ぶ代わりに、substitute_checked は None を返します（substitute は中断します）。同じ規則が名前解決の後にも適用されるため、同じテキストを持つ 2 つの異なる Name 値や、同じ名前の 2 回の指定は拒否されます。

部分評価はコンテキストを保つ

問題。 $p \in R[x, y]$ で $x = 3$ を代入すると、結果は $x$ に依存しません。結果は $R[y]$ に置くことも、 $R[x, y]$ に留めることもできます。

選択。 eval_partial はスカラーの像だけを使う代入なので、結果は同じコンテキストの $R[\Gamma]$ に属します。代入された変数は単に次数 $0$ になります。 $\Gamma$ を保つことで、結果をコンテキストを手術することなく $\Gamma$ 上の他の多項式と足し、掛け、代入でき、部分評価と完全な評価を合成できます。 $S$ 上の部分割り当てを $a$ 、残りの変数の割り当てを $b$ と書くと、

\mathrm{ev}_b \circ \varphi_a = \mathrm{ev}_{a \cup b},

が成り立ちます。両辺は $R$ を固定する準同型 $R[\Gamma] \to R$ であり、生成元上で $x_i \in S$ なら $\mathrm{ev}_b(\varphi_a(x_i)) = \mathrm{ev}_b(a_i) = a_i$ 、そうでなければ $\mathrm{ev}_b(\varphi_a(x_i)) = \mathrm{ev}_b(x_i) = b_i$ となるからです。既に割り当てた変数に $b$ が与える値は無関係で、そのため例では部分評価の結果を x = 0 で評価しています。

`type_theory` の名前はまず変数に解決される

substitute_names と eval_partial_named は、すべての Name を VariableContext::variable_by_type_theory_name で変数に写してから、変数ベースの形を呼びます。名前の往復により、1 つのコンテキスト内ではこれは情報を失いません。v.to_type_theory_name() を解決すると v に戻ります。未知の名前があると呼び出し全体が失敗するので、タイプミスによって変数が黙って置換されずに残ることはありません。多項式には束縛子がないので、捕獲は起こりえません。

呼び出しが無効になる条件

各チェック付き演算は、ちょうど次の状況で None を返します。

演算	拒否される条件
`from_named_terms_*_checked`, `variable_checked`	変数がコンテキストに含まれていない
`eval_named_checked`	変数がコンテキスト外である。インデックスが `arity()` 未満の変数が未割り当てまたは 2 回割り当てられている
`substitute_checked`, `eval_partial_checked`	変数がコンテキスト外であるか 2 回指定されている。置換先の多項式のコンテキストが異なる
`*_names_checked`	加えて、名前がコンテキストにない
`add_checked`, `mul_checked`	コンテキストが異なる

Option の結果は呼び出しが失敗したことだけを記録します。中断する形も同じ条件を検査します。

格納は構築時に選び、結果は格納に依存しない

多項式は非公開の列挙型の背後に項配列または疎なマップとして保持され、from_named_terms_as_terms / _as_sparse によって、または既存の TermPolynomial / SparsePolynomial を束ねることで選ばれます。どちらの格納も同じ正規形の不変条件を満たすため、観測可能な結果（集合としての項、評価、代入）はすべて同じで、異なるのはコストと to_terms() の順序だけです。二項演算は両オペランドの格納が一致すればそれを保ち、混在する場合は項格納側を変換して疎な格納を使います。代入と、コンストラクタ constant および variable は疎な格納を生成します。

コンテキストは統合せず、等しいことを要求する

二項演算は等しいコンテキストを要求します。 $\Gamma$ と $\Gamma'$ を自動的に統合するには、両方を和コンテキストに埋め込み、すべての指数ベクトルを番号付け直す必要があり、同じ名前が異なる位置に現れる場合には和は一意ではありません。等しさを要求すれば、すべての演算は 1 つの環 $R[\Gamma]$ における単純な演算のままです。コンテキストは構造的に比較されるので、別々に作られた同一のコンテキストから構築した多項式は自由に組み合わせられます。

正しさ / 不変条件

コンテキストの不変条件。 コンテキスト多項式のすべての指数ベクトルの長さは $|\Gamma|$ 以下です。名前付きコンストラクタはこれを保証します。from_term_polynomial と from_sparse_polynomial は検査しないため、これに違反する多項式では eval_named(_checked) と to_string が中断します。呼び出し側は polynomial.arity() <= context.size() を保証しなければなりません。
代入は、可換な係数に対して $x_i \mapsto q_i$ となる唯一の環自己準同型 $\varphi_\sigma$ を計算します。結果は正規形です（ $x \mapsto 0$ を代入したときのように零の項は消えます）。
部分評価 は $\mathrm{ev}_b \circ \varphi_a = \mathrm{ev}_{a \cup b}$ を満たします。
名前付き評価 は、インデックス順に並べた値でのインデックス評価に等しくなります。
算術は基礎となる格納のものであり、その法則を受け継ぎます。
コスト。 代入は各項を累乗の積として評価してアキュムレータに加え、各加算でアキュムレータを再正規化します。項が $m$ 個で結果が $s$ 項のとき、加算だけで多項式の積に加えて $O(m\, s \log s)$ かかります。名前の検索はコンテキストのサイズに比例します。

採用しなかった代替案

逐次代入。 結果がエントリの順序に依存し、2 回の同時代入で表現できます。
代入済み変数の射影による除去。 結果のコンテキストが変わり、 $\Gamma$ 上の他の多項式との合成が壊れます。
重複時に最後のエントリを優先する方式。 誤りを隠してしまいます。重複を拒否すれば $\sigma$ は関数のままです。
type_theory の代入機構の利用。 その捕獲回避代入は多項式には存在しない問題を解くものであり、その項は多項式の正規形を持ちません。
暗黙のコンテキスト和。 上記のとおり一意ではなく、すべての二項演算で指数の番号付け直しが必要になります。

境界

等価性のインスタンスはありません。context() と項のリストを明示的に比較してください。
密な一変数の格納はありません。コンテキスト多項式は常に多変数です。
コンテキストからの変数の消去や、コンテキストの名前変更・並べ替えはありません。
代入が準同型になるには係数が可換である必要がありますが、コードは可換性を検査しません。
エラーは理由を持たず（Option）、from_term_polynomial / from_sparse_polynomial は引数のアリティをそのまま信頼します。