Vlad Rusu

David Nowak

Defining Corecursive Functions in Coq Using Approximations

Keywords: 2012 ACM Subject Classification Theory of computation → Functional constructs corecursive function, productiveness, approximation, Coq proof assistant

We present two methods for defining corecursive functions that go beyond what is accepted by the builtin corecursion mechanisms of the Coq proof assistant. This gain in expressiveness is obtained by using a combination of axioms from Coq's standard library that, to our best knowledge, do not introduce inconsistencies but enable reasoning in standard mathematics. Both methods view corecursive functions as limits of sequences of approximations, and both are based on a property of productiveness that, intuitively, requires that for each input, an arbitrarily close approximation of the corresponding output is eventually obtained. The first method uses Coq's builtin corecursive mechanisms in a non-standard way, while the second method uses none of the mechanisms but redefines them. Both methods are implemented in Coq and are illustrated with examples.

Introduction

Coq [START_REF]The Coq Proof Assistant[END_REF] is a proof assistant based on the Calculus of Inductive Constructions. Coinductive constructions (coinductive types, relations, and proofs, and corecursive functions) have been included in Coq's underlying theory [START_REF] Giménez | Codifying guarded definitions with recursive schemes[END_REF]. However, these constructions are limited. Corecursive functions must conform to a syntactical guardedness criterion requiring that, up to standard reductions, calls to the function under definition occur directly under constructors of the coinductive representing the codomain of the function of interest. Such functions are total and by consequence are accepted by Coq.

The guardedness criterion is best illustrated by an example. Consider the set of streams S over a set A, which, intuitively, are infinite sequences of elements of A separated by the constructor _ • _.

The head (resp. the tail) of a stream s is the first element of s (resp. the stream obtained from s by removing its first element). Consider also a predicate p on A, and the following function filter, which takes a stream s ∈ S as input and aims at producing as output a stream that contains the elements of s that satisfy p. Since its output is an (infinite) stream the function does not terminate.

filter s := if p(head s) then (head s) • (filter (tail s)) else filter (tail s)

The first self-call to filter in the function's body falls directly under a call to the constructor _ • _. It is therefore syntactically guarded by the constructor. In the second self-call, the constructor is not present; the second call is not syntactically guarded. Overall, the above function definition fails to satisfy the syntactical "guarded-by-constructors" criterion because of the second self-call.

To see why the syntactical guardedness criterion is important, consider a stream in s ∈ S such that none of its elements satisfy p. Then, filter s is not a stream -none of the elements in the input are kept in the output. The unguarded call is responsible for this. Hence, filter is not a total function from S to S , and Coq's guardedness criteria rightfully reject it because Coq only accepts total functions. However, by restricting its domain to the set S of streams s such that infinitely many elements of s satisfy p, the filter function becomes a total function from S to S . Intuitively, the guarded call, which copies an element in the input into the output, is called infinitely many times and thus produces an (infinite) stream. Such a function could, in principle, be accepted by Coq; however, Coq does not eventually produced. This condition is called productiveness, and it is the condition that our function (and, in general, corecursive functions) needs to fulfill in order to be total. We note that in the literature about corecursive functions this condition (under various formulations) is well known, to the point that it has become folklore; but, to our best knowledge, it has not yet been formalized.

What is, then, the relation between guardedness and productiveness? To see this, consider the function f ilter s := if p(head s) then (head s) • (filter (tail s)) else dummy • filter (tail s), in which the second self-call is now also guarded by the constructor _ • _ by having elements of the input that do not satisfy the predicate replaced by some dummy value in the output. The effect of this guarded definition is that for each input, the next call produces a closer approximation of the output. Since "next" is a particular case of "eventually", the overall effect of guardedness is to ensure productiveness and therefore totality, in a syntactical (thus, automatically checkable) and conservative way.

Contributions.

In this paper we propose a formal definition of productiveness that captures the corresponding intuitive notion, and two methods for defining corecursive functions in which productiveness is a key ingredient. Essentially, productiveness restricts the manner in which a sequence of approximating functions converges to the function under definition, and the two methods offer two different ways for building the sequence of approximating functions. Both methods enable the definition of corecursive functions beyond what Coq accepts by default. Both methods have been implemented in Coq and are illustrated by examples. Their additional expressiveness is obtained thanks to axioms from Coq's standard library, which, to our best knowledge, do not introduce inconsistencies. The difference between the methods lies in the amount of Coq builtin coinductive features they reuse: the first method reuses them extensively, while the second method uses none but redefines them.The Coq development is available at https://project.inria.fr/ecoop2022/.

The rest of the paper is organized as follows. A theoretical part (Sections 2-4) presents a formal notion of productiveness and our two corecursive function-definition methods in a language-agnostic manner. We emphasize that knowing Coq is not necessary for understanding the theory. Section 5 gives details of the Coq implementation that are not visible in the theory but are essential in the implementation, such as the combination of axioms imported from the standard library that enable reasoning in standard mathematics. Section 6 concludes and discusses related and future work.

V. Rusu and D. Nowak 12:3

A formal notion of productiveness

We start with some basic definitions used in the rest of the paper. Consider a set C and a partial order on C. We denote by ≺ the relation defined by t ≺ t iff t t and t t . Definition 1. A sequence (s i ) i∈N of elements of C is increasing whenever for all i ∈ N, s i s i+1 ; strictly increasing, whenever for all i ∈ N, s i ≺ s i+1 ; stabilizing to c ∈ C whenever there exist m ∈ N such that for all i ≥ m, s i = c, and stabilizing whenever it is stabilizing to some c ∈ C; ascending whenever it is increasing and non-stabilizing.

Remark. A sequence is ascending iff it is increasing and has a strictly increasing subsequence.

The following is one of the several existing definitions of a complete partial order (CPO) : Definition 2. A CPO consists of a set C, a partial order on C, and an element ⊥ ∈ C satisfying ∀t ∈ T , ⊥ t, such that that any increasing sequence of elements of T has a least upper bound.

We call the least upper bound of an increasing sequence (s n ) n∈N the limit of the sequence, hereafter denoted by lim[(s n ) n∈N ].

Example 3.

Any set A can be organized as a CPO (A ∪ {⊥ A }, A , ⊥ A ) by choosing some value ⊥ A A and by defining A as the smallest relation on A ∪ {⊥ A } satisfying ⊥ A A a for all a ∈ A and a A a for all a ∈ A ∪ {⊥ A }. The properties of orders (reflexivity, anti-symmetry, transitivity) hold trivially. Any increasing sequence (a n ) n∈N stabilizes to some a ∈ A ∪ {⊥ A }, and the limit of the sequence is the value to which the sequence stabilizes. This CPO is called the flat CPO of A.

In the rest of the paper the maximal elements of a CPO with respect to its order shall play an important role: that of "well-defined corecursive values". This view is consistently held ahead in the paper.

The following definition is our formal notion of productiveness. It restricts the manner in which a sequence of functions "converges" to a given function.

Definition 4. Given a sequence of functions ( f n ) n∈N having the same domain D and codomain C, such that the codomain is organized as a CPO (C, , ⊥), we say that the sequence ( f n ) n∈N productively converges whenever for all x ∈ D, the sequence ( f n x) n∈N is increasing and its limit lim[( f n x) n∈N ] is maximal w.r.t. the order . The limit of the sequence ( f n ) n∈N is by definition the function f : D → C such that for all x ∈ D, f x = lim[( f n x) n∈N ]. We call ( f n ) n∈N the sequence of approximating functions for the limit function f .

Remark. The image of the domain D by functions f constructed as in Definition 4 is included in the set of maximal elements of C, which, as said earlier, play the role of well-defined corecursive values. This justifies us calling "corecursive" the limits of productively converging sequences ( f n ) n∈N .

Remark. We now justify why Definition 4 captures the informal definition of productiveness. For each x ∈ D, the increasing sequence ( f n x) n∈N is either stabilizing or non-stabilizing. The values x ∈ D for which ( f n x) n∈N stabilizes are inputs on which f terminates. The values x ∈ D for which ( f n x) n∈N does not stabilize are such that the increasing sequence ( f n x) n∈N is ascending: it has a strictly increasing subsequence ( f n i x) i∈N such that for all i ∈ N, f n i x ≺ f n i+1 x, i.e., f n i x and f n i+1 x both are approximations of the sequence's limit f x, but f n i+1 x is a strictly closer approximation of f x than f n i x. Thus, ( f n x) n∈N produces, as n grows, arbitrarily close approximations of the output f x.

This captures the intuition of productiveness: the ability to eventually produce, for each input, arbitrarily close (and, in case of termination, exact) approximations of the corresponding output. The next two sections present two methods for obtaining CPOs and corecursive functions as limits of sequences of approximating functions. The first method reuses as much as possible Coq's builtin mechanisms for corecursion. The second one replaces these mechanisms by other constructions.

First method

In this approach the carrier set of the CPO being defined is the set of terms of a type coinductively defined by Coq and the limits of increasing sequences in the CPO are Coq builtin corecursive functions.

The approximating sequences for the corecursive functions under definition use a functional for the function in question. We illustrate the approach by defining the filter function on streams.

CPOs as coinductive types

Example 5. The set S of streams (a.k.a infinite lists) over a base set A ∪ {⊥ A } can be organized as a CPO as follows. First, the flat CPO (A ∪ {⊥ A }, A , ⊥ A ) is built as in Example 3. Then, the set S is defined to be the set of terms of a certain coinductive type, which, conceptually, are built by applying the following rule a countably infinite number of times : a • s ∈ S whenever a ∈ (A ∪ {⊥ A }) and s ∈ S . This simultaneously defines the constructor function _

