Introduction

An ontology is commonly defined as a specification of the conceptualisation of a particular domain. It fixes the vocabulary used by knowledge engineers to denote concepts and their relations, and it constrains the interpretation of this vocabulary to the meaning originally intended by knowledge engineers. As such, ontologies have been widely adopted also in multi-agent systems. Ontology matching is commonly defined as the process that computes the semantic relationships between entities of separate ontologies. With the proliferation of ontologies used in multi-agent systems caused by different conceptualisations of even the same domain -and their subsequent specification using varying terminology-ontology matching is now seen as a necessary technology to achieve semantic alignment and to enable interoperability of separately engineered knowledge-based agents [5,11].

Until recently, most ontology matching mechanisms developed so far have taken a classical functional approach to the semantic heterogeneity problem, in which ontology matching is seen as a process taking two or more ontologies as input and producing a semantic alignment of ontological entities as output [3]. Furthermore, matching often has been carried out at design-time, before integrating knowledge-based agents or making them interoperate. This might have been successful for clearly delimited and stable domains but is untenable and even undesirable for the kind of applications that are currently deployed on the Web. Webservice composition, multi-agent communication and peer-to-peer information sharing are all of a highly distributed, dynamic and open-ended nature, and they require ontology matching to be performed during run-time. In addition, one can imagine many situations in which ontologies are not even open for inspection (e.g., when they are based on commercially confidential information).

Certainly, there exist efforts to efficiently match ontological entities at run-time, taking only those ontology fragment that are necessary for the task at hand [10,13,9,8]. However, the techniques used by these systems to establish the semantic relationships between ontological entities, even though applied at run-time, they still exploit a priori defined concept taxonomies as they are represented in the graph-based structures of the ontologies to be matched, use previously existing external sources such as thesauri (e.g. WordNet) and upper-level ontologies [7], or resort to additional background knowledge repositories or shared instances.

We claim that semantic alignment is ultimately relative to the particular situation in which it is carried out and that this situation should be made explicit and brought into the ontology matching mechanism. Even two systems with identical conceptualisation capabilities and using exactly the same vocabulary to specify their respective conceptualisations may fail to interoperate because of their differing perception of the domain. Imagine a situation in which two agents are facing each other on a checker board. Agent A 1 may conceptualise a figure on the board as situated on the "left", while agent A 2 may conceptualise the same figure as situated on the "right". Although the conceptualisation of "left" and "right" is done in exactly in the same manner by both agents, they still will need to align their respective vocabularies if they want to successfully communicate to each other actions that move figures on the checker board. Their semantic alignment, however, will only be valid in the scope of their communication within this particular situation or environment. The same agents situated differently may lead to a different alignment.

This scenario is reminiscent to those in which a group of distributed agents adapt to form an ontology and a shared lexicon in an emergent, bottom-up manner, with only local interactions and no central control authority [12]. This sort of self-organised emergence of shared meaning is namely ultimately grounded on the physical interaction of agents with the environment. In this paper, however, we address the case in which agents are already endowed with a top-down engineered ontology (it can even be the same one), which they do not adapt or refine, but for which they want to find the semantic relationships with separate ontologies of other agents on the grounds of their communication within a specific situation. In particular, we provide a formal model that formalises situated semantic alignment as a sequence of information-channel refinements in the sense of Barwise and Seligman's theory of information flow [1]. This theory is particularly useful for our endeavour because it models the flow of information occurring in distributed systems due to the particular situations -or tokens-that carry information. 1 Analogously, the semantic alignment that will allow information to flow ultimately will be carried by the particular situation agents are acting in. We shall therefore consider a scenario with two or more agents situated in an environment. Each agent will have its own viewpoint of the environment so that, if the environment is in a concrete state, both agents may have different perceptions of this state. Because of these differences there may be a mismatch in the meaning of the syntactic entities by which agents describe their perceptions (and which constitute the agents' respective ontologies). We state that these syntactic entities can be related according to the intrinsic semantics provided by the existing relationship between the agents' viewpoint of the environment. The existence of this relationship is precisely justified by the fact that the agents are situated and observe the same environment.

