David Romero Hernández

David De Frutos
email: defrutos@sip.ucm.es

Escrig Dpto

Coinductive Definition of Distances Between Processes: Beyond Bisimulation Distances ⋆

Bisimulation captures in a coinductive way the equivalence between processes, or trees. Several authors have defined bisimulation distances based on the bisimulation game. However, this approach becomes too local: whenever we have in one of the compared processes a large collection of branches different from those of the other, only the farthest away is taken into account to define the distance. Alternatively, we have developed a more global approach to define these distances, based on the idea of how much we need to modify one of the compared processes to obtain the other. Our original definition only covered finite processes. Instead, now we present here a coinductive approach that extends our distance to infinite but finitary trees, without needing to consider any kind of approximation of infinite trees by their finite projections.

Introduction

Bisimulation [START_REF] Park | Concurrency and automata on infinite sequences[END_REF][START_REF] Milner | Communication and concurrency[END_REF][START_REF] Sangiorgi | Advanced topics in bisimulation and coinduction[END_REF] is a popular way to define the semantics of processes. Starting from their operational semantics, defined by a transition system, it captures the "natural" behavior of the processes, paying attention to the branching in them, but abstracting away from possible repetitions of equivalent behaviors. Bisimulations are just coinductive proofs of the equivalence between processes, and in fact they became one of the main causes of the popularization of the study of coinduction [START_REF] Sangiorgi | Advanced topics in bisimulation and coinduction[END_REF] and coalgebras [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF][START_REF] Jacobs | Exercises in coalgebraic specification[END_REF][START_REF] Jacobs | Introduction to coalgebra. towards mathematics of states and observations[END_REF] in the last years. They can be established in many different ways, in particular by means of the bisimulation game [START_REF] Stirling | The joys of bisimulation[END_REF], that enlightens the co-character of bisimilarity.

When comparing two processes, the proof of their bisimilarity certainly indicates us that they are equivalent. The problem comes if we receive the information that they are not bisimilar. Then, if we substitute one component by the other, it is expected that the behavior of the full system will change "at least a bit". We want to quantify those deviations; they are formalized by our (new) distance between processes with respect to the bisimulation equivalence.

Recently, several variants of the bisimulation game have been used to define "bisimulation distances" [START_REF] De Alfaro | Game relations and metrics[END_REF][START_REF] Desharnais | Approximate analysis of probabilistic processes: Logic, simulation and games[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF][START_REF] Cerný | Quantitative simulation games[END_REF]. They develop the seminal ideas in several previous works, such as [START_REF] Desharnais | Metrics for labeled markov systems[END_REF][START_REF] Giacalone | Algebraic reasoning for probabilistic concurrent systems[END_REF][START_REF] Ying | Approximate bisimilarity[END_REF]. However, as we have already illustrated in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF][START_REF] Romero-Hernández | Distances between processes: A pure algebraic approach[END_REF] by means of several examples, these distances have some "limitations", that we try to remove by means of our new bisimulation distance. We also include in this paper some new examples enlightening the difference between our approach and those based in the bisimulation game.

Whenever we formalize the family of computations of a process we obtain a tree. Therefore, any distance between processes induces a distance between those trees. We have followed this path in the opposite way: let us look for a "natural" notion of distance between trees, and we will turn it into a distance between processes. In [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF] we have presented an operational definition of our new global bisimulation distance for the particular case of finite trees. Roughly speaking, we define our distance between trees "computing" the costs in order to transform one of the trees into the other. We consider a given distance d on the alphabet of actions, so that the cost of substituting an action a by another b is given by d(a, b).

In this paper, we use coinduction to define the distance between processes in which we are interested. Of course, an alternative way to define the distance between infinite trees is to approximate them by their finite projections, and then taking limits. Looking for an "homogeneous" procedure that could capture all these approximations in a compact way, we introduce our coinductive distance as the coinductive "closure" of the finite transformations by means of which we defined our distance between finite processes in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF]. Once we have it, we get all the machinery of coinductive proofs in order to study our distance.

Even if the notion of tree is omnipresent in the field of semantics of processes, there is not a clearly standardized presentation of the different classes of trees in the literature. This is why we start the paper by reminding in Section 2 the definitions on trees and labelled transition systems that we use in the following. In Section 3, we recall the previous work on bisimulation distances and our alternative operational proposal covering mainly finite trees. Section 4 is the core of the paper and presents the coinductive extension of this approach covering also infinite trees. Finally, we conclude with a short section devoted to a discussion on the continuity of the coinductive distance, and the conclusions of the paper.

We strongly acknowledge the detailed reading and the suggestions of the referees of this paper, that have contributed to improve the presentation of this work.

Preliminaries

Let us start by recalling the coalgebraic definition of labelled transition systems (lts). As usual, we use them to represent the operational semantics of processes. Definition 1. Labelled Transition Systems (lts) 1 on a set of actions A and a set of states N , are given by a function succ : N → P(A × N ). We denote each lts by the corresponding pair (N, succ). A lts with initial state (N, succ, n 0 ), is just a lts (N, succ) where some distinguished (initial) state n 0 ∈ N is fixed. To simplify our notation, we usually remove the succ component from lts's.

We say that any sequence n 0 a 1 n 1 . . . a k n k with (a i+1 , n i+1 ) ∈ succ(n i ) ∀i ∈ {0 . . . k -1}, is a path in (N, n 0 ). We denote the set of paths (or computations) by P ath(N, n 0 ). We say that the system

N is finite state, if |N | < ∞; (N, n 0 ) is finite, if |P ath(N, n 0 )| < ∞;
we say that (N, n 0 ) has only finite computations, if there is no infinite path n 0 a 1 n 1 a 2 n 2 . . . . We say that a system N is finitely branching, if for all n ∈ N we have |succ(n)| < ∞.

Example 1. (See Fig. 1) Two simple finite-state systems that however have infinitely many computations are the following:

N 1,∞ = {n 0 }, with succ(n 0 ) = {(a, n 0 )}; N 2,∞ = {n 0 , n 1 }, with succ(n 0 ) = succ(n 1 ) = {(a, n 0 ), (a, n 1 )}.
Example 2. (See Fig. 1) Next three interesting non-finitely branching systems:

1. N N = (N, succ, 0) with A = N, succ(0) = {(k, k) | k ∈ N}, succ(k) = ∅, ∀k > 0. 2. N 2 = {0} ∪ {(i, j) | i, j ∈ N, 1 ≤ j ≤ i}, taking n 0 = 0 with succ(0) = {(a, (n, 1)) | n ∈ N} and succ((i, j)) = {(a, (i, j + 1))} if j < i, while succ((i, i)) = ∅. 3. N + 2 = N 2 ∪ {(∞, n) | n ∈ N}, changing also the definition of succ, taking succ(0) = {(a, (x, 1)) | x ∈ N ∪ {∞}} and succ((∞, j)) = {(a, (∞, j + 1))}.
We can define (rooted) trees as a particular class of lts's: Definition 2. We say that a system (N, n 0 ) is (or defines) a tree t if for all n ∈ N there is a single path n 0 a 1 n 1 . . . a k n k with n k = n. Then, we say that each node n k is at level k in t, and define Level k (t) = {n ∈ N | n is at level k in t}. We define the depth of t as depth(t) = sup{l ∈ N | Level l (t) = ∅} ∈ N ∪ {∞}. We denote by T rees(A) the class of trees on the set A, and by F T rees(A), the subclass of finite state trees.

Any node n ∈ N of a tree t = (N, succ, n 0 ) induces a subtree t n = (N n , succ, n), where N n is the set of nodes n ′ k ∈ N such that there exists a path

n ′ 0 a 1 n ′ 1 . . . a k n ′ k with n ′ 0 = n.
We decompose any tree t into the formal sum n1j ∈Level1(t) a j t n1j . Since our trees are unordered, by definition, this formal sum is also unordered. The tree 0 corresponds to the system ({n 0 }, succ 0 , n 0 ) with succ 0 (n 0 ) = ∅, while if |Level 1 (t)| = 1 we have t = at ′ , which can be reversed to define the tree at ′ starting from a ∈ A and t ′ ∈ T rees(A). In a similar way, whenever Level 1 (t) = N 1 ∪ N 2 is a disjoint decomposition of that set, we can write t = n1j ∈N1 a j t n1j + n 1k ∈N2 a k t n 1k , which can be also reversed to define the sum (+) of trees. Note that + becomes commutative by definition.

For any tree t ∈ T rees(A), we define its first-level width, that we will represent by ||t||, as ||t|| = |Level 1 (t)|. We also define the first k-levels width of t, denoted by ||t|| k , as ||t|| k = max{||t n || | n ∈ l≤k Level l (t)}. Finitary trees are just trees that are finitely branching systems, or equivalently, those such that Definition 4. Let (N, succ) be a lts. We say that a relation R on N is a bisimulation, if for all (n, n ′ ) ∈ R we have

N1,∞ N2,∞ n0 n0 n1 NN N2 N + 2 0 0 0 . . . . . . . . . 1 2 3 (1, 1) (2, 1) (3, 1) (1, 1) (2, 1) (3, 1) (∞, 1) (2, 2) (3, 2) (2, 2) (3, 2) (∞, 2) (3, 3) (3, 3) (∞, 3) . . .
-∀ (a, n 1 ) ∈ succ(n) ∃ (a, n ′ 1 ) ∈ succ(n ′ ), (n 1 , n ′ 1 ) ∈ R. -∀ (a, n 2 ) ∈ succ(n ′ ) ∃ (a, n ′ 2 ) ∈ succ(n), (n ′ 2 , n 2 ) ∈ R.
We say that n and n ′ are bisimilar if there exists some bisimulation R such that (n, n ′ ) ∈ R, and then we write n ∼ n ′ .

By considering the disjoint union of two systems, we can extend the definition above to relate states from two different systems. In particular, if we consider two lts with initial state (or equivalently two trees) we say that (N, succ, n 0 ) ∼ (N ′ , succ ′ , n ′ 0 ) if and only if there is a bisimulation containing the pair (n 0 , n ′ 0 ). Usually we will simply write n 0 ∼ n ′ 0 , and the same in the case of trees, as usual. The fact that systems are represented by their unfolding is formalized by the following result. Proposition 1. For any lts with initial state (N, succ, n 0 ), and its unfolding (N , succ, n 0 ), we have n 0 ∼ n 0 . Definition 5. Given a tree t = (N, succ, n 0 ) and k ∈ N, we define its k-th cut or projection, π k (t), as the restriction of t to the nodes in l≤k Level l (t):

π k (t) = (π k (N ), succ k , n 0 ), where π k (N ) = l≤k Level l (t), succ k (n) = succ(n)
for n ∈ l<k Level l (t), and succ

k (n) = ∅ if n ∈ Level k (t).
Proposition 2. For any t ∈ T ree(A) and l, k ∈ N with l ≤ k, we have π l (π k (t)) = π l (t). Any finitary tree is unequivocally defined by its sequence of projections: ∀t, t ′ ∈ F yT ree(A)

(∀k ∈ N π k (t) ∼ π k (t ′ )) ⇒ t ∼ t ′ .
Example 3. The result above becomes false if we consider infinitary trees. For the trees N 2 and N + 2 in Ex.2, we have π k (N 2 ) ∼ π k (N + 2 ) ∀k ∈ N, since the "additional" branch executing a k provided by N + 2 can be "absorbed" by the infinitely many such branches that we already have in π k (N 2 ). Therefore, this is a (well known) counterexample disproving the continuity of bisimilarity wrt the approximations, provided by the projections π k , if we allow infinitary trees.

