immut/context API

Luna-Flow/luna-poly/immut/context は、VariableContext に束縛されたイミュータブルな多変数多項式 ContextPolynomial[A] を提供します。項はコンテキストを通じて名前で変数を参照し、このパッケージは名前による評価、部分評価、およびスカラーや多項式による変数の同時代入(Luna-Flow/type_theory の名前によるものを含む)を追加します。

多項式は TermPolynomial または SparsePolynomial として格納されます。どちらにするかは構築時に選び、その選択はコストに影響しますが結果には影響しません。これらの型は immut ファサードから再エクスポートされており、例ではそれを使います。代入の数学は immut/context の設計 にあります。

ほとんどの演算は対になっています。通常の形式は契約違反で中断 (abort) し、*_checked 形式は代わりに None を返します。契約違反は各項目に記載しています。

型

ContextPolynomial

コンテキスト Γ\Gamma の変数についての多項式と、Γ\Gamma 自身との組。

type ContextPolynomial[A] derive(@debug.Debug)
pub impl[A : Eq + @luna-generic.AddMonoid] Add for ContextPolynomial[A]
pub impl[A : Eq + @luna-generic.AddMonoid + Neg] Sub for ContextPolynomial[A]
pub impl[A : Eq + @luna-generic.AddMonoid + Mul] Mul for ContextPolynomial[A]
pub impl[A : Eq + @luna-generic.Zero + Neg] Neg for ContextPolynomial[A]
pub impl[A : Show + @luna-generic.Zero] Show for ContextPolynomial[A]
pub impl[A] @core.ContextualPolynomial for ContextPolynomial[A]
pub impl[A] @core.HasArity for ContextPolynomial[A]
pub impl[A] @core.HasContext for ContextPolynomial[A]
pub impl[A] @core.HasShape for ContextPolynomial[A]
pub impl[A] @core.HasTermCount for ContextPolynomial[A]
pub impl[A] @core.IsZero for ContextPolynomial[A]

Eq インスタンスはありません。代わりに to_terms()(および context())を比較してください。

ContextSubstitutionValue

代入における 1 つの変数の置き換え先: 係数、または同じコンテキスト上の多項式。

pub(all) enum ContextSubstitutionValue[A] {
  Scalar(A)
  Polynomial(ContextPolynomial[A])
}

コンストラクタは型主導で解決されるため、代入リストの中では Scalar(2) や Polynomial(q) を修飾なしで書けます。

構築

ContextPolynomial::from_named_terms_as_terms, ContextPolynomial::from_named_terms_as_sparse

名前付きの項から多項式を構築します。各項は (variable, exponent) 因子のリストと係数からなり、項の配列または疎なマップとして格納されます。同じ変数の因子が繰り返されると指数が加算され、等しい単項式はマージされます。因子がコンテキスト外の変数を使うと中断 (abort) します。

pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::from_named_terms_as_terms(@Luna-Flow/luna-poly/core.VariableContext, Array[(Array[(@Luna-Flow/luna-poly/core.Variable, UInt)], A)]) -> Self[A]
pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::from_named_terms_as_sparse(@Luna-Flow/luna-poly/core.VariableContext, Array[(Array[(@Luna-Flow/luna-poly/core.Variable, UInt)], A)]) -> Self[A]

ContextPolynomial::from_named_terms_as_terms_checked, ContextPolynomial::from_named_terms_as_sparse_checked

上と同様ですが、因子がコンテキストに含まれない変数を使う場合は None を返します。

pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::from_named_terms_as_terms_checked(@Luna-Flow/luna-poly/core.VariableContext, Array[(Array[(@Luna-Flow/luna-poly/core.Variable, UInt)], A)]) -> Self[A]?
pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::from_named_terms_as_sparse_checked(@Luna-Flow/luna-poly/core.VariableContext, Array[(Array[(@Luna-Flow/luna-poly/core.Variable, UInt)], A)]) -> Self[A]?

ContextPolynomial::from_term_polynomial, ContextPolynomial::from_sparse_polynomial

インデックスで変数を指定する多項式をコンテキストに束縛します。多項式の変数 ii は、コンテキストのインデックス ii の変数になります。