Semantic Alignment in an Environment

The Information Channel linking Agent Perspectives

Let us consider two agents A 1 and A 2 situated in an environment E. 2 We associate a numerable set S of states to E and, at any given instant, we suppose E to be in one of these states. We further assume that each agent is able to observe the environment and has its own perception of it. This ability is faithfully captured by a surjective function see i : S → P i , where i ∈ {1, 2}. According to Channel Theory, information is only viable where there is a systematic way of classifying some range of things as being this way or that. This idea is captured in the notion of classification:

Definition 1 ([1]) A classification is a tuple A = tok(A), typ(A), |= A where tok(A) is a set of tokens, typ(

A) is a set of types and |= A is a binary relation between tok(A) and typ(A). If a |= A α then a is said to be of type α.

For each agent A i , i ∈ {1, 2}, we consider a classification A i that models A i 's viewpoint of E. First, tok(A i ) is composed of A i 's perceptions of E states, that is, tok(A i ) = P i . Second, typ(A i ) comprises the syntactic entities by which A i describes its perceptions, the ones constituting the ontology of A i . Finally, |= Ai synthesizes how A i relates its perceptions with these syntactic entities. Now, in order to associate the environment E with a classification E we choose the power classification of S as E. which is the classification whose set of types is 2 S , whose tokens are the elements of S, and for which a is of type α if a ∈ α. The reason for taking the power classification is because, in general, there is no global conceptualisation of the environment and hence there are no sytactic entities that may play the role of types for E. However, the set of types of the power classification includes all possible token configurations potentially described by types. Thus tok(E) = S, typ(E) = 2 S and e |= E ε iff e ∈ ε.

In Channel Theory, the information flow between the components of a distributed system is modelled in terms of a channel. The relationships between the components are expressed via infomorphisms which provide a way of moving information between them:

Definition 2 ([1]) An infomorphism f : A → B from A to B is a contravariant pair of functions f = f , f

, where f : typ(A) → typ(B) and f : tok(B) → tok(A), satisfying the following fundamental property:

f (b) |= A α iff b |= B f (α)

for each token b ∈ tok(B) and each type α ∈ typ(A). 3We omit the superscripts of informorphisms if no confusion arises. Types are usually denoted by greek letters and tokens by latin letters so f (α) ≡ f (α) and f (a) ≡ f (a).

Definition 3 ([1]) A channel C consists of two infomorphisms {f i : A i → C} i∈{1,2}

with a common codomain C, called the core of C. The tokens of C are called connections and a connection c is said to connect the tokens f1 (c) and f2 (c).

4 typ(C) typ(A 1 ) f1 9 9 s s s s s s s s s typ(A 2 ) f2 e e K K K K K K K K K tok(C) |= C f1 y y s s s s s s s s s f2 % % K K K K K K K K K tok(A 1 ) |= A 1 tok(A 2 ) |= A 2

The information flow of our scenario is accurately described by the channel E = {f i : A i → E} i∈{1,2} defined as follows:

• fi (α) = {e ∈ tok(E) | see i (e) |= Ai α} for each α ∈ typ(E),

• fi (e) = see i (e) for each e ∈ tok(E),

where i ∈ {1, 2}. The fundamental property of the infomorphisms is fulfilled indeed:

fi (e) |= Ai α iff see i (e) |= Ai α {by definition of fi } iff e ∈ fi (α) {by definition of fi } iff e |= E fi (α) {by definition of |= E }

In this way, E is the core of the channel E and a state e ∈ tok(E) connects the agents' perceptions f1 (e) and f2 (e).

E A 1 f1 > > } } } } } } } } A 2 f2 ÀA A A A A A A

