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,
}

只有基于名字的 API 才需要导入 type_theory。

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 trait 同时适用于 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)")
}

常见陷阱

  • 上下文必须匹配。 两个上下文不同时，+、- 和 * 会中止；请使用 add_checked 和 mul_checked。名字相同且顺序相同的上下文即使分别创建也相等。
  • 部分求值会把变量保留在上下文中。 不要指望结果的上下文会缩小。
  • 代换只进行一遍。 替换内容本身不会再被代换；需要链式代换时请再次调用 substitute。
  • 重复会失败。 将同一个变量或名字列出两次是错误，而不是“后者生效”。
  • 绑定信任元数。 在调用 from_term_polynomial / from_sparse_polynomial 之前检查 arity() <= context.size()。
  • 没有 ==。 请改为比较 to_sparse_polynomial() 的结果（以及 context()）。

后续步骤