[Caml-list] How to simplify an arithmetic expression ?

[Caml-list] How to simplify an arithmetic expression ?

[Diego Olivier Fernandez Pons]

[-- Attachment #1: Type: text/plain, Size: 2814 bytes --]

    OCaml list,

It's easy to encapsulate a couple of arithmetic simplifications into a
function that applies them bottom up to an expression represented as a tree

let rec simplify = function
    | Plus (e1, e2) ->
        match (simplify e1, simplify e2) with
             | (Constant 0, _) -> e2

With a couple well known tricks like pushing constants to the left side and
so on...

How can I however guarantee that
    1. My final expression reaches a kind of minimal normal form
    2. My set of simplifications is optimal in the sense it doesn't traverse
subtrees without need

Here is my current simplifier and I have no way of telling if it really
simplifies the expressions as much as possible and if it does useless passes
or not

type expr =
    | Constant of float
    | Plus of expr * expr
    | Minus of expr * expr
    | Times of expr * expr
    | Variable of string

let rec normalForm = function
    | Minus (e1, e2) -> normalForm (Plus (normalForm e1, Times (Constant
(-1.0), normalForm e2)))
    | Plus (e1, e2) ->
        begin
        match (normalForm e1, normalForm e2) with
            | (Constant a, Constant b) -> Constant (a +. b)
            | (Constant 0.0, e) -> normalForm e
            | (e, Constant b) -> normalForm (Plus (Constant b, normalForm
e))
            | (Constant a, Plus (Constant b, e)) -> Plus (Constant (a +. b),
normalForm e)
            | (Plus (Constant a, e1), Plus (Constant b, e2)) -> Plus
(Constant (a +. b), normalForm (Plus (normalForm e1, normalForm e2)))
            | (Variable a, Variable b) when a = b -> Times (Constant 2.0,
Variable a)
            | (Times (Constant n, Variable b), Variable a) when a = b ->
Times (Constant (n +. 1.0), Variable a)
            | (Variable a, Times (Constant n, Variable b)) when a = b ->
Times (Constant (n +. 1.0), Variable a)
            | (Times (Constant n, Variable a), Times (Constant m, Variable
b)) when a = b -> Times (Constant (n +. m), Variable a)
            | other -> Plus (e1, e2)
        end
    | Times (e1, e2) ->
        begin
        match (normalForm e1, normalForm e2) with
            | (Constant a, Constant b) -> Constant (a *. b)
            | (Constant 0.0, e) -> Constant 0.0
            | (Constant 1.0, e) -> e
            | (e, Constant b) -> normalForm (Times (Constant b, normalForm
e))
            | (Constant a, Times (Constant b, e)) -> Times (Constant (a *.
b), e)
            | other -> Times (e1, e2)
         end
    | x -> x

let (++) = fun x y -> Plus (x, y)
let ( ** ) = fun x y -> Times (x, y)
let ( --) = fun x y -> Minus (x, y)
let f = function fl -> Constant fl

let x = Variable "x"
let h = fun i -> f i ** x -- f i ** f i ** x ++ (f 3.0 ++ f i)
let e = List.fold_left (fun t i -> Plus (t, h i)) (f 0.0) [1.0; 2.0; 3.0;
4.0; 5.0]

normalForm e


        Diego Olivier

[-- Attachment #2: Type: text/html, Size: 3682 bytes --]

Re: [Caml-list] How to simplify an arithmetic expression ?

[Gabriel Scherer]

In my experience, the OCaml code doing recursive call and pattern
matching is a relatively bad way to reason about such rewrite systems.
Your questions are extremely pertinent, and relatively difficult to
answer in general.

For a start, I think your code indeed repeats useless traversals. This
can be seen syntactically by the nesting of two normalForm calls, such
as:

  | (e, Constant b) -> normalForm (Plus (Constant b, normalForm e))

You reduce e to a normal form, then repeat the reduction on some
expression containing e. The outer call will surely re-traverse (the
normal form of) e, which is useless here.

One approach I like for such simplifications is the "normalization by
evaluation" approach. The idea is to define a different representation
of normal forms of your system as "semantic values"; I mean a
representation that has a meaning in itself and not just "what's left
after this arbitrary transformation"; in your case, that could be
multivariate polynomials (defined as an independent datatype). Then
you express your normalization algorithm as an evaluation of your
expression into semantic values; you can reify them back into the
expression datatype, and if you did everything right you get normal
forms (in particular, normalizing a reified value will return exactly
this value). The main difficulty is to understand what are the normal
forms you're looking for; then the code is relatively easy and can be
made efficient.

I'm afraid my explanation may be a bit too abstract and high-level. Do
not hesitate to ask for more concrete details.

On Sun, Oct 2, 2011 at 1:51 PM, Diego Olivier Fernandez Pons
<dofp.ocaml@gmail.com> wrote:
>     OCaml list,
> It's easy to encapsulate a couple of arithmetic simplifications into a
> function that applies them bottom up to an expression represented as a tree
> let rec simplify = function
>     | Plus (e1, e2) ->
>         match (simplify e1, simplify e2) with
>              | (Constant 0, _) -> e2
> With a couple well known tricks like pushing constants to the left side and
> so on...
> How can I however guarantee that
>     1. My final expression reaches a kind of minimal normal form
>     2. My set of simplifications is optimal in the sense it doesn't traverse
> subtrees without need
> Here is my current simplifier and I have no way of telling if it really
> simplifies the expressions as much as possible and if it does useless passes
> or not
> type expr =
>     | Constant of float
>     | Plus of expr * expr
>     | Minus of expr * expr
>     | Times of expr * expr
>     | Variable of string
> let rec normalForm = function
>     | Minus (e1, e2) -> normalForm (Plus (normalForm e1, Times (Constant
> (-1.0), normalForm e2)))
>     | Plus (e1, e2) ->
>         begin
>         match (normalForm e1, normalForm e2) with
>             | (Constant a, Constant b) -> Constant (a +. b)
>             | (Constant 0.0, e) -> normalForm e
>             | (e, Constant b) -> normalForm (Plus (Constant b, normalForm
> e))
>             | (Constant a, Plus (Constant b, e)) -> Plus (Constant (a +. b),
> normalForm e)
>             | (Plus (Constant a, e1), Plus (Constant b, e2)) -> Plus
> (Constant (a +. b), normalForm (Plus (normalForm e1, normalForm e2)))
>             | (Variable a, Variable b) when a = b -> Times (Constant 2.0,
> Variable a)
>             | (Times (Constant n, Variable b), Variable a) when a = b ->
> Times (Constant (n +. 1.0), Variable a)
>             | (Variable a, Times (Constant n, Variable b)) when a = b ->
> Times (Constant (n +. 1.0), Variable a)
>             | (Times (Constant n, Variable a), Times (Constant m, Variable
> b)) when a = b -> Times (Constant (n +. m), Variable a)
>             | other -> Plus (e1, e2)
>         end
>     | Times (e1, e2) ->
>         begin
>         match (normalForm e1, normalForm e2) with
>             | (Constant a, Constant b) -> Constant (a *. b)
>             | (Constant 0.0, e) -> Constant 0.0
>             | (Constant 1.0, e) -> e
>             | (e, Constant b) -> normalForm (Times (Constant b, normalForm
> e))
>             | (Constant a, Times (Constant b, e)) -> Times (Constant (a *.
> b), e)
>             | other -> Times (e1, e2)
>          end
>     | x -> x
> let (++) = fun x y -> Plus (x, y)
> let ( ** ) = fun x y -> Times (x, y)
> let ( --) = fun x y -> Minus (x, y)
> let f = function fl -> Constant fl
> let x = Variable "x"
> let h = fun i -> f i ** x -- f i ** f i ** x ++ (f 3.0 ++ f i)
> let e = List.fold_left (fun t i -> Plus (t, h i)) (f 0.0) [1.0; 2.0; 3.0;
> 4.0; 5.0]
> normalForm e
>
>         Diego Olivier
>

Re: [Caml-list] How to simplify an arithmetic expression ?

[Ernesto Posse]

> On Sun, Oct 2, 2011 at 1:51 PM, Diego Olivier Fernandez Pons
> <dofp.ocaml@gmail.com> wrote:
>>     OCaml list,
>> It's easy to encapsulate a couple of arithmetic simplifications into a
>> function that applies them bottom up to an expression represented as a tree
>> let rec simplify = function
>>     | Plus (e1, e2) ->
>>         match (simplify e1, simplify e2) with
>>              | (Constant 0, _) -> e2
>> With a couple well known tricks like pushing constants to the left side and
>> so on...
>> How can I however guarantee that
>>     1. My final expression reaches a kind of minimal normal form
>>     2. My set of simplifications is optimal in the sense it doesn't traverse
>> subtrees without need
>> Here is my current simplifier and I have no way of telling if it really
>> simplifies the expressions as much as possible and if it does useless passes
>> or not
>> type expr =
>>     | Constant of float
>>     | Plus of expr * expr
>>     | Minus of expr * expr
>>     | Times of expr * expr
>>     | Variable of string
>> let rec normalForm = function
>>     | Minus (e1, e2) -> normalForm (Plus (normalForm e1, Times (Constant
>> (-1.0), normalForm e2)))
>>     | Plus (e1, e2) ->
>>         begin
>>         match (normalForm e1, normalForm e2) with
>>             | (Constant a, Constant b) -> Constant (a +. b)
>>             | (Constant 0.0, e) -> normalForm e
>>             | (e, Constant b) -> normalForm (Plus (Constant b, normalForm
>> e))
>>             | (Constant a, Plus (Constant b, e)) -> Plus (Constant (a +. b),
>> normalForm e)
>>             | (Plus (Constant a, e1), Plus (Constant b, e2)) -> Plus
>> (Constant (a +. b), normalForm (Plus (normalForm e1, normalForm e2)))
>>             | (Variable a, Variable b) when a = b -> Times (Constant 2.0,
>> Variable a)
>>             | (Times (Constant n, Variable b), Variable a) when a = b ->
>> Times (Constant (n +. 1.0), Variable a)
>>             | (Variable a, Times (Constant n, Variable b)) when a = b ->
>> Times (Constant (n +. 1.0), Variable a)
>>             | (Times (Constant n, Variable a), Times (Constant m, Variable
>> b)) when a = b -> Times (Constant (n +. m), Variable a)
>>             | other -> Plus (e1, e2)
>>         end
>>     | Times (e1, e2) ->
>>         begin
>>         match (normalForm e1, normalForm e2) with
>>             | (Constant a, Constant b) -> Constant (a *. b)
>>             | (Constant 0.0, e) -> Constant 0.0
>>             | (Constant 1.0, e) -> e
>>             | (e, Constant b) -> normalForm (Times (Constant b, normalForm
>> e))
>>             | (Constant a, Times (Constant b, e)) -> Times (Constant (a *.
>> b), e)
>>             | other -> Times (e1, e2)
>>          end
>>     | x -> x
>> let (++) = fun x y -> Plus (x, y)
>> let ( ** ) = fun x y -> Times (x, y)
>> let ( --) = fun x y -> Minus (x, y)
>> let f = function fl -> Constant fl
>> let x = Variable "x"
>> let h = fun i -> f i ** x -- f i ** f i ** x ++ (f 3.0 ++ f i)
>> let e = List.fold_left (fun t i -> Plus (t, h i)) (f 0.0) [1.0; 2.0; 3.0;
>> 4.0; 5.0]
>> normalForm e
>>
>>         Diego Olivier
>>


On Sun, Oct 2, 2011 at 10:08 AM, Gabriel Scherer
<gabriel.scherer@gmail.com> wrote:
> In my experience, the OCaml code doing recursive call and pattern
> matching is a relatively bad way to reason about such rewrite systems.

Why? In general, reduction in (pure) functional languages is
rewriting. Diego's function does not seem to have side-effects, so why
would this be a bad way?

As I understand it, this style is very much one of the reasons why ML
was designed this way. 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.

> Your questions are extremely pertinent, and relatively difficult to
> answer in general.
>
> For a start, I think your code indeed repeats useless traversals. This
> can be seen syntactically by the nesting of two normalForm calls, such
> as:
>
>  | (e, Constant b) -> normalForm (Plus (Constant b, normalForm e))
>
> You reduce e to a normal form, then repeat the reduction on some
> expression containing e. The outer call will surely re-traverse (the
> normal form of) e, which is useless here.

Another problem might be that the "rewriting" rules do not seem to be
exhaustive although I haven't checked very carefully.


> One approach I like for such simplifications is the "normalization by
> evaluation" approach. The idea is to define a different representation
> of normal forms of your system as "semantic values"; I mean a
> representation that has a meaning in itself and not just "what's left
> after this arbitrary transformation"; in your case, that could be
> multivariate polynomials (defined as an independent datatype). Then
> you express your normalization algorithm as an evaluation of your
> expression into semantic values; you can reify them back into the
> expression datatype, and if you did everything right you get normal
> forms (in particular, normalizing a reified value will return exactly
> this value). The main difficulty is to understand what are the normal
> forms you're looking for; then the code is relatively easy and can be
> made efficient.

I wonder if such an approach (normalization by evaluation) might be a
bit of an overkill. 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. 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?




-- 
Ernesto Posse

Modelling and Analysis in Software Engineering
School of Computing
Queen's University - Kingston, Ontario, Canada

Re: [Caml-list] How to simplify an arithmetic expression ?

[Xavier Leroy]

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

Re: [Caml-list] How to simplify an arithmetic expression ?

[Gabriel Scherer]

On Sun, Oct 2, 2011 at 6:32 PM, Xavier Leroy <Xavier.Leroy@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
>
>

Re: [Caml-list] How to simplify an arithmetic expression ?

[Xavier Clerc]

[-- Attachment #1: Type: text/plain, Size: 903 bytes --]

----- Mail original -----
> De: "Diego Olivier Fernandez Pons" <dofp.ocaml@gmail.com>
> À: "caml-list" <caml-list@inria.fr>
> Envoyé: Dimanche 2 Octobre 2011 13:51:13
> Objet: [Caml-list] How to simplify an arithmetic expression ?
> OCaml list,
> It's easy to encapsulate a couple of arithmetic simplifications into a
> function that applies them bottom up to an expression represented as a
> tree
Not absolutely sure it will fit your needs, but it will at least advertise a nice tool... The "moca" preprocessor allows you to add properties to constructors of a sum type (e. g. associativity, commutativity, etc.). Example from the webpage (*): type t = private      | Zero      | One      | Opp of t      | Add of t * t        begin          associative          commutative          neutral (Zero)          opposite (Opp)        end   ;; Regards, Xavier Clerc (*) http://moca.inria.fr/eng.htm

[-- Attachment #2: Type: text/html, Size: 1331 bytes --]

Re: [Caml-list] How to simplify an arithmetic expression ?

[Gabriel Scherer]

> 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.scherer@gmail.com> wrote:
> On Sun, Oct 2, 2011 at 6:32 PM, Xavier Leroy <Xavier.Leroy@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
>>
>>
>

Re: [Caml-list] How to simplify an arithmetic expression ?

[Goswin von Brederlow]

Diego Olivier Fernandez Pons <dofp.ocaml@gmail.com> writes:

>     OCaml list,
>
> It's easy to encapsulate a couple of arithmetic simplifications into a function
> that applies them bottom up to an expression represented as a tree
>
> let rec simplify = function
>     | Plus (e1, e2) ->
>         match (simplify e1, simplify e2) with
>              | (Constant 0, _) -> e2 
>
> With a couple well known tricks like pushing constants to the left side and so
> on...
>
> How can I however guarantee that
>     1. My final expression reaches a kind of minimal normal form

First you have to define what you mean by that.

For a (good) compiler a minimal normal form would be one that uses the
least number of instructions (optimize size) or least number of cpu
cycles (optimize speed) to execute. And that is quite a complex problem.

One simplification that will probably destroy any idea of a simple
minimal normal form is probably eliminating common subexpressions.
Some optimizations will require complex heuristics or much larger
patterns.

>     2. My set of simplifications is optimal in the sense it doesn't traverse
> subtrees without need

That you have to think through. I don't think you can get the compiler
to tell you when a traversal isn't needed. You could annotate your
syntax tree with traversal counts and check if the count goes up too
much somewhere. If you do extra unneeded traversals then I expect them
to become exponential quite quickly so it should be easy to spot by
running a bunch of expressions through your code.

>
> Here is my current simplifier and I have no way of telling if it really
> simplifies the expressions as much as possible and if it does useless passes or
> not

It doesn't.

1 - 1 -> 0
a + b + 2 * (a + b) -> 3 * a + 3 * b or 3 * (a + b)?
(a + 1) * (a - 1) -> a * a - 1
9 * a -> 8 * a + a?

The last would be something a compiler does to optimize speed since a
muliplication by a power of 2 is a shift and shift + add is faster than
multiplication.

MfG
        Goswin

Re: [Caml-list] How to simplify an arithmetic expression ?

[Goswin von Brederlow]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

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

(1*Y)? That certainly isn't optimal.

MfG
        Goswin

Re: [Caml-list] How to simplify an arithmetic expression ?

[Gabriel Scherer]

On Wed, Oct 5, 2011 at 3:17 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> (1*Y)? That certainly isn't optimal.

The inefficiency is in the code translating the semantic value back
into the expression type, not in the evaluation code.
Feel free to add the few lines needed to spot that corner case and
behave accordingly, as I did for the initialization of the sum (to
avoid "+ 0" everywhere).
Note that this doesn't stop the simplification to be involutive, so
still a valid simplification/normalization; whether the normal form
actually respects our sense of "optimality" is a different question.

On Wed, Oct 5, 2011 at 3:17 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> Gabriel Scherer <gabriel.scherer@gmail.com> writes:
>
>>> 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)))).
>
> (1*Y)? That certainly isn't optimal.
>
> MfG
>        Goswin
>