Algebraic Properties of Rewrite Rules
-------------------------------------

The rewrite mechanism understands the algebraic properties of
functions like `+' and `*'.  In particular, pattern matching takes the
associativity and commutativity of the following functions into
account:

     + - *  = !=  && ||  and or xor  vint vunion vxor  gcd lcm  max min  beta

For example, the rewrite rule:

     a x + b x  :=  (a + b) x

will match formulas of the form,

     a x + b x,  x a + x b,  a x + x b,  x a + b x

Rewrites also understand the relationship between the `+' and `-'
operators.  The above rewrite rule will also match the formulas,

     a x - b x,  x a - x b,  a x - x b,  x a - b x

by matching `b' in the pattern to `-b' from the formula.

Applied to a sum of many terms like `r + a x + s + b x + t', this
pattern will check all pairs of terms for possible matches.  The
rewrite will take whichever suitable pair it discovers first.

In general, a pattern using an associative operator like `a + b' will
try 2 n different ways to match a sum of n terms like `x + y + z - w'.
First, `a' is matched against each of `x', `y', `z', and `-w' in turn,
with `b' being matched to the remainders `y + z - w', `x + z - w',
etc.  If none of these succeed, then `b' is matched against each of
the four terms with `a' matching the remainder.  Half-and-half
matches, like `(x + y) + (z - w)', are not tried.

Note that `*' is not commutative when applied to matrices, but rewrite
rules pretend that it is.  If you type `m v' to enable matrix mode
(See Matrix Mode), rewrite rules will match `*' literally,
ignoring its usual commutativity property.  (In the current
implementation, the associativity also vanishes--it is as if the
pattern had been enclosed in a `plain' marker; see below.)  If you are
applying rewrites to formulas with matrices, it's best to enable
matrix mode first to prevent algebraically incorrect rewrites from
occurring.

The pattern `-x' will actually match any expression.  For example, the
rule

     f(-x)  :=  -f(x)

will rewrite `f(a)' to `-f(-a)'.  To avoid this, either use a `plain'
marker as described below, or add a `negative(x)' condition.  The
`negative' function is true if its argument "looks" negative, for
example, because it is a negative number or because it is a formula
like `-x'.  The new rule using this condition is:

     f(x)  :=  -f(-x)  :: negative(x)    or, equivalently,
     f(-x)  :=  -f(x)  :: negative(-x)

In the same way, the pattern `x - y' will match the sum `a + b' by
matching `y' to `-b'.

The pattern `a b' will also match the formula `x/y' if
`y' is a number.  Thus the rule `a x + b x := (a+b) x'
will also convert `a x + x / 2' to `(a + 0.5) x' (or
`(a + 1:2) x', depending on the current fraction mode).

Calc will *not* take other liberties with `*', `/', and `^'.  For
example, the pattern `f(a b)' will not match `f(x^2)', and `f(a + b)'
will not match `f(2 x)', even though conceivably these patterns could
match with `a = b = x'.  Nor will `f(a b)' match `f(x / y)' if `y' is
not a constant, even though it could be considered to match with `a =
x' and `b = 1/y'.  The reasons are partly for efficiency, and partly
because while few mathematical operations are substantively different
for addition and subtraction, often it is preferable to treat the
cases of multiplication, division, and integer powers separately.

Even more subtle is the rule set

     [ f(a) + f(b) := f(a + b),  -f(a) := f(-a) ]

attempting to match `f(x) - f(y)'.  You might think that Calc will
view this subtraction as `f(x) + (-f(y))' and then apply the above two
rules in turn, but actually this will not work because Calc only does
this when considering rules for `+' (like the first rule in this set).
So it will see first that `f(x) + (-f(y))' does not match `f(a) +
f(b)' for any assignments of the meta-variables, and then it will see
that `f(x) - f(y)' does not match `-f(a)' for any assignment of `a'.
Because Calc tries only one rule at a time, it will not be able to
rewrite `f(x) - f(y)' with this rule set.  An explicit `f(a) - f(b)'
rule will have to be added.

Another thing patterns will *not* do is break up complex numbers.
The pattern `myconj(a + b i) := a - b i' will work for formulas
involving the special constant `i' (such as `3 - 4 i'), but
it will not match actual complex numbers like `(3, -4)'.  A version
of the above rule for complex numbers would be

     myconj(a)  :=  re(a) - im(a) (0,1)  :: im(a) != 0

(Because the `re' and `im' functions understand the properties of the
special constant `i', this rule will also work for `3 - 4 i'.  In
fact, this particular rule would probably be better without the `im(a)
!= 0' condition, since if `im(a) = 0' the righthand side of the rule
will still give the correct answer for the conjugate of a real
number.)

It is also possible to specify optional arguments in patterns.  The
rule

     opt(a) x + opt(b) (x^opt(c) + opt(d))  :=  f(a, b, c, d)

will match the formula

     5 (x^2 - 4) + 3 x

in a fairly straightforward manner, but it will also match reduced
formulas like

     x + x^2,    2(x + 1) - x,    x + x

