символьное вычисление

Моя проблема: манипулирование символьными выражениями.

Символьное выражение строится, исходя из целочисленных констант и переменных, с помощью операторов типа +, -, *, /, 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, которая делает это, дайте мне знать.