> Below is a quick tentative implementation of NbE, on a slightly
> restricted expression type (I removed the not-so-interesting Minus
> nodes).
Sorry, I forgot to give a small example of what the implementation
does. Really the obvious thing, but it may not be so obvious just
looking at the code.
Here is an example of (X*2+Y)*(3+(Y*2+Z)) being 'rewritten' to
(1*Y)*Z+((2*Y)*Y+(3*Y+((2*X)*Z+((4*X)*Y+6*X)))).
In a more readable way, it computes that (2X+Y)*(3+2Y+Z) equals
YZ+2Y²+3Y+2XZ+4XY+6X.
(The ordering of the result monomials is arbitrary, as implemented by
Pervasives.compare, but a more human-natural order could be
implemented.)
# test1;;
- : expr = Plus (Times (Variable "X", Constant 2.), Variable "Y")
# test2;;
- : expr =
Plus (Constant 3., Plus (Times (Variable "Y", Constant 2.), Variable "Z"))
# show (eval test1);;
- : (Poly.key * float) list = [(["Y"], 1.); (["X"], 2.)]
# show (eval test2);;
- : (Poly.key * float) list = [(["Z"], 1.); (["Y"], 2.); ([], 3.)]
# show (eval (Times(test1,test2)));;
- : (Poly.key * float) list =
[(["Y"; "Z"], 1.); (["Y"; "Y"], 2.); (["Y"], 3.); (["X"; "Z"], 2.);
(["X"; "Y"], 4.); (["X"], 6.)]
# reify (eval (Times(test1,test2)));;
- : expr =
Plus (Times (Times (Constant 1., Variable "Y"), Variable "Z"),
Plus (Times (Times (Constant 2., Variable "Y"), Variable "Y"),
Plus (Times (Constant 3., Variable "Y"),
Plus (Times (Times (Constant 2., Variable "X"), Variable "Z"),
Plus (Times (Times (Constant 4., Variable "X"), Variable "Y"),
Times (Constant 6., Variable "X"))))))
On Sun, Oct 2, 2011 at 6:48 PM, Gabriel Scherer
<gabriel.sche...@gmail.com> wrote:
> On Sun, Oct 2, 2011 at 6:32 PM, Xavier Leroy <xavier.le...@inria.fr> 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
>>
>>
>
--
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
