Re: [Caml-list] How to simplify an arithmetic expression ?

[Xavier Leroy <Xavier.Leroy@inria.fr>]

On Sun, Oct 2, 2011 at 10:08 AM, Gabriel Scherer wrote:
> One approach I like for such simplifications is the "normalization by
> evaluation" approach.

NBE is neat, but I'm skeptical that it will work out of the box here:
if you apply NBE to a standard evaluator for arithmetic expressions,
it's not going to take advantage of associativity and distributivity
the way Diego wants.

On 10/02/2011 05:09 PM, Ernesto Posse wrote:
> In general, whenever you have an algebraic
> structure with normal forms, normal forms can be obtained by
> equational reasoning: using the algebra's laws as rewriting rules. 

Yes, writing down a system of equations is the first thing to do.
But, to obtain a normalization procedure, you need to orient those
rules and complete them (in the sense of Knuth-Bendix completion) with
extra rules to derive a confluent, terminating rewriting system.

Here is a good, down-to-earth introduction to Knuth-Bendix completion:

A.J.J. Dick, "An Introduction to Knuth-Bendix Completion"
http://comjnl.oxfordjournals.org/content/34/1/2.full.pdf

And here is a solid textbook on rewriting systems:

Franz Baader and Tobias Nipkow. "Term Rewriting and All That".
http://www4.in.tum.de/~nipkow/TRaAT/

Hope this helps,

- Xavier Leroy