GUARDIAN: Guarded Expressions in Practice

REDUCE

20.27 GUARDIAN: Guarded Expressions in Practice

Computer algebra systems typically drop some degenerate cases when evaluating expressions, e.g., \(x/x\) becomes \(1\) dropping the case \(x=0\). We claim that it is feasible in practice to compute also the degenerate cases yielding guarded expressions. We work over real closed ﬁelds but our ideas about handling guarded expression can be easily transferred to other situations. Using formulas as guards provides a powerful tool for heuristically reducing the combinatorial explosion of cases: equivalent, redundant, tautological, and contradictive cases can be detected by simpliﬁcation and quantiﬁer elimination. Our approach allows to simplify the expressions on the basis of simpliﬁcation knowledge on the logical side. The method described in this paper is implemented in the REDUCE package GUARDIAN.

Authors: Andreas Dolzmann and Thomas Sturm

20.27.1 Introduction

\( \newenvironment {gex}{\left [\begin {array}{c|c}}{\end {array}\right ]} \newcommand {\gc }[1]{\boldsymbol {#1}} \newcommand {\true }{\textrm {T}} \newcommand {\false }{\textrm {F}} \newcommand {\E }{\textrm {E}} \newcommand {\GE }{\textrm {GE}} \newcommand {\gscheme }{\textrm {gscheme}} \newcommand {\sign }{\textrm {sign}} \)It is meanwhile a well-known fact that evaluations obtained with the interactive use of computer algebra systems (CAS) are not entirely correct in general. Typically, some degenerate cases are dropped. Consider for instance the evaluation

\[ \frac {x^2}{x}=x, \]

which is correct only if \(x\neq 0\). The problem here is that CAS consider variables to be transcendental elements. The user, in contrast, has in mind variables in the sense of logic. In other words: The user does not think of rational functions but of terms.

Next consider the valid expression

\[ \frac {\sqrt {x}+\sqrt {-x}}{x}. \]

It is meaningless over the reals. CAS often oﬀer no choice than to interprete surds over the complex numbers even if they distinguish between a real and a complex mode.

Corless and Jeﬀrey [CJ92] have examined the behavior of a number of CAS with such input data. They come to the conclusion that simultaneous computation of all cases is exemplary but not feasible due to the combinatorial explosion of cases to be considered. Therefore, they suggest to ignore the degenerate cases but to provide the assumptions to the user on request. We claim, in contrast, that it is in fact feasible to compute all possible cases.

Our setting is as follows: Expressions are evaluated to guarded expressions consisting of possibly several conventional expressions guarded by quantiﬁer-free formulas. For the above examples, we would obtain

\[ \begin {gex} \gc {x\neq 0}&\gc {x} \end {gex},\quad \begin {gex} \gc {\false }&\gc {\frac {\sqrt {x}+\sqrt {-x}}{x}} \end {gex}. \]

As the second example illustrates, we are working in ordered ﬁelds, more precisely in real closed ﬁelds. The handling of guarded expressions as described in this paper can, however, be easily transferred to other situations.

Our approach can also deal with redundant guarded expressions, such as

\[ \begin {gex} \gc {\true } & \gc {|x|-x}\\ x\geq 0 & 0\\ x<0 & -2x \end {gex} \]

which leads to algebraic simpliﬁcation techniques based on logical simpliﬁcation as proposed by Davenport and Faure [DF94].

We use formulas over the language of ordered rings as guards. This provides powerful tools for heuristically reducing the combinatorial explosion of cases: equivalent, redundant, tautological, and contradictive cases can be detected by simpliﬁcation [DS97b] and quantiﬁer elimination [Tar48, Col75, Wei88, RLW93, Wei97, Wei94]. In certain situations, we will allow the formulas also to contain extra functions such as \(\sqrt {\cdot }\) or \(|\cdot |\). Then we take care that there is no quantiﬁer elimination applied.

Simultaneous computation of several cases concerning certain expressions being zero or not has been extensively investigated as dynamic evaluation [GD96, DR94a, DR94b, BGDW95]. It has also been extended to real closed ﬁelds [DGV96]. The idea behind the development of these methods is of a more theoretical nature than to overcome the problems with the interactive usage of CAS sketched above: one wishes to compute in algebraic (or real) extension ﬁelds of the rationals. Guarded expressions occur naturally when solving problems parametrically. Consider, e.g., the Gröbner systems used during the computation of comprehensive Gröbner bases [Wei92].

The algorithms described in this paper are implemented in the REDUCE package GUARDIAN. It is based on the REDUCE [Hea95, Mel95] package REDLOG [DS97a, DS96] implementing a formula data type with corresponding algorithms, in particular including simpliﬁcation and quantiﬁer elimination.

20.27.2 An outline of our method

Guarded expressions

A guarded expression is a scheme

\[ \begin {gex} \gc {\gamma _0} & \gc {t_0}\\ \gamma _1 & t_1\\ \vdots& \vdots \\ \gamma _n& t_n \end {gex} \]

where each \(\gamma _i\) is a quantiﬁer-free formula, the guard, and each \(t_i\) is an associated conventional expression. The idea is that some \(t_i\) is a valid interpretation iﬀ \(\gamma _i\) holds. Each pair \((\gamma _i,t_i)\) is called a case.

The ﬁrst case \((\gamma _0,t_0)\) is the generic case: \(t_0\) is the expression the system would compute without our package, and \(\gamma _0\) is the corresponding guard.

The guards \(\gamma _i\) need neither exclude one another, nor do we require that they form a complete case distinction. We shall, however, assume that all cases covered by a guarded expression are already covered by the generic case; in other words:

\begin{equation} \bigwedge _{i=1}^n(\gamma _i\longrightarrow \gamma _0).\label {gencoversall} \end{equation}

Consider the following evaluation of \(|x|\) to a guarded expression:

\[ \begin {gex} \gc {\true } & \gc {|x|}\\ x\geq 0 & x\\ x<0 & -x \end {gex}. \]

Here the non-generic cases already cover the whole domain. The generic case is in some way redundant. It is just present for keeping track of the system’s default behavior. Formally we have

\begin{equation} \Bigl (\bigvee _{i=1}^n\gamma _i\Bigr )\longleftrightarrow \gamma _0. \label {formalredund} \end{equation}

As an example for a non-redundant, i.e., necessary generic case we have the evaluation of the reciprocal \(\frac {1}{x}\):

\[ \begin {gex} \gc {x\neq 0}& \gc {\frac {1}{x}} \end {gex}. \]

In every guarded expression, the generic case is explicitly marked as either necessary or redundant. The corresponding tag is inherited during the evaluation process. Unfortunately it can happen that guarded expressions satisfy (\ref {formalredund}) without being tagged redundant, e.g., specialization of

\[ \begin {gex} \gc {\true }&\gc {\sin x}\\ x=0&0 \end {gex} \]

to \(x=0\) if the system cannot evaluate \(\sin (0)\). This does not happen if one claims for necessary generic cases to have, as the reciprocal above, no alternative cases at all. Else, in the sequel “redundant generic case” has to be read as “tagged redundant.”

With guarded expressions, the evaluation splits into two independent parts: Algebraic evaluation and a subsequent simpliﬁcation of the guarded expression obtained.

Guarding schemes

In the introduction we have seen that certain operators introduce case distinctions. For this, with each operator \(f\) there is a guarding scheme associated providing information on how to map \(f(t_1,\ldots ,t_m)\) to a guarded expression provided that one does not have to care for the argument expressions \(t_1\), …, \(t_m\). In the easiest case, this is a rewrite rule

\[ f(a_1,\ldots ,a_m)\to G(a_1,\ldots ,a_m). \]

The actual terms \(t_1\), …, \(t_m\) are simply substituted for the formal symbols \(a_1\), …, \(a_m\) into the generic guarded expression \(G(a_1,\ldots ,a_m)\). We give some examples:

\begin{align} \frac {a_1}{a_2} & \to \begin {gex} \gc {a_2\neq 0} & \gc {\frac {a_1}{a_2}} \end {gex}\nonumber \\ \sqrt {a_1} & \to \begin {gex} \gc {a_1\geq 0} & \gc {\sqrt {a_1}} \end {gex}\nonumber \\ \sign (a_1) & \to \begin {gex} \gc {\true } & \gc {\sign (a_1)}\\ a_1>0 & 1\\ a_1=0 & 0\\ a_1<0 & -1 \end {gex}\nonumber \\ |a_1| & \to \begin {gex} \gc {\true } & \gc {|a_1|}\\ a_1\geq 0 & a_1\\ a_1<0 & -a_1 \end {gex}\label {absrewrite} \end{align}

For functions of arbitrary arity, e.g., \(\min \) or \(\max \), we formally assume inﬁnitely many operators of the same name. Technically, we associate a procedure parameterized with the number of arguments \(m\) that generates the corresponding rewrite rule. As \(\tt min\_scheme(2)\) we obtain, e.g.,

\[ \min (a_1,a_2) \to \begin {gex} \gc {\true } & \gc {\min (a_1,a_2)}\\ a_1\leq a_2 & a_1\\ a_2\leq a_1 & a_2 \end {gex}\label {binminscheme}, \]

while for higher arities there are more case distinctions necessary.

For later complexity analysis, we state the concept of a guarding scheme formally: a guarding scheme for an \(m\)-ary operator \(f\) is a map

\[ \gscheme _f: \E ^m \to \GE \]

where \(\E \) is the set of expressions, and \(\GE \) is the set of guarded expressions. This allows to split \(f(t_1,\ldots ,t_m)\) in dependence on the form of the parameter expressions \(t_1\), …, \(t_m\).

Algebraic evaluation

Evaluating conventional expressions

The evaluation of conventional expressions into guarded expressions is performed recursively: Constants \(c\) evaluate to

\[ \begin {gex} \gc {\true } & \gc {c} \end {gex}. \]

For the evaluation of \(f(e_1,\ldots ,e_m)\) the argument expressions \(e_1\), …, \(e_m\) are recursively evaluated to guarded expressions

\begin{equation} e_i'=\begin {gex} \gc {\gamma _{i0}} & \gc {t_{i0}}\\ \gamma _{i1} & t_{i1}\\ \vdots & \vdots \\ \gamma _{in_i} & t_{in_i}\end {gex}\quad \mbox {for}\quad 1\leq i\leq m. \label {eprimes} \end{equation}

Then the operator \(f\) is “moved inside” the \(e_i'\) by combining all cases, technically a simultaneous Cartesian product computation of both the sets of guards and the sets of terms:

\begin{equation} \Gamma =\prod _{i=1}^m\{\gamma _{i0},\ldots ,\gamma _{in_i}\},\quad T=\prod _{i=1}^m\{t_{i0},\ldots ,t_{in_i}\}. \label {cartprod} \end{equation}

This leads to the intermediate result

\begin{equation} \begin {gex} \gc {\gamma _{10}\land \dots \land \gamma _{m0}}& \gc {f(t_{10},\dots ,t_{m0})}\\ \vdots &\vdots \\ \gamma _{1n_1}\land \dots \land \gamma _{m0}& f(t_{1n_1},\dots ,t_{m0})\\ \vdots &\vdots \\ \gamma _{1n_1}\land \dots \land \gamma _{mn_m}& f(t_{1n_1},\dots ,t_{mn_m}) \end {gex}. \label {intermediate} \end{equation}

The new generic case is exactly the combination of the generic cases of the \(e_i'\). It is redundant if at least one of these combined cases is redundant.

Next, all non-generic cases containing at least one redundant generic constituent \(\gamma _{i0}\) in their guard are deleted. The reason for this is that generic cases are only used to keep track of the system default behavior. All other cases get the status of a non-generic case even if they contain necessary generic constituents in their guard.

At this point, we apply the guarding scheme of \(f\) to all remaining expressions \(f(t_{1i_1},\ldots ,t_{mi_m})\) in the form (\ref {intermediate}) yielding a nested guarded expression

\begin{equation} \begin {gex} \gc {\Gamma _0} & \begin {gex} \gc {\delta _{00}} & \gc {u_{00}}\\ \vdots & \vdots \\ \delta _{0k_0} & u_{0k_0} \end {gex}\\ \vdots & \vdots \\ \Gamma _N & \begin {gex} \gc {\delta _{N0}} & \gc {u_{N0}}\\ \vdots & \vdots \\ \delta _{Nk_N} & u_{Nk_N} \end {gex} \end {gex},\label {nestedge} \end{equation}

which can be straightforwardly resolved to a guarded expression

\[ \begin {gex} \gc {\Gamma _0\land \delta _{00}} & \gc {u_{00}}\\ \vdots & \vdots \\ \Gamma _0\land \delta _{0k_0} & u_{0k_0}\\ \vdots & \vdots \\ \Gamma _N\land \delta _{N0} & u_{N0}\\ \vdots & \vdots \\ \Gamma _N\land \delta _{Nk_N} & u_{Nk_N} \end {gex}. \]

This form is treated analogously to the form (\ref {intermediate}): The new generic case \((\Gamma _0\land \delta _{00},u_{00})\) is redundant if at least one of \(\bigl (\Gamma _0,f(t_{10},\dots ,t_{m0})\bigr )\) and \((\delta _{00},u_{00})\) is redundant. Among the non-generic cases all those containing redundant generic constituents in their guard are deleted, and all those containing necessary generic constituents in their guard get the status of an ordinary non-generic case.

Finally the standard evaluator of the system—reval in the case of REDUCE—is applied to all contained expressions, which completes the algebraic part of the evaluation.

Evaluating guarded expressions

The previous section was concerned with the evaluation of pure conventional expressions into guarded expressions. Our system currently combines both conventional and guarded expressions. We are thus faced with the problem of treating guarded subexpressions during evaluation.

When there is a guarded subexpression \(e_i\) detected during evaluation, all contained expressions are recursively evaluated to guarded expressions yielding a nested guarded expression of the form (\ref {nestedge}). This is resolved as described above yielding the evaluation subresult \(e_i'\).

As a special case, this explains how guarded expressions are (re)evaluated to guarded expressions.

Example

We describe the evaluation of the expression \(\min (x,|x|)\). The ﬁrst argument \(e_1=x\) evaluates recursively to

\begin{equation} e_1'=\begin {gex} \gc {\true } & \gc {x} \end {gex} \label {evalx} \end{equation}

with a necessary generic case. The nested \(x\) inside \(e_2=|x|\) evaluates to the same form (\ref {evalx}). For obtaining \(e_2'\), we apply the guarding scheme (\ref {absrewrite}) of the absolute value to the only term of (\ref {evalx}) yielding

\[ \begin {gex} \gc {\true } & \begin {gex} \gc {\true } & \gc {|x|}\\ x\geq 0 & x\\ x<0 & -x \end {gex} \end {gex}, \]

where the inner generic case is redundant. This form is resolved to

\[ e_2'=\begin {gex} \gc {\true \land \true } & \gc {|x|}\\ \true \land x\geq 0 & x\\ \true \land x<0 & -x \end {gex} \]

with a redundant generic case. The next step is the combination of cases by Cartesian product computation. We obtain

\[ \begin {gex} \gc {\true \land (\true \land \true )} & \gc {\min (x,|x|)}\\ \true \land (\true \land x\geq 0) & \min (x,x)\\ \true \land (\true \land x<0) & \min (x,-x) \end {gex}, \]

which corresponds to (\ref {intermediate}) above. For the outer \(\min \), we apply the guarding scheme (\ref {binminscheme}) to all terms yielding the nested guarded expression

\[ \begin {gex} \gc {\true \land (\true \land \true )} & \begin {gex} \gc {\true } & \gc {\min (x,|x|)}\\ x\leq |x| & x\\ |x|\leq x & |x| \end {gex}\\ \true \land (\true \land x\geq 0) & \begin {gex} \gc {\true } & \gc {\min (x,x)}\\ x\leq x & x\\ x\leq x & x \end {gex}\\ \true \land (\true \land x<0) & \begin {gex} \gc {\true } & \gc {\min (x,-x)}\\ x\leq -x & x\\ -x\leq x & -x \end {gex} \end {gex}, \]

which is in turn resolved to

\[ \begin {gex} \gc {(\true \land (\true \land \true ))\land \true } & \gc {\min (x,|x|)}\\ (\true \land (\true \land \true ))\land x\leq |x| & x\\ (\true \land (\true \land \true ))\land |x|\leq x & |x|\\ (\true \land (\true \land x\geq 0))\land \true & \min (x,x)\\ (\true \land (\true \land x\geq 0))\land x\leq x & x\\ (\true \land (\true \land x\geq 0))\land x\leq x & x\\ (\true \land (\true \land x<0))\land \true & \min (x,-x)\\ (\true \land (\true \land x<0))\land x\leq -x & x\\ (\true \land (\true \land x<0))\land -x\leq x & -x \end {gex}. \]

From this, we delete the two non-generic cases obtained by combination with the redundant generic case of the \(\min \). The ﬁnal result of the algebraic evaluation step is the following:

\begin{equation} \begin {gex} \gc {(\true \land (\true \land \true ))\land \true } & \gc {\min (x,|x|)}\\ (\true \land (\true \land \true ))\land x\leq |x| & x\\ (\true \land (\true \land \true ))\land |x|\leq x & |x|\\ (\true \land (\true \land x\geq 0))\land x\leq x & x\\ (\true \land (\true \land x\geq 0))\land x\leq x & x\\ (\true \land (\true \land x<0))\land x\leq -x & x\\ (\true \land (\true \land x<0))\land -x\leq x & -x \end {gex}.\label {example} \end{equation}

Worst-case complexity

Our measure of complexity \(|G|\) for guarded expressions \(G\) is the number of contained cases:

\[ \left |\begin {gex} \gc {\gamma _0} & \gc {t_0}\\ \gamma _1 & t_1\\ \vdots& \vdots \\ \gamma _n& t_n \end {gex}\right |=n+1. \]

As in Section 20.27.2.0, consider an \(m\)-ary operator \(f\), guarded expression arguments \(e_1'\), …, \(e_m'\) as in equation (\ref {eprimes}), and the Cartesian product \(T\) as in equation (\ref {cartprod}). Then

\begin{align*} |f(e_1',\ldots ,e_m')| & \leq \sum _{(t_1,\dots ,t_m)\in T}|\gscheme _f(t_1,\dots ,t_m)| \\ & \leq \max _{(t_1,\ldots ,t_m)\in T}|\gscheme _f(t_1,\ldots ,t_m)|\cdot \#T\\ & = \max _{(t_1,\ldots ,t_m)\in T}|\gscheme _f(t_1,\ldots ,t_m)|\cdot \prod _{j=1}^m|e_j'|\\ & \leq \max _{(t_1,\ldots ,t_m)\in T}|\gscheme _f(t_1,\ldots ,t_m)|\cdot \bigl (\max _{1\leq j\leq m}|e_j'|\bigr )^m. \end{align*}

In the important special case that the guarding scheme of \(f\) is a rewrite rule \(f(a_1,\ldots ,a_m)\to G\), the above complexity estimation simpliﬁes to

\[ |f(e_1',\ldots ,e_m')| \leq |G|\cdot \prod _{j=1}^m|e_j'| \leq |G|\cdot \bigl (\max _{1\leq j\leq m}|e_j'|\bigr )^m. \]

In other words: \(|G|\) plays the role of a factor, which, however, depends on \(f\), and \(|f(e_1',\ldots ,e_m')|\) is polynomial in the size of the \(e_i\) but exponential in the arity of \(f\).

Simpliﬁcation

In view of the increasing size of the guarded expressions coming into existence with subsequent computations, it is indispensable to apply simpliﬁcation strategies. There are two diﬀerent algorithms involved in the simpliﬁcation of guarded expressions:

1.: A formula simpliﬁer mapping quantiﬁer-free formulas to equivalent simpler ones.
2.: Eﬀective quantiﬁer elimination for real closed ﬁelds over the language of ordered rings.

It is not relevant, which simpliﬁer and which quantiﬁer elimination procedure is actually used. We use the formula simpliﬁer described in [DS97b]. Our quantiﬁer elimination uses test point methods developed by Weispfenning [Wei88, RLW93, Wei97]. It is restricted to formulas obeying certain degree restrictions wrt. the quantiﬁed variables. As an alternative, REDLOG provides an interface to Hong’s QEPCAD quantiﬁer elimination package [HCJE93]. Compared to the simpliﬁcation, the quantiﬁer elimination is more time consuming. It can be turned oﬀ by a switch.

The following simpliﬁcation steps are applied in the given order:

Contraction of cases This is restricted to the non-generic cases of the considered guarded expression. We contract diﬀerent cases containing the same terms:

\[ \begin {gex} \gc {\gamma _0}&\gc {t_0}\\ \vdots & \vdots \\ \gamma _i & t_i\\ \vdots & \vdots \\ \gamma _j & t_i\\ \vdots & \vdots \end {gex}\quad \mbox {becomes}\quad \begin {gex} \gc {\gamma _0}&\gc {t_0}\\ \vdots & \vdots \\ \gamma _i\lor \gamma _j & t_i\\ \vdots & \vdots \\ \end {gex}. \]

Simpliﬁcation of the guards The simpliﬁer is applied to all guards replacing them by simpliﬁed equivalents. Since our simpliﬁer maps \(\gamma \lor \gamma \) to \(\gamma \), this together with the contraction of cases takes care for the deletion of duplicate cases.

Keep one tautological case If the guard of some non-generic case becomes “\(\true \),” we delete all other non-generic cases. Else, if quantiﬁer elimination is turned on, we try to detect a tautology by eliminating the universal closures \(\underline \forall \gamma \) of the guards \(\gamma \). This quantiﬁer elimination is also applied to the guards of generic cases. These are, in case of success, simply replaced by “\(\true \)” without deleting the case.

Remove contradictive cases A non-generic case is deleted if its guard has become “\(\false \).” If quantiﬁer elimination is turned on, we try to detect further contradictive cases by eliminating the existential closure \(\underline \exists \gamma \) for each guard \(\gamma \). This quantiﬁer elimination is also applied to generic cases. In case of success they are not deleted but their guards are replaced by “\(\false \).” Our assumption (\ref {gencoversall}) allows then to delete all non-generic cases.

Example revisited

We turn back to the form (\ref {example}) of our example \(\min (x,|x|)\). Contraction of cases with subsequent simpliﬁcation automatically yields

\[ \begin {gex} \gc {\true } & \gc {\min (x,|x|)}\\ \true & x\\ |x|-x\leq 0 & |x|\\ \false & -x \end {gex}, \]

of which only the tautological non-generic case survives:

\begin{equation} \begin {gex} \gc {\true } & \gc {\min (x,|x|)}\\ \true & x \end {gex}.\label {minabs} \end{equation}

Output modes

An output mode determines which part of the information contained in the guarded expressions is provided to the user. GUARDIAN knows the following output modes:

Matrix Output matrices in the style used throughout this paper. We have already seen that these can become very large in general.

Generic case Output only the generic case.

Generic term Output only the generic term. Thus the output is exactly the same as without the guardian package. If the condition of the generic case becomes “\(\false \),” a warning “contradictive situation” is given. The computation can, however, be continued.

Note that output modes are restrictions concerning only the output; internally the system still computes with the complete guarded expressions.

A smart mode

Consider the evaluation result (\ref {minabs}) of \(\min (x,|x|)\). The generic term output mode would output \(\min (x,|x|)\), although more precise information could be given, namely \(x\). The problem is caused by the fact that generic cases are used to keep track of the system’s default behavior. In this section we will describe an optional smart mode with a diﬀerent notion of generic case. To begin with, we show why the problem can not be overcome by a “smart output mode.”

Assume that there is an output mode which outputs \(x\) for (\ref {minabs}). As the next computation involving (\ref {minabs}) consider division by \(y\). This would result in

\[ \begin {gex} \gc {y\neq 0} & \gc {\frac {\min (x,|x|)}{y}}\\ y\neq 0 & \frac {x}{y} \end {gex}. \]

Again, there are identic conditions for the generic case and some non-generic case, and, again, the term belonging to the latter is simpler. Our mode would output \(\frac {x}{y}\). Next, we apply the absolute value once more yielding

\[ \begin {gex} \gc {y\neq 0} & \gc {\frac {|\min (x,|x|)|}{|y|}}\\ xy\geq 0 \land y\neq 0 & \frac {x}{y}\\ xy<0 \land y\neq 0 & \frac {-x}{y} \end {gex}. \]

Here, the condition of the generic case diﬀers from all other conditions. We thus have to output the generic term. For the user, the evaluation of \(|\frac {x}{y}|\) results in \(\frac {|\min (x,|x|)|}{|y|}\).

The smart mode can turn a non-generic case into a necessary generic one dropping the original generic case and all other non-generic cases. Consider, e.g., (\ref {minabs}), where the conditions are equal, and the non-generic term is “simpler.”

In fact, the relevant relationship between the conditions is that the generic condition implies the non-generic one. In other words: Some non-generic condition is not more restrictive than the generic condition, and thus covers the whole domain of the guarded expression. Note that from the implication and (\ref {gencoversall}) we may conclude that the cases are even equivalent.

Implication is heuristically checked by simpliﬁcation. If this fails, quantiﬁer elimination provides a decision procedure. Note that our test point methods are incomplete in this regard due to the degree restrictions. Also it cannot be applied straightforwardly to guards containing operators that do not belong to the language of ordered rings.

Whenever we happen to detect a relevant implication, we actually turn the corresponding non-generic case into the generic one. From our motivation of non-generic cases, we may expect that non-generic expressions are generally more convenient than generic ones.

20.27.3 Examples

We give the results for the following computations as they are printed in the output mode matrix providing the full information on the computation result. The reader can derive himself what the output in the mode generic case or generic term would be.

Smart mode or not:
\[ \frac {1}{x^2+2x+1}=\begin {gex} \gc {x+1\neq 0}& \gc {\frac {1}{x^2+2x+1}} \end {gex}. \]
The simpliﬁer recognizes that the denominator is a square.
Smart mode or not:
\[ \frac {1}{x^2+2x+2}=\begin {gex} \gc {\true }& \gc {\frac {1}{x^2+2x+2}} \end {gex}. \]
Quantiﬁer elimination recognizes the positive deﬁniteness of the denominator.
Smart mode:
\[ |x|-\sqrt {x}=\begin {gex} \gc {x\geq 0} & \gc {-\sqrt {x}+x} \end {gex}. \]
The square root allows to forget about the negative branch of the absolute value.
Smart mode:
\[ |x^2+2x+1|=\begin {gex} \gc {\true }&\gc {x^2+2x+1} \end {gex}. \]
The simpliﬁer recognizes the positive semideﬁniteness of the argument. REDUCE itself recognizes squares within absolute values only in very special cases such as \(|x^2|\).
Smart mode:
\[ \min \bigl (x,\max (x,y)\bigr )=\begin {gex} \gc {\true }&\gc {x} \end {gex}. \]
Note that REDUCE does not know any rules about nested minima and maxima.
Smart mode:
\[ \min \bigl (\sign (x),-1\bigr )=\begin {gex} \gc {\true }&\gc {-1} \end {gex}. \]
Smart mode or not:
\[ |x|-x=\begin {gex} \gc {\true }&\gc {|x|-x}\\ x\geq 0&0\\ x<0&-2x \end {gex}. \]
This example is taken from [DF94].
Smart mode or not:
\[ \sqrt {1+x^2 y^2 (x^2+y^2-3)}={} \begin {gex}\gc {\true }&\gc {\sqrt {x^4 y^2 + x^2 y^4 - 3 x^2 y^2 + 1}}\end {gex} \]
The Motzkin polynomial is recognized to be positive semideﬁnite by quantiﬁer elimination.

The evaluation time for the last example is 119 ms on a SUN SPARC-4. This illustrates that eﬃciency is no problem with such interactive examples.

20.27.4 Outlook

This section describes possible extensions of the GUARDIAN. The extensions proposed in Section 20.27.4.0 on simpliﬁcation of terms and Section 20.27.4.0 on a background theory are clear from a theoretical point of view but not yet implemented. Section 20.27.4.0 collects some ideas on the application of our ideas to the REDUCE integrator. In this ﬁeld, there is some more theoretical work necessary.

Simpliﬁcation of terms

Consider the expression \(\sign (x)x-|x|\). It evaluates to the following guarded expression:

\[ \begin {gex} \gc {\true } & \gc {-|x|+\sign (x)x}\\ x\neq 0 & 0\\ x=0 & -x \end {gex}. \]

This suggests to substitute \(-x\) by \(0\) in the third case, which would in turn allow to contract the two non-generic cases yielding

\[ \begin {gex} \gc {\true } & \gc {-|x|+\sign (x)x}\\ \true & 0\end {gex}. \]

In smart mode second case would then become the only generic case.

Generally, one would proceed as follows: If the guard is a conjunction containing as toplevel equations

\[ t_1=0,\quad \dots ,\quad t_k=0, \]

reduce the corresponding expression modulo the set of univariate linear polynomials among \(t_1\), …, \(t_k\).

A more general approach would reduce the expression modulo a Gröbner basis of all the \(t_1\), …, \(t_k\). This leads, however, to larger expressions in general.

One can also imagine to make use of non-conjunctive guards in the following way:

1.: Compute a DNF of the guard.
2.: Split the case into several cases corresponding to the conjunctions in the DNF.
3.: Simplify the terms.
4.: Apply the standard simpliﬁcation procedure to the resulting guarded expression. Note that it includes contraction of cases.

According to experiences with similar ideas in the “Gröbner simpliﬁer” described in [DS97b], this should work well.

Background theory

In practice one often computes with quantities guaranteed to lie in a certain range. For instance, when computing an electrical resistance, one knows in advance that it will not be negative. For such cases one would like to have some facility to provide external information to the system. This can then be used to reduce the complexity of the guarded expressions.

One would provide a function assert(\(\varphi \)), which asserts the formula \(\varphi \) to hold. Successive applications of assert establish a background theory, which is a set of formulas considered conjunctively. The information contained in the background theory can be used with the guarded expression computation. The user must, however, not rely on all the background information to be actually used.

Technically, denote by \(\Phi \) the (conjunctive) background theory. For the simpliﬁcation of the guards, we can make use of the fact that our simpliﬁer is designed to simplify wrt. a theory, cf. [DS97b]. For proving that some guard \(\gamma \) is tautological, we try to prove

\[\underline {\forall }(\Phi \longrightarrow \gamma )\]

instead of \(\underline {\forall }\gamma \). Similarly, for proving that \(\gamma \) is contradictive, we try to disprove

\[\underline {\exists }(\Phi \land \gamma ).\]

Instead of proving \(\underline {\forall }(\gamma _1\longrightarrow \gamma _2)\) in smart mode, we try to prove

\[\underline {\forall }\bigl ((\Phi \land \gamma _1)\longrightarrow \gamma _2\bigr ).\]

Independently, one can imagine to use a background theory for reducing the output with the matrix output mode. For this, one simpliﬁes each guard wrt. the theory at the output stage treating contradictions and tautologies appropriately. Using the theory for replacing all cases by one at output stage in a smart mode manner leads once more to the problem of expressions or even guarded expressions “mysteriously” getting more complicated. Applying the theory only at the output stage makes it possible to implement a procedure unassert(\(\varphi \)) in a reasonable way.

Integration

CAS integrators make “mistakes” similar to those we have examined. Consider, e.g., the typical result

\[ \int x^a\,dx=\frac {1}{a+1}x^{a+1}. \]

It does not cover the case \(a=-1\), for which one wishes to obtain

\[ \int x^{-1}\,dx=\ln x. \]

This problem can also be solved by using guarded expressions for integration results.

Within the framework of this paper, we would have to associate a guarding scheme to the integrator int. It is not hard to see that this cannot be done in a reasonable way without putting as much knowledge into the scheme as into the integrator itself. Thus for treating integration, one has to modify the integrator to provide guarded expressions.

Next, we have to clarify what the guarded expression for the above integral would look like. Since we know that the integral is deﬁned for all interpretations of the variables, our assumption (\ref {gencoversall}) implies that the generic condition be “\(\true \).” We obtain the guarded expression

\[ \begin {gex} \gc {\true }& \gc {\int x^a\,dx}\\ a\neq -1& \frac {1}{a+1}x^{a+1}\\ a=-1 & \ln x \end {gex}. \]

Note that the redundant generic case does not model the system’s current behavior.

Combining algebra with logic

Our method, in the described form, uses an already implemented algebraic evaluator. In the previous section, we have seen that this point of view is not suﬃcient for treating integration appropriately.

Also our approach runs into trouble with built-in knowledge such as

\begin{align} \sqrt {x^2} &= |x|\label {sqrtrule},\\ \sign (|x|) &= 1\label {signrule}. \end{align}

Equation (\ref {sqrtrule}) introduces an absolute value operator within a non-generic term without making a case distinction. Equation (\ref {signrule}) is wrong when not considering \(x\) transcendental. In contrast to the situation with reciprocals, our technique cannot be used to avoid this “mistake.” We obtain

\[ \sign (|x|)=\begin {gex} \gc {\true } & \gc {1}\\ x\neq 0 & 1\\ x=0 & 0 \end {gex} \]

yielding two diﬀerent answers for \(x=0\).

We have already seen in the example Section 20.27.3 that the implementation of knowledge such as (\ref {sqrtrule}) and (\ref {signrule}) is usually quite ad hoc, and can be mostly covered by using guarded expressions. This observation gives rise to the following question: When designing a new CAS based on guarded expressions, how should the knowledge be distributed between the algebraic side and the logic side?

20.27.5 Conclusions

Guarded expressions can be used to overcome well-known problems with interpreting expressions as terms. We have explained in detail how to compute with guarded expressions including several simpliﬁcation techniques. Moreover we gain algebraic simpliﬁcation power from the logical simpliﬁcations. Numerous examples illustrate the power of our simpliﬁcation methods. The largest part of our ideas is eﬃciently implemented, and the software is published. The outlook on background theories and on the treatment of integration by guarded expressions points on interesting future extensions.

PrevTail

Front

Hosted by