From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p92GUrrA023623 for ; Sun, 2 Oct 2011 18:30:53 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Al0BAH6QiE7UGyoCk2dsb2JhbABBFpktjksiAQEBAQkJCwkUAyKBUwEBAwJTJRELGAkWDwkDAgECAUUTCAEBh3kEthGHIQSTYIUljBs X-IronPort-AV: E=Sophos;i="4.68,477,1312149600"; d="scan'208";a="111428593" Received: from smtp2-g21.free.fr ([212.27.42.2]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Oct 2011 18:30:47 +0200 Received: from [192.168.1.3] (unknown [82.237.71.191]) by smtp2-g21.free.fr (Postfix) with ESMTP id CE24A4B0249 for ; Sun, 2 Oct 2011 18:30:40 +0200 (CEST) Message-ID: <4E88922C.6080303@inria.fr> Date: Sun, 02 Oct 2011 18:32:44 +0200 From: Xavier Leroy User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.21) Gecko/20110831 Thunderbird/3.1.13 MIME-Version: 1.0 To: caml-list@inria.fr References: In-Reply-To: X-Enigmail-Version: 1.1.2 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] How to simplify an arithmetic expression ? 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