Dariusz Biernacki

Sergueï Lenglet

Environmental Bisimulations for Delimited-Control Operators

We present a theory of environmental bisimilarity for the delimited-control operators shift and reset. We consider two different notions of contextual equivalence: one that does not require the presence of a top-level control delimiter when executing tested terms, and another one, fully compatible with the original CPS semantics of shift and reset, that does. For each of them, we develop sound and complete environmental bisimilarities, and we discuss up-to techniques.

Introduction

Control operators for delimited continuations [START_REF] Danvy | Abstracting control[END_REF][START_REF] Felleisen | The theory and practice of first-class prompts[END_REF] provide elegant means for expressing advanced control mechanisms [START_REF] Danvy | Abstracting control[END_REF][START_REF] Hieb | [END_REF]. Moreover, they play a fundamental role in the semantics of computational effects [START_REF] Filinski | Representing monads[END_REF], normalization by evaluation [START_REF] Balat | Extensional normalisation and typedirected partial evaluation for typed lambda calculus with sums[END_REF] and as a crucial refinement of abortive control operators such as callcc [START_REF] Felleisen | The theory and practice of first-class prompts[END_REF][START_REF] Sitaram | Reasoning with continuations II: Full abstraction for models of control[END_REF]. Of special interest are the control operators shift and reset [START_REF] Danvy | Abstracting control[END_REF] due to their origins in continuation-passing style (CPS) and their connection with computational monads -as demonstrated by Filinski [START_REF] Filinski | Representing monads[END_REF], shift and reset can express in direct style arbitrary computational effects, such as mutable state, exceptions, etc. Operationally, the control delimiter reset delimits the current continuation and the control operator shift abstracts the current delimited continuation as a first class value that when resumed is composed with the thencurrent continuation.

Because of the complex nature of control effects, it can be difficult to determine if two programs that use shift and reset are equivalent (i.e., behave in the same way) or not. Contextual equivalence [START_REF] Morris | Lambda Calculus Models of Programming Languages[END_REF] is widely considered as the most natural equivalence on terms in languages similar to the λ-calculus. Roughly, two terms are contextually equivalent if we cannot tell them apart when they are executed within any context. The latter quantification over contexts makes this relation hard to use in practice, so we usually look for simpler characterizations of contextual equivalence, such as coinductively defined bisimilarities.

In our previous work, we defined applicative [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF] and normal form [START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF] bisimilarities for shift and reset. Applicative bisimilarity characterizes contextual equivalence, but still quantifies over some contexts to relate terms (e.g., λ-abstractions are applied to the same arbitrary argument). As a result, some equivalences remain quite difficult to prove. In contrast, normal form bisimilarity does not contain any quantification over contexts or arguments in its definition: the tested terms are reduced to normal forms, which are then decomposed in bisimilar subterms. Consequently, proofs of equivalence are usually simpler than with applicative bisimilarity, and they can be simplified even further with up-to techniques. However, normal form bisimilarity is not complete, i.e., there exist contextually equivalent terms which are not normal form bisimilar.

Environmental bisimilarity [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF] is a different kind of behavioral equivalence which in terms of strength and practicality can be situated in between applicative and normal form bisimilarities. It has originally been proposed in [START_REF] Sumii | A bisimulation for dynamic sealing[END_REF] and has been since defined in various higher-order languages (see, e.g., [START_REF] Sato | The higher-order, call-by-value applied Pi-calculus[END_REF][START_REF] Sumii | A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation[END_REF][START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF]). Like applicative bisimilarity, it uses some particular contexts to test terms, except that the testing contexts are built from an environment, which represents the knowledge built so far by an outside observer. Environmental bisimilarity usually characterizes contextual equivalence, but is harder to establish than applicative bisimilarity. Nonetheless, like with normal form bisimilarity, one can define powerful up-to techniques [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF] to simplify the equivalence proofs. Besides, the authors of [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF] argue that the additional complexity of environmental bisimilarity is necessary to handle more realistic features, like local state or exceptions.

In the quest for a powerful enough (i.e., as discriminative as contextual equivalence) yet easy-to-use equivalence for delimited control, we study in this paper the environmental theory of a calculus with shift and reset. More precisely, we consider two semantics for shift and reset: the original one [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF], where terms are executed within a top-level reset, and a more relaxed semantics where this requirement is lifted. The latter is commonly used in implementations of shift and reset [START_REF] Dybvig | A monadic framework for delimited continuations[END_REF][START_REF] Filinski | Representing monads[END_REF] as well as in some studies of these operators [START_REF] Asai | Polymorphic delimited continuations[END_REF][START_REF] Kameyama | Axioms for control operators in the CPS hierarchy[END_REF], including our previous work [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF][START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF]. So far, the behavioral theory of shift and reset with the original semantics has not been studied. Firstly, we define environmental bisimilarity for the relaxed semantics and study its properties; especially we discuss the problems raised by delimited control for the definition of bisimulation up to context, one of the most powerful up-to techniques. Secondly, we propose the first behavioral theory for the original semantics, and we pinpoint the differences between the equivalences of the two semantics. In particular, we show that the environmental bisimilarity for the original semantics is complete w.r.t. the axiomatization of shift and reset of [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF], which is not the case for the relaxed semantics, as already proved in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF] for applicative bisimilarity.

In summary, we make the following contributions in this paper.

-We show that environmental bisimilarity can be defined for a calculus with delimited control, for which we consider two different semantics. In each case, the defined bisimilarity equals contextual equivalence. -For the relaxed semantics, we explain how to handle stuck terms, i.e., terms where a capture cannot go through because of the lack of an outermost reset. -We discuss the limits of the usual up-to techniques in the case of delimited control. -For the original semantics, we define a contextual equivalence, and a corresponding environmental bisimilarity. Proving soundness of the bisimilar-ity w.r.t. contextual equivalence requires significant changes from the usual soundness proof scheme. We discuss how environmental bisimilarity is easier to adapt than applicative bisimilarity. -We give examples illustrating the differences between the two semantics.

The rest of the paper is organized as follows: in Section 2, we present the calculus λ S used in this paper, and recall some results, including the axiomatization of [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]. We develop an environmental theory for the relaxed semantics in Section 3, and for the original semantics in Section 4. We conclude in Section 5. An extended version of this article [START_REF] Biernacki | Environmental bisimulations for delimited-control operators[END_REF] contains most of the omitted proofs.

2 The Calculus λ S

Syntax

The language λ S extends the call-by-value λ-calculus with the delimited-control operators shift and reset [START_REF] Danvy | Abstracting control[END_REF]. We assume we have a set of term variables, ranged over by x, y, z, and k. We use k for term variables representing a continuation (e.g., when bound with a shift), while x, y, and z stand for any values; we believe such distinction helps to understand examples and reduction rules. The syntax of terms is given by the following grammar:

Terms: t ::= x | λx.t | t t | Sk.t | t
Values, ranged over by v, are terms of the form λx.t. The operator shift (Sk.t) is a capture operator, the extent of which is determined by the delimiter reset ( • ). A λ-abstraction λx.t binds x in t and a shift construct Sk.t binds k in t; terms are equated up to α-conversion of their bound variables. The set of free variables of t is written fv(t); a term t is closed if fv(t) = ∅.

We distinguish several kinds of contexts, represented outside-in, as follows:

Pure contexts:

E ::= | v E | E t Evaluation contexts: F ::= | v F | F t | F Contexts: C ::= | λx.C | t C | C t | Sk.C | C
Regular contexts are ranged over by C . The pure evaluation contexts ); the free variables of t may be captured in the process. We extend the notion of free variables to contexts (with fv( ) = ∅), and we say a context C (respectively

E , F ) is closed if fv(C ) = ∅ (respectively fv(E ) = ∅, fv(F ) = ∅).

Reduction Semantics

The call-by-value reduction semantics of λ S is defined as follows, where t{v/x} is the usual capture-avoiding substitution of v for x in t:

