符号计算

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 测试，并使它们浮动到表达式的顶部（在过程中复制内容），例如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

当然，这并不总是那么容易。我不知道用最小和最大函数给语义空间提供什么表示。

编辑：关于外部库，我不知道也不确定是否有。您也许应该寻找与其他符号代数软件的绑定，但我还没有听说过（几年前有一个关于此的简街夏季项目，但我不确定是否有任何可交付成果）。
如果您在生产应用程序中需要它，也许您应该直接考虑自己编写绑定，例如。到圣人或马克西玛。我不知道那会是什么样子。