1 Introduction
The main contribution of this paper is an algorithm for computing semiFourier sequences for expressions constructed from arithmetic operations, exponentiations and integrations. The semiFourier sequence is a relaxed version of Fourier sequence for polynomials (expressions made of additions and multiplications). Below we elaborate on the above statements.
Fourier sequence of polynomials is a finite sequence of successive differentiation. As an example, consider
Then the Fourier sequence of is given by
It has an obvious but important property: the successive differentiation eventually leads to a constant. It also has another nice property due to BudanFourier [1, 2]: Let denote the number of sign changes in the sequence (with zeros ignored). Then the number of roots of in , counted with multiplicities, is equal to , where is a nonnegative integer.
One naturally wonders whether one can do the same for nonpolynomials. Consider
Let us compute the successive differentiation as we did above. We obtain
Note that the successive differentiation will not lead to a constant. Thus Fourier sequence for does not exist.
In [5, 6], Strzeboński (one of the coauthors of this paper) relaxed the notion of Fourier sequence to “semi”Fourier sequence. For the above example, a semiFourier sequence is given by
Note that before/after each differentiation one is allowed to multiply by another expression, , which is nonzero for all values of in the domain of . Of course when we require that , then it is a Fourier sequence. By allowing to be other than , one obtains a relaxed version of Fourier sequence. Since is nonzero for all real values of , the semiFourier sequence still preserves the BudanFourier’s property mentioned above (Theorem 2.4 in [5]).
Strzeboński also proved constructively that a semiFourier sequence exists for expressions constructed from arithmetic operations, exponentiations, logarithms and arctangents, by providing an algorithm for computing such a sequence.^{1}^{1}1The definition of a semiFourier sequence in this paper is a bit stricter than the definition used in [5, 6], however the semiFourier sequences constructed in [5, 6] satisfy the stricter requirements.
One again naturally wonders whether semiFourier sequences exist for even larger class of functions and whether one can find them algorithmically. One natural class to consider is the set (called ExpInt) of expressions constructed from arithmetic operations, exponentiations and integrations (). It is easy to see that logarithms and arctangents belong to ExpInt, since they are integrals of and . However there are many expressions in ExpInt that cannot be expressed in terms of arithmetic operations, exponentiation, logarithms and arctangents, such as
Many elementary and special functions can be represented as ExpInt expressions, such as rational functions, exponential functions, logarithm, radicals (), inverse trigonometric functions (), (inverse) hyperbolic trigonometric functions (), hyperbolic sine/cosine integrals
, logistic sigmoid function (
), error function (), logarithmic integral function (), exponential integral function (), polylogarithm function (), Spence function (), Gudermannian function (), Dawson function (), Kummer function (), Incomplete beta function (), Incomplete gamma function (), Incomplete elliptic integral (), etc.The main contribution of this paper is to prove constructively that there exists a semiFourier sequence for every ExpInt expression, by providing an algorithm for computing such a sequence. For a semiFourier sequence computed by the algorithm for the above , see Example 2.
Of course, the main task of such an algorithm is figuring out ’s at each step, so that the sequence eventually terminates. It was quite challenging because most choices of ’s lead to infinite sequences and because, at each step, it was by no means obvious to predict which ’s would be the lucky ones. We overcame the challenge by defining a partial ordering (ranking) on expressions, and ensuring that the rank decreases.
One again wonders whether there is even larger class of functions for which semiFourier sequences exist. It is easy to see that semiFourier sequences exist for any real analytic function with finitely many roots, since one can take to be a polynomial which has the same roots as with the same multiplicities. However, in general cannot be constructed algorithmically, since we cannot compute the roots of (in fact, the original reason for introducing semiFourier sequences was to be able to isolate roots algorithmically). Finding a larger class of functions for which semiFourier sequences exist and can be found algorithmically is an open problem which we leave for future work.
There are several closely related works. As mentioned above, in [5, 6], Strzeboński, one of the authors of the present paper, introduced the notions, and algorithms for semiFourier sequence for exponential  logarithmic  arctan expressions and showed that the sequences have the BudanFourier property. This present paper gives an algorithm for larger class of expressions. By construction, it is immediate that the output sequences have the BudanFourier property. In [5, 6], Strzeboński also gave real root isolation algorithms. However, in the present paper, we do not do so, mainly because such real root isolation algorithm would require zerotesting which is nontrivial for ExpInt and interesting on its own, deserving a separate paper. Hence we leave it for the future research.
In [4], Richardson gave an algorithm for recognizing zeros among exponentiallogarithmic expressions. For this, he generates certain sequences of expressions. They are similar but not the same as a semiFourier sequence. Thus they do not have the BudanFourier property either. This present paper deals with larger family of expressions and the results have the BudanFourier property.
In [3], Kovanskii studied zeros of Pfaffian functions. It involves sequence of functions defined by certain differential equations. The sequence is not semiFourier in general. As the result, it does not have the BudanFourier property. The present paper deals with smaller family of expressions. However, it generates semiFourier sequence with the BudanFourier property.
2 Problem
In this section, we state the main problem precisely. For this, we need several notions.
Definition 1 (ExpInt expression).
An expint expression is an expression constructed with the variable symbol , rational numbers, the binary operator symbols and and the unary operator symbols , , and . The set of all expint expressions is denoted by .
Of course, the symbols , and stand for inverse, exponential and integration (antiderivative) respectively. As usual, for convenience, we use the following usual shorthands:
Example 1.
We list several expressions that can be rewritten as ExpInt expressions.
In the above, we have used the following translations. Note that integrals may include arbitrary constants.
Definition 2 (Expression differentiation).
Expression differentiation is the operation defined recursively as follows.