(β v ) F [(λx.t) v] → v F [t{v/x}] (shift) F [ E [Sk.t] ] → v F [ t{λx. E [x] /k} ] with x / ∈ fv(E ) (reset) F [ v ] → v F [v]
The term (λx. Finally, we write → * v for the transitive and reflexive closure of → v , and we define the evaluation relation of λ S as follows.

Definition 3. We write t ⇓ v t ′ if t → * v t ′ and t ′ → v .
The result of the evaluation of a closed term, if it exists, is a normal form. If a term t admits an infinite reduction sequence, we say it diverges, written t ⇑ v . Henceforth, we use Ω = (λx.x x) (λx.x x) as an example of such a term.

CPS Equivalence

In [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF], the authors propose an equational theory of shift and reset based on CPS [START_REF] Danvy | Abstracting control[END_REF]. The idea is to relate terms that have βη-convertible CPS translations.

Definition 4. Terms t 0 and t 1 are CPS equivalent, written t 0 ≡ t 1 , if their CPS translations are βη-convertible.

Kameyama and Hasegawa propose eight axioms in [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF] to characterize CPS equivalence: two terms are CPS equivalent iff one can derive their equality using the equations below. Note that the axioms are defined on open terms, and suppose variables as values.

(λx.t) v = KH t{v/x} (λx.E [x]) t = KH E [t] if x / ∈ fv(E ) E [Sk.t] = KH t{λx. E [x] /k} (λx.t 0 ) t 1 = KH (λx. t 0 ) t 1 v = KH v Sk. t = KH Sk.t λx.v x = KH v if x / ∈ fv(v) Sk.k t = KH t if k / ∈ fv(t)
We use the above relations as examples throughout the paper. Of particular interest is the axiom [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF], which can be difficult to prove with bisimilarities [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF].

(λx.E [x]) t = KH E [t] (if x / ∈ fv(E )), called β Ω in

Context Closures

Given a relation R on terms, we define two context closures that generate respectively terms and evaluation contexts. The term generating closure R is defined inductively as the smallest relation satisfying the following rules:

t R t ′ t R t ′ x R x t R t ′ λx.t R λx.t ′ t 0 R t ′ 0 t 1 R t ′ 1 t 0 t 1 R t ′ 0 t ′ 1 t R t ′ Sk.t R Sk.t ′ t R t ′ t R t ′
Even if R is defined only on closed terms, R is defined on open terms. In this paper, we consider the restriction of R to closed terms unless stated otherwise. The context generating closure R of a relation R is defined inductively as the smallest relation satisfying the following rules: R

F 0 R F 1 v 0 R v 1 v 0 F 0 R v 1 F 1 F 0 R F 1 t 0 R t 1 F 0 t 0 R F 1 t 1 F 0 R F 1 F 0 R F 1
Again, we consider only the restriction of R to closed contexts.

Environmental Relations for the Relaxed Semantics

In this section, we define an environmental bisimilarity which characterizes the contextual equivalence of [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF][START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF], where stuck terms can be observed.

Contextual Equivalence

We recall the definition of contextual equivalence ≈ c for the relaxed semantics (given in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]).

Definition 5. For all t 0 , t 1 be terms. We write t 0 ≈ c t 1 if for all C such that C [t 0 ] and C [t 1 ] are closed, the following hold:

-

C [t 0 ] ⇓ v v 0 implies C [t 1 ] ⇓ v v 1 ; -C [t 0 ] ⇓ v t ′ 0 , where t ′ 0 is stuck, implies C [t 1 ] ⇓ v t ′ 1 , with t ′ 1 stuck as well;
and conversely for

C [t 1 ].
The definition is simpler when using the following context lemma [START_REF] Milner | Fully abstract models of typed λ-calculi[END_REF] (for a proof see Section 3.4 in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]). Instead of testing with general, closing contexts, we can close the terms with values and then put them in evaluation contexts.

Lemma 3 (Context Lemma). We have t 0 ≈ c t 1 iff for all closed contexts F and for all substitutions σ (mapping variables to closed values) such that t 0 σ and t 1 σ are closed, the following hold:

-

F [t 0 σ] ⇓ v v 0 implies F [t 1 σ] ⇓ v v 1 ; -F [t 0 σ] ⇓ v t ′ 0 , where t ′ 0 is stuck, implies F [t 1 σ] ⇓ v t ′ 1 , with t ′ 1 stuck as well;
and conversely for F [t 1 σ].

In [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF], we prove that ≈ c satisfies all the axioms of CPS equivalence except for Sk.k t = KH t (provided k / ∈ fv(t)): indeed, Sk.k t is stuck, but t may evaluate to a value. Conversely, some contextually equivalent terms are not CPS equivalent, like Turing's and Church's call-by-value fixed point combinators. Similarly, two arbitrary diverging terms are related by ≈ c , but not necessarily by ≡.

Definition of Environmental Bisimulation and Basic Properties

Environmental bisimulations use an environment E to accumulate knowledge about two tested terms. For the λ-calculus [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF], E records the values (v 0 , v 1 ) the tested terms reduce to, if they exist. We can then compare v 0 and v 1 at any time by passing them arguments built from E. In λ S , we have to consider stuck terms as well; therefore, environments may also contain pairs of stuck terms, and we can test those by building pure contexts from E.

Formally, an environment E is a relation on closed normal forms which relates values with values and stuck terms with stuck terms; e.g., the identity environment I is {(t, t) | t is a normal form}. An environmental relation X is a set of environments E, and triples (E, t 0 , t 1 ), where t 0 and t 1 are closed. We write t 0 X E t 1 as a shorthand for (E, t 0 , t 1 ) ∈ X ; roughly, it means that we test t 0 and t 1 with the knowledge E. The open extension of X , written X • , is defined as follows

: if - → x = fv(t 0 ) ∪ fv(t 1 ) 4 , then we write t 0 X E • t 1 if λ - → x .t 0 X E λ - → x .t 1 . Definition 6. A relation X is an environmental bisimulation if 1. t 0 X E t 1 implies: (a) if t 0 → v t ′ 0 , then t 1 → * v t ′ 1 and t ′ 0 X E t ′ 1 ; (b) if t 0 = v 0 , then t 1 → * v v 1 and E ∪ {(v 0 , v 1 )} ∈ X ; (c) if t 0 is stuck, then t 1 → * v t ′ 1 with t ′ 1 stuck, and E ∪ {(t 0 , t ′ 1 )} ∈ X ; (d) the converse of the above conditions on t 1 ; 2. E ∈ X implies: (a) if λx.t 0 E λx.t 1 and v 0 E v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}; (b) if E 0 [Sk.t 0 ] E E 1 [Sk.t 1 ] and E ′ 0 E E ′ 1 , then t 0 {λx. E ′ 0 [E 0 [x]] /k} X E t 1 {λx. E ′ 1 [E 1 [x]] /k} for a fresh x.
Environmental bisimilarity, written ≈, is the largest environmental bisimulation. To prove that two terms t 0 and t 1 are equivalent, we want to relate them without any predefined knowledge, i.e., we want to prove that t 0 ≈ ∅ t 1 holds; we also write ≃ for ≈ ∅ .

The first part of the definition makes the bisimulation game explicit for t 0 , t 1 , while the second part focuses on environments E. If t 0 is a normal form, then t 1 has to evaluate to a normal form of the same kind, and we extend the environment with the newly acquired knowledge. We then compare values in E (clause (2a)) by applying them to arguments built from E, as in the λcalculus [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF]. Similarly, we test stuck terms in E by putting them within contexts E ′ 0 , E ′ 1 built from E (clause (2b)) to trigger the capture. This reminds the way we test values and stuck terms with applicative bisimilarity [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF], except that applicative bisimilarity tests both values or stuck terms with the same argument or context. Using different entities (as in Definition 6) makes bisimulation proofs harder, but it simplifies the proof of congruence of the environmental bisimilarity.

