symbolic computation

Question

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.

Braxy

ocamllex and ocamlyacc will allow you to do this. – Visakhapatnam

It's not clear to me how I can do this using the lex an the yacc. Can you be more specific? – Braxy

I read your question wrong; nothing more. – Visakhapatnam

Answer 1

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.

Cichocki

Regarding Max/Min and their interaction with Add/Mul, the theory of Tropical Semirings might be relevant here. – Smokeproof

Indeed, the Max/Min are the troublemakers. But the fact is that they are quite important. I use the exprs to compute symbolic intervals, so for eg at intersections I need to insert a Min when I cat compare the given exprs. unions I would need to perform a max. I thought maybe restricting the problem to polynomials but then I cannot handle cases like a*b. The rewrite rules approach seems a bit easier but then you're right: proving the Church-Rosser is a mess. The semantic approach is a great idea, but I need to figure out how I can apply it in the presence of Min/Max. – Braxy

Regarding the libraries, bindings are not an option since I will perform operation on the expressions in a fix-point iteration. My intuition is that the overhead added by the foreign interface will not be acceptable. – Braxy

Are you doing polyhedral abstract interpretation ? In this case, I think there are external specialized solvers around. But you will probably have to do approximations to make the problem tractable. – Cichocki

I am doing abstract interpretation, but not a polyhedral one. That is because I aim to handle non affine expressions. More concrete, I'm trying to do a symbolic range analysis. If you know more about it, maybe you can share some approaches. I already went through Eigenmann et al solutions. – Braxy

Answer 2

The usual approach to such a problem is:

1. Start with a string, such a as "a + 1 > a"
2. Go through a lexer, and separate your input into distinct tokens: [Variable('a'); Plus; Number(1); GreaterThan; Variable('a')]
3. Parse the tokens into a syntax tree (what you have now). This is where you use the operator precedence rules: Max( Add( Var('a'), Const(1)), Var('a'))

4. Make a function that can interpret the syntax tree to obtain your final result

   let eval_expr expr = match expr with
       | Number n -> n
       | Add a b -> (eval_expr a) + (eval_expr b)
       ...
   

---

Pardon the syntax, I haven't used Ocaml in a while.

About libraries, I don't remember any out of the top of my mind, but there certainly are good ones easily available - this is the kind of task that the FP community loves doing.

Castellatus

It seems to me that you suggest a way to evaluate a symbolic expression given that you know the variables. This is pretty easy and I already know how to do it. What I need is to work with expressions containing unknown variables and be able to compare them. – Braxy

Consider highlighting the hard parts better next time :) I actually though you only needed to do the easy bits. – Castellatus