A C R Costa

G P Dimuro

J Dugdale
email: julie.dugdale@imag.fr

Y Demazeau

A Formal Notion of Objective Expectations in the Context of Multiagent Systems Routines

This paper introduces an objective notion of routine expectation, to allow for the external account of expectations in the context of routine procedures, in multiagent systems (MAS). The notion of expectation as usually applied to MAS is briefly reviewed. A formalization of routine procedure is given, so that the formal notion of routine expectation can be defined with respect to actions and facts. A view previously proposed in the literature, to base expectation values on a combination of probability values and utility values, is adopted. However, it is adapted to the context of repetitive, periodic system routines, where utility values can be replaced by the degrees of perfection with which actions and facts are realized.

Introduction: motivation and related works

In general there are different ways of considering the notion of expectation in agent systems. For example, a mentalist, or cognitivist approach defines an expectation as a complex set of cognitive elements (a combination of goals, beliefs, etc.) [START_REF] Castelfranchi | Mind as an anticipatory device: For a theory of expectations[END_REF]. Such kind of subjectivist approach may also take the way adopted in [START_REF] Piunti | Expectations driven approach for situated, goaldirected agents[END_REF][START_REF] Piunti | Modeling expectations for affective agents[END_REF], briefly suggested in [START_REF] Castelfranchi | Mind as an anticipatory device: For a theory of expectations[END_REF], which gives expectations a combination of probability values and utility values, assigned to the possible outcomes of the actions (using the notion of subjective expected utility values [START_REF] Savage | The Foundations of Statistics[END_REF]).

A crucial aspect of both these works is that an agent's expectation is related to a momentary situation in the system. That is, it relates to a situation that is artificially isolated from the whole behavior of the agent, and from the continuous operation of the system. The agent is seen as having a goal and performing an action at a given instant (or believing that a given event will happen that will help to achieve the goal), so that the entire past and future ways in which the agent participates in the system is not taken into account. Expectations about future agent interactions can not be adequately studied in such settings.

However, most practically important agent systems, including human ones, are important precisely because of their continuous functioning over time and, in particular, because of their repetitive, periodic functioning; that is, their routines. Routines have long been recognized as an essential feature of the operational dynamics of social systems (cf., e.g., Giddens in [START_REF] Giddens | The Constitution of Society: Outline of the Theory of Structuration[END_REF]), and the same idea seems to apply to multiagent systems.

Here the functioning aims at the continuous monitoring and/or control of some target system, or the continuous servicing of their users [START_REF] Costa | A minimal dynamical organization model[END_REF].

An example of the importance of periodic routines and expected patterns of behavior in managing electricity in home situations was seen in [START_REF] Dugdale | Modélisation située des activités individuelles et collectives pour la conception[END_REF]. Also, modeling expectations seems very promising in the idea of developing personal assistants that will support a human user in his/her usual day-life activities [START_REF] Crépin | Privacy preservation in a decentralized calendar system[END_REF].

We thus develop a complementary point of view. We formulate in set-theoretic terms an objective, behavioristic notion of expectation, centered around the objective effects of the actions that the agents perform, at a given moment, within the context of some system routine. We do not consider here, however, the possible ways in which the two approaches may be combined. Specially, we do not consider how the context of system routines can be integrated into the mentalist approach.

In this paper, we introduce two novel aspects concerning agent expectations. First, we extend the notion of expectation so that, in the context of system routines, it may be applied not only to the facts resulting from the execution of agent actions or environment events, but also to the actions and events themselves. In fact, we consider that objective expectations of actions and events are fundamental, and that objective expectations of facts should be derived from them. Accordingly, in Sect. 2 we formalize a notion of system routine where those two kinds of expectations may be defined.

Secondly, we would like to stay as close as possible to the subjective expected utility values approach to expectations. However, utility values, as such, can not be fruitfully considered in connection to actions and facts that happen in system routines. This is because routines are usually adopted in a system only when all the actions are clearly useful to the routines where they occur. That is, less useful actions tend to be replaced by actions more adapted, and thus more useful, to the routine and to the functioning of the system as a whole. If an action is included in a routine, or if a fact is counted upon by the routine to operate properly, it is clear that it certainly has a utility for the routine, and there is no point in trying to quantify that value. Therefore, in order that the objective expected utility of an action (or fact or event) could stay close to the model of subjective expected utility, it was necessary to replace the subjective components by corresponding objective components. Specially, the subjective probabilities and utility values that essentially constitute the subjective expected utility values were respectively replaced by objective probabilities and by objective degrees of perfection of the realization of actions, facts and events. This is explained in Sect. 3 of the paper.

A contextualized example of the approach is given in Sect. 4. Section 5 concludes the paper with a discussion.

Periodic Routines and their Performances

In the following, let Act be a finite set of agent actions and Ctx be the set of contexts where those actions may be performed, with the empty action denoted by ε. Let T = t 0 , t 1 , . . . be a linear, discrete time structure. The effects of the performance of an action α ∈ Act, in a context C ∈ Ctx, at a certain time t ∈ T , may be defined in a rule-based form with the help of pre-and post-conditions, which can assume degrees of perfection varying in the interval [0, 1], as the degrees of truth in Fuzzy Logic [START_REF] Zadeh | Fuzzy sets[END_REF], as follows: pre1 : d1 . . . pren : dn [α : C] post1 : f1(d1, . . . , dn) : min1 . . . postm : fm(d1, . . . , dn) : minm

where pre[α : C] = {pre 1 , . . . , pre n }, with n ∈ N, is the set of pre-conditions to be evaluated at any time the action α is ready to be performed in the context An action α is said to be satisfactorily performed in the context C, at time t ∈ T , if and only if each post-condition assumes, at time t + 1, a degree of perfection equal or greater than the minimum degree of perfection required for that post-condition. In particular, a satisfactorily performed action α is said to be perfectly performed in the context C, at time t, if and only if all post-conditions assume, at time t + 1, a degree of perfection equal to 1. An action α is said to be non-satisfactorily performed in the context C, at time t, if and only if at least one of the post-conditions assumes, at time t + 1, a degree of perfection less than the minimum required for that post-condition. A non-satisfactorily performed action α is said to be non-performed at time t, if and only if all post-conditions assume, at time t + 1, a degree of perfection equal to 0. Definition 1. Let α ∈ Act be an action performed in the context C at time t. The degree of satisfaction of α's performance is given by the function ds t α:C : [0, 1] m → {s, ns} × [0, 1]. This evaluates the degrees of perfection u 1 , . . . , u m ∈ [0, 1] assumed, at time t + 1, by the post-conditions post 1 , . . . , post m of the action α. It generates a pair ds t α:C (u 1 , . . . , u m ) = (x, k) ∈ ({s, ns} × [0, 1]), where:

(i) k ∈ [0, 1] is the degree of perfection, obtained by an operator τ : [0, 1] m → [0, 1],
which is application dependent; (ii) x = s indicates that the action α was satisfactorily performed (so that k > 0; in particular, if k = 1 then the action α was perfectly performed); (iii) x = ns indicates that the action α was non-satisfactorily performed (so that k < 1; in particular, if k = 0 then α was non-performed);

A routine over Act, in a context C ∈ Ctx, with period π, where π ∈ N and π > 1, is a permanently (i.e., infinitely) repeated, structured subset of actions of Act in C. The main repeated structured set of actions in a routine ρ is the body of ρ. The set of all possible routine bodies RB Act is given by a set of regular expressions over Act:

any action α ∈ Act is a routine body: The length of a routine body is defined as shown in the left-hand column of Table 1. The length of a routine's body is the period of that routine (note the case of the parallel composition, reserving a time slot for its eventual sequential realization, with one alternative fully performed before the other). So, any routine ρ, with period π, is such that ρ = b ω , where b ∈ RB Act , π = length(b), and ω indicates infinite repetition of the body b. The set of actions of the routine ρ = b ω , denoted by act[ρ], is the same as the set of actions of its body, as defined in the right-hand column of Table 1.

α ∈ Act ⇒ α ∈ RB Act -if
(b) = 1, if b = α ∈ Act act[b] = {α}, if b = α ∈ Act length(b; b ′ ) = length(b) + length(b ′ ) act[b; b ′ ] = act[b] ∪ act[b ′ ] length(b + b ′ ) = max{length(b), length(b ′ )} act[b + b ′ ] = act[b] ∪ act[b ′ ] length(b | b ′ ) = length(b) + length(b ′ ) act[b | b ′ ] = act[b] ∪ act[b ′ ] length(b n ) = n • length(b) act[b n ] = act[b] • b | b ′ ∈ RB Act (parallel
A cut of a routine ρ is any non-empty subset of actions in Act that the routine may simultaneously perform at a given time instant. The set of cuts of a routine ρ = b ω is denoted by Cuts[ρ] and is the same as the set of cuts of its body Cuts[b], which is defined recursively as follows, for routine bodies b, b ′ ∈ RB Act :

Cuts[b] = {{α}}, if b = α ∈ Acts Cuts[b; b ′ ] = Cuts[b] ∪ Cuts[b ′ ] Cuts[b + b ′ ] = Cuts[b] ∪ Cuts[b ′ ] Cuts[b | b ′ ] = Cuts[b] ∪ Cuts[b ′ ] ∪ {X ∪ Y | X ∈ Cuts[b], Y ∈ Cuts[b ′ ]} ∪ {{ε}} Cuts[b n ] = Cuts[b]
The notion of a cut of a routine is central to our concept of routine expectation. It was drawn from the notion of cut in occurrence nets from Net Theory [START_REF] Petri | Net Theory and Applications. Number 84 in LNCS[END_REF]. Definition 2. Let ρ be a routine over Act and Cuts[ρ] be the set of cuts of ρ. A performance of a routine ρ in the context C is a periodic mapping

≪ ρ : C ≫: T → ℘(Cuts[ρ]) × Cuts[ρ] × ℘(Act) × ℘(Act × [0, 1]),
which gives, for each time t ∈ T , a 4-tuple where:

(i) the first component ≪ ρ : C ≫ t [1] is the set of cuts enabled by the performance ≪ ρ : C ≫ at time t; (ii) the second component ≪ ρ : C ≫ t [2] is the cut selected to be performed at time t in ≪ ρ : C ≫, among the enabled cuts at that time; 5 (iii) the third component ≪ ρ : C ≫ t [3] is the step of the performance ≪ ρ : C ≫ at time t, which is the subset of actions of the selected cut ≪ ρ : C ≫ t [2]
that are put into execution by the system's agent(s) at time t;

(iv) the fourth component ≪ ρ :

C ≫ t [4] is the result of the step ≪ ρ : C ≫ t [3],
indicating the degree of satisfaction of the performance of each action of that step.

The period of the performance ≪ ρ : C ≫ is given by the period of ρ. The set of all possible performances ≪ ρ : C ≫ of ρ in the context C is denoted by Prfs

[≪ ρ : C ≫] t and ecuts[≪ ρ : C ≫] t =≪ ρ : C ≫ t [1]
. The trace of subsets of enabled cuts by

≪ ρ : C ≫ in T is defined as the time-indexed sequence: trace[ecuts[≪ ρ : C ≫]] T = ecuts[≪ ρ : C ≫] t 0 , ecuts[≪ ρ : C ≫]
ρ : C ≫] t =≪ ρ : C ≫ t [2] ∈ ecuts[≪ ρ : C ≫] t . The trace of selected cuts by ≪ ρ : C ≫ in T is defined as the time-indexed sequence: trace[scut[≪ ρ : C ≫]] T = scut[≪ ρ : C ≫] t 0 , scut[≪ ρ : C ≫] t 1 , . . . . (iii)
The steps of the performance ≪ ρ : C ≫ are specified by a mapping step : Prfs[ρ :

C] → T → ℘(Act), such that, given the selected cut scut[≪ ρ : C ≫] t , the subset of actions that are executed by the agent at the time t is denoted by

