Jean-Guillaume Dumas
email: jean-guillaume.dumas@imag.fr.

Dominique Duval
email: dominique.duval@imag.fr.

Burak Ekici
email: burak.ekici@imag.fr.

Damien Pous
email: damien.pous@ens-lyon.fr.

Jean-Claude Reynaud
email: claude.reynaud@imag.fr.

Hilbert-Post completeness for the state and the exception effects

A theory is complete if it does not contain a contradiction, while all of its proper extensions do. In this paper, first we introduce a relative notion of syntactic completeness; then we prove that adding exceptions to a programming language can be done in such a way that the completeness of the language is not made worse. These proofs are formalized in a logical system which is close to the usual syntax for exceptions, and they have been checked with the proof assistant Coq.

Introduction

In computer science, an exception is an abnormal event occurring during the execution of a program. A mechanism for handling exceptions consists of two parts: an exception is raised when an abnormal event occurs, and it can be handled later, by switching the execution to a specific subprogram. Such a mechanism is very helpful, but it is difficult for programmers to reason about it. A difficulty for reasoning about programs involving exceptions is that they are computational effects, in the sense that their syntax does not look like their interpretation:typically, a piece of program with arguments in X that returns a value in Y is interpreted as a function from X + E to Y + E where E is the set of exceptions. On the one hand, reasoning with f : X → Y is close to the syntax, but it is error-prone because it is not sound with respect to the semantics. On the other hand, reasoning with f : X + E → Y + E is sound but it loses most of the interest of the exception mechanism, where the propagation of exceptions is implicit: syntactically, f : X → Y may be followed by any g : Y → Z, since the mechanism of exceptions will take care of propagating the exceptions raised by f , if any. Another difficulty for reasoning about programs involving exceptions is that the handling mechanism is encapsulated in a try-catch block, while the behaviour of this mechanism is easier to explain in two parts (see for instance [START_REF] Gosling | The Java Language Specification, Third Edition[END_REF]Ch. 14] for Java or [3, §15] for C++): the catch part may recover from exceptions, so that its interpretation may be any f : X + E → Y + E, but the try-catch block must propagate exceptions, so that its interpretation is determined by some f : X → Y + E.

In [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF] we defined a logical system for reasoning about states and exceptions and we used it for getting certified proofs of properties of programs in computer algebra, with an application to exact linear algebra. This logical system is called the decorated logic for states and exceptions. Here we focus on exceptions. The decorated logic for exceptions deals with f : X → Y , without any mention of E, however it is sound thanks to a classification of the terms and the equations. Terms are classified, as in a programming language, according to the way they may interact with exceptions: a term either has no interaction with exceptions (it is "pure"), or it may raise exceptions and must propagate them, or it is allowed to catch exceptions (which may occur only inside the catch part of a try-catch block). The classification of equations follows a line that was introduced in [START_REF] Domínguez | Diagrammatic logic applied to a parameterisation process[END_REF]: besides the usual "strong" equations, interpreted as equalities of functions, in the decorated logic for exceptions there are also "weak" equations, interpreted as equalities of functions on non-exceptional arguments. This logic has been built so as to be sound, but little was known about its completeness. In this paper we prove a novel completeness result: the decorated logic for exceptions is relatively Hilbert-Post complete, which means that adding exceptions to a programming language can be done in such a way that the completeness of the language is not made worse. For this purpose, we first define and study the novel notion of relative Hilbert-Post completeness, which seems to be a relevant notion for the completeness of various computational effects: indeed, we prove that this notion is preserved when combining effects. Practically, this means that we have defined a decorated framework where reasoning about programs with and without exceptions are equivalent, in the following sense: if there exists an unprovable equation not contradicting the given decorated rules, then this equation is equivalent to a set of unprovable equations of the pure sublogic not contradicting its rules.

Informally, in classical logic, a consistent theory is one that does not contain a contradiction and a theory is complete if it is consistent, and none of its proper extensions is consistent. Now, the usual ("absolute") Hilbert-Post completeness, also called Post completeness, is a syntactic notion of completeness which does not use any notion of negation, so that it is well-suited for equational logic. In a given logic L, we call theory a set of sentences which is deductively closed: everything you can derive from it (using the rules of L) is already in it. Then, more formally, a theory is (Hilbert-Post) consistent if it does not contain all sentences, and it is (Hilbert-Post) complete if it is consistent and if any sentence which is added to it generates an inconsistent theory [START_REF] Tarski | III On some fundamental concepts in mathematics[END_REF]Def. 4].

All our completeness proofs have been verified with the Coq proof assistant.

First, this shows that it is possible to formally prove that programs involving exceptions comply to their specifications. Second, this is of help for improving the confidence in the results. Indeed, for a human prover, proofs in a decorated logic require some care: they look very much like familiar equational proofs, but the application of a rule may be subject to restrictions on the decoration of the premises of the rule. The use of a proof assistant in order to check that these unusual restrictions were never violated has thus proven to be quite useful.

Then, many of the proofs we give in this paper require a structural induction.

There, the correspondence between our proofs and their Coq counterpart was eased, as structural induction is also at the core of the design of Coq.

A major difficulty for reasoning about programs involving exceptions, and more generally computational effects, is that their syntax does not look like their interpretation: typically, a piece of program from X to Y is not interpreted as a function from X to Y , because of the effects. The best-known algebraic approach for dealing with this problem has been initiated by Moggi: an effect is associated to a monad T , in such a way that the interpretation of a program from X to Y is a function from X to T (Y ) [START_REF] Moggi | Notions of Computation and Monads[END_REF]: typically, for exceptions, T (Y ) = Y + E. Other algebraic approaches include effect systems [START_REF] Lucassen | Polymorphic effect systems[END_REF], Lawvere theories [START_REF] Plotkin | Notions of Computation Determine Monads[END_REF], algebraic handlers [START_REF] Plotkin | Handlers of Algebraic Effects[END_REF], comonads [START_REF] Uustalu | Comonadic Notions of Computation[END_REF][START_REF] Petricek | Coeffects: a calculus of context-dependent computation[END_REF], dynamic logic [START_REF] Mossakowski | A generic complete dynamic logic for reasoning about purity and effects[END_REF], among others. Some completeness results have been obtained, for instance for (global) states [START_REF] Pretnar | The Logic and Handling of Algebraic Effects[END_REF] and for local states [START_REF] Staton | Completeness for Algebraic Theories of Local State[END_REF]. The aim of these approaches is to extend functional languages with tools for programming and proving sideeffecting programs; implementations include Haskell [START_REF] Benton | Monads and Effects[END_REF], Idris [START_REF] Idris | The Effects Tutorial[END_REF], Eff [START_REF] Bauer | Programming with algebraic effects and handlers[END_REF], while Ynot [START_REF] Ynot | The Ynot Project[END_REF] is a Coq library for writing and verifying imperative programs.

Differently, our aim is to build a logical system for proving properties of some families of programs written in widely used non-functional languages like Java or C++ 1 . The salient features of our approach are that:

(1) The syntax of our logic is kept close to the syntax of programming languages. This is made possible by starting from a simple syntax without effect and by adding decorations, which often correspond to keywords of the languages, for taking the effects into account.

(2) We consider exceptions in two settings, the programming language and the core language. This enables for instance to separate the treatment, in proofs, of the matching between normal or exceptional behavior from the actual recovery after an exceptional behavior.

In Section 2 we introduce a relative notion of Hilbert-Post completeness in a logic L with respect to a sublogic L 0 . Then in Section 3 we prove the relative Hilbert-Post completeness of a theory of exceptions based on the usual throw and try-catch statement constructors. We go further in Section 4 by establishing the relative Hilbert-Post completeness of a core theory for exceptions with individualized TRY and CATCH statement constructors, which is useful for expressing the behaviour of the try-catch blocks. All our completeness proofs have been verified with the Coq proof assistant and we therefore give the main ingredients of the framework used for this verification and the correspondence between our Coq package and the theorems and propositions of this paper in Section 5.

Relative Hilbert-Post completeness

Each logic in this paper comes with a language, which is a set of formulas, and with deduction rules. Deduction rules are used for deriving (or generating) theorems, which are some formulas, from some chosen formulas called axioms. A theory T is a set of theorems which is deductively closed, in the sense that every theorem which can be derived from T using the rules of the logic is already in T . We describe a set-theoretic intended model for each logic we introduce; the rules of the logic are designed so as to be sound with respect to this intended model. Given a logic L, the theories of L are partially ordered by inclusion. There is a maximal theory T max , where all formulas are theorems. There is a minimal theory T min , which is generated by the empty set of axioms. For all theories T and T ′ , we denote by T + T ′ the theory generated from T and T ′ .

Example 2.1. With this point of view there are many different equational logics, with the same deduction rules but with different languages, depending on the definition of terms. In an equational logic, formulas are pairs of parallel terms (f, g) : X → Y and theorems are equations f ≡ g : X → Y . Typically, the language of an equational logic may be defined from a signature (made of sorts and operations). The deduction rules are such that the equations in a theory form a congruence, i.e., an equivalence relation compatible with the structure of the terms. For instance, we may consider the logic "of naturals" L nat , with its language generated from the signature made of a sort N , a constant 0 : 1 → N and an operation s : N → N . For this logic, the minimal theory is the theory "of naturals" T nat , the maximal theory is such that s k ≡ s ℓ and s k • 0 ≡ s ℓ • 0 for all natural numbers k and ℓ, and (for instance) the theory "of naturals modulo 6" T mod6 can be generated from the equation s 6 ≡ id N . We consider models of equational logics in sets: each type X is interpreted as a set (still denoted X), which is a singleton when X is 1, each term f : X → Y as a function from X to Y (still denoted f : X → Y ), and each equation as an equality of functions. Definition 2.2. Given a logic L and its maximal theory T max , a theory T is consistent if T = T max , and it is Hilbert-Post complete if it is consistent and if any theory containing T coincides with T max or with T .