As a consequence, we will restrict ourselves to finitely branching processes all along the rest of the paper. It would not be enough to consider instead just image finiteness trees, because our approach considers all the successors of each node in an homogeneous way, without taking care of their labels. Then, problems can appear as soon as a node has infinitely many successors. The well known bisimulation game [START_REF] Nielsen | Bisimulation, games, and logic[END_REF][START_REF] Stirling | Bisimulation, modal logic and model checking games[END_REF], allows us to characterize the bisimilarity relation. It is played by two players: the attacker (A) and the defender (D). The former executes any fireable transition from one of the compared trees, and the second has to reply it in the other tree. The attacker wins if the defender cannot counteract one of his moves; while the defender wins if he can reply forever.

Classical and Global bisimulation distances

Theorem 1. ( [START_REF] Nielsen | Bisimulation, games, and logic[END_REF][START_REF] Stirling | Bisimulation, modal logic and model checking games[END_REF]) For any t,t ′ ∈ T rees(A) t ∼ t ′ (resp. t ∼ t ′ ) if and only if D (resp. A) has a winning strategy for the bisimulation game starting at (t, t ′ ).

Most of the recent approaches to define distances between processes -e.g. [START_REF] Fahrenberg | The quantitative linear-timebranching-time spectrum[END_REF]use quantitative versions of the bisimulation game. As in the plain bisimulation game, the defender has to simulate the action played by the attacker, but in this case he can fail to reply an a transition, firing instead some b. However, whenever he cheats the attacker, he has to pay him for the distance d(b, a). Then, the distance between two trees t and t ′ (equivalently, between two processes) is defined as the value of that game starting from the roots of t and t ′ . In the following, we will call "classical" the distances defined following this approach.

Inspired by the notion of amortized bisimulation [START_REF] Kiehn | Amortised bisimulations[END_REF], we have developed a coinductive presentation of the classical bisimulation distances [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF]. Instead of giving a definition of the distance between two trees, that requires the use of fixpoint theory, we state when an indexed family of relations between trees provides a collection of bounds on the distances between the pairs of trees in them.

As done for instance in [START_REF] Cerný | Simulation distances[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF], and thoroughly discussed in [START_REF] De Alfaro | Discounting the future in systems theory[END_REF], when comparing pairs of processes, it is natural to introduce a "discount factor" α ∈ (0, 1). Then, the differences in the k-th level of the compared trees are weighted by α k , following the idea that differences in the far future are less important than those in the near. As a consequence, it is possible to obtain finite distances when comparing two processes with "infinitely many differences" between them. However, we will also allow that α = 1 to cover the case in which we are not interested in the weighting of those differences. Definition 6. (see [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF]) Given a domain of actions (A, d) and a discount factor α ∈ (0, 1], we say that a family of relations between trees,

R ⊆ T rees(A) × T rees(A) × R + , is a classical bisimulation distance family (cbdf ) for d and α, if it satisfies t R d t ′ t R d t ′ =⇒ ∧ ⇐= t 1 R d-d(b,a) α t ′ 1 t 1 R d-d(b,a) α t ′ 1 ∀ a ∃b ∀ b ∃a
where, we take tR d t ′ if and only if (t, t ′ , d) ∈ R and implicitly, we are assuming that the values dd(b, a) are nonnegative. We say that t and t ′ are at most at classical bisimulation distance d for the factor α, and then we write d α d (t, t ′ ) ≤ d, if there is some cbdf R with tR d t ′ . Proposition 3. (see [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF]) The value of the quantitative game -see [START_REF] Fahrenberg | The quantitative linear-timebranching-time spectrum[END_REF]-defining the "classical" bisimulation distance

dist α d (t, t ′ ) is inf({d ∈ R + | d α d (t, t ′ ) ≤ d}).
It is well known that, for finitary trees, this classical bisimulation distance is indeed a quantitative refinement of bisimilarity.

Theorem 2. For all t, t ′ ∈ F yT rees(A) and any discount factor α ∈ (0, 1], we have t ∼ t ′ if and only if d α d (t, t ′ ) ≤ 0, if and only if dist α d (t, t ′ ) = 0. In spite of this, we consider that in some cases this distance generates values that do not accurately reflect the differences between some pairs of trees.

Example 4. (see Fig. 2) We have a service that allows some access to the bits of our password, once we have identified ourselves in the appropriate way. Let us abstract this service as the tree t = i∈1..64 a i . Now, let us assume that a ′ i represents a cracked access to the corresponding position. Then, for each j ∈ {1 . . . 64} the system represented by the tree t ′ j = ( i =j a i ) + a ′ j certainly is wrong, but does not compromise too much the security of the system. Instead, the totally cracked system represented by t ′ 1..64 = i∈1..64 a ′ i corresponds to a disastrous situation. If we take d(a i , a

′ i ) = 1, we obtain dist 1 d (t ′ j , t) = 1, but also dist 1 d (t ′ 1..64 , t) = 1. t tN t N ′′ t N ′ t N ′′′ • n0 n ′′ 0 n ′ 0 n02 . . . • • • n1 n0 n ′′ 1 n ′′ 2 n ′ 1 n ′ 0 n11 n12 t ′ 1..64 • n1 n0 n ′′ 3 n ′′ 2 n ′ 1 n ′ 0 n21 n22 . . . • • • n1 n0 n ′′ 3 n ′′ 2 n ′ 1 n ′ 0 n31 n32 . . . . . . . . . . . . a1 a2 a64 a ′ 1 a ′ 2 a ′ 64 0 0 1 0 1 0 1 0 0 0 1 0 0 0 2 0 0 0 1 0 0 0 4 0 Fig. 2. Trees used in Ex. 4 -Ex.8
The bad behavior of the "classical" bisimulation distance stems from the fact that the quantitative bisimulation game only considers single computations of the compared trees. As a consequence, it cannot capture the differences "accumulated" by repeated use of a system, as illustrated in Ex.4. Later, we will see how our "global" approach copes with this feature in a more satisfactory manner.

In [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF], we have presented our operational definitions that allow us to obtain bounds for our new global distances between finite trees. These bounds are given by the cost of any transformation that turns one of the trees into the other. The following definition states which are the valid steps of those transformations and their costs. Roughly, any application of idempotency of + has no cost, while the change of an action a at level k into another b has as cost α k d(b, a). (A,d) and a discount factor α ∈ (0, 1], we inductively define the distance steps on F T rees(A) by .64 ) = 1. We consider that our global distance reflects in a much more accurate way the "intuitive" distance between these trees.

Definition 7. Given a domain of actions

1. d ≥ 0 ⇒ (t 1 α,d t + t ∧ t + t 1 α,d t). 2. d ≥ d(a, b) ⇒ at 1 α,d bt. 3. t 1 α,d t ′ ⇒ t + t ′′
Example 6. We have to pass an examination about a subject with l lessons. A good student would study all of them, thus getting S = 1..l a l , which means that he totally knows the subject. At the exam the examiners choose somehow k lessons, and then each student can select a single one to develop. This means that any student that ignores up to k-1 lessons could perfectly pass the exam. These students are represented by S I = i / ∈I a i , where I is the set of lessons that they did not study. Now, at which extend such an student is risky? What happens if the day of the exam he forgets some lesson?. If |I| = k -1, then as soon as he forgets a single lesson he is in risk of failing; instead, if |I| = 1 he has definitely much more chances. This is again captured by our global bisimulation distance, but not by the classical one. The situation is similar to that studied in [START_REF] Henzinger | From model checking to model measuring[END_REF], where they wanted to capture how many failures are allowed before a system will fail to satisfy the requirements at its specification.

The coinductive global bisimulation distance

To get a general coinductive definition of our global distance for FyTrees(A), we keep the first three rules in Def.7, that allow us to make changes at the first level of the trees. But instead of rule 4, we introduce a coinductive rule that allows us to replace any non trivial subtree t at depth one by another t ′ , getting a distance αd, whenever (t, t ′ , d) is in the family that defines our global distance.

We formalize our definition in two steps. The first one, introduces the rules that produce the steps of the coinductive transformations between trees, starting from any family of triples (t, t ′ , d), with t, t ′ ∈ F yT rees(A) and d ∈ R + . Definition 8. Given a domain of actions (A, d), a discount factor α ∈ (0, 1] and a family D ⊆ F yT rees(A) × F yT rees(A) × R + , we define the family of relations ≡ D,α d , by: 1. For all d ≥ 0 we have (i) ( j∈J a j t j ) + at + at ≡ D,α d ( j∈J a j t j ) + at , and (ii) ( j∈J a j t j ) + at ≡ D,α d ( j∈J a j t j ) + at + at.

2.

( j∈J a j t j ) + at ≡ D,α d(a,b) ( j∈J a j t j ) + bt.

3. For all (t, t ′ , d) ∈ D we have ( j∈J a j t j ) + at ≡ D,α αd ( j∈J a j t j ) + at ′ . Remark 2. To simplify the notation, we will simply write ≡ d instead of ≡ D,α d , whenever D and α will be clear from the context.

Next, the second one. Inspired by the conditions imposed to bisimulations -that can be seen as "circular proofs" of bisimilarity of all the pairs in them-we introduce the coinductive proof obligations imposed to the families of triples as above, in order to define satisfactory coinductive families of distances. Definition 9. Given a domain of actions (A, d) and a discount factor α ∈ (0, 1], we say that a family D is an α-coinductive collection of distances (α-ccd) between finitary trees, if for all (t, t ′ , d) ∈ D there exists a finite coinductive transformation sequence In particular, using the trivial sequence C := 0 = 0, we can prove that 0 ≡ α d 0 for all d ∈ R + . This could not be inferred if we would impose instead the condition d = n j=1 d j . In fact, the case of 0 is the only one in which we need the inequality in Def. 9, because for any other tree t ′ we can apply Def. 8.1 twice, by considering any summand at of t ′ . Instead, in Def. 7 we can apply 7.1 even to t = 0, thus we can indeed simply take d = n i=1 d i at the end of the definition.

C := t = t 0 ≡ D,α d1 t 1 ≡ D,α d2 . . . ≡ D,α dn t n = t ′ ,
Remark 4. In order to avoid technical difficulties, the authors defining the classical bisimulation distance usually consider processes without termination. Instead, since we have mainly consider finite trees in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF], we needed to take into account termination. Our Def. 7 does not allow any "unexpected" termination when comparing two trees. If we desire to allow some terminations without necessarily entailing an infinite distance, then two simple extensions are possible. We could either establish a fixed payment f (that however will be weighted by the level at which it occurs), for any unexpected termination, including at any α-ccd D all the pairs (t, 0, f ), and no proof obligation for them. Or instead, we could pay for any lost action, considering a function lost : Act → R + . Then, we could introduce tuples (at + t ′ , 0, d) in the α-ccd family D, and for each one of them we need to check that there exist (t, 0, d 1 ), (t ′ , 0, d 2 ) ∈ D such that αd 1 + d 2 + lost(a) ≤ d. However, in order to make more understandable the paper, in the following we will not consider any of these extensions.

The next example presents a pair of trees with infinitely many differences, but a finite global bisimulation distance between them.

Example 7. (see Fig. 2) Let us consider the domain of actions (N, d), where d is the usual distance for numbers, and the trees t N = unf old(N ) and t N ′ = unf old(N ′ ), with N = {n 0 , n 1 }, succ(n 0 ) = {(0, n 0 ), (0, n 1 )} and succ(n 1 ) = ∅; and