pub fn[A] ContextPolynomial::from_term_polynomial(@Luna-Flow/luna-poly/core.VariableContext, @term.TermPolynomial[A]) -> Self[A]
pub fn[A] ContextPolynomial::from_sparse_polynomial(@Luna-Flow/luna-poly/core.VariableContext, @sparse.SparsePolynomial[A]) -> Self[A]

ContextPolynomial::constant

コンテキスト上の定数多項式 cc。疎な形式で格納されます。

pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::constant(@Luna-Flow/luna-poly/core.VariableContext, A) -> Self[A]

ContextPolynomial::variable

コンテキストの 1 つの変数だけからなる多項式。疎な形式で格納されます。コンテキストがその変数を含まない場合は中断 (abort) します。

pub fn[A : Eq + @luna-generic.AddMonoid + @luna-generic.One] ContextPolynomial::variable(@Luna-Flow/luna-poly/core.VariableContext, @Luna-Flow/luna-poly/core.Variable) -> Self[A]

ContextPolynomial::variable_checked

variable と同様ですが、コンテキスト外の変数に対しては None を返します。

pub fn[A : Eq + @luna-generic.AddMonoid + @luna-generic.One] ContextPolynomial::variable_checked(@Luna-Flow/luna-poly/core.VariableContext, @Luna-Flow/luna-poly/core.Variable) -> Self[A]?
test "construction" {
  let ctx = @immut.VariableContext::from_names(["x", "y"])
  let x = ctx.require_variable("x")
  let y = ctx.require_variable("y")
  let p = @immut.ContextPolynomial::from_named_terms_as_sparse(ctx, [
    ([(x, 2U)], 1),
    ([(x, 1U), (y, 1U)], 3),
    ([(y, 1U), (x, 1U)], 1),
    ([], 4),
  ])
  inspect(p, content="4 + 1 * x^2 + 4 * x * y")
  let q : @immut.ContextPolynomial[Int] = @immut.ContextPolynomial::variable(ctx, y)
  inspect(q, content="1 * y")
  let stranger = @immut.VariableContext::from_names(["z"]).require_variable("z")
  let missing : @immut.ContextPolynomial[Int]? = @immut.ContextPolynomial::variable_checked(ctx, stranger)
  assert_true(missing is None)
}

問い合わせと変換

ContextPolynomial::context

多項式が束縛されているコンテキストを返します。

pub fn[A] ContextPolynomial::context(Self[A]) -> @Luna-Flow/luna-poly/core.VariableContext

ContextPolynomial::to_terms

インデックスで変数を指定する項を、格納順に返します。項の格納では降順、疎な格納では昇順です。

pub fn[A] ContextPolynomial::to_terms(Self[A]) -> Array[(@Luna-Flow/luna-poly/core.ExponentVector, A)]

ContextPolynomial::to_term_polynomial, ContextPolynomial::to_sparse_polynomial

要求されたインデックス指定の格納形式で多項式を返し、必要なら変換します。コンテキストは破棄されます。

pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::to_term_polynomial(Self[A]) -> @term.TermPolynomial[A]
pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::to_sparse_polynomial(Self[A]) -> @sparse.SparsePolynomial[A]

ContextPolynomial::term_count, ContextPolynomial::arity, ContextPolynomial::is_zero, ContextPolynomial::shape

項数、使用中の変数の個数(使用されている最大のインデックスに 1 を加えた値)、項がないかどうか、そして PolynomialShape::Contextual(context~, arity~, term_count~)。

pub fn[A] ContextPolynomial::term_count(Self[A]) -> Int
pub fn[A] ContextPolynomial::arity(Self[A]) -> Int
pub fn[A] ContextPolynomial::is_zero(Self[A]) -> Bool
pub fn[A] ContextPolynomial::shape(Self[A]) -> @Luna-Flow/luna-poly/core.PolynomialShape

ContextPolynomial::to_string

コンテキストの変数名を使い、項を格納順に c * x^2 * y の形で文字列化します。ゼロは係数のゼロとして表示されます。

pub fn[A : Show + @luna-generic.Zero] ContextPolynomial::to_string(Self[A]) -> String

評価

ContextPolynomial::eval

TermPolynomial::eval と同様に、インデックスで与えた値で評価します。values[i] はコンテキストの変数 ii の値です。values.length() < arity() のときは中断 (abort) します。

