Raphaël Cauderlier
email: raphael.cauderlier@irif.fr

Catherine Dubois
email: catherine.dubois@ensiie.fr

FoCaLiZe and Dedukti to the Rescue for Proof Interoperability *

Numerous contributions have been made for some years to allow users to exchange formal proofs between different provers. The main propositions consist in ad hoc pointwise translations, e.g. between HOL Light and Isabelle in the Flyspeck project or uses of more or less complete certificates. We propose in this paper a methodology to combine proofs coming from different theorem provers. This methodology relies on the Dedukti logical framework as a common formalism in which proofs can be translated and combined. To relate the independently developed mathematical libraries used in proof assistants, we rely on the structuring features offered by FoCaLiZe, in particular parameterized modules and inheritance to build a formal library of transfer theorems called MathTransfer. We finally illustrate this methodology on the Sieve of Eratosthenes, which we prove correct using HOL and Coq in combination.

Introduction

According to the IEEE Standards Glossary, interoperability can be considered as the ability of computer systems or software to exchange and make use of information. Prover interoperability as a way for exchanging formal proofs between different theorem provers is a research topic that received many contributions along years. The most successful approach is probably the integration of automatic theorems provers (ATP) in interactive proof assistants (ITP) like Coq [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF] or Isabelle [START_REF] Blanchette | Automatic Proof and Disproof in Isabelle/HOL[END_REF]. In that case more or less detailed witnesses are provided and proofs can be imported or re-built. Furthermore many ad hoc pairwise translations have been proposed e.g. between HOL Light and Isabelle in the Flyspeck project [START_REF] Kaliszyk | Scalable LCF-Style Proof Translation[END_REF], between HOL Light and Coq [START_REF] Denney | A Prototype Proof Translator from HOL to Coq[END_REF][START_REF] Wiedijk | Encoding the HOL Light logic in Coq[END_REF][START_REF] Keller | Importing HOL Light into Coq[END_REF] or between HOL and Nuprl [START_REF] Howe | Importing Mathematics from HOL into Nuprl[END_REF]. To avoid the quadratic blowup in the number of translators to develop, proof formats are emerging either for proofs in a specific logic such as the OpenTheory format [START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF] for ITPs in the HOL family or relying on logical frameworks [START_REF] Miller | Foundational Proof Certificates: Making Proof Universal and Permanent[END_REF][START_REF] Schürmann | An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf[END_REF][START_REF] Horozal | Representing Model Theory in a Type-Theoretical Logical Framework[END_REF] such as λ-prolog and Twelf to represent proofs in several logics. We propose to combine proofs coming from different theorem provers relying on the Dedukti logical framework [START_REF] Saillard | Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice[END_REF], a typed λ-calculus with dependent types and rewriting, as a common formalism in which proofs can be translated and combined.

In [START_REF] Assaf | Mixing HOL and Coq in Dedukti[END_REF], Assaf and Cauderlier describe a manual attempt of interoperability between HOL and Coq where they prove in Coq the correctness of the insertion sort algorithm on polymorphic lists and instantiate it with HOL natural numbers. This experiment relies on a translation to Dedukti for both the sorting function and the definition of HOL natural numbers (using respectively Coqine and Holide) and the result is checked by Dedukti. The interaction between both parts only happens at the level of booleans. However, for such a simple fact the proof is very long and verbose (around 700 Dedukti lines).

The goal of this paper is to make prover interoperability reach a new scale. We can notice that the art specific to the case study of Assaf and Cauderlier required a lot of work that could be automated and has to be automated to scale up. For this task, we use Zenon Modulo [START_REF] Bury | Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo[END_REF], an automated theorem prover outputting Dedukti proofs.

In this work, we go beyond simple boolean interaction. When a type and operations over this type, such as natural numbers and arithmetic operations, are independently defined in two ITPs, we can translate them but we end up with distinct isomorphic structures A and B in Dedukti. A theorem ϕ A proved for A does not give us for free the corresponding theorem ϕ B about B in which we are interested. Two solutions to this problem have been proposed:

modify one of the translators to make it use the type and operations of the other structure thus identifying structures A and B, keep structures A and B distinct and use tactics to automatically prove transfer theorems of the form

ϕ A → ϕ B .
The first solution is favored in several ad hoc interoperability proposals [START_REF] Keller | Importing HOL Light into Coq[END_REF][START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF].

The main limitation of this solution is the complexification of the translators which lacks scalability: for interoperability between n proof systems independently defining a mathematical structure, n -1 translators need to be modified to become customizable and point to the definition of the nth proof system. The second solution has first been proposed in the context of formalization in Isabelle/HOL of quotient structures [START_REF] Huffman | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL[END_REF] and recently ported to Coq [START_REF] Zimmermann | Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant[END_REF]. Its main limitation is that the definitions of the morphisms and the proofs that operations are preserved by morphisms are left to the human user. We propose a compromise between these two solutions: we prove transfer theorems in Fo-CaLiZe [START_REF] Pessaux | FoCaLiZe: Inside an F-IDE[END_REF], an ITP featuring a customizable Dedukti translator and use them to relate independent developments coming from uncustomizable translators.

The first contribution of this paper is a FoCaLiZe library of mathematical structures, morphisms, and transfer theorems called MathTransfer. The second contribution is a proposed methodology for scalable interoperability relying on Dedukti, Zenon Modulo, FoCaLiZe, and MathTransfer. The third contribution is the correctness proof of the Sieve of Erathostenes considered as the combination of a lemma coming from HOL and another coming from Coq. This proof illustrates our methodology.

The paper is structured as follows. In Sections 2, 3, and 4 we present very briefly resp. the Dedukti logical framework, the FoCaLiZe system, and the Math-Transfer library. These tools form the basis of our approach to interoperability presented in Section 5. Sections 6 and 7 are devoted to a case study illustrating it on a correctness proof of the Sieve of Eratosthenes. Finally, we conclude and discuss in Section 8 the generality and reusability of our development.

The MathTransfer library and our interoperability case study are distributed together at the following URL: https://gitlab.math.univ-paris-diderot. fr/cauderlier/math_transfer.

Dedukti, a Universal Proof Language

Dedukti [START_REF] Saillard | Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice[END_REF] is a variant of the dependently-typed λ-calculus Twelf, a logical framework based on the Curry-Howard correspondence. Logics are encoded in Dedukti by providing a signature and then proof checking in the encoded logic is reduced to type checking in the encoding signature. For example, the conjunction in natural deduction can be encoded by the following signature: The type Prop of logical propositions is first declared, then to each proposition A we associate the dependent type of its proofs proof A. The conjunction and is then declared and so are finally the usual elimination and introduction rules.

The dependent product Πx : A. B is written x: A -> B in Dedukti. It is used to encode universal quantification. Dependent products and arrow types are introduced by λ-abstractions and eliminated by applications. The λ-abstraction λx : A. b is written x: A => b in Dedukti. For example, a proof of commutativity of conjunction in Dedukti is the term

A: Prop => B: Prop => H: proof ( and A B ) => and_intro B A ( and_elim2 A B H ) ( and_elim1 A B H )
of type A: Prop -> B: Prop -> proof (and A B) -> proof (and B A)

Dedukti also features rewriting which is used to express computational higher-order logics such as the Calculus of Inductive Constructions implemented in the Coq proof assistant [START_REF] Assaf | A Framework for Defining Computational Higher-Order Logics[END_REF].