Example 2.3. In Example 2.1 we considered two theories for the logic L nat : the theory "of naturals" T nat and the theory "of naturals modulo 6" T mod6 . Since both are consistent and T mod6 contains T nat , the theory T nat is not Hilbert-Post complete. A Hilbert-Post complete theory for L nat is made of all equations but s ≡ id N , it can be generated from the axioms s•0 ≡ 0 and s•s ≡ s.

If a logic L is an extension of a sublogic L 0 , each theory T 0 of L 0 generates a theory F (T 0 ) of L. Conversely, each theory T of L determines a theory G(T ) of L 0 , made of the theorems of T which are formulas of L 0 , so that G(T max ) = T max ,0 . The functions F and G are monotone and they form a Galois connection, denoted F ⊣ G: for each theory T of L and each theory T 0 of L 0 we have F (T 0 ) ⊆ T if and only if T 0 ⊆ G(T ). It follows that T 0 ⊆ G(F (T 0 )) and F (G(T )) ⊆ T . Until the end of Section 2, we consider: a logic L 0 , an extension L of L 0 , and the associated Galois connection F ⊣ G.

Definition 2.4. A theory T ′ of L is L 0 -derivable from a theory T of L if T ′ = T + F (T ′ 0 ) for some theory T ′ 0 of L 0 . A theory T of L is (relatively) Hilbert-Post complete with respect to L 0 if it is consistent and if any theory of L containing T is L 0 -derivable from T .
Each theory T is L 0 -derivable from itself, as T = T + F (T min,0 ), where T min,0 is the minimal theory of L 0 . In addition, Theorem 2.6 shows that relative completeness lifts the usual "absolute" completeness from L 0 to L, and Proposition 2.7 proves that relative completeness is well-suited to the combination of effects.

Lemma 2.5. For each theory T of L, a theory T ′ of L is L 0 -derivable from T if and only if T ′ = T + F (G(T ′ )). As a special case, T max is L 0 -derivable from T if and only if T max = T + F (T max ,0 ). A theory T of L is Hilbert-Post complete with respect to L 0 if and only if it is consistent and every theory

T ′ of L containing T is such that T ′ = T + F (G(T ′ )). Proof. Clearly, if T ′ = T + F (G(T ′ )) then T ′ is L 0 -derivable from T . So, let T ′
0 be a theory of L 0 such that T ′ = T + F (T ′ 0 ), and let us prove that T ′ = T + F (G(T ′ )). For each theory T ′ we know that F (G(T ′ )) ⊆ T ′ ; since here T ⊆ T ′ we get T + F (G(T ′ )) ⊆ T ′ . Conversely, for each theory T ′ 0 we know that

T ′ 0 ⊆ G(F (T ′ 0 )) and that G(F (T ′ 0 )) ⊆ G(T ) + G(F (T ′ 0 )) ⊆ G(T + F (T ′ 0 )), so that T ′ 0 ⊆ G(T + F (T ′ 0
)); since here T ′ = T + F (T ′ 0 ) we get first T ′ 0 ⊆ G(T ′ ) and then T ′ ⊆ T + F (G(T ′ )). Then, the result for T max comes from the fact that G(T max ) = T max ,0 . The last point follows immediately. Theorem 2.6. Let T 0 be a theory of L 0 and T = F (T 0 ). If T 0 is Hilbert-Post complete (in L 0 ) and T is Hilbert-Post complete with respect to L 0 , then T is Hilbert-Post complete (in L).

Proof. Since T is complete with respect to L 0 , it is consistent. Since T = F (T 0 ) we have T 0 ⊆ G(T ). Let T ′ be a theory such that T ⊆ T ′ . Since T is complete with respect to L 0 , by Lemma 2.5 we have

T ′ = T + F (T ′ 0 ) where T ′ 0 = G(T ′ ). Since T ⊆ T ′ , T 0 ⊆ G(T ) and T ′ 0 = G(T ′ ), we get T 0 ⊆ T ′ 0 . Thus, since T 0 is complete, either T ′ 0 = T 0 or T ′ 0 = T max ,0 ; let us check that then either T ′ = T or T ′ = T max . If T ′ 0 = T 0 then F (T ′ 0 ) = F (T 0 ) = T , so that T ′ = T + F (T ′ 0 ) = T . If T ′ 0 = T max ,0 then F (T ′ 0 ) = F (T max ,0
); since T is complete with respect to L 0 , the theory T max is L 0 -derivable from T , which implies (by Lemma 2.5) that

T max = T + F (T max ,0 ) = T ′ .
Proposition 2.7. Let L 1 be an intermediate logic between L 0 and L, let F 1 ⊣ G 1 and F 2 ⊣ G 2 be the Galois connections associated to the extensions L 1 of L 0 and L of L 1 , respectively. Let T 1 = F 1 (T 0 ). If T 1 is Hilbert-Post complete with respect to L 0 and T is Hilbert-Post complete with respect to L 1 then T is Hilbert-Post complete with respect to L 0 .

Proof. This is an easy consequence of the fact that

F = F 2 • F 1 .
Corollary 2.10 provides a characterization of relative Hilbert-Post completeness which is used in the next Sections and in the Coq implementation.

Definition 2.8. For each set E of formulas let Th(E) be the theory generated by E; and when E = {e} let Th(e) = Th({e}). Then two sets

E 1 , E 2 of formulas are T -equivalent if T + Th(E 1 ) = T + Th(E 2 ); and a formula e of L is L 0 -derivable from a theory T of L if {e} is T -equivalent to E 0 for some set E 0 of formulas of L 0 . Proposition 2.9. Let T be a theory of L. Each theory T ′ of L containing T is L 0 -derivable from T if and only if each formula e in L is L 0 -derivable from T .
Proof. Let us assume that each theory T ′ of L containing T is L 0 -derivable from T . Let e be a formula in L, let T ′ = T + Th(e), and let T ′ 0 be a theory of L 0 such that

T ′ = T + F (T ′ 0 ). The definition of Th(-) is such that Th(T ′ 0 ) = F (T ′ 0 ), so that we get T + Th(e) = T + Th(E 0 ) where E 0 = T ′ 0 . Conversely, let us assume that each formula e in L is L 0 -derivable from T . Let T ′ be a theory containing T . Let T ′′ = T + F (G(T ′ )), so that T ⊆ T ′′ ⊆ T ′ (because F (G(T ′ )) ⊆ T ′ for any T ′ ).
Let us consider an arbitrary formula e in T ′ , by assumption there is a set E 0 of formulas of L 0 such that T + Th(e) = T + Th(E 0 ). Since e is in T ′ and T ⊆ T ′ we have T + Th(e) ⊆ T ′ , so that T + Th(E 0 ) ⊆ T ′ . It follows that E 0 is a set of theorems of T ′ which are formulas of L 0 , which means that E 0 ⊆ G(T ′ ), and consequently Th(E 0 ) ⊆ F (G(T ′ )), so that T + Th(E 0 ) ⊆ T ′′ . Since T + Th(e) = T + Th(E 0 ) we get e ∈ T ′′ . We have proved that T ′ = T ′′ , so that T ′ is L 0 -derivable from T .

Corollary 2.10. A theory T of L is Hilbert-Post complete with respect to L 0 if and only if it is consistent and for each formula e of L there is a set E 0 of formulas of L 0 such that {e} is T -equivalent to E 0 .

Completeness for exceptions

Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. E.g., one can easily and simultaneously compute dynamic evaluation in exact linear algebra using exceptions [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF]. There, we proposed to deal with exceptions as a decorated effect: a term f : X → Y is not interpreted as a function f : X → Y unless it is pure. A term which may raise an exception is instead interpreted as a function f : X → Y + E where "+" is the disjoint union operator and E is the set of exceptions. In this section, we prove the relative Hilbert-Post completeness of the decorated theory of exceptions in Theorem 3.5.

As in [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF], decorated logics for exceptions are obtained from equational logics by classifying terms. Terms are classified as pure terms or propagators, which is expressed by adding a decoration or superscript, respectively (0) or (1); decoration and type information about terms may be omitted when they are clear from the context or when they do not matter. All terms must propagate exceptions, and propagators are allowed to raise an exception while pure terms are not. The fact of catching exceptions is hidden: it is embedded into the try-catch construction, as explained below. In Section 4 we consider a translation of the try-catch construction in a more elementary language where some terms are catchers, which means that they may recover from an exception, i.e., they do not have to propagate exceptions.

Let us describe informally a decorated theory for exceptions and its intended model. Each type X is interpreted as a set, still denoted X. The intended model is described with respect to a set E called the set of exceptions, which does not appear in the syntax. A pure term u (0) : X → Y is interpreted as a function u : X → Y and a propagator a (1) : X → Y as a function a : X → Y + E; equations are interpreted as equalities of functions. There is an obvious conversion from pure terms to propagators, which allows to consider all terms as propagators whenever needed; if a propagator a (1) : X → Y "is" a pure term, in the sense that it has been obtained by conversion from a pure term, then the function a : X → Y + E is such that a(x) ∈ Y for each x ∈ X. This means that exceptions are always propagated: the interpretation of (b • a) (1) : X → Z where a (1) : X → Y and b (1) :

Y → Z is such that (b • a)(x) = b(a(x)) when a(x)
is not an exception and (b • a)(x) = e when a(x) is the exception e (more precisely, the composition of propagators is the Kleisli composition associated to the monad X + E [13, § 1]). Then, exceptions may be classified according to their name, as in [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF]. Here, in order to focus on the main features of the proof of completeness, we assume that there is only one exception name. Each exception is built by encapsulating a parameter. Let P denote the type of parameters for exceptions. The fundamental operations for raising exceptions are the propagators throw More precisely, first the definition of the monadic equational logic L eq is recalled in Fig. 1, (as in [START_REF] Moggi | Notions of Computation and Monads[END_REF], this terminology might be misleading: the logic is called monadic because all its operations are have exactly one argument, this is unrelated to the use of the monad of exceptions).

Terms are closed under composition:

u k • • • • • u1 : X0→X k for each (ui : Xi-1→Xi) 1≤i≤k , and idX : X→X when k = 0 Rules: (equiv) u u ≡ u u ≡ v v ≡ u u ≡ v v ≡ w u ≡ w (subs) u : X → Y v1 ≡ v2 : Y → Z v1 • u ≡ v2 • u (repl) v1 ≡ v2 : X → Y w : Y → Z w • v1 ≡ w • v2 Empty type 0 with terms [ ]Y : 0 → Y and rule: (initial) u : 0 → Y u ≡ [ ]Y
Figure 1: Monadic equational logic L eq (with empty type)