step[≪ ρ : C ≫] t and step[≪ ρ : C ≫] t =≪ ρ : C ≫ t [3] ⊆ scut[≪ ρ : C ≫] t .
The trace of steps of the performance ≪ ρ : C ≫ in T is defined as the time-indexed sequence:

trace[step[≪ ρ : C ≫]] T = step[≪ ρ : C ≫] t 0 , step[≪ ρ : C ≫] t 1 , . . . . (iv)
The results of the steps of the performance ≪ ρ : C ≫ at time t is given by a mapping result :

Prfs[ρ : C] → T → ℘(Act × [0, 1]) such that, given the step step[≪ ρ : C ≫] t of the performance ≪ ρ : C ≫ at time t ∈ T , the set of results of that step is denoted by result[≪ ρ : C ≫] t and result[≪ ρ : C ≫ ] t =≪ ρ : C ≫ t [4] = {(α, ds t α:C (u 1 , . . . , u m )) | α ∈ step[≪ ρ : C ≫] t }
, where ds t α:C (u 1 , . . . , u m ) is the degree satisfaction of the performance of α, obtained by the evaluation of the degrees of perfection u 1 , . . . , u m assumed by α's post-condition post 1 , . . . , post m at time t + 1 (see Def. 1). The trace of results of steps of the performance ≪ ρ : C ≫ in T is given by the sequence:

trace[result[≪ ρ : C ≫]] T = result[≪ ρ : C ≫] t 0 , result[≪ ρ : C ≫] t 1 , . . .
The set of possible steps of a cut c is the set of its subsets ℘(c). Given a family of cuts X, the set of possible steps derived from X is given by psteps

[X] = c∈X ℘[c].
The effects of a cut c ∈ Cuts[ρ], in a context C, may be defined in a rule-based form with the help of pre-and post-conditions, analogously to rule [START_REF] Castelfranchi | Mind as an anticipatory device: For a theory of expectations[END_REF], where the set of pre-conditions is the union of the sets of pre-conditions of all the actions that constitute the cut c, given by pre

[c] = {pre[α] | α ∈ c}. Similarly, the set of post-conditions of a cut c ∈ Cuts[ρ] is given by post[c] = {post[α] | α ∈ c}. Considering a performance ≪ ρ : C ≫∈ Prfs[ρ : C] in a context C ∈ Ctx, a selected cut c ∈ ecuts[≪ ρ : C ≫] t is
said to be satisfactorily (perfectly) performed at time t if and only if all its actions are satisfactorily (perfectly) performed at that time. On the contrary, a selected cut c ∈ ecuts[≪ ρ : C ≫] t is non-satisfactorily performed at time t if and only if at least one of its actions is non-satisfactorily performed at time t. A non-satisfactorily performed selected cut c is said to be non-performed at time t if and only all its actions are non-performed at time t.

Given a selected cut c ∈ ecuts[≪ ρ : C ≫] t , the set of pre-conditions of a step s ⊆ c is the union of the set of pre-conditions of the actions that constitute that step, that is,

pre[s] = {pre[α] | α ∈ s} ⊆ pre[c]. Analogously, the set of post-conditions of a step s ⊆ c is given by post[s] = {post[α] | α ∈ s} ⊆ post[c].
A step s ⊆ c can either be satisfactorily (perfectly, non-satisfactorily) performed or non-performed, in the same way as was defined for selected cuts.

Therefore, a selected cut scut[≪ ρ : C ≫] t of a routine performance ≪ ρ : C ≫ at time t is satisfactorily (or perfectly) performed if and only if step[≪ ρ : 7Definition 4. Consider a routine ρ over Act, in a given context C ∈ Ctx, with period π, whose performance ≪ ρ : C ≫ is done in a time sequence T = t 0 , t 1 , . . .. Then:

C ≫] t = scut[≪ ρ : C ≫] t and step[≪ ρ : C ≫] t is satisfactorily (or perfectly) performed. It is non-satisfactorily performed if either step[≪ ρ : C ≫] t = scut[≪ ρ : C ≫] t or step[≪ ρ : C ≫] t is non-satisfactorily performed. It is non-performed whenever either step[≪ ρ : C ≫] t = ∅ or step[≪ ρ : C ≫] t is non-performed.
(i) The performance ≪ ρ : C ≫ is
C] = {c 1 , c 2 , c 3 }, where c 1 = {α 1 }, c 2 = {α 2 } and c 3 = {α 3 }.
The cuts enabled during a perfectly performed performance ≪ ρ : C ≫ in the time interval [t 0 , t 2 ) (just one cycle) are given by: ecuts[≪ ρ :

C ≫] t0 = {c 1 }, ecuts[≪ ρ : C ≫] t1 = {c 2 , c 3 }.
Then, there are only two possibilities of traces of a perfectly performed performance ≪ ρ : C ≫ in that interval:

(i) either the selected cuts are scut[≪ ρ : C ≫] = t 0 → c 1 , t 1 → c 3 , and the traces of steps and results of steps are, respectively:

trace[step[≪ ρ : C ≫]] [t 0 ,t 2 ) = t0 → c1, t1 → c2 trace[result[≪ ρ : C ≫]] [t 0 ,t 2 ) = t0 → {(α1, (s, 1))}, t1 → {(α2, (s, 1))}
(ii) or, the selected cuts are scut[≪ ρ : C ≫] = t 0 → c 1 , t 1 → c 2 , and the traces of steps and results of steps are, respectively:

trace[step[≪ ρ : C ≫]] [t 0 ,t 2 ) = t0 → c1, t1 → c3, trace[result[≪ ρ : C ≫]] [t 0 ,t 2 ) = t0 → {(α1, (s, 1))}, t1 → {(α3, (s, 1))},
where each step in each time, which coincides with the cut selected at that time, is perfectly performed. Consider that the pre-conditions of both actions α 2 and α 3 are the post-conditions generated by the performance of the action α 1 , and the minimum degrees of truth required for the post-conditions of both α 2 and α 3 are equal to 1. Then, supposing that, in both cases (i) and (ii) above, one has that result[≪ ρ :

C ≫ ] t0 = {(α 1 , (s, k 1 < 1))}, then, probably, one would have result[≪ ρ : C ≫] t0 = {(α 2 , (ns, k 2 < 1))} (in case (i)) or result[≪ ρ : C ≫] t0 = {(α 3 , (ns, k 3 < 1))} (case (ii))
, characterizing examples of ≪ ρ : C ≫ that are non-satisfactorily performed (failed performances whenever

k 1 = k 2 = k 3 = 0). Example 2. Consider Act = {α 1 , α 2 , α 3 } and let ρ = ((α 1 + α 2 ) 3 | α 3
) ω be a routine with period equal to 4. The possible cuts in the performance of this routine are Cuts[ρ : 2 shows the cuts enabled during a performance ≪ ρ : C ≫ in 5 cycles, the selected cuts in each time t and the trace of steps of the performance, which was perfectly performed in the first cycle, but failed in the second cycle, since the cut at time t 6 failed. The third and fourth cycles ≪ ρ : C ≫ were just non-satisfactorily performed, since the cuts at times t 8 and t 12 were non-satisfactorily performed. At time t 8 , the action α 1 of the selected cut at that time was executed in the respective performance step, with a performance satisfactoriness degree of 0.5, but in a non-satisfactory way (since at least one of its post-conditions did not have the required minimum degree of truth). At time t 12 , the action α 3 of the selected cut at that time was not even executed in the respective performance step. Finally, the fifth cycle failed, since the step at time t 19 was empty.

C] = {c 0 , c 1 , c 2 , c 3 , c 4 , c 5 }, where: c 0 = {ε}, c 1 = {α 1 }, c 2 = {α 2 }, c 3 = {α 3 }, c 4 = {α 1 , α 3 } and c 5 = {α 2 , α 3 }. Table

Expectations

We consider two kinds of expectations: (i) expectations of actions, that is, that some set of actions happen in the performance of a given routine at a given time, and (ii) expectations of facts, which are expectations that some facts become true, with a certain degree, as a consequence of some set of actions occurring in a given routine at a given time. For example, in calendar systems [START_REF] Crépin | Privacy preservation in a decentralized calendar system[END_REF], expectations of actions typically occur when a user requests that the personal assistants perform some actions for him or her. Alternatively, expectations of facts occur when personal assistants interact together in order to fulfil a global goal that is given by the user they support.

{c0, c1, c2, c3, c4, c5} {c0, c1, c2, c3, c4, c5} {c0, c1, c2, c3, c4, c5} {c0} c1 c1 c5 c0 c1 c1 c5 c0 {(α1, (s, 1))} {(α1, (s, 1))} {(α2, (s, 1)), (α3, (s, 1))} {(ε, (s, 1))} t4 t5 t6 t7 {c0, c1, c2, c3, c4, c5} {c0, c1, c2} {c0, c1, c2} {c0} c5 c2 c1 c0 c5 c2 c1 c0 {(α2, (s, 1)), (α3, (s, 1))} {(α2, (s, 1))} {(α1, (ns, 0))} {(ε, (s, 1))} t8 t9 t10 t11 {c0, c1, c2, c3, c4, c5} {c0, c1, c2} {c0, c1, c2} {c0} c4 c1 c2 c0 c4 c1 c2 c0 {(α1, (ns, 0.7)), (α3, (s, 1))} {(α1, (s, 1))} {(α2, (s, 1))} {(ε, (s, 1))} t12 t13 t14 t15 {c0, c1, c2, c3, c4, c5} {c0, c1, c2} {c0, c1, c2} {c0} c4 c1 c2 c0 {α1} c1 c2 c0 {(α1, (s, 1))} {(α1, (s, 1))} {(α2, (s, 1))} {(ε, (s, 1))} t16 t17 t18 t19 {c0, c1, c2, c3, c4, c5} {c0, c1, c2, c3, c4, c5} {c0, c1, c2, c3, c4, c5} {c3} c1 c1 c2 c3 c1 c1 c2 ∅ {(α1, (s, 1))} {(α1, (s, 1))} {(α2, (s, 1))} ∅ . . . . . . . . . . . . Given the set E = ecuts[≪ ρ : C ≫] ti ⊆ Cuts[ρ]
of the cuts enabled by a performance ≪ ρ : C ≫ at a certain time t i ∈ T , it may be possible to have a cut-selection probability distribution over E, given by χ ti ≪ρ:C≫ : E → [0, 1], such that, for each c ∈ E, χ ti ≪ρ:C≫ (c) gives the probability of the selection of c, considering the context C ∈ Ctx, such that c∈E χ ti ≪ρ:C≫ (c) = 1. Denote by ρ χ the routine ρ with associated cut-selection probability functions χ ti ≪ρ:C≫ , where i ∈ N. Definition 5. Given a performance ≪ ρ χ : C ≫ of a routine ρ χ in a context C, the cut selection expectation of ≪ ρ χ : C ≫ at a certain time t i ∈ T is the subset of cuts of the cuts enabled at time t i whose cut-selection probabilities are maximal in