N ′ = {n ′ 0 , n ′ 1 }, succ ′ (n ′ 0 ) = {(0, n ′ 0 ), (1, n ′ 1 )} and succ ′ (n ′ 1 ) = ∅. Then, we have t N ≡ D,1/2 2
t N ′ , using the family D = {(t N , t N ′ , 2)}. We can prove that this is indeed a 1 2 -ccd, by considering the sequence:

C := t N ≡ D,1/2 1 t N ′′ ≡ D,1/2 1 t N ′ , where t N ′′ = unf old(N ′′ ), with N ′′ = {n ′′ 0 , n ′′ 1 , n ′′ 2 , n ′′ 3 }, succ ′′ (n ′′ 0 ) = {(1, n ′′ 1 ), (0, n ′′ 2 )}, succ ′′ (n ′′ 1 ) = ∅, succ ′′ (n ′′ 2 ) = {(0, n ′′ 2 ), (0, n ′′ 3 )} and succ ′′ (n ′′ 3 ) = ∅.
The first step is obtained by application of rule 2 in Def.8, while the second one is obtained by application of rule 3, using the fact that 2 1 2 = 1. Note how the coinductive procedure "aggregates" the summands that produce the bound for the distance 2 in a single step. In fact, it is not necessary at all to sum any infinite series, as it would be the case if we would obtain that bound as the limit for the distances between the corresponding finite approximations of the two compared processes. Finally, we can observe that no bound d < 2 for the distance can be obtained in this way: t N ≡ D,1/2 d t N ′ does not hold for any d < 2, because for any such d we have d < 1 + d/2; so that, the check for the condition in Def. 9 would fail.

But, making greater the differences in the example above, we can get pairs of trees that are infinitely far away each other, wrt our global bisimulation distance.

Example 8. (see Fig. 2) Let us consider the tree t N from Ex.7, and the tree

t N ′′′ = (N ′′′ , succ ′′′ , n 0,2 ) with N ′′′ = {n 0,2 } ∪ {n i,j | i ∈ N -{0}, j ∈ {1, 2}}, succ ′′′ (n i,1 ) = ∅ and succ ′′′ (n i,2 ) = {(2 i , n i+1,1 ), (0, n i+1,2 )}. We have dist 1/2 d (t N , t N ′′′ ) = 1. Instead, t N ≡ 1/2 d
t N ′′′ does not hold for any d ∈ R + . As a matter of fact, for the finite projections of these two trees, we have

π k (t N ) ≡ 1/2 k π k (t N ′′′ ), for all k ∈ N, but we do not have π k (t N ) ≡ 1/2 d π k (t N ′′′ ), for any d < k.
Based on the notion of bisimilarity, our coinductive global bisimulation distance, and the α-ccd used to define it, inherit most of its basic properties, once quantified in the adequate way. As a consequence, we can assume that any ccd is ttc or +c, when convenient.

Given a family D, we define its tt-closure as the least family

D * defined by the clauses i) D ⊆ D * ; ii) If (t, t ′ , d), (t ′ , t ′′ , d ′ ) ∈ D * then (t, t ′′ , d + d ′ ) ∈ D * .

Given a family D, we define its +-closure as the family

D + = {(t + t ′′ , t ′ + t ′′ , d) | (t, t ′ , d) ∈ D}.
T := t = t 0,2 α,d11 t 1,1 1 α,d12 t 1,2 α,d21 • • • 1 α,d k2 t k,2 α,d (k+1)1 t k+1,1 = t ′
, where the d 1i + d 2i = d, and the distance steps t l,1 1 α,d l2 t l,2 in it are exactly all the first level steps in S. So that, no one of the subsequences producing t l,2 α,d (l+1)1 t l+1,1 contains any first level step.

Proposition 6. Any sequence S l producing t l,2 = m i=1 a i t i α,d (l+1)1 t l+1,1 = m i=1 a i t ′
i can be reordered getting an "ordered" sequence

O := t l,2 = m i=1 a i t i α,d 1 (l+1)1 a i t 1 i α,d 2 (l+1)1 a i t 2 i α,d 3 (l+1)1 • • • α,d m (l+1)1 a i t m i = m i=1 a i t ′ i = t l+1,1
, where m j=1 d j (l+1)1 = d, t j i = t ′ i ∀j ≤ i, and t j i = t i ∀j > i. This means that for each j ∈ {1, . . . , m} a i t j-1 i α,d j (l+1)1 a i t j i corresponds to a j t j α,d j (l+1)1 a j t ′ j , so that the distance steps in the former are exactly those from S l working at the corresponding summand a j t j of t. As a consequence, for each j ∈ {1, . . . , m} we also have t j α,(d j (l+1)1 )/α t ′ j , which is obtained by removing the common prefix a j from the steps of the subsequence generating a j t j α,d j (l+1)1

a j t ′ j .
Proposition 7. For t, t ′ ∈ F T rees(A), the operational (Def.7) and the coinductive definition of our distance between trees coincide, that means t

≡ α d t ′ ⇔ t α,d t ′ .
Proof. ⇒ | Given an α-ccd relating finite trees with (t, t ′ , d) ∈ D, we can "unfold" the corresponding sequence, C, checking t ≡ D,α d t ′ , into a sequence of distance steps, S, proving that t α,d t ′ . We proceed by induction on depth(t), as follows.

Let t i ≡ D,α di t i+1 be an intermediate step in the coinductive sequence C. If depth(t i ) = 0, we will trivially get t i α,di t i+1 . For depth(t) ≥ 1, we apply rule 3 in Def.8, getting

t i = t i 1 + at 1 ≡ D,α di t i 1 + at ′ 1 = t i+1 for (t 1 , t ′ 1 , d i /α) ∈ D. By a n 1 ba n-1 ba n-1 1 2 b 2 a n-2 . . . b n-1 a 1 2 n-1 b n ab n-1 1 a n a 2 b n-2 1 2 ab n-1 . . . a n 1 2 n-1 a n-1 b
Fig. 3. Arborescent presentation of the operational sequences induced by an α-ccd applying the induction hypothesis, we get t 1 α,di/α t ′ 1 , and using rules 4 and 3 in Def.7, we obtain the desired result

t i = t i 1 + at 1 α,di t i 1 + at ′ 1 = t i+1
. ⇐ | Given a sequence of distance steps, S, proving that t α,d t ′ , we can "fold" it into a coinductive sequence, C, checking t ≡ D,α d t ′ . For each (t, t ′ , d) ∈ D we consider the factorization of the sequence S and its reordering as done in Prop.6. We get t

= i∈I0 a i t i α,d i 02 i∈I0 a i t ′ i 1 α,d i 11 i∈I1 a i t i α,d i 12 i∈I1 a i t ′ i 1 α,d i 21 • • • α,d i (k+1)2 i∈I k+1 a i t ′ i = t ′ ,
2 ,1 ba n-1 1 1 2 ,1/2 b 2 a n-2 1 1 2 ,1/4 • • • 1 1 2 , 1 2 n-1
b n . If we preserve the structure of the sequences C n , whose unfolding produce these operational sequences, we can visualize them in a arborescent way -see Fig. 3-. The structure reminds that of B-trees, where we have nodes containing keys and pointers between them. The last give access to the elements in between the former that are located at nodes at "lower" levels. By means of the (inorder) traversing of the obtained tree we recover the original operational sequences. We are just "pushing the distance steps down" that correspond to "lower" levels, by introducing arcs that "move" the steps to the corresponding level. But whenever we have several steps in a row, that are not first level, then we group all of them introducing a single arc. We proceed in the same way down and down, introducing a "leaf" whenever we arrive to the level of a distance step, and new arcs going down, if there are other steps at the group at lower levels, either before or after the one which generated that leaf.

It is interesting to observe that we can also turn a n into b n in the opposite way, which means to use the same 1 2 -ccd, but a different sequence to check that it is indeed a 1 2 -ccd. We take now

C ′n := a n = aa n-1 ≡ D,1/2 1/2•2 ab n-1 ≡ D,1/2 1
bb n-1 = b n . Its unfolding produces the "symmetric" tree on the right of Fig. This is a more illustrative example of the general form of these arborescent presentations: we can have several "leaves" together with no arc in between them, when they correspond to several consecutive steps of the sequence at the current level. We can also have "degenerated" nodes, with a single arc down the tree, which corresponds to a subsequence of steps with none at the current level.

Even if Prop.7 only concerns finite trees, it reveals the duality between induction and coinduction, which is particularly interesting in the infinite case.

Example 11. Let us consider the tree a ∞ = unf old(N 1,∞ ), with N 1,∞ as in Ex.1. In an analogous way, we obtain the tree b ∞ . We have π n (a ∞ ) = a n , with a n as in Ex.9. Therefore, a ∞ can be seen as the limit of its projections, and as we had

a n ≡ 1/2 2 b n , we have also a ∞ ≡ 1/2 2 b ∞ . This can be proved by means of the (trivial!) collection D = {(a ∞ , b ∞ , 2)}. We can check that D is indeed an 1 2 -ccd using the sequence C := a ∞ = aa ∞ ≡ D,1/2 1 ba ∞ ≡ D,1/2 1 2 •2 bb ∞ = b ∞ .
Now, the (infinite!) "unfolding" of C would produce an infinite tree, that would "generate" an "infinite" operational sequence, which (intuitively) "converges" to b ∞ , and "gives" us the bound 2 for the distance between a ∞ and b ∞ . But our coinductive approach avoids the consideration of these limits. Moreover, the "traversing" of the arborescent presentations of the sequences, needed in many of our coinductive proofs, would produce "nested" infinite sequences much more difficult to cover without the coinductive approach.

Example 12. Let us take

A = {a, b, c, d} with d(a, b) = 4, d(c, d) = 1. We can prove ac ∞ +ad ∞ ≡ 1/2 6 bc ∞ +bd ∞ , using D = {(ac ∞ +ad ∞ , bc ∞ +bd ∞ , 6), (c ∞ , d ∞ ,
2)}, where the second triple in D is checked as in Ex.11; while for the first one we consider the coinductive sequence

C := ac ∞ + ad ∞ ≡ 1/2 1 ac ∞ + ac ∞ ≡ 1/2 0 ac ∞ ≡ 1/2 4 bc ∞ ≡ 1/2 0 bc ∞ + bc ∞ ≡ 1/2 1 bc ∞ + bd ∞ .
Anyway, out of the informal level (where it is quite useful!) and the finite case (where it is sound), we will avoid the use of this unfolding in our formal developments. However, the following definition formalizes the use of finite unfolding, getting a generalized characterization of the relations ≡ α d . It combines our two approaches (inductive, Def.7, and coinductive, Def.8,9) in a more flexible way; now operational steps can be used, not only at the first level of the trees, but also at any lower level. Definition 11. We consider the extension of the family of relations The (simple) proof of this result uses the fact that operational steps not at the first level of the trees, can be "hidden" into nested coinductive steps. However, their explicit use will produce in some cases much shorter and clearer proofs.

On the continuity of the global bisimulations distance

We have proved in Prop.7 the consistency between our inductive and coinductive definitions for finite trees. This can be turned into the limit by considering the coinductive definition and the (finite) projections of infinite processes.