A monadic equational logic is made of types, terms and operations, where all operations are unary, so that terms are simply paths. This constraint on arity will make it easier to focus on the completeness issue. For the same reason, we also assume that there is an empty type 0, which is defined as an initial object : for each Y there is a unique term [ ] Y : 0 → Y and each term u (0) :

Y → 0 is the inverse of [ ] (0)
Y . In the intended model, 0 is interpreted as the empty set. Then, the monadic equational logic L eq is extended to form the decorated logic for exceptions L exc by applying the rules in Fig. 2, with the following intended meaning:

• (initial 1 ): the term [ ] Y is unique as a propagator, not only as a pure term.

• (propagate): exceptions are always propagated.

• (recover): the parameter used for throwing an exception may be recovered.

• (try): equations are preserved by the exceptions mechanism.

• (try 0 ): pure code inside try never triggers the code inside catch.

• (try 1 ): code inside catch is executed when an exception is thrown inside try.

The theory of exceptions T exc is the theory of L exc generated from some arbitrary consistent theory T eq of L eq ; with the notations of Section 2, T exc = F (T eq ).

The soundness of the intended model follows: see [8, §5.1] and [START_REF] Dumas | A duality between exceptions and states[END_REF], which are based on the description of exceptions in Java [START_REF] Gosling | The Java Language Specification, Third Edition[END_REF]Ch. 14] or in C++ [3, §15].

