In my experience, the OCaml code doing recursive call and pattern matching is a relatively bad way to reason about such rewrite systems. Your questions are extremely pertinent, and relatively difficult to answer in general.
For a start, I think your code indeed repeats useless traversals. This can be seen syntactically by the nesting of two normalForm calls, such as: | (e, Constant b) -> normalForm (Plus (Constant b, normalForm e)) You reduce e to a normal form, then repeat the reduction on some expression containing e. The outer call will surely re-traverse (the normal form of) e, which is useless here. One approach I like for such simplifications is the "normalization by evaluation" approach. The idea is to define a different representation of normal forms of your system as "semantic values"; I mean a representation that has a meaning in itself and not just "what's left after this arbitrary transformation"; in your case, that could be multivariate polynomials (defined as an independent datatype). Then you express your normalization algorithm as an evaluation of your expression into semantic values; you can reify them back into the expression datatype, and if you did everything right you get normal forms (in particular, normalizing a reified value will return exactly this value). The main difficulty is to understand what are the normal forms you're looking for; then the code is relatively easy and can be made efficient. I'm afraid my explanation may be a bit too abstract and high-level. Do not hesitate to ask for more concrete details. On Sun, Oct 2, 2011 at 1:51 PM, Diego Olivier Fernandez Pons <dofp.oc...@gmail.com> wrote: > 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 > -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
