1 Introduction

It is well-known that if, from the stream of positive natural numbers,

$$(1,2,3, \ldots) $$

one drops every second element, obtaining the stream of odd natural numbers,

$$(1,3,5, \ldots) $$

and finally one forms the corresponding stream of its partial sums,

$$(1, 1+3, 1+3+5, \ldots) $$

then one has obtained the stream of all the positive natural numbers squared:

$$(1,4,9, \ldots) $$

The cubes of the natural numbers can be obtained in a similar fashion, by drop** from the stream of positive natural numbers every third element, obtaining

$$(1,2,4,5,7,8, \ldots) $$

then forming the corresponding stream of partial sums:

$$(1,1+2,1+2+4, \ldots) $$

and then, as above, drop** every second element:

$$(1,7,19, \ldots) $$

and finally forming the corresponding stream of partial sums again:

$$(1, 1+7, 1+7+19, \ldots) $$

One then has obtained the stream of all positive natural numbers cubed:

$$(1,8,27, \ldots) $$

Moessner [5] described how the above procedure of repeatedly alternating a drop and a partial sum operation can be generalised to obtain the stream

$$\bigl(1^n,2^n,3^n, \ldots\bigr) $$

for any n≥1: drop every nth element and form the subsequent stream of partial sums, and then drop every (n−1)th element and form the subsequent stream of partial sums, etc. A proof of the correctness of this procedure, which is known as Moessner’s theorem, was given by Perron [8]. An alternative proof and further generalisations were provided by Paasche [7] and Salié [11]. All these proofs are based on a detailed bookkee** of the elements of all the intermediate streams, and use nested inductions, involving binomial coefficients and falling factorial numbers. More details about these classical proofs can be found in recent work [3, 4] by Hinze, in which he has given a new proof of Moessner’s theorem (and its generalisations), in a calculational style.

Here, we present another proof of Moessner’s theorem, based on coinduction. Coinduction is both a definition principle and a proof principle, and it is one of the cornerstones of the theory of coalgebra [9]. It is dual to the well-known principle of mathematical induction, which is well-suited for finite and well-founded structures, such as the natural numbers and finite lists. In contrast, coinduction can be used for reasoning about infinite structures such as the streams of natural numbers above.

Our proof has three main characteristics, in which it differs from the existing proofs mentioned above:

  1. 1.

    Our formalisation of Moessner’s procedure consists of a direct translation of the operational description of Moessner’s procedure with which we started this paper.

  2. 2.

    The construction of a suitable stream bisimulation, which as usual constitutes the heart of a proof by coinduction, fully exploits the circularity that is present in our definition of both the stream of natural numbers and the drop and sum operators.

  3. 3.

    Our proof is elementary to a degree that we expect that it can be easily automated, as is often the case with coinductive proofs.

None of these characteristics are shared by the afore-mentioned classic proofs by Perron, Paasche and Salié. And although Hinze’s proof does exploit some of the circularity involved, using corecursive definitions of the operators it uses, his formalisation is at a considerable distance from the original operational description of Moessner’s procedure. Moreover, the proof by Hinze is, to be sure, very interesting and clever but also somewhat ad hoc and relatively complex.

At the same time, the proofs by Paasche, Salié and Hinze deal with both Moessner’s original theorem and with the generalisations mentioned above. In contrast, our present proof deals with Moessner’s original procedure only. And although we conclude our paper with a formalisation of a representative example of these generalisations, finding a proof by coinduction for this representative example is left as future work.

2 Preliminaries

We define the set of all streams of natural numbers by

$$\mathbb{N}^\omega= \{ \sigma\mid \sigma: \mathbb{N}\to \mathbb{N}\} $$

We shall sometimes write such streams as

$$\sigma= \bigl(\sigma(0) , \sigma(1) , \sigma(2) , \ldots\bigr) $$

We call σ(0) the initial value of σ and we call the remainder of the stream the stream derivative of σ, denoted by

$$\sigma' = \bigl(\sigma(1) , \sigma(2) , \sigma(3) , \ldots\bigr) $$