Example 3.1. Using the naturals for P and the successor and predecessor functions (resp. denoted s and p) we can prove, e.g., that try(s(throw 3))catch(p) is equivalent to 2. Indeed, first the rule (propagate) shows that s(throw 3)) ≡ throw 3, then the rules (try) and (try 1 ) rewrite the given term into p(3). Now, in order to prove the completeness of the decorated theory for exceptions, we follow a classical method (see, e.g., [ Y : P → Y for each type Y , (try(a)catch(b)) (1) : X → Y for each a (1) : X → Y and b (1) : P → Y , and

(a k • • • • • a1) (max(d 1 ,...,d k )) : X0 → X k for each (a (d i ) i : Xi-1 → Xi) 1≤i≤k
with conversion from u (0) : X → Y to u (1) : X → Y Rules:

(equiv), (subs), (repl) for all decorations (initial1) a (1) :

0 → Y a ≡ [ ]Y (recover) u (0) 1 , u (0) 2 : X → P throwY • u1 ≡ throwY • u2 u1 ≡ u2 (propagate) a (1) : X → Y a • throwX ≡ throwY (try) a (1) 1 ≡ a (1)
2 : X → Y b (1) : For each a (1) : X → Y , either there is a pure term u (0) : X → Y such that a ≡ u or there is a pure term u (0) : X → P such that a ≡ throw Y •u.

P → Y try(a1)catch(b) ≡ try(a2)catch(b) (try0) u (0) : X → Y b (1) : P → Y try(u)catch(b) ≡ u (try1) u (0) : X → P b (1) : P → Y try(throwY • u)catch(b) ≡ b • u
Proof. The proof proceeds by structural induction. If a is pure the result is obvious, otherwise a can be written in a unique way as a = b • op • v where v is pure, op is either throw Z for some Z or try(c)catch(d) for some c and d, and b is the remaining part of a. If a = b (1) • throw Z • v (0) , then by (propagate) a ≡ throw Y • v (0) . Otherwise, a = b (1) • (try(c (1) )catch(d (1) )) • v (0) , then by induction we consider two cases.

• If c ≡ w (0) then by (try 0 ) a ≡ b (1) •w (0) •v (0) and by induction we consider two subcases:

if b ≡ t (0) then a ≡ (t • w • v) (0) and if b ≡ throw Y • t (0) then a ≡ throw Y • (t • w • v) (0) . • If c ≡ throw Z • w (0)
then by (try 1 ) a ≡ b (1) • d (1) • w (0) • v (0) and by induction we consider two subcases:

if b • d ≡ t (0) then a ≡ (t • w • v) (0) and if b • d ≡ throw Y • t (0) then a ≡ throw Y • (t • w • v) (0) .
Thanks to Proposition 3.2, the study of equations in the logic L exc can be restricted to pure terms and to propagators of the form throw Y • v where v is pure.

Proposition 3.3. For all v (0) 1 , v (0) 2 : X → P let a (1) 1 = throw Y •v 1 : X → Y and a (1) 2 = throw Y • v 2 : X → Y . Then a (1) 1 ≡ a (1) 2 is T exc -equivalent to v (0) 1 ≡ v (0) 2 . Proof. Clearly, if v 1 ≡ v 2 then a 1 ≡ a 2 . Conversely, if a 1 ≡ a 2 , i.e., if throw Y • v 1 ≡ throw Y • v 2 , then by rule (recover) it follows that v 1 ≡ v 2 .
In the intended model, for all v (0)

1 : X → P and v (0) 2 : X → Y , it is impossible to have throw Y (v 1 (x)) = v 2 (x) for some x ∈ X, because throw Y (v 1 (x)) is in the E summand and v 2 (x) in the Y summand of the disjoint union Y + E.
This means that the functions throw Y • v 1 and v 2 are distinct, as soon as their domain X is a non-empty set. For this reason, it is sound to make the following Assumption 3.4.

Assumption 3.4. In the logic L exc , the type of parameters P is non-empty, and for all v (0)

1 : X → P and v (0) 2 : X → Y with X non-empty, let a (1) 1 = throw Y •v 1 : X → Y . Then a (1) 1 ≡ v (0) 2 is T exc -equivalent to T max ,0 .
Theorem 3.5. Under Assumption 3.4, the theory of exceptions T exc is Hilbert-Post complete with respect to the pure sublogic L eq of L exc .

Proof. Using Corollary 2.10, the proof relies upon Propositions 3.2 and 3.3. The theory T exc is consistent, because (by soundness) it cannot be proved that throw

P ≡ id (0) P . Now, let us consider an equation between terms with domain X and let us prove that it is T exc -equivalent to a set of pure equations. When X is non-empty, Propositions 3.2 and 3.3, together with Assumption 3.4, prove that the given equation is T exc -equivalent to a set of pure equations. When X is empty, then all terms from X to Y are equivalent to [ ] Y so that the given equation is T exc -equivalent to the empty set of pure equations.

Completeness of the core language for exceptions

In this section, following [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF], we describe a translation of the language for exceptions from Section 3 in a core language with catchers. Thereafter, in Theorem 4.7, we state the relative Hilbert-Post completeness of this core language.

Let us call the usual language for exceptions with throw and try-catch, as described in Section 3, the programmers' language for exceptions. The documentation on the behaviour of exceptions in many languages (for instance in Java [START_REF] Gosling | The Java Language Specification, Third Edition[END_REF]) makes use of a core language for exceptions which is studied in [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF].

In this language, the empty type plays an important role and the fundamental operations for dealing with exceptions are tag (1) : P → 0 for encapsulating a parameter inside an exception and untag (2) : 0 → P for recovering its parameter from any given exception. The new decoration (2) corresponds to catchers: a catcher may recover from an exception, it does not have to propagate it. Moreover, the equations also are decorated: in addition to the equations '≡' as in Section 3, now called strong equations, there are weak equations denoted '∼'. As in Section 3, a set E of exceptions is chosen; the interpretation is extended as follows: each catcher f (2) : X → Y is interpreted as a function f : X + E → Y + E, and there is an obvious conversion from propagators to catchers; the interpretation of the composition of catchers is straightforward, and it is compatible with the Kleisli composition for propagators. Weak and strong equations coincide on propagators, where they are interpreted as equalities, but they differ on catchers: f (2) ∼ g (2) : X → Y means that the functions f, g : X + E → Y + E coincide on X, but maybe not on E. The interpretation of tag (1) : P → 0 is an injective function tag : P → E and the interpretation of untag (2) : 0 → P is a function untag : E → P + E such that untag(tag(p)) = p for each parameter p. Thus, the fundamental axiom relating tag (1) and untag (2) is the weak equation untag • tag ∼ id P .

Pure part: the logic Leq with a distinguished type P Decorated terms: tag (1) : P → 0, untag (2) : 0 → P , and

(f k • • • • • f1) (max(d 1 ,...,d k )) : X0 → X k for each (f (d i ) i : Xi-1 → Xi) 1≤i≤k
with conversions from f (0) to f (1) and from f (1) to f (2) Rules:

(equiv≡), (subs≡), (repl≡) for all decorations (equiv∼), (repl∼) for all decorations, (subs∼) only when h is pure More precisely, the decorated logic for the core language for exceptions L exc-core is defined in Fig. 3 as an extension of the monadic equational logic L eq . There is an obvious conversion from strong to weak equations (≡-to-∼), and in addition strong and weak equations coincide on propagators by rule (eq 1 ). Two catchers f

(empty∼) f : 0 → Y f ∼ [ ]Y (≡-to-∼) f ≡ g f ∼ g (ax) untag • tag ∼ id P (eq1) f (d 1 ) 1 ∼ f (d 2 ) 2 f1 ≡ f2 only when d1 ≤ 1 and d2 ≤ 1 (eq2) f1, f2 : X → Y f1 ∼ f2 f1 • [ ]X ≡ f2 • [ ]X f1 ≡ f2 (eq3) f1, f2 : 0 → X f1 • tag ∼ f2 • tag f1 ≡ f2
(2) 1 , f (2) 2
: X → Y behave in the same way on exceptions if and only if

f 1 • [ ] X ≡ f 2 • [ ] X : 0 → Y ,
where [ ] X : 0 → X builds a term of type X from any exception. Then rule (eq 2 ) expresses the fact that weak and strong equations are related by the property that

f 1 ≡ f 2 if and only if f 1 ∼ f 2 and f 1 • [ ] X ≡ f 2 • [ ] X .
This can also be expressed as a pair of weak equations:

f 1 ≡ f 2 if and only if f 1 ∼ f 2 and f 1 • [ ] X • tag ∼ f 2 • [ ] X • tag by rule (eq 3 ).
The core theory of exceptions T exc-core is the theory of L exc-core generated from the theory T eq of L eq . Some easily derived properties are stated in Lemma 4.1; which will be used repeatedly. 1. For all pure terms u

(0) 1 , u (0)
2 : X → P , the equation

u 1 ≡ u 2 is T exc-core -equivalent to tag • u 1 ≡ tag • u 2 and also to untag • tag • u 1 ≡ untag • tag • u 2 .
2. For all pure terms u (0) : X → P , v (0) : X → 0, the equation u

≡ [ ] P • v is T exc-core -equivalent to tag • u ≡ v.
Proof.

1. Implications from left to right are clear. Conversely, if untag•tag• u 1 ≡ untag • tag • u 2 , then using the axiom (ax) and the rule (subs ∼ ) we get u 1 ∼ u 2 . Since u 1 and u 2 are pure this means that u 1 ≡ u 2 .

First, since tag • [ ]

P : 0 → 0 is a propagator we have tag • [ ] P ≡ id 0 . Now, if u ≡ [ ] P • v then tag • u ≡ tag • [ ] P • v ≡ v. Conversely, if tag • u ≡ v then tag • u ≡ tag • [ ] P • v, and by Point 1 this means that u ≡ [ ] P • v.
The operation untag in the core language can be used for decomposing the try-catch construction in the programmer's language in two steps: a step for catching the exception, which is nested into a second step inside the try-catch block: this corresponds to a translation of the programmer's language in the core language, as in [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF], which is reminded below; then Proposition 4.2 proves the correctness of this translation. In view of this translation we extend the core language with:

• for each b (1) : P → Y , a catcher (CATCH(b)) (2)

: Y → Y such that CATCH(b) ∼ id Y and CATCH(b) • [ ] Y ≡ b • untag: if the argument of CATCH(b)
is non-exceptional then nothing is done, otherwise the parameter p of the exception is recovered and b(p) is ran.

• for each a (1) : X → Y and k (2) : Y → Y , a propagator (TRY(a, k)) (1) : X → Y such that TRY(a, k) ∼ k • a: thus TRY(a, k) behaves as k • a on non-exceptional arguments, but it does always propagate exceptions.

Then, a translation of the programmer's language of exceptions in the core language is easily obtained: for each type Y , throw

Y = [ ] Y • tag : P → Y . and for each a (1) : X → Y , b (1) : P → Y , (try(a)catch(b)) (1) = TRY(a, CATCH(b)) : X → Y . This translation is correct: see Proposition 4.2. Proposition 4.2. If the pure term [ ] Y : 0 → Y is a monomorphism with respect to propagators for each type Y , the above translation of the programmers' language for exceptions in the core language is correct.

Proof. We have to prove that the image of each rule of L exc is satisfied. It should be reminded that strong and weak equations coincide on L exc .

• (propagate) For each a (1) : X → Y , the rules of L exc-core imply that a • (try 1 ) For each u (0) : X → P and b (1) :

• [ ] X ≡ [ ] Y , so that a • [ ] X • tag ≡ [ ] Y • tag. • (recover) For each u (0) 1 , u (0) 2 : X → P , if [ ] Y • tag• u 1 ≡ [ ] Y • tag• u 2 since [ ] Y
P → Y , we have TRY([ ] Y • tag • u, CATCH(b)) ∼ CATCH(b) • [ ] Y • tag • u and CATCH(b) • [ ] Y ≡ b • untag so that TRY([ ] Y • tag • u, CATCH(b)) ∼ b • untag • tag • u. We have also untag • tag • u ∼ u (because untag • tag ∼ id and u is pure), so that TRY([ ] Y • tag • u, CATCH(b)) ∼ b • u.
Example 4.3 (Continuation of Example 3.1). We here show that it is possible to separate the matching between normal or exceptional behavior from the recovery after an exceptional behavior: to prove that try(s(throw 3))catch(p) is equivalent to 2 in the core language, we first use the translation to get:

TRY(s•[ ]•tag•3, CATCH(p)). Then (empty ∼ ) shows that s•[ ]tag•3 ∼ [ ]•tag•3. Now, the TRY and CATCH translations show that TRY([ ] • tag • 3, CATCH(p)) ∼ CATCH(p) • [ ] • tag • 3 ∼ p • untag • tag • 3.
Finally the axiom (ax) and (eq 1 ) give p • 3 ≡ 2.

In order to prove the completeness of the core decorated theory for exceptions, as for the proof of Theorem 3.5, we first determine canonical forms in Proposition 4.4, then we study the equations between terms in canonical form in Proposition 4.5. Let us begin by proving the fundamental strong equation for exceptions [START_REF] Bauer | Programming with algebraic effects and handlers[END_REF]: by replacement in the axiom (ax) we get tag•untag•tag ∼ tag, then by rule (eq 3 ):

tag

• untag ≡ id 0 (1)
Proposition 4.4.

1. For each propagator a (1) : X → Y , either a is pure or there is a pure term v (0) : X → P such that a (1) ≡ [ ] (0) Y • tag (1) • v (0) . And for each propagator a (1) : X → 0 (either pure or not), there is a pure term v (0) : X → P such that a (1) ≡ tag (1) • v (0) . 2. For each catcher f (2) : X → Y , either f is a propagator or there is an propagator a (1) : P → Y and a pure term u (0) : X → P such that f (2) ≡ a (1) • untag (2) • tag (1) • u (0) .

Proof.

1. If the propagator a (1) : X → Y is not pure then it contains at least one occurrence of tag (1) . Thus, it can be written in a unique way as a = b • tag • v for some propagator b (1) : 0 → Y and some pure term v (0) : X → P . Since b (1) : 0 → Y we have b (1) ≡ [ ] (0) Y , and the first result follows. When X = 0, it follows that a (1) ≡ tag (1) • v (0) . When a : X → 0 is pure, one has a ≡ tag (1) • ([ ] P • a) (0) .

2. The proof proceeds by structural induction. If f is pure the result is obvious, otherwise f can be written in a unique way as f = g • op • u where u is pure, op is either tag or untag and g is the remaining part of f . By induction, either g is a propagator or g ≡ b • untag • tag • v for some pure term v and some propagator b. So, there are four cases to consider. ( 1) If op = tag and g is a propagator then f is a propagator. ( 2) If op = untag and g is a propagator then by Point 1 there is a pure term w such that u ≡ tag • w, so that f ≡ g (1) • untag• tag • w (0) . ( 3) If op = tag and g ≡ b (1) • untag

• tag • v (0) then f ≡ b • untag • tag • v • tag • u. Since v : 0 → P is pure we have tag • v ≡ id 0 , so that f ≡ b (1) • untag • tag • u (0) . (4) If op = untag and g ≡ b (1) • untag • tag • v (0) then f ≡ b • untag • tag • v • untag • u. Since v
v • untag • tag ∼ v and untag • tag • v • untag • tag ∼ untag • tag • v.
Since ∼ is an equivalence relation these three weak equations imply untag

• tag • v • untag • tag ∼ v • untag • tag. By rule (eq 3 ) we get untag • tag • v • untag ≡ v • untag, and by Point 1 there is a pure term w such that u ≡ tag • w, so that f ≡ (b • v) (1) • untag • tag • w (0) .
Thanks to Proposition 4.4, in order to study equations in the logic L exc-core we may restrict our study to pure terms, propagators of the form [ ] (0) Y • tag (1) • v (0) and catchers of the form a (1) • untag (2) • tag (1) • u (0) . Proposition 4.5.

1. For all a

(1)

1 , a (1)
2 : P → Y and u

(0) 1 , u (0)
2 : X → P , let f

(2) 1 = a 1 • untag• tag• u 1 : X → Y and f (2) 2 = a 2 • untag• tag• u 2 : X → Y , then f 1 ∼ f 2 is T exc-core -equivalent to a 1 • u 1 ≡ a 2 • u 2 and f 1 ≡ f 2 is T exc-core -equivalent to {a 1 ≡ a 2 , a 1 • u 1 ≡ a 2 • u 2 }.

For all a

(1) 1

: P → Y , u (0) 1 : X → P and a (1) 2 : X → Y , let f (2) 1 = a 1 • untag•tag•u 1 : X → Y , then f 1 ∼ a 2 is T exc-core -equivalent to a 1 •u 1 ≡ a 2 and f 1 ≡ a 2 is T exc-core -equivalent to {a 1 • u 1 ≡ a 2 , a 1 ≡ [ ] Y • tag}.

Let us assume that [ ] (0)

Y is a monomorphism with respect to propagators. For all v

(0) 1 , v (0) 2 : X → P , let a (1) 1 = [ ] Y • tag • v 1 : X → Y and a (1) 2 = [ ] Y • tag • v 2 : X → Y . Then a 1 ≡ a 2 is T exc-core -equivalent to v 1 ≡ v 2 .
Proof.

1. Rule (eq 2 ) implies that

f 1 ≡ f 2 if and only if f 1 ∼ f 2 and f 1 •[ ] X ≡ f 2 •[ ] X . On the one hand, f 1 ∼ f 2 if and only if a 1 •u 1 ≡ a 2 •u 2 : indeed, for each i ∈ {1, 2}, by (ax) and (subs ∼ ), since u i is pure we have f i ∼ a i • u i . On the other hand, let us prove that f 1 • [ ] X ≡ f 2 • [ ] X if and only if a 1 ≡ a 2 . For each i ∈ {1, 2}, the propagator tag • u i • [ ] X : 0 → 0 satisfies tag • u i • [ ] X ≡ id 0 , so that f i • [ ] X ≡ a i • untag. Thus, f 1 • [ ] X ≡ f 2 • [ ] X if and only if a 1 • untag ≡ a 2 • untag. Clearly, if a 1 ≡ a 2 then a 1 •untag ≡ a 2 •untag. Conversely, if a 1 •untag ≡ a 2 •untag then a 1 • untag• tag ≡ a 2 • untag• tag,
so that by (ax) and (repl ∼ ) we get a 1 ∼ a 2 , which means that a 1 ≡ a 2 because a 1 and a 2 are propagators.

2. Rule (eq 2 ) implies that f 1 ≡ a 2 if and only if

f 1 ∼ a 2 and f 1 • [ ] X ≡ a 2 • [ ] X .
On the one hand, f 1 ∼ a 2 if and only if a 1 • u 1 ≡ a 2 : indeed, by (ax) and (subs ∼ ), since u 1 is pure we have f 1 ∼ a 1 • u 1 . On the other hand, let us prove that f

1 • [ ] X ≡ a 2 • [ ] X if and only if a 1 ≡ [ ] Y • tag, in two steps. Since a 2 • [ ] X : 0 → Y is a propagator, we have a 2 • [ ] X ≡ [ ] Y . Since f 1 • [ ] X = a 1 • untag • tag • u 1 • [ ] X with tag • u 1 • [ ] X : 0 → 0 a propagator, we have tag • u 1 • [ ] X ≡ id 0 and thus we get f 1 • [ ] X ≡ a 1 • untag. Thus, f 1 • [ ] X ≡ a 2 • [ ] X if and only if a 1 • untag ≡ [ ] Y . If a 1 • untag ≡ [ ] Y then a 1 • untag • tag ≡ [ ] Y • tag, by (ax) and (repl ∼ ) this implies a 1 ∼ [ ] Y • tag, which is a strong equality because both members are propagators. Conversely, if a 1 ≡ [ ] Y • tag then a 1 • untag ≡ [ ] Y • tag • untag, by the fundamental equation (1) this implies a 1 • untag ≡ [ ] Y . Thus, a 1 • untag ≡ [ ] Y if and only if a 1 ≡ [ ] Y • tag. 3. Clearly, if v 1 ≡ v 2 then [ ] Y • tag • v 1 ≡ [ ] Y • tag • v 2 . Conversely, if [ ] Y • tag • v 1 ≡ [ ] Y • tag • v 2 then since [ ] Y is a monomorphism with respect to propagators we get tag•v 1 ≡ tag•v 2 , so that untag•tag•v 1 ≡ untag• tag• v 2 . Now, from (ax) we get v 1 ∼ v 2 , which means that v 1 ≡ v 2 because v 1 and v 2 are pure.
Assumption 4.6 is the image of Assumption 3.4 by the above translation.

Assumption 4.6. In the logic L exc-core , the type of parameters P is non-empty, and for all v (0) 1

: X → P and v (0) 2 : X → Y with X non-empty, let a (1) 1
= [ ] Y • tag • v 1 : X → Y . Then a (1) 1 ≡ v (0) 2 is T exc -equivalent to T max,0 .
Theorem 4.7. Under Assumption 4.6, the theory of exceptions T exc-core is Hilbert-Post complete with respect to the pure sublogic L eq of L exc-core .

Proof. Using Corollary 2.10, the proof is based upon Propositions 4.4 and 4.5. It follows the same lines as the proof of Theorem 3.5, except when X is empty: because of catchers the proof here is slightly more subtle. First, the theory T exc-core is consistent, because (by soundness) it cannot be proved that untag (2) ≡ [ ] (0) P . Now, let us consider an equation between terms f 1 , f 2 : X → Y , and let us prove that it is T exc-core -equivalent to a set of pure equations. When X is non-empty, Propositions 4.4 and 4.5, together with Assumption 4.6, prove that the given equation is T exc-core -equivalent to a set of pure equations. When X is empty, then f 1 ∼ [ ] Y and f 2 ∼ [ ] Y , so that if the equation is weak or if both f 1 and f 2 are propagators then the given equation is T exc-core -equivalent to the empty set of equations between pure terms. When X is empty and the equation is f 1 ≡ f 2 with at least one of f 1 and f 2 a catcher, then by Point 1 or 2 of Proposition 4.5, the given equation is T exc-core -equivalent to a set of equations between propagators; but we have seen that each equation between propagators (whether X is empty or not) is T exc-core -equivalent to a set of equations between pure terms, so that f 1 ≡ f 2 is T exc-core -equivalent to the union of these sets of pure equations.

Verification of Hilbert-Post Completeness in Coq

All the statements of Sections 3 and 4 have been checked in Coq. The proofs can be found in http://forge.imag.fr/frs/download.php/680/hp-0.7.tar.gz, as well as an almost dual proof for the completeness of the state. They share the same framework, defined in [START_REF] Dumas | Formal verification in Coq of program properties involving the global state[END_REF]:

1. the terms of each logic are inductively defined through the dependent type named term which builds a new Type out of two input Types. For instance, term Y X is the Type of all terms of the form f : X → Y;

2. the decorations are enumerated: pure and propagator for both languages, and catcher for the core language;

3. decorations are inductively assigned to the terms via the dependent type called is. The latter builds a proposition (a Prop instance in Coq) out of a term and a decoration. Accordingly, is pure (id X) is a Prop instance;

4. for the core language, we state the rules with respect to weak and strong equalities by defining them in a mutually inductive way.

The completeness proof for the exceptions core language is 950 SLOC in Coq where it is 460 SLOC in L A T E X. Full certification runs in 6.745s on a Intel i7-3630QM @2.40GHz using the Coq Proof Assistant, v. The correspondence between the propositions and theorems in this paper and their proofs in Coq is given in Fig. 4, and the dependency chart for the main results in Fig. 5. For instance, Proposition 3.3 is expressed in Coq as:

forall {X Y} (a1 a2: term X Y) (v1 v2: term (Val e) Y), (is pure v1) /\ (is pure v2) /\ (a1 = ((@throw X e) o v1)) /\ (a2 = ((@throw X e) o v2)) -> ((a1 == a2) <-> (v1 == v2)).

hp-0. eq pr pu abs Proposition 4.5 Point 1 eq ca 2 eq pr Proposition 4.5 Point 2 eq ca pr 2 eq pr Proposition 4.5 Point 3 eq pr 1 eq pu Theorem 4.7

HPC exc core

Conclusion and future work

This paper is a first step towards the proof of completeness of decorated logics for computer languages. It has to be extended in several directions: adding basic features to the language (arity, conditionals, loops, . . . ), proving completeness of the decorated approach for other effects (not only states and exceptions); the combination of effects should easily follow, thanks to Proposition 2.7.

A Completeness for states

Most programming languages such as C/C++ and Java support the usage and manipulation of the state (memory) structure. Even though the state structure is never syntactically mentioned, the commands are allowed to use or manipulate it, for instance looking up or updating the value of variables. This provides a great flexibility in programming, but in order to prove the correctness of programs, one usually has to revert to an explicit manipulation of the state. Therefore, any access to the state, regardless of usage or manipulation, is treated as a computational effect: a syntactical term f : X → Y is not interpreted as f : X → Y unless it is pure, that is unless it does not use the variables in any manner. Indeed, a term which updates the state has instead the following interpretation: f : X × S → Y × S where '×' is the product operator and S is the set of possible states. In [START_REF] Dumas | Formal verification in Coq of program properties involving the global state[END_REF], we proposed a proof system to prove program properties involving states effect, while keeping the memory manipulations implicit. We summarize this system next and prove its Hilbert-Post completeness in Theorem A.6.

As noticed in [START_REF] Dumas | Certified proofs in programs involving exceptions[END_REF], the logic L exc-core is exactly dual to the logic L st for states (as reminded below). Thus, the dual of the completeness Theorem 4.7 and of all results in Section 4 are valid, with the dual proof. However, the intended models for exceptions and for states rely on the category of sets, which is not self-dual, and the additional assumptions in Theorem 4.7, like the existence of a boolean type, cannot be dualized without loosing the soundness of the logic with respect to its intended interpretation. It follows that the completeness Theorem A.6 for the theory for states is not exactly the dual of Theorem 4.7. In this Appendix, for the sake of readability, we give all the details of the proof of Theorem A.6; we will mention which parts are not the dual of the corresponding parts in the proof of Theorem 4.7.

As in [START_REF] Dumas | Decorated proofs for computational effects: States[END_REF], decorated logics for states are obtained from equational logics by classifying terms and equations. Terms are classified as pure terms, accessors or modifiers, which is expressed by adding a decoration or superscript, respectively (0), ( 1) and ( 2); decoration and type information about terms may be omitted when they are clear from the context or when they do not matter. Equations are classified as strong or weak equations, denoted respectively by the symbols ≡ and ∼. Weak equations relates to the values returned by programs, while strong equations relates to both values and side effects. In order to observe the state, accessors may use the values stored in locations, and modifiers may update these values. In order to focus on the main features of the proof of completeness, let us assume that only one location can be observed and modified; the general case, with an arbitrary number of locations, is considered in Remark A.7. The logic for dealing with pure terms may be any logic which extends a monadic equational logic with constants L eq,1 ; its terms are decorated as pure and its equations are strong. This pure sublogic L (0) st is extended to form the corresponding decorated logic for states L st . The rules for L st are given in Fig. 6. A theory T (0) of L (0) st is chosen, then the theory of states T st is the theory of L st generated from T (0) . Let us now discuss the logic L st and its intended interpretation in sets; it is assumed that some model of the pure subtheory T (0) in sets has been chosen; the names of the rules refer to Fig. 6.

Each type X is interpreted as a set, denoted X. The intended model is described with respect to a set S called the set of states, which does not appear in the syntax. A pure term u (0) : X → Y is interpreted as a function u : X → Y , an accessor a (1) : X → Y as a function a : S × X → Y , and a modifier f (2) : X → Y as a function f : S × X → S × Y . There are obvious conversions from pure terms to accessors and from accessors to modifiers, which allow to consider all terms as modifiers whenever needed; for instance, this allows to interpret the composition of terms without mentioning Kleisli composition; the complete characterization is given in [START_REF] Dumas | Decorated proofs for computational effects: States[END_REF].

Here, for the sake of simplicity, we consider a single variable (as done, e.g., in [START_REF] Pretnar | The Logic and Handling of Algebraic Effects[END_REF] and [START_REF] Staton | Completeness for Algebraic Theories of Local State[END_REF]), and dually to the choice of a unique exception name in Section 4. See Remark A.7 for the generalization to an arbitrary number of variables. The values of the unique location have type V . The fundamental operations for dealing with the state are the accessor lookup (1) : 1 → V for reading the value of the location and the modifier update (2) : V → 1 for updating this value. According to their decorations, they are interpreted respectively as functions lookup : S → V and update : S × V → S. Since there is only one location, it might be assumed that lookup : S → V is a bijection and that update : S × V → S maps each (s, v) ∈ S × V to the unique s ′ ∈ S such that lookup(s ′ ) = v: this is expressed by a weak equation, as explained below.

A strong equation f ≡ g means that f and g return the same result and modify the state in "the same way", which means that no difference can be observed between the side-effects performed by f and by g. Whenever lookup : S → V is a bijection, a strong equation f (2) ≡ g (2) : X → Y is interpreted as the equality f = g : S × X → S × Y : for each (s, x) ∈ S × X, let f (s, x) = (s ′ , y ′ ) and g(s, x) = (s ′′ , y ′′ ), then f ≡ g means that y ′ = y ′′ and s ′ = s ′′ for all (s, x). Strong equations form a congruence. A weak equation f ∼ g means that f and g return the same result although they may modify the state in different ways. Thus, a weak equation f (2) ∼ g (2) : X → Y is interpreted as the equality pr Y • f = pr Y • g : S × X → Y , where pr Y : S × Y → Y is the projection; with the same notations as above, this means that y ′ = y ′′ for all (s, x). Weak equations do not form a congruence: the replacement rule holds only when the replaced term is pure. The fundamental equation for states is provided by rule (ax): lookup (1) • update (2) ∼ id V . This means that updating the location with a value v and then observing the value of the location does return v. Clearly this is only a weak equation: its right-hand side does not modify the state while its left-hand side usually does. There is an obvious conversion from strong to weak equations (≡-to-∼), and in addition strong and weak equations coincide on accessors by rule (eq 1 ). Two modifiers f

Y • f 1 ≡ Y • f 2 : X → 1,
where Y : Y → 1 throws out the returned value. Then weak and strong equations are related by the property that f 1 ≡ f 2 if and only if

f 1 ∼ f 2 and Y • f 1 ≡ Y • f 2 ,
by rule (eq 2 ). This can be expressed as a pair of weak equations f 1 ∼ f 2 and lookup

• Y • f 1 ∼ lookup • Y • f 2
, by rule (eq 3 ). Some easily derived properties are stated in Lemma A.1; Point 2 will be used repeatedly.

Monadic equational logic with constants Leq,1: Types and terms: as for monadic equational logic, plus a unit type 1 and a term X : X → 1 for each X Rules: as for monadic equational logic, plus (unit) f : X → 1 f ≡ X Decorated logic for states Lst : Pure part: some logic L (0) st extending Leq,1, with a distinguished type V Decorated terms: lookup (1) : 1 → V , update (2) : V → 1, and (f k • • • • • f1) (max(d 1 ,...,d k )) : X0 → X k for each (f

(d i ) i
: Xi-1 → Xi) 1≤i≤k with conversions from f (0) to f (1) and from f (1) to f (2) Rules:

(equiv≡), (subs≡), (repl≡) for all decorations (equiv∼), (subs∼) for all decorations, (repl∼) only when h is pure (unit∼)

f : X → 1 f ∼ X (≡-to-∼) f ≡ g f ∼ g (ax) lookup • update ∼ id V (eq1) f (d 1 ) 1 ∼ f (d 2 ) 2
f1 ≡ f2 only when d1 ≤ 1 and d2 ≤ 1 2. each f (2) : 1 → 1 is such that f ∼ id 1 , each f (1) : X → 1 is such that f ≡ X , and each f (1) : 1 → 1 is such that f ≡ id 1 .

(eq2) f1, f2 : X → Y f1 ∼ f2 Y • f1 ≡ Y • f2 f1 ≡ f2 (eq3) f1, f2 : X → 1 lookup • f1 ∼ lookup • f2 f1 ≡ f2
3. For all pure terms u Our main result is Theorem A.6 about the relative Hilbert-Post completeness of the decorated theory of states under suitable assumptions.

Proposition A.2.

1. For each accessor a (1) : X → Y , either a is pure or there is a pure term v (0) : V → Y such that a (1) ≡ v (0) • lookup (1)

• (0) X .
For each accessor a (1) : 1 → Y (either pure or not), there is a pure term v (0) : V → Y such that a (1) ≡ v (0) • lookup (1) .

2. For each modifier f (2) : X → Y , either f is an accessor or there is an accessor a (1) : X → V and a pure term u (0) : V → Y such that f (2) ≡ u (0) • lookup (1) • update (2) • a (1) .

Proof.

1. If the accessor a (1) : X → Y is not pure then it contains at least one occurrence of lookup (1) . Thus, it can be written in a unique way as a = v • lookup • b for some pure term v (0) : V → Y and some accessor b (1) : X → 1. Since b (1) : X → 1 we have b (1) ≡ (0) X , and the first result follows. When X = 1, it follows that a (1) ≡ v (0) • lookup (1) . When a : 1 → Y is pure, one has a ≡ (a • V ) (0) • lookup (1) .

2. The proof proceeds by structural induction. If f is pure the result is obvious, otherwise f can be written in a unique way as f = u • op • g where u is pure, op is either lookup or update and g is the remaining part of f . By induction, either g is an accessor or g ≡ v • lookup • update • b for some pure term v and some accessor b. So, there are four cases to consider.

• If op = lookup and g is an accessor then f is an accessor.

• If op = update and g is an accessor then by Point 1 there is a pure term w such that u ≡ w •lookup, so that f ≡ w (0) •lookup•update• g (1) .

• If op = lookup and g ≡ v (0) • lookup • update • b (1) 1) .

then f ≡ u • lookup • v • lookup • update • b. Since v : V → 1 is pure we have v • lookup ≡ id 1 , so that f ≡ u (0) • lookup • update • b (
• If op = update and g ≡ v (0) • lookup • update • b (1) then f ≡ u (0) •update•v (0) •lookup•update•b (1) . Since v is pure, by (ax) and (repl ∼ ) we have (1) .

( 1 )

 1 Y : P → Y for each type Y : this operation throws an exception with a parameter p of type P and pretends that this exception has type Y . The interpretation of the term throw (1) Y : P → Y is a function throw Y : P → Y +E such that throw Y (p) ∈ E for each p ∈ P . The fundamental operations for handling exceptions are the propagators (try(a)catch(b)) (1) : X → Y for each terms a : X → Y and b : P → Y : this operation first runs a until an exception with parameter p is raised (if any), then, if such an exception has been raised, it runs b(p). The interpretation of the term (try(a)catch(b)) (1) : X → Y is a function try(a)catch(b) : X → Y + E such that (try(a)catch(b))(x) = a(x) when a is pure and (try(a)catch(b))(x) = b(p) when a(x) throws an exception with parameter p.

  Pure part: the logic Leq with a distinguished type P Decorated terms: throw[START_REF] Bauer | Programming with algebraic effects and handlers[END_REF]

Figure 2 :

 2 Figure 2: Decorated logic for exceptions L exc

Figure 3 :

 3 Figure 3: Decorated logic for the core language for exceptions L exc-core

  is a monomorphism with respect to propagators we have tag • u 1 ≡ tag • u 2 , so that, by Point 1 in Lemma 4.1, we get u 1 ≡ u 2 .• (try) Since try(a i )catch(b) ∼ catch(b)•a i for i ∈ {1, 2}, we get try(a 1 )catch(b) ∼ try(a 2 )catch(b) as soon as a 1 ≡ a 2 .• (try 0 ) For each u (0) : X → Y and b (1) : P → Y , we have TRY(u, CATCH(b)) ∼ CATCH(b) • u and CATCH(b) • u ∼ u (because CATCH(b) ∼ id and u is pure), so that TRY(u, CATCH(b)) ∼ u.

Figure 4 :Figure 5 :

 45 Figure 4: Correspondence between theorems in this paper and their Coq counterparts

2 :

 2 X → Y modify the state in the same way if and only if

Figure 6 : 3 )

 63 Figure 6: Decorated logic for states (dual to Fig. 3)

2 :

 2 V → Y , one has: u 1 ≡ u 2 is T st -equivalent to u 1 • lookup ≡ u 2 • lookup and also to u 1 • lookup • update ≡ u 2 • lookup • update.

4 . 1 .

 41 For all pure terms u (0) : V → Y , v (0) : 1 → Y , one has: u ≡ v • V is T st -equivalent to u • lookup ≡ v.Proof. By substitution in the axiom (ax) we get lookup•update•lookup ∼ lookup; then by rule (eq 3 ) update • lookup ≡ id 1 .2. Clear.

3 .

 3 Implications from left to right are clear. Conversely, if u 1 • lookup • update ≡ u 2 • lookup • update, then using the axiom (ax) and the rule (repl ∼ ) we get u 1 ∼ u 2 . Since u 1 and u 2 are pure this means that u 1 ≡ u 2 .4. First, sinceV •lookup : 1 → 1 is an accessor we have V •lookup ≡ id 1 . Now, if u ≡ v• V then u•lookup ≡ v• V •lookup, so that u•lookup ≡ v. Conversely, if u • lookup ≡ v then u • lookup ≡ v • V • lookup,and by Point (3) this means that u ≡ v • V .

  16, Prop 2.37 & 2.40]): we first determine canonical forms in Proposition 3.2, then we study the equations between terms in canonical form in Proposition 3.3.

  is pure, by (ax) and (subs

∼ ) we have untag • tag • v ∼ v.

