
. This article has been written using GNU TeXmacs [7].
One fundamental problem in symbolic computation is zero testing of expressions that involve special functions. Several such zero tests have been designed for the case when such special functions satisfy algebraic differential equations or linear difference equations. In this paper, we present an algorithm for the case of power series solutions to certain nonlinear difference equations.

How far can we push exact computations with symbolic mathematical expressions? Starting from polynomial arithmetic, efficient algorithms have been developed for computing with expressions that involve increasingly elaborate algebraic and transcendental functions. The central problem for such computations is to decide whether two expressions represent the same mathematical function or constant. This problem in turn reduces to testing whether a given expression represents zero.
One popular traditional approach for zero testing is based on “structure theorems”. For instance, given a function that is built up using algebraic functions, exponentiation, and logarithm, we may test whether using the Risch structure theorem [10]. Zeilberger's holonomic systems approach [12] is another popular tool for proving equalities, in the restricted setting of solutions to linear differential and difference equations. A powerful theoretical approach for computations with power series solutions to nonlinear differential equations was proposed by Denef and Lipshitz in [2, 3]. Several more practical alternative algorithms have also been developed for that purpose [11, 9, 4, 6].
In this paper, we study the zero testing problem for solutions of nonlinear difference equations. For such equations there are two prominent solution spaces: power series and sequences. In the latter case, there exists a zerotest for a large class of nonlinear algebraic difference equations [8]. We will consider the power series case.
In order to state our main result, we need to introduce a few notions. A power series domain is a algebra with and such that is closed under division whenever defined. We say that is a difference power series domain if it is also closed under the difference operator for some fixed . Note that the standard shift operator is of this form if one considers the power series expansion at infinity, that is, (see Example 1). Finally, is said to be effective if all these operations can be carried out through algorithms. Now assume that we are given a power series solution to the equation
(1) 
for some nontrivial polynomial . Such a power series is said to be algebraic over . A typical example is the power series part of Stirling's asymptotic expansion for the function: see section 6.1. Our main result (see section 5) is a zerotest for elements in under assumption (note that this assumption can be forced by differentiating a finite number of times). In particular, this implies that is again an effective difference power series domain.
A similar type of zerotest was designed in [4, 6] for the case when the difference operator is replaced by differentiation with respect to . We show that this approach can indeed be transposed, but there are a few subtleties. The algorithm in the differential case exploits the fact that a prime univariate differential ideal is defined by a single differential equation. In the present setting, the main difficulty is that this is not longer the case in difference algebra, so we have to work with a system of compatible difference equations (called a coherent autoreduced chain). One of the key ingredients of our algorithm, Proposition 6, is an existence result for a power series solution to such a system of difference equations.
Another feature of our algorithm is that it integrates an optimization of [6] over [4]: in order to test whether for some , the number of coefficients of that we need to evaluate only depends on and , but not on the individual coefficients of .
A proofofconcept implementation of the algorithm in Julia based on the OSCAR computer algebra system is available at https://github.com/pogudingleb/DifferenceZeroTest.
Let us start with some notions from difference algebra. Let be a field of characteristic zero. A difference algebra is a algebra together with an injective morphism of algebras. In what follows, we will always assume that is also an integral domain.
Given an indeterminate , we denote by the difference ring of difference polynomials in and by its fraction field. The algebraic variables are naturally ordered by .
For a difference polynomial , the leader of is the largest variable that occurs in , and we set . We write with and and define:
, the initial of ;
, the separant of P;
, the extended leader of ;
, the Ritt rank of .
It is convenient to further extend the definition of Ritt rank by setting for polynomials . We finally define a total ordering and a partial ordering on Ritt ranks by
A list of difference polynomials such that is called a chain.
Given , we say that is reducible with respect to a chain if there exists an with . For such that , we define the remainder of with respect to denoted by as follows:
If is not reducible with respect to , we set ;
Let be the remainder of the Euclidean pseudodivision of by as univariate polynomials in . We set .
For a chain , we define
If , we say that is reduced to zero with respect to .
Let us now consider such that and are incomparable for . So either and , or and . If , then we define the polynomial of and by
If , then we define .
We say that the chain is autoreduced if is reduced with respect to for each . We say that is coherent if for all such that and are incomparable for .
Consider a power series with and . Then we may define an injective homomorphism of algebras by
so is a difference algebra with respect to the mapping . From now on, we will assume that is a difference subalgebra of for (in particular, is closed under ). In addition, we assume that whenever . This allows us to define a second operator
on and we note that any operator in can be rewritten as an operator in by substituting for .
Example
The corresponding operator in this case will be . The conversion between and can be performed by formulas
For example, the operator can be written as
Given , we will denote by its valuation in . We extend this valuation to difference polynomials in so that is the minimum of the valuation of the nonzero coefficients of if and otherwise. The advantage of using the operator instead of is that for all . More generally, assume that is a linear difference polynomial of order . For each , we have . Let . Then, for any , we have
Furthermore, the coefficient in front of in can be written as
(2) 
where is the indicial polynomial of defined by
In particular, whenever , we have , so does not vanish at . We will denote by the largest root of in , while taking if no such root exists. This number will be an upper bound for the valuation of a power series solutions of .
Example
Given a general difference polynomial and a “point” , the unique difference polynomial such that
for all is called the additive conjugate of by . This transformation can be thought as shifting the “origin” to .
For every difference polynomial and , we define to be the homogeneous component of degree in . If has total degree , then is the decomposition of into homogeneous parts. Given , we will use as an abbreviation for .
In order to ensure the existence of solutions to certain difference equations, it is convenient to also consider logarithmic power series . Such series can still be considered as power series in and we will still denote by the valuation of in . The coefficients are polynomials in , and we will write . Note that, for every and , we have
This allows us to generalize (2) to the case when and is a homogeneous linear differential polynomial:
(3) 
where acts on as the derivation with respect to .
Let be a field of characteristic zero. Let be a difference subalgebra of with corresponding shift operator . Assume furthermore that, for all and such that , we have . We call such an algebra a difference power series domain. A series is said to be algebraic over if it satisfies a nontrivial difference equation with .
Assume now that is an effective power series domain. The most obvious way to effectively represent a algebraic power series over is to represent it by a pair where is a computable series and a nontrivial annihilator with . We say that the annihilator is nondegenerate if .
Let be algebraic over with annihilator . Assume that there exists a number such that for any with , we have . Then we define to be the smallest such number and call it the root separation of at . It corresponds to the number of initial conditions that should be known in order to determine in a unique way as a root of .
(4) 
Proof. Since does not vanish at , we have . Let . Given with , we have
(5) 
Now assume that . Then
whence
Since , we also get , which entails .
What we will really need is a stronger version of Proposition 3 that also takes care of logarithmic power series solutions. Assume that there exists a number such that for any with , we have . Then we define to be the smallest such number and call it the strong root separation of at .
(6) 
Proof. The proof is similar to the proof of Proposition 3 with the following change. Writing with , we now have
(7) 
instead of (5), and where stands for a polynomial of degree at most in .
Note that in the both propositions above, the nondegeneracy of the annihilator implies that , so the provided bounds are always finite.
The following proposition also provides us with a partial converse of Proposition 4.
Proof. implies that . Let . We have to show the existence of a unique series with and . We may decompose
Extracting the coefficient of in the relation now yields (similarly to (3))
(8) 
For all , the right hand side only depends on , and is a nonzero differential operator with . Then [6, Proposition 1] implies that the equation has a solution in for any . Therefore, there exists a solution to the equation .
;
, for ;
.
Then .
Proof. Let us prove by induction that for . The base case is already given. Assume that . Since is autoreduced, the reduction of with respect to vanishes. Since the leader of is at most , the polynomial also reduces to zero with respect to . Setting , the reduction of with respect to therefore yields a relation
where and the reduction of with respect to is zero. Since and for all , we actually must have . Writing , so that
we have
This yields a new relation of the form
(9) 
where . Differentiating this relation with respect to yields
Now we evaluate this relation at and compute the valuations of both sides. This yields
Since , we deduce , whence . Since the reduction of with respect to vanishes and for all , we have and . Evaluating (9) at , we conclude that and therefore .
We say that is effective if its elements can be represented effectively and if all field operations can be carried out by algorithms. We call an effective diophantine field if all positive integer roots of polynomials over can be determined by an algorithm. In particular, this means that has an effective zero test, i.e. there exists an algorithm which takes an element of on input and which returns true if and false otherwise.
A power series is said to be computable, if there exists an algorithm for computing as a function of . The power series domain is said to be effective, if its elements are all effective power series and if the difference algebra operations can be carried out by algorithms. We notice that the difference algebra of all computable series is effective, although it does not have an effective zero test.
Assume now that we are given an effective power series domain with an effective zero test over an effective diophantine field . Assume also that we are given an effective algebraic power series and an annihilator for . Assume finally that the annihilator is nondegenerate, that is, . In this case, , so we may compute and by expanding the power series coefficients of . In other words, the bound (4) from Proposition 3 provides us with an effective upper bound for . Proposition 4 also yields an upper bound for .
Given difference polynomials , we will now give an algorithm ZeroTest for testing whether simultaneously vanish at . In particular, this will show that the algebra is again an effective power series domain.
Algorithm ZeroTest
1  If , then return 
2  Let be an autoreduced chain consisting of elements of minimal Ritt rank in , and take this chain to be of maximal length 
3  For and : 
4 