producing, respectively,

     f(1, 1, 2, 0),   f(-1, 2, 1, 1),   f(1, 1, 1, 0)

(The latter two formulas can be entered only if default
simplifications have been turned off with `m O'.)

The default value for a term of a sum is zero.  The default value for
a part of a product, for a power, or for the denominator of a
quotient, is one.  Also, `-x' matches the pattern `opt(a) b' with `a =
-1'.

In particular, the distributive-law rule can be refined to

     opt(a) x + opt(b) x  :=  (a + b) x

so that it will convert, e.g., `a x - x', to `(a - 1) x'.

The pattern `opt(a) + opt(b) x' matches almost any formulas which are
linear in `x'.  You can also use the `lin' and `islin' functions with
rewrite conditions to test for this; See Logical Operations.
These functions are not as convenient to use in rewrite rules, but
they recognize more kinds of formulas as linear: `x/z' is considered
linear with `b = 1/z' by `lin', but it will not match the above
pattern because that pattern calls for a multiplication, not a
division.

As another example, the obvious rule to replace `sin(x)^2 + cos(x)^2'
by 1,

     sin(x)^2 + cos(x)^2  :=  1

misses many cases because the sine and cosine may both be multiplied
by an equal factor.  Here's a more successful rule:

     opt(a) sin(x)^2 + opt(a) cos(x)^2  :=  a

Note that this rule will *not* match `sin(x)^2 + 6 cos(x)^2' because
one `a' would have "matched" 1 while the other matched 6.

Calc automatically converts a rule like

     f(x-1, x)  :=  g(x)

into the form

     f(temp, x)  :=  g(x)  :: temp = x-1

(where `temp' stands for a new, invented meta-variable that doesn't
actually have a name).  This modified rule will successfully match
`f(6, 7)', binding `temp' and `x' to 6 and 7, respectively, then
verifying that they differ by one even though `6' does not
superficially look like `x-1'.

However, Calc does not solve equations to interpret a rule.  The
following rule,

     f(x-1, x+1)  :=  g(x)

will not work.  That is, it will match `f(a - 1 + b, a + 1 + b)' but
not `f(6, 8)'.  Calc always interprets at least one occurrence of a
variable by literal matching.  If the variable appears "isolated" then
Calc is smart enough to use it for literal matching.  But in this last
example, Calc is forced to rewrite the rule to `f(x-1, temp) := g(x)
:: temp = x+1' where the `x-1' term must correspond to an actual
"something-minus-one" in the target formula.

A successful way to write this would be `f(x, x+2) := g(x+1)'.  You
could make this resemble the original form more closely by using `let'
notation, which is described in the next section:

     f(xm1, x+1)  :=  g(x)  :: let(x := xm1+1)

Calc does this rewriting or "conditionalizing" for any sub-pattern
which involves only the functions in the following list, operating
only on constants and meta-variables which have already been matched
elsewhere in the pattern.  When matching a function call, Calc is
careful to match arguments which are plain variables before arguments
which are calls to any of the functions below, so that a pattern like
`f(x-1, x)' can be conditionalized even though the isolated `x' comes
after the `x-1'.

     + - * / \ % ^  abs sign  round rounde roundu trunc floor ceil
     max min  re im conj arg

You can suppress all of the special treatments described in this
section by surrounding a function call with a `plain' marker.  This
marker causes the function call which is its argument to be matched
literally, without regard to commutativity, associativity, negation,
or conditionalization.  When you use `plain', the "deep structure" of
the formula being matched can show through.  For example,

     plain(a - a b)  :=  f(a, b)

will match only literal subtractions.  However, the `plain'
marker does not affect its arguments' arguments.  In this case,
commutativity and associativity is still considered while matching
the `a b' sub-pattern, so the whole pattern will match
`x - y x' as well as `x - x y'.  We could go still
further and use

     plain(a - plain(a b))  :=  f(a, b)

which would do a completely strict match for the pattern.

By contrast, the `quote' marker means that not only the function name
but also the arguments must be literally the same.  The above pattern
will match `x - x y' but

     quote(a - a b)  :=  f(a, b)

will match only the single formula `a - a b'.  Also,

     quote(a - quote(a b))  :=  f(a, b)

will match only `a - quote(a b)'---probably not the desired effect!

A certain amount of algebra is also done when substituting the
meta-variables on the righthand side of a rule.  For example, in the
rule

     a + f(b)  :=  f(a + b)

matching `f(x) - y' would produce `f((-y) + x)' if taken literally,
but the rewrite mechanism will simplify the righthand side to `f(x -
y)' automatically.  (Of course, the default simplifications would do
this anyway, so this special simplification is only noticeable if you
have turned the default simplifications off.)  This rewriting is done
only when a meta-variable expands to a "negative-looking" expression.
If this simplification is not desirable, you can use a `plain' marker
on the righthand side:

     a + f(b)  :=  f(plain(a + b))

In this example, we are still allowing the pattern-matcher to use all
the algebra it can muster, but the righthand side will always simplify
to a literal addition like `f((-y) + x)'.