Search code examples
algorithmocamlsymbolic-math

symbolic computation

My problem: symbolic expression manipulation.

A symbolic expression is built starting from integer constants and variable with the help of operators like +, -, *, /, min,max. More exactly I would represent an expression in the following way (Caml code):

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

I imagine that in order to perform useful and efficient computation (eg. a + b - a = 0 or a + 1 > a) I need to have some sort of normal form and operate on it. The above representation will probably not work too good.

Can someone point me out how I should approach this? I don't necessary need code. That can be written easily if I know how. Links to papers that present representations for normal forms and/or algorithms for construction/ simplification/ comparison would also help.

Also, if you know of an Ocaml library that does this let me know.

Solution

  • If you drop out Min and Max, normal forms are easy: they're elements of the field of fractions on your variables, I mean P[Vars]/Q[Vars] where P, Q are polynomials. For Min and Max, I don't know; I suppose the simplest way is to consider them as if/then/else tests, and make them float to the top of your expressions (duplicating stuff in the process), for example P(Max(Q,R)) would be rewritten into P(if Q>R then Q else R), and then in if Q>R then P(Q) else P(R).

    I know of two different ways to find normal forms for your expressions expr :

    • Define rewrite rules expr -> expr that correspond to your intuition, and show that they are normalizing. That can be done by directing the equations that you know are true : from Add(a,Add(b,c)) = Add(Add(a,b),c) you will derive either Add(a,Add(b,c)) -> Add(Add(a,b),c) or the other way around. But then you have an equation system for which you need to show Church-Rosser and normalization; dirty business indeed.

    • Take a more semantic approach of giving a "semantic" of your values : an element in expr is really a notation for a mathematical object that lives in the type sem. Find a suitable (unique) representation for objects of sem, then an evaluation function expr -> sem, then finally (if you wish to, but you don't need to for equality checking for example) a reification sem -> expr. The composition of both transformations will naturally give you a normalization procedure, without having to worry for example about direction of the Add rewriting (some arbitrary choice will arise naturally from your reification function). For example, for polynomial fractions, the semantic space would be something like:

    .

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

    Of course, this is not always so easy. I don't see right know what representation give to a semantic space with Min and Max functions.

    Edit: Regarding external libraries, I don't know any and I'm not sure there are. You should maybe look for bindings to other symbolic algebra software, but I haven't heard of it (there was a Jane Street Summer Project about that a few years ago, but I'm not sure there was any deliverable produced).
    If you need that for a production application, maybe you should directly consider writing the binding yourselves, eg. to Sage or Maxima. I don't know what it would be like.