Besides, by (ax) and (repl ∼ ) we have

  8.4pl3. Below table details the proof lengths and timings for each library.

		Proof lengths & Benchmarks
	package	source	length length	execution time
			in Coq in L A T E X in Coq
	exc cl-hp	HPCompleteCoq.v	40 KB 15 KB	6.745 sec.
	exc pl-hp	HPCompleteCoq.v	8 KB	6 KB	1.704 sec.
	exc trans	Translation.v	4 KB	2 KB	1.696 sec.
	st-hp	HPCompleteCoq.v	48 KB 15 KB	7.183 sec.

  v•lookup•update ∼ v. Besides, by (ax) and (subs ∼ ) we have lookup • update • v ∼ v and lookup • update • v • lookup • update ∼ v•lookup•update. Since ∼ is an equivalence relation these three weak equations imply lookup • update • v • lookup • update ∼ lookup•update•v. By rule (eq 3 ) we get update•v•lookup•update ≡

update • v, so that f ≡ u (0) • update • (v • b)

For instance, a denotational semantics of our framework for exceptions, which relies on the common semantics of exceptions in these languages, was given in[8, § 4].

Thanks to Proposition A.2, in order to study equations in the logic L st we may restrict our study to pure terms, accessors of the form v (0) •lookup (1) • (0) X and modifiers of the form u (0) • lookup (1) • update (2) • a (1) .