We have included the superscripts (k) to indicate at which level we apply each transformation step. Each of these sequences can be obtained from the following one by removing the steps marked with (i + 1) and applying π i . Now, if we consider the operational sequences, S n , relating π n (t) and π n (t ′ ), for any n ∈ N, we obtain π n (t) 1 2 ,dn π n (t ′ ), for some d n < 6. For instance, we get π 1 (t) 1 2 ,4 π 1 (t ′ ), π 2 (t) 1 2 ,5 π 2 (t ′ ) and π 3 (t) 1 2 ,5.5 π 3 (t ′ ). The obtained distances form an increasing (but bounded) sequence, since each of the operational sequences expand the former ones, adding new costs caused by the (new) differences at the bottom levels.

Turning these operational sequences into coinductive ones, C n , as in Prop.7 we obtain the proof of π n (t) ≡ 1/2 6 π n (t ′ ), for all n ∈ N. Here, it is convenient to use the (same) value 6 at all the cases.

C 1 := a + a ≡ We expect that whenever we have π n (t) ≡ α d π n (t ′ ) ∀n ∈ N there will be a collection of uniform sequences proving these facts. For t, t ′ ∈ F T rees(A) with ||t|| n , ||t ′ || n ≤ l and t α,d t ′ , we should prove this by means of a sequence S that only uses intermediate trees t ′′ with ||t ′′ || n ≤ f (l, n), for a certain function f . But, the existence of such a uniform bound is still to be proved.

Conclusions and future work

We have presented a coinductive characterization of our global bisimulation distance, that previously we presented in an operational and an algebraic way. So, we extend our distance to the case of infinite trees without needing to introduce any complex notion of limit of our finite transformations generating the distances between finite trees. The coinductive approach makes the work in a much easier way. Our coinductive distances are always "sound" wrt the distances between their respective finite approximations. We expect that the "completeness" result, ending the proof of continuity, will also be true.

Besides the work devoted to complete the proof of the continuity theorem, now we are working in two complementary directions. On the one hand, we will try to apply our coinductive distance in order to define distances for testing, which should state how far away is a process to pass the tests imposed by any specification. On the other hand, we will continue the theoretical study of our coinductive distances. We consider that the results here are very promising, showing a new field of application of coinductive techniques into the study of the semantics of processes. We hope that much more will be shortly coming.

Fig. 1 .Definition 3 .

 13 Fig. 1. Labelled Transitions Systems and Trees used in Examples 1-2

  We consider domains of actions (A, d), where d : A×A → R + ∪{∞} is a distance between actions, with d(a, b) = d(b, a), ∀a, b ∈ A, and, as usual, d(a, b) = 0 ⇔ a = b, and d(a, c) + d(c, b) ≥ d(a, b), ∀a, b, c ∈ A where + is extended to R + ∪ {∞} as usual. Intuitively d(a, b) = ∞ expresses that two actions are absolutely not interchangeable. If the value of a distance d(a, b) is not specified in our examples, we will assume that d(a, b) = ∞.

Proposition 4 .

 4 If D is an α-ccd, then D * and D + are too.

Example 9 ./2 2 bD, 1 /2 1 ba n- 1 ≡D, 1 / 2 1/ 2 • 2

 921111222 Let us consider the family of trees {a n | n ∈ N}, defined by a 0 = 0 and a n+1 = aa n . We define b n in an analogous way. Now, if d(a, b) = 1, we have a n ≡ 1n ∀n ∈ N, using D = {(a n , b n , 2) | n ∈ N}, that is shown to be a 1 2 -ccd by considering 0=0 and the sequences C n := a n = aa n-1 ≡ bb n-1 = b n . Using the notion of unfolding above, we get the operational sequences S n := a n 1

1

 1

Fig. 4 .

 4 Fig. 4. Arborescent presentation of the operational sequence S in Ex.10

1 1 2 , 2 aac 1 12 ,10 bac 1 1 2 ,0 bac + bac 1 1 2 1 2 , 1

 122112111 3. Certainly, you can also recognize the reversibility of the operational sequences: by reading C ′n from right to left we recover C n , simply interchanging the roles of a and b. Example 10. Taking A = {a, b, c} with d(a, c) = 8, d(b, c) = 4 and d(a, b) = 10, we obtain aaa 1 2 ,13 ba(b + c) + bac, by means of the sequence S := aaa ,0 ba(c + c) + bac 1 ba(b + c) + bac. In Fig.4 we see its arborescent presentation whose folding generates the 1 2 -ccd D = {(aaa, ba(b + c) + bac, 13), (aaa, aac, 2), (aa, ac, 4), (a, c, 8), (bac + bac, ba(b + c) + bac, 1), (ac, a(b + c), 2), (c, (b + c), 4)}.

bbc

  + b, C 2 := ac + ad ≡ + bd, C 3 := acc + add ≡

  Finally, we define the family of global distance relationsα,d | d ∈ R + , taking t α,d t ′ ifthere exists a sequence S := t = t 0 1

	α,d1 t 1 1 α,d2 t 2 1 α,d3

1 α,d t ′ + t ′′ . 4. t 1 α,d t ′ ⇒ at 1 α,αd at ′ . We associate to each distance step its level, that is a natural number. The level of any step generated by 1. or 2. is one; while if the level of the corresponding premise t 1 α,d t ′ is k, then the level of a step generated by 3. (resp. 4.) is k (resp. k + 1).

  • • • 1 α,dn t n = t ′ , with n i=1 d i = d. Therefore, we can see any sequence of distance steps turning t into t ′ as a sequence of local transformations t i 1 α,di t i+1 . Each one of them either changes a single label or duplicates a partial branch at a certain level of t i . For technical reasons we want that t α,d t for any t, and all d ∈ R + . This can be obtained by considering the sequence S := t 1 α,d t + t 1 α,0 t. Although at the formal level we only work with the relations α,d , sometimes we also talk about the (global) distance defined by these bounds. Example 5. Let us consider again the systems in Ex.4. Now, it is immediate to check that t 1,1 t ′ j for all j ∈ {1 . . . 64}. Therefore, in this case, the global bisimulation distance between t and any t ′ j coincides with the classical bisimulation distance. However t 1,64 t ′ 1..64 , but we do not have t 1,d t ′ 1..64 for any d < 64: in order to transform t into t ′ 1..64 , we need to change each a i into a ′ i , paying one unit at each step. Instead, we had dist 1 d (t, t ′ 1.

	Remark 1.
	•	•	•	•
	a	b

  Corollary 1 (triangular-transitivity). For any discount factor α ∈ (0, 1], whenever we have t ≡ α d t ′ and t ′ ≡ α d ′ t ′′ , we also have t ≡ α d+d ′ t ′′ .Next, we state the relationship between our global bisimulation distance, bisimilarity and the classical bisimulation distance.Proposition 5. 1. For t, t ′ ∈ F yT rees(A), α ∈ (0, 1], we have t ∼ t ′ ⇔ t ≡ α 0 t ′ . 2.Our global bisimulation distance is greater or equal than the classical one. Corollary 2. The topology induced by our global bisimulation distance is strictly finer than that induced by the classical bisimulation distance. Proof. It is an immediate consequence of Prop.5.2 and the (counter)Ex.8. Taking R + as alphabet, and 2 i /k as labels of the edges of t N ′′′ , we obtain a family of trees {t k N ′′′ | k ∈ N}. Under the classical distance, any open ball centered in t N , contains infinitely many trees t k N ′′′ , but none of them is in any such ball for our global distance. ⊓ ⊔ Our coinductive definition of the global bisimulation distance generalizes our operational definition for finite trees.

	Lemma 1. Any sequence S producing t	α,d t ′ can be "factorized" into an
	"structured" sequence

  where for each sequence

	i∈Ij a i t i	α,d i j2	i∈Ij a i t ′ i and each i ∈ I j , we have t i	α,d i j2 /α t ′ i with
	i∈Ij d i j2 = d j2 . Now, applying the induction hypothesis, we have (t i , t ′ i , d i j2 /α) ∈
	D, for all i ∈ I j , so that	a i t i ≡ D,α αd1	a i t 1 i ≡ D,α αd2	a i t 2 i ≡ D,α αd3 • • • ≡ D,α αd |I j |
	a i t Therefore, each sequence i∈Ij a i t i |Ij | i = a i t ′ i .	α,d i j2	i∈Ij a i t ′ i at the factorization
	above can be substituted by a sequence of |I j | valid coinductive steps, getting a
	total distance k+1 j=0	i∈Ij d i j1 + k+1 j=0	|Ij | k=1 αd k = d.
					⊓ ⊔
	Next, a pair of examples to illustrate the unfolding and folding procedures.

  For all (t, t ′ , d) ∈ D we have ( j∈J a j t j ) + at ≡ ( j∈J a j t j ) + at ′ . Now, we can proceed exactly as in Def.9, using the relations ≡

	1 α,d | d ∈ i , d D,α R + in Def.7 to FyTrees(A). Now, given a family D = {(t i , t ′ d , by:
	1. t 1 α,d t ′ implies t ≡	D,α d t ′ .
	2. D,α α•d D,α d ≡ D,α d , getting the family of relations ≡	instead of

i ) | i ∈ I} with t i , t ′ i ∈ F yT

rees(A) and d i ∈ R + , we define the family of relations ≡ α d . Proposition 8. For all d ∈ R + , α ∈ (0, 1], the relations ≡ α d and ≡ α d are equal.

Therefore, lts's are just arc-labelled graphs, or more formally coalgebras succ : N → LT S(N, A) of the functor LT S(N, A) := P(A × N ) on the plain category of sets, Set. See for instance[START_REF] Jacobs | Introduction to coalgebra. towards mathematics of states and observations[END_REF][START_REF] Sangiorgi | Advanced topics in bisimulation and coinduction[END_REF] for much more on coalgebras.

⋆ Partially supported by the Spanish projects STRONGSOFT (TIN2012-39391-C04-04) and PROMETIDOS S2009/TIC-1465.

Proposition 9. For any α-ccd D, the projected family π(D) = {(π n (t), π n (t ′ ), d) | (t, t ′ , d) ∈ D, n ∈ N} is an α-ccd that proves t ≡ α d t ′ ⇒ ∀n ∈ N π n (t) ≡ α d π n (t ′ ).

Proof. Let C := t = t 0 ≡ D,α d1 . . . ≡ D,α d k t k = t ′ be the sequence proving that (t, t ′ , d) ∈ D satisfies the condition in order D to be an α-ccd. Then each projected sequence

satisfies the condition in order π(D) to be an α-ccd. It is clear that the projection under π n of any first level step in C, is also a valid step in π n (C). Moreover, any coinductive step in C using (t 1 , t ′ 1 , d) ∈ D, can be substituted by the corresponding projected step, that uses

We conjecture that the converse of Prop.9 asserting the continuity of our coinductive distance, is also true. Unfortunately, the proof of this result is being much more complicated than we expected. Our idea, is to use the reasoning in the proof of Prop.9 in the opposite direction and the correspondence between operational and coinductive sequences in the finite case. As far as we have a collection of "uniform" 2 operational sequences S n := π n (t) α,d π n (t ′ ), we could "overlap" all of them getting an infinite tree as that in Fig. 3. By "folding" this tree we obtain the coinductive sequence C, proving t ≡ α d t ′ . Next we provide a simple example.

Example 14. Let us consider the trees t = ac ∞ + ad ∞ and t ′ = bc ∞ + bd ∞ , as in Ex.12, and the same distance d as there. Then we have: 2 Uniformity here means that for any n, k ∈ N with k ≥ n the steps of all the sequences S k corresponding to the first n-levels are always the same.


Antoine Marnat
email: marnat@math.unistra.fr

There is no analogue to Jarník's relation for twisted Diophantine approximation

Keywords: twisted Diophantine approximation, Simultaneous approximation, Jarník's relation Mathematics Subject Classification (2010) 11J13

Jarník gave a relation between the two most classical uniform exponents of Diophantine approximation in dimension 2. In this paper we consider a twisted case, between the classical and the multiplicative one, and we show that no analogue to Jarník's relation holds.

Introduction and main result

Given θ = (θ 1 , θ 2 ) with 1, θ 1 , θ 2 linearly independent over Q, the exponent ω(θ) (resp. the uniform exponent ω(θ)) is defined as the supremum of the real numbers ν such that for arbitrarily large real number H (resp. for every sufficiently large real number H) the system of inequalities

0 < |q -p 1 θ 1 -p 2 θ 2 | ≤ H -ν , |p 1 | ≤ H , |p 2 | ≤ H
has an integer solution (p 1 , p 2 , q). On the other hand, the exponent λ(θ) (resp. the uniform exponent λ(θ)) is the supremum of the real numbers ν such that for arbitrarily large real number H (resp. for every sufficiently large real number H) the system of inequalities

0 < |q| ≤ H, |qθ 1 -p 1 | ≤ H -ν , |qθ 2 -p 2 | ≤ H -ν
1 has an integer solution (p 1 , p 2 , q). Dirichlet's box principle (or Minkowski's first convex body theorem) provides the lower bounds ω(θ) ≥ ω(θ) ≥ 2 and λ(θ) ≥ λ(θ) ≥ 1 2 .

