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 -- 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
