
Abstract
In this paper, we present a new zerotest for expressions which are constructed from formal power solutions to algebraic differential equations using the ring operations and differentiation. We also provide a survey of all existing methods that we know of and a detailed comparison of these methods with our approach.
Zerotesting is an important issue on the analysis side of symbolic computation. Standard mathematical notation provides a way of representing many transcendental functions. However, trivial cases apart, this notation gives rise to the following problems:
Expressions may not be defined: consider , or .
Expressions may be ambiguous: what values should we take for or ?
Expressions may be redundant: and are different expressions, but they represent the same function.
Often, one is interested in expressions which represent functions in a ring. In that case, the third problem reduces to deciding when a given expression represents the zero function.
As to the first two problems, one has to decide where and how we want our functions to be defined. In this paper, we will be concerned with expressions that represent formal power series (in fact, this approach covers most elementary calculus on special functions, using analytic continuation if necessary). The expressions will then be formed from the constants and the indeterminates using the ring operations and power series solutions to algebraic differential equations. The correctness and nonambiguity of expressions may be ensured by structural induction. This may involve zerotesting for the series represented by subexpressions.
Several classical approaches for zerotesting exist [9, 6, 10, 11, 7, 12] and we provide a quick survey of them in section 2. Our new zerotest, which is described in section 5, is based on a similar approach as [10, 11, 12]. We believe the algorithm to be interesting for five main reasons:
We treat differential equations of arbitrary order.
Our method accommodates divergent power series solutions.
It reformulates previous work from [10, 11, 12] in the more standard setting of differential algebra.
We believe it to be more efficient. With some more work, it might be possible to give complexity bounds for the algorithm (or a modified version of it) along the same lines as [12]. Such bounds are also interesting in relation to “witness conjectures” [17, 13, 16, 8].
On the longer run, the algorithm might generalize to the multivariate setting of partial differential equations with initial conditions on a subspace of dimension .
Throughout the paper, we will assume that the reader is familiar with differential algebra and the notations used in this field; see section 3 and [2] for a nice introduction. The proof of our algorithm also uses a result from the preprint [15], which is too complicated to be presented here, although we do provide a sketch of the proof in section 4.
We plan to provide some examples and more explanations in a forthcoming journal paper. We are also writing a lecture note about the subject of section 4. No implementations are available yet.
A differentially algebraic power series is a power series which satisfies a nontrivial algebraic differential equation . Consider a power series expression constructed from and the constants in some field like , using and left composition of infinitesimal power series by differentially algebraic power series . Then it is a classical problem to test whether such an expression represents zero. There are many approaches for this problem.
A more interesting example is obtained when we also allow left composition with and . In this case, the Ax theorem [1] and the Risch structure theorem [9] may be used to design a fast zerotest.
The structural approach may yield very efficient algorithms when it works. However, it requires the characterization of all possible relations in a given context, where we merely asked for a test whether a particular one holds. Consequently, the approach usually only applies in very specific situations.
This approach is interesting because it only requires fast power series expansions [3, 14] for implementing a zerotest. However, such a zerotest might be slow for expressions which can be quickly rewritten to zero (like , where is a complicated expression). Also, if we want the approach to be efficient, good bounds (such as the ones predicted by witness conjectures [17, 13, 16, 8]) would be necessary. At the moment, we only have Khovanskiitype bounds in the case of Pfaffian functions. A new strategy for obtaining bounds, which might generalize to higher order equations by adapting the algorithm in this paper, has been proposed in [12]. However, the obtained bounds are still doubly exponential.
It turns out that the set of such initial conditions is a closed algebraic set . The “difficult” cases in the zerotest correspond to the situation in which the original initial conditions are in the closure of an open subset of where the answer is “easier”. It would be interesting to investigate whether this approach of varying the initial conditions may yield a better power series analogue for Khovanskii's results. A present disadvantage of the method is that it only applies in the convergent case and that it is not yet clear how to obtain complexity bounds.
Now suppose that we want to test whether for a second algebraic differential polynomial . Then we first use differential algebra to determine a third equation which is equivalent to and under certain nondegeneracy conditions. Now we consider as an indeterminate and try to solve in a suitable differential overfield of . This field consists of so called logarithmic transseries and has the nice property that still has a unique solution in for the initial conditions of . Hence, if and only if admits a solution in , in which case we necessarily have .
The approach has the advantages that it accommodates divergent differentially algebraic power series and that the degeneracy of the initial conditions is not amplified during the resolution process. We also have a good hope to obtain complexity bounds along the same lines as in [12] and some hope to generalize the approach to the multivariate setting. We finally expect the approach to be one of the most efficient ones in practice, although no implementations are available yet.
Let be an effective field of constants of characteristic . This means that all elements of can be represented effectively and that there are algorithms for performing the field operations and testing equality (or, equivalently, for zerotesting).
Let be an effective differential ring (i.e. the differentiation is effective too). We assume that the elements of are formal power series in , that , and that the differentiation on corresponds to the differentiation on . Moreover, we will assume that is an effective power series domain, i.e. there exists an algorithm which takes and on input and which computes the coefficient of in . Notice that this implies the existence of an algorithm to compute the valuation of .
Now consider a non zero differential polynomial of order (recall that ) and a power series solution to . We will assume that is not a multiple solution, i.e. for some (if is a multiple solution, then we may always replace by a nonzero and continue doing this until is no longer a multiple solution). Choose such that the valuation of is minimal, say . Then modulo a transformation of the form
and division of the equation by a suitable power of , we may also assume that
(1) 
where and . Let be the polynomial we get from when reinterpreting as an indeterminate . Then (1) yields a recurrence relation for all but a finite number of coefficients of :
(2) 
Indeed, the only for which this relation does not hold are roots of . There are at most such and they correspond to the initial conditions for . Let be the largest root of in (or if such a root does not exist). Then we notice in particular that is the unique solution to whose first coefficients are .
In what follows, we will show that the differential ring is again an effective power series domain. Now elements in can naturally be represented as the images of differential polynomials in under the substitution . It therefore suffices to design an algorithm to test whether for a given differential polynomial . Our algorithm is based on Ritt reduction and the resolution of algebraic equation in more general rings of formal power series. We will use standard notations from differential algebra:
denotes the initial and denotes the separant of a differential polynomial .
The rank of is given by , where is the order of and the degree of in . Notice that the set of possible ranks is wellordered w.r.t. the lexicographical ordering. We will write for .
Given , we denote by the Ritt reduction of with respect to . We thus have a relation
where , and .
Remark
It is well known that any nontrivial algebraic equation with coefficients in has a solution in the field of Puiseux series over the algebraic closure of . We will sketch the proof of an analogous result in the case of algebraic differential equations. For a full proof (of a more general result) we refer to [15].
In order to solve equations of the form , it is clear that solutions to such equations might involve logarithms. In fact, they may even involve iterated logarithms.
Let be the totally ordered group of logarithmic monomials with powers in . More precisely, the elements of are monomials
(3) 
where and stands for the th iterated logarithm. Given such a monomial, we write if and only if , where denotes the least with in (3). This defines a total ordering on . The asymptotic relation corresponds to writing as in analysis.
A subset is said to be gridbased, if there exist monomials and in , such that . A gridbased logarithmic transseries is a mapping with gridbased support. We will usually write such series using the infinite sum notation and we denote the set of all logarithmic transseries by . Since the support of each nonzero is gridbased (whence wellordered), this support admits a maximal element which is called the dominant monomial of .
It can be shown [13] that is a field for the operations
In the second formula, the gridbased support property ensures that is a finite sum. There also exists a natural derivation on , which sends each monomial of the form (3) to
(4) 
This derivation extends to the whole of by (infinitary) “strong linearity” [13].
Before proving that solutions to algebraic differential equations with coefficients in always exist, we first observe that we have the following uniqueness result:
Lemma
Proof. Each series in may be expanded as a Puiseux series in
(5) 
where the coefficients are series in and . Notice that we may interpret as the lexicographical product of and . For the expansion (5), the recurrence relation (2) still determines the coefficients of in a unique way for all .
A classical way to solve algebraic equations over power series is to use the Newton polygon method. We have generalized this method to algebraic differential equations. In fact, it is more convenient to solve asymptotic differential equations of the form
(6) 
where and . In the sequel, we will assume that is algebraically closed.
In order to solve (6), we start by determining all possible dominant monomials of nonzero solutions and their corresponding coefficients. Actually, it is convenient to characterize such potential dominant monomials first. It suffices to characterize when is a potential dominant monomial: we will then say that is a potential dominant monomial, if is a potential dominant monomial for the equation
Here denotes the unique differential polynomial in with for all .
Write using multiindices and let . Then the dominant part of is defined to be the scalar differential polynomial
in , where . We also define the dominant part of w.r.t. by
where is the valuation of in and denotes the coefficient of in .
Assume first that and . Then we define the differential Newton polynomial of by and we have
for all and . Here , if with . We say that is a potential dominant monomial of a solution to if and only if admits such a nonzero constant root (and is a potential dominant term). Furthermore, admits a nonzero root if and only if , because and is algebraically closed.
If or , then we use the technique of “upward shifting”. Given , we define to be the unique differential polynomial in such that
for all . For instance, , and we notice that the logarithmic solution of transforms to the nonlogarithmic solution of under upward shifting . Now we proved in [15] that after a finite number of replacements we obtain a differential polynomial with and . We say that is a potential dominant monomial w.r.t. (6) if and only if and admits a nonzero root in .
It is clear that if is a solution to (6), then must be a potential dominant monomial of a solution. We say that a potential dominant monomial is classical, if is not homogeneous (i.e. ). These classical potential dominant monomials are finite in number and they can be determined from something which resembles the Newton polygon in the algebraic case [13, 15], by using a succession of multiplicative conjugations and upward shiftings of the dominant parts w.r.t. .
Once we have found a potential dominant term of a solution to (6), we may consider the refinement
(7) 
In other words, a refinement is a change of variables together with the imposition of a new asymptotic constraint. It transforms (6) into a new asymptotic differential equation
(8) 
Using the possibly transfinite process of determining potential dominant terms and making refinements, one finds all solutions to (6). However, a more careful study is required to ensure that one remains in the context of gridbased transseries and that (for instance) no transseries like
(9) 
may occur as solutions of (6).
In order to do this, it is convenient to associate an invariant to the equation (6): the highest possible degree of the differential Newton polynomial that we can achieve for a monomial is called the Newton degree of (6) and we denote it by . In the algebraic case, the Newton degree measures the number of solutions to the asymptotic equation (6), when counting with multiplicities. In the differential case, it only gives a lower bound (see theorem 3 below). Also, an equation of Newton degree does not admit any solutions.
Now we have shown in [13, 15] that the Newton degree decreases during refinements and that quasilinear equations (i.e. equations of Newton degree ) always admit solutions. Finally, in the case when , it is possible to replace by a solution to a quasilinear equation of the form
(10) 
and force the Newton degree to strictly decrease after a finite number of steps. In other words, the transfinite resolution process has been replaced by an essentially finite algorithm, which avoids solutions of the form (9). In particular, these methods yield the following theorem:
Theorem
In this sequel, we assume that , and are as in section 3. We will give an algorithm to test whether for given . We will write if and only .
Algorithm 0
Step 1 [Initialize]
Step 2 [Reduction]
while
if then return
else if then
else if then
else if then
else
Step 3 [Final test]
let be minimal with
return
Remark
In particular, the minimal in step 3 can be found by expanding the power series coefficients of in using any fast expansion algorithm for solutions to differential equations [3, 14].
Theorem
Proof. In the loop in step 2, we notice that the rank of strictly decreases at each iteration. Also, the rank of (or ) in each recursive call of the zerotest is strictly smaller than the rank of (and whence the rank of ). These two observations, and the fact that the set of possible ranks is wellordered, imply the termination of the algorithm; the existence of a minimal with will be proved below.
As to the correctness of the algorithm, we claim that at the start and the end inside the loop in step 2, we maintain the properties that and the existence of a relation of the form
(11) 
for and differential polynomials and with . Indeed, we have and at the first entry. If and , then we have , with . If , and , then for some and differential polynomial . Also, , where is the degree of in the highest occurring in . Consequently, denoting , we have . The case when is treated in a similar way. This proves our claim; notice that (11) implies . By definition, we also have if at the first test in the loop.
Let us now assume that the algorithm reaches step 3. Since , we may write with for some . For this , we have , which implies that there exists a minimal number , such that both and . If , then we have , whence and . Conversely, assume that . Then theorem 3 implies the existence of a series with and . Since and , we have a relation of the form
(12) 
where and are differential polynomials. Now implies , so that . But, by lemma 2, there exists a unique solution in to the equation with the side condition . Hence , and .