The first result is Jarník's relation [START_REF] Jarník | Zum khintchineschen "Übertragungssatz[END_REF] linking both uniform exponents:

Theorem 1 [START_REF] Jarník | Zum khintchineschen "Übertragungssatz[END_REF]. For any pair of real numbers θ = (θ 1 , θ 2 ) with 1, θ 1 , θ 2 linearly independent over Q, both uniform exponents satisfy the relation

λ(θ) + 1 ω(θ) = 1. ( * )
Recently, Laurent [START_REF] Laurent | Exponents of diophantine approximmation in dimension two[END_REF] proved a theorem giving every possible value of the quadruple Ω(θ) = (ω(θ), λ(θ), ω(θ), λ(θ)) when θ ranges over R n such that 1, θ 1 , θ 2 are Q-linearly independent, called spectrum.

Theorem 2 [START_REF] Laurent | Exponents of diophantine approximmation in dimension two[END_REF]. For any pair of real numbers θ = (θ 1 , θ 2 ) with 1, θ 1 , θ 2 linearly independent over Q the four exponents of Diophantine approximation satisfy the relations 2 ≤ ω(θ) ≤ +∞, λ(θ) + 1 ω(θ) = 1, ω(θ)(ω(θ)-1) ω(θ)+ω(θ) ≤ λ(θ) ≤ ω(θ)-(ω(θ) -1) ω(θ)

.

Conversely, for each quadruple ω, ω, λ, λ satisfying

2 ≤ ω ≤ +∞, λ + 1 ω = 1, ω(ω-1) ω+ω ≤ λ ≤ ω-(ω-1) ω ,
there exists a pair of real numbers θ

= (θ 1 , θ 2 ) with 1, θ 1 , θ 2 linearly independent over Q with ω(θ) = ω, λ(θ) = λ, ω(θ) = ω, λ(θ) = λ.
In [START_REF] Jarník | Zum khintchineschen "Übertragungssatz[END_REF], Jarník noticed that there is no analogue to relation ( * ) in higher dimension. It is an open question to find an analogue to Jarník's relation in the multiplicative case, recently studied by German [START_REF] German | Transference inequalities for multiplicative Diophantine exponents[END_REF].

Given θ = (θ 1 , θ 2 ) with 1, θ 1 , θ 2 linearly independent over Q, the multiplicative exponent ω × (θ) (resp. the uniform multiplicative exponent ω× (θ)) is defined as the supremum of the real numbers ν such that for arbitrarily large real number H (resp. for every sufficiently large real number H) the system of inequalities

0 < |q -p 1 θ 1 -p 2 θ 2 | ≤ H -ν , max(1, |p 1 |) max(1, |p 2 |) ≤ H 2
has an integer solution (p 1 , p 2 , q). On the other hand, the multiplicative exponent λ × (θ) (resp. the uniform multiplicative exponent λ× (θ)) is the supremum of the real numbers ν such that for arbitrarily large real number H (resp. for every sufficiently large real number H) the system of inequalities

0 < |q| ≤ H, |qθ 1 -p 1 | • |qθ 2 -p 2 | ≤ H -2ν
has an integer solution (p 1 , p 2 , q). Minkowski's first convex body theorem [START_REF] Minkowski | Geometrie der Zahlen[END_REF] provides the lower bounds

ω × (θ) ≥ ω× (θ) ≥ 2 and λ × (θ) ≥ λ× (θ) ≥ 1 2 .
We observe that

{x, y ∈ R | max(1, |x|) max(1, |y|) ≤ H 2 } = ∪ 0≤i≤1 {x, y ∈ R | |x| ≤ H 2i , |y| ≤ H 2(1-i) },
where we have a union of uncountably many sets. It is thus natural to consider the following twisted exponents. See the paper of Harrap [START_REF] Harrap | Twisted inhomogeneous Diophantine approximation and badly approximable sets[END_REF] for further twisted Diophantine approximation.

Given θ = (θ 1 , θ 2 ) with 1, θ 1 , θ 2 linearly independent over Q, and i, j non negative real numbers with i + j = 1, the twisted exponent ω i,j (θ) (resp. the uniform twisted exponent ωi,j (θ)) is defined as the supremum of the real numbers ν such that for arbitrarily large real number H (resp. for every sufficiently large real number H) the system of inequalities

0 < |q -p 1 θ 1 -p 2 θ 2 | ≤ H -ν , |p 1 | ≤ H 2i , |p 2 | ≤ H 2j
has an integer solution (p 1 , p 2 , q) with (p 1 , p 2 ) = (0, 0).

On the other hand, the twisted exponent λ i,j (θ) (resp. the uniform twisted exponent λi,j (θ)) is the supremum of the real numbers ν such that for arbitrarily large real number H (resp. for every sufficiently large real number H) the system of inequalities

0 < |q| ≤ H, |qθ 1 -p 1 | ≤ H -2iν , |qθ 2 -p 2 | ≤ H -2jν
has an integer solution (p 1 , p 2 , q). Again, Minkowski's first convex body theorem [START_REF] Minkowski | Geometrie der Zahlen[END_REF] provides the lower bounds ω i,j (θ) ≥ ωi,j (θ) ≥ 2 and λ i,j (θ) ≥ λi,j (θ) ≥ 1 2 .

In his PhD thesis, the author gives relations analogue to those of Theorem 2 in the twisted case. At present, there is no construction proving that these relations are best possible.

The goal of this paper is to show that there is no analogue to Jarník's relation in the twisted case. We first need to introduce the following notion.

Fix two real numbers R > 1 and µ > 1, we call (µ, R)-sequences a pair of sequences of positive integers (A n ) n≥1 and (B n ) n≥1 satisfying the following properties:

(i) There exist disjoint finite non-empty sets of prime numbers S and T such that, for each n ≥ 1, the set S contains all the prime factors of A n and the set T contains all the prime factors of B n .

(ii) For each p ∈ S and q ∈ T , the sequence (ν p (A n )) n≥1 and (ν q (B n )) n≥1 are strictly increasing sequences of positive integers.

(iii) We have

lim n→+∞ log(A n+1 ) log(A n ) = lim n→+∞ log(B n+1 ) log(B n ) = µ and lim n→+∞ log(B n ) log(A n ) = R.
For fixed R > 1 and µ > 1 and any choice of S and T , one can construct such sequences. For example, suppose that S = {p 1 , . . . , p k } and T = {q 1 , . . . , q l }, where p 1 , . . . , p k , q 1 , . . . , q l are distinct prime numbers.

Setting P = p 1 p 2 • • • p k and Q = q 1 q 2 • • • q l , we consider A n = P aµ n log Q and B n = Q aµ n R log P ,
where x is the integer part of the real number x. Then the sequences (A n ) n≥1 and (B n ) n≥1 form a pair of (µ, R)-sequences, provided that the real parameter a is large enough to ensure property (ii). Theorem 3. Let i, j be two non negative real numbers with i ≥ j and i + j = 1. Fix two real numbers µ and R satisfying the conditions:

µ > 2, R < j(µ -2), R > µ µ -2 and R > µ i(µ -1) . ( 1
)
For any (µ, R)-sequences (A n ) n≥1 and (B n ) n≥1 , we consider the pair of real numbers

θ = (θ 1 , θ 2 ) =   n≥1 A -1 n , n≥1 B -1 n   .
Its twisted exponents satisfy

ωi,j (θ) = min 2j µ -1 R , 2i µ -1 µ R , λi,j (θ) = min 1 2i (1 - R µ -1 ), 1 2j (1 - µ (µ -1)R ) , ω i,j (θ) = 2i(µ -1).
Hence, for any (µ, R)-sequences, one gets a point θ. Theorem 3 then computes the three exponents ωi,j (θ), λi,j (θ) and ω i,j (θ) for each i, j for which (1) holds.

Note that in the case

i = j = 1/2, one gets ω(θ) = min µ -1 R , µ -1 µ R , λ(θ) = min 1 - R µ -1 , 1 - µ (µ -1)R ,
which agrees with Jarník's relation ( * ).

With a suitable choice of the parameters µ and R, we can deduce the following theorem as a corollary. Theorem 4. Let i, j be two non negative real numbers with i > j and i + j = 1. Let ŵ be a real number with ŵ > 6i and

λ ∈ 1 2i 1 - 2j ŵ , min 1 2i , 1 2j 1 - 2i ŵ .
There exists uncountably many θ such that ωi,j (θ) = ŵ and λi,j (θ) = λ.

Thus, no analogue to Jarník's relation holds for the twisted Diophantine approximation. It is still an open question to find the optimal interval for λi,j (θ).

Sequence of minimal points and proof of Theorems 3 and 4

The main tool to compute the exponents of Diophantine approximation and prove Theorem 3 is the notion of minimal points, as introduced by Davenport and Schmidt in [1, §3] or Jarník in [START_REF] Jarník | Zum khintchineschen "Übertragungssatz[END_REF].

Let L and N be two functions from Z l to R + where l is a positive integer.

Definition. A sequence of (L, N )-minimal points (M k ) k≥0 ∈ (Z l ) N is a sequence such that (i) (N (M k )) k≥0 is an increasing sequence with N (M 0 ) ≥ 1 , (ii) (L(M k )) k≥0 is a decreasing sequence with L(M 0 ) ≤ 1, (iii) for every k ≥ 0 and every point M ∈ Z l , if N (M ) < N (M k+1 ) then L(M ) ≥ L(M k ).
We can normalize any functions L and N to satisfy the conditions N (M 0 ) ≥ 1 and L(M 0 ) ≤ 1. These conditions are not restrictive. They are imposed to simplify the further use of minimal points. Note that there is no unicity, because there may exist

M k and M k such that L(M k ) = L(M k ) and N (M k ) = N (M k ) but M k = M k .
Let x = (x 0 , x 1 , x 1 ) be an integer triple. Consider the following functions with parameters i, j and θ

