Luna Flow
日本語

immut/context チュートリアル

このチュートリアルでは、名前付き変数で多項式を書き、それを変換する方法を示します。名前による評価、一部の変数だけを評価して残りを保つこと、変数への多項式の代入、そしてこれらすべてを Luna-Flow/type_theory から来た名前で行うことです。

クイックスタート

moon add Luna-Flow/luna-poly@0.2.0
import {
  "Luna-Flow/luna-poly/immut",
  "Luna-Flow/type_theory/core" @tt_core,
}

type_theory のインポートは名前ベースの API にだけ必要です。

test "context quick start" {
  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),
    ([], 4),
  ])
  inspect(p, content="4 + 1 * x^2 + 3 * x * y")
  inspect(p.eval_named([(x, 2), (y, 5)]), content="38")
}

各項は (variable, exponent) の因子のリストと係数です。[] は定数項です。

日常的なタスク

ストレージを選ぶ

降順での走査には _as_terms で、係数の検索には _as_sparse で構築します。結果は同じで、表示の順序だけが異なります。

test "storage" {
  let ctx = @immut.VariableContext::from_names(["x", "y"])
  let x = ctx.require_variable("x")
  let y = ctx.require_variable("y")
  let terms = [([(x, 1U)], 2), ([(y, 2U)], 1), ([], 7)]
  let t = @immut.ContextPolynomial::from_named_terms_as_terms(ctx, terms)
  let s = @immut.ContextPolynomial::from_named_terms_as_sparse(ctx, terms)
  inspect(t, content="1 * y^2 + 2 * x + 7")
  inspect(s, content="7 + 2 * x + 1 * y^2")
  inspect(t.eval([1, 3]) == s.eval([1, 3]), content="true")
}

演算子で構築する

定数と単一の変数は +、-、*、pow で組み合わせられます。

test "operators" {
  let ctx = @immut.VariableContext::from_names(["a", "b"])
  let a : @immut.ContextPolynomial[Int] = @immut.ContextPolynomial::variable(ctx, ctx.require_variable("a"))
  let b : @immut.ContextPolynomial[Int] = @immut.ContextPolynomial::variable(ctx, ctx.require_variable("b"))
  let p = (a + b).pow(2) - @immut.ContextPolynomial::constant(ctx, 1)
  inspect(p, content="-1 + 1 * a^2 + 2 * a * b + 1 * b^2")
}

一部の変数を評価し、他は残す

eval_partial は列挙した変数を値で置き換え、同じコンテキスト上の多項式を返します。

test "partial 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_sparse(ctx, [([(x, 1U), (y, 1U)], 3), ([(y, 2U)], 1), ([], 4)])
  let q = p.eval_partial([(x, 2)])
  inspect(q, content="4 + 6 * y + 1 * y^2")
  inspect(q.eval_named([(x, 0), (y, 5)]), content="59")
  inspect(p.eval_named([(x, 2), (y, 5)]), content="59")
}

q にはもう x が含まれていませんが、依然としてコンテキスト (x, y) に属しているため、eval_named には添字で読み取られるすべての変数を引き続き列挙します。x にどんな値を与えても結果は同じです。

変数に多項式を代入する

substitute は変数をスカラー (Scalar) または多項式 (Polynomial) で一斉に置き換えます。

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, 1U)], 1), ([(y, 1U)], 1)])
  let y_poly = @immut.ContextPolynomial::variable(ctx, y)
  let once = p.substitute([(x, Polynomial(y_poly)), (y, Scalar(2))])
  inspect(once, content="2 + 1 * y")
  let twice = once.substitute([(y, Scalar(2))])
  inspect(twice, content="4")
}

代入は同時に行われます。x は y になりますが、その新しい y が同じ呼び出しの中で 2 に置き換えられることはありません。続けるには substitute を再度呼び出してください。

type_theory の名前を使う

変数が type_theory の項から来る場合は _names 版を使います。名前は多項式のコンテキスト内で解決されます。