ecuts[≪ ρ χ : C ≫] t ⊆ Cuts[ρ χ ], that is, csxpt[≪ ρ χ : C ≫] ti = {c ∈ ecuts[≪ ρ χ : C ≫] ti | ∀c ′ ∈ ecuts[≪ ρ χ : C ≫] ti : χ ti ≪ρ:C≫ (c ′ ) ≤ χ ti ≪ρ:C≫ (c)}
Given the cut scut[≪ ρ : C ≫] ti , selected at time t i in a performance ≪ ρ : C ≫, the probability that an action α ∈ scut[≪ ρ : C ≫] ti is executed in the step step[≪ ρ : C ≫] ti by an agent, in the context C ∈ Ctx and at t i , is given by the function

φ ti scut[≪ρ:C≫] t i : scut[≪ ρ : C ≫] ti → [0, 1]. The probability of α ∈ scut[≪ ρ : C ≫] ti not being executed in the step step[≪ ρ : C ≫] ti is 1 -φ ti scut[≪ρ:C≫] t i (α).
Then, the probability of a step being executed in scut[≪ ρ : C ≫ ti ] is given by the function

Φ ti scut[≪ρ:C≫] t i : ℘[scut[≪ ρ : C ≫] ti ] → [0, 1], defined by Φ t i scut[≪ρ:C≫] t i (X) = α∈scut[≪ρ:C≫] t i P r(α), with P r(α)= φ t i scut[≪ρ:C≫] t i (α) if α ∈ X 1-φ t i scut[≪ρ:C≫] t i (α) otherwise. (2)
Denote by ρ Φ the routine ρ with associated step probability functions Φ ti scut[≪ρ:C≫] t i for each selected cut, with i ∈ N.

Definition 6. Given a performance ≪ ρ Φ : C ≫, the step expectation in a cut scut[≪ ρ Φ : C ≫] ti selected at time t i , are the steps of the cut scut[≪ ρ Φ : C ≫] ti whose probabilities of being executed at

t i are maximal in ℘[scut[≪ ρ Φ : C ≫] ti ]: stxpt[scut[≪ ρΦ : C ≫]] t i = {X ∈ ℘[scut[≪ ρΦ : C ≫] t i ] | ∀X ′ ∈ ℘[scut[≪ ρΦ : C ≫] t i ] : Φ t i scut[≪ρ Φ :C≫] t i (X ′ ) ≤ Φ t i scut[≪ρ Φ :C≫] t i (X)}.
The overall step probability of any possible step being executed in a performance ≪ ρ : C ≫ at a given time t i ∈ T is given by a function σ ti ≪ρ:C≫ : psteps[ecuts[≪ ρ : C ≫]] t1 → [0, 1], defined by:

σ t i ≪ρ:C≫ (X) = c∈ecuts[≪ρ:C≫] t 1 χ t i ≪ρ:C≫ (c) • P r(X), with P r(X) = Φ t i c (X) if X ⊆ c 0 otherwise, (3)
where χ and Φ are the cut-selection probability functions and step probability functions, respectively. Denote by ρ σ the routine ρ with associated overall step probability functions σ ti ≪ρ:C≫ , with i ∈ N. Definition 7. The possible-step expectation of a performance ≪ ρ σ : C ≫ ti , at a certain time t i ∈ T , is the subset of possible steps whose probabilities of being executed by the performance ≪ ρ σ : C ≫ of the routine ρ σ at time

t i and context C are maximal in psteps[ecuts[≪ ρ σ : C ≫]] t1 , that is, psxpt[ecuts[≪ ρσ : C ≫]] t 1 = {X ∈ psteps[ecuts[≪ ρσ : C ≫]] t 1 | ∀X ′ ∈ psteps[ecuts[≪ ρσ : C ≫]] t 1 : σ t i ≪ρσ :C≫ (X ′ ) ≤ σ t i ≪ρσ :C≫ (X)}.
Then, considering a routine with period π, the possible step expectation of a performance ≪ ρ σ : C ≫, in a period that starts at time t i , is a sequence

psxpt[≪ ρσ : C ≫] π = psxpt[≪ ρσ : C ≫] t i , . . . , psxpt[≪ ρσ : C ≫] t i +π-1 .
Definition 8. The expectation of the result of an action α ∈ Act in a context C, at time t i , is defined as rxpt[α : C] t i ≡ pre1 : d1, . . . , pren : dn ⇒ post1 : f1(d1, . . . , dn), . . . , postm : fm(d1, . . . , dn), [START_REF] Savage | The Foundations of Statistics[END_REF] where f 1 , . . . , f m : [0, 1] n → [0, 1] are the functions giving the expected degrees of perfection of the post-conditions post 1 , . . . , post m of α, considering the degrees of perfection d 1 , . . . , d n of the pre-conditions pre 1 , . . . , pre n at time t i . 8The expectation of the result of a set of actions X ⊆ Act, which are performed at a certain time t i in a context C, is defined as rxpt

[X : C] ti = {rxpt[α : C] ti | α ∈ X}. Definition 9. Consider a possible-step expectation psxpt[≪ ρ σ : C ≫ ti ] of a perfor- mance ≪ ρ σ : C ≫, at a certain time t i ∈ T . The expectation of the results of a performance ≪ ρ σ : C ≫ at time t i , is then defined as rxpt[≪ ρ σ : C ≫] ti = {rxpt[X : C] ti | X ∈ psxpt[≪ ρ σ : C ≫] ti }.
The resulting expectation of ≪ p ρσ : C ≫, in a period π that starts at time

t i , is rxpt[≪ ρ σ : C ≫] π = rxpt[≪ ρ σ : C ≫] ti , . . . , rxpt[≪ ρ σ : C ≫] ti+π-1 .

A Contextualized Example

Consider the routine ρ σ of a porter (agent a 1 ), who is in charge of opening and closing the front-door of a building, and a person (agent b) who needs to get inside the building to reach the office where he works everyday. Let the routine be represented in the Petri net shown in Fig. 1, where

= {ε}, c 1 = {β 1 }, c 2 = {α 1 }, c 3 = {β 2 }, c 4 = {α 1 , β 2 }, c 5 = {β 3 }, c 6 = {α 2 }, c 7 = {β 4 }, c 8 = {β 5 } , c 9 = {α 2 , β 4 } e c 10 = {α 2 , β 5 }.
Let χ ti ≪ρ:C≫ be the cut-selection probability functions associated to ρ σ and consider a particular performance ≪ ρ σ : C ≫ in a context C, where, at time t 1 , the enabled cuts are ecuts[≪ ρ σ : C ≫] t1 = {c 0 , c 2 , c 3 , c 4 }, and the cut-selection probabilities are χ t1 ≪ρσ:C≫ (c 0 ) = 0.05, χ t1 ≪ρσ:C≫ (c 2 ) = 0.1, χ t1 ≪ρσ:C≫ (c 3 ) = 0.15 and χ t1 ≪ρσ:C≫ (c 4 ) = 0.7. Then, the cut selection expectation of ≪ ρ

σ : C ≫ is csxpt[≪ ρ σ : C ≫] t1 = {c 4 }, that is, the cut that is expected to be selected at time t 1 is c 4 = {α 1 , β 2 }.
Consider that the cut that is selected at time t 1 fits that expectation, that is, scut[≪ ρ σ : C ≫] t1 = c 4 . Suppose that the porter (agent a) is very attentive, and usually opens the door (action α 1 ) when the office employee appears in the scene. However, the office employee (agent b) is easily distracted and sometimes stops before approach-ing the door (action β 2 ) in order to do an action that is not in the routine, such as to talk to someone or to answer the mobile phone. Suppose that the probabilities of the actions α 1 , β 2 ∈ c 4 being executed at the step at time t 1 are φ t1 c4 (α 1 ) = 0.9 and φ t1 c4 (β 2 ) = 0.7, respectively. The possible steps of the selected cut c 4 are given by ℘[c 4 ] = {∅, {α 1 }, {β 2 }, {α 1 , β 2 }}. Then, the probability of each possible step being executed at time t 1 , according to Eq. ( 2), is:

Φ t 1 c 4 (∅) = (1 -φ t 1 c 4 (α1)) • (1-φ t 1 c 4 (β2)) = 0.03, Φ t 1 c 4 ({α1}) = φ t 1 c 4 (α1) • (1-φ t 1 c 4 (β2)) = 0.27 Φ t 1 c 4 ({β2}) = (1 -φ t 1 c 4 (α1)) • φ t 1 c 4 (β2) = 0.07, Φ t 1 c 4 ({α1, β2}) = φ t 1 c 4 (α1) • φ t 1 c 4 (β2) = 0.63.
The step expectation related to the cut c 4 at time

t 1 is sxpt[≪ ρ σ : C ≫] t1 ={{α 1 , β 2 }}.
The probability of the possible steps being executed in the performance ≪ ρ σ : C ≫ at time t 1 (Eq. ( 3)), given that the enabled cuts are ecuts[≪ ρ σ ≫] t1 = {c 0 , c 2 , c 3 , c 4 }, are:

σ t 1 ≪ρ:C≫ ({α1, β2}) = χ t i ≪ρ:C≫ (c4) • Φ t 1 c 4 ({α1, β2}) = 0.7 • 0.63 = 0.441 σ t 1 ≪ρ:C≫ ({α1}) = χ t 1 ≪ρ:C≫ (c2) • Φ t 1 c 2 ({α1}) + χ t 1 ≪ρ:C≫ (c4) • Φ t 1 c 4 ({α1}) = 0.279 σ t 1 ≪ρ:C≫ ({β2}) = χ t 1 ≪ρ:C≫ (c3) • Φ t 1 c 3 ({β2}) + χ t 1 ≪ρ:C≫ (c4) • Φ t 1 c 4 ({β2}) = 0.154 σ t 1 ≪ρ:C≫ (∅) = χ t 1 ≪ρ:C≫ (c0) • Φ t 1 c 0 (∅) + . . . + χ t 1 ≪ρ:C≫ (c4) • Φ t 1 c 4 (∅) = 0.126
Then, the possible-step expectation of the performance ≪ ρ σ : C ≫ at time t 1 is psxpt[≪ ρ σ : C ≫] t1 = {{α 1 , β 2 }}. Now, consider that the possible step at time t 1 is indeed the step {α 1 , β 2 }, and that the expectation of the performance result of the actions α Finally, consider the result expectation rxpt[α 1 : C] t1 and suppose that the door is half-open and that the porter is not sure that the employee is already at the scene, such that the degrees of perfection of α 1 's pre-conditions are d s2 = 0.9 and d s3 = 0.7 at time t 1 in the context C. In such a situation, the result expectation of the performance of α 1 is that the door may not be opened correctly, since the degree of perfection of α 1 's post-condition s 4 is expected to be f s4 (0.9, 0.7) = min{0.9, 0.7} = 0.7.