L λ (x) = max |x 0 θ 1 -x 1 | 1/(2i) , |x 0 θ 2 -x 2 | 1/(2j) , N λ (x) = |x 0 |, L ω (x) = |x 1 θ 1 + x 2 θ 2 -x 0 |, N ω (x) = max |x 1 | 1/(2i) , |x 2 | 1/(2j) ,
where |x| is the absolute value of the real number x. They are related to the twisted exponents through the following proposition.

Proposition 1. Let θ = (θ 1 , θ 2 ) be a pair of real numbers and 0 < j ≤ i < 1 such that i + j = 1. Let (a n ) n≥1 (resp. (b n ) n≥1 ) be a sequence of (L λ , N λ )-minimal points of θ (resp. (L ω , N ω )-minimal points). We have the relations λi,j (θ) = lim inf n→∞ -log L λ (an) log N λ (a n+1 ) , λ i,j (θ) = lim sup n→∞ -log L λ (an) log N λ (an) , ωi,j (θ) = lim inf n→∞ -log Lω(bn) log Nω(b n+1 ) , ω i,j (θ) = lim sup n→∞ -log Lω(bn) log Nω(bn) .
We omit the proof of Proposition 1. It is an easy consequence of the definitions of a sequence of minimal points and of the twisted exponents. This proposition gives us the exact values of the two uniform exponents if we have enough information about the tail of a sequence of minimal points, since only the asymptotic behavior is significant. From now on, every statement is implicitly considered for sufficiently large n.

For every (µ, R)-sequences (A n ) n≥1 and (B n ) n≥1 with µ and R satisfying the conditions (1) from Theorem 3, we set θ

= (θ 1 , θ 2 ) = n≥1 A -1 n , n≥1 B -1 n .
We also set for every integer n ≥ 1 the integers

A n = n k=1 A n A -1 k and B n = n k=1 B n B -1 k . ( 2
)
With this notation, we have Lemma 1. Under the assumption of Theorem 3, the sequence of primitive integer points

(A 1 , A 1 , 0), (B 1 , 0, B 1 ), . . . , (A n , A n , 0), (B n , 0, B n ), (A n+1 , A n+1 , 0), . . . ( 3
)
consists ultimately of a sequence of (L ω , N ω )-minimal points.

Lemma 2. Under the assumption of Theorem 3, consider

C n = (A n B n , A n B n , A n B n ) and D n = (A n+1 B n , A n+1 B n , A n+1 B n ).
Ultimately, C n and D n consist in (L λ , N λ )-minimal points . We denote by E n,1 , . . . , E n,sn (resp. F n,1 , . . . , F n,tn ) the intermediate

(L λ , N λ )-minimal points between C n = E n,0 and D n = E n,sn+1 (resp. D n = F n,0 and C n+1 = F n,tn+1 ). For 0 ≤ k ≤ s n and 0 ≤ k ≤ t n , the intermediate (L λ , N λ )-minimal points are of the shape E n,k = E n,k,0 , E n,k,1 , E n,k,0 B n B n , F n,k = F n,k ,0 , F n,k ,0 A n A n , F n,k ,2 .
Furthermore, they satisfy

L λ (F n,k ) = F n,k,0 θ 2 1 2j ( 1 N λ (F n,k+1 ) A n+1 ) 1 2j , N λ (F n,1 ) B n+1 Bn , L λ (E n,k ) = E n,k,0 θ 1 1 2i ( 1 N λ (E n,k+1 ) B n ) 1 2i , N λ (E n,1 ) A n+1
An , where x denotes the distance from the real number x to a nearest integer.

Lemmas 1 and 2 will be proved in Section 3. We show now how Theorem 3 and 4 can be derived from Proposition 1 and Lemmas 1 and 2.

Proof of Theorem 3.

First, notice that

|A n θ 1 -A n | |A n A -1 n+1 | and |B n θ 2 -B n | |B n B -1 n+1 |.
Using Proposition 1, we can thus compute ωi,j (θ) = min

  lim inf n→∞ -log |A n -A n θ 1 | log |B n | 1 2j , lim inf n→∞ -log |B n -B n θ 2 | log |A n+1 | 1 2i   = min 2j lim inf n→∞ log A n+1 -log A n log B n , 2i lim inf n→∞ log B n+1 -log B n log A n+1 = min 2j µ -1 R , 2i µ -1 µ R , λi,j (θ) = min lim inf n→∞ min 0≤k≤sn - log L λ (E n,k ) log N λ (E n,k+1 ) , lim inf n→∞ min 0≤k≤tn - log L λ (F n,k ) log N λ (F n,k+1 ) = min lim inf n→∞ min 0≤k≤sn 1 2i 1 - log B n log E n,k+1,0 lim inf n→∞ min 0≤k≤tn 1 2j 1 - log A n+1 log F n,k+1,0 , = min lim inf n→∞ 1 2i 1 - log B n log E n,1,0 , lim inf n→∞ 1 2j 1 - log A n+1 log F n,1,0 = min 1 2i 1 - R µ -1 , 1 2j 1 - µ (µ -1)R , ω i,j (θ) = max   lim sup n→∞ -log |A n -A n θ 1 | log |A n | 1 2j , lim sup n→∞ -log |B n -B n θ 2 | log |B n | 1 2i   = max 2j lim sup n→∞ log A n+1 -log A n log |A n | , 2i lim sup n→∞ log B n+1 -log B n log |B n | = max (2j(µ -1), 2i(µ -1)) = 2i(µ -1).
This completes the proof of Theorem 3.

Proof of Theorem 4.

Theorem 4 is a corollary from Theorem 3 if we choose the parameters from the following proposition Proposition 2. For every ω > 6i, the parameters

R ∈   ω 2i , ω 2i 1 + 1 + 16ij ω2 2   , µ = 2iR 2iR - ω .
satisfy the conditions (1) from Theorem 3.

The key point is to notice that

R ∈   ω 2i , ω 2i 1 + 1 + 16ij ω2 2   is equivalent to 0 < R(2iR -ω) < 2j.
With the choices of the Proposition 2, we have ωi,j (θ) = min 2j

µ -1 R , 2i µ -1 µ R = min 2j ω R(2iR -ω) , ω = ω, λi,j (θ) = min 1 2i 1 - R(2iR -ω) ω , 1 2j 1 - 2i ω ∈ 1 2i 1 - 2j ω , min 1 2i , 1 2j 1 - 2i ω .
To get uncountably many pairs θ with given exponents, note that Theorem 3 also holds for

θ = (θ 1 , θ 2 ) =   n≥1 ε n A -1 n , n≥1 ε n B -1 n   ,
where ε n and ε n are ±1. In this case we define

A n = n k=1 ε n A n ε k A -1 k and B n = n k=1 ε n B n ε k B -1 k .

Proof of the lemmas on minimal points

First of all, observe that in the definition of (µ, R)-sequences, the condition (ii) on the disjointness of the sets S and T of prime numbers ensures that for every

n ≥ 1, gcd(A n , B n ) = gcd(A n , A n ) = gcd(B n , B n ) = 1,
where A n and B n are given by ( 2). This ensures that the terms in the sequences in Lemmas 1 and 2 are primitive points.

Proof of Lemma 1 .

Since R > 1 and i ≥ j we have

|A n | 1 2i < |B n | 1 2j . Furthermore, the condition R < j(µ -2) from (1) implies that µ R > i j . This implies that |B n | 1 2j < |A n+1 | 1 2i
. Thus, the sequence (3) is increasing with respect to N ω . To prove that it consists ultimately of consecutive (L ω , N ω )-minimal points , it is enough to show that, if n is large enough, there is no primitive integer point x = (x 0 , x 1 , x 2 ) either with

N ω (x) = max{|x 1 | 1 2i , |x 2 | 1 2j } < B 1 2j n and L ω (x) = |x 0 -x 1 θ 1 -x 2 θ 2 | < |A n -A n θ 1 |, (4) or with
N ω (x) = max{|x 1 | 1 2i , |x 2 | 1 2j } < A 1 2i n+1 and L ω (x) = |x 0 -x 1 θ 1 -x 2 θ 2 | < |B n -B n θ 2 |.
(5) Assuming that there is a primitive point (x 0 , x 1 , x 2 ) satisfying (4), one finds

A n B n x 0 -A n B n x 1 -A n B n x 2 = A n B n (x 0 -x 1 θ 1 -x 2 θ 2 ) -B n (A n -A n θ 1 )x 1 -A n (B n -B n θ 2 )x 2 (6)
The left hand side of this equality is an integer. If it is 0, then B n divides A n B n x 2 , thus B n divides x 2 and so x 2 = 0 because of the hypothesis

|x 2 | < B n . Thus we obtain A n x 0 -A n x 1 = 0. As x is a primitive point, this implies that (x 0 , x 1 ) = ±(A n , A n ) and so |x 0 -x 1 θ 1 -x 2 θ 2 | = |A n -A n θ 1 |
contrary to the hypothesis. So the left hand side of (6) has absolute value at least 1 and thus

1 ≤ A n B n |A n -A n θ 1 | + B n |A n -A n θ 1 ||x 1 | + A n |B n -B n θ 2 ||x 2 | A 2 n A -1 n+1 B n + A n A -1 n+1 B 1+i/j n + A n B 2 n B -1 n+1 , because |A n -A n θ 1 | ≤ 2 A n A n+1 and |B n -B n θ 2 | ≤ 2 B n B n+1 .
We obtain a contradiction by showing that the three summands in the last expression above tend to zero as n goes to infinity. First, R < µ -2 implies that

R + 2 -µ = lim n→∞ 2 log A n + log B n -log A n+1 log A n = -ρ 1 < 0. That is, A 2 n A -1 n+1 B n ∼ n→∞ A -ρ 1 n → n→∞ 0.
Then, R < j(µ -1) implies that

R + j(1 -µ) = lim n→∞ j log A n + log B n -j log A n+1 log A n = -ρ 2 < 0.
That is,

A n A -1 n+1 B 1/j n ∼ n→∞ A -ρ 2 /j n → n→∞ 0. Finally, (µ -2)R > 1 implies that R(µ -2) -1 = lim n→∞ log A n + 2 log B n -log B n+1 -log A n = ρ 3 > 0. That is, A n B 2 n B -1 n+1 ∼ n→∞ A -ρ 3 n → n→∞ 0.
Similarly, if the condition (5) has a solution (x 0 , x 1 , x 2 ), A n+1 can not divide x 1 and we deduce the lower bound

1 ≤ A n+1 B n |B n -B n θ 1 | + B n |A n+1 -A n+1 θ 1 ||x 1 | + A n+1 |B n -B n θ 2 ||x 2 | B 2 n B -1 n+1 A n+1 + B n A 2 n+1 A -1 n+2 + A 1+j/i n+1 B n B -1 n+1 .
Again, the three summands in this expression tend to zero as n goes to infinity because R(µ -2) > µ, R < µ(µ -2) and R(µ -1) > µ i according to [START_REF] Davenport | Approximation to real numbers by algebraic integers[END_REF]. Thus, we proved Lemma 1.

Proof of Lemma 2.

First, we show that ultimately the point C n and D n are (L λ , N λ )-minimal points, then we prove the properties of the (L λ , N λ )-minimal points lying respectively between C n and D n and D n and C n+1 .

Since A n+1 > A n and B n+1 > B n by the property about valuations of (µ, R)sequences, the sequence

C 1 , D 1 , . . . , C n , D n , C n+1 , . . . is a non zero integer multiple of (B n , B n ). Thus, D n is a (L λ , N λ )-minimal point. Consider any (L λ , N λ )-minimal point x = (x 0 , x 1 , x 2 ) ∈ Z 3 with N λ (C n ) ≤ x 0 < N λ (D n ).
We claim that for n large enough, we have