pub fn[A : @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval(Self[A], Array[A]) -> A

ContextPolynomial::eval_checked

eval と同様ですが、values が arity() より短い場合は None を返します。

pub fn[A : @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval_checked(Self[A], Array[A]) -> A?

ContextPolynomial::eval_named

変数ごとに与えた値で評価します。インデックスが arity() 未満のコンテキスト変数にはちょうど 1 回ずつ値を割り当てる必要があります。それより後ろのコンテキスト変数への割り当ては受け付けられ、無視されます。コンテキスト外の変数、割り当ての欠落、重複した割り当てのいずれかがあると中断 (abort) します。

pub fn[A : @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval_named(Self[A], Array[(@Luna-Flow/luna-poly/core.Variable, A)]) -> A

ContextPolynomial::eval_named_checked

eval_named と同様ですが、同じ状況で None を返します。

pub fn[A : @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval_named_checked(Self[A], Array[(@Luna-Flow/luna-poly/core.Variable, A)]) -> A?
test "evaluation" {
  let ctx = @immut.VariableContext::from_names(["x", "y"])
  let x = ctx.require_variable("x")
  let y = ctx.require_variable("y")
  let p = @immut.ContextPolynomial::from_named_terms_as_terms(ctx, [([(x, 2U)], 1), ([(x, 1U), (y, 1U)], 3)])
  inspect(p.eval([2, 5]), content="34")
  inspect(p.eval_named([(y, 5), (x, 2)]), content="34")
  assert_true(p.eval_named_checked([(x, 2)]) is None)
  assert_true(p.eval_named_checked([(x, 2), (x, 3), (y, 5)]) is None)
}

部分評価と代入

以下のすべての形式は 同じ コンテキスト上の多項式を返します。値を割り当てた変数は単にその多項式に現れなくなります。置き換えは 1 回のパスで同時に適用されます。置き換え先の多項式にさらに代入が行われることはありません。

ContextPolynomial::substitute

列挙した各変数をスカラーまたは等しいコンテキスト上の多項式で置き換え、列挙していない変数はそのまま残します。変数がコンテキスト外にある場合、同じ変数が 2 回列挙された場合、置き換え先の多項式のコンテキストが異なる場合は中断 (abort) します。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::substitute(Self[A], Array[(@Luna-Flow/luna-poly/core.Variable, ContextSubstitutionValue[A])]) -> Self[A]

ContextPolynomial::substitute_checked

substitute と同様ですが、同じ状況で None を返します。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::substitute_checked(Self[A], Array[(@Luna-Flow/luna-poly/core.Variable, ContextSubstitutionValue[A])]) -> Self[A]?

ContextPolynomial::substitute_names

substitute と同様ですが、変数を Luna-Flow/type_theory の Name 値で指定し、多項式のコンテキスト内で解決します。名前がコンテキストにない場合も中断 (abort) します。同じ名前を持つ 2 つのエントリは重複とみなされます。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::substitute_names(Self[A], Array[(@Luna-Flow/type_theory/core.Name, ContextSubstitutionValue[A])]) -> Self[A]

ContextPolynomial::substitute_names_checked

substitute_names と同様ですが、同じ状況で None を返します。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::substitute_names_checked(Self[A], Array[(@Luna-Flow/type_theory/core.Name, ContextSubstitutionValue[A])]) -> Self[A]?

ContextPolynomial::eval_partial, ContextPolynomial::eval_partial_checked

一部の変数にスカラーを代入します。eval_partial(a) は、すべての値を Scalar で包んだ substitute であり、失敗するケースも同じです。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval_partial(Self[A], Array[(@Luna-Flow/luna-poly/core.Variable, A)]) -> Self[A]
pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval_partial_checked(Self[A], Array[(@Luna-Flow/luna-poly/core.Variable, A)]) -> Self[A]?

ContextPolynomial::eval_partial_named, ContextPolynomial::eval_partial_named_checked

type_theory の名前を使う同様の操作です。スカラー値による substitute_names に相当します。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval_partial_named(Self[A], Array[(@Luna-Flow/type_theory/core.Name, A)]) -> Self[A]
pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::eval_partial_named_checked(Self[A], Array[(@Luna-Flow/type_theory/core.Name, A)]) -> Self[A]?

代入の結果は、入力の格納形式にかかわらず常に疎な形式で格納されます。

test "substitution" {
  let ctx = @immut.VariableContext::from_names(["x", "y"])
  let x = ctx.require_variable("x")
  let y = ctx.require_variable("y")
  let p = @immut.ContextPolynomial::from_named_terms_as_sparse(ctx, [([(x, 2U)], 1), ([(y, 1U)], 1)])
  let y_plus_1 = @immut.ContextPolynomial::from_named_terms_as_sparse(ctx, [([(y, 1U)], 1), ([], 1)])
  inspect(p.substitute([(x, Polynomial(y_plus_1))]), content="1 + 3 * y + 1 * y^2")
  inspect(p.eval_partial([(x, 3)]), content="9 + 1 * y")
  let named = p.eval_partial_named([(y.to_type_theory_name(), 10)])
  inspect(named, content="10 + 1 * x^2")
  assert_true(p.substitute_checked([(x, Scalar(1)), (x, Scalar(2))]) is None)
  assert_true(p.substitute_names_checked([(@tt_core.Name::new("w"), Scalar(1))]) is None)
}

算術演算

ContextPolynomial::add, ContextPolynomial::sub, ContextPolynomial::mul, ContextPolynomial::neg

演算子 +、-、* および単項 -。二項演算子は 2 つのコンテキストが異なると中断 (abort) します。項の格納同士のオペランドからは項の格納の結果が、疎な格納同士からは疎な結果が、混在したオペランドからは疎な結果が得られます。符号反転は格納形式を保ちます。

pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::add(Self[A], Self[A]) -> Self[A]
pub fn[A : Eq + @luna-generic.AddMonoid + Neg] ContextPolynomial::sub(Self[A], Self[A]) -> Self[A]
pub fn[A : Eq + @luna-generic.AddMonoid + Mul] ContextPolynomial::mul(Self[A], Self[A]) -> Self[A]
pub fn[A : Eq + @luna-generic.Zero + Neg] ContextPolynomial::neg(Self[A]) -> Self[A]

ContextPolynomial::add_checked, ContextPolynomial::mul_checked

+ および * と同様ですが、コンテキストが異なる場合は None を返します。

pub fn[A : Eq + @luna-generic.AddMonoid] ContextPolynomial::add_checked(Self[A], Self[A]) -> Self[A]?
pub fn[A : Eq + @luna-generic.AddMonoid + Mul] ContextPolynomial::mul_checked(Self[A], Self[A]) -> Self[A]?

ContextPolynomial::pow

同じ格納形式で pep^e を返します。pow(0) は定数 1 です。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::pow(Self[A], UInt) -> Self[A]
test "arithmetic" {
  let ctx = @immut.VariableContext::from_names(["x"])
  let x = ctx.require_variable("x")
  let a = @immut.ContextPolynomial::from_named_terms_as_terms(ctx, [([(x, 1U)], 1)])
  let b = @immut.ContextPolynomial::constant(ctx, 1)
  inspect((a + b).pow(2), content="1 + 2 * x + 1 * x^2")
  let other = @immut.ContextPolynomial::constant(@immut.VariableContext::from_names(["t"]), 1)
  assert_true(a.add_checked(other) is None)
  assert_true(a.mul_checked(b) is Some(_))
}

ジェネリックなアクセス

ContextPolynomial::ops

ContextOps レコードを返します。from_terms は項の格納による多項式を構築し、eval_named_checked、add_checked、mul_checked は上記のメソッドです。

pub fn[A : Eq + @luna-generic.AddMonoid + Mul + @luna-generic.One] ContextPolynomial::ops() -> @Luna-Flow/luna-poly/core.ContextOps[Self[A], A]
test "ops" {
  let ctx = @immut.VariableContext::from_names(["x"])
  let x = ctx.require_variable("x")
  let ops = @immut.ContextPolynomial::ops()
  let p = ops.from_terms(ctx, [(@immut.ExponentVector::from_array([1U]), 2)])
  debug_inspect(ops.eval_named_checked(p, [(x, 5)]), content="Some(10)")
}

非推奨

ソース互換性のために残されている、隠されたメソッド形式:

非推奨代替
p.output(logger)to_string または文字列補間
p.to_repr()Repr(p) または debug_inspect