Next: Algebraic Properties of Rewrite Rules, Previous: Basic Rewrite Rules, Up: Rewrite Rules [Contents][Index]

A rewrite rule can also be *conditional*, written in the form
‘` old := new :: cond`’. (There is also the obsolete
form ‘

For example, the formula ‘`n > 0`’ simplifies to 1 or 0 if ‘`n`’
is replaced by a positive or nonpositive number, respectively (or if
‘`n`’ has been declared to be positive or nonpositive). Thus,
the rule ‘`f(x,y) := g(y+x,x) :: x+y > 0`’ would apply to
‘`f(0, 4)`’ but not to ‘`f(-3, 2)`’ or ‘`f(12, a+1)`’
(assuming no outstanding declarations for ‘`a`’). In the case of
‘`f(-3, 2)`’, the condition can be shown not to be satisfied; in
the case of ‘`f(12, a+1)`’, the condition merely cannot be shown
to be satisfied, but that is enough to reject the rule.

While Calc will use declarations to reason about variables in the
formula being rewritten, declarations do not apply to meta-variables.
For example, the rule ‘`f(a) := g(a+1)`’ will match for any values
of ‘`a`’, such as complex numbers, vectors, or formulas, even if
‘`a`’ has been declared to be real or scalar. If you want the
meta-variable ‘`a`’ to match only literal real numbers, use
‘`f(a) := g(a+1) :: real(a)`’. If you want ‘`a`’ to match only
reals and formulas which are provably real, use ‘`dreal(a)`’ as
the condition.

The ‘`::`’ operator is a shorthand for the `condition`

function; ‘` old := new :: cond`’ is equivalent to
the formula ‘

If you have several conditions, you can use ‘`... :: c1 :: c2 :: c3`’
or ‘`... :: c1 && c2 && c3`’. The two are entirely equivalent.

It is also possible to embed conditions inside the pattern:
‘`f(x :: x>0, y) := g(y+x, x)`’. This is purely a notational
convenience, though; where a condition appears in a rule has no
effect on when it is tested. The rewrite-rule compiler automatically
decides when it is best to test each condition while a rule is being
matched.

Certain conditions are handled as special cases by the rewrite rule
system and are tested very efficiently: Where ‘`x`’ is any
meta-variable, these conditions are ‘`integer(x)`’, ‘`real(x)`’,
‘`constant(x)`’, ‘`negative(x)`’, ‘`x >= y`’ where ‘`y`’
is either a constant or another meta-variable and ‘`>=`’ may be
replaced by any of the six relational operators, and ‘`x % a = b`’
where ‘`a`’ and ‘`b`’ are constants. Other conditions, like
‘`x >= y+1`’ or ‘`dreal(x)`’, will be less efficient to check
since Calc must bring the whole evaluator and simplifier into play.

An interesting property of ‘`::`’ is that neither of its arguments
will be touched by Calc’s default simplifications. This is important
because conditions often are expressions that cannot safely be
evaluated early. For example, the `typeof`

function never
remains in symbolic form; entering ‘`typeof(a)`’ will put the
number 100 (the type code for variables like ‘`a`’) on the stack.
But putting the condition ‘`... :: typeof(a) = 6`’ on the stack
is safe since ‘`::`’ prevents the `typeof`

from being
evaluated until the condition is actually used by the rewrite system.

Since ‘`::`’ protects its lefthand side, too, you can use a dummy
condition to protect a rule that must itself not evaluate early.
For example, it’s not safe to put ‘`a(f,x) := apply(f, [x])`’ on
the stack because it will immediately evaluate to ‘`a(f,x) := f(x)`’,
where the meta-variable-ness of `f`

on the righthand side has been
lost. But ‘`a(f,x) := apply(f, [x]) :: 1`’ is safe, and of course
the condition ‘`1`’ is always true (nonzero) so it has no effect on
the functioning of the rule. (The rewrite compiler will ensure that
it doesn’t even impact the speed of matching the rule.)