L λ (x) = |x 0 θ 1 -x 1 | 1/(2i) .
Indeed, for such x, recall that (x 0 , x 2 ) is an integer multiple of (B n , B n ). Since x 0 is strictly less than A n+1 B n and B n and A n+1 are coprime, the points (x 0 , x 1 ) and (A n+1 , A n+1 ) are linearly independent. Thus we have

1 ≤ det x 0 x 1 A n+1 A n+1 ≤ |x 0 ||A n+1 -A n+1 θ 1 | + A n+1 |x 1 -θ 1 x 0 |.
This provides

|x 1 -θ 1 x 0 | 1 A n+1 , ( 10
) because R > µ(µ -2) implies for sufficiently large n |x 0 ||A n+1 -A n+1 θ 1 | ≤ A 2 n+1 B n A -1 n+2 ≤ 1 2 .
Furthermore,

|x 2 -θ 2 x 0 | = x 0 B n |B n θ 2 -B n | A n+1 B n B n+1 . ( 11
)
Finally, the condition R > µ i(µ-1) implies that . Hence the result.

Let E n,0 = C n , E n,1 , . . . , E n,sn , E n,sn+1 = D n denote a sequence of (L λ , N λ )minimal points, chosen with positive first coordinate. Suppose that n is large enough, by the above each E n,k has the form

E n,k = E n,k,0 , E n,k,1 , E n,k,0 B n B n where E n,k,0 B n ∈ N * (0 ≤ k ≤ s n + 1), and we have L λ (E n,k ) 2i = |E n,k,0 θ 1 -E n,k,1 | for k = 0, . . . , s n but not for k = s n + 1.
We now show that

B n 2N λ (E n,k+1 ) ≤ L λ (E n,k ) 2i ≤ B n N λ (E n,k+1 )
. By Minkowski's first convex body theorem, for each real number H > 0, there exists a non-zero integer point (x 0 , x 1 ) satisfying the three conditions

B n | x 0 , |x 0 | ≤ H and |x 0 θ 1 -x 1 | ≤ B n H .
For n large enough, fix k ∈ {1, . . . , s n } and choose H in the range

N λ (E n,k ) < H < N λ (E n,k+1 ),
then we get a non-zero integer point x = (x 0 , x 1 , x 2 ) where x 0 and x 1 are given by Minkowski's theorem and x 2 = x 0 B -1 n B n . This point satisfies

N λ (E n,k ) < N λ (x) < N λ (E n,k+1 )
and the conditions (10) and (11). So,

L λ (x) 2i = |x 0 θ 1 -x 1 | ≤ B n H .
By definition of (L λ , N λ )-minimal points, we have L λ (E n,k ) < L λ (x). Thus, by letting H tend to E n,k+1,0 we get the upper bound

L λ (E n,k ) 2i ≤ B n N λ (E n,k+1
) .

For the lower bound, notice that B n divides E n,k,0 and E n,k+1,0 , and that two consecutive (L λ , N λ )-minimal points are independent. Thus

B n ≤ det E n,k,0 E n,k,1 E n,k+1,0 E n,k+1,1 ≤ E n,k,0 |E n,k+1,1 -θ 1 E n,k+1,0 | + E n,k+1,0 |E n,k,1 -E n,k,0 θ 1 |, ≤ 2E n,k+1,0 |E n,k,1 -E n,k,0 θ 1 |.
So,

L λ (E n,k ) 2i ≥ B n 2N λ (E n,k+1
) .

In particular, since E 0 = C n we have

N λ (E n,1 ) B n L λ (C n ) 2i B n A n A -1 n+1 B n A n+1 A n .
Similarly, we show that for n large enough, any (L λ , N λ )-minimal point x = (x 0 , x 1 , x 2 ) with N λ (D n ) ≤ N λ (x) < N λ (C n+1 ) has L λ (x) = |x 0 θ 2 -x 2 | 1/(2j) , 14 and that the intermediate (L λ , N λ )-minimal points F n,k = (F n,k,0 , F n,k,0

A n+1 A n+1 , F n,k,2 ) satisfy A n+1 2N λ (F n,k+1 ) ≤ L λ (F n,k ) 2j ≤ A n+1 N λ (F n,k+1
) . via Minkowski's first convex body theorem and consideration on a good determinant.

This completes the proof of Lemma 2.

Notation:

  Given two sequences (a n ) n≥1 and (b n ) n≥1 , we write a n b n (resp. a n b n ) if, for sufficiently large n, there exists a real number c 1 such that a n ≥ c 1 b n (resp. there exists a real number c 2 such that a n ≤ c 2 b n ). Finally, we write a n b n if both a n b n and a n b n .

is strictly increasing with respect to N λ . Note that, if n is large enough

n+1 B n and we have j ≤ i.

Suppose that a non-zero integer point x = (x 0 , x 1 , x 2 ) satisfies

We have the integer determinant

n+1 tends to zero as n goes to infinity. Since R < j(µ -1) and

, it follows that B n L λ (C n ) 2j tends to zero as well. Thus, if n is large enough, the determinant in (8) is zero. Then, (x 0 , x 2 ) is a non-zero integral multiple of (B n , B n ), in particular B n divides x 0 . Consider the integer determinant, for x = (x 0 , x 1 , x 2 ) with the stronger assumption that

(9) Since R < µ -2 summands tend to zero as n goes to infinity. Thus for sufficiently large n, the determinant in (9) is zero. Then, (x 0 , x 1 ) is a non-zero integral multiple of (A n , A n ), in particular A n divides x 0 . Since A n and B n are coprime,

Similarly, if a non-zero integer point x = (x 0 , x 1 , x 2 ) satisfies

and if n is large enough, then (x 0 , x 1 ) is a non-zero integral multiple of (A n+1 , A n+1 ) and if we strengthen the condition to N λ (x) ≤ N λ (D n ) = A n+1 B n , then (x 0 , x 2 )


Collence Chisita

Blessing Chiparaushe

Steering and strengthening knowledge economy through Open Access initiatives: Case of Zimbabwe By

Keywords: Collence Chisita, Blessing Chiparaushe. Steering and strengthening knowledge economy through Open Access initiatives: open access, knowledge coordination and local e-content, digital literacy 1 Collence. Takaingenhamo Chisita

Steering and strengthening knowledge economy through Open Access initiatives

Collence Chisita, Blessing Chiparaushe

Introduction

The teaching, learning and research landscape in Zimbabwe's Higher and Tertiary education is experiencing seismic transition due to innovative disruptions induced by the proliferation and ICTs and the need to maintain high standards . Emerging technologies are making it to democratise and leverage institutional intellectual content for the benefit of teaching, research and learning. [START_REF] Copeland | Electronic Theses and Dissertations: promoting hidden research[END_REF] states that globally there are frantic efforts to promote "open access" as evidenced by the thrust towards IRs providing access to ETDs.

In Zimbabwe the principal shape of OA expression is the Institutional Repository (IR), followed by the OA journal (Nyambi, 2010). The IR wave has also swept through Zimbabwe academic landscape with all fifteen (15) universities having developed one using Free Open Source Software such as DSpace and Greenstone. Academic libraries are taking advantage of the proliferation of modern technologies to leverage their content as strategy to contribute towards realisation of institutional goals as well as enhancing visibility. This has seen institutions developing ETD repositories. ETD refers to a master's thesis or doctoral dissertation that is archived and circulated electronically rather than in print and bound format [START_REF] Goodfellow | Electronic theses and dissertations: a review of this valuable resource for nurse scholars worldwide[END_REF]. Easier and convenient access to scientific information will ultimately help to deepen and widen access to information.

Open access as a publishing philosophy dates back to the last decade of the twentieth century.

Frustration over ever escalating publisher prices and stringent terms combined with expanding digital distribution capabilities led to a multifaceted strategy. It includes new business models, institutional policies, national and granting agency requirements, self publishing and author retention of rights among others. But open access has not displaced the publisher monopoly [START_REF]Supporting and enhancing Scholarship in the digital age: Role of Open access Institutional repositories[END_REF]. Scholars want their work to be more broadly read, but also must publish in high impact journals and with prestigious publishers in order to advance their careers. The beginning of the Open access initiative is attributed to the continued phenomenal increase in the cost of subscription to scholarly journals especially in science and medicine vis-à-vis diminishing library budgets thus rendering libraries incapable of satisfying the information demands of users.

The market share of monopoly capitalism has seen 50% of scholarly publications being controlled by a group of five publishers thus making it difficult for libraries, researchers and scientists failing to meet subscriptions to the scholarly literature they needed for research and teaching [START_REF]Supporting and enhancing Scholarship in the digital age: Role of Open access Institutional repositories[END_REF]. Upon realising this unfair global knowledge divide, Africa and the Global South have come together to push for equitable production and sharing of information on the global village hence the promulgation of the Dakar Declaration on Open Access in April 2016 (CODESRIA 2016). [START_REF] Macdonald | These five companies control more than half of academic publishing: That is why we are still paying for knowledge[END_REF] argues that predatory, oligopolistic and monopolistic tendencies in the publishing industry are counter-productive to scientists and researchers who need to advance knowledge. This is why ETDs have been welcomed and now deeply rooted in the scholarly ambience of academic institutions in Zimbabwe.

There is a sharp contrast between developed and developing countries with regards to the knowledge economy, for example, the former has a rich networked information/knowledge economy characterised by a robust ICT Infrastructure, high volumes of knowledge generation, networking and use, while the latter has an emaciated information economy consisting of a high number of consumers or downloaders relying on the core to satisfy information needs [START_REF] Benkler | The Wealth of Networks: How Social Production Transforms Markets and Freedom[END_REF].

Furthermore Africa is affected by the neo-colonial brain drain which has seen scholars migrating to the west where and they end up publishing works with foreign universities leaving Africa with a low publishing of scholarly communication (World Bank , 2005). OA initiatives provides Zimbabwe and rest of Africa with an opportunity to transform the unfavourable situation through encouraging more publications through inter-institutional and inter discipline collaborations to produce more relevant intellectual output.

"There is no way we can succeed in the eradication of poverty if the developing world is not part of knowledge creation, its dissemination and utilisation to promote innovation. Higher Education is a critical factor in making this possible and must be part of any development strategy" Doctor Mamphela Ramphele(2000)

The dialectical relationship between publisher and researcher or scholars has provided a fertile ground to critique and change exploitative models of publishing so that scientists and researchers will have affordable and sustainable access to their content [START_REF] Macdonald | These five companies control more than half of academic publishing: That is why we are still paying for knowledge[END_REF].

Furthermore, the author notes that as research become more data intensive, a scholar's ability to store, access and share primary data will be crucial to the advancement of scholarship. Copyright and Open Access principles are not specimens of parallel dimension even though the two exist as distinct policies but should be reconciled to ensure the balance in protecting interests of stakeholders, for example, authors, publishers and scholars. Publishing in OA platforms benefits scholars since their works gain more recognition, visibility and expanded readership. However profit driven publishers favour business models that restrict access and then profit from controlling access to scholarly communication. Look at the explosion in selfpublishing on the web.

Research Methodology

