algorithm - 符号计算

Question

我的问题:符号表达式操作。

在 +、-、*、/、min、max 等运算符的帮助下，从整数常量和变量开始构建符号表达式。更准确地说，我会用以下方式表示一个表达式(Caml 代码):

type sym_expr_t = 
  | PlusInf
  | MinusInf
  | Const of int
  | Var of var_t
  | Add of sym_expr_t * sym_expr_t
  | Sub of sym_expr_t * sym_expr_t
  | Mul of sym_expr_t * sym_expr_t
  | Div of sym_expr_t * sym_expr_t
  | Min of sym_expr_t * sym_expr_t
  | Max of sym_expr_t * sym_expr_t

我想，为了执行有用且高效的计算(例如 a + b - a = 0 或 a + 1 > a)，我需要某种范式并对其进行运算。上面的表示可能效果不太好。

有人能指出我应该如何处理这个问题吗？我不需要代码。如果我知道怎么做，那可以很容易地写出来。提供范式表示和/或构造/简化/比较算法的论文链接也会有所帮助。

此外，如果您知道可以执行此操作的 Ocaml 库，请告诉我。

Answer 1

如果你去掉 Min 和 Max，范式很简单:它们是你变量的分数域的元素，我的意思是 P[ Vars]/Q[Vars] 其中 P、Q 是多项式。对于 Min 和 Max，我不知道；我想最简单的方法是将它们视为 if/then/else 测试，并使它们 float 到表达式的顶部(在此过程中复制内容)，例如 P(Max(Q,R)) 将被重写为 P(if Q>R then Q else R)，然后在 if Q>R then P(Q) else P(R) .

我知道有两种不同的方法可以找到表达式的范式 expr :

• 定义符合您直觉的重写规则 expr -> expr，并表明它们正在规范化。这可以通过引导您知道正确的方程式来完成:从 Add(a,Add(b,c)) = Add(Add(a,b),c) 您将导出 Add(a,Add(b,c)) -> Add(Add(a,b),c) 或相反。但是你有一个方程系统，你需要展示 Church-Rosser 和归一化；确实是肮脏的生意。

• 采用更语义化的方法来为您的值提供“语义化”:expr 中的元素实际上是存在于 sem< 类型中的数学对象的符号。为 sem 的对象找到一个合适的(唯一的)表示，然后是一个评估函数 expr -> sem，最后(如果你愿意，但你不需要)例如用于相等性检查)具体化 sem -> expr。两种转换的组合自然会为您提供一个规范化过程，而不必担心例如 Add 重写的方向(您的具体化功能会自然地产生一些任意选择)。例如，对于多项式分数，语义空间将类似于:

.

  type sem = poly * poly
  and poly = (multiplicity * var * degree) list
  and multiplicity = int
  and degree = int

当然，这并不总是那么容易。我不知道用 Min 和 Max 函数赋予语义空间什么表示。

编辑:关于外部库，我不知道，我不确定是否有。您也许应该寻找与其他符号代数软件的绑定(bind)，但我还没有听说过(几年前有一个 Jane Street Summer Project，但我不确定是否产生了任何可交付成果)。
如果您需要将其用于生产应用程序，也许您应该直接考虑自己编写绑定(bind)，例如。到 Sage 或 Maxima。我不知道那会是什么样子。