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