Translators from various ITPs to Dedukti have been developed [START_REF] Assaf | Expressing Theories in the λΠ-Calculus Modulo Theory and in the Dedukti System[END_REF]. In particular, Holide [START_REF] Assaf | Translating HOL to Dedukti[END_REF], Coqine [START_REF] Assaf | A Framework for Defining Computational Higher-Order Logics[END_REF], and Focalide [START_REF] Cauderlier | ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti[END_REF] are translators from respectively the OpenTheory format for ITPs in the HOL family, the Coq proof assistant and the FoCaLiZe framework. Some ATPs also produce Dedukti files, e.g. iProver Modulo [START_REF] Burel | Experimenting with Deduction Modulo[END_REF] and Zenon Modulo [START_REF] Bury | Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo[END_REF][START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF] which is used in this work.

Dedukti is a mere proof checker for a wide variety of logics, it is not intended for direct human use and it intentionally lacks features commonly found in similar systems such as modularity, type inference and implicit arguments. While these features are not needed in a proof checker, they are crucial for scalability of interoperability developments. We propose to compensate this lack by using FoCaLiZe as an interoperability framework for linking mathematical libraries.

3 FoCaLiZe, Zenon Modulo, and Focalide to the Rescue FoCaLiZe (http://focalize.inria.fr) has been designed as a formal environment for developing certified programs and libraries. It provides a set of tools to formally specify and implement functions and prove logical statements. Fo-CaLiZe comes with three backends, a backend to OCaml for execution and two backends for formal verification. The historic one produces Coq code and requires the use of the ATP Zenon which can output proofs as Coq terms. A more recent backend, called Focalide, produces Dedukti code [START_REF] Cauderlier | ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti[END_REF] and requires to use Zenon Modulo [START_REF] Bury | Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo[END_REF], an extension of Zenon which produces Dedukti proofs [START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF]. In this work, we only use the Focalide backend.

We present here very briefly the main ingredients of FoCaLiZe. For more details please consult [START_REF] Pessaux | FoCaLiZe: Inside an F-IDE[END_REF].

In FoCaLiZe, specifications are written in a typed version of first-order logics; implementations are written with the help of a pure functional programming language very close to ML with algebraic datatypes, first class citizens functions, polymorphic types, recursion and pattern-matching. FoCaLiZe proposes a highlevel proof language and discharges the logical details to Zenon or Zenon Modulo (according to the used backend). A proof in this language consists of intermediate lemmas and hints to the prover. When a proof is out of scope of the prover, a manual proof expressed in the backend language, Coq or Dedukti, is required.

A FoCaLiZe unit, named a species, is made of signatures, properties, definitions of functions and types and also proofs of user-defined properties. A species mearly defines a set of values and functions manipulating them where the meaning of the functions are given by properties. Inside a species, the type Self denotes the type of these values, it is usually abstract early in the development and made concrete later. When a species is complete, that is every function is definied and every property is proven, it can be turned into a collection which is close to an abstract data type. FoCaLiZe features modularity, more precisely multiple inheritance. Thus a species can be defined by inheriting from some others, allowing the reuse of all the signatures, definitions and proofs coming from them. When the definition of a function is inherited, it is possible to give it a new definition overriding the inherited one. This feature is not used here. A FoCaLiZe development appears as a hierarchy of species linked by inheritance, such as the one described in Fig. 1. Moreover species can be parameterized by collections. In that case, inside a species, the user is allowed to use functions and properties as black boxes as in a functor. In the following, we say a species is instanciated when it is applied to a particular collection.

Similarly to the possibility to prove directly a theorem in one of the target logical languages, FoCaLiZe allows the definition of global symbols by custom external expressions of the target languages (OCaml, Coq, and Dedukti). It is, with modularity, a key feature for our interoperability application. For example, addition of integers is defined in FoCaLiZe standard library as follows. It is declared with its type in the FoCaLiZe side, each branch in the definition maps + to a function written in the corresponding target language:

let ( + ) = internal int -> int -> int external | caml -> {* Ml_builtins . bi__int_plus *} | coq -> {* coq_builtins . bi__int_plus *} | dedukti -> {* dk_int . plus *} ;;
In this article, we use FoCaLiZe as an interoperability framework to provide the features missing in Dedukti for this task: modularity offered by FoCaLiZe inheritance, and proof automation provided by Zenon Modulo.

MathTransfer, a Library of Transfer Theorems

If A and B are two isomorphic mathematical structures, then for any formula ϕ A expressed in the language of A, the formula ϕ A → ϕ B is a theorem where ϕ B is the formula corresponding to ϕ A in the language of B. Theorems of the form ϕ A → ϕ B are called transfer theorems. The use of transfer theorems is a way to formalize rigorously the mathematical habit of reasoning modulo isomorphism.

MathTransfer is a FoCaLiZe library of transfer theorems about natural numbers. More precisely, the MathTransfer library contains:

definitions of the mathematical structures obtained by adding common arithmetic operations on natural numbers, definitions of (iso)morphisms between abstract representations of natural numbers, proofs that all operations are preserved by the morphisms, and -84 transfer theorems.

Each structure is defined as a FoCaLiZe species. Because the definitions of some operations depend on other operations, these species are organized in a hierarchy presented in Fig. 1 (where frames represent species and an arrow goes from a species S 1 to a species S 2 if S 1 directly inherits from S 2 ).

The species in this hierarchy contain only the axiomatisations of the operations, not their other properties. For example, the species corresponding to the multiplication (× frame in Fig. 1) contains:

a new binary operation × representing multiplication, two first-order axioms: ∀n. 0 × n = 0 and ∀m n. succ(m)

× n = n + (m × n).
This species is written as follows in FoCaLiZe: Morphisms on the other hand form a parameterized hierarchy of species. A morphism from a representation A of natural numbers is defined by a function morph of type A -> Self preserving zero and successors. From Peano axioms, assumed both in A and in the current species, we prove that morph is a bijection preserving all the operations. For example, here is the parameterized species proving that multiplication is preserved by the morphism (proof is omitted):

species NatTimesMorph ( A is NatTimes ) = inherit NatTimes , NatPlusMorph ( A ); theorem morph_times : all a1 a2 : A , morph ( A ! times ( a1 , a2 )) = times ( morph ( a1 ) , morph ( a2 )) proof = ...; end ;;

These proofs of preservation of operations are not fully automatized because they require reasoning by induction which is not handled by Zenon Modulo but Zenon Modulo is extensively used for the subproofs.

By inheriting from both the morphism hierarchy and the list of statements, we can state and automatically prove the transfer theorems. Below is a fragment of the species containing the 7 transfer theorems relative to the previous 7 theorems about multiplication: Each transfer proof relies on three ingredients:

the corresponding theorem in the parameter A, bijectivity of morph (hypotheses morph_injective and morph_surjective), preservation of some operations by the morphism (hypotheses morph_zero, morph_succ, morph_times).

These transfer proofs are not automatically found by Zenon Modulo but are generated by a specialized transfer tactic written in Dedukti and similar to the transfer tactics for Isabelle and Coq [START_REF] Huffman | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL[END_REF][START_REF] Zimmermann | Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant[END_REF].

Methodology for Dedukti-Based Interoperability

In this section, we propose an interoperability methodology based on Dedukti and MathTransfer. More precisely we detail below the different steps which must be followed when we want to use a lemma from a tool/formalism A in a formal proof of a theorem in another formalism B. The statements of the lemma in A and B do not need to be syntactically identical but thanks to the ATP Zenon Modulo some degree of rephrasing of the lemma is tolerated. Some prerequisites about A and B are required before applying the process. First translators from A and B to Dedukti must exist. Then we rely on the fact that formalisms A and B have already been merged in Dedukti, it means that the logical linking of both logics has been done (sources of inconsistencies have been identified and fixed).

The steps are the following ones (between parentheses appears the formalism or the tool to be used to realize the step):

1. identify the lemma L to exchange between A and B and prove it (A); 2. prove in B the target theorem with the exported A lemma L considered as an hypothesis (B); 3. translate both the A lemma L and the B development T in Dedukti (use the corresponding translators); 4. if needed, extend the FoCaLiZe hierarchies of the MathTransfer library with the operations appearing in the statement of the lemma L (FoCaLiZe); 5. instantiate the FoCaLiZe hierarchies with external definitions and proofs from A and B; if the statements do not exactly match, use Zenon Modulo (FoCaLiZe with the help of Zenon Modulo); 6. automatically transfer the lemma L (FoCaLiZe); 7. translate the whole FoCaLiZe development in Dedukti (use Focalide); 8. write the proof of the final target theorem (a trivial Dedukti proof).

In Sections 6 and 7, we apply this methodology to the correctness proof of the Sieve of Eratosthenes which is a small but typical case study where A is HOL and B is Coq.

Presentation of the Example: an Incomplete Coq Proof of the Sieve of Eratosthenes

In [START_REF] Assaf | Mixing HOL and Coq in Dedukti[END_REF], Assaf and Cauderlier managed to link a Coq development with an HOL development directly in Dedukti because the example was chosen to minimize the interaction between Coq and HOL types. We now consider a more complicated example: a proved version of the Sieve of Eratosthenes. In this new proof of concept of interoperability in Dedukti, HOL and Coq have to agree on the type of natural numbers despite having slightly different definitions for it:

in Coq, the type of natural numbers is defined as an inductive type; in HOL, inductive types are not primitive and natural numbers are encoded.

The Sieve of Eratosthenes is a well-known algorithm for listing all the prime numbers smaller than a given bound. In this section, we propose a certified implementation of this algorithm in the Coq proof assistant. We decompose this task in three: we have to program the sieve in Coq, to specify its correctness, and to prove it. In Section 6.1, we program the sieve in Coq and in Section 6.2 we specify it and sketch a proof of the correctness of the algorithm. We highlight the mathematical theorems on which this proof relies. In order to experiment with interoperability, we will not prove these mathematical results in Coq but import them from the OpenTheory libraries3 .

Programming the Sieve of Eratosthenes in Coq

Divisibility plays two purposes in our development: we need a divisibility test inside the definition of the algorithm and we also need divisibility to define primality and specify the algorithm. In order to get a simple definition of primality, we introduce strict divisibility: we say that a is a strict divisor of b if a divides b and 1 < a < b. Using Euclidean division, we define strict divisibility as a boolean function (sd in Coq, definition omitted here). A natural number p > 1 is then called a prime number if and only if it has no strict divisor.

We now have all the prerequisites for defining the sieve's core function. We use the usual fuel trick for avoiding a termination proof. In the following definition, filter p l computes the list of elements of l that satisfy the boolean function p and negb is boolean negation. When fuel is bigger than the length of l, Sieve l fuel gives the expected result so the length of l is a convenient default value for fuel. Finally, the prime numbers smaller than 2 + n can be computed by the following function where interval 2 n computes the interval [2, 2 + n].

Definition eratosthenes n := Sieve ( interval 2 n ) n .

Specification and Correctness Proof

The specification of the Sieve of Eratosthenes is quite simple: a number p is a member of the list returned by eratosthenes n if and only if p is a prime number smaller than 2 + n.

We first define the prime predicate to be satisfied when its argument is a prime natural number: We state the specification of the Sieve of Eratosthenes as the following three lemmata (where In is the list membership predicate).

A natural number returned by the function erathostenes is a prime number and is lower than the bound: Any prime number lower than the bound will be returned by the function erathostheses:

Lemma complete p n : prime p -> p <= 2 + n -> In p ( eratosthenes n ).
For completeness, it is enough to prove that the Sieve function preserves prime numbers (assuming it received enough fuel).

The first soundness lemma also relies on an invariant of the Sieve function, namely that the members of Sieve l fuel are all members of l. The proof is then concluded by a simple soundness property of intervals.

The second soundness lemma is where arithmetic is required. Let p be a member of eratosthenes n, we can easily prove that 2 ≤ p by an argument similar to the proof of the first soundness lemma. To prove that p has no strict divisor, we use the following standard arithmetic result: Lemma 1. Let n be a natural number greater than 2, n has a prime divisor.

For the sake of our proof of concept, we shall not prove this result in Coq. Fortunately, the prime divisor lemma is proved in OpenTheory natural-prime library so item number 1 on our interoperability checklist presented in Section 5 is skipped.

We prove the correctness of the Sieve of Eratosthenes in Coq when Lemma 1 is considered as a parameter thus completing item number 2 on our checklist. This development can be split into three parts of approximately the same size:

straightforward arithmetic results such as commutativity of addition and multiplication, these results are proved in both Coq standard library and OpenTheory but they are so straightforward that they are easier to reprove than to import and Coqine is not yet able to translate the part of the standard library in which they are proved, correctness of auxiliary functions which could be reused in other developments (modaux, strict divisibility and functions manipulating lists), and correctness of the functions Sieve and eratosthenes which are specific to this problem.

As in [START_REF] Assaf | Mixing HOL and Coq in Dedukti[END_REF], the results that we want to import from HOL are hypotheses of the final theorem that has to be provided in Dedukti.

In this section, we follow the steps outlined in Section 5 to import in our Coq development the prime divisor lemma from HOL. The prerequisites for the methodology to apply are met thanks to the work of Assaf and Cauderlier [START_REF] Assaf | Mixing HOL and Coq in Dedukti[END_REF] that we summarize in Section 7.1. The various steps of the methodology are then followed in Sections 7.2 to 7.5. These steps are also pictured in Fig. 2. Two sources of inconsistencies were identified. First, Coq and HOL do not agree on the question of type inhabitation: Coq allows empty types whereas we can prove in HOL that all types are inhabited. Second, the notions of booleans and logical propositions are identified in HOL and distinguished in Coq.

Type inhabitation is solved in [START_REF] Keller | Importing HOL Light into Coq[END_REF] and [START_REF] Assaf | Mixing HOL and Coq in Dedukti[END_REF] by identifying HOL types not with Coq types but with Coq inhabited types (in the Coq type ΣA : Type 0 . A).

The difference between HOL booleans and Coq propositions is solved by identifying the type of HOL booleans with the type of Coq booleans, which are reflected as proposition by the symbol hol_to_coq.Is_true of type hol.bool -> coq.prop. This symbol is used to express provability in HOL as a special case of provability in Coq.

Extension of the MathTransfer Hierarchies up to the Prime Divisor Lemma

MathTransfer, as we have seen, contains transfer theorems corresponding to the most common arithmetic operations and relations such as found in OpenTheory base library. OpenTheory does also contain arithmetic definitions and theorems outside its base library. In particular, it defines divisibility and primality and it contains the following statement of the prime divisor lemma:

∀n, n = 1 → ∃p, (prime(p) ∧ p | n)
Following item number 4 on our checklist, we extend the FoCaLiZe hierarchies that we presented in Section 4 by four blocks:

a definition of divisibility, a definition of strict (non-trivial) divisibility, this notion is used in the definition of primality, a definition of primality, this notion appears in the statement of the prime divisor lemma, the statement of the prime divisor lemma.

The extended hierarchy of operation definitions is shown in Fig. 3. It is not required to state and transfer all the HOL lemmas dealing with divisibility and primality, it is enough to do so for the few ones that we are interested in such as the prime divisor lemma. The notion of isomorphism between representations of natural numbers is extended to take the new operations into account and the prime divisor lemma is automatically transferred.

Instantiation of Coq Natural Numbers

We can instantiate the hierarchy of species on the Coq side using FoCaLiZe external Dedukti definitions mapping directly the symbols to their Coqine translation in Dedukti. All the proofs required to instantiate the axioms characterizing the operations are trivial Dedukti proofs of reflexivity. For example, the species NatTimes is instantiated as follows: The theorems number 117 and 157 in the Holide output of OpenTheory base library respectively state ∀n. 0×n = 0 and ∀m n. succ(m)×n = (m×n)+n. The first one is exactly the statement of zero_times but the statement of succ_times is ∀m n. succ(m) × n = n + (m × n). The gap is filled by Zenon Modulo thanks to a previous import of the commutativity of addition (property plus_commutes).

The hierarchy is fully implemented and can be turned in a collection, that is a species where every signature received a definition and every property has been proved.

species HolPrimeDiv = collection HolPrimeDivColl = inherit NatPrimeDiv , HolPrime ; implement HolPrimeDiv ; ... end ;; end ;;

Instantiation of the Morphism

If f is a function of type α → α and n is a natural number, we note f n the nth iteration of the function f

(f 0 = Id, f n = f • f • . . . f , n times).
Both the Coq Init library4 and the OpenTheory base library define this polymorphic iteration of a function f . We use them to define the isomorphism between HOL natural numbers and Coq ones. The morphism from HOL natural numbers to Coq ones is defined by an HOL iteration of the Coq successor function morph(n) := coq_succ n (coq_zero) (coq_zero and coq_succ are mapped to the Dedukti translation of the Coq definitions) and its inverse is defined by a Coq iteration of the HOL successor function inv_morph(n) := hol_succ n (hol_zero).

By instantiating all the morphisms and transfer hierarchies (items 5 and 6 of our methodology), we finally obtain in FoCaLiZe the prime divisor theorem on the Coq formulation of arithmetic structures. Once translated in Dedukti by Focalide, this theorem matches the assumption of the correctness proof of the Sieve of Eratosthenes translated from Coq so we obtain a Dedukti proof of the correctness of the Sieve of Eratosthenes (item number 8 of our methodology).

Quantitatively, the size of the various parts of this development are given in Fig. 4. The HOL part of the development consists in a fragment of the OpenTheory library that was developed independently and contains thousands of theorems irrelevant to our case study. The Coq development however is of reasonable size and was specifically developed for this case study. In the case of FoCaLiZe, more than half of the generated code is produced by Zenon Modulo; this shows how useful proof automation has been in this development. Finally, the small Dedukti development is taken from the merging of Coq and HOL logics in [START_REF] Assaf | Mixing HOL and Coq in Dedukti[END_REF].

Conclusion

We achieved our goal of certifying a Coq implementation of the Sieve of Eratosthenes using arithmetic results from OpenTheory. FoCaLiZe inheritance and parametrization allowed us to devise MathTransfer, a library of mathematical structures and transfer theorems. Zenon Modulo was of great help during this formalization since a lot of small steps of equational reasoning were needed and proving them in Dedukti would have been painful. We tried to do as much work as possible in a system independent way. The MathTransfer library is independent of HOL and Coq. Thanks to the symmetry in the roles of Coq and HOL, we can not only import lemmas from HOL to Coq but also in the other direction. Moreover, the definitions of the operations do not need to be identical in both systems. It is usual in FoCaLiZe to limit the dependencies to the definitions of methods thanks to late binding [START_REF] Prevosto | Making proofs in a hierarchy of mathematical structures[END_REF]. For small differences Zenon Modulo can fill the gap, for bigger ones such as divisibility (which is derived from Euclidean division on the Coq side) the equivalence of the definitions can be proved in either system. This working example of interoperability needs to be reproduced with bigger proofs but also with proofs coming from some other systems if their underlying logics can be encoded within Dedukti. We believe that the methodology illustrated in this paper is scalable. However more automation is required in particular for the extension of MathTransfer. We expect the work of Gauthier and Kaliszyk [START_REF] Gauthier | Matching concepts across HOL libraries[END_REF] on automatic discovering of isomorphic structures from different formal libraries to adapt for this task. A limitation of our approach to interoperability in Dedukti is the trust we can have in the final proof because it is expressed in an uncommon logic whose consistency is not yet proved. Users of ITPs might expect from an interoperability development to obtain a proof in their trusted system. In order to translate back the proof in the combined logic to one of the original systems, we need to remove from the proof the use of unnecessary axioms of the other system. Preliminary work in this topic has been proposed in [START_REF] Cauderlier | A Rewrite System for Proof Constructivization[END_REF] where Cauderlier uses Dedukti rewriting to automatically remove classical axioms in Zenon proofs.

  Prop: Type . proof: Prop -> Type . and: Prop -> Prop -> Prop . and_intro: A: Prop -> B: Prop -> proof A -> proof B -> proof ( and A B ). and_elim1: A: Prop -> B: Prop -> proof ( and A B ) -> proof A . and_elim2: A: Prop -> B: Prop -> proof ( and A B ) -> proof B .

Fig. 1 .

 1 Fig. 1. The FoCaLiZe species hierarchy of MathTransfer structures

  species NatTimesTransfer ( A is NatTimesThm ) = inherit NatTimesMorph ( A ) , NatTimesThm ; proof of times_zero = by property A ! times_zero , morph_zero , morph_times , morph_injective , morph_surjective ; proof of times_succ = by property A ! times_succ , morph_succ , morph_times , morph_injective , morph_surjective ; proof of times_assoc = by property A ! times_assoc , morph_times , morph_injective , morph_surjective ; ... end ;;

Fixpoint

  Sieve ( l : list )( fuel : nat ) { struct fuel } : list := match fuel with | O => Nil | S fuel => match l with | Nil => Nil | Cons a l => Cons a ( Sieve ( filter ( fun b => negb ( sd a b )) l ) fuel ) end end .

  Inductive Istrue : bool -> Prop := ITT : Istrue true . Definition prime p := 2 <= p /\ forall d , Istrue ( negb ( sd d p )).

  Lemma sound_1 p n : In p ( eratosthenes n ) -> p <= 2 + n . Lemma sound_2 p n : In p ( eratosthenes n ) -> prime p .

Fig. 2 .

 2 Fig. 2. The methodology in action for HOL/Coq interoperability

Fig. 3 .

 3 Fig. 3. The FoCaLiZe hierarchy of MathTransfer structures extended up to primality

  species CoqTimes = inherit NatTimes , CoqPlus ; let times ( m : coq_nat , n : coq_nat ) = internal coq_nat external | dedukti -> {* Coq__Init__Peano . mult m n *} ; proof of zero_times = dedukti proof definition of zero , times {* ( n : cc . eT abst_T => logic . eq_refl abst_T abst_zero ). *} ; proof of succ_times = dedukti proof definition of succ , plus , times {* ( m : cc . eT abst_T => n : cc . eT abst_T => logic . eq_refl abst_T ( abst_times ( abst_succ m ) n )). *} ; end ;; 7.4 Instantiation of HOL Natural Numbers Thanks to FoCaLiZe external definitions again, we can import in FoCaLiZe the HOL definitions of natural numbers and arithmetic operations. All the required proofs are found in the OpenTheory libraries. For example, the species NatTimes is instantiated as follows: species HolTimes = inherit NatTimes , HolPlus ; let times ( p : hol_nat , q : hol_nat ) = internal hol_nat external | dedukti -> {* HolNaturals . Nu mb er_ 2E Na tur al _2 E_2 A p q *} ; proof of zero_times = dedukti proof definition of zero , times {* HolNaturals . thm_117 . *} ; theorem hol_succ_times : all m n : Self , times ( succ ( m ) , n ) = plus ( times (m , n ) , n ) proof = dedukti proof definition of succ , plus , times {* HolNaturals . thm_157 . *} ; proof of succ_times = <1 >1 assume m n : Self , prove times ( succ ( m ) , n ) = plus (n , times (m , n )) <2 >1 prove times ( succ ( m ) , n ) = plus ( times (m , n ) , n ) by property hol_succ_times <2 >2 prove plus ( times (m , n ) , n ) = plus (n , times (m , n )) by property plus_commutes <2 >f conclude <1 >f conclude ; end ;;

  Size of the various parts of the development

		HOL Coq FoCaLiZe Zenon Modulo Dedukti
	Source Code	3.2M 31K	129K	9K
	Generated Dedukti Code 90M 828K	1.3M	1.7M
	Fig. 4.

The purpose is to illustrate the methodology previously presented. Of course, this example is simple enough to be completely realized within Coq or done by reusing e.g. the translation from Hol Light to Coq proposed by Keller and Werner[START_REF] Keller | Importing HOL Light into Coq[END_REF].

The Coq Init library is the part of Coq standard library defining logical connectives and basic datatypes such as natural numbers and lists.

This work has been supported in part by the VECOLIB project of the French national research organization ANR (grant ANR-14-CE28-0018).


Sébastien Harispe

Stefan Janaqi

Sylvie Ranwez

Jacky Montmain

From Theoretical Framework To Generic Semantic Measures Library

Keywords: measures-library.org Semantic Similarity Measures, Unifying Framework, Semantic Measures Library, Software for Semantic Measure Computation

Semantic Measures (SMs) are of critical importance in multiple treatments relying on ontologies. However, the improvement and use of SMs are currently hampered by the lack of a dedicated theoretical framework and an extensive generic software solution. To meet these needs, this paper introduces a unified theoretical framework of graph-based SMs, from which we developed the open source Semantic Measures Library and toolkit, a solution that paves the way for design, computation and analysis of SMs. More information at dedicated website: http://www.semantic-

Introduction

Numerous initiatives take advantage of ontologies to characterize entities, such as scientific publications, people or genes. To exploit such knowledge for information retrieval and knowledge discovery, inexact searches have to be performed, which require measures that are capable of assessing the degree of likeness of entities. Semantic measures (SMs) are designed for this purpose: to capture the relatedness of concepts (and by extension semantically characterized entities), by taking into account the semantic space in which they are defined. This paper explores graph-based SMs, here denoted SMs for convenience. Study of SMs involves various communities which have designed numerous measures for specific treatments and ontologies [START_REF] Pesquita | Semantic similarity in biomedical ontologies[END_REF][START_REF] Pedersen | Measures of semantic similarity and relatedness in the biomedical domain[END_REF]. However, no unifying theoretical framework has been proposed to explicitly characterize core elements of SMs through the spectrum of similarity and graph theory. Indeed, given the lack of contributions focusing on theoretical aspects of SMs, studies are often restricted to a specific community and do not benefit to a broader target audience.

Likewise, most of software dedicated to SMs are developed for particular ontologies (e.g. WordNet, UMLS, Gene Ontology, MeSH, Disease Ontology [START_REF] Pirró | A Feature and Information Theoretic Framework for Semantic Similarity and Relatedness[END_REF][START_REF] Pedersen | WordNet::Similarity: measuring the relatedness of concepts[END_REF][START_REF] Yu | GOSemSim: an R package for measuring semantic similarity among GO terms and gene products[END_REF][START_REF] Li | DOSim: An R package for similarity between diseases based on Disease Ontology[END_REF]). This diversity of software solutions has drawbacks given that SM evaluations rely exclusively on empirical studies. Therefore, the lack of an extensive software solution slows down studies of SMs as well as the sharing of new findings related to the domain.

This paper proposes a unified theoretical framework and a generic software solution to mutualize efforts and advance the increasing role of SMs in numerous fields. The second section introduces the framework which defines a reduced set of abstract primitive functions that are commonly used for SM design. The third section presents the Semantic Measures Library, an extensive open source library dedicated to the computation, development and analysis of SMs.

A Unifying Theoretical Framework for Semantic Measures

Most SMs are expressed reducing an ontology to a graph , with being the set of classes represented as vertices and the set of edges representing the oriented pairwise relationships defined between two classes. is assumed to contain a taxonomical sub-graph defining a partial order on with if is a subclass of . Moreover, classical knowledge bases are composed of a collection of entities which are conceptually characterized through classes, e.g. genes annotated by concepts [START_REF] Pesquita | Semantic similarity in biomedical ontologies[END_REF] or PubMed articles indexed by MeSH descriptors. SMs used to compare entities are extension of those designed to compare pairs of classes. We therefore focus on SMs estimating the similarity of pairs of classes, that is to say a tion . Formulas of existing measures proposed in the literature are not presented, we orient the reader to the numerous surveys for detailed presentations [START_REF] Pesquita | Semantic similarity in biomedical ontologies[END_REF][START_REF] Pedersen | Measures of semantic similarity and relatedness in the biomedical domain[END_REF].

This section defines a unifying theoretical framework aiming to: (i) better characterize SMs at a theoretical level through the definition of the primitive abstract functions on which SMs rely, (ii) distinguish common and relevant features of SMs, (iii) analyse measures' characteristics and properties, (iv) design and optimize SMs in accordance with usage contexts. Presented results expand previous works on the characterization of SMs through abstract formulations [START_REF] Pirró | A Feature and Information Theoretic Framework for Semantic Similarity and Relatedness[END_REF][START_REF] Sánchez | Semantic similarity estimation in the biomedical domain: An ontology-based information-theoretic perspective[END_REF][START_REF] Blanchard | A generic framework for comparing semantic similarities on a subsumption hierarchy[END_REF][START_REF] Cross | Unifying ontological similarity measures: A theoretical and empirical investigation[END_REF]. Their main goal was to establish links between various models of semantic similarity rather than distinguishing the primitive functions governing measures design. Our contribution focuses mainly on the definition of those primitive functions. It is therefore not constrained to a specific model of similarity (e.g. feature, information theory, geometric and transformation models).

The set of primitive functions which can be used to express most abstract formulations of SMs is:



: semantic representation of a class (denoted ̃). With a set composed of paths, classes or any subset of , we define .  ̃ : salience of the representation of a class, i.e. the amount of information carried by a semantic representation ̃, .  ( ̃ ̃): commonalities of the pair ̃ ̃ , .  ̃ ̃ : differences of the pair ( ̃ ̃ , .  ( ̃ ̃): amount of information defined in the semantic space, which is not found in the couple of representations ̃ ̃ , .

Once the representation of a class and the corresponding operators used to estimate the commonalities and differences are defined, some abstract functions estimating similarity can be used. For instance, the similarity can be assessed based on an abstract expression of the ratio model ( ), initially proposed by Tversky to compare semantic elements represented as sets of features [START_REF] Cross | Unifying ontological similarity measures: A theoretical and empirical investigation[END_REF]:

̃ ̃ ( ̃ ̃) ( ̃ ̃) ̃ ̃
with ̃ , and two parameters defining the asymmetrical contribution of the operator .

The unifying framework is not constrained to a specific measure but rather relies on primitive functions commonly used to define SMs. As an example, numerous similarity measure expressions rely on a function estimating the amount of information carried by the representation of an element, e.g. the cardinality when compared elements are represented by sets. Such a function enables the use of the abstracted form of two general expressions unifying binary measures: Gower & Legendre and Caillez & Kuntz parameterized measures [START_REF] Blanchard | A generic framework for comparing semantic similarities on a subsumption hierarchy[END_REF]. Those abstract measures, among others, can be used to derive most of SMs through specific expressions of the abstract functions on which they rely ( ) [START_REF] Sánchez | Semantic similarity estimation in the biomedical domain: An ontology-based information-theoretic perspective[END_REF][START_REF] Blanchard | A generic framework for comparing semantic similarities on a subsumption hierarchy[END_REF]. To define a concrete measure, SM designers should specify the primitive functions distinguished by the framework. As an example: (i) representing a class by the set of its subclasses, ; Research on SMs is driven by a cycle consisting of three aspects: theoretical studies, software development and empirical studies. Another important aspect for SM studies is therefore to provide ways to take advantage of theoretical contributions through software solutions.

3

The Semantic Measures Library

The Semantic Measures Library (SML) is a generic software solution dedicated to SM computation, analysis and development. By generic, we mean that the SML can be used to take advantage of SMs on a wide range of semantic graphs. Following the abstraction layers defined in the previous section, a large collection of SMs has been implemented. Moreover, thanks to the code base available (e.g. graph algorithms), new measures can easily be designed and evaluated. The SML is written in JAVA and open-sourced under the GPL-compatible CeCILL licence. In addition, the SML-Toolkit enables non-developers to benefit from functionalities provided by the SML through command-line interfaces. Documentation, tutorials and downloads of both the SML and the toolkit are available at http://www.semantic-measures-library.org.

Conclusion

This paper defines a unifying theoretical framework for SMs. By underlining close relationships between measures, we distinguish the primitive functions required for their design. Besides facilitating the definition of countless new measures, this new insight allows us to study SMs which are grouped in accordance with the expressions of the abstract functions they rely on. This leads us to draw interesting perspectives regarding the theoretical studies of SMs.

To address the handicapping lack of a generic, extensive and efficient software solutions dedicated to SMs, we developed the open source Semantic Measures Library (SML) and associated toolkit. The SML, both highly tuneable and not limited to a particular semantic graph, is suited for diverse application contexts. Downloads and documentation are available at http://www.semantic-measures-library.org.

  defining the commonality classes as a function of the Information Content (IC) carried by their Most Informative Common Ancestor (MICA), ̃ ̃ ; (iii) evaluating the difference of two classes by ̃ ̃ ; (iv) setting with and equal to 1 corresponds to the measure proposed by Pirró & Euzenat [3].


Hadi Sayed
email: hadii.sayed95@gmail.com

Ali El-Amine
email: ali.el-amine@imt-atlantique.fr

Hussein Al

Haj Hassan
email: hhajhassan@aust.edu.lb

Loutfi Nuaymi
email: loutfi.nuaymi@imt-atlantique.fr

Roger Achkar
email: rachkar@aust.edu.lb

Reinforcement Learning for Radio Resource Management of Hybrid-Powered Cellular Networks

Keywords: Cellular Networks, Reinforcement learning, Renewable energy, Smart grid

In this paper, we consider cellular networks powered by both renewable energy and the Smart Grid. We study the problem of minimizing the cost of on-grid energy while maximizing the satisfaction of users with different requirements. We consider patterns of renewable energy generation, traffic variation and real-time price of grid energy. Knowing that these patterns are all time related, we use Q-learning to extract a common pattern as well as to decide the number of radio resource blocks activated to maximize the users' satisfaction and minimize the on-grid energy cost. Results show that using Q-learning achieves a good tradeoff with more than 75% reduction in energy cost and negligible degradation in users' satisfaction.

I. INTRODUCTION

Cellular networks are witnessing exponential increase in mobile traffic with no sign of slowing down. Based on CISCO VNI, it is forecasted that the global mobile data traffic will witness an increase of seven-fold between 2016 and 2021 [START_REF]Cisco Visual Networking Index: Global Mobile Data Traffic Forecast Update[END_REF]. As a fast solution, mobile operators are deploying more base stations (BSs). This imposes serious challenges on mobile operators in terms of both operational and capital expenditures. Focusing on operation expenditure, the energy cost can reach more than 32% of the total operational cost with BSs as the most consuming part of the network [START_REF] Zhou | Energy source aware target cell selection and coverage optimization for power saving in cellular networks[END_REF].

Many approaches are proposed to reduce the energy consumption of cellular networks [START_REF] Suarez | An overview and classification of research approaches in green wireless networks[END_REF]. Motivated by the temporal variation in traffic, several studies propose activating/deactivating resource blocks of BSs such as [START_REF] Al | A novel energy model for renewable energy-enabled cellular networks providing ancillary services to the smart grid[END_REF]. In contrast to switching-off techniques that save energy by shutting down the BS (or switching it to a sleep state), deactivating resource blocks reduce the energy consumption without interrupting the service or causing coverage holes. In addition, mobile operators have already started deploying renewable energy (RE) sources and storage units at the level of BSs [START_REF] Al | Integrating cellular networks, smart grid, and renewable energy: Analysis, architecture, and challenges[END_REF]. This will allow BSs to consume free and clean energy instead of totally relying on the grid energy. However, deciding the number of active resource blocks will become more challenging due to the intermittent nature of RE, the variation of grid energy price and the different users' requirement. In [START_REF] Carreno | Renewable energy use in cellular networks[END_REF], the authors study the trade-off between user satisfaction and the ratio of RE usage in cellular networks. Determining the number of active resource blocks in a single BS powered by RE and power grid is studied in [START_REF] Gong | Energy-aware resource allocation for energy harvesting wireless communication systems[END_REF]. The authors aim at minimizing the average grid energy while satisfying users' Quality of Service (QoS), which is expressed in terms of outage probability. In [START_REF] Chiang | Renewable energy-aware video download in cellular networks[END_REF], the authors propose a new resource allocation policy for RE-powered BSs to reduce the grid power consumption for mobile video download applications. For more studies please refer to [START_REF] Al | Integrating cellular networks, smart grid, and renewable energy: Analysis, architecture, and challenges[END_REF], [START_REF] Al | Renewable energy in cellular networks: A survey[END_REF]. Although these studies succeed to reduce the on-grid energy consumption, they only consider one type of user traffic with a hard constraint on the achievable user rate as a satisfaction metric. In [START_REF] Al | Grid energy consumption of mixed-traffic cellular networks with renewable energy sources[END_REF], we study the trade-off between grid energy consumption and users' satisfaction for a single BS. The study considers several types of users with different requirements, where the satisfaction of a user is calculated based on several utility functions depending on the user's type. However, [START_REF] Al | Grid energy consumption of mixed-traffic cellular networks with renewable energy sources[END_REF] does not provide any algorithm for determining the number of active resource blocks. In [START_REF] Al | A novel energy model for renewable energy-enabled cellular networks providing ancillary services to the smart grid[END_REF], we use activating/deactivating resource blocks to help cellular networks provide the Smart Grid (SG) with ancillary services. However, this study considers only a heuristic to determine the number of active resource blocks.

In this paper, we employ Q-learning in order to determine the number of active resource blocks for a REpowered BS while taking into consideration variation of grid energy cost, availability of RE and traffic variation. As all of these parameters vary based on time, Qlearning is used to extract a common pattern as well as decide the number of active resource blocks for each period of the day to minimize the grid energy cost and maximize the satisfaction of users.

Normalized load, energy and price

Traffic load Harvested energy Electricity price

Fig. 1. Typical patterns of traffic [START_REF] Auer | How much energy is needed to run a wireless network? Wireless Communications[END_REF], grid energy price variation for one day in France [START_REF] Epex | european power exchange spot information[END_REF] and RE generation [START_REF]national renewable energy laboratory[END_REF].

The rest of the paper is structured as follows: In Section II, we detail the system model and explain the considered scenario. The proposed approach is presented in Section III. Results are presented and discussed in Section IV before concluding in Section V.

II. SYSTEM MODEL

We consider a BS powered by a RE source, a battery and connected to the SG. The BS is responsible of serving different types of users, where N HQ , N SQ and N BE are respectively the number of hard-quality (e.g., voice), soft-quality (e.g., video streaming) and besteffort users (e.g., web). The number of users follows the traffic pattern presented in Figure 1. These users are randomly distributed in the targeted area.

A. Users' satisfaction

Utility functions have been used to measure the satisfaction of users in cellular networks with mixed traffic. Chen et al. proposed a unified utility function for various types of traffic using the sigmoid function [START_REF] Chen | Utility-based resource allocation for mixed traffic in wireless networks[END_REF]. The proposed utility is a sigmoid function that represents user satisfaction with respect to allocated resources, where each application is differentiated by specific utility parameters. The unified sigmoid function for different traffic types is expressed as:

u(r) = 1 α + βe -λ(r-R0) + γ (1)
where α, β, λ and γ are pre-determined parameters to determine the shape of the utility function depending on the type of traffic. r is the allocated resources or achieved user rate. R 0 is the resource requirement (or required rate) of the user and represents the point of inflexion. For a given utility function, the utility is concave when the allocated resources are smaller than R 0 , which means that the user strongly requires the resources of R 0 . When the allocated resources are larger than R 0 , the utility function is convex, which means that the user does not strongly require the resources. α, β and γ mainly affect the range of the utility. Moreover, adjusting these parameters for different traffic types is essential to have comparable values of the corresponding utilities.

We consider 3 types of traffic: Hard Quality (HQ), Soft Quality (SQ) and Best Effort (BE). HQ traffic, such as Voice, needs a minimum amount of resources. Allocating more resources for SQ traffic increases its utility until certain limit. BE traffic does not require a specific amount of resources (R 0 = 0). Based on [START_REF] Chen | Utility-based resource allocation for mixed traffic in wireless networks[END_REF], the utility function of HQ, SQ and BE traffic can be expressed as follows:

U HQ (r) = 1 1 + e -λ HQ (r-R0)
(2)

U SQ (r) = 1 1 + e -λ SQ (r-R0) (3)
U BE (r) = 1 1 + βe -λ BE r - 1 1 + β (4)

B. User rate computation

In our work, we consider that the rate is calculated based on 3GPP TR 36.942 [START_REF]3gpp. evolved universal terrestrial radio access (e-utra); radio frequency (rf) system scenarios[END_REF]. The received signal power, P r , to a user from a BS with transmitting power, P t , is calculated as follows:

P r = 10log 10 (P t × 1000) -(Lo + G T -G R ) [dBm]
(5) where Lo is the path loss calculating using Cost 231 extended Hata model as in [START_REF]3gpp. evolved universal terrestrial radio access (e-utra); radio frequency (rf) system scenarios[END_REF]. G T and G R are respectively the gain of the transmitter and receiver. The detected signal-to-noise (SNR) ratio is calculated as:

SN R = P r -N [dB] ( 6
)
where N is the thermal noise power expressed by:

N = 10log 10 (1000×KT 0 ×BW )+N F [dBm]. ( 7
)
where KT 0 is the thermal density noise, BW is the user's allocated bandwidth, and N F is the noise figure. Using the calculated SNR, the user rate is calculated based on [START_REF]3gpp. evolved universal terrestrial radio access (e-utra); radio frequency (rf) system scenarios[END_REF].

C. Energy models 1) Base station power model: The power model of the BS follows the EARTH model [START_REF] Auer | How much energy is needed to run a wireless network? Wireless Communications[END_REF]. The power demand (input power), P in , of a BS consists of a static part P 0 and a load dependent part related to the BS transmitted power P T . Moreover, the power demand depends on the number of active resource blocks. It can be expressed as:

P in = N trx × (P 0 + n n max × ∆P × P T ) (8)
where N trx is the number of transceiver chains of the BS, n is the number of active resource blocks, n max is the maximum available resource blocks and ∆P is the slope of the load dependent power part. In order to control the power demand of a BS, we consider that the BS can activate or deactivate its radio resource blocks.

2) Renewable energy model: RE sources are known to have intermittent nature, i.e., energy is not available all the time. We consider the use of solar panels where RE is generated following the RE pattern shown in Figure 1. As shown by the figure, solar panels do not generate energy during the night. Moreover, the amount of energy generation depends on the the time of the day. Indeed, the exact shape of the pattern also depends on the location of the solar panel and the time of the year.