Example. This example is taken from [2] and we will resort to it throughout the paper. There are two observers, M r.1 and M r.2, each having a partial viewpoint of a box. This box consists of six sectors and each sector can enclose a ball. The box is "magic" because observers are not able to distinguish the depth inside it. Figure 1 shows the scenario we are describing and illustrates schematically what M r.1 and M r.2 can observe. Intuitively, the state 1 0 1 0 0 0 , for instance, means that there are only two balls in the box, one in the left up sector and another in the left centered sector. Notice that M r.1 sees a ball on the left if there is a ball in at least one of the sectors of the left column of the box and sees a ball on the right provided that there is ball in at least one of the sectors of the right column. Then M r.1's perceptions of the states of E can be represented as two-dimensional binary vectors, and the function see 1 can be defined formally as follows: where e ∈ S. The function see 2 can be defined analogously on three-dimensional binary vectors as representations of M r.2's perceptions. Note that M r.1 has the notions of a ball being on the left or on the right and so has M r.2, but this last one has also the notion of a ball being in the center. After these considerations, A 1 is defined by:

see 1 (e) =              (0 0) if e = 0 0 0 0 0 0 (1• tok(A 1 ) = (1 1), (1 0), (0 1), (0 0) • typ(A 1 ) = {left, right} • (v 1 v 2 ) |= A1 left iff v 1 = 1 (v 1 v 2 ) |= A1 right iff v 2 = 1

On the other hand, A 2 is defined by:

• tok(A 2 ) = (1 1 1), (1 1 0), (1 0 1), (0 1 1), (1 0 0), (0 1 0), (0 0 1), (0 0 0)

• typ(A 2 ) = {left, center, right} • (v 1 v 2 v 3 ) |= A2 left iff v 1 = 1 (v 1 v 2 v 3 ) |= A2 center iff v 2 = 1 (v 1 v 2 v 3 ) |= A2 right iff v 3 = 1

Finally, a channel E = {f i : A i → E} i∈{1,2} as defined above explains the information flow of this scenario.

The Logic of the Semantic Alignment

In the previous subsection, we have shown how channel E explains the information flow of our scenario. Now, we want to relate the agents' syntactic entities, i.e., the agents' types, and obtain meaningful relationships justified by E.

In Channel Theory, the sum operation gives us a way of putting the two components of a channel C = {f i : A i → C} i∈{1,2} together into a single classification A 1 + A 2 (see Definition 4), and the infomorphisms together into a single infomorphism f = f 1 + f 2 (see Proposition 1).

Definition 4 ([1]

) Let A 1 and A 2 be two classifications. The sum of A 1 and A 2 denoted by

A 1 + A 2 is the classification with tok(A 1 + A 2 ) = tok(A 1 ) × tok(A 2 ) = { a, b | a ∈ tok(A 1 ) and b ∈ tok(A 2 )}, typ(A 1 + A 2 ) = typ(A 1 ) typ(A 2 ) = { i, γ | i = 1 and γ ∈ typ(A 1 ) or i = 2 and γ ∈ typ(A 2 )} and relation |= A1+A2 defined by: a, b |= A1+A2 1, α if a |= A1 α a, b |= A1+A2 2, β if b |= A2 β

There exist two infomorphisms σ 1 : We just give the definition of f (see [1] for the rest of the proof): on types,

A 1 → A 1 + A 2 and σ 2 : A 2 → A 1 + A 2 definedf ( 1, α ) = f 1 (α) and f ( 2, β ) = f 2 (β); on tokens, f (c) = f 1 (c), f 2 (c) .

Note that typ(A 1 + A 2 ) is the disjoint union of typ(A 1 ) and typ(A 2 ). We attach importance to take the disjoint union because A 1 and A 2 could use some identical types in order to describe their perceptions of E (for instance, in the Magic Box example, left and right are both M r.1's types and M r.2's types). Therefore, A 1 + A 2 is the place where we should look for relationships between agents' types. Moreover, as we will see f = f 1 + f 2 is of use to find meaningful relationships justified by E.

Channel Theory provides a way to make these relationships explicit in a logical fashion by means of "theories" and "local logics":

Definition 5 ([1]) Given a set Σ, a sequent of Σ is a pair Γ, ∆ of subsets of Σ. A binary relation between subsets of Σ is called a consequence relation on Σ. A theory T is a pair Σ, where is a consequence relation on Σ. A sequent Γ, ∆ of Σ for which Γ ∆ is called a constraint of the theory T .

When it comes to writing constraints of a theory T = Σ, , we will use the usual notational conventions. For example, we write α β, γ instead of {α} {β, γ} and Γ, Γ ∆, α instead of Γ∪Γ ∆∪{α}.

A theory is regular if it satisfies the properties Identity, Weakening and Global Cut (see [1]). Regularity refers to the purely structural properties that any theory must satisfy. From here on, all the theories considered are regular. Every classification generates a theory in a natural way: Definition 6 ([1]) Let A be a classification. A token a ∈ tok(A) satisfies a sequent Γ, ∆ of typ(A) provided that if a is of every type in Γ then it is of some type in ∆. The theory generated by A, written T h(A), is the theory typ(A), A where Γ A ∆ if every token in A satisfies Γ, ∆ .

The notion of local logic puts a classification and a theory together but with an important added twist. In order to model reasonable but unsound inferences, the notion of' "normal token" is introduced.

Definition 7 ([1])

A local logic L is a tuple tok(L), typ(L), |= L , L , N L where:

1. tok(L), typ(L), |= L is a classification denoted by Cla(L), 2. typ(L), L is a regular theory denoted by T h(L), 3. N L is a subset of tok(L), called the normal tokens of L, which satisfy all the constraints of T h(L).

Definition 8 ([1])

A local logic L is sound if every token in Cla(L) is normal, that is, N L = tok(L). L is complete if every sequent of typ(L) satisfied by every normal token is a constraint of T h(L).

Just like with theories, a classification generates a local logic in a natural way: Definition 9 ([1]) Given a classification A, the local logic generated by A, written Log(A), is the local logic on A, i.e., Cla(Log(A)) = A, such that T h(Log(A)) = T h(A) and all its tokens are normal, i.e., N Log(A) = tok(A).

The local logic generated by a classification is sound and complete. Furthermore, given a classification A and a local logic L on A, L is sound and complete if and only if L = Log(A) (see [1]). The main notion of Channel Theory is the notion of "distributed logic":

Definition 10 ([1]) Let f : A → B be an infomorphism. Given a local logic L on B, the inverse image of L under f , denoted f −1 [L], is the local logic on A with Γ f −1 [L] ∆ if f (Γ) L f (∆) and N f −1 [L] = {a ∈ tok(A) | a = f (b) for some b ∈ N L }. Given a channel C = {f i : A i → C} i∈{1,2} and a local logic L on C, the distributed logic of C generated by L, written DLog C (L), is the logic f −1 [L] where f = f 1 + f 2 .

DLog C (L) represents the reasoning about relations among the components of the channel C justified by the logic L on the core. Consider L = Log(C). We denote DLog C (Log(C)) by Log(C). Log(C) then captures in a logical fashion the information flow inherent in the channel. Now, let us return to our scenario modeled by E. Log(E) explains the relationships between the agents' viewpoints of the environment. On the one hand, T h(Log(E)) contains the most meaningful relationships between agents' types according to the channel E. On the other hand, N Log(E) contains those pairs of agents' perceptions connected together by the environment state of which they come from. [1]):

E A 1 f1 : : u u u u u u u u u u σ1 / / A 1 + A 2 f O O A 2 f2 d d I I I I I I I I I I σ2 o o Log(E) is complete since Log(E) is complete but it is not necessarily sound because although Log(E) is sound, f = f 1 + f 2 is not token surjective in general (seeN Log(E) = { f1 (e), f2 (e) | e ∈ tok(E)} ⊆ tok(A 1 + A 2 ) If Log(E) is also sound then Log(E) = Log(A 1 + A 2 )

, as we comment above. It means that there is no meaningful compatibility between agents' viewpoints of the environment according to E. It is just the fact that Log(E) is unsound what allows a meaningful compatibility between the agents' viewpoints. This compatibility relation is expressed at the type level in terms of constraints by T h(Log(E)) and at the token level in terms of pairs of tokens by N Log(E) .

Example. Following the previous example, Log(E) includes among its constraints:

1, left Log(E) 2, left , 2, center , 2, right 1, right Log(E) 2, left , 2, center , 2, right

Let us check the first constraint (the second one can be verified in a similar way). We have to prove:

f ( 1, left ) Log(E) f ( 2, left ), f ( 2, center ), f ( 2, right )

Let e = (e ij ) ∈ tok(E) and assume that e |= E f ( 1, left ). Then e ∈ f ( 1, left ), that is, see 1 (e) |= A1 left. Therefore e 11 + e 21 + e 31 ≥ 1 and we can assure that there exists i ∈ {1, 2, 3} such that e i1 = 1. Hence e i1 + e i2 ≥ 1.

If i = 3 then e |= E f ( 2, left ), if i = 2 then e |= E f ( 2, center ) and if i = 1 then e |= E f ( 2, right ).

The necessary and sufficient conditions for a token a 1 , a 2 of A 1 + A 2 being normal are the following:

if a 1 = (0 0) then a 2 = (0 0 0) if a 2 = (0 0 0) then a 1 = (0 0)

Aligning Agent Perspectives through Communication

We have stated that T h(Log(E)) contains the most meaningful relations between agents' types. The problem is that neither agent can make use of this theory because they do not know the channel E completely. We present a method by which agents obtain approximations to T h(Log(E)). These approximations gradually become more reliable as the method is applied.

A 1 and A 2 communicate by exchanging information about their perceptions of the environment states. This information is expressed in terms of their own classification relations. Specifically, if E is in a concrete state e, we assume that agents can convey to each other which types are satisfied by their respective perceptions of e and which are not. This exchange generates a channel C = {f i : A i → C} i∈{1,2} . Furthermore, T h(C) provides the logical relationships between the agents' types justified by the fact that agents have observed e. If E turns to another state e and agents proceed as before, another channel

C = {f i : A i → C } i∈{1,2}

gives account of the new situation. The significant point is that C refines C (see Definition 11). Theorem 1 ensures that the refined channel involves more reliable information.

The communication ends when agents have observed all the environment states. Again this situation can be modeled by a channel, call it

C * = {f * i : A i → C * } i∈{1,2} . Theorem 2 states that T h(C * ) = T h(Log(E)). Definition 11 ([1]) Let C = {f i : A i → C} i∈{1,2} and C = {f i : A i → C } i∈{1,2} be two information channels with the same component classifications A 1 and A 2 . A refinement infomorphism r from C to C is an infomorphism r : C → C such that for each i ∈ {1, 2}, f i = r • f i (i.e., fi = r • f i and fi = f i • ř). The channel C is a refinement of C if there exists a refinement infomorphism r from C to C.

Theorem 1 asserts that the more refined channel gives more reliable information. Although its theory has less constraints, it has more normal tokens to which they apply.

Theorem 1 Let C = {f i : A i → C} i∈{1,2} and C = {f i : A i → C } i∈{1,2} be two channels. If C is a refinement of C then: 1. T h(Log(C )) ⊆ T h(Log(C)) 2. N Log(C ) ⊇ N Log(C) PROOF: Since C is a refinement of C then there exists a refinement infomorphism r from C to C. Let us write A = A 1 + A 2 , f = f 1 + f 2 and f = f 1 + f 2 .

1. Let Γ and ∆ be subsets of typ(A) and assume that

Γ Log(C ) ∆, which means f [Γ] C f [∆]. We have to prove Γ Log(C) ∆, or equivalently, f [Γ] C f [∆].

We proceed by reductio ad absurdum. Suppose c ∈ tok(C) does not satisfy the sequent

f [Γ], f [∆] . Then c |= C f (γ) for all γ ∈ Γ and c |= C f (δ) for all δ ∈ ∆.

Let us choose an arbitrary γ ∈ Γ. We have that γ = i, α for some

α ∈ typ(A i ) and i ∈ {1, 2}. Thus f (γ) = f ( i, α ) = fi (α) = r • f i (α) = r( f i (α)). Therefore: c |= C f (γ) iff c |= C r( f i (α)) iff ř(c) |= D f i (α) iff ř(c) |= D f ( i, α ) iff ř(c) |= D f (γ) Consequently, ř(c) |= C f (γ) for all γ ∈ Γ. Since f [Γ] C f [∆] then there exists δ * ∈ ∆ such that ř(c) |= C f (δ * ).

A sequence of equivalences similar to the above one justifies c |= C f (δ * ), contradicting that c is a counterexample to f [Γ], f [∆] . Hence Γ Log(C) ∆ as we wanted to prove.

2. Let a 1 , a 2 ∈ tok(A) and assume a 1 , a 2 ∈ N Log(C) . Therefore, there exists c token in C such that a 1 , a 2 = f (c). Then we have

a i = fi (c) = f i • ř(c) = f i (ř(c))

, for i ∈ {1, 2}. Hence a 1 , a 2 = f (ř(c)) and a 1 , a 2 ∈ N Log(C ) . Consequently, N Log(C ) ⊇ N Log(C) which concludes the proof.

Refining the Semantic Alignment

We assume that typ(A i ) is finite for i ∈ {1, 2} and S is infinite numerable, though the finite case can be treated in a similar form. We also choose an infinite numerable set of symbols {c n | n ∈ N} 6 .

Agent communication starts from the observation of E. Let us suppose that E is in state e 1 ∈ S = tok(E). A 1 's perception of e 1 is f 1 (e 1 ) and A 2 's perception of e 1 is f 2 (e 1 ). We take for granted that A 1 can communicate A 2 those properties that are and are not satisfied by f 1 (e 1 ) according to its classification A 1 . So can A 2 do. Since both typ(A 1 ) and typ(A 2 ) are finite, this process eventually finishes. After this communication a channel

C 1 = {f 1 i : A i → C 1 } i=1,2 arises. C 1 A 1 f 1 1 = = { { { { { { { { A 2 f 1 2 a a C C C C C C C C

On the one hand, C 1 is defined by: tok(C 1 ) = {c 1 }, typ(C 1 ) = typ(A 1 + A 2 ) and c 1 |= C 1 i, α if f i (e 1 ) |= Ai α, for α ∈ typ(A i ) and i ∈ {1, 2}. On the other hand, f 1 i (α) = i, α and f 1 i (c 1 ) = f i (e 1 ), for α ∈ typ(A i ) and i ∈ {1, 2}. Clearly, f 1 1 and f 1 2 are infomorphims. Note in this case both agents know C 1 . Hence they can compute separately T h(C 1 ) = typ(C 1 ), C 1 . This theory represents the logical relationships between the agents' types justified by the fact that agents have observed e 1 .

Example. Assume that the environment is in state e

1 =   1 0 1 0 0 0   . A 1 's perception of e 1 is

(1 0) and A 2 's perception of e 1 is (0 1 1). T h(C 1 ) includes among its constraints:

1, left C 1 2, center and 1, left C 1 2, right

Now, let us assume that E turns to a new state e 2 . Agents can proceed as above exchanging this time information about their perceptions of e 2 . Therefore, another channel

C 2 = {f 2 i : A i → C 2 } i∈{1,2} comes up. First of all, C 2 is defined by: tok(C 2 ) = {c 1 , c 2 }, typ(C 2 ) = typ(A 1 + A 2 ) and for 1 ≤ k ≤ 2, c k |= C 2 i, α if f i (e k ) |= Ai α, for all α ∈ typ(A i ) and i ∈ {1, 2}. Second, f 2 i (α) = i, α and f 2 i (c k ) = f i (e k ) again for 1 ≤ k ≤ 2, α ∈ typ(A i ) and i ∈ {1, 2}. f 2 1 and f 2 2

are infomorphims by definition. The theory T h(C 2 ) = typ(C 2 ), C 2 represents the logical relationships between the agents' types justified by the fact that agents have observed e 1 and e 2 . The significant point is that

C 2 is a refinement of C 1 : C 2 f 1 A 1 f 2 1 = = | | | | | | | | f 1 1 / / C 1 A 2 f 2 2 a a B B B B B B B B f 1 2 o o

It is easy to prove that f 1 defined as the identity function on types and the inclusion function on tokens is a refinement infomorphism. By Theorem 1, C 2 constraints are more reliable than C 1 constraints.

Example. Let us assume that the environment changes to the state e 2 = 0 0 0 1 1 0 . Then A 1 's perception of e 2 is (1 1) and A 2 's perception of e 2 is (1 1 0). In this case:

1, left C 2 2, center but 1, left C 2 2, right

In the general situation, once the states e 1 , e 2 , . . . , e n have been observed and a new state e n+1 appears, the channel

C n+1 = {f n+1 i : A i → C n+1 } i∈{1,2} informs about agents communication up to this moment. First, tok(C n+1 ) = {c 1 , c 2 , . . . , c n+1 }, typ(C n+1 ) = typ(A 1 + A 2 ) and for each 1 ≤ k ≤ n + 1, c k |= C n+1 i, α if f i (e k ) |= Ai α, for all α ∈ typ(A i ) and i ∈ {1, 2}. Second, f n+1 i (α) = i, α and f n+1 i (c k ) = fi (e k ) for 1 ≤ k ≤ n + 1, α ∈ typ(A i ) and i ∈ {1, 2}. Clearly, f n+1 1 and f n+1 2 are infomorphims. The theory T h(C n+1 ) = typ(C n+1

), C n+1 represents the logical relationships between the agents' types justified by the fact that agents have observed e 1 , . . . , e n , e n+1 . Also C n+1 is a refinement of C n . f n defined as the identity function on types and the inclusion function on tokens is a refinement infomorphism. By Theorem 1, C n+1 constraints are more reliable than C n constraints.

Remember we have assumed that S is infinite numerable. It is therefore unpractical to let communication finish when all environment states have been observed by A 1 and A 2 . At that point, the family of channels {C n } n∈N would inform of all the communication stages. It is therefore up to the agents to decide when to stop communicating should a good enough approximation have been reached for the purposes of their respective tasks. But the study of possible termination criteria is outside the scope of this paper and left for future work. From a theoretical point of view, however, we can consider the channel C * = {f i : A i → C * } i∈{1,2} which informs of the end of the communication after observing all environment states. C * is defined as follows: tok(C * ) = {c n | n ∈ N}, typ(C * ) = typ(A 1 + A 2 ) and for n ∈ N, c n |= C * i, α if f i (e n ) |= Ai α, for all α ∈ typ(A i ) and i ∈ {1, 2}. In addition, f * i (α) = i, α and f * i (c n ) = f i (e n ) for n ∈ N, α ∈ typ(A i ) and i ∈ {1, 2}. By definition, f * 1 and f * 2 are infomorphims. Theorem 2 below is the cornerstone of the theory exposed in this paper. In short, it ensures that at each communication stage agents obtain a theory that approximates the most meaningful relationships between their types: Theorem 2 The following statements hold:

1. For all n ∈ N, C * is a refinement of C n .

T h(Log(E)) = T h(C * ).

PROOF:

1. It is easy to prove that for each n ∈ N, g n defined as the identity function on types and the inclusion function on tokens is a refinement infomorphism from C * to C n .

2. It follows directly from:

c n |= C * i, α iff fi (e n ) |= Ai α {by definition of |= C * } iff e n |= E fi (α)

{because f i is infomorphim} iff e n |= E f ( i, α ) {by definition of f }

Conclusions

In this paper we have exposed a formal model of semantic alignment as a sequence of information-channel refinements that are relative to the particular states of the environment in which two agents communicate and align their respective conceptualisations of these states. Before us, Kent [6] and Kalfoglou and Schorlemmer [4,10] have applied Channel Theory to formalise semantic alignment using also Barwise and Seligman's insight to focus on tokens as the enablers of information flow. Their approach to semantic alignment, however, like most ontology matching mechanisms developed to date (regardless of whether they follow a functional, design-time-based approach, or an interaction-based, run-time-based approach), still defines semantic alignment in terms of a priori design decisions such as the concept taxonomy of the ontologies or the external sources brought into the alignment process. Instead the model we have presented in this paper makes explicit the particular states of the environment in which agents are situated and are attempting to gradually align their ontological entities. In the future we plan to further refine the model presented here (e.g., to include pragmatic issues such as termination criteria for the alignment process) and to devise concrete ontology negotiation protocols based on this model that agents may be able to enact.