Example 1. We have (λx.t

0 ) t 1 ≃ (λx. t 0 ) t 1 , because the relation X = {(∅, (λx.t) t ′ , (λx. t ) t ′ ), (∅, (λx.t) v , (λx. t )v)}∪{(E, t, t) | E ⊆ I}∪{E | E ⊆ I} is a bisimulation. Indeed, if t ′ evaluates to v, then (λx.t) t ′ → * v (λx.t) v and (λx. t ) t ′ → * v (λx. t ) v, which both reduce to t{v/x} .
As usual with environmental relations, the candidate relation X in the above example could be made simpler with the help of up-to techniques.

Definition 6 is written in the small-step style, because each reduction step from t 0 has to be matched by t 1 . In the big-step style, we are concerned only with evaluations to normal forms.

Definition 7. A relation X is a big-step environmental bisimulation if t 0 X E t 1 implies: 1. t 0 X E t 1 implies: (a) if t 0 → * v v 0 , then t 1 → * v v 1 and E ∪ {(v 0 , v 1 )} ∈ X ; (b) if t 0 → * v t ′ 0 with t ′ 0 stuck, then t 1 → * v t ′ 1 , t ′ 1 stuck, and E ∪ {(t ′ 0 , t ′ 1 )} ∈ X ; (c) the converse of the above conditions on t 1 ; 2. E ∈ X implies: (a) if λx.t 0 E λx.t 1 and v 0 E v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}; (b) if E 0 [Sk.t 0 ] E E 1 [Sk.t 1 ] and E ′ 0 E E ′ 1 , then t 0 {λx. E ′ 0 [E 0 [x]] /k} X E t 1 {λx. E ′ 1 [E 1 [x]
] /k} for a fresh x. Lemma 4. If X is a big-step environmental bisimulation, then X ⊆ ≈.

Big-step relations can be more convenient to use when we know the result of the evaluation, as in Example 1, or as in the following one.

Example 2. We have t ≃ t . Indeed, we can show that t

→ * v v iff t → * v v, therefore {(∅, t , t )} ∪ {(E, t, t) | E ⊆ I} ∪ {E | E ⊆ I} is a big-step environmental bisimulation.
We use the following results in the rest of the paper.

Lemma 5 (Weakening).

If t 0 ≈ E t 1 and E ′ ⊆ E then t 0 ≈ E ′ t 1 .
A smaller environment is a weaker constraint, because we can build less arguments and contexts to test the normal forms in E. The proof is as in [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF]. Lemma 6 states that reduction (and therefore, evaluation) is included in ≃.

Lemma 6. If t 0 → v t ′ 0 , then t 0 ≃ t ′ 0 .

Soundness and Completeness

We now prove soundness and completeness of ≃ w.r.t. contextual equivalence.

Because the proofs follow the same steps as for the λ-calculus [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF], we only give here the main lemmas and sketch their proofs. The complete proofs can be found in [START_REF] Biernacki | Environmental bisimulations for delimited-control operators[END_REF]. First, we need some basic up-to techniques, namely up-to environment (which allows bigger environments in the bisimulation clauses) and up-to bisimilarity (which allows for limited uses of ≃ in the bisimulation clauses), whose definitions and proofs of soundness are classic [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF].

With these tools, we can prove that ≃ is sound and complete w.r.t. contextual equivalence. For a relation R on terms, we write R nf for its restriction to closed normal forms. The first step consists in proving congruence for normal forms, and also for any terms but only w.r.t. evaluation contexts.

Lemma 7. Let t 0 , t 1 be normal forms. If t 0 ≈ E t 1 , then C [t 0 ] ≈ E C [t 1 ]. Lemma 8. If t 0 ≈ E t 1 , then F [t 0 ] ≈ E F [t 1 ].
Lemmas 7 and 8 are proved simultaneously by showing that, for any environmental bisimulation Y, the relation

X = {( E nf , F 0 [t 0 ], F 1 [t 1 ]) | t 0 Y E t 1 , F 0 E F 1 } ∪ {( E nf , t 0 , t 1 ) | E ∈ Y, t 0 E t 1 } ∪ { E nf | E ∈ Y}
is a bisimulation up-to environment. Informally, the elements of the first set of X reduce to elements of the second set of X , and we then prove the bisimulation property for these elements by induction on t 0 E t 1 . We can then prove the main congruence lemma.

Lemma 9. t 0 ≃ t 1 implies C [t 0 ] ≈ ≃ nf C [t 1 ].
We show that {( ≃ nf , t 0 , t 1 ) | t 0 ≃ t 1 }∪{ ≃ nf } is a bisimulation up-to bisimilarity by induction on t 0 ≃ t 1 . By weakening (Lemma 5), we can deduce from Lemma 9 that ≃ is a congruence, and therefore is sound w.r.t. ≈ c .

Corollary 1 (Soundness). We have ≃ ⊆ ≈ c .

The relation ≃ is also complete w.r.t. contextual equivalence.

Theorem 1 (Completeness). We have ≈ c ⊆ ≃.

The proof is by showing that

{(≈ c nf , t 0 , t 1 ) | t 0 ≈ c t 1 } ∪ {≈ c
nf } is a big-step bisimulation, using Lemma 3 as an alternate definition for ≈ c .

Bisimulation up to context

Equivalence proofs based on environmental bisimilarity can be simplified by using up-to techniques, such as up to reduction, up to expansion, and up to context [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF]. We only discuss the last, since the first two can be defined and proved sound in λ S without issues. Bisimulations up to context may factor out a common context from the tested terms. Formally, we define the context closure of X , written X , as follows: we have t 0 X E t 1 if

-either t 0 = F 0 [t ′ 0 ], t 1 = F 1 [t ′ 1 ], t ′ 0 X E t ′ 1 , and F 0 E F 1 ; -or t 0 E t 1 .
Note that terms t ′ 0 and t ′ 1 (related by X E ) can be put into evaluation contexts only, while normal forms (related by E) can be put in any contexts. This restriction to evaluation contexts in the first case is usual in the definition of up-to context techniques for environmental relations [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF][START_REF] Sumii | A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation[END_REF][START_REF] Sato | The higher-order, call-by-value applied Pi-calculus[END_REF][START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF].

Definition 8. A relation X is an environmental bisimulation up to context if 1. t 0 X E t 1 implies: (a) if t 0 → v t ′ 0 , then t 1 → * v t ′ 1 and t ′ 0 X E t ′ 1 ; (b) if t 0 = v 0 , then t 1 → * v v 1 and E ∪ {(v 0 , v 1 )} ⊆ E ′ nf for some E ′ ∈ X ; (c) if t 0 is stuck, then t 1 → * v t ′ 1 with t ′ 1 stuck, and E ∪ {(t 0 , t ′ 1 )} ⊆ E ′ nf for some E ′ ∈ X ; (d) the converse of the above conditions on t 1 ; 2. E ∈ X implies: (a) if λx.t 0 E λx.t 1 and v 0 E v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}; (b) if E 0 [Sk.t 0 ] E E 1 [Sk.t 1 ] and E ′ 0 E E ′ 1 , then t 0 {λx. E ′ 0 [E 0 [x]] /k} X E t 1 {λx. E ′ 1 [E 1 [x]
] /k} for a fresh x.

Lemma 10. If X is an environmental bisimulation up to context, then X ⊆ ≈.

The soundness proof is the same as in [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF]. While this definition is enough to simplify proofs in the λ-calculus case, it is not that helpful in λ S , because of the restriction to evaluation contexts (first item of the definition of X ). In the λcalculus, when a term t reduces within an evaluation context, the context is not affected, hence Definition 8 is enough to help proving interesting equivalences. It is not the case in λ S , as (a part of) the evaluation context can be captured. Indeed, suppose we want to construct a candidate relation X to prove the β Ω axiom, i.e., E [t] is equivalent to (λx.E [x]) t, assuming x / ∈ fv(E ). The problematic case is when t is a stuck term E 0 [Sk.t 0 ]; we have to add the stuck terms (λx.E

[x]) E 0 [Sk.t 0 ] and E [E 0 [Sk.t 0 ]] to an environment E of X .
For X to be a bisimulation, we then have to prove that for all Problem (ii) could be somewhat dealt with in the particular case of the β Ω axiom by changing clause (2b) of Definition 8 into

