`[<<][meta][>>][..]`
Wed Feb 10 14:25:46 CET 2010

## Commutation rewrite rule in CPS

```termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
where
add k Zero a = a
add k (Lit a) (Lit b) = Lit (a + b)                    -- evaluate
add k a b = k b a                                      -- commute

If maching fails, add calls its continuation k.  The first k passed in
continuation k = Add which returns the term unevaluated.

With normalization and all association rules:

termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
where
add k Zero a = 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 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)
where
add k Zero a = 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 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][>>][..]`