5  If , then 
6  If , then return 
7  Expand until a nonzero coefficient is found 
8  If this coefficient comes from one of the , then return 
9  For : 
10  If , then return 
11  For : 
12  If , then return 
13  Let 
14  Let , where 
15  Return the result of the test 
Remark
Proof. Let us first prove that the algorithm always terminates. To each input , we assign the tuple with the Ritt ranks of . We order such tuples lexicographically, and this ordering is wellfounded. Then the assigned tuple strictly decreases for this ordering during any recursive call. This shows that our algorithm always terminates.
In step 1, note that we assumed that as an element of for all . So if , then we indeed have . The correctness of the algorithm is also clear if we return during one of the steps 6, 8, 10, or 12.
Assume now that we reach step 15. By construction, this means that for every and for every . Furthermore, since we passed step 11, the chain is both coherent and autoreduced.
Applying Proposition 5, we obtain a unique logarithmic power series with and . Since , Proposition 6 implies that . Since each of is reducible to zero with respect to and none of the initials of vanishes at , we deduce that . Proposition 4 applied to and its roots and implies that whenever the test succeeds, so the returned result is correct.
Remark
Consider Stirling's series
Rewritten in terms of , the rightmost series satisfies
where . The coefficients of this difference equation belong to
where we note that is transcendental over . In particular, comes with a natural zero test and our algorithm yields a zero test for .
One can perform the same computations for functions of the form . Having a zero test for expressions involving the corresponding Stirling series can be used to prove identities for the gamma function, for example, to formally establish the Legendre duplication formula:
(10) 
In order to do this, we inductively construct a zero test for the ring
and then test whether the following expression is zero:
Our implementation allows to do this; the details can be found in the notebook https://github.com/pogudingleb/DifferenceZeroTest/blob/main/examples/LegendreDuplication.ipynb.
Note that, althought the identity (10) can be proved for integer values of using the algorithms for Precursive sequences, we are not aware of an existing symbolic computation algorithm that could be used to verify this identity automatically.
The example from the previous subsection required the incorporation of logarithms in our base ring . Such logarithms are usually construed as solutions to differential equations. In fact, it is possible to alternate the adjunction of solutions to differential equations to our base ring with the adjunction solutions to difference equations, while preserving our ability to do zero testing. Let us briefly explain how this works.
Assume that is an effective power series domain that is closed under both and differentiation . Given a algebraic power series over , we have seen that is an effective power series domain that is closed under . Moreover, there is a polynomial with . Differentiating this equation, we get
so is algebraic over . Consequently, is an effective power series domain that is closed under . By induction, we obtain a sequence of effective power series domains with and such that each is closed under . We conclude that is an effective power series domain that is closed under both and .
In a similar way, given a dalgebraic power series over , and in view of the algorithm from [4], we may construct a sequence of effective power series domains that are closed under , with and . Then is an effective power series domain that is closed both under and .
The Barnes Gfunction is a solution of the difference equation
and the loggamma integral is defined by
These functions are related via
In view of subsection 6.2, such relations can be proved automatically using our algorithm in combination with the zero test from [4]. Alternatively, we may derive a difference equation for :
After rewriting and in terms of , we may then directly use our new algorithm. Our implementation allows to do this; the details can be found in the notebook https://github.com/pogudingleb/DifferenceZeroTest/blob/main/examples/LoggammaIntegral.ipynb.
The authors would like to thank the referees for helpful comments and suggestions. Gleb Pogudin was partially supported NSF grants DMS1853482, DMS1760448, DMS1853650, CCF1564132, and CCF1563942 and by the Paris IledeFrance region.
J. Della Dora, C. Dicrescenzo, and D. Duval. A new method for computing in algebraic number fields. In G. Goos and J. Hartmanis, editors, Eurocal'85 (2), volume 174 of Lect. Notes in Comp. Science, pages 321–326. Springer, 1985.
J. Denef and L. Lipshitz. Power series solutions of algebraic differential equations. Math. Ann., 267:213–238, 1984.
J. Denef and L. Lipshitz. Decision problems for differential equations. The Journ. of Symb. Logic, 54(3):941–950, 1989.
J. van der Hoeven. A new zerotest for formal power series. In Teo Mora, editor, Proc. ISSAC '02, pages 117–122. Lille, France, July 2002.
J. van der Hoeven. Relax, but don't be too lazy. JSC, 34:479–542, 2002.
J. van der Hoeven. Computing with Dalgebraic power series. AAECC, 30(1):17–49, 2019.
J. van der Hoeven. The Jolly Writer. Your Guide to GNU TeXmacs. Scypress, 2020.
Manuel Kauers. An algorithm for deciding zeroequivalence of nested polynomially recurrent sequences. ACM Transactions on Algorithms, 2007.
A. PéladanGerma. Tests effectifs de nullité dans des extensions d'anneaux différentiels. PhD thesis, Gage, École Polytechnique, Palaiseau, France, 1997.
R. H. Risch. Algebraic properties of elementary functions in analysis. Amer. Journ. of Math., 4(101):743–759, 1975.
J. Shackell. A differentialequations approach to functional equivalence. In Proc. ISSAC '89, pages 7–10. Portland, Oregon, A.C.M., New York, 1989. ACM Press.
D. Zeilberger. A holonomic systems approach to special functions identities. Journal of Comp. and Appl. Math., 32:321–368, 1990.