,

, for ,

,

,

,

,

Remark 3.
We explicitly listed the above well known properties of differentiation, because we want to emphasize the obvious but crucial facts (that will be used later):

The derivative (the result of the differentiation) of an expint expression is itself an expint expression.

Let . If is a subexpression of , then it is a subexpression of .
Remark 4.
An expression can be naturally viewed as a partial function, after fixing the meaning of the distinct int subexpressions by choosing antiderivatives.
Notation 5.
We write iff for every choice of antiderivatives corresponding to the distinct int subexpressions in and and for every in the domain of , we have .
Definition 6 (SemiFourier sequence).
Let . A sequence of pairs of elements of is a semiFourier sequence for if


, for ,

.
Now we are ready to state the problem precisely.
Problem 1 (Main).
Devise an algorithm with the following specification.

[leftmargin=4em,style=nextline,itemsep=0.3em]
 Input:

 Output:

a semiFourier sequence of
Example 2.

[leftmargin=4em,style=nextline,itemsep=0.3em]
 Input:

 Output:

where
3 Algorithm
In this section, we describe an algorithm that solves the problem posed in the previous section.
Definition 7 (Equivalence).
Let . We say that and are equivalent, and write , if can be transformed into by applying the commutative ring properties of and . We write if is equivalent to a subexpression of .
Example 3.
Definition 8 (Extension tower).
An extension tower , where , is defined recursively as follows

,

For , , , and
where and if then and .
Note that if then , , and can be easily transformed into equivalent elements of . In the following when we write , , and for expressions we mean equivalent elements of .
Definition 9 (Rank).
The rank of an expintegrate expression is defined recursively as follows:

,

for ,

,

,

,

,

.
Algorithm 1 ().
— Main —

[leftmargin=4em,style=nextline,itemsep=0.3em]
 Input:

 Output:

a semiFourier sequence of

[leftmargin=!,labelwidth=1em]

Find a sequence of all distinct subexpressions of of the form , where , ordered by the nondecreasing value of .

Set .

Return .
Algorithm 2 ().

[leftmargin=4em,style=nextline,itemsep=0.3em]
 Input:

such that


is a sequence containing all distinct subexpressions of of the form , where , ordered by the increasing value of .

 Output:

such that

for

for

.


[leftmargin=!,labelwidth=1em]

If

For rewrite as .

For set .

Return .


If

For rewrite as , where are free of , for .

Compute .

Set .

For , set .

Return .


If

For rewrite as , where are free of , for .

Compute .

Set .

For , set .

Return .


If

For rewrite as , where and are free of , for .

Compute .

Set .

For , set .

Return .

Algorithm 3 ().

[leftmargin=4em,style=nextline,itemsep=0.3em]
 Input:

such that .
 Output:

a semiFourier sequence of such that , for .

[leftmargin=!,labelwidth=1em]

If does not contain any of ,

Set and .

For set and .

Return .


Let be maximal such that .

If , let .

Set .

Compute .

Return .


If , let .

Compute .

For , set .

For ,

Set .

For , set .

Set .


Set . While and decrement .

If , return .

Set .

Compute .

Return .


If , let .

Compute .

For , set .

For ,

Set .

For , set .


Set . While and increment .

If , return .

Set .

Compute .

Return .

Example 4.
We illustrate the algorithm by tracing it on the input from Example 2.


Calling with , we obtain

Calling with , we obtain
Example 5.
We illustrate the algorithm by tracing it on the input , which is taken from Step 3 of Example 4.
The algorithm is recursive. Hence we trace the recursive calls.
4 Proof of Correctness of Algorithm
In this section, we prove that the main algorithm is correct. We need to show the termination and the partial correctness. In the following subsections, we will show them one by one.
4.1 Termination
Since the main algorithm consists of a fixed sequence of steps, it suffices to show that the subalgorithms and terminate. The subalgorithm terminates since each recursion reduces the value of the natural number until it becomes . Hence, it remains to show that the subalgorithm terminates. For this, it is convenient to introduce an ordering over .
Definition 10 (Ordering).
Let be the function from to such that
Let be the binary relation over such that
where and . ∎
It is obvious but crucial to note that does not contain infinite descending chains. In the following we will show that when makes a recursive call, the first argument decreases with . Let be such that it contains at least one of . Let be maximal such that and let . Note

.
Note that where .
Hence where .
Thus . 
.
Note that
Comments
There are no comments yet.