3) Energy storage model: Energy storage units are important in renewable systems to avoid the loss of excess generated RE as well as to compensate their unavailability. We consider that the storage is characterized by a capacity, which is defined as the maximum amount of energy that can be stored, and efficiency, which characterizes the loss due to the energy losses from (dis)charging. Degradation of battery is not considered in this work.

4) Grid energy: Due to the intermittent nature of RE, connecting the BS to the SG is important to ensure continuity of service. We consider that the grid has no constraint regarding the amount of energy procured by the network. However, the grid notifies the network by the price of grid energy each period (hourly in our case). We also consider that the network does not have any knowledge regarding the future price of energy. An example of a typical grid energy price throughout a day in France can be found in Figure 1.

D. Problem formulation

The objective of this work is to minimize the grid energy cost and maximize the utility of the users. We consider a greedy use of RE, i.e., RE is consumed when it is available, stored when the amount of energy harvested exceeds what the BS needs and battery is used when RE is not available. The energy demand of BS depends on the number of active resource blocks as presented in Section II-C1. Thus, the objective of this work is translated into determining the number of resource blocks as follows:

max[η × ( N HQ k=1 U k + N SQ l=1 U l + N BE m=1 U m ) (N HQ .U max HQ + N SQ .U max SQ + N BE .U max BE ) -(1 -η) × ( E cost E norm cost )] (9)
U K , U l and U m represent respectively the utility functions of HQ user k, SQ user l and BE user m. N HQ , N SQ and N BE represent respectively the number of hard quality, soft quality and best effort users. U max HQ , U max SQ , and U max BR represents the theoretical maximum utilities of HQ, SQ and BE users, respectively. E cost represents the cost of energy during the observation period, and η ∈ [0, 1] is a parameter that controls the trade-off between users satisfaction and energy cost. We calculate E cost as follows:

E cost = E grid × P rice (10)
E grid and P rice represent the consumed grid energy and the price of grid energy, respectively. E norm cost is used to normalize the cost to be between 0 and 1. The consumed grid energy can be calculated as follows:

E grid = max(0, E -E all ) (11)
E is the energy demand of the BS. E all is the allocated energy from the battery and renewable source. Moreover, the maximization problem in Equation 9 is constrained as follows:

n ac ≤ n max (12)
where n ac is the amount of active resources and n max is the maximum available resource blocks. Moreover, the RE causality constraint can be expressed as follows:

E all ≤ E av (13)
where E all represents the allocated RE (during a period) and E av represents the available RE (at the same period).

III. PROPOSED APPROACH In this section, we present the proposed Q-learning algorithm that determines the number of active resource blocks of the BS. The first phase of the algorithm consists of the training phase. During this phase, the BS explores the environment using historical data of traffic load, RE generation and price of the grid energy. These variations change in time following different but specific patterns. In other words, each of the parameters has its specific pattern that is related in time, and Qlearning is used to learn the best action by finding a common pattern. Once this step is complete, the system goes online.

We consider that the state of the BS is represented by periods of the day. The number of states is a trade-off between the accuracy of the decision and the complexity of the problem. On one hand, when a small step duration is considered, the Q-learning algorithm will be able to take more accurate decisions. On the other hand, this will increase the number of states thus, extending the learning time.

