OCaml list,

It's easy to encapsulate a couple of arithmetic simplifications into a
function that applies them bottom up to an expression represented as a tree

let rec simplify = function
    | Plus (e1, e2) ->
        match (simplify e1, simplify e2) with
             | (Constant 0, _) -> e2

With a couple well known tricks like pushing constants to the left side and
so on...

How can I however guarantee that
    1. My final expression reaches a kind of minimal normal form
    2. My set of simplifications is optimal in the sense it doesn't traverse
subtrees without need

Here is my current simplifier and I have no way of telling if it really
simplifies the expressions as much as possible and if it does useless passes
or not

type expr =
    | Constant of float
    | Plus of expr * expr
    | Minus of expr * expr
    | Times of expr * expr
    | Variable of string

let rec normalForm = function
    | Minus (e1, e2) -> normalForm (Plus (normalForm e1, Times (Constant
(-1.0), normalForm e2)))
    | Plus (e1, e2) ->
        begin
        match (normalForm e1, normalForm e2) with
            | (Constant a, Constant b) -> Constant (a +. b)
            | (Constant 0.0, e) -> normalForm e
            | (e, Constant b) -> normalForm (Plus (Constant b, normalForm
e))
            | (Constant a, Plus (Constant b, e)) -> Plus (Constant (a +. b),
normalForm e)
            | (Plus (Constant a, e1), Plus (Constant b, e2)) -> Plus
(Constant (a +. b), normalForm (Plus (normalForm e1, normalForm e2)))
            | (Variable a, Variable b) when a = b -> Times (Constant 2.0,
Variable a)
            | (Times (Constant n, Variable b), Variable a) when a = b ->
Times (Constant (n +. 1.0), Variable a)
            | (Variable a, Times (Constant n, Variable b)) when a = b ->
Times (Constant (n +. 1.0), Variable a)
            | (Times (Constant n, Variable a), Times (Constant m, Variable
b)) when a = b -> Times (Constant (n +. m), Variable a)
            | other -> Plus (e1, e2)
        end
    | Times (e1, e2) ->
        begin
        match (normalForm e1, normalForm e2) with
            | (Constant a, Constant b) -> Constant (a *. b)
            | (Constant 0.0, e) -> Constant 0.0
            | (Constant 1.0, e) -> e
            | (e, Constant b) -> normalForm (Times (Constant b, normalForm
e))
            | (Constant a, Times (Constant b, e)) -> Times (Constant (a *.
b), e)
            | other -> Times (e1, e2)
         end
    | x -> x

let (++) = fun x y -> Plus (x, y)
let ( ** ) = fun x y -> Times (x, y)
let ( --) = fun x y -> Minus (x, y)
let f = function fl -> Constant fl

let x = Variable "x"
let h = fun i -> f i ** x -- f i ** f i ** x ++ (f 3.0 ++ f i)
let e = List.fold_left (fun t i -> Plus (t, h i)) (f 0.0) [1.0; 2.0; 3.0;
4.0; 5.0]

normalForm e


        Diego Olivier