Point 4 in Proposition A.2 is not dual to Point 1 in Proposition 4.4

Proposition A.3.

1. For all a

(1)

2 : X → V and u

2 : V → Y , let f

For all a

(1) 1

Let us assume that (0)

X is an epimorphism with respect to accessors. For all v

Let us assume that (0)

V is an epimorphism with respect to accessors and that there exists a pure term k (0)

Proof.

1. Rule (eq 2 ) implies that

On the one hand, f 1 ∼ f 2 if and only if u 1 • a 1 ≡ u 1 • a 2 : indeed, for each i ∈ {1, 2}, by (ax) and (repl ∼ ), since u i is pure we have

, so that by (ax) and (subs ∼ ) we get a 1 ∼ a 2 , which means that a 1 ≡ a 2 because a 1 and a 2 are accessors.

2. Rule (eq 2 ) implies that

ax) and (subs ∼ ) this implies a 1 ∼ lookup • X , which is a strong equality because both members are accessors. Conversely, if

X is an epimorphism with respect to accessors we get

The assumption for Theorem A.6 comes form the fact that the existence of a pure term k (0) X : 1 → X, which is used in Point 4 of Proposition A.3, is incompatible with the intended model of states if X is interpreted as the empty set. The assumption for Theorem A.6 is not dual to the assumption for Theorem 4.7.

