Dépt. de Mathématiques
(Bât. 425)
Université Paris-Sud
91405 Orsay Cedex
France
Email: joris@texmacs.org
A new zero-test for formal power
series
November 03, 2023
Abstract
In this paper, we present a new zero-test 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.
Zero-testing 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 non-ambiguity of expressions may be ensured by structural induction. This may involve zero-testing for the series represented by subexpressions.
Several classical approaches for zero-testing exist [9, 6, 10, 11, 7, 12] and we provide a quick survey of them in section 2. Our new zero-test, 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 non-trivial 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 zero-test.
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.
, where 
denotes the input
size) for the number of zeros for systems of real Pfaffian functions
[6]. These bounds may be adapted to the power series
context.
This approach is interesting because it only requires fast power series
expansions [3, 14] for implementing a
zero-test. However, such a zero-test 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 Khovanskii-type 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.
. If we want to test a new
relation, then we include it in and look
whether we obtain a contradiction. If not, then we keep on adding the
derivatives of all relations in into . Under certain hypotheses, this
process always ends up in a contradiction or a proof that the added
relations all hold. However, the approach does not seem to provide any
reasonable complexity bounds.
at the top of this section are
usually specified by a finite number of algebraic differential
equations and initial conditions. Now instead of asking whether a
given expression represents zero, we may ask for which initial
conditions for the expression represents zero.
It turns out that the set of such initial conditions is a closed
algebraic set 
. The
“difficult” cases in the zero-test 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.
and that 
satisfies the
algebraic differential equation 
.
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 non-degeneracy 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 zero-testing).
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 non-zero 
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 well-ordered 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
is again an effective power series domain, we may repeat the
construction after replacing 
by , and add as many other functions 
as we like. In fact, it suffices to add one 
for each new subexpression of the form 
.
It is well known that any non-trivial 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 grid-based, if
there exist monomials 
and 
in , such that 
. A grid-based logarithmic transseries
is a mapping 
with grid-based 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
non-zero 
is grid-based (whence well-ordered),
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 grid-based 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 
be a differential polynomial of the form be a
solution to and let 
be
defined as in section 3. Then the equation 
with side condition 
admits 
as its unique solution in 
.
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 non-zero 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 multi-indices 
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
non-zero constant root 
(and 
is a potential dominant term). Furthermore,
admits a non-zero 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 non-logarithmic 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 non-zero 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 grid-based 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 quasi-linear 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 quasi-linear 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 
over . Then 
solutions in
when counting with multiplicities.
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
if and only if
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 and 
, its Newton degree 
is
the minimal degree of a term 
in 
with 
.
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 terminates and is
correct.
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 zero-test 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 well-ordered, 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 .