We define the set of possible actions A that corresponds to setting the number of active resource blocks.

The number of possible actions is related to the bandwidth of the BS. An episode starts at the beginning of the day and finishes at the end of the day. During each epoch of an episode (period of a day), the BS chooses an action, then stores a quality-value linking the states s ∈ S to the chosen action a ∈ A. The action consists of choosing the number of active resource blocks in order to maximizes the reward r. We define the reward as the weighted-sum of the average utility of users U avg and the cost of the using grid energy, E cost . r = (1 -η)U avg -ηE cost /E norm cost [START_REF] Chen | Utility-based resource allocation for mixed traffic in wireless networks[END_REF] Note that for η = 0, the problem reduces to maximizing the utility of the users without considering the energy cost, whereas for η = 1 the problem becomes minimizing the energy cost.

The reward is then used to update the Q-value locally, Q(s t , a t ), indicating the level of convenience of selecting action a t when in state s t (t represent the current period). The Q-value is updated following the update rule:

Q(s t , a t ) ← Q(s t , a t )+ α[r t + γ max a∈A Q(s t+1 , a t+1 ) -Q(s t , a t )] ( 15
)
where α is the learning rate that represents the speed of convergence, and γ ∈ [0, 1] is the discount factor that determines the current value of the future state costs. During the learning phase, the agent selects the corresponding action based on the -greedy policy, i.e., it selects with probability 1the action associated with the maximum Q-value, and with probability selects a random action (here y is a random variable uniformly distributed between 0 and 1):

