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

Commutativity and associativity

Exploiting those laws is a bit less straightforward.  However, how far
can we get with local reasoning only?

I.e. a problem is this: ((1 + a) + 2)

Currently this doesn't add the two literals.  Making that happen
requires two transformations:

 ((1 + a) + 2) -> ((a + 1) + 2) -> (a + (1 + 2))

Using local reasoning (rewriting), the outer '+' should be able to
reduce the expression.  Using a normal form is probably best.

Normalization:

  (1 + 1)       -> 2                  [e1]
  (1 + (1 + a)) -> (2 + a)            [e2]
  (a + 1)       -> (1 + a)            [c]
  ((x + y) + z) -> (x + (y + z))      [a]

((1 + a) + 2)

-> (1 + (a + 2))  [a]
-> (1 + (2 + a))  [c]
-> (3 + a)        [e2]





[Reply][About]
[<<][meta][>>][..]