E 1 E E 2 , we have t 0 {λy. E 1 [(λx.E [x]) E 0 [y]] /k} X E t 0 {λy. E 2 [E [E 0 [y]]] /k} . At
(b) if E 0 [Sk.t 0 ] E E 1 [Sk.t 1 ] and E ′ 0 X E E ′ 1 , then t 0 {λx. E ′ 0 [E 0 [x]] /k} X E t 1 {λx. E ′ 1 [E 1 [x]
] /k} for a fresh x.

and similarly for clause (2a). In plain text, we build the testing contexts E ′ 0 , E ′ 1 from X E (instead of E), and the resulting terms have to be in X E (without any evaluation context restriction). The resulting notion of bisimulation up to context is sound. The new clause would be more difficult to establish in general than the original one (of Definition 8), because it tests more pairs of contexts. However, for the β Ω axiom, we would have to prove that for all

E 1 X E E 2 , t 0 {λy. E 1 [(λx.E [x]) E 0 [y]] /k} X E t 0 {λy. E 2 [E [E 0 [y]]] /
[x]) E 0 [y] X E • E [E 0 [y]] to hold, we must have (λx.E [x]) E 0 [v 0 ] X E E [E 0 [v 1 ]] for all v 0 E v 1 . Because E 0 can be anything, it means that we must have (λx.E [x]) t ′ 0 X E E [t ′ 1 ] with t ′ 0 E t ′ 1 ; t ′ 0 and t ′
1 are plugged in different contexts, therefore bisimulation up to context (which factors out only a common context) cannot help us there; a new kind of up-to technique is required. The β Ω axiom example suggests that we need more powerful up-to techniques for environmental bisimilarity for delimited control; we leave these potential improvements as a future work. Note that we do not have such issues with up-to techniques for normal form bisimilarity: it relates open terms without having to replace their free variables, and normal form bisimulation up to context is not restricted to evaluation contexts only. But even if environmental bisimulation up to context is not as helpful as wished, it still simplifies equivalence proofs, as we can see with the next example.

Example 3. In [START_REF] Danvy | A functional abstraction of typed contexts[END_REF], a variant of Turing's call-by-value fixed point combinators using shift and reset has been proposed. Let θ = λxy.y (λz.x x y z). We prove that t 0 = θ θ is bisimilar to its variant t 1 = θ Sk.k k . Let θ ′ = λx. θ x , v 0 = λy.y (λz.θ θ y z), and v 1 = λy.y (λz.θ ′ θ ′ y z). We define E inductively such that v 0 E v 1 , and if

v ′ 0 E v ′ 1 , then λz.θ θ v ′ 0 z E λz.θ ′ θ ′ v ′ 1 z. Then X = {(E, t 0 , t 1 ), (E, t 0 , θ ′ θ ′ ), E} is a (big-step) bisimulation up to context. Indeed, we have t 0 ⇓ v v 0 , t 1 ⇓ v v 1 , and θ ′ θ ′ ⇓ v v 1 ,
therefore clause (1b) of Definition 8 is checked for both pairs. We now check clause (2a), first for

v 0 E v 1 . For all v ′ 0 E v ′ 1 , we have v ′ 0 (λz.θ θ v ′ 0 z) E v ′ 1 (λz.θ ′ θ ′ v ′ 1 z) (because λz.θ θ v ′ 0 z E λz.θ ′ θ ′ v ′ 1 z), hence the result holds. Next, let λz.θ θ v ′ 0 z E λz.θ ′ θ ′ v ′ 1 z (with v ′ 0 E v ′ 1 )
, and let

v ′′ 0 E v ′′ 1 . We have to check that θ θ v ′ 0 v ′′ 0 X E θ ′ θ ′ v ′ 1 v ′′ 1 , which is true, because θ θ X E θ ′ θ ′ , and v ′ 0 v ′′ 0 E v ′ 1 v ′′ 1 .

Environmental Relations for the Original Semantics

The original CPS semantics for shift and reset [START_REF] Danvy | Abstracting control[END_REF] as well as the corresponding reduction semantics [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF] assume that terms can be considered as programs to be executed, only when surrounded by a top-level reset. In this section, we present a CPS-compatible bisimulation theory that takes such a requirement into account. Henceforth, we call programs, ranged over by p, terms of the form t .

Contextual Equivalence

To reflect the fact that terms are executed within an enclosing reset, the contextual equivalence we consider in this section tests terms in contexts of the form C only. Because programs cannot reduce to stuck terms, the only possible observable action is evaluation to values. We therefore define contextual equivalence for programs as follows.

Definition 9. Let t 0 , t 1 be terms. We write t 0 .

≈ c t 1 if for all C such that C [t 0 ] and C [t 1 ] are closed, C [t 0 ] ⇓ v v 0 implies C [t 1 ] ⇓ v v 1 , and conversely for C [t 1 ] .

Note that

. ≈ c is defined on all terms, not just programs. It is easy to check that ≈ c is more discriminative than . ≈ c . We will see in Section 4.4 that this inclusion is in fact strict.

Lemma 11. We have ≈ c ⊆ . ≈ c .

Definition and Properties

We now propose a definition of environmental bisimulation adapted to programs (but defined on all terms, like . ≈ c ). Because stuck terms are no longer observed, environments E henceforth relate only values. Similarly, we write R v for the restriction of a relation R on terms to pairs of closed values. Definition 10. A relation X is an environmental bisimulation for programs if 1. if t 0 X E t 1 and t 0 and t 1 are not both programs, then for all 3) of Definition 10 deal with programs and environment in a classical way (as in plain λ-calculus). The problematic case is when relating terms t 0 and t 1 that are not both programs (clause (1)). Indeed, one of them may be stuck, and therefore we have to test them within some contexts E 0 , E 1 (built from E) to potentially trigger a capture that otherwise would not happen. We cannot require both terms to be stuck, as in clause (2b) of Definition 6, because a stuck term can be equivalent to a term free from control effect. E.g., we will see that v

E 0 E E 1 , we have E 0 [t 0 ] X E E 1 [t 1 ] ; 2. if p 0 X E p 1 (a) if p 0 → v p ′ 0 , then p 1 → * v p ′ 1 and p ′ 0 X E p ′ 1 ; (b) if p 0 → v v 0 , then p 1 → * v v 1 , and {(v 0 , v 1 )} ∪ E ∈ X ; (c)

Soundness and Completeness

We sketch the proofs of soundness and completeness of . ≃ w.r.t.

. ≈ c ; see [START_REF] Biernacki | Environmental bisimulations for delimited-control operators[END_REF] for the complete proofs. The soundness proof follows the same scheme as in Section 3.3, with some necessary adjustments. As before, we need up-to environment and up-to bisimilarity techniques to prove the following lemmas.

Lemma 13. If v 0 . ≈ E v 1 , then C [v 0 ] . ≈ E C [v 1 ]. Lemma 14. If t 0 . ≈ E t 1 , then F [t 0 ] . ≈ E F [t 1 ].
We prove Lemmas 13 and 14 by showing that a relation similar to the relation X defined in Section 3.3 is a bisimulation up to environment. We then want to prove the main congruence lemma, akin to Lemma 9, by showing that

Y ={( . ≃ v , t 0 , t 1 ) | t 0 . ≃ t 1 } ∪ { . ≃ v
} is a bisimulation up to bisimilarity. However, we can no longer proceed by induction on t 0 . ≃ t 1 , as for Lemma 9. Indeed, if p 0 = t 0 , p 1 = t 1 with t 0 . ≃ t 1 , and if t 0 is a stuck term, then p 0 reduces to some term, but the induction hypothesis does not tell us anything about t 1 . To circumvent this, we decompose related programs into related subcomponents.