a t = arg max a∈A Q(s t , a t ), if y > rand(A), otherwise (16)
By implementing the -greedy policy, the BS would have explored all possible actions and avoided local minima. For more details on Q-learning please refer to [START_REF] Richard S Sutton | Introduction to reinforcement learning[END_REF]. Algorithm 1 details the general Q-learning training phase used in this mechanism.

IV. SIMULATIONS AND RESULTS

We consider a Macro-base station serving a 1200 m radius cell. Mobiles are distributed randomly with equal number of each type of users. The BS operates with 2 GHz carrier frequency and 10 MHz bandwidth. We adopt cost 213 Walfisch-Ikegami for path loss [START_REF]3gpp. evolved universal terrestrial radio access (e-utra); radio frequency (rf) system scenarios[END_REF] and consider the noise figure as 9 dB. The amount of RE generated is 35% of the BS demand when operating at full load. We use the Q-learning algorithm to determine the number of active resource blocks. Patterns of RE generation, price of grid energy and traffic are used for the training phase. Indeed, minor changes in pattern may be observed due to specific events or small errors. Figure 2 presents the evolution of the sum of the maximum Qvalue of each state (case η = 0.2 and maximum number of users = 10). As shown in the figure, the algorithm converges after a large number of episodes. This is not a problem as this step is done offline using patterns derived from historical data. The evolution of the average utility of users and the grid energy cost are presented in Figure 3 and Figure 4, respectively. At the beginning of the training phase, the average utility and the cost take wide range of values. Then the range (for each of utility and cost) starts to shrink. Indeed, the minor changes of average utility and cost after a large number of episodes is due to the random distribution of users.