so that X is a split epimorphism; it follows that X is an epimorphism with respect to all terms, and especially with respect to accessors.

Theorem A.6. If every non-empty type is inhabited and if V is non-empty, the theory of states T st is Hilbert-Post complete with respect to the pure sublogic L (0) st of L st .

Proof. Using Corollary 2.10, the proof relies upon Propositions A.2 and A.3. it follows the same lines as the proofs of Theorems 3.5 and 4.7. The theory T st is consistent: it cannot be proved that update (2)

V because the logic L st is sound with respect to its intended model and the interpretation of this equation in the intended model is false as sson as V has at least two elements: indeed, for each state s and each x ∈ V , lookup • update(x, s) = x because of (ax) while lookup • V (x, s) = lookup(s) does not depend on x. Let us consider an equation (strong or weak) between terms with domain X in L st ; we distinguish two cases, whether X is empty or not. When X is empty, then all terms from X to Y are strongly equivalent to [ ] Y , so that the given equation is T st -equivalent to the empty set of equations between pure terms. When X is non-empty then it is inhabited, thus by Remark A.5 X is an epimorphism with respect to accessors. Thus, Propositions A.2 and A.3 prove that the given equation is T st -equivalent to a finite set of equations between pure terms.

Remark A.7. This can be generalized to an arbitrary number of locations. The logic L st and the theory T st have to be generalized as in [START_REF] Dumas | Decorated proofs for computational effects: States[END_REF], then Proposition A.2 has to be adapted using the basic properties of lookup and update, as stated in [START_REF] Plotkin | Notions of Computation Determine Monads[END_REF]; these properties can be deduced from the decorated theory for states, as proved in [START_REF] Dumas | Formal verification in Coq of program properties involving the global state[END_REF]. The rest of the proof generalizes accordingly, as in [START_REF] Pretnar | The Logic and Handling of Algebraic Effects[END_REF].


Gavin Kemp

Genoveva Vargas-Solar

Catarina Ferreira

Da Silva

Parisa Ghodous

Christine Collet

Pedropablo Lopez Amaya

Towards Cloud big data services for intelligent transport systems

Keywords: ITS, Big Data, Cloud Services, NoSQL

In later years, the increase in computation power and data storage has opened new perspectives to data analysis. The possibility to analyse big data brings new insights into obscure and useful correlations in data providing undiscovered knowledge. Applying big data analytics to the transport data has brought better understanding to the transports network revealing unexpected choking points in cities. This technology is still largely inaccessible to small companies due to their limited computational resources and complex for large ones due to the time needed to develop a big data analytical system Using the high scalability of Cloud and the use of specialized services in a services oriented architecture, new perspective are to developing efficient and scalable big data infrastructure adapted to transport systems. This paper presents a big data infrastructure using service oriented architecture.

Introduction

During the last five years, the problem of providing intelligent real time data management using cloud computing technologies has attracted attention from both academic researchers, like [START_REF] Gulisano | StreamCloud: An elastic and scalable data streaming system[END_REF], [START_REF] Lecue | STAR-CITY[END_REF]and industrial practitioners like Google Big Query, IBM, Thales. They mostly concentrate on modelling stream traffic flow, yet they barely combine different data flows with other big data to provide new Intelligent Transport Services (ITS). ITS apply technology for integrating computers, electronics, satellites and sensors for making every transport mode (road, rail, air, water) more efficient, safe, and energy saving. ITS effectiveness relies on the prompt processing of the acquired transport-related information for reacting to congestion, dangerous situations, and, in general, optimizing the circulation of people and goods. Integration, storage and analysis of huge data collections must be adapted to support ITS for providing solutions that can improve citizens' lifestyle and safety.

In order to address these challenges it is important to consider that big data introduce aspects to consider according to its properties described by the 5V's model [START_REF] Jagadish | [END_REF]: Volume, Velocity, Variety, Veracity, Value.

Volume and velocity (i.e., continuous production of new data) have an important impact in the way data is collected, archived and continuously processed. Transport data are generated at high speed by arrays of sensors or multiple events produced by devices and transport media (buses, cars, bikes, trains, etc.). These data need to be processed in real-time, near real-time or in batch, or as streams. Important decisions must be made in order to use distributed storage support that can maintain these data collections in apply on them analysis cycles. Collected data, involved in transport scenarios, can be very heterogeneous in terms of formats and models (unstructured, semi-structured and structured) and content. Data variety imposes new requirements to data storage and database design that should dynamically adapt to the data format, in particular scaling up and down. ITS and associated applications aim at adding value to collected data. Adding value to big data depends on the events they represent and the type of processing operations applied for extracting such value (i.e., stochastic, probabilistic, regular or random). Adding value to data, given the degree of volume and variety, can require important computing, storage and memory resources. Value can be related to quality of big data (veracity) concerning (1) data consistency related to its associated statistical reliability; (2) data provenance and trust defined by data origin, collection and processing methods, including trusted infrastructure and facility.

Processing and managing big data, given the volume and veracity and given the greedy algorithms that are sometimes applied to it, for example, giving value and making it useful for applications, requires enabling infrastructures. Cloud architectures provide unlimited resources that can support big data management and exploitation. The essential characteristics of the cloud lie in on-demand self-service, broad network access, resource pooling, rapid elasticity and measured services [START_REF] Grance | The NIST Definition of Cloud Computing Recommendations of the National Institute of Standards and Technology[END_REF]. These characteristics make it possible to design and implement services to deal with big data management and exploitation using cloud resources to support applications such as ITS.

The objective of our work is to manage and aggregate cloud services for managing big data and assist decision making for transport systems. Thus this paper presents our approach for developing data storage, data cleaning and data integration services to make an efficient decision support system. Our services will implement algorithms and strategies that consume storage and computing resources of the cloud. For this reason, appropriate consumption models will guide their use.

The remainder of the paper is organized as follows. Section 2 describes work related to ours. Section 3 introduces our approach for managing transport big data on the cloud for supporting intelligent transport systems applications. Section 4 presents a case study of the application that validates our approach. Finally, Section 5 concludes the paper and discusses future work.

Related work

This section focuses on big data transport projects, namely to optimize taxi usage, and on big data infrastructures and applications for transport data events.

Transdec [START_REF] Demiryurek | TransDec:A Spatiotemporal Query Processing Framework for Transportation Systems[END_REF] is a project to create a big data infrastructure adapted to transport. It is built on three tiers comparable to the MVC (Model, View, Controller) model for transport data. The presentation tier, based on GoogleTM Map, provides an interface to express queries and expose the result, the query interface provides standard queries for the presentation tier and a data tier is spatiotemporal database built with sensor data and traffic data. This work provides an interesting query system taking into account the dynamic nature of town data and providing time relevant results in real-time.

Urban insight [START_REF] Artikis | Self-Adaptive Event Recognition for Intelligent Transport Management[END_REF]is a project studying European town planning. In Dublin they are working event detection through big data, in particular on an accident detection system using video stream for CCTV (Closed Circuit Television) and crowdsourcing. Using data analysis they detect anomalies in the traffic and identify if it is an accident or not. When there is an ambiguity they rely on crowdsourcing to get further information. The project RITA [START_REF] Thompson | RITA[END_REF] in the United States is trying to identify new sources of data provided by connected infrastructure and connected vehicles. They work to propose more data sources usable for transport analysis. L. Jian,and co [START_REF] Jian | Improved Design of Communication Platform of Distributed Traffic Information Systems Based on SOA[END_REF] propose a service-oriented model to encompass the data heterogeneity of several Chinese towns. Each town maintains its data and a service that allows other towns to understand their data. These services are aggregated to provide a global data sharing service. These papers propose methodologies to acknowledge data veracity and integrate heterogeneous data into one query system. An interesting line to work on would be to produce predictions based on this data to build decision support systems.