Occasionally, we shall also use the derivative of the derivative of σ, which will be denoted by σ″. We can view streams as states of an abstract machine, for which initial value and derivative together determine the behaviour: one can think of the initial value σ(0) as an (initial) observation on σ; and when we take one single transition step in state σ, we reach the new state σ′.

Next we define various streams and stream functions by so-called stream differential equations [10]. In analogy to differential equations in classical mathematics, stream differential equations define streams by specifying their stream derivative and their initial value.

  • The stream \(\overline{n} = (n,n,n, \ldots)\), for every n∈ℕ, is given by the following stream differential equation:

    $$\overline{n}'= \overline{n} $$

    with initial value \(\overline{n}(0) = n\).

  • The element-wise sum

    $$\sigma+ \tau= \bigl(\sigma(0) + \tau(0) , \sigma(1) + \tau(1) , \sigma(2) + \tau(2), \ldots\bigr) $$

    of two streams σ,τ∈ℕω can be specified by the following stream differential equation:

    $$(\sigma+ \tau)' = \sigma' + \tau' $$

    with initial value

    $$(\sigma+ \tau) (0) = \sigma(0) + \tau(0) $$

    (We use overloading: the same symbol is used for the sum of natural numbers and the sum of streams.)

  • Using the operation of sum, we can specify the stream of the positive natural numbers nat=(1,2,3,…) by

    $$\mbox {\textsf {nat}}'= \mbox {\textsf {nat}}+ \overline {1}$$

    with initial value nat(0)=1.

  • The (element-wise) Hadamard product

    $$\sigma\odot\tau= \bigl(\sigma(0) \cdot\tau(0) , \sigma(1) \cdot \tau(1) , \sigma(2) \cdot\tau(2), \ldots\bigr) $$

    of two streams σ,τ∈ℕω satisfies

    $$(\sigma\odot\tau)' = \sigma' \odot \tau' $$

    with initial value

    $$(\sigma\odot\tau) (0) = \sigma(0) \cdot\tau(0) $$

  • The following notation will be convenient. For a stream σ and for n≥0, we define

    $$\sigma^{\langle0 \rangle} = \overline {1}\qquad \sigma^{\langle n+1 \rangle} = \sigma\odot \sigma^{ \langle n \rangle} $$

    Thus σ 〈1〉=σ, σ 〈2〉=σ⊙σ, σ 〈3〉=σ⊙σ⊙σ, and so on. Also,

    $$\mbox {\textsf {nat}}^{ \langle n \rangle} = \bigl(1^n, 2^n, 3^n, \ldots\bigr) $$

  • Scalar multiplication

    $$k\sigma= \bigl(k \cdot\sigma(0) , k \cdot\sigma(1) , k \cdot\sigma (2) , \ldots \bigr) $$

    of a stream σ∈ℕω with a natural number k∈ℕ satisfies:

    $$(k\sigma)' = k\sigma' $$

    with initial value

    $$(k\sigma) (0) = k \cdot\sigma(0) $$

  • For every σ∈ℕω, the stream

    $$\varSigma \sigma = \bigl(\sigma(0) , \sigma(0) + \sigma(1) , \sigma(0) + \sigma(1) + \sigma(2) , \ldots\bigr) $$

    of partial sums of σ is defined by the following stream differential equation:

    $$( \varSigma \sigma )' = \bigl( \varSigma \sigma' \bigr) + \overline{\sigma(0)} $$

    with initial value

    $$( \varSigma \sigma ) (0) = \sigma(0) $$

  • We define drop operators \(D_{k}^{i}\), for all k≥2 and 0≤i<k, and for all σ∈ℕω, by the following system of stream differential equations: for all k≥2 and 0≤i<k−1,

    with initial values

    The operator \(D_{k}^{i}\) repeatedly drops the i-th element of every block of k elements of the incoming stream (please note that we start counting the elements of streams with 0). For instance,

    $$D_3^1(\sigma) = \bigl(\sigma(0), \sigma(2), \sigma(3), \sigma(5), \sigma(6), \sigma(8) ,\ldots\bigr) $$

  • It will be convenient to have one function symbol for the composition of a drop operator with the operator for partial sums. Therefore we define, for all k≥2 and 0≤i<k,

    $$\varSigma_k^i = \varSigma\circ D_k^i $$

    These operators satisfy the following differential equations: for all k≥2 and 0≤i<k−1,

    with initial values