-p 0 = v 0 ; -p 0 = F 0 [ E 0 [t 0 ] ], p 1 = F 1 [ E 1 [t 1 ] ] , F 0 . ≃ F 1 , E 0 . ≃ E 1 , t 0 . ≃ t 1 and t 0 → v t ′ 0 or t 0 is stuck; -p 0 = F 0 [ E 0 [r 0 ] ], p 1 = F 1 [ E 1 [t 1 ] ] , F 0 . ≃ F 1 , E 0 . ≃ E 1 , r 0 . ≃ t 1 but r 0 . ≃ t 1 .
Lemma 15 generalizes Lemma 2 to related programs: we know p 0 can be decomposed into contexts F , E , and a redex r, and we relate these subterms to p 1 . We can then prove that Y (defined above) is a bisimulation up to bisimilarity, by showing that, in each case described by Lemma 15, p 0 and p 1 reduce to terms related by Y. From this, we deduce . ≃ is a congruence, and is sound w.r.t.

. ≈ c . Lemma 16. t 0 . ≃ t 1 implies C [t 0 ] . ≈ . ≃ v C [t 1 ].
Corollary 2 (Soundness). We have .

≃ ⊆

. ≈ c . Remark 1. Following the ideas behind Definition 10, one can define an applicative bisimilarity B for programs. However, proving that B is sound seems more complex than for . ≃. We remind that the soundness proof of an applicative bisimilarity consists in showing that a relation called the Howe's closure B • is an applicative bisimulation. To this end, we need a version of Lemma 15 for B • . However, B • is inductively defined as the smallest congruence which contains B and satisfies B • B ⊆ B • (1), and condition (1) makes it difficult to write a decomposition lemma for B • similar to Lemma 15.

We prove completeness of Definition 11. Let t 0 , t 1 be closed terms. We write t 0 ≈c t 1 if for all closed F , F

[t 0 ] ⇓ v v 0 implies F [t 1 ] ⇓ v v 1 ,

Examples

We illustrate the differences between ≃ and Proving Lemma 19 without the β Ω axiom and Lemmas 20 and 21 without ≡ requires complex candidate relations (see the proof of Lemma 20 in [START_REF] Biernacki | Environmental bisimulations for delimited-control operators[END_REF]), because of the lack of powerful enough up-to techniques.

Conclusion

We propose sound and complete environmental bisimilarities for two variants of the semantics of λ S . For the semantics of Section 3, we now have several bisimilarities, each with its own merit. Normal form bisimilarity [START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF] (and its up-to techniques) leads to minimal proof obligations, however it is not complete, and distinguishes very simple equivalent terms (see Proposition 1 in [START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF]). Applicative bisimilarity [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF] is complete but sometimes requires complex bisimulation proofs (e.g., for the β Ω axiom). Environmental bisimilarity ≃ (Definition 6) is also complete, can be difficult to use, but this difficulty can be mitigated with up-to techniques. However, bisimulation up to context is not as helpful as we could hope (see Section 3.4), because we have to manipulate open terms (problem (i)), and the context closure of an environmental relation is restricted to evaluation contexts (problem (ii)). As a result, proving the β Ω axiom is more difficult with environmental than with applicative bisimilarity. We believe dealing with problem (i) requires new up-to techniques to be developed, and lifting the evaluation context restriction (problem (ii)) would benefit not only for λ S , but also for process calculi with passivation [START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF]; we leave this as a future work.