H. V. Jagadish and co [START_REF] Jagadish | [END_REF] propose a big data infrastructure based on five steps: data acquisition, data cleaning and information extraction, data integration and aggregation, big data analysis and data interpretation. X. Chen and co [START_REF] Chen | High performance integrated spatial big data analytics[END_REF] use Hadoopgis to get information on demographic composition and health from spatial data. J. lin and D. Ryaboy [START_REF] Lin | Scaling big data mining infrastructure : The twitter Experience[END_REF] present their experience on twitter to extract information from log information. They concluded that an efficient big data infrastructure is a balancing speed of development, ease of analysis, flexibility and scalability. Proposing a big data infrastructure on the cloud will make developing big data infrastructures more accessible to small businesses for several reasons: little initial investment, ease of development throught Service-Oriented Architecture (SOA) and using services developed by specialist of each service. N. J. Yuan and co [START_REF] Yuan | T-finder: A recommender system for finding passengers and vacant taxis[END_REF], Y. Ge and co [START_REF] Ge | An energy-efficient mobile recommender system[END_REF] and D. H. Lee and co [START_REF] Lee | Taxi Dispatch System Based on Current Demands and Real-Time Traffic Conditions[END_REF] worked a transport project to help taxi companies optimize their taxi usage. They work on optimizing the odds of a client needing a taxi to meet an empty taxi, optimizing travel time from taxi to clients, based on historical data collected from running taxis. Using knowledge from experienced taxi drivers, they built a mapping of the odds of passenger presence at collection points and direct the taxis based on that map. These research works do not use real-time data thus making it complicated to make accurate predictions and react to unexpected events. They also use data limited to GPS and taxi usage, whereas other data sources could be accessed and used. D. Talia [START_REF] Talia | Clouds for scalable big data analytics[END_REF] presents the strengths of using the cloud for big data analytics in particular from a scalability stand point. They propose the development of infrastructures, platforms and service dedicated to data analytics. J. Yu and co [START_REF] Yu | RTIC-C: A Big Data System for Massive Traffic Information Mining[END_REF] propose a service oriented data mining infrastructure for big traffic data. They propose a full infrastructure with services such accident detection. For this purpose they produce a large database with the collected data by individual companies. Individual services would have to duplicate the data to be able to use it. This makes for highly redundant data as the same data I stored by the centralised database, the application and probably the data producers. What is more, companies could be reluctant to giving away their data with no control for its use. H. Demirkan and D. Delen [START_REF] Demirkan | Leveraging the capabilities of service-oriented decision support systems: Putting analytics and big data in cloud[END_REF] proposes a service oriented decision support system using big data and the cloud. A data service provides a centralised database to which application can query.

The state of the art reveals a limited use of predictions from big data analytics for transport-oriented systems. The heavy storage and processing infrastructures needed for big data and the current available data-oriented cloud services make possible the continuous access and processing of real time events to gain constant awareness, produce big data-based decision support systems, which can help take immediate informed actions. Cloud based big data infrastructure often concentrate around the massive scalability but don't propose a cheap method to simply aggregate big data services.

Managing transport data in smart cities

Consider the scenario where a taxi company needs to embed decision support in electric vehicles, to help their global optimal management. The company uses electric vehicles that implement a decision cycle to reach their destination while ensuring optimal recharging, through mobile recharging units. The decision making cycle aims at ensuring vehicles availability both temporally and spatially; and service continuity by avoiding congestion areas, accidents and other exceptional events. The taxis and mobile devices of users are equipped with video camera and location trackers that can emit the location of the taxis and people. For this purpose, we need data on the position of the vehicles and their energies levels, have a mechanism to communicate unexpected events and have usage and location of the mobile recharging station. In cloud computing everything is viewed as a service (XaaS). As a consequence cloud software (SaaS) is built as an aggregate of services exploiting services available on the cloud infrastructure (IaaS). In this spirit, we build a big data infrastructure were individual companies (Figure 2), specialized in their level of big data; can propose services on each level of big data. This also means that the companies wanting a big data infrastructure will be able to simply build it from an aggregation of services proposed by specialized companies.

Next section explains how the services are built to insure high scalability of cloud and the controlled cost.

Some Cloud Big data services for transport

Data acquisition service

The first step of a big data infrastructure is well collecting the big data. This is basically hardware and infrastructure services that transfer, to NoSQL data stores adapted to the format of the data, the data acquired by the vehicles, users, and sensors deployed in cities (e.g. roads, streets, public spaces). This is done by companies and entities such as town or companies managing certain public spaces, who have data collecting facilities. These companies propose and sell their data on a cloud infrastructure. Clients using the same cloud infrastructure could then pay to have access the data., in our case the universities Openstack infrastructure [START_REF]Openstack[END_REF]. Using object storage such as Swift [START_REF] Openstack | swift[END_REF] using MongoDB [START_REF] Sadalage | NoSQL Distilled[END_REF], these companies will have a cheap highly scalable and sharable data store. Also the sharding capability of these data stores offers high horizontal scalability but also faster analysis threw MapReduce and data availability.

In the taxis scenario, data from the town and from the vehicles would be stored on several object data stores known as container with Swift. Since there are several companies involved, they will store there data on separate data stores. When a client wishes to access the data, the company would propose REST (representational state of transfer) [START_REF] Valverde | Dealing with REST Services in Model-driven Web Engineering Methods[END_REF] services to which the client can query to get access to the data. These companies propose different service to historical data and real-time data. The historical data service provides authentication to the client so they can apply Openstack MapReduce service (Sahara) [START_REF] Openstack | sahara[END_REF] on their container. The real-time data service provides a Json or XML file of the latest data produced.

We are implementing and testing the data acquisition service. This services uses NodeJS module to acquire the city data from the Grand Lyon [START_REF] Grandlyon | Smart Data[END_REF] but also from Twitter and from Bing search engine using REST requests. Still using REST requests these services will post the data onto a Mongodb database container to store as historical data. The service provides functions to access data via REST either with the key to the data store when wanting to query or analyses the historical data or the latest file acquired when using the real-time data service. The data is stored under XML, Json or the original image file or PDF before data extraction.

Information extraction and cleaning service

The next step is cleaning and data extraction. This consists of both extracting the information from unstructured data and cleaning the data. This could be done by the company producing the data or an independent company depending on the level of structuration of the data. Highly structured data would likely be cleaned by the company producing the data as they understand best its production and thus know how best to clean it up. For highly unstructured data like sound or video data, highly specialized expert would be needed to extract the information.

This would be used to pot outliers in the data. Using MapReduce, the company acquiring the data or the company contracted to do it would perform statistical analysis to identify for example outliers in the data. This is important as, for example, a malfunction in a sensor loop could either ignore passing traffic or register non-existing traffic. Cleaning these events is important since inaccurate data produced by a dodgy sensor can break a model.

Integration and aggregation services

The objective of big data analytics is to use the large volume of data to extract new knowledge by searching, for example, for patterns in the data. This often has a consequence of data coming from a wide variety of sources. This means the data has to be aggregated into a usable format for the analytics tools to use. This service proposes services for real-time data aggregation and historical data aggregation.

The real-time data aggregation service gets the data from the individual data stores real-time data services and proposes a formatted file with the data from all the data acquiring service simply by fusing together the data provided by the real-time data acquisition services. Thus we aggregate data from the city, state of recharging stations, having location of people based on the time stamp or the GPS location.

The historical data aggregation will have to find a way to do similar action but with the data stores. The problem is that having data on several separate data stores is not a usable format. Importing all the data into a new huge data store would be redundant on already existing resources making this service potentially excessively expensive and as for temporary stores would be long to build when having to import terabytes of data as well as being expensive on network cost as well as time consuming. To solve this problem, this service will to propose a query interface for simple querying and processing service to process the data masse by converting a form simple programing language into UNQL queries to collect and pre-process the data before being integrated into a model.

Big data analytical and decision support services

The whole point of big data is to identify and extract information form the mass of data. Predictive tools can be developed to anticipate the future. The role of this service is to provide a computer model of the historical data. It also provides the algorithm applied to the individual pieces of data. Thus using the model provided by the analytical service and the algorithm applied to the real-time data we can approach similar situations and act accordingly.

The decision support service composes several services. On the strategic level and using the model and the algorithm proposed by the big data analytical services, the decision support service provides an interface exposing the data situation in real-time but also predictions on events. For example, regularly observing an increase in the population in one place and traffic jams 30 minutes later we can deduct cause and effect and intervene in future situations so the taxis avoid and evacuate that area.

This service also generates data on the decision taken by the strategists to build more elaborate model including the consequence of this decision to then provide better decision support. On the vehicle level, services will provide advice to the vehicle for optimal economic driving based on the driving conditions. It also provides a database were the information on the dangers of the road is stored.

CONCLUSION

This paper proposes a set of big data services as a starting point of a dedicated and flexible infrastructure for managing and exploiting transport data. Our approach uses NoSQL systems deployed in a multi-cloud setting and makes sharding decisions for ensuring data availability.

Our transport data service architecture is validated in a scalable and adaptable ITS case study of electric vehicles using big data analytics on the cloud. This provides a global view of current status of town transport, helps making accurate strategic decisions, and insures maximum security to the vehicles and their occupants.

For the time being our data transport services concentrate in improving design issues with respect to NoSQL support. We are currently measuring performance with respect to different sizes of data collections. We have noticed that NoSQL provides reasonable response times once an indexing phase has been completed. We are willing to study the use of indexing criteria and provide strategies for dealing with continuous data. These issues concern our future work.

Figure 1 :

 1 Figure 1: Big Data servicesFigure1shows the services that this application relies on. These services concern data acquisition and cleaning and information extraction in one side of the spectrum, and on the other side big data analysis, integration and aggregation services, and decision-making support.

Figure 2 :

 2 Figure 2: Big Data infrastructure

ACKNOWLEDGEMENT

We thank the Région Rhône-Alpes who finances the thesis work of Gavin Kemp by means of the ARC 7 programme (http://www.arc7-territoiresmobilites.rhonealpes.fr/), as well as the competitiveness cluster LUTB Transport & Mobility Systems, in particularly Mr. Pascal Nief, Mr. Timothée David and Mr. Philippe Gache for putting us in contact with local companies and projects to gather use case scenarios for our work.