(It is straightforward to prove that all of the stream differential equations [10] mentioned above are well-defined, that is, have a unique solution.)

In our proof of Moessner’s theorem, we will use a few basic properties of the operators above, all of which are easily verified.

Proposition 2.1

For all n,m∈ℕ,

$$\overline{n+m} = \overline{n} + \overline{m} $$

For all σ,τ,ρ∈ℕω,

We use stream differential equations not only because they offer a very succinct and convenient way of specifying streams. Equally importantly, they also allow us to build stream bisimulation relations, which are defined in terms of stream derivatives and initial values. Stream bisimulations are the key ingredient of proofs by coinduction, as we will see shortly.

Definition 2.2

(stream bisimulation)

A relation R⊆ℕω×ℕω is a (stream) bisimulation if all (σ,τ)∈R satisfy the following two properties:

  1. (1)

    σ(0)=τ(0)

  2. (2)

    (σ′,τ′)∈R

Theorem 2.3

(coinduction proof principle)

For a stream bisimulation relation R⊆ℕω×ℕω and for all σ,τ∈ℕω,

$$(\sigma, \tau) \in R \Rightarrow \sigma= \tau $$

Proof

If R is a bisimulation relation, then one proves σ(n)=τ(n), for all σ,τ∈ℕω with (σ,τ)∈R, by induction on n∈ℕ. □

Example 2.4

We illustrate the use of the coinduction proof principle with a simple example. The shuffle product [1, 10] of two streams σ and τ can be defined, using binomial coefficients, by

$$(\sigma\otimes\tau) (n) = \sum_{k=0}^n \binom{n}{k} \cdot\sigma (k) \cdot\tau(n-k) $$

Alternatively and equivalently, the shuffle product can be defined by the following stream differential equation:

$$(\sigma\otimes\tau)' = \bigl(\sigma' \otimes\tau \bigr) + \bigl(\sigma\otimes\tau'\bigr) $$

with initial value

$$(\sigma\otimes\tau) (0) = \sigma(0) \cdot\tau(0) $$

An advantage of this definition is that it avoids the use of binomial coefficients. Now let us look at two basic properties of the shuffle product:

The first property is straightforward to prove. If we base a proof of the second property, associativity, on the classical definition, then we shall encounter a double summation of terms with binomial coefficients. However, if we base a proof on the stream differential equation above, then our reasoning is pleasantly free of binomial coefficients. To this end, we define R⊆ℕω×ℕω to be the smallest set such that

  1. (i)

    for all σ, τ and ρ in ℕω,

    $$\bigl( (\sigma\otimes\tau)\otimes\rho, \sigma \otimes( \tau \otimes\rho) \bigr) \in R $$
  2. (ii)

    for all (σ 1,σ 2)∈R and (τ 1,τ 2)∈R,

    $$( \sigma_1 + \tau_1 , \sigma_2 + \tau_2 ) \in R $$

It is easy to prove that R is a bisimulation relation. The associativity of the shuffle product now follows by the coinduction proof principle, Theorem 2.3.

The example above will not play a role in the rest of this paper, apart from the last part of Sect. 7, where we discuss future research.

3 Moessner’s theorem

Using the definitions from Sect. 2, we shall now formalise Moessner’s construction, which we shall start not with the stream of natural numbers but with the constant stream \(\overline {1}= (1,1,1, \ldots)\). This formulation is equivalent to the description given in the introduction because, as we shall see, \(\varSigma \overline {1}= \mbox {\textsf {nat}}\) whence \(\varSigma^{n}_{n+1} \overline {1}= \mbox {\textsf {nat}}\), for all n≥1.

Theorem 3.1

(Moessner’s theorem)

For all n≥1,

$$\varSigma^1_2 \varSigma^2_3 \cdots \varSigma^n_{n+1} \overline {1}= \mbox {\textsf {nat}}^{ \langle n \rangle} $$

We note that the above formula is a direct translation of the operational description of Moessner’s procedure, given in the introduction.

4 The proof: warming up

We shall first prove Moessner’s theorem for n=1 and n=2. The proofs will be by coinduction and consist of the construction of a stream bisimulation relation. After that, it will be easy to define one (big) bisimulation relation for Moessner’s theorem in its full generality, for all n≥1 at the same time.

4.1 Moessner theorem for n=1

In order to prove

$$\varSigma^1_2 \overline {1}= \mbox {\textsf {nat}}$$

by coinduction, a first naive attempt at the definition of a suitable stream bisimulation R⊆ℕω×ℕω is to put

$$R = \bigl\{ \bigl( \varSigma^1_2 \overline {1}, \mbox {\textsf {nat}}\bigr) \bigr \} $$

In order to check whether R is a stream bisimulation relation, we compute initial values on the left and the right, which are equal to 1. Thus R satisfies stream bisimulation property (1), of Definition 2.2. Computing stream derivatives gives

$$\bigl(\varSigma^1_2 \overline {1}\,\bigr)' = \varSigma^0_2 \overline {1}+ \overline {1}$$

and

$$\mbox {\textsf {nat}}'= \mbox {\textsf {nat}}+ \overline {1}$$

We see that R is not closed under stream derivatives, and so does not satisfy stream bisimulation property (2). In order to ensure that R will be closed under stream derivatives, our second attempt at defining R is now as follows: let R⊆ℕω×ℕω be the smallest set satisfying

  1. (i)

    \(( \varSigma^{1}_{2} \overline {1}, \mbox {\textsf {nat}}) \in R \)

  2. (ii)

    \(( \varSigma^{0}_{2} \overline {1}, \mbox {\textsf {nat}}) \in R \)

  3. (iii)

    for all σ∈ℕω, (σ,σ)∈R

  4. (iv)

    for all (σ 1,τ 1)∈R and (σ 2,τ 2)∈R,

    $$(\sigma_1 + \sigma_2 , \tau_1 + \tau_2 ) \in R $$

We note that we have ensured that

$$\bigl( \bigl(\varSigma^1_2 \overline {1}\,\bigr)' , \mbox {\textsf {nat}}' \bigr) = \bigl( \varSigma^0_2 \overline {1}+ \overline {1}, \mbox {\textsf {nat}}+ \overline {1}\,\bigr) \in R $$

by clauses (ii), (iii) and (iv). Similarly, also

$$\bigl( \bigl(\varSigma^0_2 \overline {1}\,\bigr)' , \mbox {\textsf {nat}}' \bigr) = \bigl( \varSigma^0_2 \overline {1}+ \overline {1}, \mbox {\textsf {nat}}+ \overline {1}\,\bigr) \in R $$

It follows that our new R is indeed closed under derivatives. Also, one easily checks that initial values left and right are equal, for all pairs in R. Thus R is a stream bisimulation. It follows, by coinduction Theorem 2.3, that \(\varSigma^{1}_{2} \overline {1}= \mbox {\textsf {nat}}\).

4.2 Moessner theorem for n=2

For a proof by coinduction of

$$\varSigma^1_2 \varSigma^2_3 \overline {1}= \mbox {\textsf {nat}}^{ \langle2 \rangle} $$

we will define a relation R⊆ℕω×ℕω such that

$$\bigl( \varSigma^1_2 \varSigma^2_3 \overline {1}, \mbox {\textsf {nat}}^{ \langle2 \rangle } \bigr) \in R $$

and such that R is a stream bisimulation. As before, we investigate stream derivatives left and right and compute

(using Proposition 2.1 for the last equality). Also,

We make a (mental) note to include the following three pairs in R:

$$\bigl( \varSigma^0_2 \varSigma^1_3 \overline {1}, \mbox {\textsf {nat}}\odot(\mbox {\textsf {nat}}+ \overline {1}) \bigr) , \bigl( \varSigma^0_2 \overline {1}, \mbox {\textsf {nat}}\bigr) , ( \overline {1}, \overline {1}) \in R $$

We recognize the latter two pairs from the proof of Moessner’s theorem for the case n=1, and we continue with the computation of the stream derivatives of the streams in the first pair. Skip** a few intermediate steps, in which again some of the properties from Proposition 2.1 are used, we find:

$$\bigl( \varSigma^0_2 \varSigma^1_3 \overline {1}\,\bigr)' = \varSigma^0_2 \varSigma^1_3 \overline {1}+ \varSigma^0_2 \overline {1}+ \varSigma^0_2 \overline {1}+ \overline {1}+ \overline {1}$$

and

Based on the above analysis of (repeated) stream derivatives, we come to the following definition: let R⊆ℕω×ℕω be the smallest set satisfying

  1. (i)

    \(( \varSigma^{1}_{2} \overline {1}, \mbox {\textsf {nat}}) \in R\) and \(( \varSigma^{1}_{2} \varSigma^{2}_{3} \overline {1}, \mbox {\textsf {nat}}^{ \langle2 \rangle } ) \in R \)

  2. (ii)

    \(( \varSigma^{0}_{2} \overline {1}, \mbox {\textsf {nat}}) \in R \) and \(( \varSigma^{0}_{2} \varSigma^{1}_{3} \overline {1}, \mbox {\textsf {nat}}\odot(\mbox {\textsf {nat}}+ \overline {1}) ) \in R\)

  3. (iii)

    for all σ∈ℕω, (σ,σ)∈R

  4. (iv)

    for all (σ 1,τ 1)∈R and (σ 2,τ 2)∈R, (σ 1+σ 2,τ 1+τ 2)∈R

One easily verifies that R is a stream bisimulation relation. It follows, by coinduction Theorem 2.3, that \(\varSigma^{1}_{2} \overline {1}= \mbox {\textsf {nat}}\) and that \(\varSigma^{1}_{2} \varSigma^{2}_{3} \overline {1}= \mbox {\textsf {nat}}^{ \langle2 \rangle}\). In other words, the above relation R proves Moessner’s theorem for n=1 and n=2 at the same time.

5 The proof: general case

We shall now prove Moessner’s Theorem 3.1, for all n≥1. For the proof, we define again a stream bisimulation relation, generalising the relations used previously, as follows: Let R⊆ℕω×ℕω be the smallest set satisfying

  1. (i)

    for all n≥1,

    $$\bigl( \varSigma^1_2 \varSigma^2_3 \cdots \varSigma^n_{n+1} \overline {1}, \mbox {\textsf {nat}}^{ \langle n \rangle} \bigr) \in R $$
  2. (ii)

    for all n≥1,

    $$\bigl( \varSigma^0_2 \varSigma^1_3 \cdots \varSigma^{n-1}_{n+1} \overline {1}, \mbox {\textsf {nat}}\odot(\mbox {\textsf {nat}}+ \overline {1})^{ \langle n-1 \rangle} \bigr) \in R $$
  3. (iii)

    for all σ∈ℕω,

    $$(\sigma, \sigma) \in R $$
  4. (iv)

    for all (σ 1,τ 1)∈R and (σ 2,τ 2)∈R,

    $$(\sigma_1 + \sigma_2 , \tau_1 + \tau_2 ) \in R $$

Next we will prove that R is a stream bisimulation. Moessner’s theorem then follows by coinduction, Theorem 2.3.

In order to prove that the relation R is a bisimulation, we shall use the following facts.

Proposition 5.1

For all n≥1,

$$\mbox {\textsf {nat}}^{ \langle n \rangle}(0) = 1 $$

and

Proposition 5.2

For all k,n≥1,

$$\bigl( \varSigma^1_{k+1} \varSigma^2_{k+2} \cdots \varSigma^n_{k+n} \overline {1}\, \bigr) (0) = 1 $$

and

Proposition 5.3

For all n≥1,

$$\bigl( \mbox {\textsf {nat}}\odot(\mbox {\textsf {nat}}+ \overline {1})^{ \langle n-1 \rangle} \bigr) (0) = 2^{n-1} $$

and

where, for 0≤i≤n−1,

Proposition 5.4

For all k,n≥1,

$$\bigl( \varSigma^0_{k+1} \varSigma^1_{k+2} \cdots \varSigma^{n-1}_{k+n} \overline {1}\, \bigr) (0) = 2^{n-1} $$

and

with the a i ’s as above, in Proposition 5.3.

The proofs of Propositions 5.1, 5.2 and 5.3 are straightforward. The proof of Proposition 5.4 is by induction on n. In the induction step, one uses the following property of binomial coefficients: for all n≥1 and 0≤i≤n−1,

$$a_i^{n-1} = a_i^{n-2} + a_{i-1}^{n-3} + \cdots+ a_0^{n-1-i} $$

Furthermore, one uses at various places the elementary properties of Proposition 2.1.

Using these four propositions, one can easily show that the relation R, defined at the beginning of this section, is a stream bisimulation relation. Moessner’s theorem, now for all n≥1, follows as before by coinduction.

6 Stream calculus

The coinductive proof of the previous section is what we see as the main contribution of this paper. In the present section, we want to give yet another proof of Moessner’s theorem, which can be viewed as an equational version of the proof by coinduction: by using a bit of elementary stream calculus [10], of which we shall briefly recall the basics below, we can find closed expressions for each of the streams in Moessner’s theorem. The theorem is then proved by showing that these expressions are equal.

We define the set of all streams of real numbers by

$$\mathbb{R}^\omega= \{ \sigma\mid \sigma: \mathbb{N}\to \mathbb{R}\} $$

For r∈ℝ, we define the constant stream

$$[r] = (r,0,0,0, \ldots) $$

An important constant stream is defined by

$$X= (0,1,0,0,0, \ldots) $$

Its relevance will become clear below, once we will have introduced the stream operator of convolution product.

The operation of sum is given, as before, by

$$(\sigma+ \tau) (n) = \sigma(n) + \tau(n) $$

for σ,τ∈ℝω and n≥0.

We shall also need yet another type of product, called the (convolution) product:

$$(\sigma\times\tau) (n) = \sum_{k=0}^{n} \sigma(k) \cdot\tau(n-k) $$

The convolution product is different from the Hadamard product, introduced in Sect. 2, because it is not pointwise but convolving. Because the definition of convolution does not involve binomial coefficients, it is also different from the shuffle product.

We note that, for any r∈ℝ and any stream σ,

$$[r] \times\sigma= \bigl( r \cdot\sigma(0), r \cdot\sigma(1), r \cdot\sigma(2), \ldots\bigr) $$

Since the latter is equal to, or rather, extends the scalar multiplication introduced in Sect. 2 to streams of real numbers, the following shorthand is justified:

$$[r] \times\sigma= r \sigma $$

Also the following notation will be convenient: for streams σ and n≥0, we define

$$\sigma^0 = [1]\qquad \sigma^{n+1} = \sigma\times \sigma^n $$

We note that σ 1=σ, σ 2=σ×σ, σ 3=σ×σ×σ, and so on. (Please note the difference between these powers of the convolution product, on the one hand, and the powers of the Hadamard product, on the other hand. The Hadamard powers were defined previously by \(\sigma^{ \langle0 \rangle} = \overline {1}= (1,1,1, \ldots)\) and σ 〈n+1〉=σ⊙σ 〈n〉.)

We continue with our summary of stream calculus. Every stream σ with σ(0)≠0 has an inverse in ℝω with respect to convolution product. This multiplicative inverse is denoted by σ −1. It is unique and satisfies

$$\sigma^{-1} \times\sigma= [1] $$

As usual, we shall often write 1/σ for σ −1 and σ/τ for σ×τ −1.

The relevance of the constant stream X lies in the following property: for all σ∈ℝω,

$$X \times\sigma= \bigl(0, \sigma(0), \sigma(1), \sigma(2), \ldots\bigr) $$

For instance, taking σ=X yields

and so on.

The streams above allow us to introduce the following notions. We call a stream π∈ℝω polynomial if there are k≥0 and a i ∈ℝ such that

A stream ρ∈ℝω is rational if it is the quotient ρ=σ/τ of two polynomial streams σ and τ with τ(0)≠0. For instance, the following streams are rational:

$$\frac{[1]}{[1]-2X} = \bigl(2^0,2^1,2^2,2^3, \ldots\bigr) $$
$$\frac{X}{([1]-X)^2} = (0,1,2,3, \ldots) $$

One can compute a stream from its initial value and derivative by the so-called fundamental theorem of stream calculus [10]: for all σ∈ℝω,

$$\sigma = \bigl[\sigma(0)\bigr] + \bigl(X \times\sigma'\bigr) $$

The fundamental theorem of stream calculus allows us to solve stream differential equations. For a trivial example, take

$$\sigma(0) = 1 \qquad\sigma'= \sigma $$

By the fundamental theorem, we have

Using σ=[1]×σ, this yields the following solution

$$\sigma= \frac{[1]}{[1]-X} $$

(which happens to be equal to the stream \(\overline {1}\)).

In the remainder of this section, we shall apply the stream calculus above for yet another proof of Moessner’s theorem. More specifically, we shall prove that both streams on the left-hand side and the right-hand side of Moessner’s identity are rational, using the fundamental theorem together with the propositions from Sect. 5. Then Moessner’s follows simply from the observation that these rational streams are equal.

6.1 A rational expression for \(\varSigma^{1}_{2} \varSigma^{2}_{3} \cdots \varSigma^{n}_{n+1} \overline {1}\)

For notational convenience, we introduce the following constants:

for all n≥1. For the numbers P n , we have

And for the numbers Q n , we have

where the coefficients \(a_{i}^{j}\) are defined as in Proposition 5.3. As a consequence, we obtain the following recurrence relation for Q n :

This recurrence together with the above formula for P n allows us to compute a closed rational expression for (both Q n and) P n , yielding the following formulae, for the first few values of n:

(A general formula for P n , for arbitrary n≥1, will be discussed below.)

6.2 A rational expression for nat 〈n〉

In a similar fashion, we are able to compute rational expressions for all the (Hadamard) powers of nat. We compute as follows:

From this formula, the following recurrence relation is easily derived:

where we have replaced \(\overline {1}\) by nat 〈0〉. It leads to the following rational expressions, again for the first few values of n

6.3 Yet another proof of Moessner’s theorem

Because the rational expressions for P 1, P 2, etc. are equal to those for nat 〈1〉, nat 〈2〉, etc., we have proved Moessner’s theorem again, for each of these cases. For a general proof, for all n≥1 at the same time, we have to determine a general expression for arbitrary n, for both P n and nat 〈n〉. To this end, we use the fact that there exists a generating function for the n-powers of the natural numbers [2, 12]. Such generating functions can be (almost literally) translated into an expression in stream calculus: for all n≥1:

$$ P_n = \sum _{m=0}^{n-1} A(n,m) \frac{X^m}{([1]-X)^{n+1}} = \mbox {\textsf {nat}}^{ \langle n \rangle} $$
(1)

where A(n,m) are the so-called Eulerian numbers, which are defined, for every n≥1 and 0≤m≤n−1, by the following recurrence relation:

Identity (1) above constitutes yet another proof of Moessner’s theorem.

7 Discussion

Here are what we see as the main constituents of our coinductive proof of Moessner’s theorem.

  • Streams are viewed as single entities.

  • The coinduction proof principle, Theorem 2.3, says that in order to prove that two streams are the same, it suffices to show that they behave the same (since two streams have the same behaviour if they are related by a bisimulation). For streams, in other words,

    being is doing

  • Showing that two streams behave the same (and hence are equal) is particularly easy when their behaviour is circular. Circularity makes it possible to construct finite or (using induction) finitary bisimulation relations.

  • For the proof of Moessner’s theorem, the circularity involved is expressed by the stream differential equations for the operations of partial summation and drop**, on the one hand, and the stream of natural numbers, on the other hand. To illustrate this circularity for the natural numbers, we recall that

    $$\mbox {\textsf {nat}}'= \mbox {\textsf {nat}}+ \overline {1}$$

    Here we have circular behaviour in that after one transition step of nat, we obtain a new state nat′ that contains nat again as a summand.

  • We arrived at the definition of the bisimulation relation R used in the proof of Moessner’s theorem in a fairly standard way. First we constructed R for the cases of n equal to 1 (Sect. 4.1) and 2 (Sect. 4.2). For each of these cases, we included first the pair of streams that we wanted to prove equal (clause (i) of the definition of R). Then we computed their derivatives and observed that they consist of sums of the streams we started out with together with some new streams. The latter were added as new pairs, in clause (ii). Closing R under sums, in clause (iii) and including the identity relation, in clause (iv), then was sufficient to prove that R is a bisimulation. Having gone through this process for the first few values of n, the general definition of R emerged (Sect. 5).

Our coinductive proof of Moessner’s theorem, based on the construction of a bisimulation relation, is closely related to our second proof, based on rational expressions. For the definition of the bisimulation relation, we had to analyse the initial values and derivatives of P n and nat 〈n〉, which resulted in the propositions of Sect. 5. Similarly, the recurrence relations that led to the rational expressions for P n and nat 〈n〉 are based on these same propositions.

We see two main subjects for future research:

  1. (1)

    We want to analyse the precise relationships between our present two proofs, on the one hand, and the proofs by Perron [8], Paasche [7] and Salié [11], and by Hinze [3], on the other hand. Such an analysis will be more difficult than one might expect, since our coinductive proof exploits another type of circularity (of the natural numbers, of the various stream operators) than any of the other proofs. This difference makes a direct comparison rather difficult. Also, our formalisation, that is, our mathematical formulation of Moessner’s theorem is different from any of the other proofs: ours is an almost literal translation of the operational description of Moessner’s procedure.

  2. (2)

    We want to try and apply our coinductive proof method to the following generalisation of Moessner’s theorem [3, 7, 11]. A first contribution to a coinductive proof of this generalisation is already contained in our formulation of it here: we present its ingredients in terms of again a stream differential equation, using the following slightly adapted version of the drop operator: for all σ∈ℕω and all k≥2 and 0≤i<k, we define

    The difference between this definition and the one in Sect. 2 lies in the value of \(( D_{k}^{0} \sigma )'\), which changes the cycle of the drop operator from k to k+1. Using this new definition, we define an operation M on streams σ∈ℕω of natural numbers by the following stream differential equation:

    $$M(\sigma) (0) = \sigma(0)\qquad \bigl(M(\sigma)\bigr)' = M\bigl( \varSigma\circ D^1_2 \bigl(\sigma' \bigr) \bigr) $$

    The question with which we want to conclude the present paper is: to give a coinductive proof of the fact that

    $$M(\overline {1}) = (0!,1!,2!, \ldots) $$

    The fact that we are able to formalise also this generalised version of Moessner’s theorem can be considered in itself already as a contribution. In order to be able to come up with a coinductive proof, we will have to understand better which type of circularity is underlying the stream of factorial numbers. The following characterisation [10] might turn out to be useful:

    $$(0!,1!,2!, \ldots) = \bigl([1]-X\bigr)^{-\underline{1}} $$

    where the operator of (underlined) inverse is with respect to the shuffle product, introduced in Example 2.4. Shuffle inverse is formally defined by the following stream differential equation:

    $$\bigl(\sigma^{-\underline{1}}\bigr)' = -\sigma' \otimes\bigl( \sigma^{-\underline{1}} \otimes\sigma^{-\underline {1}} \bigr) $$

    with initial value

    $$\sigma^{-\underline{1}}(0) = \sigma(0)^{-1} $$