• _ : (A ∪ {⊥ A }) × S → S .
Then, we define the constant stream ⊥ ∈ S as the stream satisfying the equation ⊥ = ⊥ A • ⊥. This is an example of a corecursive definition, which is accepted by Coq, since the occurrence of ⊥ in the right-hand side is guarded by (a direct call to) the constructor _ • _. On the set S we define the functions head and tail by head(a • s) = a and tail(a • s) = s. We also define the nth element of a stream by induction: nth 0 s = head s and nth (n + 1) s = nth n (tail s). Regarding the order relation , it is the relation on S defined "pointwise", by s 1 s 2 iff for all n ∈ N, nth n s 1 A nth n s 2 . Then, we define the limit lim[(s n ) n∈N ] of an increasing sequence of streams (s n ) n∈N by lim[(s n

) n∈N ] = (lim A [(head s n ) n∈N ]) • (lim[(tail s n ) n∈N ]
). That is, the head of the limit of a sequence of streams is the limit (in A ∪ {⊥ A }) of the heads of the streams in the sequence, and the tail of the limit is the limit (in S ) of the tails of the streams in the sequence. This is another example of a corecursive function, and one that can be defined in Coq using the tool's builtin constructions for corecursion, because in the right-hand side of lim[(s n

) n∈N ] = (lim A [(head s n ) n∈N ]) • (lim[(tail s n ) n∈N ]) the call to
lim is guarded by the constructor _ • _. In order to prove that the defined limit is indeed the least upper bound one can, e.g., reduce that property to a "pointwise" one, i.e., first proving that for all m ∈ N ,

nth m (lim[(s n ) n∈N )] = (lim A [(nth m s n ) n∈N ]
) and then using the fact that lim A computes least upper bounds in the flat CPO of A. Finally, we note that the limits of ascending sequences of streams over A ∪ {⊥ A } are streams over A (i.e., they do not contain any ⊥ A ), and are maximal with respect to .

Remark. As illustrated by the above example, the maximal elements in CPOs play the role of "well defined" corecursive values, since they do not contain ⊥ subterms, themselves interpreted as "undefined". The ascending sequences "push away" ⊥ subterms, to the effect that, in their limit, all such subterms have been eliminated. Since ⊥ is interpreted as "undefined", terms containing ⊥ are "partially defined", and "pushing ⊥ away" amounts to producing "better defined" values.

Remark. The ability to define a CPO using Coq's builtin mechanisms relies on the ability of those mechanisms to accept the definitions of limits as corecursive functions. This works for many interesting coinductive datatypes (streams, colists, possibly infinite binary trees, . . . ) but not in general.

For coinductive datatypes that are mutually dependent with inductive datatypes, the limits may require corecursive functions that contain self-calls guarded not by constructors of the coinductive datatype, but by recursive functions on the inductive datatype. Such "improperly guarded" functions are rejected by Coq. A second method presented ahead in the paper deals with such difficult cases.

12:5

Remark. The construction in Example 5 is not the only way to organize streams over a set A into a CPO. Another possibility is to define the set of streams S as the set obtained by applying the rules ⊥ ∈ S and a • s ∈ S if a ∈ A and s ∈ S for a finite or a countably infinite number of times. In this definition ⊥ is a constructor (unlike ⊥ in Example 5 where it was a defined function). The order relation and the notion of limit are also slightly different. We chose the construction in Example 5

because it has fewer technical complications: for example, the head function is total in Example 5, but partial in the alternative construction, which makes it more complicated to define. Equivalently, the function could be defined by filter := F filter where F is the pseudocode for the functional below, which takes a function as input and produces an (anonymous) function as output:

Approximating sequences using functionals

F f := λ s. if p(head s) then (head s) • ( f (tail s)) else f (tail s)
These definitions, when translated to Coq syntax, are rejected by the tool, because they fail the guardedness criterion: the call to filter in the "else" case is not guarded by the constructor _ • _.

We show below an alternative way in which a functional F can be used for uniquely defining the function, say, f , of interest, while ensuring that the fixpoint equation f = F f holds. Assume a CPO (C, , ⊥). We extend the order from C to functions D → C by f 1 f 2 iff f 1 x f 2 x for all x ∈ D.

Definition 7. A functional F : (D → C) → D → C is increasing if for all f 1 , f 2 : D → C, f 1 f 2 implies F f 1 F f 2 .
Example 8. The functional F from the previous example is increasing. Indeed, consider two functions f 1 , f 2 : D → S , with D, S as in the example in question (in particular, S is organized as a CPO as in Example 5) and assume f 1 f 2 . We have to show that F f 1 s F f 2 s for all s ∈ D. Calling productive a functional satisfying the above definition is justified by the fact that it generates a sequence of functions that productively converges. Its limit is characterized by the following theorem. We first show that f is a fixpoint of F, i.e., f = F f , which amounts to proving that for all

If p (head s) = true then F f 1 s = (head s) • f 1 (tail s) and F f 2 s = (head s) • f 2 (tail s); and F f 1 s F f 2 s because f 1 f 2 implies in particular f 1 (tail s) f 2 (tail s), and then (head s) • f 1 (tail s) (head s) • f 2 (tail s) holds thanks to the definition of . If p (head s) = false then F f 1 s = f 1 (tail s), F f 2 s = f 2 (tail s), and F f 1 s F f 2 s is just f 1 (tail s) f 2 (tail s), established above.
x ∈ D, f x = F f x. We fix an arbitrary x ∈ D. By definition of f , f x is maximal, hence, in order to prove f x = F f x it is enough to prove f x F f x. Moreover f x is the least upper bound of (F n x) n∈N , hence, in order to show that f x F f x it is enough to prove that F f x is an upper bound of the sequence (F n x) n∈N . This is proved by case analysis: For n = 0, F 0 x = ⊥ F f x, and,

for n > 0, we have that for all y ∈ D, F n-1 y f y because f y is an upper bound for the sequence (F k y) k∈N , which, since F is increasing, implies that for all y ∈ D, F (F n-1 ) y = F n y F f y.

Setting y := x in the previous relation proves that F f x is an upper bound of the sequence (F n x) n∈N also in the case n > 0, and the proof of the fact that f is a fixpoint of F is completed.

Next, we show that f is the only fixpoint of F. Assume a solution f of the fixpoint equation; we show f = f . Note that it is enough to show f f , i.e., f x f x for all x ∈ D, because from the latter by the maximality of f x we obtain f x = f x for all x ∈ D, i.e., the desired f = f . Moreover, in order to prove that f x f x for all x ∈ D, it is enough to prove that f x is an upper bound for the sequence (F n x) n∈N , because by definition f x is the least upper bound of the sequence.

Hence, what we have to prove is that for all n ∈ N, (for all x ∈ D, F n x f x), which is done by induction on n. The base case n = 0 is trivial, as it amounts to showing that for all x ∈ D, ⊥ f x.

In the inductive step, we have the inductive hypothesis that for all x ∈ D, F n x f x. By using the fact that F is increasing we obtain that for all x ∈ D ,

F n+1 x = F (F n ) x F f x = f x, which
proves the inductive step. That was what remained to prove; the proof of the theorem is complete.

The productiveness condition is more convenient to establish via the following sufficient conditions. either there exists n ∈ N such that F n x ∈ K;

or, for all n ∈ N, there exists m ∈ N with n < m such that F n x ≺ F m x.

Proof. By Definitions 4 and 9, we have to show that for all x ∈ D, the sequence (F n x) n∈N has a limit in K. We first prove that the sequence is increasing, i.e., for all n ∈ N, by induction on n. In the base case n = 0, we have, for each x ∈ D, F 0 x = x = ⊥ F 1 x, which settles this case. For the inductive step, we assume that for each x ∈ D, F n x F n+1 x and prove that, again for each x ∈ D,

F n+1 x F n+2 x. We have F n+1 x = F (F n ) x and since F is increasing, using the induction hypothesis F (F n ) x F (F n+1 ) x = F n+2
x holds for each x ∈ D, which proves the induction step and the fact that the sequence is increasing.

Hence, the sequence (F n x) n∈N has a limit; we just have to show the limit is in K.

if there exists n ∈ N such that F n x ∈ K, then, since the sequence is increasing and by definition of maximality, for all m ≥ n, F m x = F n x ∈ K; and the limit is F n x ∈ K as required.

if, for all n ∈ N, there exists m ∈ N with n < m such that F n x ≺ F m x: we first note that each F n x must be in C \ K (otherwise the hypothesis for this case is contradicted). Hence, the sequence has a strictly increasing subsequence, or, equivalently, the sequence is ascending. Since we have assumed that (C, , ⊥) is a CPO+ the limit of the sequence of interest is, again, in K.

V. Rusu and D. Nowak

12:7

Example 14. We prove using Lemma 13 that the functional F : (D → S ) → D → S for the filter function from Example 6 is productive. We have already established that it is increasing and that the CPO (S , , ⊥) is a CPO+. We prove the condition at the second item the statement of Lemma 13, i.e., for all x ∈ D and n ∈ N, there exists m ∈ N with n < m such that F n x ≺ F m x, which amounts to finding a strictly increasing sequence of natural numbers (n i ) i∈N such that F n i x ≺ F n i+1 x for all i ∈ N. This is where we use the fact that D is the set of streams x for which, given a predicate p : (A ∪ {⊥ A }) → {true, false} on the base type of S with p ⊥ A = false, it holds that p (nth n x) = true for infinitely many n ∈ N. We first prove by induction on n that F n = ffilter n where ffilter =

λn.λx.(if n = 0 then ⊥ else (if p(head x) then (head x)•(ffilter (n-1) (tail x)) else ffilter (n-1) (tail x)))
is a recursive, "finite approximation" of the corecursive filter function that we are trying to define.