This researcher is premised on qualitative paradigm as evidenced by its phenomenological thrust which seeks to describe phenomenon relating to Open Access in Zimbabwe. [START_REF] Dogan | the risk of information management without knowledge Management systems[END_REF] states that unlike the positivist paradigm that focuses on measurements, the phenomenological approach places emphasis on social aspects relating to the phenomenon under study. The researchers used the phenomenological approach because of its appropriateness in case studies and its potential to lend itself to researchers of any lived experience studying. The research is premised on the phenomenological philosophy with its thrust towards exploring and description of the Open Access phenomena as it is experienced in the academia [START_REF] Giorgi | The descriptive phenomenological method in psychology: A modified Harris, Evan[END_REF]).

The research site for the research was the academic libraries. The target population are assistant librarians who are strategically positioned to deal with OA and library consortia activities. Currently, there are (15) fifteen Universities in Zimbabwe. The researchers selected one University in each of the ten provinces of Zimbabwe. Therefore each university is represented by one respondent drawn from the library. The researchers triangulated interviews and experience to collect data to understudy the Open Access phenomenon in Zimbabwe's academic landscape. The researcher analysed the data qualitatively and made recommendations to policy makers.

Research Objectives

The researchers' objectives were to find answers to the following research questions:

 What is the state of Open Access in Zimbabwe's academic libraries?

 What policies are in place to support OA & ETDs?

 How many academic institutions have developed IRs?

 What is the role of the library consortia in promoting OA&ETDs?

 What needs to be done to strengthen OA& ETDs in Zimbabwe? The  Academic libraries should buttress their existence as ecosystems rather than egosystems in order to build viable wired and networked platforms for knowledge discovery.

Conclusion

  possible for Universities in Zimbabwe to capture and share scholarly content through ETD platforms. Increased demand for Higher education coupled with adaption of new budding technologies is driving development in Higher Education. These institutions are managing technological impermanence and improving quality of service through engaging and adapting creative and innovative technology-centric developments, for example, ICT's, open access, open source and digital resource sharing. Access to scholarly communication is central to realising the vision of providing high information services timeously and hence the need to invest in robust and efficient information and communication infrastructure. The ubiquitous nature of ICTs has enabled academic libraries to develop digital platforms for end users, content and the public to connect each other in search of knowledge. Such platforms enable easier accessibility and discoverability of ETD content. The endorsement of Open Access policies by members of the Zimbabwe University Library Consortium (ZULC) has given credence to the importance of the Open Access Initiatives and accessibility of ETDs. The development marks a victorious start in the battle to conquer knowledge frontiers and reposition the country in the global information / knowledge landscape. Singh (2015) describes ETDs as rich and unique sources of information "…untapped and underutilised asset…" Literature Review The OA and ETDs movement would have been inapprehensible without ICTs. The ubitiquos and insidious nature of ICTs has led to the development of academic library consortia, econtent production and licensing, resource sharing, digital repositories and preservation. Ranga (2015) states that ICTs and consequent convergence of technology has given incredible advantage to the development of scholarly communication as evidenced by the proliferation of e-content, e-publishing, e-communication and e-content portals. The author concedes that libraries are central in widening and deepening access to scholarly communication and supporting the evolution of the knowledge economy. Academic institutions have adopted Open Access Initiatives (OAI) and Institutional Repositories (IRs)

Cayabyab

  repositories. Such technologies are characterised by alternative models of submission, for example, mediated and self submission. ZULC members have taken advantage of technological development to establish ETDs that are accessible from the internet. Ferras -Fernandez (2013) argue that from a webometrics and infometrics perspective, open access ETDs have more citation counts and impact than those that are pass word protected. This gives credence to the viability of the OA initiatives with regards to promoting access to scholarly communication in academic institutions. Organisations involved in institutional web ranking and altmetrics consider IRs and openness as they contribute significantly in the scoring for institutional web ranking. The OA dispensation has resulted in the proliferation of online self-publishing and self-archiving platforms thus democratising publishing and access to content. Kusekwa and Mushawani (2014) opine that the Open Access culture has strongly gripped academic institutions in Zimbabwe as evidenced by the proliferation of Institutional Repositories (IRs) and ETDs. The adaptation of ICTs has helped to leverage intellectual capital through Open Access platforms. Library consortia are the vanguard in the Open Access initiative in Zimbabwe as evidenced by the adaptation and use of Free Open Source Software (FOSS), IRs, training workshops, OA policies, knowledge management and increased use of knowledge discovery tools to access e-resources. Technology has helped library consortia with cost effective ways of providing and sustaining quality library services and access to TDs. Open Access initiative is enabling academic libraries to overcome the restrictive barriers to access scholarly and scientific journals imposed by profit driven commercial publishing houses via subscription fees, license fees or pay-per-view fees. Open access initiative is premised on the notion that all digital scholarly communication should be available free of charge and free from the fetters of licensing and copyright. " ... free availability of literature on the public internet, permitting any users to read, download, copy, distribute , print , search, or link to the full texts of these articles, crawl them for indexing, pass them as data to software, , use them for any other lawful purposes, without financial , legal and technical barriers, other than those inseparable from gaining access to the internet…" Budapest Open Access Initiative (BOAI, 2012). Furthermore OA initiative should be analysed in the context of copyright laws with reference to public domain works. Intellectual Property Rights and copyright should be interpreted in the context of utilitarian and natural rights philosophies (Sheuefen, 2014).The former views intellectual property as a product by society and for the benefit of society, while the latter posit that an individual has a natural right to benefit from his or her labour hence the need for copyright (Eger, T. and Sheufen, Mark (2012), in Scheufen, Mark The ability to tackle or reconcile copyright and OA interests in the globalised knowledge age is critical for . There are variations with regards to how countries regulate public domain works, for example, some laws are explicit while others are not. Throughout the world there are specific laws enacted by governments to protect authors' copyrighted works, for example, the Copyright and Neighbouring Rights Act in Zimbabwe (2000). However, people should be educated that publishing in open access journals or platforms should not be misinterpreted for freedom from copyright protection because such articles still fall within the domain of legal protection. Generally, copyright persist for fifty years (50) in Africa and Asia and seventy (70) years in Europe and United States of America (Public Domain Review, 2015). However there is need for specificity with regards to how such laws will deal with public domain works and open access in order to move Africa into the knowledge economy.

Findings and discussion 

 discussion The interviews with fifteen (15) assistant librarians indicated that academic libraries in Zimbabwe have established IR's using commercial or free open source software, for example, DSpace and Greenstone. A total of six (6) academic libraries are listed on the OpenDOAR, while 40 per cent are excluded or not listed. Researchers found out that the reason why these institutions were not listed was because either their repositories were still in infant stage of development or they had not yet established one. 80% of the respondents from academic libraries indicated that they had also started publishing in open access journals as a way of commitment to the open access initiatives. However there is still need to educate researchers on the pros and cons of open access, for example, the Directory of Open Access Journals (DOAJ) to distinguish genuine high impact journals from predatory ones. Through IRs, academic libraries are able to generate new e-content and explore opportunities to license their content. The contents of these IRs include local e-content such peerreviewed articles, conference proceedings, theses and dissertations, technical reports, grey-literature and other formats.  Nearly all fifteen Universities in Zimbabwe have IRs and ETDs that are operational  All institutional repositories had ETDs. Figure 1 below shows some statistics of ETDs available in selected university IRS as at 23 rd June 2016.

Figure 1 :

 1 Figure 1: Statistics of ETDs in selected university IRs in Zimbabwe

  Zimbabwe's academic libraries should strive to use common protocol and standards to interoperability and enhance resource sharing. The challenges that are currently being experienced in the implementation of ETD programmes should be viewed from a historical dialectical and materialistic perspective as an interlude for creativity and innovation. OA platforms should be viewed as opportune technologies to transform the knowledge landscape and move Zimbabwe and other African countries from a imbecile subaltern position to one of a serious and intelligent minded equal partners in re-positioning Africa on the global knowledge economy. It would be folly for knowledge producers to view the OA initiative as an overture for the "dispossession of the already disposed" but rather it's an opportunity to strengthening the standing of academic institutions and quality of African scholarship to widen access. Through OA promotion should utilise webometrics/ infometrics to raise an awareness OA/ETD initiatives. Digital commons should be viewed as an opportunity for carving a new niche for African scholarship and democratic access to scholarly content. It is imperative that all key-stakeholders including government, the academia , private sector and communities of interest and practice should be consulted in order to make this golden opportunity a reality for the African renaissance in the global knowledge landscape. The ETD revolution signals a progressive dispensation. Globally its implementation and development has not been an easy and free from infallibity because it is a long term process operating in a dynamic and complex environment.ETDs provide an avenue to strengthen science through local open publishing. ETDs are critical in providing academic libraries to create non-elitist and democratic virtual spaces capable of providing students with value adding epistemic experiences irrespective of time and distance.

Country File download (as @September 2015)

	United States	33,890
	China	26,614
	South Africa	12,344
	Zimbabwe	11,567
	Germany	6,231

following webometrics indicate the countries that have accessed and downloaded from ETDs. The country file downloads are;

Table 1 :

 1 Webometric Downloads of ETD from one local University which is member of ZULC  The interviews also revealed that 100 per cent of the Universities were signatory to OA Policies. The responses indicated that through partnerships with EIFL members of the Zimbabwe University Library Consortium (ZULC) were working towards a national mandate for OA. Responses from interviews indicated that all members of the ZULC observed the OA week in October every year. ZULC also conducts workshops to sensitise stakeholders on the OA Initiative. These workshops have culminated in the commissioning of an OA Policy and resolutions relating to establishment of National Open Access Policy Board and closer cooperation between government, universities, research institutions and librarians.  Institutional repositories in Zimbabwe have, to a larger extent, grown because they are populated with electronic theses and dissertations. Populating the IRs with ETDs is not difficult considering that university graduates are expected to carry out research will be compiled into research reports / theses & dissertations. It must also be stressed that universities in Zimbabwe have made it requirement that every graduating student should submit a print copy and electronic copy of their dissertation to the library. Libraries then upload the electronic versions of theses & dissertations (ETDs) o their IRs. Many universities have policy frameworks that give the libraries the mandate of collecting theses and dissertations and uploading them on IRs. Open Access policies, These VLEs model or simulate conventional real-world education through integrating a set of equivalent virtual concepts for continuous assessment thus affording students access to web-based access to class content, grades, assessments, and other class tools Open or Access Education Resources (O.A.E.R). The adoption of content/knowledge and document management systems will strengthen the position and role of t academic libraries in information flows. This transition is evidenced by the reconfiguration of library space and architecture into learning and collaborative spaces among members of ZULC; There is need for a robust national thrust to coordinate the management and development of ETD repositories with regards to access and preservation. The Database of African Theses and Dissertations (DATA) is a good initiative and it has been in operation for some time. There is need to strengthen this project; and,

	intellectual property policies and student ordinances of universities are some typical
	examples of legal documents enabling libraries in universities collect and manage
	ETDs using IRs.
	 Responses from the interviews indicated	that academic libraries have to grapple
	with issues relating to infrastructural development, access and preservation of ETD
	content in the advent of technological impermanency. IRs solutions are most viable
	and sustainable when they are built on open standards. They further indicated that
	they would build on the strength of OA initiatives and policies currently in place even
	though they still have to deal with issues relating to standards and protocols for
	sharing resources.
	 ZULC members with Virtual Learning Environments (VLE) should combine this with
	their IR assets to develop and provide flexible way for reinforcing website, collating a
	university's research outputs across a particular subject area or period of time and
	supporting teaching, learning and research.

 libraries capacity to share resources. IR resources should be shareable, and findable through federated searches. This is important in leveraging and enhancing access to Electronic Theses and Dissertations(ETD); 