Notice, however, that the notion of routine is defined so that even if all pre-conditions are totally true (i.e., d s2 = d s3 = 1, so that f s4 (1, 1) = 1) there is always a possibility that the door is not correctly opened after the performance of α 1 . For instance, the action α 1 may not be performed correctly, or some condition (which happens only rarely and so is justifiably not included in the routine) occurs negatively affecting the result of the action.

Conclusion

This paper introduced an objective notion of expectation of actions and facts in the context of routine-oriented multiagent systems. Expectations were defined on behavioral terms, inspired by the notion of maximal expected utility, where utility values were substituted by degrees of perfection of actions (involving degrees of perfection of facts). The proposed notion of expectations was defined in order to ground the cognitive concept of expectation in the context of routine-oriented multiagent systems. In this way, notions that are essential for proactive agents, like surprise and disappointment, can be defined in such context. We hope to integrate these aspects in our future work. In terms of applications, such as modeling family behaviors in domestic settings [START_REF] Dugdale | Modélisation située des activités individuelles et collectives pour la conception[END_REF], our proposed approach may help the cognitive modeling of expectations, since the subjective model should be compatible with the objective one. The same may happen for personal assistants in, e.g., calendar systems [START_REF] Crépin | Privacy preservation in a decentralized calendar system[END_REF].

  b and b ′ are routine bodies (b, b ′ ∈ RB Act ), then the following regular compositions of b and b ′ are also routine bodies: • b; b ′ ∈ RB Act (sequential composition of the routine bodies b and b ′ ); • b + b ′ ∈ RB Act (alternative composition of the routine bodies b and b ′ );

  composition of the routine bodies b and b ′ ); 4 • b n ∈ RB Act (n-times repetition of the routine body b, with n ∈ N and n > 0);

  [ρ : C]. The four components of a performance are accessed through the following functions: Definition 3. Consider a performance ≪ ρ : C ≫ ∈ Prfs[ρ : C]. Then 6 : (i) The cuts enabled by the performance ≪ ρ : C ≫ in each time t are specified by a mapping ecuts : Prfs[ρ : C] → T → ℘(Cuts[ρ]), such that the cuts enabled by a performance ≪ ρ : C ≫, at a given time t ∈ T , is denoted by ecuts

2 α

 2 Table(a) Agent actions Action Agent: action specification α1 a: to open the door α2 a: to close the door β1 b: to enter into the scene β2 b: to approach the door β3 b: to pass through the open door β4 b: to withdraw from the door β5 b: to leave the scene

Fig. 1 .

 1 Fig. 1. The Petri net representation and action specifications of the routine ρ

1 and β 2

 2 in the context C are defined, respectively, as rxpt[α 1 : C] t1 ≡ s 2 : d s2 , s 3 : d s3 ⇒ s 4 : f s4 (d s2 , d s3 ) and rxpt[β 2 : C] t1 ≡ s 2 : d s2 ⇒ s 5 : f s5 (d s2 ) where s 2 , s 3 , s 4 and s 5 are situations specified in Fig. 1(b), and f s4 : [0, 1] 2 → [0, 1] and f s5 : [0, 1] → [0, 1], defined by f s4 (x, y) = min{x, y} and f s5 (x) = x, are the expecting functions of actions α 1 and β 2 , respectively, as specified in Eq. (4). Thus, the result expectation of the performance ≪ ρ : C ≫, at time t 1 , is rxpt[≪ ρ σ : C ≫] t1 = {{rxpt[α 1 : C] t1 , rxpt[β 1 : C] t1 }}.

  C, and d 1 , . . . , d n are their respective degrees of perfection at that moment; post[α : C] = {post 1 , . . . , post m }, with m ∈ N, is the set of post-conditions that result from the performance of α in the context C, and f 1 (d 1 , . . . , d n ), . . . , f m (d 1 , . . . , d n ) are their respective expected degrees of perfection after that performance, determined by the functions f 1 , . . . , f m : [0, 1] n → [0, 1] that give the expected values of the post-conditions considering the degrees of perfection of all pre-conditions; min 1 , . . . , min n , with 0 < min i ≤ 1, are the minimum degrees of perfection required for the post-conditions in order that the performance of the action α be considered satisfactory. In particular, it holds that d i = 1, for any pre i ∈ pre[ε : C], and f j (d 1 , . . . , d n ) = min j = 1, for any post j ∈ post[ε : C], in any context C.

Table 1 .

 1 Recursive definitions of length and set of actions of routine bodies, for b, b ′ ∈ RBAct

	Length	Set of actions
	length

Table 2 .

 2 Sample performances of the routine ρ = ((α1 + α2) 3 | α3) ω

	Time Enabled Cuts	Selected Cut	Step	Results
	t0
	t1
	t2
	t3