Figure 5 presents the number of resource blocks in each period (hour) of the day when the maximum number of users is 10. From the figure we can see that the highest number of active resource blocks is observed at the time where traffic is high (19-23). Although we have high traffic at time 21, we observe lower number of active resource blocks. This is because the price of grid energy is still high and stored RE has been used. After time 21, we see that the number of active RBs increases again. This is due to the fact that the price of the grid energy decreased. It is worth noting that Figure 5 is one of the possible solutions. By repeating the training, we have noticed several possible solutions. These solutions are slightly different in terms of the activated radio resource blocks but lead to almost the same values of average utility and grid energy cost.

To study the effect of parameter η, we present the variation of cost gain, with respect to the case of no RE, and average utility of users in Figure 6 and Figure 7, respectively. We can notice that no significant change in the value of utility or cost for small values of η. For a specific number of users, the cost gain starts to increase and the average utility of users starts to decrease after a certain value of η (e.g., η = 0.6 for 10 users). This threshold decreases with the increase in the maximum number of users. An example of the tradeoff (case of maximum of 10 users) is shown in Figure 8.

Table II shows the utility of users and cost of grid energy for the proposed algorithm and existing algorithms (maximum number of users is 20). For the existing al- gorithms, we consider: 1) Reference: BS operates at the maximum number of available resource blocks without using RE; 2) Greedy: only RE is used in a greedy way (use when available); 3) Traffic, RE and Price of grid energy (TRP) aware algorthim: it determines the number of active resource blocks by discretization the state of a BS based on RE generation, price of grid energy and traffic, similar algorithms are found in [START_REF] Al | Classification of renewable energy scenarios and objectives for cellular networks[END_REF] and [START_REF] El-Amine | Services kpi-based energy management strategies for green wireless networks[END_REF]. From Table II, we can see that the best utility is achieved by the reference and greedy, since all the resource blocks are activated. However, the price is very high compared with other algorithms. TRP reduces the cost of grid energy, but this comes with a price in terms of average utility of users. The proposed algorithm (η = 0.2) achieves significant reduction in the cost with better value of average utility than TRP. The proposed algorithm (η = 0.8) further reduces the cost but with the worst utility among all algorithms. In summary, the proposed algorithm (η = 0.2) achieves the best tradeoff with large reduction in the cost and slight decrease in the user utility.