In contrast, we do not have as many options when considering the semantics of Section 4 (where terms are evaluated within a top-level reset). The environmental bisimilarity of this paper . ≃ (Definition 10) is the first to be sound and complete w.r.t. Definition 9. As argued in [START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF] (Section 3.2), normal form bisimilarity cannot be defined on programs without introducing extra quantifications (which defeats the purpose of normal form bisimilarity). Applicative bisimilarity could be defined for programs, but proving its soundness would require a new technique, since the usual one (Howe's method) does not seem to apply (see Remark 1). This confirms that environmental bisimilarity is more flexible than applicative bisimilarity [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF]. However, we would like to simplify the quantification over contexts in clause (1) of Definition 10, so we look for sub-classes of terms where this quantification is not mandatory.

Other future works include the study of the behavioral theory of other delimited control operators, like the dynamic ones (e.g., control and prompt [START_REF] Felleisen | The theory and practice of first-class prompts[END_REF] or shift 0 and reset 0 [START_REF] Danvy | A functional abstraction of typed contexts[END_REF]), but also of abortive control operators, such as callcc, for which no sound and complete bisimilarity has been defined so far.

Lemma 15 ..≃ p 1 , then either p 0 .≃ p 1 ,

 15101 If p 0 or one of the following holds:

.≃

  by showing that the relation ≈c , defined below, coincides with . ≈ c and . ≃. By doing so, we also prove a context lemma for . ≈ c .

  and conversely for F [t 1 ] . By definition, we have . ≈ c ⊆ ≈c . With the same proof technique as in Section 3.3, we prove the following lemma. Lemma 17 (Completeness). We have ≈c ⊆ . Defining up-to context for programs is possible, with the same limitations as in Section 3.4.

  , so the reduction rules specify both the notion of reduction and the chosen call-by-value evaluation strategy that is encoded in the grammar of the evaluation contexts. Furthermore, the reduction relation→ v is compatible with evaluation contexts F , i.e., F [t] → v F [t ′ ] whenever t → v t ′ .There exist terms which are not values and which cannot be reduced any further; these are called stuck terms.Definition 1. A term t is stuck if t is not a value and t → v . Lemma 1. A closed term t is stuck iff t = E [Sk.t ′ ]for some E , k, and t ′ . For all closed terms t, either t is a normal form, or there exist a unique redex r and a unique context F such that t = F [r].

	t) v is the usual call-by-value redex for β-reduction (rule (β v )).
	The operator Sk.t captures its surrounding context E up to the dynamically
	nearest enclosing reset, and substitutes λx. E [x] for k in t (rule (shift)). If a
	reset is enclosing a value, then it has no purpose as a delimiter for a potential
	capture, and it can be safely removed (rule (reset)). All these reductions may
	occur within a metalevel context F For example, the term E [Sk.t] is stuck because there is no enclosing reset; the
	capture of E by the shift operator cannot be triggered.
	Definition 2. A term t is a normal form if t is a value or a stuck term.
	We call redexes (ranged over by r) terms of the form (λx.t) v, E [Sk.t] ,
	and v . Thanks to the following unique-decomposition property, the reduction
	relation → v is deterministic.
	Lemma 2.

  this point, we would like to use the up-to context technique, because the subterms (λx.E [x])E 0 [y] and E [E 0 [y]] are similar to the terms we want to relate (they can be written (λx.E [x]) t ′′ and E [t ′′ ] with t ′′ = E 0 [y]). However, we have at bestt 0 {λy. E 1 [(λx.E [x]) E 0 [y]] /k} X E • t 0 {λy. E 2 [E [E 0 [y]]] /k} (and not X E ), because (i) (λx.E [x]) E 0 [y] and E [E 0 [y]] are open terms, and (ii) t 0 can be any term, so (λx.E [x]) E 0 [y] and E [E 0[y]] can be put in any context, not necessarily in an evaluation one. Therefore, Definition 8 cannot help there.

  the converse of the above conditions on p1 ; 3. for all E ∈ X , if λx.t 0 E λx.t 1 and v 0 E v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}.

	Environmental bisimilarity for programs, written bisimulation for programs. As before, the relation to characterize . ≈ c .	. ≈, is the largest environmental . ≈ ∅ , also written . ≃, is candidate
	Clauses (2) and (

  Suppose we want to prove (λx.t 0 ) t 1 . ≃ (λx. t 0 ) t 1 (as in Example 1). Because (λx. t 0 ) t 1 is not a program, we have to put both terms into a context first: we have to change the candidate relation of Example 1 into X= {(∅, (λx.t 0 ) t 1 , (λx. t 0 ) t 1 )} ∪ {(∅, E [ (λx.t 0 ) t 1 ] , E [(λx. t 0 ) t 1 ] )} ∪ {(∅, E [ (λx.t 0 ) v ] , E [(λx. t 0 ) v] )} ∪ {(E, t, t) | E ⊆ I} ∪ {E | E ⊆ I}. In contrast,to prove t The next lemma shows that ≃ is more discriminative than E.g., we have directly (λx.t 0 ) t 1 . ≃ (λx. t 0 ) t 1 , because (λx.t 0 ) t 1 ≃ (λx. t 0 ) t 1 .

	≃ Sk.k v, provided that k / ∈ fv(v).
	Example 4. . ≃ t , we do not have to change the candidate relation
	of Example 2, since both terms are programs.
	We can give a definition of big-step bisimulation by removing clause (2a) and
	changing → v into → * v in clause (2b). Lemmas 5 and 6 can also be extended to . ≃.
	Lemma 12. We have ≃ ⊆	. ≃.
	A consequence of Lemma 12 is that we can use Definition 6 as a proof
	technique for

. . ≈ and . ≃. . ≃.

  The relation {(∅, Ω, Sk.Ω), (∅,E [Ω] , E [Sk.Ω] ), (∅, E [Ω], Ω )} is a bisimulation for programs. Lemma 18 does not hold with ≃ because Ω is not stuck.We sketch the proof for t closed; for the general case, see[START_REF] Biernacki | Environmental bisimulations for delimited-control operators[END_REF]. We prove that E.g., the following equivalence can be derived from the axioms[START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF].Lemma 20. If k /∈ fv(t 1 ), then (λx.Sk.t 0 ) t 1This equivalence does not hold with ≃, because the term on the right is stuck, but the term on the left may not evaluate to a stuck term (if t 1 does not terminate). We can generalize this result as follows, again by using ≡.

	related by	. ≃, by giving some examples of terms ≃, but not by ≃. First, note that . . ≃ relates non-terminating terms
	with stuck non-terminating terms.
	Lemma 18. We have Ω	. ≃ Sk.Ω.
	As wished,	. ≃ satisfies the only axiom of [14] not satisfied by ≃.
	Lemma 19. If k / ∈ fv(t), then t	. ≃	• Sk.k t.

{(∅, t, Sk.k t), (∅, E [t] , E [Sk.k t] )}∪ ≃ is a bisimulation for programs. Indeed, we have E [Sk.k t] → v (λx. E [x] ) t , and because ≃ verifies the β Ω axiom (≃ is complete, and ≈ c verifies the β Ω axiom [4]), we know that (λx. E [x] ) t ≃ E [t] holds. From Example 2, we have E [t] ≃ E [t] , therefore we have E [Sk.k t] ≃ E [t] . Consequently, . ≃ • is complete w.r.t. ≡. Corollary 3. We have ≡ ⊆ . ≃ • . As a result, we can use ≡ (restricted to closed terms) as a proof technique for . ≃. . ≃ Sk.((λx.t 0 ) t 1 ). Lemma 21. If k / ∈ fv(t 1 ) and x / ∈ fv(E ), then we have (λx.E [Sk.t 0 ]) t 1 . ≃ E [Sk.((λx.t 0 ) t 1 )].

This terminology comes from Kameyama (e.g., in[START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]).

Given a metavariable m, we write -→ m for a set of entities denoted by m.

Acknowledgments We thank Ma lgorzata Biernacka and the anonymous referees for many helpful comments on the presentation of this work.


K Harkouken Saiah

N Sabouret

J-Y Donnart

An Ontology for Semantic Representation of an Urban Virtual Environment

Keywords: Knowledge Representation and Reasoning, Semantic Virtual Environments, Ontology, Urban Simulation

We present in this paper a model of semantic representation of a dynamic virtual environment. Our model is embodied into a simulation architecture of a virtual city. The objective is to enable agents to make action decision consistent with the semantic state of their environment. The idea is to represent the services offered by the environment into an ontology of services and deduce the available object that has the best quality of service at any given time of the simulation. For this, we defined a layer of the ontology containing the general concepts of representation of the environment. This representation allows us to apply a unified model of reasoning to infer elements of knowledge useful for decision-making agents.

Introduction

Knowledge representation for virtual environments (VE) became an important issue with increasing interest in the last decade [START_REF] Aylett | Intelligent virtual environments: a stateof-the-art report[END_REF] [START_REF] Chevaillier | Semantic modelling of virtual environments using mascaret[END_REF]. Indeed, the agents operating in VE need semantic informations on it to adapt their behavior to identifiable elements of that environment and making a choice of action [START_REF] Tutenel | The role of semantics in games and simulations[END_REF]. Semantic Virtual Environments (SVE) [START_REF] Otto | Towards semantic virtual environments[END_REF] have been proposed to address this lack of semantic informations (environmental knowledge) necessary to support intelligent interactions between agents and their environment. In fact, SVE provide a coherent representation of (i) the simulated world and the behavior of its entities, (ii) the interactions and tasks that users and agents can perform in the environment, and (iii) elements of knowledge that the agents can use to make decisions [START_REF] Stanney | Handbook of virtual environments: design, implementation, and applications[END_REF].

The work carried out for the representation of VE are divided into two categories corresponding to two levels of semantics.

The first category of these works aims at an explicit representation of the contents of the environment to reproduce the scenes. Therefore, the agents have direct access to the definitions of entities of the environment. These representations are mainly geometric and topological information of the environment. Several approaches have been proposed for this representation. Most of them offer an ontological representation [START_REF] Gruber | Toward principles for the design of ontologies used for knowledge sharing[END_REF] containing different types of environmental information for different types of application.

Otto [START_REF] Otto | Towards semantic virtual environments[END_REF] uses domain ontologies to create virtual environments in a platform he called "SeVEn". The goal is to find a representation of the environment independent from the software description to create virtual objects that can be reused in several virtual environments. This reuse is possible by adding information relevant to the tasks of an object in the field of virtual environments generation. Following the same principle, [START_REF] Pellens | Conceptual modeling of object behavior in a virtual environment[END_REF], [START_REF] Troyer | On generating virtual worlds from domain ontologies[END_REF] propose to generate a virtual world from an ontology. It contains a description of the objects and their properties defined by domain experts.

Kalogerakis et al. [START_REF] Kalogerakis | Coupling ontologies with graphics content for knowledge driven visualization[END_REF] have defined an ontology "X3DOntology" associated with entities defined in description files of 3D virtual worlds. This provide a semantic representation of the scene to infer its content. We can find the same approach in [START_REF] Vanacken Lode | Using relations between concepts during interaction modelling for virtual environments[END_REF] but at a higher level, making the correspondence between the objects of the virtual environment and the concepts of the ontology.

These works give agents direct access to descriptions of VE entities. However, this definition of the world doesn't allow them to deduce information for decision support to identify (i) the object that allows them to perform an action, (ii) what actions can be performed on an object (iii) the relationship between two objects, (iv) and the relationship between actions.

The second category of works on semantic representation of VE has been made to strengthen the agent-object interactions that include not only information related to the geometry of the scene, but also knowledge about the possible interactions with the objects in the environment [START_REF] Edward | Knowledge representation -an ontology for managing a virtual environment[END_REF] (what can be done? how this can be done? why and how it should be done?).

In [START_REF] Grimaldo | Simulating socially intelligent agents in semantic virtual environments[END_REF] and [START_REF] Chu | Using pluggable procedures and ontology to realize semantic virtual environments 2[END_REF], the authors have extended the principle of using ontologies to represent SVE incorporating the semantic description related to the function of objects so that agents can design their own animation procedures like path planning.

Kallmann & Thalmann [START_REF] Kallmann | Direct 3d interaction with smart objects[END_REF] have proposed Smart Object whose idea is to include in the description of the object all the required information to describe how to interact with it. They distinguish information on: (i) the properties of the object (semantic and physical), (ii) how to interact with the object (actions, positions, gestures), (iii) the behavior of the object in response to an action and (iv) the behavior of actors to achieve interaction. Following the same philosophy, Badawi [START_REF] Marwan | Autonomous agents interacting with their virtual environment through synoptic objects[END_REF] proposes Synoptic Objects STAR FISH. The idea is to define a minimum set of primitive actions which are used to build complex actions.

In a lower level of representation [START_REF] Chevaillier | Semantic modelling of virtual environments using mascaret[END_REF] they developed a meta-model to represent the semantic of the VE and its structural properties, geometrical, topological, the behavior of agents and interactions between agents and users.

These works propose a semantic representation of VE which offers data for decision-making of agents. This give them the ability to interact with the VE and avoid having aberrant behaviors (that never occur in real life). But these solutions do not give agents the elements of knowledge to make the best choice of action for a given situation. They can provide the utility and function of an object of the environment but agents should make the connection with their actions plan to decide if it suits them or not.

Instead, we propose in this paper a method that avoids agents to find which element of the environment will allow them to carry out their plan. The idea is to provide agents with a sorted list of objects according to their relevance regarding their actions plans. Our goal is not to influence the decisions of agents or decide for them, but we aim to provide them with knowledge they need to make a decision consistent with the context. The goal of our approach is to decentralize and capitalize calculations made by agents by strengthening communication links between the decisionmaking of the agents and the representation of their environment. Our choice is justified by the complexity of the calculations for the decision and the large number of agents contained in the SVE.

Published works with similar objectives, propose a representation of the environment that integrates the description of possible actions that agents can perform. In this case, the interactions between the elements of the simulated world and the agents are managed by their environment and are related to what is defined in it. However, the heterogeneity of SVE (different categories of its elements) increases the size of the representation and affects the calculations cost to be performed by agents.

Our first contribution is to overcome this problem by proposing a unified representation model of the environment which allows us to do a generic calcul of decision support elements (measure of relevance between the action of the agent and function given by an element of the environment). The idea is to have simple calculations and applicable to all elements of the environment by treating uniformly requests of agents. Our study focuses on modeling the semantics of a virtual urban environment which has the distinction of being complex and heterogeneous, ie, it is composed of several types of objects with different features. The objective is to propose a model to represent the semantic of the environment allowing us to apply a unified treatment for all its components.

Our second contribution is to represent the types of objects that make up the environment by services (services offered by objects of the environment), where each service of the environment will be evaluated according to the type of object that proposed it. We were inspired by the techniques of semantic web [START_REF] Berners-Lee | The semantic web[END_REF] [17] by defining the elements of the environment in a Ontology of Services. We consider that each object type offers one or more services with some quality. The Quality of Service is derived from the unified reasoning we have applied on our representation model and it will be used by agents to make their decision.

In the remainder of this article, we present the architecture on which we are working, and then we describe the representation model we proposed. Finally, we discuss the first results of the implementation of this model and perspectives of our work.

Architecture

Our representation module of the environment is part of a platform of the project Terra Dynamica1 , which is a simulation project of a virtual dynamical city. The architecture of the project consists of several modules interacting with each other (semantic representation of the environment, decisionmaking, affective, path-finding and patrol).

As shown in figure 1, the environment semantic representation module interacts with the decision-making module of the agents. These interactions are summarized in an exchange of requests / responses between the two modules. The decision-making module queries the semantic representation module so that it offers him the environment entities enabling to define an action plan for the agents or to choose the best element of the environment allowing them to make an action. For the latter case, we distinguish two situations (i) agents that want to achieve immediate action (which they consider very important) and (ii) agents that want to perform a task plan in an opportunistic manner (when a opportunistic situation occurs). We therefore considered three types of interactions between the semantic representation module and the decisionmaking module :

• Interrogative mode: during the planning phase the semantic representation module is requested to provide information on the environment to make a plan of action. The semantic module responds to these requests by providing the elements of the environment allowing to achieve the action plan in line with the context of the environment (Query: what allows me to eat, Answer: a restaurant, sandwich, etc.).

• Reactive mode: it occurs during the carrying out of the agents plan. In this case, the agents know what element of the environment they want to use (defined during the planning step). When they are preparing to use a service provided by this element, a request is submitted to the semantic module to return the quality of service in relation with the context on one hand and action on the other hand. • Pro-active mode: agents can submit an application of interest for a given service. The semantic module takes account for propose the elements of the environment providing the service when they arise. We also distinguish two types of queries sent by the decision-making modules of the agents:

• Request to obtain a given service (for interrogative mode and pro-active mode), • Request on the consistency to use an element of the environment for obtaining a given service (for reactive mode). We will see in section 4 how these queries are implemented.

Model

Our representation model of the environment is based on a two-level ontology that provides support for a generic mechanism for reasoning about the dynamic and functioning of the simulated environment (see Fig. 2).

Ontology of Services

In our model, an ontology is a pair O =< C, R >, where C is the set of concepts and R is the set of binary relations. The ontology of services is not limited to relations of hierarchy (isa) or meronymy (partof ), but we also defined specific relationships with our goal of representation.

The generic level of our ontology of services contains general knowledge of environmental concepts C which consists of three subsets C = S ∪ O ∪ C r where:

• S the set of all services,

• O the set of all types of objects in the environment, • C r collects the evaluation criteria of the quality of service rendered by an object type.

Definition of object types

An object type is an element of the environment providing one or more services. Each object type provides a service with a certain quality (rendering service).

Definition of services

A service is a tuple name, C r (s) ⊂ C r , O(s) ⊂ O such that name is the service name, C r (s) the set of criteria for evaluating service s and O(s) the set of object types providing this service.

We have defined the relationship of f ers(o, s) ∈ O × S between services and object types. It allows us to say that one object type o offers a service s ∈ S such that o ∈ O(s). For example, the service Eat can be offered by several types of objects O(Eat) ={Restaurant, Fast Food, Cafeteria, etc}, this service will be evaluated according to the criteria C r (Eat) = {Cost, Time, Quantity, Quality, Ambiance}.

We have defined two hierarchy levels of service S a and S b , as we can see in Fig. 3.

• Behavior service S b : set of services allowing to have a behavior and to respond to a motivation, • Action service S a : set of services allowing to make an action. Such as S = S b ∪ S a and S b ∩ S a = φ.

This two types of services are related by the relation Implements(s, s ) ∈ S a × S b , which means that a behavior service can be obtained (implemented) by one or more action service. For example, the service s = Eat ∈ S b is a behavior service which can be achieved by different ways (implemented with different action services) s 1 = have a snack, s 2 = N ibble, etc, with s 1 , s 2 ∈ S a .

For each behavior service there is at least one action service that implements it ∀s ∈ S b , ∃s ∈ S a such that implements(s , s), where a service action is related to a single service behavior ∀s ∈ S a , ∃!s ∈ S b such that implements(s , s). For example, the service Drink proposed by the Restaurant depends on the service eat proposed by the same object Restaurant because we can't use the service Drink of the restaurant if we don't intend to eat.

We use the dependency relationship between the services in calculating the quality of service (section 3.2.1). Fig. 4: Ontology of services : example of service "Eat" Definition of criteria for evaluating services C r Services are evaluated according to a set of criteria. A criterion can be shared by multiple services, such as Cost, or it can be specific to a service, such as quality of food which is reserved for catering services.

Let C r the set of criteria. Each service s ∈ S will be assessed according to a subset of C r which we denote C r (s) ⊂ C r .

The set of criteria C r (s) of an action service s ∈ S a is a subset of criteria C r (s ) of behavior service s ∈ S b it implements (∀s ∈ S a , s ∈ S b , implements(s, s ) ⇒ C r (s) ⊆ C r (s )).

We have defined a non-hierarchical relation applies between services and criteria, such that applies(c, s) ∈ C r ×S, which means that the criterion c is applied to evaluate the service s (see Fig. 4).

We have defined for each criterion c ∈ C r a set of values denoted V (c). This set contains all possible values of a given criterion c. We have for example the values V (cost) = {expensive, not cher, free}.

Quality of Service

Quality of Service QoS is calculated thanks to the following parameters:

• Effectiveness, to assess whether an environmental element meets the needs of the agent and allows it to perform its task. • Difficulty, calculate the induced cost by additional constraints to access the desired service. • Proximity, measure the accessibility of a service based on the abundance of elements in the environment that offer the desired service. Note that the QoS is independent of agents preferences (we have set one type of calculation for any object type or service).

We note that the decisional module of agents take into account other information about the environment and the state of the simulation in addition to the QoS for making a decision (geometric and topological data extracted from the DB, distance from an object, the presence of a queue, etc.).

Parameters for calculating the QoS Effectiveness

The effectiveness of an object type o ∈ O offering a service s ∈ S a searched by an agent is the ratio between the number of criteria satisfied with the service provided by the object type and the total number of evaluation criteria of service s.

To do this, we define the following sets: Let QC(o, s) ⊆ C r (s) the set of criteria that apply to assess the service s proposed by an object type o ∈ O such that s ∈ S a , o ∈ O(s) and ∃of f ers(o, s). For example, the service s = have a snack proposed by the object type o 1 = Vending machine have the set criteria as QC(o 1 , s) = { Cost, Time, Quality, Quantity } and the type of object o 2 = Fast food restaurant offering the same service s have the set criteria as QC(o 2 , s) = { Cost, Time, Quality, Quantity, Ambiance }.

We have defined a set of values on the criteria of the service s we noted V q (s, c) ⊆ V (c) such that c ∈ C r (s). The set V q (s, c) contains all possible values that can take a service s for one of its criteria c. For example, the criterion c = Quantity for the service s = have a snack will have a value in the set { Medium, Small }.

We have defined a set EQ(s) (Estimated Quality) containing all possible combinations of pairs (criterion, value) for a service s with EQ(s) = {(c, v) ∈ C r (s) × V q (s, c)}. In the previous example, EQ( have a snack) contains all { (Quantity, Small), (Quantity, Medium) }.

Let EQ(o, s) the set of effects expected by the use of an object type o ∈ O to obtain a given service s ∈ S a with EQ(o, s

) = {(c, v)/c ∈ QC(o, s) ∧ v ∈ V q (s, c)}.
For example, the service s = have a snack proposed by the object o = Vending machine will result in EQ(o, s) = {(Cost, Not expensive), (Time, Speed), (Quantity, Small)}.

Efficiency Ef f (o, s) of the object type o relative to the requested service s is therefore calculated as follows:

Ef f (o, s) = |EQ(s) ∩ EQ(o, s)| |QC(o, s)| 2

Difficulty

The difficulty parameter is based on additional conditions to be added to obtain a service. We consider that an object type offers a service with a difficulty when it depends on another service offered by the same object type.The difficulty Dif f (o, s) of the service s offered by the object type o and having a relationship of dependence (dep(s, s )) with another service s is the rate of criteria in addition to consider (criteria of s ) for obtain service s.

Dif f (o, s) = |C r (s )| -|QC(o, s) ∩ QC(o, s )| |C r (s )|
The difficulty is not taken into account in the case where the agent had planned an action corresponding to the service s in its original plan. In this case, the solution to have both services will be considered an optimized solution.

Proximity

We measured the proximity of a service based on the attendance of the type that offer this service. Our goal is to enable agents to tell the difference between one object type they can find very often in the environment, making it more accessible and less difficult to find, and an object type not very common in the environment and may be the only way for getting given service.

Let o ∈ O an object type providing the service sought s. We defined the set O p (o) containing the instances of objects with the object type o. Let O s (s) the set of instances of the object types o ∈ O offering the service s.

The proximity P rox(o, s) of an object type o offering the service s will be calculated as the ratio between the number of its instances, and the number of instances of object types that offer same service s:

P rox(o, s) = |O p (o)| |O s (s)|

calculating the QoS

The quality of service offered by an object type of the environment takes into account the three parameters we mentioned above, with a variant on the weight of their importance. For example, an agent may prefer to have an object type which provides a service with maximum efficiency 2 We denote by |X| the number of elements of the set X regardless of the means to do so (difficulty parameter) or difficult to find (proximity parameter).

We calculated the QoS by a weighted sum of three parameters as follows:

QoS(o, s) = p 1 Ef f (o, s) + p 2 Dif f (o, s) + p 3 P rox(o, s) 3 i p i
In the implementation of our model (next section), we assumed that all parameters have the same importance weight of (p 1 = p 2 = p 3 = 1).

Implementation and first results

We have implemented our model in the platform development of the Terra Dynamica project (see Fig. 5), developed in C++. We built our ontology using the Protégé3 . Access to the ontology is done by sending SPARQL queries4 . These requests are processed according to the three modes of interaction defined above (interrogative, reactive, pro-active).

Requests sent by the decisional module contain the name of the service desired by the agent. These are transformed into SPARQL queries to return a set of object types offering this service. The principle of the research of object types offering a service is to explore the hierarchy of downwards services if we have a behavior service as an input, this will allow us to define the set of services that implements it (knowing that an object type is connected with an action service). Once all the services that can satisfy the agent are found, we will ask our ontology to infer all object types that allow us to have these services.

All object types that returned from querying our ontology will be sorted according to the QoS we have calculated for each object type. Finaly, the decision module selects an instance of one of these object types with the best QoS. The first results show that the actors of the simulation exhibit a good reactivity to the context. We have seen actors who were heading breweries and bakeries to satisfy their hunger motivation (interrogative mode).We can also see actors throw something in the garbage and continue their activity (pro-active mode). And finally, we found that actors used the objects services when it was possible for the reactive mode (no queue on the same object while another object type is available a little further).

Conclusion

We presented in this paper a model for representing the semantic of a complex and heterogeneous virtual environment (virtual city). We propose an ontology of services which defines the semantic of the elements of the environment through the services they offer. Our model of representation allows us to deduce in an unified manner the quality of service (QoS) provided by an object type of environment. This will be used for decision support of the agents. Our goal is to allow agents to make the best choice among all object types in the environment that enable them to achieve their action. To do this, we proposed a generic level in the ontology to represent the definition of concepts that allow us to make our calculation of QoS. The semantic of the environment is used at key moments in the evolution of agents (during the planning and execution of the plan) to accompany the agent in these behaviors by allowing it to react to what happens in its environment in a consistent manner and opportunistic.

We have implemented our model in the simulation platform project where we got the first results. The numerical evaluation of the results is not the purpose of this article but we plan to evaluate our model on its performance especially for a large number of heterogeneous elements of the environment and a large number of agents.

In the near future, we are considering the addition of a fourth parameter to assess the QoS that defines the availability of the element of environment. As it is now, the agents observe the availability of an object in the environment when they can see it. But this can be avoided by taking into account knowledge of the environment that will be used to filter out inconsistent results (eg, the banking services offered by the bank are unavailable after 6pm).

Fig. 1 :

 1 Fig. 1: System architecture: interactions between semantic module representation of the VE and the decision-making module of the agents.

Fig. 2 :

 2 Fig. 2: Representation model of the environment: Ontology of services

Fig. 3 :

 3 Fig. 3: General concepts of the ontology of services.

Fig. 5 :

 5 Fig. 5: Screenshot of the Terra Dynamica simulator.

http://www.terradynamica.com/

http://protege.stanford.edu/

http://www.w3.org/TR/rdf-sparql-query/

Acknowledgment

This research received support from the TerraDynamica Project (FUI8) funded by the City of Paris, the Local Councils of Val d'Oise, Seine-Saint-Denis, Yvelines, the Regional Councils of Ile de France and Aquitaine and the French Ministry of Economy, Finances and Industry, Directorate for Competitiveness of Industry and Services.