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 p92GnOa1024035 for ; Sun, 2 Oct 2011 18:49:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoIBACuViE5KfVI0kGdsb2JhbABBFoRPlCqOdwgiAQEBAQkJDQcUBCGBUwEBAQEBAQESAg8EGQEbEgsBAwELBgMCCw0CAgkdAgIiAREBBQEKEgYTCAoQh1kGmnEKiwlEglyDVz2IbgIEBoEnhGGBEwSTYI0UPYNv X-IronPort-AV: E=Sophos;i="4.68,477,1312149600"; d="scan'208";a="111429442" Received: from mail-ww0-f52.google.com ([74.125.82.52]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Oct 2011 18:49:19 +0200 Received: by wwj40 with SMTP id 40so5411544wwj.9 for ; Sun, 02 Oct 2011 09:49:19 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=vv2zm3ts1Glow4+8UDJpZ4qbSrC9Il+UMbGlzX/oqW0=; b=C06zi3Q84qPTCmNJpNW5zPnshzVctZgMB0HXYgBS0wVHvxgp4ibiHC/X2mgIgZCVXE nCTzIEWuRxoWaM5irxZ2zDZ5P2bx5WCAzoHAYyYtnpoqqbMXbKMgRUldebwuF9qeUhFp OGo+oOzMXZvzwMokzqqsZlwWzM02gUc7xH9wY= Received: by 10.227.167.1 with SMTP id o1mr16260834wby.6.1317574158083; Sun, 02 Oct 2011 09:49:18 -0700 (PDT) MIME-Version: 1.0 Received: by 10.227.155.67 with HTTP; Sun, 2 Oct 2011 09:48:57 -0700 (PDT) In-Reply-To: <4E88922C.6080303@inria.fr> References: <4E88922C.6080303@inria.fr> From: Gabriel Scherer Date: Sun, 2 Oct 2011 18:48:57 +0200 Message-ID: To: Xavier Leroy Cc: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p92GnOa1024035 Subject: Re: [Caml-list] How to simplify an arithmetic expression ? On Sun, Oct 2, 2011 at 6:32 PM, Xavier Leroy wrote: > 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. My idea was to use a semantic domain which is a quotient over those associativity and distributivity laws. If you choose a canonical representation of multivariate polynomials (sums of product of some variables and a coefficient) and compute on them, you get associativity and distributivity for free. But indeed, the rewriting that happens implicitly may not implement the exact same rules Diego had in mind. In particular, canonical polynomial representations may be much bigger than the input expression, due to applying distributivity systematically. Not all rewrite systems are suitable for NbE. Most reasonable semantic domains probably induce very strong rewrite rules, or none at all. For the middle ground, finding a suitable semantic domain is probably just as hard as completing the rewrite system as you suggest. > On 10/02/2011 05:09 PM, Ernesto Posse wrote: > If we are talking about optimization, then yes, > there may be better ways of doing this, but if we are talking about > correctness, readability, and reasoning, then I don't see why this > style would be considered bad. "Optimization" is important here. By calling the deep-recursive transformation twice in a case, you get an exponential algorithm which can be so slow and memory-hungry that impracticality borders incorrectness. > On 10/02/2011 05:09 PM, Ernesto Posse wrote: > So in principle at least, shouldn't Diego's problem be solvable this way, > without the need for a special semantic domain for normal forms? When > would the normalization by evaluation approach be preferable? Can you > show a small example? Yes, implementing the rewrite system directly is possible and probably a more precise way to get a result (in particular if you already know the rewrite rules you wish to have, but not the semantic domain their normal forms correspond to). I'm not sure it's simpler. Below is a quick tentative implementation of NbE, on a slightly restricted expression type (I removed the not-so-interesting Minus nodes). You can normalize an expression `e` with `reify (eval e)`. `show (eval e)` is a representation whose toplevel printing is more redable, which helps testing. type var = string type expr = | Constant of float | Plus of expr * expr | Times of expr * expr | Variable of var (* multivariate polynomials: maps from multiset of variables to coefficients 2*X²*Y + 3*X + 1 => {["X","X","Y"]↦2, ["X"]↦3, ∅↦1} *) module MultiVar = struct (* multisets naively implemented as sorted lists *) type t = var list let compare = Pervasives.compare end module Poly = Map.Make(MultiVar) type value = float Poly.t let sort vars = List.sort String.compare vars let constant x = Poly.singleton [] x let variable v = Poly.singleton [v] 1. (* BatOption.default *) let default d = function | None -> d | Some x -> x let plus p1 p2 = let add_opt _vars c1 c2 = Some (default 0. c1 +. default 0. c2) in Poly.merge add_opt p1 p2 let times p1 p2 = (* naive implementation *) let p2_times_monome vars coeff acc = let add_monome v c acc = let monome = Poly.singleton (sort (vars @ v)) (c *. coeff) in plus monome acc in Poly.fold add_monome p2 acc in Poly.fold p2_times_monome p1 Poly.empty (* evaluate expressions into values *) let rec eval = function | Constant x -> constant x | Variable v -> variable v | Plus(e1, e2) -> plus (eval e1) (eval e2) | Times(e1, e2) -> times (eval e1) (eval e2) let show p = Poly.fold (fun vars coeff acc -> (vars, coeff)::acc) p [] (* translate values back into expressions *) let reify p = let monome vars coeff = let times_var acc var = Times (acc, Variable var) in List.fold_left times_var (Constant coeff) vars in (* extract the first elem before summing, to avoid a dummy 0. initial accumulator *) if Poly.is_empty p then Constant 0. else let (v,c) = Poly.min_binding p in let p' = Poly.remove v p in Poly.fold (fun v c acc -> Plus(monome v c, acc)) p' (monome v c) > 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 > >