V. CONCLUSION

With the increase in traffic requirements and demand, satisfying users and minimizing the operational cost have became two important objectives to be achieved in future cellular networks. In this paper, we study the problem of determining the number of resource blocks that combines these two objectives. We consider different types of users with different requirements. Motivated by the fact that parameters of the problem such as renewable energy generation, traffic load and price of grid energy vary with time following specific patterns, we use Q-learning to determine the hourly number of active resource block that fits these patterns. Results show that Q-learning can find a good tradeoff where significant cost reduction is achieved with negligible degradation in users' satisfaction.

Fig. 2 .Fig. 3 .

 23 Fig. 2. Convergence of the Q-Learning algorithm for η = 0.2.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Evolution of grid energy cost for η = 0.2

Fig. 6 .Fig. 7 .

 67 Fig. 6. Energy cost gain with respect to η for several numbers of maximum users.

Fig. 8 .

 8 Fig. 8. Trade-off between cost gain and average utility of users with respect to η in case of maximum of 10 users.

  Table I summarizes the parameters considered in the system.

	Algorithm 1 : Q-Learning Algorithm: Training phase
	Initialize Q(s,a) to zero for all s ∈ S, a ∈ A(s)
	repeat(for each episode):
	Initialize s
	repeat(for each time t):
	Choose a t using -greedy policy in (16)
	Compute r t
	Update Q(s t , a t ) using the update rule in (15)
	s t ← s t+1
	until the end of the day
	until convergence
	TABLE I
	VALUES AND ASSUMPTIONS.
	Parametters	Values and assumptions
	Number of sectors in a BS	3
	Carrier frequency	2GHz
	Number of resource blocks	50
	Storage size	4000 Wh
	Cell radius	1200 m
	Path loss	Cost 231 extended Hata
		model
	GT	15 dBi
	GR	0 dBi
	Noise figure	9 dB
	BS power model	EARTH
	Environment	Urban
	Maximum number of users	10,20,30,40,50,60

TABLE II UTILITY

 II AND COST OF SIMULATED ALGORITHMS.

				1
				0.9
				0.8
			Normalized gain	0.4 0.5 0.6 0.7
				0.3
				0.2	Average utility
					Cost gain
				0.1
				0	0.2	0.4	0.6	0.8	1
						2
	Algorithm	Uaverage Ecostmean
	Reference	0.89	1.491
	Greedy	0.89	1.05
	TRP	0.78	0.745
	Qlearning (η = 0.2)	0.85	0.29
	Qlearning (η = 0.8)	0.6	0.22