test "type theory names" {
  let ctx = @immut.VariableContext::from_names(["x", "y"])
  let x = ctx.require_variable("x")
  let p = @immut.ContextPolynomial::from_named_terms_as_sparse(ctx, [([(x, 2U)], 1), ([], 1)])
  let n = @tt_core.Name::new("x")
  inspect(p.eval_partial_named([(n, 3)]), content="10")
  let y_poly = @immut.ContextPolynomial::variable(ctx, ctx.require_variable("y"))
  inspect(p.substitute_names([(n, Polynomial(y_poly))]), content="1 + 1 * y^2")
  assert_true(p.substitute_names_checked([(@tt_core.Name::new("z"), Scalar(0))]) is None)
}

さらに進む

不正な入力をチェック付き形式で扱う

失敗しうるすべての演算には、None を返す _checked 形式があります。

fn try_eval(p : @immut.ContextPolynomial[Int], at : Array[(@immut.Variable, Int)]) -> String {
  match p.eval_named_checked(at) {
    Some(v) => v.to_string()
    None => "invalid assignment"
  }
}

test "checked" {
  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, 1U), (y, 1U)], 1)])
  inspect(try_eval(p, [(x, 2), (y, 3)]), content="6")
  inspect(try_eval(p, [(x, 2)]), content="invalid assignment")
  inspect(try_eval(p, [(x, 2), (y, 3), (y, 4)]), content="invalid assignment")
}

既存の添字指定の多項式を束縛する

from_term_polynomial と from_sparse_polynomial は TermPolynomial または SparsePolynomial に名前を付けます。これらは多項式がコンテキストの持つ変数より多くの変数を使わないことを信頼するので、自分で確認してください。

fn bind_checked(
  ctx : @immut.VariableContext,
  p : @immut.SparsePolynomial[Int],
) -> @immut.ContextPolynomial[Int]? {
  if p.arity() <= ctx.size() {
    Some(@immut.ContextPolynomial::from_sparse_polynomial(ctx, p))
  } else {
    None
  }
}

test "binding" {
  let ctx = @immut.VariableContext::from_names(["u"])
  let ok = @immut.SparsePolynomial::from_array([([3U], 1)])
  let too_wide = @immut.SparsePolynomial::from_array([([0U, 1], 1)])
  inspect(bind_checked(ctx, ok).unwrap(), content="1 * u^3")
  assert_true(bind_checked(ctx, too_wide) is None)
}

コンテキスト多項式に対する汎用コード

ContextOps レコードと ContextualPolynomial トレイトは、immut と mutable の両方のコンテキスト多項式で動作します。

fn[P, A] add_and_eval(ops : @immut.ContextOps[P, A], a : P, b : P, at : Array[(@immut.Variable, A)]) -> A? {
  match ops.add_checked(a, b) {
    Some(sum) => ops.eval_named_checked(sum, at)
    None => None
  }
}

test "generic" {
  let ctx = @immut.VariableContext::from_names(["x"])
  let x = ctx.require_variable("x")
  let p = @immut.ContextPolynomial::from_named_terms_as_sparse(ctx, [([(x, 1U)], 2)])
  let q = @immut.ContextPolynomial::constant(ctx, 1)
  debug_inspect(add_and_eval(@immut.ContextPolynomial::ops(), p, q, [(x, 4)]), content="Some(9)")
}

よくある落とし穴

  • コンテキストは一致しなければなりません。 2 つのコンテキストが異なると +、-、* は中断 (abort) します。add_checked と mul_checked を使ってください。同じ名前を同じ順序で持つコンテキストは、別々に作成されたものでも等しくなります。
  • 部分評価は変数をコンテキストに残します。 結果のコンテキストが縮むことを期待しないでください。
  • 代入は 1 パスです。 置換結果の中には代入されません。連鎖させるには substitute を再度呼び出してください。
  • 重複は失敗します。 変数や名前を 2 回列挙するとエラーになり、「最後のものが優先」にはなりません。
  • 束縛はアリティを信頼します。 from_term_polynomial / from_sparse_polynomial の前に arity() <= context.size() を確認してください。
  • == はありません。 代わりに to_sparse_polynomial() の結果 (と context()) を比較してください。

次のステップ