Table (

 (

		b) Conditions
	Notation Condition
	s1	the scene started
	s2	the office employee is in the scene
	s3	the door is closed
	s4	the door is open
	s5	the office employee is near the door
	s6	the office employee is inside the building
	s7	the office employee withdrew from the door
	s8	the scene ended
	Table(c) Action pre-and post-conditions
	Action Pre-conditions Post-conditions
	α1	{s2, s3}	{s4}
	α2	{s4, s6}	{s3}
	β1	{s1}	{s2}
	β2	{s2}	{s5}
	β3	{s4, s5}	{s6}
	β4	{s6}	{s7}
	β5	{s7}	{s8}

  Table(a) specifies the agent actions involved in ρ σ , Table (b) specifies the conditions that may occur in ρ σ , and Table(c) specifies the pre-and post-conditions of those actions in terms of such situations.The structure of the routine ρ σ can be described as ρ = (β 1 ; (α 1 | β 2 ); β 3 ; (α 2 | β 4 ; β 5 )) ω . Routine ρ σ has period π = 7 and overall step probability functions σ ti ≪ρ:C≫ (specified below). The possible cuts in any performance of ρ are c 0

Observe that the empty action ε is the neutral element of the parallel composition operator, that is, ε | b = b | ε = b, for any routine body b.

A routine may enable more than one cut at a given time. However, only one cut must be selected to be performed at each time.

For simplicity, in this paper, given any function f : T → X, where T is the time sequence, we denote f (t) by f t .

Observe that the enablement of a subset of cuts of a routine ρ at time t + 1 of a performance ≪ ρ : C ≫ may depend on the step of the performance of the routine ρ at time t, which indicates if the cut selected at time t was or was not satisfactorily performed.

The notion of expectation of the result of an action can be treated as a particular case of the notion of expectation adopted in[START_REF] Cranefield | Verifying social expectations by model checking truncated paths[END_REF][START_REF] Cranefield | Modelling and monitoring social expectations in multi-agent systems[END_REF], if one includes the treatment of probabilities and degrees of perfection of realization of actions in periodic routines.

Acknowledgements. This work was done while ACRC was visiting lecturer at UJF, and GPD was an invited researcher at the LIG/MAGMA Group, in Grenoble, between January and February 2009. Support from CNPq and CAPES is also acknowledged. The authors thank M. Piunti for noting how the objective degrees of perfection could support a notion of utility value (related to routines, not to actions) for the system as a whole.


Vincent Janes

Eric Klein

Sébastien Romon

Franziska Schmidt

Hai Pham Doan

DESIGNING WIM DATA AGGREGATING SYSTEMS Ajouter photo

Keywords: Weigh-in-motion (WIM), database, heavy vehicles Pesage en marche (WIM), base de données, véhicules lourds

WIM systems are still a fairly young technology. Like many developing technology platforms, these are subject to fragmentation in terms of uses and standards. This paper addresses to efforts aimed at dealing with this fragmentation by observing two on-going projects. First system considered is the FIWI WIM database led by ISWIM, which through a cooperative effort aims at creating a WIM sensors and systems cartography. Second system considered is SITL system, which aims at developing a WIM data processing system. It is based mostly on open-source or free-use software. This system, while having a short term operational goals, is also meant as a demonstrator for promoting a formal WIM data model. Those two projects aim at serving and strengthing WIM users community by mutual understanding and promotion of common tools.

Introduction

Compared to other roadside technologies WIM is fairly recent. While a lot of effort has been placed on sensor and measurement technologies, from our experience, data exploitation could be improved. This article deals with two on-going projects aiming at getting a better return on available measurements.

From our experience even inside a single country, WIM data is largely fragmented, both qualitatively and quantitatively. Qualitatively:

type of measurable data depends on type of sensor considered, type of actually collected data depends on collection architecture, measurement specs depend on sponsor's particular needs, data format depends on manufacturers' choice. Quantitatively, even for a single type of measurement:

data is spread between several different agencies, even inside a single agency it is not unusual to have several distinct repositories. Even when different organisms use the same tools or data format it is still unusual for them to share their data. Also many WIM systems we did encounter had limited exploitation tools implemented.

In addition to those facts, technical progress in recent period, notably in data storage (size and price) and communication network (3G…) has strongly affected the size and type of data storages we are able to consider.

All those elements led us into working on projects aiming at improving data knowledge and processing.

Two on-going projects deal with those observations: FIWI database is a website aimed at gathering WIM related information from various sources and thus establishing a description of data panorama. It has an important cooperative aspect. SITL is a more technical oriented project as it aims at aggregating data from a two well described fragmented sources into agile entity.

FIWI database project aims at embracing data diversity while BDTL project aims at performing synthesis in a given instance.

FIWI-WIM database

FIWI-WIM database is a subset of ISWIM. It aims at providing ISWIM members with information regarding FIWI deployment and activity in other countries and agencies. This database will be made available on the FIWI webpage www.free.fiwi.fr before Spring 2012.

System relies on a PHP-MySQL architecture web interface for accessing and managing data.

There are four parts that can be accessed by tags: a list of all WIM sites that are included in this database, aggregated data (which are the statistics of the WIM data files that can be found on the webpage), the detailed data which are the WIM files that are given by the WIM stations and the membership login and explanation.

WIM sites database

The WIM sites database webpage lists WIM equipment deployment. WIM equipments are described through a detailed pre-set template that addresses their main features: location, site characteristics, lanes, WIM type, sensor type, calibration method, data collected…

Aggregated data

Also in addition to site detailed description is uploaded aggregated data. As opposed to site data that is aimed as describing WIM systems, those statistics provide traffic description elements like traffic volume, weight and vehicle type distributions… These figures give context elements for WIM system implementation and general hints regarding regional traffic conditions and regulation.

Data samples

This database is not meant as a quantitative exhaustive data storage but rather as a explanatory depiction. Thus the webpage doesn't contain large bulks of data that may be expensive in terms of storage and would probably not be available for confidentiality reasons, but rather small data samples allowing for understanding of data formats and system architecture.

Data samples are documented prior to publication by a standard upload form listing their main features, notably measured parameters (vehicle type, timestamp, lane, speed, length, gross weight, number of axles, axle loads…) and data collection period and duration.

Principle and membership

This webpage is meant as a cooperation platform: Data collection is done by member voluntary contributions. Every member which has WIM data available and wants to share, can login on the webpage and provide some pieces of WIM data (the registration is monitored by the administrator of the webpage). Data administration is shared between the system administrator and voluntary members acting as regional data "supervisors" (per country or region). The webpage is available to guests although most data is only available to registered members. So there are several memberships:

Simple guest which are just visiting the webpage just see very fiew pieces of WIM data, Registered FIWI members (the registration is simple, free and can be done on the FIWI webpage) see more WIM data, Data providers are people who own WIM data and upload it on the webpage. This data is not shown directly on the webpage, but must be approved by the supervisors. These supervisors control the WIM data uploaded by the providers, check it and if and when they approve it, it will appear for other people.

The administrator of the system checks the memberships of the supervisors.

Through this cooperative effort, member community is able to develop a shared vision of WIM équipement deployment and ways of use. This effort can prove itself useful in fueling new systems development and joint initiatives.

Some shotscreens

In this paragraph, we show you 2 shotscreens of this database, giving you a general idea of the formatting and objective of this webpage. The first shotscreen, in Figure 1, shows you how is configured the page giving you access to the aggregated data available. The second one, in Figure 2, is a shotscreen of the page making it possible for the data provider to upload some WIM data.

Figure 1: Shotscreen of the webpage of the database FIWI giving the list of WIM stations with aggregated data available.

Figure 2: Webpage where the data provider can upload new data. This data is then reviewed by his supervisor, before it is visible on the visible webpage.

SITL

3.1 Context SITL, for "Système d'Information Trafic Lourd" (Heavyweight Traffic Information System), originates mostly from a road structure related need but it also aims at catering several other needs.

SITL idea emerged after an important push in field sensor deployment. HS-WIM sensor network has organically developed. It started with a limited number of sensors that was increased over the years. As for most pioneering projects, most of the support organization was developed "on the spot" as needs made themselves apparent. This evolution notably applied to analysis system that was incrementally up-graded.

Then population grew, and the data stack slowly built itself. The incremental evolution type has several advantages in project early stages but also bears growth problem that tend to sum up over time. While original system catered for most of expressed needs it was becoming increasingly difficult to maintain and new development seemed compromised by early choices.

WIM sensor deployment is an expensive process, both in terms of finance and political will, so it is important it bears fruits. We felt we could improve the return on those equipments by improving our analysis tool, and that for that purpose we needed to go into recreating it from the beginning.

Objectives

The situation reading was basically that we had amassed a huge amount of data and knowhow but we couldn't fully take advantage from it because it was fragmented and lacked a proper architecture. So our objectives were to: capture most of this valuable existing knowledge and to integrate it into a durable agile model, make it available and usable to larger audience comprising: specialists such as researchers and R&D users, end-users such as road administrations or law enforcement (regarding max weight enforcement).

Design principles

Off-the shelf conceptual models

We did not intend to create new concepts. On the contrary, we tried to stick to well-known and proven concepts, as often as possible. In the long run, popular off-the shelf model will prove more durable than obscure in-house particular models. Popular models also mean there is a higher chance people have studied, are familiar or can get information on subject, or that tools exist or are developed for it.

Standard compliance

Prolonging precedent principle, compliance to public standards broadens the audience further and deeper to anyone familiar with them. Anyone skilled in used standards can get quickly started, all existing standard-compatible tools can be quickly applied.

Clarity over optimization

We ruled that clarity had to be considered a prime objective over low-level optimization.

While we aimed at a robust and functional model we ruled we wouldn't embark in fine, product-specific tuning and would rely on general software and hardware improvement for improvement, which good standard compliance would help us integrate.

Open-source approach

Project was completely developed on free open-source software by non-specialist developers. That approach might be slightly detrimental in terms of performance over custom designed project but difference could be remedied at lower cost over time by hardware investment and flexibility and compatibility with community input could largely make up for this limitation.

It also allows for quick deployment and distribution without any licensing hassle.

Choices

Deciding to use off-the-shelf models saves time in conception but also requires investing some time in researching and choosing among existing models. After some digging we elected a few concepts that seemed us strong and rich enough to base our architecture on them. Those concept were: relational database model, business intelligence model.

Relational Model (SQL)

Regarding relational database it was also a very strong pillar, relational database (often known as SQL databases) have been invented in the 70s. They are widespread and a very mature field: RDBS offering is very mature. There are number of very powerful systems including open-source. The off-the-shelf associated tools offering is also constantly growing.

We settled for Postgresql which seemed technically adequate, completely free, as opposed to other systems like MySQL, and backed by open-software foundation rather than a commercial firm.

Databases and SQL subject have become a mainstream academic subject which means it is easy to find people competent on subject.

Figure 2 Main components used

Business Intelligence (BI)

Historically, business intelligence was invented as a way to analyze business data for large commercial firms, like sales per shop or per city, industrial costs, hence the "business" term, but those techniques are actually applicable to any decision-making activity. SAP-Business Object or SpagoBI are example of well-known BI tools.

In an initial step we chose not to implement any particular BI interface but we retained a typical BI star-schema. While initial interface would be a simple web query interface, this provision would allow to later implement most common BI tools or to connect some third party application.

Hardware improvement

We took into account trends into hardware improvement, notably we thought recent and future improvement in communication network speed and improvements in data-storage. The foresight in hardware improvement led us to consider large exhaustive storage.

Functionally oriented architecture

Our architecture is functionally oriented, which means it is based on WIM principles rather than purely software rules. While this is a downside in the sense it is probably less optimized than a more software-oriented architecture, it is also an upside in the sense that it makes the architecture easier to apprehend for any WIM worker.

Implementation

General principles and technical choices were settled we started developing core system tools.

Source Data

We have been working about two different formats; in the context of this article we'll mostly discuss the per-vehicle micro-data format. Data is produced by "EPM" WIM equipment network. Each equipment is out-fitted with a dedicated ADSL internet connection which allows for high data volumes. Data for all stations is currently gathered on a centralized data server. Data repository consists in XML format, under a classic "tree-type" model. Measurements are stored per vehicle.

Fig 1 Source Data Model -xml markup

One may note that technically all data are not independent (for example vehicle type is deduced from axle positions). We did keep redundant data when those seemed expensive to recomputed afterward and/or when those redundant data was produced by WIM hardware itself. One can note that this choice doesn't prevent to recomputed redundant information (e.g. if vehicle types are to be redefined and/or refined) and it could be used to benchmark WIM's firmwares.

Integration tools

One of the main works to do was to transfer database from an XML repository to SQL database. For that purposed we used Talend Open Studio software. This software is free and open source. It is an ETL tool that, through a graphical interface, generates independent Java programs that can be deployed on any architecture featuring a Java Virtual Machine (Windows, Linux, Unix…).

The tool has a large array of extensions, including most formats (cvs, xls, xml…) and DBMS (Oracle, MySQL, SQL-server, Sybase), which allowed us to quickly cope with various data sources.

Database

Model is mostly based on star schema, which is classic BI database architecture.

Fact table

This table includes one row per heavyweight vehicle. For each vehicle is recorded date, speed, total weight, and weight per axle for up to eight axles. Are also recorded all measurements in case there are several. This table is meant to harbor the bulk of raw numeric measurement data, at the lowest granularity level available. This is the main table with, currently, over thirty million lines.

Fig 3 Abbreviated Fact table model (axle data, up to eight axles)

Dimension tables

Highly disaggregated data, while retaining most information, is almost impossible to use. In order to give some meaningful information it has to be aggregated. Aggregation families will depend on purpose and organism, for example, depending on standard or organism considered there are several ways to classify heavy-weight vehicles, based on their axle distribution. Dimension tables' role is to list those aggregation rules inside a table. This allows every user to access information under an aggregation model that suits his needs.

In that regard we consider those tables mostly list rules and conventions (as opposed to fact table raw data).

There is a potential dimension table for each column of fact table. Each table is supposed to list all aggregation rules for the column. Whenever possible, classes are intricate.

Fig 4 Examples of dimension tables for intricate aggregation classes

Restitutions

The data model allows for several types of analysis among which: Aggregations by month, year, vehicle types... sophisticated aggressiveness evaluation (per vehicle or statistical) cross-dimensional analysis

The fact data is almost unaltered and exhaustive allows for sophisticated experimental studies and statistical treatments.

Data access/ visualization

Data is accessed through different interface, depending on user. Advanced users access interface through ODBC connection. This is the simplest method, it is easy implemented and powerful but can only cater for a limited part of audience as it requires SQL proficiency and exerts direct pressure on DB server workload. Other method aimed at common user visualizes data through a query/restitution web interface. At this point this GUI is still in the works: based on our experience we already have a pretty good idea about restitutions to implement but technology choice is not settled yet. Data restitutions are either through table, graphics or GIS systems.

Further development

Apart from obvious incremental improvements in engine and treatment there are many foreseeable opportunities regarding the system.

Integrating data inside model

Integration tools allow manipulating and processing complex and diverse data storages. So far we've been working on integrating the two most common formats available inside French WIM architecture but there is a strong potential for addressing more exotic data sources allowing for comparisons or cross studies between different systems at a national or an international data, for a reasonable cost.

Integrating model inside data

In the opposite corner to integrating data is making source data to be compatible with us, which means making data producers to adopt a unified data model. This is done by publicity and making resources available to partners.

Creating WIM data community

Which leads us to our final step: standardization is seldom a one-way road; this type of action is more of a community work: On one hand it's resources wasted that work by a given party can't be reused by others.

On the other hand one given party can't do the work for all other parties, at least without feedback. There is intrinsically, formal or not, a WIM community, comprising WIM producers, WIM system users, WIM data users… There are many patterns along which this community can organize itself.

Fragmented community where parties mostly ignore each other.

A particular party, generally a large commercial firm or public entity is able, by its size or influence, to lead alone making its private standards de-facto standards. Balanced community, possibly with one or several core members, able to push a general architecture for common good. Of course it is likely, particularly in a fragmented community, to have several clusters of various types existing at the same time. Balanced community is probably the best and most durable option but it requires enough political will. Question is whether WIM community is big enough, community commons are important enough, to sustain a vivid community life and make it up for the efforts associated with cooperation. Creating community is done by publicity, making resources available… and creating debate.

Examples of applications

Pavements

The data aggregating system can be used to evaluate the impacts of a heavy traffic (overall flow or individual vehicle truck) through the assessment of the aggressiveness in the context of studies on weight and dimensions law changes, monitoring of road asset by administrations, or studies on pavement deterioration mechanisms. Traffic data are converted into aggressiveness by applying a power law on axle loads, whose factors depend on type of structure and axle. The data system can also help to improve the pavement design method by characterizing accurately traffic aggressiveness.

Bridges

In this case also, the detailed data makes it possible for engineers to assess the damage of one particular traffic on one particular bridge, by using the concept of influence lines. Indeed, with these two elements, it is possible to assess the fatigue and the extreme effects to which the structure is submitted. For example, we had recently to assess the consequences of changes in the weights and dimensions allowed for the trucks on the residual capacity of the bridges. Then, fatigue has to be assessed for steel and composite bridges, extreme loads have to be studied especially in the case of reinforced or prestressed bridges.

Statistics of traffic: overloading, dimensions, …

These two databases have two advantages for this last application: the first advantage, which is linked with the first database, is that one user may know which information one WIM station for one precise country may provide. So for example, French WIM data provide lateral position of the vehicles in the lane, whereas Dutch provide the type of truck. The second advantage is that, with the second database which unifies all kind of formatting of WIM data, every data file may be used in the same manner. So statistics may be done easily by transferring the original data in the database and using the same treatment for all data afterwards.

Conclusion

In this paper, we presented two projects that have been launched and finished recently in France: the first one is the database FIWI, visible on internet, which makes a general description of the type of WIM stations and WIM data one may find all around the word. In this first project, the data providers are volunteers who want to advertise their data, and so share a small amount via this webpage. For more information, the webpage user may contact them and deal directly with them. FIWI looks for more providers, so if you want to participate you are welcome! The second project is a kind of tool which makes it possible to transfer all WIM data files in the same format. It is useful to apply the same procedures to all WIM files.

Fig 2

 2 Fig 2 Simple Talend integration project -MS-Excel to PostgreSQL


Frédéric Blanqui

Thérèse Hardin

Pierre Weis

On the implementation of construction functions for non-free concrete data types

Many algorithms use concrete data types with some additional invariants. The set of values satisfying the invariants is often a set of representatives for the equivalence classes of some equational theory. For instance, a sorted list is a particular representative wrt commutativity. Theories like associativity, neutral element, idempotence, etc. are also very common. Now, when one wants to combine various invariants, it may be difficult to find the suitable representatives and to efficiently implement the invariants. The preservation of invariants throughout the whole program is even more difficult and error prone. Classically, the programmer solves this problem using a combination of two techniques: the definition of appropriate construction functions for the representatives and the consistent usage of these functions ensured via compiler verifications. The common way of ensuring consistency is to use an abstract data type for the representatives; unfortunately, pattern matching on representatives is lost. A more appealing alternative is to define a concrete data type with private constructors so that both compiler verification and pattern matching on representatives are granted. In this paper, we detail the notion of private data type and study the existence of construction functions. We also describe a prototype, called Moca, that addresses the entire problem of defining concrete data types with invariants: it generates efficient construction functions for the combination of common invariants and builds representatives that belong to a concrete data type with private constructors.

Introduction

Many algorithms use data types with some additional invariants. Every function creating a new value from old ones must be defined so that the newly created value satisfy the invariants whenever the old ones so do.

One way to easily maintain invariants is to use abstract data types (ADT): the implementation of an ADT is hidden and construction and observation functions are provided. A value of an ADT can only be obtained by recursively using the construction functions. Hence, an invariant can be ensured by using appropriate construction functions. Unfortunately, abstract data types preclude pattern matching, a very useful feature of modern programming languages [START_REF] Doligez | The Objective Caml system release 3.09, Documentation and user's manual[END_REF][START_REF]Haskell 98 Language and Libraries, The revised report[END_REF][START_REF] Moreau | A pattern matching compiler for multiple target languages[END_REF][START_REF] Moreau | Tom Manual version 2.3[END_REF]. There have been various attempts to combine both features in some way.

In [START_REF] Wadler | Views: a way for pattern matching to cohabit with data abstraction[END_REF], P. Wadler proposed the mechanisms of views. A view on an ADT α is given by providing a concrete data type (CDT) γ and two functions in : α → γ and out : γ → α such that in • out = id γ and out • in = id α . Then, a function on α can be defined by matching on γ (by implicitly using in) and the values of type γ obtained by matching can be injected back into α (by implicitly using out). However, by leaving the applications of in and out implicit, we can easily get inconsistencies whenever in and out are not inverses of each other. Since it may be difficult to satisfy this condition (consider for instance the translations between cartesian and polar coordinates), these views have never been implemented. Following the suggestion of W. Burton and R. Cameron to use the in function only [START_REF] Burton | Pattern matching with abstract data types[END_REF], some propositions have been made for various programming languages but none has been implemented yet [START_REF] Burton | Views: An extension to Haskell pattern matching[END_REF][START_REF] Okasaki | Views for standard ML[END_REF].

In [START_REF] Burton | Pattern matching with abstract data types[END_REF], W. Burton and R. Cameron proposed another very interesting idea which seems to have attracted very little attention. An ADT must provide construction and observation functions. When an ADT is implemented by a CDT, they propose to also export the constructors of the CDT but only for using them as patterns in pattern matching clauses. Hence, the constructors of the underlying CDT can be used for pattern matching but not for building values: only the construction functions can be used for that purpose. Therefore, one can both ensure some invariants and offer pattern matching. These types have been introduced in OCaml by the third author [START_REF] Weis | Private constructors in OCaml[END_REF] under the name of concrete data type with private constructors, or private data type (PDT) for short. Now, many invariants on concrete data types can be related to some equational theory. Take for instance the type of list with the constructors [] and ::. Given some elements v 1 ..v n , the sorted list which elements are v 1 ..v n is a particular representative of the equivalence class of v 1 ::..::v n ::[] modulo the equation x::y::l=y::x::l. Requiring that, in addition, the list does not contain the same element twice is a particular representative modulo the equation x::x::l=x::l.

Consider now the type of join lists with the constructors empty, singleton and append, for which concatenation is of constant complexity. Sorting corresponds to associativity and commutativity of append. Requiring that no argument of append is empty corresponds to neutrality of empty wrt append. We have a structure of commutative monoid.

More generally, given some equational theory on a concrete data type, one may wonder whether there exists a representative for each equivalence class and, if so, whether a representative of C(t 1 . . . t n ) can be efficiently computed knowing that t 1 . . . t n are themselves representatives.

In [START_REF] Thompson | Laws in Miranda[END_REF][START_REF] Thompson | Lawful functions and program verification in Miranda[END_REF], S. Thompson describes a mechanism introduced in the Miranda functional programming language for implementing such non-free concrete data types without precluding pattern matching. The idea is to provide conditional rewrite rules, called laws, that are implicitly applied as long as possible on every newly created value. This can also be achieved by using a PDT which construction functions (primed constructors in [START_REF] Thompson | Laws in Miranda[END_REF]) apply as long as possible each of the laws. Then, S. Thompson studies how to prove the correctness of functions defined by pattern matching on such lawful types. However, few hints are given on how to check whether the laws indeed implement the invariants one has in mind. For this reason and because reasoning on lawful types is difficult, the law mechanism was removed from Miranda.

In this paper, we propose to specify the invariants by unoriented equations (instead of rules). We will call such a type a relational data type (RDT). Sections 2 and 3 introduce private and relational data types. Then, we study when an RDT can be implemented by a PDT, that is, when there exist construction functions computing some representative for each equivalence class. Section 4 provides some general existence theorem based on rewriting theory. But rewriting may be inefficient. Section 5 provides, for some common equational theories, construction functions more efficient than the ones based on rewriting. Section 6 presents Moca, an extension of OCaml with relational data types whose construction functions are automatically generated. Finally, Section 7 discusses some possible extensions.

Concrete data types with private constructors

We first recall the definition of a first-order term algebra. It will be useful for defining the values of concrete and private data types.

Definition 1 (First-order term algebra) A sorted term algebra definition is a triplet A = (S, C, Σ) where S is a non-empty set of sorts, C is a non-empty set of constructor symbols and Σ : C → S + is a signature mapping a non-empty sequence of sorts to every constructor symbol. We write C : σ 1 . . . σ n σ n+1 ∈ Σ to denote the fact that Σ(C) = σ 1 . . . σ n σ n+1 . Let X = (X σ ) σ∈S be a family of pairwise disjoint sets of variables. The sets T σ (A, X ) of terms of sort σ are inductively defined as follows:

-If x ∈ X σ , then x ∈ T σ (A, X ).

-If C : σ 1 . . . σ n+1 ∈ Σ and t i ∈ T σi (A, X ), then C(t 1 , . . . , t n ) ∈ T σn+1 (A, X ). Let T σ (A) be the set of terms of sort σ containing no variable.

In the following, we assume given a set S 0 of primitive types like int, string, . . . and a set C 0 of primitive constants 0, 1, "foo", . . . Let Σ 0 be the corresponding signature (Σ 0 (0) = int, . . . ).

In this paper, we call concrete data type (CDT) an inductive type à la ML defined by a set of constructors. More formally: Definition 2 (Concrete data type) A concrete data type definition is a triplet Γ = (γ, C, Σ) where γ is a sort, C is a non-empty set of constructor symbols and

Σ : C → (S 0 ∪ {γ}) + is a signature such that, for all C ∈ C, Σ(C) = σ 1 ..σ n γ. The set V al(γ) of values of type γ is the set of terms T γ (A Γ ) where A Γ = (S 0 ∪ {γ}, C 0 ∪ C, Σ 0 ∪ Σ).
This definition of CDTs corresponds to a small but very useful subset of all the possible types definable in ML-like programming languages. For the purpose of this paper, it is not necessary to use a more complex definition.

Example 1

The following type4 cexp is a CDT definition with two constant constructors of sort cexp and a binary operator of sort cexp cexp cexp.

type cexp = Zero | One | Opp of cexp | Plus of cexp * cexp
Now, a private data type definition is like a CDT definition together with construction functions as in abstract data types. Constructors can be used as patterns as in concrete data types but they cannot be used for value creation (except in the definition of construction functions). For building values, one must use construction functions as in abstract data types. Formally:

Definition 3 (Private data type) A private data type definition is a pair Π = (Γ, F ) where Γ = (π, C, Σ) is a CDT definition and F is a family of con- struction functions (f C ) C∈C such that, for all C : σ 1 ..σ n π ∈ Σ, f C : T σ1 (A Γ ) × . . . × T σn (A Γ ) → T π (A Γ ). Let V al(π)
be the set of the values of type π, that is, the set of terms that one can build by using the construction functions only. The function f :

T π (A Γ ) → T π (A Γ ) such that, for all C : σ 1 ..σ n π ∈ Σ and t i ∈ T σi (A Γ ), f (C(t 1 ..t n )) = f C (f (t 1 )..f (t n )), is called the normalization func- tion associated to F .
This is quite immediate to see that:

Lemma 1. V al(π) is the image of f .
PDTs have been implemented in OCaml by the third author [START_REF] Weis | Private constructors in OCaml[END_REF]. Extending a programming language with PDTs is not very difficult: one only needs to modify the compiler to parse the PDT definitions and check that the conditions on the use of constructors are fulfilled.

Note that construction functions have no constraint in general: the full power of the underlying programming language is available to define them.

It should also be noted that, because the set of values of type π is a subset of the set of values of the underlying CDT γ, a function on π defined by pattern matching may be a total function even though it is not defined on all the possible cases of γ. Defining a function with patterns that match no value of type π does not harm since the corresponding code will never be run. It however reveals that the developer is not aware of the distinction between the values of the PDT and those of the underlying CDT, and thus can be considered as a programming error. To avoid this kind of errors, it is important that a PDT comes with a clear identification of its set of possible values. To go one step further, one could provide a tool for checking the completeness and usefulness of patterns that takes into account the invariants, when it is possible. We leave this for future work. This type exp is indeed a PDT built upon the CDT cexp. Prompted by the keyword private, the OCaml compiler forbids the use of exp constructors (outside the module my exp.ml containing the definition of exp) except in patterns. If Zero is supposed to be neutral by the writer of my exp.ml, then he/she will provide construction functions as follows:

Relational data types

We mentioned in the introduction that, often, the invariants upon concrete data types are such that the set of values satisfying them is indeed a set of representatives for the equivalence classes of some equational theory. We therefore propose to specify invariants by a set of unoriented equations and study to which extent such a specification can be realized with an abstract or private data type. In case of a private data type however, it is important to be able to describe the set of possible values. Definition 4 (Relational data type) A relational data type (RDT) definition is a pair (Γ, E) where Γ = (π, C, Σ) is a CDT definition and E is a finite set of equations on T π (A Γ , X ). Let = E be the smallest congruence relation containing E. Such an RDT is implementable by a PDT (Γ, F ) if the family of construction functions F = (f C ) C∈C is valid wrt E:

(Correctness) For all C : σ 1 ..σ n π and v i ∈ V al(σ i ), f C (v 1 ..v n ) = E C(v 1 ..v n ). (Completeness) For all C : σ 1 ..σ n σ, v i ∈ V al(σ i ), D : τ 1 ..τ p σ ∈ Σ and w i ∈ V al(τ i ), f C (v 1 ..v n ) = f D (w 1 ..w p ) whenever C(v 1 ..v n ) = E D(w 1 ..w p ).
We are going to see that the existence of a valid family of construction functions is equivalent to the existence of a valid normalization function:

Definition 5 (Valid normalization function) A map f : T π (A Γ ) → T π (A Γ ) is a valid normalization function for an RDT (Γ, E) with Γ = (π, C, Σ) if: (Correctness) For all t ∈ T π (A Γ ), f (t) = E t. (Completeness) For all t, u ∈ T π (A Γ ), f (t) = f (u) whenever t = E u.
Note that a valid normalization function is idempotent (f • f = f ) and provides a decision procedure for = E (the boolean function λxy.f (x) = f (y)).

Theorem 6

The normalization function associated to a valid family is a valid normalization function.

Proof.

-Correctness. We proceed by induction on the size of t ∈ T π . We have C :

σ 1 ..σ n π ∈ Σ and t i such that t = C(t 1 ..t n ). By definition, f (t) = f C (f (t 1 ).. f (t n ))
. By induction hypothesis, f (t i ) = E t i . Since the family is valid and

f (t 1 )..f (t n ) are values, f C (f (t 1 )..f (t n )) = E C(f (t 1 )..f (t n )). Thus, f (t) = E t. -Completeness. Let t, u ∈ T π such that t = E u. We have t = C(t 1 ..t n ) and u = D(u 1 ..u p ). By definition, f (t) = f C (f (t 1 )..f (t n )) and f (u) = f D (f (u 1 )..f (u p )). By correctness, f (t i ) = E t i and f (u j ) = E u j . Hence, C(f (t 1 )..f (t n )) = E D(f (u 1 )..f (u p ))
. Since the family is valid and

f (t 1 )..f (t n ) are values, f C (f (t 1 ) ..f (t n )) = f D (f (t 1 )..f (t n )). Thus, f (t) = f (u).
Conversely, given f : T π (A Γ ) → T π (A Γ ), one can easily define a family of construction functions that is valid whenever f is a valid normalization function.

Definition 7 (Associated family of constr. functions) Given a CDT Γ = (π, C, Σ) and a function f : T π (A Γ ) → T π (A Γ ), the family of construction functions associated to f is the family (f C ) C∈C such that, for all C :

σ 1 ..σ n π ∈ Σ and t i ∈ T σ1 (A Γ ), f C (t 1 , . . . , t n ) = f (C(t 1 , . . . , t n )).

On the existence of construction functions

In this section, we provide a general theorem for the existence of valid families of construction functions based on rewriting theory. We recall the notions of rewriting and completion. The interested reader may find more details in [START_REF] Dershowitz | Rewrite systems[END_REF].

Standard rewriting. A rewrite rule is an ordered pair of terms (l, r) written l → r. A rule is left-linear if no variable occurs twice in its left hand side l.

As usual, the set Pos(t) of positions in t is defined as a set of words on positive integers. Given p ∈ Pos(t), let t| p be the subterm of t at position p and t[u] p be the term t with t| p replaced by u.

Given a finite set R of rewrite rules, the rewriting relation is defined as follows: t → R u iff there are p ∈ Pos(t), l → r ∈ R and a substitution θ such that t| p = lθ and u = t[rθ] p . A term t is an R-normal form if there is no u such that t → R u. Let = R be the symmetric, reflexive and transitive closure of → R .

A reduction ordering ≻ is a well-founded ordering (there is no infinitely decreasing sequence t 0 ≻ t 1 ≻ . . .) stable by context (C(..t..) ≻ C(..u..) whenever t ≻ u) and substitution (tθ ≻ uθ whenever t ≻ u). If R is included in a reduction ordering, then → R is well-founded (terminating, strongly normalizing).

We say that → R is confluent if, for all terms t, u, v such that u ← * R t → * R v, there exists a term w such that u → * R w ← * R v. This means that the relation

← * R → * R is included in the relation → * R ← * R (

composition of relations is written by juxtaposition).

If → R is confluent, then every term has at most one normal form. If → R is well-founded, then every term has at least one normal form. Therefore, if → R is confluent and terminating, then every term has a unique normal form. Standard completion. Given a finite set E of equations and a reduction ordering ≻, the standard Knuth-Bendix completion procedure [START_REF] Bendix | Computational problems in abstract algebra, chapter Simple word problems in universal algebra[END_REF] tries to find a finite set R of rewrite rules such that:

• R is included in ≻, • → R is confluent, • R and E have same theory: = E = = R .
Note that completion may fail or not terminate but, in case of successful termination, R-normalization provides a decision procedure for = E since t = E u iff the R-normal forms of t and u are syntactically equal.

However, since permutation theories like commutativity or associativity and commutativity together (written AC for short) are included in no reduction ordering, dealing with them requires to consider rewriting with pattern matching modulo these theories and completion modulo these theories. In this paper, we restrict our attention to AC. Definition 9 (Associative-commutative equations) Let Com be the set of commutative constructors, i.e. the set of constructors C such that E contains an equation of the form C(x, y) = C(y, x). Then, let E AC be the subset of E made of the commutativity and associativity equations for the commutative constructors, = AC be the smallest congruence relation containing E AC and E ¬AC = E \ E AC .

Rewriting modulo AC. Given a set R of rewrite rules, rewriting with pattern matching modulo AC is defined as follows: t → R,AC u iff there are p ∈ Pos(t), l → r ∈ R and a substitution θ such that t| p = AC lθ and u = t[rθ] p . A reduction ordering ≻ is AC-compatible if, for all terms t, t ′ , u, u ′ such that t = AC t ′ and u

= AC u ′ , t ′ ≻ u ′ iff t ≻ u. The relation → R,AC is confluent modulo AC if (← * R,AC = AC → * R,AC ) ⊆ (→ * R,AC = AC ← * R,AC
). Completion modulo AC. Given a finite set E of equations and an ACcompatible reduction ordering ≻, completion modulo AC [START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF] tries to find a finite set R of rules such that:

• R is included in ≻, • → R,AC is confluent modulo AC, • E and R ∪ E AC have same theory: = E = = R∪EAC .
Definition 10 A theory E has a complete presentation if there is an AC-compatible reduction ordering for which the AC-completion of E ¬AC successfully terminates.

Many interesting systems have a complete presentation: (commutative) monoids, (abelian) groups, rings, etc. See [START_REF] Hullot | Compilation de formes canoniques dans les thories quationnelles[END_REF][START_REF] Chenadec | Canonical forms in finitely presented algebras[END_REF] for a catalog. Moreover, there are automated tools implementing completion modulo AC. See for instance [START_REF] Contejean | CiME version 2.02. LRI[END_REF][START_REF] Gaillourdet | The new Waldmeister loop at work[END_REF].

A term may have distinct R, AC-normal forms but, by confluence modulo AC, all normal forms are AC-equivalent and one can easily define a notion of normal form for AC-equivalent terms [START_REF] Hullot | Compilation de formes canoniques dans les thories quationnelles[END_REF]:

Definition 11 (AC-normal form) Given an associative and commutative constructor C, C-left-combs (resp. C-right-combs) and their leaves are inductively defined as follows:

-If t is not headed by C, then t is both a C-left-comb and a C-right-comb. The leaves of t is the one-element list

leaves(t) = [t]. -If t is not headed by C and u is a C-right-comb, then C(t, u) is a C-right-comb.
The leaves of C(t, u) is the list t :: leaves(u).

-If t is not headed by C and u is a C-left-comb, then C(u, t) is a C-left-comb.
The leaves of C(u, t) is the list leaves(u)@[t], where @ is the concatenation.

Let orient be a function associating a kind of combs (left or right) to every ACconstructor. Let ≤ be a total ordering on terms. Then, a term t is in AC-normal form wrt orient and ≤ if:

-Every subterm of t headed by an AC-constructor C is an orient (C)-comb whose leaves are in increasing order wrt ≤. -For every subterm of t of the form C(u, v) with C commutative but nonassociative, we have u ≤ v.

As it is well-known, one can put any term in AC-normal form:

Theorem 12 Whatever the function orient and the ordering ≤ are, every term t has an AC-normal form t ↓ AC wrt orient and ≤, and t = AC t ↓ AC .

Proof. Let A be the set of rules obtained by choosing an orientation for the associativity equations of E AC according to orient :

-If orient (C) is "left", then take C(x, C(y, z)) → C(C(x, y), z). -If orient (C) is "right", then take C(C(x, y), z) → C(x, C(y, z)).
→ A is a confluent and terminating relation putting every subterm headed by an AC-constructor into a comb form according to orient . Let comb be a function computing the A-normal form of a term. Let now sort be a function permuting the leaves of combs and the arguments of commutative but non-associative constructors to put them in increasing order wrt ≤. Then, the function sort • comb computes the AC-normal form of any term and sort (comb(t)) = AC t.

This naturally provides a decision procedure for AC-equivalence: the function λxy.sort (comb(x)) = sort (comb(y)). It follows that R, AC-normalization together with AC-normalization provides a valid normalization function, hence the existence of a valid family of construction functions:

Theorem 13 If E has a complete presentation, then there exists a valid family of construction functions.

Proof.

Assume that E has a complete presentation R. We define the computation of normal forms as it is generally implemented in rewriting tools. Let step be a function making an R, AC-rewrite step if there is one, or failing if the term is in normal form. Let norm be the function applying step until a normal form is reached. Since R is a complete presentation of E, by definition of the completion procedure, sort •comb •norm is a valid normalization function. Thus, by Theorem 8, the associated family of construction functions is valid.

The construction functions described in the proof are not very efficient since they are based on rewriting with pattern matching modulo AC, which is NPcomplete [START_REF] Benanav | Complexity of matching problems[END_REF], and do not take advantage of the fact that, by definition of PDTs, they are only applied to terms already in normal form. We can therefore wonder whether they can be defined in a more efficient way for some common equational theories like the ones of Figure 1.

+ z = x + (y + z) commutativity Com(C) C(x, y) = C(y, x) x + y = y + x neutrality N eu(C, E) C(x, E) = x x + 0 = x inverse Inv(C, I, E) C(x, I(x)) = E x + (-x) = 0 idempotence Idem(C) C(x, x) = x x ∧ x = x nilpotence N il(C, A) C(x, x) = A x ⊕ x = ⊥ (exclusive or)
Rewriting provides also a way to check the validity of construction functions:

Theorem 14 If E has a complete presentation R and F = (f C ) C∈C is a family such that, for all C : σ 1 ..σ n π ∈ Σ and terms

v i ∈ V al(σ i ), f C (v 1 ..v n ) is an R, AC-normal form of C(v 1 ..v n ) in AC-normal form, then F is valid. Proof. -Correctness. Let C : σ 1 ..σ n π ∈ Σ and v i ∈ V al(σ i ). Since f C (v 1 ..v n ) is an R, AC-normal form of C(v 1 ..v n ), we clearly have f C (v 1 ..v n ) = E C(v 1 ..v n ). -Completeness. Let C : σ 1 ..σ n π ∈ Σ, v i ∈ V al F (σ i ), D : τ 1 ..τ p π ∈ Σ, and w i ∈ V al F (τ i ) such that C(v 1 ..v n ) = E D(w 1 ..w p ). Since R is a complete pre- sentation of E, norm(C(v 1 ..v n )) = AC norm(D(w 1 ..w p )). Thus, f C (v 1 ..v n ) = f D (w 1 ..w p ).
It follows that rewriting provides a natural way to explain what are the possible values of an RDT: values are AC-normal forms matching no left hand side of a rule of R.

The construction functions of type 2 can be easily extended to deal with ring or lattice structures (distributivity and absorbance equations).

More general results can be expected by using or extending results on the modularity of completeness for the combination of rewrite systems. The completeness of hierarchical combinations of non-AC-rewrite systems is studied in [START_REF] Rao | Completeness of hierarchical combinations of term rewriting systems[END_REF]. Note however that the modularity of confluence for AC-rewrite systems has been formally established only recently in [START_REF] Jouannaud | Modular church-rosser modulo[END_REF].

Note that the construction function definitions of type 1 or 2 provide the same results with call-by-value, call-by-name or lazy evaluation strategy.

The detailed study of the complexity of theses definitions (compared to ACrewriting) is left for future work.

The Moca system

We now describe the Moca prototype, a program generator that implements an extension of OCaml with RDTs. Moca parses a special ".mlm" file containing the RDT definition and produces a regular OCaml module (interface and implementation) which provides the construction functions for the RDT. Moca provides a set of keywords for specifying the equations described in Figure 1.

For instance, the RDT exp can be defined in Moca as follows: Moca also features user's arbitrary rules with the construction: rule pattern -> pattern. These rules add extra clauses in the definitions of construction functions generated by Moca: the LHS pattern is copied verbatim as the pattern of a clause which returns the RHS pattern considered as an expression where constructors are replaced by calls to the corresponding construction functions. Of course, in the presence of such arbitrary rules, we cannot guarantee the termination or completeness of the generated code. This construction is thus provided for expert users that can prove termination and completeness of the corresponding set of rules. That way, the programmer can describe complex RDTs, even those which cannot be described with the set of predefined equational invariants.

Moca also accepts polymorphic RDTs and RDTs mutually defined with record types (but equations between record fields are not yet available).

The equations of Figure 1 also support n-ary constructor, implemented as unary constructors of type t list -> t. In this case, Plus gets a single argument of type exp list. Normal forms are modified accordingly and use lists instead of combs. For instance, associative normal forms get flat lists of arguments: in a Plus(l) expression, no element of l is a Plus(l ′ ) expression. The corresponding data structure is widely used in rewriting.

Finally, Moca offers an important additional feature: it can generate construction functions that provide maximally shared representatives. To fire maximal sharing, just add the --sharing option when compiling the ".mlm" file. In this case, the generated type is slightly modified, since every functional constructor gets an extra argument to keep the hash code of the term. Maximally shared representatives have a lot of good properties: not only data size is minimal and user's memoized functions can be light speed, but comparison between representatives is turned from a complex recursive term comparison to a pointer comparisona single machine instruction. Moca heavily uses this property for the generation of construction functions: when dealing with non-linear equations, the maximal sharing property allows Moca to replace term equality by pointer equality.

Future work

We plan to integrate Moca to the development environment Focal [START_REF] Rioboo | FoCal Reference Manual, version 0.3.1[END_REF]. Focal units contain declarations and definitions of functions, statements and proofs as first-class citizens. Their compilation produces both a file checkable by the theorem prover Coq [START_REF]The Coq Proof Assistant Reference Manual[END_REF] and a OCaml source code. Proofs are done either within Coq or via the automatic theorem prover Zenon [START_REF] Doligez | version 0.4.1[END_REF], which issues a Coq file when it successes. Every Focal unit has a special field, giving the type of the data manipulated in this unit. Thus, it would be very interesting to do a full integration of private/relational data types in Focal, the proof of correctness of construction functions being done with Zenon or Coq and then recorded as a theorem to be used for further proofs. This should be completed by the integration of a tool on rewriting and equational theories able to complete equational presentations, to generate and prove the corresponding lemmas and to show some termination properties. Some experiments already done within Focal on coupling CiME [START_REF] Contejean | CiME version 2.02. LRI[END_REF] and Zenon give a serious hope of success.

Acknowledgments. The authors thank Claude Kirchner for his comments on a previous version of the paper.

Example 2

 2 Let us now start our running example with the type exp describing operations on arithmetic expressions. type exp = private Zero | One | Opp of exp | Plus of exp * exp

  let rec zero = Zero and one = One and opp x = Opp x and plus = function | (Zero,y) -> y | (y,Zero) -> y | (x,y) -> Plus(x,y)

Theorem 8 Example 3

 83 The family of construction functions associated to a valid normalization function is valid. We can choose cexp as the underlying CDT and E = { Plus x Zero = x} to define a RDT implementable by the PDT exp, with the valid family of construction functions zero, one, opp, plus.

Fig. 1 .

 1 Fig. 1. Some common equations on binary constructorsName Abbrev Definition Example associativity Assoc(C) C(C(x, y), z) = C(x, C(y, z)) (x + y) + z = x + (y + z) commutativity Com(C) C(x, y) = C(y, x) x + y = y + x neutrality N eu(C, E) C(x, E) = x x + 0 = x inverse Inv(C, I, E) C(x, I(x)) = E x + (-x) = 0 idempotence Idem(C) C(x, x) = x x ∧ x = x nilpotence N il(C, A) C(x, x) = A x ⊕ x = ⊥ (exclusive or)

  type exp = private Zero | One | Opp of exp | Plus of exp * exp begin associative commutative neutral(Zero) opposite(Opp) end

Examples are written with OCaml[START_REF] Doligez | The Objective Caml system release 3.09, Documentation and user's manual[END_REF], they can be readily translated in any programming language offering pattern-matching with textual priority, as Haskell, SML, etc.

When there is no commutative symbol, construction functions can be easily implemented by simulating innermost rewriting as follows:

Definition 15 (Linearization) Let VPos(t) be the set of positions p ∈ Pos(t) such that t| p is a variable x ∈ X . Let ρ : VPos(t) → X be an injective mapping and lin(t) be the term obtained by replacing in t every subterm at position p ∈ VPos(t) by ρ(p). Let now Eq(t) be the conjunction of true and of the equations ρ(p) = ρ(q) such that t| p = t| q and p, q ∈ VPos(t).

Definition 16 Given a set R of rewrite rules, let F (R) be the family of construction functions (f C ) C∈C defined as follows:

• For every rule l → r ∈ R with l = C(l 1 , . . . , l n ), add to the definition of f C the clause lin(l 1 ), . . . , lin(l n ) when Eq(l) -> lin(r), where t is the term obtained by replacing in t every occurrence of a constructor C by a call to its construction function f C .

• Terminate the definition of f C by the default clause x -> C(x).

Theorem 17

Assume that E AC = ∅ and E has a complete presentation R. Then, F (R) is valid wrt E (whatever the order of the non-default clauses is).

We now consider the case of commutative symbols. We are going to describe a modular way of defining the construction functions by pursuing our running example, with the type exp. Assume that Plus is declared to be associative and commutative only. The construction functions can then be defined as follows: Assume now that Plus is declared to have Opp as inverse. Then, the completion modulo AC of { Plus(Zero, x) = x, Plus(Opp(x), x) = Zero} gives the following well known rules for abelian groups [START_REF] Hullot | Compilation de formes canoniques dans les thories quationnelles[END_REF]:

The rules for Opp are easily translated as follows:

The third rule of abelian groups is called an extension of the second one since it is obtained by first adding the context P lus([], y) on both sides of this second rule,then normalizing the right hand side. Take now two terms x and y in normal form and assume that (x, y) matches none of the three clauses previously defining plus, that is, x and y are distinct from Zero, and x is not of the form Plus(x 1 , x 2 ). To get the normal form of Plus(x, y), we need to check that x and the normal form of its opposite Opp(x) do not occur in y. The last clause defining plus needs therefore to be modified as follows: Forgetting about Zero and Opp, suppose now that Plus is declared associative, commutative and idempotent. The function plus is kept but the insert function is modified as follows:

and insert_plus x = function | Plus(y,_) as u when x = y -> u | Plus(y,_) as u when x < y -> Plus(x,u) | Plus(y,t) -> Plus (y,insert_plus x t) | u when x > u -> Plus(u,x) | u when x = u -> u | u -> Plus(x,u)

Nilpotence can be dealt with in a similar way. In conclusion, for various combinations of the equations of Figure 1, we can define in a nice modular way construction functions that are more efficient than the ones based on rewriting modulo AC. We summarize this as follows:

Let us give schemes for construction functions for theories of type 2. A clause is generated only if the conditions Neu(C,E), Inv(C,I,E), etc. are satisfied. These conditions are not part of the generated code. Proof. Assume that E = n i=1 E i where E 1 , . . . , E n are pairwise disjoint theories of type 1 or 2. Whatever the type of E i is, we saw that E i has a complete presentation R i . Therefore, since E 1 , . . . , E n share no symbol, by definition of completion, the AC-completion of E successfully terminates with R = n i=1 R i . Thus, → R,AC is terminating and AC-confluent. Since F = (f C ) C∈C computes R, AC-normal forms in AC-normal forms, by Theorem 14, F is valid.