[<<][meta][>>][..]

Wed Feb 10 14:25:46 CET 2010

Commutation rewrite rule in CPS

termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = add (add Add)
    where
      add k Zero a = a
      add k One a = add k 1 a
      add k (Lit a) (Lit b) = Lit (a + b)                    -- evaluate
      add k a@(Lit _) (Add b@(Lit _) c) = Add (add k a b) c  -- associate
      add k a b = k b a                                      -- commute

If maching fails, add calls its continuation k.  The first k passed in
is (add Add).  If that version of add fails again it calls its
continuation k = Add which returns the term unevaluated.

With normalization and all association rules:

termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = add (add norm)
    where
      add k Zero a = a
      add k One a = add k (Lit 1) a
      add k (Lit a) (Lit b) = Lit (a + b)                                  -- e
      add k (Lit a) (Add (Lit b) c) = Add (Lit (a + b)) c                  -- a1
      add k (Add (Lit a) b) (Add (Lit c) d) = Add (Lit (a + c)) (Add b d)  -- a2
      add k a (Add b@(Lit _) c) = Add b (Add a c)                          -- a3
      add k a b = k b a                                                    -- c

      norm a b@(Lit _) = Add b a    -- n 
      norm a b = Add a b


I guess starting from equivalences (the algebraic rules) these rewrite
rules could be derived using Knuth - Bendix?

After thinking some more, this is the simplest set of rules I can find:


termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = add (add Add)
    where
      add k Zero a = a
      add k One a = add k (Lit 1) a
      add k (Lit a) (Lit b) = Lit (a + b)                                  -- e
      add k (Lit a) (Add (Lit b) c) = Add (Lit (a + b)) c                  -- ae1
      add k (Add (Lit a) b) (Add (Lit c) d) = Add (Lit (a + c)) (Add b d)  -- ae2
      add k a (Add b@(Lit _) c) = Add b (Add a c)                          -- an
      add k a@(Lit _) b = Add a b                                          -- n  
      add k a b = k b a                                                    -- c


For multiplication, the rules will look almost exactly the same.  Now,
the question is: how to abstract over such a pattern match?

Or..  How many combinations of rewrite rules should we allow?
I.e. allowing Signum 

[Reply][About]

[<<][meta][>>][..]