Then, we notice that if p(head x) = true then ffilter (n + 1) x = (head x) • (ffilter n (tail x), and if p(head x) = false then ffilter (n + 1) x = ffilter n (tail x). That is, for the positions in the sequence x where p holds, the output of ffilter "grows", and for the positions where p does not hold, the output of ffilter stays the same. Finally, for all i ∈ N, let n i be i-th position where p holds in x; this gives us the strictly increasing sequence (n i ) i∈N such that

F n i x = ffilter n i x ≺ ffilter n i+1 x = F n i+1
x for all i ∈ N. Hence, using Lemma 13 we have established that the functional F = λ f.λ s. if p(head s) then

(head s) • ( f (tail s)) else f (tail s) is productive.
Using Theorem 10 we obtain that F has a unique fixpoint; we call filter the fixpoint in question. The fixpoint equation states that filter s = if p(head s) then (head s) • (filter (tail s)) else filter (tail s) for all x ∈ D. We note that D being the set of streams having infinitely many positions satisfying the filtering predicate is essential: outside this domain the functional F is not productive and one cannot use Theorem 10 as above to define the filter function.

Summarizing, what we have obtained in the present section is a method by which corecursive functions can be defined in Coq -details about the Coq implementation are given in Section 5even when the functions are not directly accepted by Coq because they do not satisfy Coq's builtin criteria for corecursive definitions. A function defined using our approach is abstract (it involves limits of ascending sequences in a certain CPO), but is the unique one satisfying the equation induced by its functional. We use the term "validation" for the process by which one can gain confidence that a given definition is the adequate one; one can reasonably claim that uniquely satisfying its fixpoint equation is the best validation possible for a corecursive function.

Finally, we note that from the user's point of view, by using our approach one gets the same result that one would have gotten if Coq had directly accepted the corecursive definition. Our definitions are not executable because they use axioms -i.e., the term filter s is not automatically reduced to the term if p(head s) then (head s) • (filter (tail s)) else filter (tail s) by Coq -but, in order to avoid nontermination, such reductions are not performed in Coq-builtin corecursive definitions either: one still has to prove a fixpoint equation and manually perform, e.g., rewriting with it in order to reduce it.

Second method

When the technique presented for in the previous section fails, we need to replace Coq's builtin mechanisms for coinduction, which no longer fulfill their role, by other constructions.

CPOs built by completion

The main idea is to start from the "finite subset" of the intended CPO and from an order relation on the given subset, and to "complete" them with values that are the equivalence classes of ascending

(C • , • ) is a function µ : C • → N such that for all x, y ∈ C • , x ≺ • y implies µ x < µ y.
That is, that the measure is compatible with the relation ≺ • . It is then easy to prove that a measure is also compatible with • : x • y implies µ x ≤ µ y.

Example 16. Consider the set L of finite lists over a base set A, inductively defined by the rules nil ∈ L and a • l ∈ L whenever a ∈ A and l ∈ L. Define an order on L by l 1 L l 2 iff l 1 is a prefix of l 2 .

Then, the function length mapping each list to its length is a measure on (L, L ).

Remark. For ascending sequences (s n ) n∈N , the sequence (µ s n ) n∈N is a sequence of natural numbers that tends to infinity. This is the main reason why we chose natural numbers as measure values. A common predecessor of two elements is, in our approach, an "under-approximation" of the two elements. Thus, two sequences are in the ∼ relation whenever there there is a sequence of pointwise "under-approximations" of two sequences, whose measures tend to infinity. In some sense, the pointwise "difference" between the sequences intuitively tends to "nothing" 1 . In order to show that ∼ restricted to ascending sequences is an equivalence, the following property of an order is required:

Definition 18. An order on a set A is weakly total whenever for all a ∈ A, the restriction of to the set {a ∈ A|a a} is total.

Example 19. The prefix order L on lists over a set A is weakly total: when l 1 and l 2 are both prefixes of a given list l then, if length l 1 ≤ length l 2 , l 1 L l 2 holds, otherwise, l 2 l l 1 holds. If A contains two elements a 1 a 2 , the order is not total, as [a 1 ; a 2 ] and [a 2 ; a 1 ] are incomparable.

Lemma 20. Assuming a set C • and a weakly total order • on C 12:9

Proof. Fix an arbitrary N ∈ N. Since (s n ) n∈N is ascending, there exists k ∈ N such that µ s k ≥ N.

From the hypothesis we obtain m ∈ N such that s k • s m . Let n := (max k m) and x := s k . Since the sequences are increasing, x s n , x • s n , and from µ s k ≥ N we obtain µ x ≥ N. Hence, for all

N ∈ N there are n ∈ N, x ∈ C • such that x • s n , x • s n , µ x ≥ N. By Def. 17, (s n ) n∈N ∼ (s n ) n∈N .
Remark. This definition deserves a few comments. First, K is defined as equivalence classes of ascending sequences because, on the one hand, the sequences have to be increasing because they need to have limits -as we shall see, the set K will be a set of limits -and, on the other hand, they are non-stabilizing because if one sequence were stabilizing to a value, e.g., v ∈ C • then the limit (also x, y ∈ C • and z ∈ K, which implies x • y and, given the definition of y z for x an element and z a equivalence class of ascending sequences, from the fact that any sequence in z overtakes y at some position, we obtain thanks to x • y that the sequence also overtakes x at the same position, which implies x z and settles this case;

v

3.

x ∈ C • and y, z ∈ K: then, y z implies y = z, and transitivity follows easily;

4.

x, y, z ∈ K, in which case the transitivity of follows from that of equality.

The following lemma gives a useful alternative definition for the order in a particular case.

Lemma 24. For all x ∈ C • and ascending sequences (s n ) n∈N of elements of C if the sequence stabilizes to some value v ∈ C then the proposed limit v is an upper bound for the (increasing) sequence. To show that it is the least such bound, assume another upper bound w;

) n∈N ∈ [(s n ) n∈N ] ∼ we found m ∈ N such that x • s m . But this is x [(s n ) n∈N ] ∼
then, in particular, v w because v is an element of the sequence.

if the sequence does not stabilize then it is ascending, and as already observed before, s n ∈ C • for all n ∈ N, and the proposed limit is the equivalence class [(s n ) n∈N ] ∼ .

We Example 27. Going back to the example of finite lists, their prefix order, and the measure defined by lengths of lists, the constructions in this section enable us to build a CPO of lists and streams. The streams are not defined by Coq corecursive functions (as in the earlier construction in Section 3) but by equivalence classes of ascending sequences of lists. One important difference in practice is that, unlike the approach in Section 3, the constructor _ • _ is not directly available for streams, and the functions head and tail do not have simple definitions. All three functions can be defined, and the standard relations between them can be proved, with some effort; but having them readily available as in the approach from Section 3 is preferable. We now give an example where that approach fails.

Example 28. The set T of Rose trees over a set A is coinductively definable in Coq by the rules ⊥ ∈ T and tree a l ∈ T whenever a ∈ A and l is a list over T . Note the mixture of coinduction and induction: the trees are defined coinductively, but their definition relies on inductively defined lists.

When t = tree a l we define label t = a and forest t = l; when t = ⊥ we define label t = ⊥ A (the least element in the flat CPO of A) and let forest t be the singleton [⊥ A ]. Assuming an order T on T , the limit of an increasing sequence (t n ) n∈N of Rose trees would naturally be defined as lim[(t n

) n∈N ] = ⊥ if t n = ⊥ for all n ∈ N and lim[(t n ) n∈N ] = tree (lim A [(label t n ) n∈N ]) (map lim (forest t n ) n∈N ) otherwise.
This corecursive definition of limits is not guarded by constructors, since the corecursive call to lim occurs under the map function, which is not a constructor but a defined function. Hence, the definition of limits of increasing sequences of Rose trees is rejected by Coq, and without limits there is no CPO.

Example 29. One can define and organize the set T = F ∪ R, with F the set of finite trees and R that of Rose trees, in a CPO using the approach described in this section. We first define the finite trees F over A inductively, by the rules ⊥ ∈ F and tree a l ∈ F whenever a ∈ A and l is a list over F.

The measure function is the tree's height, recursively defined by height ⊥ = 0 and height (tree a l) = 1 + max (map height l) where max computes the maximum value in a list of natural numbers. The order relation is based on the following recursive function, whose effect is to "cut" a given finite tree t at given depth n: cut = λn.λt.if n = 0 or t = ⊥ then ⊥ else tree (label t) (map (cut (n -1)) (forest t));

we then define the order relation F by t 1 F t 2 whenever t 1 = cut(height t 1 ) t 2 . The set R of Rose trees consists of equivalence classes of ascending sequences of finite trees. We have proved in Coq that all the requirements presented earlier in this section for obtaining a CPO for T = F ∪ R hold.

By contrast, a perhaps more natural definition of the "prefix order" F by t 1 F t 2 whenever t 1 = ⊥ or t 1 = tree a l 1 , t 2 = tree a l 2 , length l 1 = length l 2 and for all n < length l 1 , nth n l

Approximating sequences without functionals

In Section 3.2 the approximating sequence ( f n ) n∈N for defining a function was defined using a functional, which used functions over streams (such as the constructor _ • _) that were readily available in Coq, due to the fact that the CPO for streams had been defined as a builtin Coq coinductive type.

However, in the case of CPOs built by completion, such constructors are no longer available. One can try to replace them by defined functions, but this may turn out to be excessively difficult. For instance, in the CPO of Example 29, extending the constructor tree from finite trees F to a fully defined function tree : A → list T → T , with T = F ∪ R, is difficult: each of the trees in its second argument of type list T may be a finite tree in F or a Rose tree in R -an equivalence class of ascending sequences of elements in F. Even when all elements in the list are equivalence classes, it is not clear how the result -again, an equivalence class of ascending sequence of elements in F -can be built.

Hence, we have to make do without constructors or defined functions replacing them. This severely limits the functionals that one may write, making the functional-based definition of corecursive functions from Section 3.2 essentially useless. Example 31 below illustrates this issue. In this section we present an approach that does not require a functional, but does require a "finite version" f • of the corecursive function f under definition, which moreover has to satisfy a productiveness requirement.

: D • → C • is
productive whenever, for all increasing sequences (x n ) n∈N of elements in D • that have a limit in K D , the sequence ( f • x n ) n∈N of elements in C • is also increasing and has a limit in K C .

Remark. Definition 30 of a productive function implies the function is also increasing. It also implies that the function maps ascending sequences to ascending sequences. Calling such a function productive is justified by the fact that it generates a sequence of functions that productively converges according to Definition 4. This sequence is built as follows: for all x ∈ K D , choose an arbitrary ascending sequence (x n ) n∈N ∈ x; and set ( f n x) = ( f • x n ) for all n ∈ N. Then, ( f n ) n∈N productively converges according to Definition 4: for all x ∈ K D , ( f n x) n∈N is increasing and its limit is in K C .

Example 31. In the CPO of finite and Rose trees from Example 29, the sets C • and D • from the above definition are both the set F of finite trees. Consider the following recursive endofunction of F: mirror • = λt.if t = ⊥ then ⊥ else tree (label t)(map mirror • (rev (forest t))), where rev is the function that computes the reverse of a list. As its name indicates, the function computes the "mirror image" of finite trees. We have defined this function in Coq and have proved that it is productive according to Definition 30, using the fact that the mirror • function preserves the height of its argument.

Note how the functional for mirror • : λφ t.if t = ⊥ then ⊥ else tree (label t)(map φ (rev (forest t)))

uses the constructor tree. Writing the corresponding functional for a full mirror function for both finite and Rose trees would require a corresponding defined function tree : A → list T → T . As stated above, such a function is hard to define. Hence our alternative solution avoiding these issues.

The following theorem states that productive functions map equivalent ascending sequences in their domain to equivalent ascending sequences in their codomain. The above result enables us to define functions f : K D → C as limits of approximating sequences

( f • s n ) n∈N ∼ C ( f • s n ) n∈N .

Proof. By

( f n : K D → C) n∈N .
The definition of each of the functions f n below depends on an arbitrary choice for a representative in its argument (which is an equivalence class), however, thanks to the above theorem, the limit (i.e. the defined function f ) does not depend on that choice. The functions are built as in the Remark following Definition 30: for all x ∈ K D , choose an arbitrary ascending sequence (x n ) n∈N ∈ x;

and set (

f n x) = ( f • x n ) for all n ∈ N.
We have observed that ( f n ) n∈N productively converges according to Definition 4; its limit is [(

f • x n ) ∈N ] ∼ C ∈ K C
, which, by above theorem, is independent of the choice for (x n ) n∈N ∈ x. Hence, the limit f := λx.lim[( f n x) n∈N ] is also independent on the initial choice.

Of course, the natural question that arises regards validation: do the functions thus defined match the intention of the user? Unlike the case of functional-based corecursive functions in an earlier section, we do not have a functional and a fixpoint equation as validation mechanisms. A certain degree of confidence in the definition of f is already obtained from the (assumed) confidence in f • - is also defined, which like pos takes a position p and a tree t and navigates the tree from root to children, but unlike pos, the children are chosen "backwards" (counting back starting from the last child) instead of forwards. We have then proved that for all positions p and trees t (finite or Rose), pos p (mirror t) = pos_rev p t, meaning that, intuitively, mirror "reverses" all positions in the tree.

as we have f ([(x n ) n∈N ] ∼ D ) = [( f • x n ) n∈N ] ∼ C -
The proofs were performed by first defining finite versions pos • and pos_rev • for the new functions involved, then proving pos • p (mirror • f ) = pos_rev • p f for finite trees f , and finally proving that the corresponding property on Rose trees reduces to that on finite trees whose height is large enough (here, larger the length of the list p). The Coq proofs are available in the companion Coq development.

Implementation

The corecursive function-definition methods presented in Sections 2-4 have been implemented in the Coq proof assistant. The implementation has two motivations. The first one is ensuring that the results are sound, i.e., no case has been forgotten in a proof, and no assumption was left implicit. This is a standard motivation for using a proof assistant. The second motivation aims at providing Coq itself with stronger mechanisms for corecursive definitions than the builtin ones available in the tool.

This is achieved at the cost of assuming several axioms from Coq's standard library; we state which axioms were used, where, and for what purpose. To our best knowledge the combination of axioms we imported from the standard library does not introduce inconsistencies (cf. [START_REF] Chlipala | Certified Programming with Dependent Types[END_REF]Chapter 12]).

Understanding the rest of this section requires knowledge about Coq's inductive and coinductive types, recursive and corecursive definitions, and its module system.

Sequences

Some notions are used by both methods. The main concept is that of sequences over a given type, encoded as functions from the natural numbers to the type in question. The fact that an element belongs to a sequence (parameterized by a given type) is also defined using an existential quantifier.

Definition Seq {A:Type }: Type := nat -> A Definition sin{A:Type }(a:A)(q: Seq(A:=A)): Prop := exists i, a = q i.

Then, given a relation R (i.e., a binary predicate, of type A->A->Prop), the various kinds of sequences from Definition 1 (increasing, strictly increasing, stabilizing, ascending) are defined. Next, the fact that a value lub_val is the least upper bound (w.r.t. a relation R) of a sequence q is defined as Definition lub{A:Type} (R:A-> A-> Prop) ( lub_val : A) (q:Seq(A:=A)) := ( forall a, sin a q -> R a lub_val ) /\ ( forall lub_val ',( forall a,sin a q-> R a lub_val ')-> R lub_val lub_val ').

The definition of lub is only relevant for order relations R, and will only be used for such relations.

For the first method these definitions are enough. The second method requires the property noted in the Remark following Definition 1: if R is an order, then a sequence is ascending if and only if it is increasing and has a strictly increasing sequence. This one-line property required quite a few intermediary lemmas in order to be formally proved, using classical logic and the following axiom: This axiom, from Coq's standard library, enables one to "choose" an element P satisfying a predicate P just based on the knowledge that P is satisfiable. In informal mathematical reasoning this is often implicitly assumed. In a Coq formal development, however, it has to be explicitly assumed. Here we use it in order to turn a total relation into a function having the relation in question as its graph:

Lemma functional_choice : forall (A B:Type) (R:A->B->Prop), ( forall x:A, exists y:B, R x y)->( exists f:A->B, forall x:A, R x (f x)).

The constructive_indefinite_description axiom occurs several times in the Coq development.

Remark. We have not formalized Definition 4 of productive convergence of sequences of functions.

That definition is useful in the paper for a unified presentation of the two methods and for giving the intuitive notion of productiveness a mathematical meaning. In Coq these motivations do not apply.

First method

This method reuses Coq's builtin coinduction mechanisms for organizing coinductive types as CPOs.

Stream CPO

The Coq definition for the stream CPO closely follows the approach outlined in Example 5. First, the flat CPO over a given type A (cf. Example 3) is encoded using Coq's option type. A relation leo on this type is also defined, which we prove to be an order relation, having None as the bottom element: In Example 3, None was denoted by ⊥ A and leo was denoted by the infix symbol _ A _. Then, a lemma states that for each increasing sequence in the leo order, there exists a least upper bound:

Lemma leo_lub {A:Type} : forall (q:Seq (A:= option A)), increasing leo q-> exists b,lub leo b q.

The least upper bound of a sequence is obtained using constructive_indefinite_description:

Definition limF{A:Type }(q:Seq(A:= option A))(H: increasing leo q):= constructive_indefinite_description _ ( leo_lub q H).

Next, a stream over a type T is obtained by applying the constructor scons to an element in T and another stream over T. The stream bot, which is an infinite repetition of None, is also defined.

CoInductive Stream {T:Type} := scons : T -> Stream -> Stream .

CoFixpoint bot{T:Type }: Stream (T:=T) := scons None bot.

In Example 5 the constructor scons is denoted by an infix operation _ • _ and bot is denoted by ⊥.

The head (hd) and tail (tl) of a stream are also defined, in the expected manner.

Next comes the order relation on streams. In Example 5 the order _ _ was defined pointwise.

We here give an alternative, coinductive definition, and prove that the two definitions are equivalent. Next, the limit of an increasing sequence of streams over the flat CPO of a given set is defined by:

CoFixpoint lim{A:Type }(q:Seq(A:= Stream (T:= option A)))(H: increasing les q) := scons ( proj1_sig (limF(fun n => hd(q n))( increasing_smap_hd q H)))

(lim(fun n => tl(q n))( increasing_smap_tl q H)).

The function is parameterized by base type A of the underlying flat CPO. The type of the argument q is a sequence of streams over the flat order of A. The function takes a second argument: a proof that the sequence is increasing w.r.t. the order les of streams. The function returns a stream, built with scons, whose head is the limit (limF, in the flat CPO) of a stream that consists in mapping the head of streams to the sequence q, and whose tail is the (corecursively called) limit of the sequence of streams obtained by mapping the tail of streams to the sequence q. There are also some proof terms being used for ensuring that the various sequences whose limits are being invoked are increasing.

Finally, we prove that the proposed limit is the actual least upper bound of an increasing sequence:

Lemma lim_lub {A:Type }(q:Seq(A:= Stream (T:= option A)))(H: increasing les q): lub les (lim q H) q.

We also formalize the main artifact in the first method for corecursive function definition -Theorem 10, which says that a productive functional has a unique fixpoint. For productiveness we use the more convenient sufficient conditions given by Lemma 13. These conditions are placed in a Coq module type, which can be seen as an interface that other modules need to implement in order to benefit from the results implied by the conditions (here, the function definition method embodied in Theorem 10).

The filter function on streams

The proposed functional for the filter function for streams over a type A is written as follows: where S:= {s:Stream(T:=option A)|forall n,exists m,n<=m ∧ P(nth m q)=true} is the subtype of streams that have an infinite number of elements satisfying the filtering predicate P: option A-> bool, and head, tail are the restrictions of the hd, resp. tl functions on streams to the subtype S. We prove the conditions in Lemma 13, which enables us to use the Coq formalization of Theorem 10 and to define a function filter satisfying the two following theorems:

E
Theorem filter_fix : forall s, bisim ( filter s)( Filter ( filter s))

Theorem filter_fix_unique : forall f,( forall s,bisim (f s) ( Filter f s))-> forall s,bisim ( filter s)(f s).

The theorems state the existence and uniqueness of filter as the unique fixpoint of Filter... except for the fact that instead of the expected equality we get bisimulation, coinductively defined as follows:

CoInductive bisim{T: Type }: Stream (T:=T) -> Stream (T:=T) -> Prop := | bisim_def : forall a s1 s2 , bisim s1 s2 -> bisim(scons a s1)( scons a s2).

In the presentation of the first function-definition method from Section 3 we allowed ourselves, for simplicity of notation, to use equality instead of bisimulation. When translating informal mathematical reasoning to Coq such notation abuses and other similar approximations are revealed. Bisimulation is the natural equality between streams; by contrast, the standard equality of Coq is too strong. We note that, after having proved that bisimulation is a congruence relation, by importing a certain library (Setoid) one can perform rewriting with the fixpoint "equation" filter_fix in Coq.

Other examples

The companion Coq development also contains a definition of the stream of Fibonacci numbers, which, like the filter function is not accepted by Coq's builtin coinduction mechanisms. There is also a construction for a CPO of colists, which can be seen as the union of finite lists and streams.

Accordingly, colists have a constructor nil for the empty colist, in addition to bot and scons like in the above definition of streams. The filter function on colists, defined as the unique fixpoint of a certain functional, turns out to be quite different from the filter function of streams: it is total on the subtype of "well-formed" colists (those that do not contain bot) and uses a non-executable "oracle" to determine whether its current argument is such that none of its elements satisfy the filtering predicate.

If this is the case, the function returns nil, otherwise, it behaves like the filter function for streams.

Second method

Unlike the first method, in which each individual coinductive type has to be organized as a CPO, the second method provides a generic construction of CPOs, if some assumptions are met. Particular

CPOs can be defined as instances of the generic notions, by providing definitions and lemmas that instantiate the assumptions. Corecursive functions between CPOs can then be defined.

Generic CPO

The generic construction of CPOs requires a set Cc (C • , in Section 4.1), a least element, and an order relation ordc (for • ), which must be weakly total. There is also a measure mu (for µ) compatible with the strict order. These requirements are gathered in a Coq module type:

Parameter Cc: Type.

Parameter bot: Cc.

Parameter ordc: Cc -> Cc -> Prop.

Parameter bot_is_least : forall x,ordc bot x.

Parameter ordc_refl : forall x,ordc x x.

Parameter ordc_trans : forall x y z,ordc x y->ordc y z->ordc x z.

Parameter ordc_antisym : forall x y,ordc x y->ordc y x->x=y.

Parameter ordc_wtot : forall x y z,ordc x z->ordc y z->ordc x y\/ ordc y x.

Parameter mu: Cc -> nat.

Parameter mu_sordc : forall x y,ordc x y-> x<>y-> mu x<mu y.

The type Cc is "extended" to a type C by adding equivalence classes of ascending sequences of elements in Cc, and the order ordc is extended to a relation ord, which is then proved to be an order: Like in Definition 25, the code for lim needs to decide whether its argument s is stabilizing or not. This is not decidable, because a decision procedure would have to examine a whole infinite sequence.

We make it decidable by proving a theorem called excluded_middle_informative stating that every proposition is decidable: forall P,{P}+{∼P} -a consequence of classical logic and

Defining Corecursive Functions in Coq Using Approximations

On equivalence classes

There is no universally accepted way for expressing equivalence classes modulo a given equivalence relation in Coq. One option, supported by the tool's standard library, is to use setoids, which are a triple consisting of a type, a binary relation on the type, and a proof that the relation is an equivalence. This approach is mainly used to obtain a generalized rewriting, using the setoid's equivalence relation (which moreover needs to be proved to be a congruence for the contexts under which rewriting is desired) instead of equality. For example, rewriting using bisimulation of streams falls in this category. However, in the present context, we just need equivalence classes for their own sake. Rewriting is not an issue, and using the powerful but complicated machinery of setoids did not seem cost-effective. We therefore opted for a more direct approach that uses axioms from the standard library: constructive_indefinite_description for obtaining a representative of a class; functional extensionality (two functions are equal iff they are pointwise equal) and propositional extensionality (propositional equality coincides with equivalence) for proving that if two elements are in the equivalence relation they are in the same equivalence class. In standard mathematics these properties are implicitly assumed, but in Coq they have to be explicitly assumed since they are not provable otherwise.

The CPO of finite and Rose trees

In order to obtain this CPO the parameters of the generic CPO (the type Cc, the relation ordc, the function mu, and the various constraints relating them) have to be instantiated with actual definitions and lemmas. This essentially amounts to encoding the content of Example 29 in Coq. The hardest part was establishing that the relation ordc is transitive; several nontrivial lemmas about cutting trees at given heights had to be proved. Perhaps the most difficult part of all the development effort was to convince ourselves that weak totality of the order is a crucial requirement, and therefore to abandon the apparently natural "prefix order", also defined in Example 29, which does not have this property.

The mirror function

Defining a function using the second method is composed of a generic part, which assumes two generic CPOs and a function between their "finite parts" that has to satisfy a productiveness constraint (Definition 30). Accordingly, in Coq we write a module type where such a function and its productiveness requirement are assumed. Any module that implements that module type gains access to the corecursive function definition method described at the end of Section 4.2. A recursive fmirror function between finite trees is written in such a module, and by the generic mechanism described above, this function is transformed into a corecursive function mirror between Rose trees.

Finally, to gain confidence in the obtained definition we define functions fpos and fpos_rev (cf.

Example 33) that compute labels at given positions in finite trees; transform these functions into pos and pos_rev that do the corresponding operations on Rose trees; and prove the following lemma:

Lemma mirror_pos : forall p t, pos p ( mirror t) = pos_rev p t.

Comparison with related work

We start with classical results and with their applications for the purpose of defining functions.

Kleene's fixpoint theorem [19, Chapter 5] can be used to define functions as least fixpoints of continuous functionals over CPOs. A functional is continuous if it commutes with least upper bounds.

The least fixpoint is the least upper bound of an increasing sequence of functions, obtained by iterating the functional starting from the constant "bottom" function. This has been formalized and used for defining recursive functions in Coq [START_REF] Bertot | Fixed point semantics and partial recursion in Coq[END_REF]. Unsurprisingly, they use the same kinds of axioms as we do.

In our first method we use the same iteration as in Kleene's fixpoint theorem to obtain a fixpoint, but require productiveness instead of continuity; and we obtain a unique fixpoint, not just a least fixpoint. The stronger fixpoint result, and the fact that productiveness is a natural requirement for corecursive functions, suggest that our method is well-adapted for the purpose of defining such functions.

Our second method has similarities with the classical construction of the real numbers based on equivalence classes of Cauchy sequences of rational numbers [10, Appendix A]. However, Cauchy sequences over a base set require the base set to be organized as a metric space, with a distance function satisfying certain properties. An approach for defining corecursive functions based on Cauchy sequences is mentioned in [START_REF] Kozen | Applications of metric coinduction[END_REF]. They use another classical result (Banach's fixpoint theorem [START_REF] Banach | Sur les opérations dans les ensembles abstraits et leur applications aux équations intégrales[END_REF]) to define corecursive functions as unique fixpoints of eventually contracting functionals. By contrast, we organize the base set as a CPO, use ascending sequences instead of Cauchy sequences, and (in the second method) do not use functionals, but a "finite version" of the corecursive function under definition, which has to satisfy a certain productiveness requirement to ensure a proper definition.

We now present related work about corecursion in proof assistants and similar formalisms. In Coq, but unguarded can be transformed into an equivalent, guarded function. This has been done for the filter function on streams in [START_REF] Bertot | Filters on coinductive streams, an application to Eratosthenes' sieve[END_REF] and generalized in [START_REF] Bertot | Inductive and coinductive components of corecursive functions in Coq[END_REF] to other unguarded functions. Their idea is to use an ad-hoc predicate stating that the definition under study is, in some sense, productive. However, their approach does not use a general, formal notion of productiveness, nor does it handle the case where corecursive calls are guarded by some non-constructor function, like the mirror function for Rose trees presented in this paper. Our approach is not subject to these limitations. In other related work, a constructive version of the CPO of streams in Coq is mentioned in [START_REF] Paulin-Mohring | A constructive denotational semantics for Kahn networks in Coq[END_REF] in the context of a coinductive formalization of Kahn networks. However, the author does not use her formalization of CPO to extend the class of corecursive stream functions admissible by Coq.

We note that coinductive proofs in Coq, which by default are subject to the same syntactical requirements as corecursive functions, can be performed using more relaxed, semantical requirements by using parameterized coinduction implemented in the Paco extension of Coq [START_REF] Hur | The power of parameterization in coinductive proof[END_REF]. We have tried to adapt parameterized coinduction to corecursive function definition, but have given up because we found that it is not adaptable. Parameterized coinduction works for coinductive proofs, because, there, witness terms do not matter -any term of the right type will do. By contrast, in corecursive functions, witness terms do matter, since they expresses what the function is supposed to compute.

Agda [20] is also a dependently-typed programming language and proof assistant that offers support for corecursive function definition. In the core tool there is a guardedness checker similar to that of Coq, but more liberal as it allows, e.g., the definition of two mutually dependent functions, one of which is recursive and the other one, corecursive. This enables it to accept the definition of the mirror function on Rose trees, which Coq does not accept. Extensions to Agda with sized types [START_REF] Veltri | Guarded recursion in agda via sized types[END_REF] provide users with a uniform, automatic way of handling termination and productiveness, based on type annotations written by the user. The current implementation of sized types in Agda is unsound (cf. [20, chapter Safe Agda] and https://github.com/agda/agda/issues/2820).

Isabelle/HOL [21] is another major proof assistant which supports corecursive function definition.

A guardedness criterion (there called primitive corecursion) similar to that of Coq and Agda is implemented [START_REF] Biendarra | Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL[END_REF], based on bounded natural functors, a conservative extension of Higher Order Logic. The framework has further been extended to accept function definitions that go beyond primitive corecursion [START_REF] Blanchette | Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL[END_REF]. Isabelle/HOL now accepts function definitions where corecursive calls can be guarded by functions other than constructors, provided the functions are proved to be friendly (essentially, a friendly function needs to destruct at most one constructor of input to produce one constructor of output). Unguarded corecursive calls, such as those in the filter function on streams, are also accepted, provided they are proved to eventually produce a constructor of output. Like in our approach, all proof obligations are the responsibility of the user. They have the additional advantage of using no supplementary axioms, as those of Higher Order Logic are expressive enough.

Beyond generic proof assistants, support for corecursion also exists in tools targeting particular languages. For example, Dafny is a specification and verification language dedicated to the C# language, which has support for corecursive function definition [START_REF] K. Rustan | Co-induction simply -automatic co-inductive proofs in a program verifier[END_REF], based on a guardedness criterion similar to those existing in the already mentioned tools. Coinductive proofs are also supported.

Finally, beyond the area of formal verification, it is very worth mentioning the Haskell functional language, which offers support for corecursive function definition by means of lazy evaluation.

Future work

We have encountered corecursive functions that are productive yet do not obey the guarded-byconstructors criterion in our planned future work. The Prelude dataflow synchronous programming language [START_REF] Forget | A Synchronous Language for Critical Embedded Systems with Multiple Real-Time Constraints[END_REF] has a flow sampling construction whose semantics is best described using a filter function on colists (which we have defined in the companion Coq development as an instance of our first method). This opens the way to a mechanized semantics of Prelude in Coq, which would then enable V. Rusu and D. Nowak

12:21

program verification and semantically correct code generation for the language. While formalizing in Coq the paper [START_REF] Uustalu | The essence of dataflow programming[END_REF] about the semantics of dataflow languages we have encountered unguarded corecursive functions on streams that can also be defined using our first method. More speculative future work includes a comparison and possible cross-fertilization of our approach with the sized-type approach of Agda and the bounded-natural-functor approach of Isabelle/HOL.

Example 6 .

 6 This method assumes a functional F : (D → C) → D → C for the function of interest. The functional may be obtained, e.g., from an attempt to define the function f : D → C of interest directly in Coq, via a statement of the form f := F f . It is, of course, assumed that the attempt failed -i.e., it failed the guardedness criteria -otherwise one would just define f directly in Coq. Consider the set S of streams over A ∪ {⊥ A } as in Example 5 and assume a predicate p : A ∪ {⊥ A } → {true, false} such that p ⊥ A = false. Let D be the subset of S consisting of streams s over A, such that p (nth n s) = true for infinitely many n ∈ N. The following pseudocode statement is an attempt to define the filter function over D, which computes the substream of values satisfying p: filter s := if p(head s) then (head s) • (filter (tail s)) else filter (tail s)

Definition 9 .

 9 Assume again a CPO (C, , ⊥) and a functional F : (D → C) → D → C. Let : D → C be the constant function such that x = ⊥, for all x ∈ D, and let F n : (D → C) → D → C be the functional inductively defined by F 0 f = f and, for all n ∈ N, F n+1 f = F(F n f ). A functional F : (D → C) → D → C is productive whenever it is increasing and the sequence of functions (F n ) n∈N productively converges (cf. Definition 4).

Definition 11 .Example 12 .Lemma 13 .

 111213 A CPO (C, , ⊥) is a CPO+ if each ascending sequence has a maximal limit. Per the observation at the end of Example 5, the CPO of streams is a CPO+. Assume a CPO+ (C, , ⊥) having the set of maximal elements K ⊆ C, and a functional F : (D → C) → D → C. Then, F is productive whenever it is increasing and, for all x ∈ D:

Definition 17 .

 17 Two sequences (s n ) n∈N and (s n ) n∈N of elements of C • are in the ∼ relation whenever for all N ∈ N there exist n ∈ N and x ∈ C • such that x • s n , x • s n , and µ x ≥ N.

  ) of the sequence being also in K would imply a nonempty intersection of C • and K, which we wish to avoid. Second, the relation is an order relation (this is established by Lemma 23 below). It is a conservative extension of • , and elements in K are in the order iff they are equal. Combined with the fact that there is no situation in which x y for x ∈ K and y ∈ C • , we obtain that the elements in K are maximal w.r.t. . Like in the case of the CPO of streams in an earlier example, the maximal elements play the role of "well-defined corecursive values". Finally, the third case defining the relation requires an explanation. An element x (in C • ) is in the order with an equivalence class y of ascending sequences (in K) whenever each sequence in the class "overtakes" x at some position m ∈ N according to the base relation • . Combined with the fact that (s n ) n∈N is increasing, this implies that the sequence overtakes x for all positions n ≥ m. Several results hereafter (Lemma 24, Theorem 26, Theorem 32) critically depend on the proposed definition of the relation. Lemma 23. Assume a measure µ on (C • , • ) like in Definition 15, with • a weakly total order. Then, with C and being the completions of C • and • respectively, given in Definition 22, the relation on C is an order.Proof. Reflexivity is trivial since amounts to • on C • and to equality on K, both of which are reflexive. For anti-symmetry, we note that it reduces to the anti-symmetry of • , because the nontrivial remaining case has the form "x y and y x for x ∈ C • and y ∈ K implies x = y", which holds because its premise y x is impossible. Let us now consider transitivity, thus, x y and y z. There are only four possibilities when those relations can hold:1. x, y, z ∈ C • , in which case the transitivity of reduces to that of • ;

  by definition; which proves the lemma. Definition 25. Given a set C • and weakly total order • on C • , consider the completion of C • to C and of • to as in Definition 22. For an increasing sequence (s n ) n∈N of elements of C, we define lim[(s n ) n∈N ] as follows: if the sequence stabilizes at a value, say, v ∈ C, then lim[(s n ) n∈N ] = v; otherwise, the sequence does not stabilize, which implies that for all n ∈ N, s n ∈ C • , and we define lim[(s n ) n∈N ] = [(s n ) n∈N ] ∼ , i.e., the equivalence class of the sequence w.r.t. the relation ∼. Note that in the second case of the above definition it is essential that the ascending sequence (s n ) n∈N be composed of elements of C • because ∼ is only an equivalence for such sequences. Theorem 26. Assume a measure on (C • , • ) like in Definition 15, with • a weakly total order. Then, with C and being the completions of C • and • respectively, given in Definition 22, and with the limits of increasing sequences introduced in Definition 25, the triple (C, , ⊥) is a CPO.Proof. In order to prove the theorem we have to prove that the limits of increasing sequences proposed in Definition 25 are least upper bounds. Consider an increasing sequence (s n ) n∈N of elements of C.

Definition 30 .

 30 Assume two CPOs (D, D , ⊥ D ) and (C C , ⊥ C ) defined as in Theorem 26, thus, their base sets are decomposed as C = C • ∪ K C and D = D • ∪ K D . Then, a function f •

Theorem 32 .

 32 In the context of Definition 30, let ∼ D denote the equivalence relation on ascending sequences in the CPO (D, D , ⊥ D ) (cf. Definition 17, Lemma 20). Let ∼ C denote the corresponding equivalence in (C C , ⊥ C ). Then, for any pair of equivalent ascending sequences (s n ) n∈N ∼ D (s n ) n∈N and any productive function f • : D • → C • , we have the equivalence

  and from the independence of choice of representative from Theorem 32. The confidence can be improved by proving properties of f that the user expects.Example 33. By applying the above process to the mirror • function from Example 31, and noting that in this case K D = K C = R (the set of Rose trees), we obtain a well-defined function mirror : R → R. To increase confidence in this function we prove that the mirror function "reverses" positions in Rose trees. A position p is a finite sequence of natural numbers, and in a given tree t it indicates the label (in the set A ∪ ⊥ A , if we consider trees over A) obtained by navigating in the tree, starting from the root and choosing children indexed by the successive numbers in p. Let pos p t be the label in question (or ⊥ A , since the position may "overflow"). A function pos_rev

  Axiom constructive_indefinite_description : forall (A:Type) (P:A->Prop), ( exists x, P x) -> {x:A | P x}.

  Inductive option (A:Type ): Type := None: option A | Some: A -> option A. Inductive leo{A:Type} : option A -> option A -> Prop := | leo_none : forall a, leo None a | leo_some : forall a, leo (Some a) (Some a)

  CoInductive les{T:Type} : Stream (T:=T)-> Stream (T:=T)-> Prop := les_def : forall a b s s', leo a b-> les s s'-> les(scons a s)( scons b s ').

  in Coq Using Approximations Definition Filter (f:S-> Stream (T:= option A))(s: S): Stream (T:= option A):= if P (head s) then scons (head s) (f (tail s)) else f (tail s).

  Inductive C:Type := |elt: forall (e:Cc),C |cls: forall (ec: EqClass ),C. Inductive ord : C-> C-> Prop := | elt_elt : forall e1 e2 ,ordc e1 e2 -> ord (elt e1)( elt e2) | elt_cls : forall e ec , ( forall t, in t ec -> exists n, ordc e (nth t n) )-> ord (elt e)( cls ec) | cls_cls : forall ec ,ord (cls ec)( cls ec). More information about our encoding of equivalence classes is given at the end of this section. The type C is obtained by "wrapping" elements in Cc into a constructor elt and equivalence classes into a constructor cls. The relation ord has three cases, corresponding the three cases by which • is extended to in Definition 22. Then, the limit of an increasing sequence of elements in C is defined: Definition lim (s:Seq(T:=C))(H: increasing ord s):C := match ( excluded_middle_informative ( stabilizing s)) with | left stab => let (c, _) := constructive_indefinite_description _ stab in c |right nostab => (cls ( class_of (exist _ (fun n => extract_elt (s n)) (conj ( extract_elt_incr _ Hinc nostab ) ( incr_nostab_nostab _ Hinc nostab ))))) end.

constructive_indefinite_description.

  Applying that theorem to (stabilizing s) leads to two cases: if the sequence is stabilizing (with stab being a proof of stabilization) then the value to which it stabilizes is "fetched" by constructive_indefinite_description. If the sequence is not stabilizing (with nostab being a proof of non-stabilization) then, intuitively the equivalence class of s should be returned -except for the fact that s is a sequence over C and we only have equivalence classes of ascending sequences over Cc. Various wrappers, conversion operations, and proof terms are used to produce the adequate equivalence class. Of course, none of these details were visible in the mathematical definition of the limit (Definition 25), but in Coq all the details are exposed. The proof of the fact that lim actually computes the least upper bound of its argument amounts to a similar exposure and management of many details, none of which is visible in the mathematical statements -Theorem 26 and its proof.

  corecursive function definitions have to satisfy a guardedness-by-constructors criterion. This criterion ensures a strong version of productiveness, namely, that each evaluation step produces a strictly closer approximation of the final result than the previous steps. By contrast, productiveness only requires that eventually a strictly closer approximation is obtained. In some cases, a function that is productive

Theorem 10. If

  a functional F is productive then lim[(F n ) n∈N ] is the unique fixpoint of F.

E C O O P 2 0 2 2 12:6 Defining Corecursive Functions in Coq Using Approximations Proof.

  Let the type of the functional be (D → C) → D → C. By Definition 4, for all x ∈ D, the sequence (F n x) n∈N is increasing and its limit is maximal w.r.t. . Hence, for all x ∈ D, lim[(F n x) n∈N ] exists, and let f : D → C be defined by f x = lim[(F n x) n∈N ] for all x ∈ D.

2 2 12:8 Defining Corecursive Functions in Coq Using Approximations based

  on Coq's builtin mechanisms seen in the previous section. We also show an example where the present construction of a CPO is essential because Coq's builtin mechanisms for coinduction fail. Given a set C • and an order • on it, a measure on

	Definition 15.

sequences, according to a certain equivalence relation. We illustrate the notions introduced in this section by giving an alternative construction of a CPO of streams, different from the construction E C O O P 2 0

  Given two ascending sequences (s n ) n∈N and (s n ) n∈N , if for all k ∈ N there exists m ∈ N such that s k s m , then (s n ) n∈N ∼ (s n ) n∈N .

	The next lemma gives a useful sufficient condition for the equivalence of ascending sequences.
	Lemma 21.

• , the restriction of the relation ∼ from Definition 17 to ascending sequences of elements of C • is an equivalence relation.

Proof.

For reflexivity, we use the fact that the sequence (µ s n ) n∈N of measures of an ascending sequence (s n ) n∈N tends to infinity, hence, for each N there is n ∈ N such that µ s n ≥ N, and we take x := s n in Definition 17 to show (s n ) n∈N ∼ (s n ) n∈N . For symmetry, it is enough to note that Definition 17 is a symmetrical statement in (s n ) n∈N , (s n ) n∈N . For transitivity assume (s

n ) n∈N ∼ (s n ) n∈N and (s n ) n∈N ∼ (s n ) n∈N .

Fix an arbitrary N ∈ N. By Definition 17, there exist m, m ∈ N and y, y ∈ C • such that y • s m , y • s m , y • s m , y • s m , and µ y, µ y ≥ N. Since the sequences are increasing, we have y, y • s (max m m ) and since • is weakly total, y • y or y • y. Assume y • y . Then, for the arbitrarily chosen N, we set n := (max m m ) and x := y in Definition 17 and, since the sequences are increasing, we obtain (s n ) n∈N ∼ (s n ) n∈N . The other case (y • y) is similar.

  The reverse implication in Lemma 21 does not hold in general: there exists sequences (s n ) n∈N and (s n ) n∈N such that for all n, m ∈ N, s n and s m are incomparable, yet (s n ) n∈N ∼ (s n ) n∈N because the sequences have in common another sequence that pointwise under-approximates them and whose measure tends to infinity, i.e., they obey Definition 17. The latter is the proper definition of equivalence: if instead we had taken for all k ∈ N there exists m ∈ N such that s k s m as in Lemma 21 we would be distinguishing certain sequences -namely, those that have a common sequence of under-approximations whose sizes tend to infinity, yet are pointwise incomparable -that should not be distinguished, because pointwise the difference between them becomes "negligible". Assuming a set C • and a weakly total order relation • on C • , the completion of the set and its order to a set C and an order on C are defined as follows:

	Definition 22.

C = C • ∪ K, where K is the set of equivalence classes modulo ∼ of ascending sequences of elements in C • : is the smallest relation on C satisfying for all x, y ∈ C • , x y if x • y;

for all x, y ∈ K, x y if x = y; for all x ∈ C • and y ∈ K, x y if for all (s n ) n∈N ∈ y, there exists m ∈ N such that x • s m .

  • , x [(s n ) n∈N ] ∼ iffthere exists m ∈ N such that x s m .Proof. By Definition 22, x [(s n ) n∈N ] ∼ means: for all (s n ) n∈N ∈ [(s n ) n∈N ] ∼ , there exists m ∈ N such that x • s n . The "only if" direction is trivial since obviously (s n ) n∈N ∈ [(s n ) n∈N ] ∼ .We thus focus on the "if" direction. By hypothesis, there exists m ∈ N such that x • s m . Choose anarbitrary (s n ) n∈N ∈ [(s n ) n∈N ] ∼ , i.e., (s n ) n∈N ∼ (s n ) n∈N .By Definition 17, there exists x ∈ C • and m ∈ N such that x • s m , x • s m and µ x > µ x. Since the sequences are increasing, we obtain x, x • s (max m, m ) . From the latter and the weak totality of • we obtain x • x or x • x. But x • x contradicts the established µ x > µ x. Hence, x • x and then x • s m follows from x • s m by transitivity. Summarizing, for the arbitrarily chosen sequence (s n

Rusu and D. Nowak 12:11 hence

  first show that [(s n ) n∈N ] ∼ is an upper bound for (s n ) n∈N : s k [(s n ) n∈N ] ∼ for all k ∈ N. We apply Lemma 24 with x := s k : there exists m := k such s k s m , which implies s k [(s n ) n∈N ] ∼ . , s n i w for all i ∈ N, and due to the properties of the measure, µ s n i µ w for all i ∈ N.But this is impossible, since the sequence of measures of a strictly increasing sequence is a strictly increasing sequence of natural numbers, which tends to infinity. Hence, w ∈ C • is impossible. It follows that w ∈ K, i.e., w = [(s n ) n∈N ] ∼ for some ascending sequence (s n ) n∈N . From our hypothesis s k w for all k ∈ N, we obtain that for all k ∈ N there exists m ∈ N such that s k• s m . Using Lemma 21, (s n ) n∈N ∼ (s n ) n∈N , i.e., [(s n ) n∈N ] ∼ = [(s n ) n∈N ] ∼ =w and in particular [(s n ) n∈N ] ∼ w. Since the upper bound w was chosen arbitrarily, we have proved that [(s n ) n∈N ] ∼ is the least upper bound for (s n ) n∈N . The proof of the theorem is complete.

Then, we show that [(s n ) n∈N ] ∼ is the least upper bound for (s n ) n∈N . Assume any upper bound w ∈ C, thus, s k w for all k ∈ N. Suppose first that w ∈ C • . Since (s n ) n∈N is ascending, it has a strictly increasing subsequence (s n i ) i∈N . Now, w is also an upper bound for the subsequence, V.

2 2 12:12 Defining Corecursive Functions in Coq Using Approximations

			1	F nth n l 2
	fails to meet the critical weak totality requirement (Definition 18). Indeed, e.g., for t , t	⊥,
	t = tree a [t , t ], t 1 = tree a [t , ⊥] and t 2 = tree a [⊥, t ] satisfy t 1	F t and t 2	F t, yet t 1 and t 2 are
	incomparable. Without weak totality there is no sequence equivalence and ultimately no CPO 2 .

2

Our earlier attempt with metric spaces also required a weakly total order for obtaining a proper notion of distance.

E C O O P 2 0

Rusu and D. Nowak 12:13 sequences

  are equivalent, we have the equality[(s n ) n∈N ] ∼ D = [(s n ) n∈N ] ∼ D . In particular, it follows that [(s n ) n∈N ] ∼ D is an upper bound for (s n ) n∈N , thus for all n ∈ N, s n D [(s n ) n∈N ] ∼ Dand by Lemma 24, (i): for all n ∈ N, there exists m ∈ N such that s n • D s m . Since f • is productive, it is also increasing, and thus from (i) we obtain (ii): for all n ∈ N , there exists m ∈ N such that f • s n • C f • s m . Using Lemma 21 we obtain ( f • s m ) m∈N ∼ C ( f • s m ) m∈N , which proves the lemma.

Definition 22 and Theorem 26 the equivalence class [(s n ) n∈N ] ∼ D is the least upper bound of (s n ) n∈N and the equivalence class [(s n ) n∈N ] ∼ D is the least upper bound of (s n ) n∈N . Since the two V.

6 Conclusion, related work, and future work

	This paper presents two methods for defining corecursive functions that go beyond the guarded-

by-constructor setting available in the Coq proof assistant. The first method reuses the dedicated coinduction mechanisms available in Coq, which works as long as the underlying coinductive datatypes are not mutually dependent with inductive types. The second method is not subject to this V.

Rusu and D. Nowak 12:19 restriction

  , as it does not rely on Coq's coinduction mechanisms but redefines them, at the cost of some additional work. Both methods have in common the interpretation of maximal values in CPOs as well-defined corecursive values, and they both rely on a mathematical notion of productiveness that captures the corresponding intuitive notion of productiveness (the ability of a function to eventually generate, for each input, an arbitrarily close approximation of the corresponding output). Both methods are implemented in Coq and are illustrated by defining corecursive functions that Coq's dedicated mechanisms reject. This gain in expressiveness is obtained at the cost of using axioms from the standard library of Coq, which are known not to introduce inconsistencies: using them amounts to losing constructiveness, but gaining access to standard mathematical reasoning. Both methods were presented independently of Coq; especially the second one, which is independent from Coq's builtin mechanisms for corecursion, could be implemented in other proof assistants. An interesting target is Lean [14], a dependently-typed language and proof assistant that includes the additional feature of quotient types that would naturally encode equivalence classes in the second method.The methods we propose transform a problem currently without solution (defining corecursive functions that do not satisfy the guardedness condition) into a problem that is solvable: defining and reasoning about functions that approximate the function under definition. In practice the approximating functions are recursive, as can be seen from the examples in the paper (Examples 14 and 31) and from the additional ones in the companion Coq development. Now, if for a given corecursive function the corresponding approximating recursive functions are difficult to reason about, then applying our methods may be difficult. However, most of the difficulty does not arise from the methods, but from the intrinsic complexity of the corecursive function being defined.

This intuition can be formalized using a notion of distance, thus turning C • into a metric space. We have tried but discarded that approach because is complicates matters (one now has an order, a distance, and a measure, which have to satisfy certain properties) without any other benefit that perhaps a better intuition for the notion of equivalence.

21

The Isabelle/HOL Proof Assistant. https://isabelle.in.tum.de/.


Stéphane Viollet
email: stephane.viollet@cnrs.fr

Nicolas Huloux
email: nicolas@aflokkat.com

Julien Diperi

Jean-Marc Ingargiola

Akiko Kato

Yan Ropert-Coudert
email: yan.ropert-coudert@cebc.cnrs.fr

Open source bio-logger for monitoring and recording inertial movement

Keywords: inertial measurement unit, data logger, sport, hydrofoil

I. INTRODUCTION

A bio-logger is a device attached to an animal or a human in order to record data about their movement (position, speed, temperature, etc...) and their surroundings. Bio-loggers have been originally developed for studying birds and marine animals (see [START_REF] Fehlmann | Bio-logging[END_REF]), and have been extensively used for fully automated monitoring of a wide variety of terrestrial and marine organisms [START_REF] Ripperger | Thinking small: nextgeneration sensor networks close the size gap in vertebrate biologging[END_REF][START_REF] Ropert-Coudert | Bio-logging: recording the ecophysiology and behaviour of animals moving freely in their environment[END_REF][START_REF] Rutz | New frontiers in biologging science[END_REF], see Williams et al. for a review [START_REF] Williams | Optimizing the use of biologgers for movement ecology research[END_REF]). Nowadays, many bio-loggers are available on the market (Wildlife Computers, Little Leonardo, Star Oddi...), however, they rely on proprietary hardware and software architecture which leaves little room for customization. In addition, most studies on animals or humans use only a portion of what could be done with these sensors [START_REF] Marin | Human and animal motion tracking using inertial sensors[END_REF].

Recently, it has been shown that Euler angles could be derived from attitude estimation algorithms such as the one proposed by Madgwick [START_REF] Madgwick | Estimation of imu and marg orientation using a gradient descent algorithm[END_REF] on the basis of accelerometer, rate gyro and magnetometer signals composing the so-called Inertial Measurement Unit (IMU). Inertial studies have found an interest in sport performance evaluation [START_REF] Minetto | Machine learning approach to sport activity recognition from inertial data[END_REF]. In their recent systematic review, Camomilla et al. have evaluated the usefulness of magneto-inertial sensors for sport performance metrics during training or competition [START_REF] Camomilla | In-field use of wearable magneto-inertial sensors for sports performance evaluation[END_REF].

The present work details an open-source magneto-inertial sensor encased in a data logger originally designed for mea-suring pitch, roll and heading to reconstruct head-body movements in penguins and which is applied here to a hydrofoil kiteboard. Kiteboarding is a worldwide sport featuring 1,5 millions kitesurfers. Inertial sensor have already been used for the study of the motion of the kite itself [START_REF] Nebas | A smartphone based system for kite and board measurements in kitesurfing[END_REF], or to measure jump height [START_REF]WOO -Worldwide Kiteboarding Game[END_REF]. Here and for the first time, we show that inertial data logging of the kiteboard can provide useful information on other parameters, such as turning rate amplitude, pitch and roll angle values during straight trajectories and synchronized movement analysis during heading changes (maneuvers).

II. STAND-ALONE DATA LOGGER

A. Hardware description

Figure 1 shows our magneto-inertial data logger, constructed with off-the-shelf components: the core controller is an Arduino-compatible Nano 33 board wired via a custommade connection board to an Adafruit data logger board. The latter includes a micro SD card for recording the data and a real-time clock circuit (RTC) for dating the recorded files. The Arduino board includes a 9-axis IMU and a Bluetooth LE chip for wireless communication with external devices. Finally, a single cell lithium-polymer battery was used for powering. The component specifications and costs are summarized in table I.

B. Software description

The logger software was written in C with the Arduino IDE. A fully annotated version that describes the program flow and functionality can be downloaded on Github [START_REF] Viollet | Biologger code[END_REF]. The program is based on standard Arduino libraries to address the various peripherals of the microcontroller. Time is a very critical parameter when dealing with bio-logging. To ensure a constant sampling time, timing interval, in milliseconds, between two successive acquisitions was measured. The time-lapse is then compared to a threshold set to 10ms, and supplementary acquisition points can be done if the time lapse is superior to the the threshold. Later, in section III-B, the performance of this strategy is provided.

Sensor raw values (accelerations, angular rates, magnetic inclinations) are recorded on the SD memory card every 10 ms. More, from these raw values, the three Euler angles are computed simultaneously and at the same time, leading to a total of 13 parameters recorded every 10 ms. The logger can be remotely controlled with the Bluetooth Low Energy interface (BLE), by sending control commands to start, stop the acquisition or read the sensor values. Hence, the three Euler angles can be sent via BLE on request, Which is particularly useful once the logger is secured in its sealed waterproof package without any external button. The two programs written in python that are used to fully control the logger are provided for a linux or an IOS interface.

III. FIELD TESTS: KITEBOARD ATTITUDE MEASUREMENT

Prior to field tests, the logger was calibrated following the procedure described in the Arduino LSM9DS1 library, written by Verbeek [START_REF] Verbeek | Lsm9ds1 library[END_REF]. As water is not compatible with electronic components, the electronic boards and the battery were secured in a waterproof plastic bag (a condom) and then placed in a custom 3D printed box. This waterproof logger is then fixed to an aluminum fuselage of a hydrofoil (IC6V2, FOne, France) with an adhesive rubber band (Electrical tape, 3M, USA). The place of the logger on the fuselage was chosen to reduce hydrodynamic perturbation and let the hydrofoil work normally. The fuselage is tightly screwed to its corresponding aluminum mast which is fixed to a kiteboard (custom made). The Figure 2 shows the hydrofoil used for this study and the logger in its waterproof casing on the fuselage.

The man chosen for the experiment, which is one of the author, has 3 years of learning hydrofoil and could be considered as a skilled kitesurfer. He was asked to record its trajectories from a GPS watch (Ambit3 Peak, Suunto, Finland). This measure is computed to find an estimation of the heading, which is then compared to the heading metric provided by the logger. At the very beginning of the experiment the logger was immersed into water at a depth of 90 cm, i.e., the length of the mast between the hydrofoil plane and the kiteboard. Then, during the experiment the logger was at a depth of around 40 cm, which is the usual functional depth of a hydrofoil designed for kitesurfing. The Figure 3 shows the 23 minutes GPS record from the GPS watch. During the experiment 13 straight two-way trajectories were recorded of about 400 m long each. The average speed was about 8 m/s (i.e., 29 km/h), a value which is coherent with the 32 km/h wind speed measured on the day we conducted the experiment in Marseille, France (source [START_REF]Diabox -Pacific Palissades[END_REF]). Also, the pitch was very constant during the whole experiment and was equal to -7.2 • ± 11.6 • , which corresponds to a slight pitch up of the kiteboard. In addition, the angular speed was relatively low in pitch and roll (inferior to 10 • /s) but the heading rate was high during the maneuvers. This metric could be interpreted as an evaluation of the ability of the kitesurfer to change more or less rapidly the heading.

Figure 5 shows the heading measured by the logger (black) along with the estimated heading from the GPS watch (grey). The heading estimated from the GPS at a sample number i was calculated as:

H GP S eading (i) = arctan 2 Y pos (i) -Y pos (i -1) X pos (i) -X pos (i -1) (1)
where,

X pos = R * λ and Y pos = R * ϕ ( 2
)
where R is the radius of the earth equal to 6371 km, λ is the longitude and ϕ the lattitude in radian.

The speed of the kiteboarder (Fig. 5) was calculated as:

S GP S peed = diff (X pos ) 2 + diff (Y pos ) 2 (3)
with diff the approximate derivative function (difference between adjacent elements).

As the two headings cannot be synchronized during the experiment, we applied a post hoc time correction from the calculation of the cross correlation function between the heading signal measured by the logger and the GPS estimated heading calculated from 1. The time lag between the two signals corresponds to the maximum correlation found here to be equal to 67 samples. The heading measured from the logger was filtered by means of 1D median filter (dimension to filter along of 140 samples). The Figure 5 indicates an excellent correlation between the two heading signals, validating the good accuracy of the logger. We described here the design and performance of magnetoinertial sensor able to measure and record in real time the 3D orientations based on Euler angle of an hydrofoild fixed to a kiteboard. Angular velocities along the sensing axes were also estimated. We compared the measured heading with the estimated heading from a GPS watch and showed an excellent correlation despite the fact that the heading measurement was done into the sea at a depth of 40 cm. We are now working on a highly miniaturized version (26 × 31 mm 2 ) of the logger in order to reduce its impact on the hydrodynamics of the hydrofoil or other bodies it would be attached to. In addition, it could be valuable to compare the orientation provided by the logger with another logger placed for example on the leg of the kitesurfer.

Fig. 1 .

 1 Fig. 1. Data logger design for onboard recording as a stand-alone device. Yaw, pitch and roll angles are recorded at 100 Hz.

Fig. 2 .Figure 4

 24 Fig.2. Hydrofoil of the kiteboard equipped with the logger. The logger is encapsulated in a condom to make it waterproof before being placed in a custom 3D printed box.

Fig. 3 .

 3 Fig. 3. Trajectories of the kitesurfer recorded with a GPS watch at 1 Hz. The starting and end points are the point indicated by the red dot.

(x10 4 )Fig. 4 .

 44 Fig. 4. Measured Euler angles (roll, pitch, heading) samples.

Fig. 5 .Fig. 6 .Fig. 7 .

 567 Fig. 5. a. Measured heading from the logger (black) and estimated heading from GPS (grey). b. Linear speed of the kiteboarder calculated from the GPS positions. c. Correlation rate used to synchronize the heading signals.

ACKNOWLEDGMENT

This research was supported by CNRS (Mission for Transversal and Interdisciplinary Initiatives, PenGaze project) and Aix-Marseille University.

B. Real-time acquisition performance

The performance of the real time acquisition is assessed from the fine measure of the time-lapse between two successive acquisitions. Histograms of this time-lapse has been plotted as a proxy of the performance. To compare different computational burden of the micro-controller, we studied 3 cases:

• case 1: only tri-axes accelerometer signals are recorded on the SD card, Euler angle computing is disabled • case 2: tri-axes accelerometer signals and computed Euler angle are recorded on the SD card • case 3: all signals of the magneto-inertial sensor and the three Euler angles are recorded on the SD card Histograms shown in Figure 7 were computed with 200 bins for each case. As expected, over a total of 105000 samples, we obtained a large number of time intervals equal to 10 ms, which correspond to the sampling time: from 86000 in case 3 up to 99000 in case 1. However, the number of lapses of time equal to 20 ms was a bit higher in case 3 due to a higher quantity of data to record on the SD card. In any case, this test confirmed the good performance of the data logger in terms of real time acquisition.