Boris Lesner
email: boris.lesner@unicaen.fr

Bruno Zanuttini
email: bruno.zanuttini@unicaen.fr

Handling Ambiguous Effects in Action Learning

Keywords: stochastic action, maximum likelihood, factored MDP

We study the problem of learning stochastic actions in propositional, factored environments, and precisely the problem of identifying STRIPS-like effects from transitions in which they are ambiguous. We give an unbiased, maximum likelihood approach, and show that maximally likely actions can be computed efficiently from observations. We also discuss how this study can be used to extend an RL approach for actions with independent effects to one for actions with correlated effects.

Introduction

Learning how one's actions affect the environment is a central issue in Artificial Intelligence, and especially in Reinforcement Learning (RL) problems. This task is far from being trivial because of many factors. In particular, actions may affect the environment differently depending on the state where they are taken. They may also be stochastic, that is, have different possible outcomes, each of which occurs with some probability each time we take the action.

A third difficulty, which is our focus in this article, is that the effects of an action are typically ambiguous in some states. Precisely, if some fact is true in the state where we took the action and in the resulting state, then it is ambiguous whether this fact was set to true by the action, or was simply unaffected by it (and persisted true). This of course makes no difference in the starting state in question, but may matter a lot if we want to generalize the corresponding observation to other states, where the fact in question is not true. To give a concrete example, assume that you want to learn the effects of the action "play the National Lottery" by observing your neighbours. If one of them suddenly has an expensive car parked in front of his house, then he must have won (effect "become rich" occurred). On the other hand, assume another one always has had an expensive car parked in front of his huge villa. Then you will see no change when he wins, nor when he looses. Technically, for this neighbour (state) both winning and losing (effects) provoke no change (self-transition). Then, this ambiguity must be resolved for generalizing from a few "poor" neighbours and a few "rich" neighbours to a generic player.

We address here this specific problem for environments and actions described in factored form over propositional variables, with STRIPS-like effects. We provide an in-depth study of ambiguity and of maximum likelihood approaches to learning in the presence of ambiguous effects. Though the obvious motivation for this work is RL, we place our study in a general learning context, where some transitions between states are observed, from which the effects of the (unique) stochastic action which provoked them must be learnt together with their probabilities. In this setting, we propose a linear programming approach for computing the most likely effect distributions, and use it to propose a generalization of SLF-Rmax [START_REF] Strehl | Efficient structure learning in factored-state MDPs[END_REF] to deal with ambiguous effects.

Ambiguous effects are discussed in several works [13, in particular], and implicitly dealt with in approaches to relational RL [START_REF] Džeroski | Relational reinforcement learning[END_REF][START_REF] Pasula | Learning symbolic models of stochastic domains[END_REF][START_REF] Rodrigues | Incremental learning of relational action rules[END_REF]. Still, to the best of our knowledge they have never been investigated in depth. For instance, propositional actions are often learnt as dynamic bayesian networks (DBNs) which assume independent effects on variables [START_REF] Kearns | Efficient reinforcement learning in factored MDPs[END_REF][START_REF] Degris | Learning the structure of factored Markov Decision Processes in reinforcement learning problems[END_REF][START_REF] Strehl | Efficient structure learning in factored-state MDPs[END_REF]. Then ambiguity is bypassed by learning the effects on x independently in states satisfying x and x. But such DBNs (without synchronic arcs) cannot represent effect distributions as simple as {(x 1 x 2 , .5), (∅, .5)}, while STRIPS-like descriptions, as we study here, are fully expressive (see the discussion by Boutilier et al. [START_REF] Boutilier | Decision-theoretic planning: Structural assumptions and computational leverage[END_REF]).

Closest to ours is the work by Walsh et al. [START_REF] Walsh | Exploring compact reinforcementlearning representations with linear regression[END_REF]. Our work can in fact be seen as using their linear regression approach (for known effects) with all 3 n possible effects, but introducing new techniques for reducing the exponential number of unknowns and dealing with ambiguity.

Section 2 introduces our formal setting. In Sections 3-5 we study the problem of computing most likely actions given observed transitions. We give an application to RL and conditional actions in Section 6, and conclude in Section 7.

Formal setting

We consider propositional environments, described through n Boolean variables x 1 , . . . , x n . A state s is an assignment to x 1 , . . . , x n . There is a hidden stochastic action a, which can be described as a probability distribution on a finite set of effects (we identify the action and the distribution to each other). We write {(p i , e i ) | i = 1, . . . , ℓ} (with i p i = 1) for this distribution, meaning that each time a is taken, exactly one of the effects e i occurs, as sampled i.i.d. according to the p i 's. Effects are STRIPS-like, that is, each effect is a consistent term on x 1 , . . . , x n . When a is taken in some state s and effect e i occurs, the resulting state s ′ is obtained from s by changing all affected variables to their value in e i . We write s ′ = apply(s, e i ). For convenience, states and terms are also seen as sets of literals, and 3 X denotes the set of all terms/effects.

For instance, for n = 3, s = 000 and s ′ = 010 are two states, and e 1 = x 1 x 2 , e 2 = x 3 are two effects. The distribution {(e 1 , .7), (e 2 , .2), (∅, .1)} defines an action a. Each time a is taken in a state, e 1 occurs (with probability .7), or e 2 occurs (.2), or nothing occurs (.1). If effect e 1 occurs in state s above, the resulting state is s ′ , while effects e 2 and ∅ provoke a transition from s to itself. Ambiguous Effects and Compact Representation. Ambiguity is a consequence of the following straightforward result.

Proposition 1. Let s, s ′ be two states. Then the effects e ∈ 3 X which satisfy apply(s, e) = s ′ are exactly those for which s ′ \ s ⊆ e ⊆ s ′ holds.

It follows that the effects which may have occurred when a transition from s to s ′ is observed, can be compactly represented, as the set interval [s ′ \ s, s ′ ]. As an example, the effects which provoke a transition from s = 000 to s ′ = 010 are x 2 , x 1 x 2 , x 2 x 3 , and x 1 x 2 x 3 . That is, we are sure that the (atomic) effect x 2 occurred, but any other literal in s ′ may have been set to true, or left true, by the action. These effects are compactly represented by the set interval [x

2 , x 1 x 2 x 3 ] ∩ [∅, x 1 x 2 x 3 ] is [x 2 , x 2 x 3 ], and [x 2 , x 1 x 2 x 3 ] ∩ [x 2 x 3 , x 1 x 2 x 3 ] is empty, since x 2 x 2 x 3 ⊆ x 2
x 3 holds (here, because x 2 and x 2 x 3 are inconsistent together).

Sampled Effects and Induced Observations. We consider an agent which must learn the effect distribution of a unique action a, from transitions provoked by this action in the environment. Remember that (except in Section 6) we assume a to be unconditional, i.e., to have the same effect distribution D in all states s.

For generality, we assume nothing about the states s in which transitions are observed; what we only require is that the environment samples the effects fairly to D. This setting arises naturally in many contexts. For instance, a robot may train in the factory, so as to learn accurate models of its actuators, but the situations s which it can experiment may be restricted by the facilities in the factory. In an RL setting, the agent may lose control on the visited states if other agents or exogenous events can intervene at any moment in the environment.

Formally, the examples sampled by the environment form a multiset of pairs state/effect, of the form T = {(s i , e i ) | i = 1, . . . , m}, and the learner sees the corresponding multiset of transitions between states {(s i , s ′ i ) | i = 1, . . . , m} (with s ′ i = apply(s i , e i )). For simplicity of presentation, we define the observations induced by T to be the multiset of intervals

O T = {[s ′ i \ s i , s ′ i ] | i = 1, . . . ,
m}, and assume that this is the only data available to the learner. That this information is equivalent to the multiset of transitions is a consequence of Proposition 1, together with the observation that s i can be easily retrieved from s ′ i \ s i and s ′ i . Importantly, observe that e i is always in the set interval [

s ′ i \ s i , s ′ i ].
Example 1. Let D = {(x 1 , .5), (x 1 x 2 , .3), (∅, .2)}, and let T = {(01, x 1 ), (00, x 1 ), (00, ∅), (00, x 1 x 2 ), (01, x 1 )} in which, for instance, the first element corresponds to state s = 01 having been chosen, and effect x 1 having been sampled. The observations induced by T are

O = {[x 1 , x 1 x 2 ], [x 1 , x 1 x 2 ], [∅, x 1 x 2 ], [x 1 , x 1 x 2 ], [x 1 , x 1 x 2 ]} The frequency of an observation o = [s ′ \ s, s ′ ] in O T , written f o,O T (or f o ), is the proportion of indices i such that [s ′ i \ s i , s ′ i ] is precisely o in O T . In Exam- ple 1, f [x1,x1x2] is 1/5 + 1/5 = .4.
Observe that this corresponds in fact to the manifestation of two different effects (but this is hidden to the learner).

Most Likely Actions

We now characterize the maximally likely effect distributions D (i.e., actions)

given observations O = {[s ′ i \ s i , s ′ i ] | i = 1, . . . , m}.
First recall from Bayes rule that the likelihood of D given O satisfies P r(D|O) = P r(D) P r(O|D)/ P r(O). In particular, if all distributions D have the same prior likelihood P r(D), the most likely distribution D given O is the one which maximizes P r(O|D).

Likelihood and Fairness. We first need a few straightforward lemmas. Write O for a multiset of observations induced by states/effects in T , and

D = {(p i , e i ) | i ∈ I}, D ′ = {(p ′ j , e ′ j ) | j ∈ J} for two effect distributions. Moreover, write ||D - D ′ || 1 for the L1-distance between D, D ′ , that is, ||D -D ′ || 1 = e∈3 X |p e -p ′
e |, with p e = p i for e = e i in D and p e = 0 otherwise, and similarly for p ′ e . For instance, the L1-distance from the distribution in Example 1 to the distribution

{(x 1 , .6), (∅, .4)} is (.6 -.5) + (.3 -0) + (.4 -.2) = 0.6. Lemma 1. If for some o ∈ O, there is no i ∈ I with e i ∈ o, then P r(O|D) is 0.
This follows from the fact that when a transition from s to s ′ is observed, the effect which provoked it must be in the interval

[s ′ \ s, s ′ ]. Now write D T = {(e, p e )} for the distribution of effects in T = {(s ′ , e ′ )}, that is, p e is given by p e = |{(s ′ , e ′ ) ∈ T | e ′ = e}| / |T |. Lemma 2. P r(O|D) > P r(O|D ′ ) is equivalent to ||D T -D|| 1 < ||D T -D ′ || 1 .
This follows, e.g., from the following bound [START_REF] Weissman | Inequalities for the l1 deviation of the empirical distribution[END_REF], which extends Chernoff's bound to multivalued random variables:

P r(||D T -D|| 1 ≥ ǫ) ≤ (2 ℓ -2)e -mǫ 2 /2 (1)
where m is the number of samples observed (size of T ) and ℓ is the number of effects (with nonzero probability) in D. Note that other distances could be used. We use L1-distance because approximating the transition probabilities T (•|s, D) in an MDP with respect to it provides guarantees on the resulting value functions, but the infinite norm, for instance, gives similar results [7, "simulation lemma"]). These observations lead us to introduce the following definition.

Definition 1. Let D = {(p i , e i ) | i ∈ I} be an effect distribution. A multiset of observations O is said to be ǫ-fair to D if 1.
for all intervals o ∈ O, there is an i ∈ I with p i = 0 and e i ∈ o, and 2. there is a multiset of states/effects T such that O is induced by T and the distribution of effects in T is at L1-distance at most ǫ to D.

Hence (Lemmas 1-2) the effect distributions D to which O is 0-fair are perfectly likely given O, and otherwise, the smaller ǫ, the more likely D given O.

Clearly enough, a multiset O is always 0-fair to at least one distribution D. Such D can be built from one effect e o in each interval o ∈ O, with the frequency f o as its probability. However, there are in general many such "perfectly likely" distributions. In fact, each possible choice of effects in the construction above leads to a different one. Further, in some given observed interval it may be the case that two different effects provoked the corresponding transitions, increasing still more the number of candidate distributions. Still worse, the different most likely distributions may be arbitrarily distant from each other (hence inducing arbitrarily different planning problems, if learnt actions are used for planning). Summarizing, we have that (with high confidence) O is always ǫ-fair to the hidden effect distribution D which indeed generated it, for some small ǫ. Nevertheless, O can also be ǫ-fair, for some small ǫ, to some distribution which is very different from D. Another way to state this is that fairness gives a lower bound on the distance to the real, hidden D. Anyway, this lower bound is a correct, unbiased measure of likelihood (Lemma 2).

Example 2. Let o 1 = [x 1 , x 1 x 2 ], o 2 = [x 2 , x 1 x 2 ], and O = {o 1 × 5, o 2 × 5} (o 1 , o 2 observed 5 times each). Then O is 0-fair to D 1 = {(x 1 , .5), (x 2 , .5)}, to D 2 = {(x 1 x 2 , 1)}, and to D 3 = {(x 1 , .4), (x 1 x 2 , .3), (x 2 , .3)}. As to the last point, D 3 indeed induces O if x 1 x 2 is
Computing fairness. If some additional constraints have to be satisfied (like accounting for other observations at the same time), in general there will not be any effect distribution to which the observations are 0-fair. Hence we investigate how to compute in general how fair a given multiset of observations is to a given effect distribution.

To that aim, we give an alternative definition of fairness. To understand the construction, observe the following informal statements for a sufficiently large multiset of observations O generated by a distribution D = {(p i , e i ) | i ∈ I}:

if e i induced o ∈ O, then the observed frequency of o should be close to p i , -it is possible that some e i ∈ D with a sufficiently small p i has never been observed, i.e., that O contains no interval o with e i ∈ o, -every o ∈ O must be induced by some effect e i with p i = 0, -if o 1 , o 2 ∈ O intersect, it may be that only one e i ∈ D induced both (in different states s), and then f o1 , f o2 should approximately sum up to p i , -dually, if o ∈ O contains e i , e j , it may be that both participated in inducing o, and then p i , p j should approximately sum up to f o .

Generalizing these observations, we can see that one effect may induce several observed intervals, and dually that one interval may be induced by several effects. We take these possibilities into account by introducing values which we call contributions of effects to intervals, written c e,o , and reflecting how often, among the times when e was sampled, it induced interval o.

We are now ready to characterize ǫ-fairness. The value to be minimized in Proposition 2 is the L1-distance between D and the frequencies of the realizations of effects. A particular combination of c e,o 's indicates a particular hypothesis about which effect provoked each observed transition, and how often. We note that an arbitrary optimal solution (i.e., combination of c e,o 's) of the program is not necessarily a witness of ǫ-fairness, in the sense that it may let some observation o ∈ O be unexplained by any effect e with nonzero probability.

Nevertheless, from such a solution a correct witness can always be straightforwardly retrieved (with the same, optimal value).

Example 4 (continued). Let again

O = {[x 1 , x 1 x 2 ] × 5, [x 2 , x 1 x 2 ]
× 5}, and let D = {(x 1 , 0), (x 2 , .25), (x 1 x 2 , .25), (x 1 , .5)}. Observe that the fairness of O to D cannot be better than 1 (due to a .5-excess on effect x 1 ). Hence the contributions c x1,o1 = .5, c x2,o2 = .25, c x1x2,o2 = .25 are optimal. Nevertheless, they do not respect the constraint that there is an effect e ∈ o 1 with p e > 0 and c e,o1 > 0.

Still, an optimal solution respecting this constraint can be easily retrieved by "redirecting" the contribution of x 1 to o 1 to the effect x 1 x 2 .

Clearly, this program is not practical, since it has exponentially many variables. We will see in Section 5 how to reduce this number in practice.

Variance of Sets of Observations

We now turn to the more general question of how likely it is that several multisets of observations O 1 , . . . , O q are all induced by the same effect distribution D. Naturally, we want to measure this by the radius of a ball centered at D and containing all O i 's. The smaller this radius, the more likely are all O i 's induced by D, and the smaller over all distributions D, the less the "variance" of O i 's.

From the analysis in Section 3 it follows that fairness is the correct (unbiased) measure for defining the radius of such balls. The center of a ball containing all O i 's and with minimal radius is known as the Chebyshev center of the O i 's.

We have however taken care in our definition of fairness that any observed interval is accounted for by at least one effect with nonzero probability. As an unfortunate and rather surprising consequence, the center does not always exist. Still, we define O 1 , . . . , O q to be ǫ-variant (together) if there is an effect distribution D such that for all i = 1, . . . , q, O i is ǫ-fair to D. Clearly, variance inherits from fairness the property of being a correct, unbiased measure (of homogeneity), and the property of underestimating the real (hidden) variance.

Example 5. Let O 1 = {[x 1 ], [x 2 ] × 2, [x 3 ] × 2}, O 2 = {[x 2 ] × 4, [
It is important to note that when restricted to two multisets of observations, variance does not define a distance. Intuitively, this is simply because the witness D 12 for the variance of O 1 , O 2 needs not be the same as the witness D 23 for O 2 , O 3 . In fact, the triangle inequality can even be made "very false". The good news is that variance inherits the linear programming approach from fairness. Indeed, consider the following linear program (built on top of the one for fairness) for computing the variance of O 1 , . . . , O q , as well as a witness distribution D = {(p e , e) | e ∈ 3 X }:

Example 6. Consider the multisets

O 1 = {[x 1 , x 1 x 2 ]}, O 2 = {[x 2 , x 1 x 2 ]}, and O 3 = {[x 2 , x 1 x 2 ]}. Then O 1 , O 2 are 0-variant (using D = {(x 1 x 2 , 1)}),
Variables: p e (∀e ∈ 3 X ) c i e,o (∀i = 1, . . . , q, o ∈ O i , e ∈ o) Minimize: max i=1,...,q e∈3 X |p e -o∈Oi c i e,o | Subject to: p e ≥ 0 (∀e ∈ 3 X ) c i e,o ≥ 0 (∀i = 1, . . . , q, o ∈ O i , e ∈ o) e∈3 X p e = 1 e∈o c i e,o = f o (∀i = 1, . . . , q, o ∈ O i )
As Example 5 shows, the program may compute a (nonattained) infimum value, but this is still sufficient for our application in Section 6.

Proposition 4. The optimal value σ of the above linear program satisfies σ ≤ ǫ if and only if O 1 , . . . , O q are (ǫ + α)-variant for all α > 0.

Restriction to Intersections of Intervals

The linear programming formulations of fairness and variance which we gave involve an exponential number of variables (enumerating all 3 n effects). We now show how to restrict this. The restriction will not give a polynomial bound on the number of variables in general, but it proves useful in practice. The basic idea is to identify to only one (arbitrary) effect all the effects in some intersection of intervals

o 1 ∩ • • • ∩ o q (one per O i ).
Definition 2. Let O 1 , . . . , O q be observations. A maximal intersecting family (MIF) for O 1 , . . . , O q is any maximal multiset of intervals M = {o i1 , . . . , o ir } satisfying (for all j, j ′ = j): [START_REF] Boutilier | Decision-theoretic planning: Structural assumptions and computational leverage[END_REF]

i j = i j ′ , (2) o ij ∈ O ij , and (3) o i1 ∩• • •∩o ir = ∅.
A set of effects E ⊆ 3 X is said to be sufficient for O 1 , . . . , O q if for all MIFs M = {o i1 , . . . , o ir }, there is at least one effect e ∈ E with e

∈ o i1 ∩ • • • ∩ o ir . Example 7. Let o 1 = [x 1 , x 1 x 2 ], o ′ 1 = [x 2 , x 1 x 2 ], o 2 = [∅, x 1 x 2 ], o ′ 2 = [x 1 x 2 ]}, and O 1 = {o 1 , o ′ 1 }, O 2 = {o 2 , o ′ 2 }. The MIFs for O 1 , O 2 are {o 1 , o 2 } (with intersec- tion [x 1 , x 1 x 2 ]), {o ′ 1 , o 2 } (intersection [x 2 , x 1 x 2 ]), and {o ′ 2 } (intersection [x 1 x 2 ]
). Hence, for example, {x 1 , x 2 , x 1 x 2 } and {x 1 x 2 , x 1 x 2 } are sufficient sets of effects.

The proof of the following proposition (omitted) is simple though tedious. Proposition 5. Let O 1 , . . . , O q be multisets of observations, and E be a sufficient set of effects for O 1 , . . . , O q . The program for computing variance has the same optimal value when effect variables p e 's range over e ∈ E (instead of 3 X ).

Given multisets O 1 , O 2 , a sufficient set of effects can be easily computed by [START_REF] Boutilier | Decision-theoretic planning: Structural assumptions and computational leverage[END_REF] intersecting all intervals in O 1 with those in O 2 , yielding a set of intervals O 12 , (2) retaining the ⊂-minimal intervals in (O 1 ∪O 2 ∪O 12 )\{∅}, and (3) choosing one effect in each remaining interval. For a greater number of intervals, Steps (1)-( 2) are applied recursively first. Such computation is very efficient in practice, and indeed generates a small number of effects as compared to 3 n .

Application: Learning Conditions of Actions

We now show how the tools of Sections 3-5 can be applied to learning conditional actions. Precisely, we consider a hidden action a, consisting of formulas c 1 , . . . , c ℓ , each associated with an effect distribution D i . Conditions c i are assumed to partition the state space, so that when a is taken in s, an effect is sampled from D i , where c i is the unique condition satisfied by s. Such actions are known as Probabilistic STRIPS Operators (PSO [START_REF] Kushmerick | An algorithm for probabilistic planning[END_REF]).

When c 1 , . . . , c ℓ are unknown but a has independent effects on the variables, SLF-Rmax [START_REF] Strehl | Efficient structure learning in factored-state MDPs[END_REF] learns a DBN representation with KWIK guarantees [START_REF] Li | Knows what it knows: a framework for self-aware learning[END_REF], provided a bound k on the number of variables used in

c 1 ∪ • • • ∪ c ℓ is known a priori.
We also assume such a known bound k, and build on SLF-Rmax for addressing PSO's. Note that using synchronic arcs, SLF-RMAX could in principle deal with nonindependent (correlated) effects, but the bound k would then depend also on an a priori bound on the amount of correlation (maximum size of an effect). The approach we propose does not suffer from this dependence, and hence is more sample-efficient. The price we pay is that our approach is only heuristic. Basic Principles. SLF-Rmax gathers statistics (observations) about the action behavior in specific families of states (using Rmax-like exploration). Precisely, for each set C of k variables and each term c on C, a multiset of observations O c is gathered in states satisfying c. For instance, for k = 2 and c = x 1 x 3 , O c will contain transitions observed only in states s satisfying x 1 and x 3 . For technical reasons (see below), statistics are also gathered on terms over 2k variables.

The full approach works by first learning the conditions c 1 , . . . , c ℓ of a, then learning the distribution D i for each of them using maximum likelihood. As concerns conditions, define the following property, respective to a given measure of homogeneity µ for multisets of observations (think of our notion of variance). Definition 3. A term c over k variables is said to be an ǫ-likely condition for action a (wrt µ) if µ(O c∧c 1 , . . . , O c∧c K ) ≤ ǫ holds, where c 1 , . . . , c K enumerate all n-k k 2 k terms over k variables disjoint from c.

Example 8. Let n = 3 variables, k = 1 variable in the (hidden) conditions of a, and assume the following transitions (s, s ′ ) have been observed 10 times each:

(000, 000), (110, 111), (011, 000), (101, 101), (111, 111)

We have for instance

O x1x3 = {[x 3 , x 1 x 2 x 3 ] × 10} and O x1x3 = {[∅, x 1 x 2 x 3 ] × 10, [∅, x 1 x 2 x 3 ] × 10}. The term x 1 is an ǫ-likely condition because O x1x2 , O x1x2 , O x1x3 , O x1x3
are homogeneous, e.g., they are all fair to D = {(x 3 , 1)}. Contrastingly,

x 3 is not ǫ-likely because O x2x3 = {[∅, x 1 x 2 x 3 ] × 10} and O x2x3 = {[x 3 , x 1 x 2 x 3 ] × 10}
do not have even one likely effect in common.

Given enough observations for each 2k-term c, it turns out that with high probability, retaining ǫ-likely conditions (for small ǫ, as derived from Equation 1) is correct. The argument is essentially as follows [START_REF] Strehl | Efficient structure learning in factored-state MDPs[END_REF]:

1. any correct condition c = c i is ǫ-likely; indeed, all O c∧c j 's are homogeneous because by definition they are all induced by D i , 2. for any ǫ-likely c, by homogeneity O c is close in particular to O c∧ci for the real condition c i , and since O c∧ci is induced by D i , by the triangle inequality the most likely explanations of O c are close to the correct D i .

Handling Ambiguity. With ambiguous effects, we propose to use variance as the measure µ in Definition 3. Because variance underestimates the radius of the L1ball centered at the real distribution (Section 4), we get a complete approach.

Proposition 6. With high confidence (as given by Equation 1), any real condition c i of a is an ǫ-likely condition of a with respect to variance.

However, because the soundness of SLF-Rmax (Observation 2 above) relies on the triangle inequality, our approach is not sound in general, that is, a condition c may be ǫ-likely while inducing an incorrect distribution of effects. Still, choosing the candidate condition c with the smallest ǫ (that is, with the smallest L1-ball centered at it) gives a promising heuristic. In particular, the worst cases where two most likely explanations are very distant from one another are not likely to be frequent in practice. We give some preliminary experimental results below. Also observe that we could get a sound but incomplete approach by minimizing instead of maximizing the radius over all D's in the definition of variance. This however requires to solve a mixed integer instead of a linear program, and anyway did not prove interesting in our early experiments.

Importantly, our approach inherits the sample complexity of SLF-Rmax. A straightforward application of Equation 1 and an analysis parallel to the one of SLF-Rmax [START_REF] Strehl | Efficient structure learning in factored-state MDPs[END_REF] shows that we need a similar number of samples: essentially, for each candidate 2k-term c ∧ c j (there are n 2k 2 2k of them) we need the (polynomial) number of observations given by Equation 1for O c∧c j to be fair to the target distribution. Observe that 1/ǫ can be used as a default estimate of the number of effects in the target distribution (ℓ in Equation 1). Overall, the sample complexity is polynomial for a fixed bound k, just as for SLF-Rmax.

Preliminary Experiments. We ran some proof-of-concept experiments on two 512-state problems (n = 9 variables). These only aim at demonstrating that though heuristic, our approach can work well in practice, in the sense that it learns a good model with the expected sample complexity. Hence we depict here the reward cumulated over time in an RL setting, averaged over 10 runs. For both problems on which we report here, learning can be detected to have converged at this point where the cumulated reward starts to increase continuously.

We first tested the Builder domain [START_REF] Dearden | Abstraction and approximate decision-theoretic planning[END_REF] (slightly modified by removing the "wait" action, forcing the agent to act indefinitely). The number of variables in the conditions is k = 2 for one action, 5 for another, and 1 for all others. Actions modify up to 4 variables together and have up to 3 different effects.

Figure 1 (left) shows the behaviour of our approach ("PSO-Rmax"). The behaviour of (unfactored) Rmax [START_REF] Brafman | R-max: A general polynomial time algorithm for near-optimal reinforcement learning[END_REF] is shown as a baseline; recall that Rmax provably converges to optimal behaviour in a number of steps polynomial in the number of states. Both algorithms were run with m = 10 in Equation 1(in the corresponding equation for Rmax), as appeared to be most efficient. We have not run SLF-Rmax here because the effects of actions on variables are not independent (we leave extensions of SLF-Rmax to this setting for future work). Each "step" on the x-axis corresponds to 100 observed transitions. As can be seen, our algorithm efficiently exploits the structure and is very fast to converge to a near-optimal policy (by exploring an average of 57 states only). In no run have we observed behaviours keeping on deviating from the optimal one, as could happen in theory since our algorithm is not guaranteed to be sound and might learn an incorrect model. Inportantly, we also tested the behaviour of our approach with 3 dummy variables added along with actions to flip them, thus artificially extending the domain to 4096 states. As Figure 1 shows, this had almost no consequence on the convergence of our approach.

We also ran some experiments on a 3 × 2 Stocktrading domain [START_REF] Strehl | Efficient structure learning in factored-state MDPs[END_REF]. Here the effects are independent, so that DBNs are a compact representation (k = 2 variables in conditions for SLF-Rmax) while PSOs are not (k = 6 and k = 7). Experiments confirm that SLF-Rmax converges much faster than our approach. Despite this, as Figure 1 (right) shows, our algorithm behaves similarily as R max , which could be expected since considering all 2k-terms over 9 variables with k = 6 or 7 amounts to exploiting no structure. Nevertheless, again our method always converged to optimal behaviour despite its heuristic nature.

Conclusion

We have studied a maximum likelihood, unbiased approach to learning actions from transitions in which effects are ambiguous. We have shown that the maximally likely actions could be computed by a linear program with exponentially many variables, but that this number could be greatly reduced in pratice. Moreover, if a known, polynomial-size set of candidate effects is learnt or known in advance, then this can be exploited directly in the program.

We have proposed an application of our study to RL, for hidden actions with correlated effects, extending SLF-Rmax [START_REF] Strehl | Efficient structure learning in factored-state MDPs[END_REF]. Our approach is complete but not sound in general, but some proof-of-concept experiments suggest that it may work in pratice. Nevertheless, this application is mainly illustrative, and our projects include using variance as a measure of information in techniques based on induction of decision trees [START_REF] Degris | Learning the structure of factored Markov Decision Processes in reinforcement learning problems[END_REF], which prove to be more powerful in practice.

Another interesting perspective is to study information criteria able to bias the search for likely actions (e.g., MDL), and to integrate them efficiently in our linear programming approach. Finally, an important perspective in an RL context is to design exploration strategies able to help the agent disambiguate or learn the set of effects before trying to learn their relative probabilities.

  sampled once in s = 01 and twice in s = 10. Now despite O is 0-fair to D 1 and to D 2 , their L1-distance is maximal (2), and so are the transition functions T (•|00, •) which they induce in s = 00.

Proposition 2 .Proposition 3 .

 23 Let O be a multiset of observations and D = {(p i , e i ) | i ∈ I} be an effect distribution with ∀o ∈ O, ∃i ∈ I, e i ∈ o. Then O is ǫ-fair to D if and only if the following inequality holds: min e∈D |p D (e) -o∈O c e,o | ≤ ǫ where the minimum is taken over all combinations of nonnegative values for c e,o 's (for all effects e, observed intervals o) which satisfy the three conditions: ∀o ∈ O, e ∈ D if e / ∈ o then c e,o = 0 ∀o ∈ O e∈D c e,o = f o ∀o ∈ O ∃e such that p e = 0 and c e,o = 0 Proposition 3 below shows that the minimum is indeed well-defined (as the objective value of a linear program). Example 3 (continued). The multiset O from Example 2 is 0-fair to D 3 = {(x 1 , .4), (x 1 x 2 , .3), (x 2 , .3)}, as witnessed by contributions c x1,o1 = .4, c x1x2,o1 = .1, c x1x2,o2 = .2, c x2,o2 = .3. Now for D = {(x 1 x 2 , .9), (x 1 , .1)} we get 0.2-fairness with c x1x2,o1 = c x1x2,o2 = .5, and for D = {x 1 , .45), (x 2 , .55)} we get 0.1-fairness. Finally, O is not fair to D = {x 1 , 1)}, since no effect explains o 2 . Linearity. Fairness provides an effective way to compute most likely distributions. To see this, consider the following linear program 1 for given O and D: Variables: c e,o (∀o ∈ O, e ∈ O) Minimize: e∈3 X |p e -o∈O c e,o | Subject to: c e,o ≥ 0 (∀o ∈ O, e ∈ O) e∈o c e,o = f o (∀o ∈ O) This program implements Proposition 2, but ignoring the last constraint ∀o ∈ O, ∃e ∈ 3 X , p e = 0 and c e,o = 0 (this would be a strict inequality constraint). Still, it can be shown that it correctly computes how fair O is to D. Assume for all o ∈ O there is an e ∈ o with p e > 0. Then the optimal value of the program above is the minimal ǫ such that O is ǫ-fair to D.

  x 4 ]}, and O 3 = {[x 3 ] × 4, [x 4 ]}. It can be shown that O 2 and O 3 cannot be both 0.8-fair to any D, while for any ǫ > 0 there is a D to which all of O 1 , O 2 , O 3 are (0.8 + ǫ)-fair. Hence the center of O 1 , O 2 , O 3 does not exist (it is the argmin of an open set).

  and so are O 2 , O 3 (using D = {(x 2 , 1)}). Nevertheless, because the intervals in O 1 and O 3 are disjoint, for any distribution D the fairness of either O 1 or O 3 (or both) to D is at least 1, hence O 1 , O 3 are not ǫ-variant for any ǫ < 1.

Fig. 1 .

 1 Fig. 1. Cumulative rewards for Builder (left) and Stocktrading (right).

  2 , x 1 x 2 x 3 ]. Set intervals obey the rule [e 1 , e 2 ] ∩ [e 3 , e 4 ] = [e 1 ∪ e 3 , e 2 ∩ e 4 ]. For instance, [x

The objective is indeed linear, since it consists in minimizing the absolute values.

Acknowledgements. This work is supported by the French National Research Agency under grant LARDONS (ANR-2010-BLAN-0215).


Serdar Erbatur

Deepak Kapur

Andrew M Marshall

Catherine Meadows

Paliath Narendran

Christophe Ringeissen

Asymmetric Unification and the Combination Problem in Disjoint Theories

Keywords: Equational theory, asymmetric unification, combination problem Théorie équationnelle, Unification asymétrique, problème de combinaison

Asymmetric unification is a new paradigm for unification modulo theories that introduces irreducibility constraints on one side of a unification problem. It has important applications in symbolic cryptographic protocol analysis, for which it is often necessary to put irreducibility constraints on portions of a state. However many facets of asymmetric unification that are of particular interest, including its behavior under combinations of disjoint theories, remain poorly understood. In this paper we give a new formulation of the method for unification in the combination of disjoint equational theories developed by Baader and Schulz that both gives additional insights into the disjoint combination problem in general, and furthermore allows us to extend the method to asymmetric unification, thus giving the first unification method for asymmetric unification in the combination of disjoint theories.

Unification asymétrique et problème de combinaison dans des théories disjointes 1 Introduction

We examine the disjoint combination problem in the newly developed paradigm of asymmetric unification. This new unification problem was developed based on newly identified requirements arising from symbolic cryptographic protocol analysis [START_REF] Erbatur | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis[END_REF]. Its application involves unificationbased exploration of a space in which the states obey rich equational theories that can be expressed as a decomposition R ⊎ E, where R is a set of rewrite rules that is confluent, terminating and coherent modulo E. However, in order to apply state space reduction techniques, it is usually necessary for at least part of this state to be in normal form, and to remain in normal form even after unification is performed. This requirement can be expressed as an asymmetric unification problem {s 1 = ↓ t 1 , . . . , s n = ↓ t n } where the = ↓ denotes a unification problem with the restriction that any unifier leaves the right-hand side of each equation irreducible (see Definition 4).

The concept of asymmetric unification has its genesis in the unification method that is commonly used in symbolic analysis of cryptographic protocols. Here, two different requirements must be satisfied. The first is to have a generic unification algorithm that can be applied to a large class of equational theories that are encountered in cryptographic protocol analysis. The second is to guarantee that certain terms always be in normal form with respect to R (see Section 2), so that it is possible to apply state space reduction techniques. This is done by decomposing the theory into R ⊎ E so that R has the finite variant property [START_REF] Comon | The Finite Variant Property: How to Get Rid of Some Algebraic Properties[END_REF] with respect to E, i.e., for any term t there is a finite set of irreducible variants V (t) of pairs (u, σ), where u is a term and σ is a substitution, so that for each (u, σ) ∈ V (t) we have tσ ↓= E u and for any substitution τ there is a (u, σ) ∈ V (t) and a substitution ρ such that tτ ↓= E uρ. In other words, the set of variants gives a complete representation of the irreducible forms of t under any substitution. A unification problem is then solved by computing the variants of each side and unifying those modulo E. This approach to unification is used in a number of tools, including ProVerif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF], OFMC [START_REF] Mödersheim | Models and Methods for the Automated Analysis of Security Protocols[END_REF], Maude-NPA [START_REF] Escobar | Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties[END_REF], and Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF]. More recently, it has been formalized in a procedure known as folding variant narrowing [START_REF] Escobar | Folding Variant Narrowing and Optimal Variant Termination[END_REF], which terminates if and only if the terms being unified have a finite number of variants.

Although variant narrowing is sound and complete for theories with the finite variant property, it is not optimally efficient. In [START_REF] Erbatur | Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions[END_REF] it is pointed out that this issue can often be addressed by computing the set of variants of only one side of a unification problem s = ? t, replacing it with a new asymmetric problem s = ↓ t 1 , . . . , s = ↓ t n . One may then apply more efficient specialpurpose asymmetric unification algorithms that satisfy the irreducibility constraints. Recent work on asymmetric algorithms for exclusive-or [START_REF] Liu | Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis[END_REF], [START_REF] Erbatur | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis[END_REF] and free Abelian groups [START_REF] Liu | Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis[END_REF] indicate that such algorithms can lead to significant enhancement of performance.

Although asymmetric unification has the potential of playing an important role in cryptographic protocol analysis, and possibly other unification-based state exploration as well, it is still not that well understood. Until the development of special-purpose algorithms for exclusive-or and free Abelian group theories mentioned above, the only known asymmetric unification algorithm was variant narrowing. Since then, some better understanding has been developed. For Example, we know that asymmetric unification is strictly harder than "symmetric" unification. In particular, there are theories for which symmetric unification is decidable and asymmetric unification is not. Still, there are many questions that remain to be answered. One of the most important of these unanswered questions is the problem of asymmetric unification in a combination of theories, in particular how to produce an algorithm for the combined theory by combining algorithms for the separate theories. This is particularly significant for cryptographic protocol analysis. Cryptographic protocols generally make use of more than one cryptoalgorithm. Often, these cryptoalgorithms can be described in terms of disjoint equational theories. In the case in which the algorithm used is variant narrowing, the problem is straightforward. If the combination of two theories with the finite variant property also has the finite variant property, then one applies variant narrowing. However, in attempting to combine theories with special-purpose algorithms, the path is less clear. This is an important point with respect to efficiency since, as pointed out above, special-purpose asymmetric unification algorithms have the promise of being more efficient than variant narrowing.

In this paper we take the first step to solving this problem, by showing that the combination method for the unification problem in disjoint equational theories developed by Baader and Schulz in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] can be modified and extended to the asymmetric unification paradigm, thus providing the first general combination method for this new paradigm. The only restrictions on this new method are those inherited from the asymmetric unification problem and those inherited from Baader and Schulz. From [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] we require that the algorithms being combined solve the asymmetric unification with linear constant restriction problem, although we show this reduces to solving the general asymmetric unification problem.

Preliminaries

We use the standard notation of equational unification [START_REF] Baader | Unification Theory[END_REF] and term rewriting systems [START_REF] Baader | Term rewriting and all that[END_REF]. The set of Σ-terms, denoted by T (Σ, X ), is built over the signature Σ and the (countably infinite) set of variables X . The terms t| p and t[u] p denote respectively the subterm of t at the position p, and the term t having u as subterm at position p. The symbol of t occurring at the position p (resp. the top symbol of t) is written t(p) (resp. t(ǫ)). The set of positions of a term t is denoted by P os(t), the set of non variable positions for a term t over a signature Σ is denoted by P os(t) Σ . A Σ-rooted term is a term whose top symbol is in Σ. The set of variables of a term t is denoted by V ar(t). A term is ground if it contains no variables. A term t is linear if each variable of t occurs only once in t.

A Σ-substitution σ is an endomorphism of T (Σ, X ) denoted by {x 1 → t 1 , . . . , x n → t n } if there are only finitely many variables x 1 , . . . , x n not mapped to themselves. We call the domain of σ the set of variables {x 1 , . . . , x n } and the range of σ the set of terms {t 1 , . . . , t n }. Application of a substitution σ to a term t (resp. a substitution φ) may be written tσ (resp. φσ).

Given a first-order signature Σ, and a set E of Σ-axioms (i.e., pairs of Σ-terms, denoted by l = r), the equational theory = E is the congruence closure of E under the law of substitutivity. By a slight abuse of terminology, E will be often called an equational theory. An axiom l = r is variable-preserving if V ar(l) = V ar(r). An axiom l = r is linear (resp. collapse-free) if l and r are linear (resp. non-variable terms). An equational theory is variable-preserving (resp. linear/ collapse-free) if all its axioms are variable-preserving (resp. linear/ collapse-free). An equational theory E is finite if for each term t, there are finitely many terms s such that t = E s.

A Σ-equation is a pair of Σ-terms denoted by s = ? t. An E-unification problem is a set of Σ-equations, S = {s 1 = ? t 1 , . . . , s m = ? t m }. The set of variables of S is denoted by V ar(S).

A solution to S, called an E-unifier , is a substitution σ such that s i σ = E t i σ for all 1 ≤ i ≤ m. A substitution σ is more general modulo E than θ on a set of variables V , denoted as σ ≤ V E θ, if there is a substitution τ such that xστ = E xθ for all x ∈ V . Two substitutions θ 1 and θ 2 are equivalent modulo E on a set of variables V , denoted as θ 1 = V E θ 2 , if and only if xθ 1 = E xθ 2 for all x ∈ V . A complete set of E-unifiers of S is a set of substitutions denoted by CSU E (S) such that each σ ∈ CSU E (S) is an E-unifier of S, and for each E-unifier θ of S, there exists σ ∈ CSU E (S) such that σ ≤ V ar(S) E θ. Equational unification problems are classified based on the function symbols that appear in them, i.e., their signature (Sig). An E-unification problem S is elementary if and only if Sig(S) = Inria Sig(E). S is called an E-unification problem with constants if Sig(S) \ Sig(E) contains only free constants. Finally, if there are uninterpreted function symbols in Sig(S) \ Sig(E), then S is called a general E-unification problem.

Let E 1 and E 2 be two equational theories built over the disjoint signatures Σ 1 and Σ 2 . The elements of Σ i will be called i-symbols. A term t is an i-term if and only if it is of the form t = f (t 1 , , . . . , t n ) for an i-symbol f or t is a variable. An i-term is pure (or an i-pure term) if it only contains i-symbols and variables. An equation s = ? t is i-pure (or just pure) iff there exists an i such that s and t are i-pure terms or variables. A subterm s of an i-term t is called an alien subterm (or just alien) of t iff it is a non-variable j-term, j = i, such that every proper superterm of s in t is an i-term. A unification problem S is an i-pure problem if all equations in S are i-pure. Definition 1. Let Γ be an E-unification problem, let X denote the set of variables occurring in Γ and C the set of free constants occurring in Γ. For a given linear ordering < on X ∪ C, and for each c ∈ C define the set V c as {x | x is a variable with x < c}. An E-unification problem with linear constant restriction (LCR) is an E-unification problem with constants, Γ, where each constant c in Γ is equipped with a set V c of variables. A solution of the problem is an E-unifier σ of Γ such that for all c, x with x ∈ V c , the constant c does not occur in xσ. We call σ an E-unifier with linear constant restriction.

A rewrite rule is an ordered pair l → r such that l, r ∈ T (Σ, X ) and l ∈ X . We use R to denote a term rewrite system which is defined as a set of rewrite rules. The rewrite relation on T (Σ, X ), written t → R s, hold between t and s iff there exists a non-variable p ∈ P os Σ (t), l → r ∈ R and a substitution σ, such that t| p = lσ and s

= t[rσ] p . The relation → R/E on T (Σ, X ) is = E • → R • = E . The relation → R,E on T (Σ, X ) is defined as: t → R,E t ′ if
there exists a position p ∈ P os Σ (t), a rule l → r ∈ R and a substitution σ such that t| p = E lσ and t ′ = t[rσ] p . The transitive (resp. transitive and reflexive) closure of → R,E is denoted by

→ + R,E (resp. → * R,E ). A term t is → R,E irreducible (or in R, E-normal form) if there is no term t ′ such that t → R,E t ′ . If → R,E
is confluent and terminating we denote the irreducible version of a term, t, by t → ! R,E or t ↓ R,E . Definition 2. A rewrite rule l → r is duplicating if r contains more occurrences of some variable than l; otherwise, l → r is non-duplicating. We say that R is non-duplicating if every l → r ∈ R is non-duplicating. Definition 3. We call (Σ, E, R) a decomposition of an equational theory ∆ over a signature Σ if ∆ = R ⊎ E and R and E satisfy the following conditions:

1. E is variable preserving, i.e., for each s = t in E we have V ar(s) = V ar(t).

2. E has a finitary and complete unification algorithm. That is, an algorithm that produces a finite complete set of unifiers.

3. For each l → r ∈ R we have V ar(r) ⊆ V ar(l).

4. R is confluent and terminating modulo E, i.e., the relation → R/E is confluent and terminating. This definition is inherited directly from [START_REF] Erbatur | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis[END_REF] where asymmetric unification and the corresponding theory decomposition are first defined. The last restrictions ensure that s → ! R/E t iff s → ! R,E t (see [START_REF] Escobar | Variant Narrowing and Equational Unification[END_REF], [START_REF] Erbatur | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis[END_REF]).

The relation

→ R,E is E-coherent, i.e.,
Definition 4 (Asymmetric Unification). Given a decomposition (Σ, E, R) of an equational theory, a substitution σ is an asymmetric R, E-unifier of a set S of asymmetric equations {s 1 = ↓ t 1 , . . . , s n = ↓ t n } iff for each asymmetric equations s i = ↓ t i , σ is an (E ∪ R)-unifier of the equation s i = ? t i and (t i ↓ R,E )σ is in R, E-normal form. A set of substitutions Ω is a complete set of asymmetric R, E-unifiers of S (denoted CSAU R∪E (S) or just CSAU (S) if the background theory is clear) iff: (i) every member of Ω is an asymmetric R, E-unifier of S, and (ii) for every asymmetric R, E-unifier θ of S there exists a σ ∈ Ω such that σ ≤

V ar(S) E θ.

Example 1. Let R = {x ⊕ 0 → x, x ⊕ x → 0, x ⊕ x ⊕ y → y} and E be the AC theory for ⊕.

Consider the equation y ⊕ x = ↓ x ⊕ a, the substitution σ 1 = {y → a} is an asymmetric solution but, σ 2 = {x → 0, y → a} is not.

Definition 5 (Asymmetric Unification with Linear Constant Restriction). Let S be a set of of asymmetric equations with some LCR. A substitution σ is an asymmetric R, E-unifier of S with LCR iff σ is an asymmetric solution to S and σ satisfies the LCR.

Combining Asymmetric Unification Algorithms

Here we modify and extend the method for unification in the union of disjoint equational theories, developed by Baader and Schulz [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF], to the combination of asymmetric unification algorithms in the union of disjoint equational theories.

Problem Description:

Let ∆ 1 and ∆ 2 denote two equational theories with disjoint signatures Σ 1 and Σ 2 . Let ∆ be the combination, ∆ = ∆ 1 ∪∆ 2 , of the two theories having signature Σ 1 ∪Σ 2 . Let A i , i ∈ {1, 2}, be an asymmetric ∆ i -unification with linear constants restriction algorithm. We then give an algorithm which uses A 1 and A 2 to solve the elementary asymmetric unification problem over ∆. Recall that elementary implies that terms can only contain symbols in the signature of the theory or variables. But this is not restrictive, if we wish to have additional free functional symbols, these function symbols define a new empty theory and lead to another combination. Therefore, in what follows we will assume that a problem, Γ 0 , in the combined theory ∆, is an elementary asymmetric ∆-unification problem. In order to satisfy the requirements for asymmetric unification we make the following assumptions.

Restrictions: for each constituent theory (Σ i , ∆ i ):

1. There is a decomposition

∆ i = R i ⊎ E i and u → ! Ri,Ei v iff u -→ ! Ri/Ei v (see note (2) below).
2. E i is collapse-free and there exists a finitary E i -unification algorithm.

3. There exists a finitary complete asymmetric ∆ i -unification algorithm with linear constants restriction, A i (see note (3) below).

4. Variables are → Ri,Ei -normal forms.

5. Each R i is non-duplicating.

Notes on the Restrictions:

1. All Restrictions, except (3), are due to the asymmetric unification definition.

Inria 2. The definition of decomposition requires that -→ Ri/Ei be confluent and terminating. Thus, if u → ! Ri,Ei v iff u -→ ! Ri/Ei v, we have that → Ri,Ei is also confluent and terminating. 3. We show in Section 3.5 that there exists an asymmetric ∆ i -unification algorithm with linear constants restriction if there exists a general asymmetric ∆ i -unification algorithm.

According to our Restrictions, E 1 and E 2 are both variable preserving and collapse-free. Consequently, we have the following property:

Lemma 1. t = E1∪E2 s, if t is a non-variable i-term and s is a non-variable j-term, j = i.

Rewriting in the Combined Theory

The definition of asymmetric unification in the combined theory ∆, where ∆ = ∆ 1 ∪ ∆ 2 , requires us to not only find ∆-unifiers but also decide if a term is in → (R1∪R2),(E1∪E2) normal form. Therefore, we need to first ensure the modularity of rewriting, i.e., ensure that we can compute -→ (R1∪R2),(E1∪E2) -normal forms.

Consider now the combined theory (Σ, ∆), where

Σ = Σ 1 ∪ Σ 2 and ∆ = ∆ 1 ∪ ∆ 2 . Let R = R 1 ∪ R 2 and E = E 1 ∪ E 2 . Therefore, → R,E denotes → R1∪R2,E1∪E2 . Theorem 1. → R,E = -→ R1,E1 ∪ -→ R2,E2
Proof. Follows from the the fact that Σ 1 ∩ Σ 2 = ∅ and E = E 1 ∪ E 2 is variable preserving and collapse-free.

The relation -→ Ri,Ei is decidable for each sub-theory due to the assumption that -→ Ri,Ei is convergent. Therefore we obtain the following corollary to Theorem 1.

Corollary 1. The relation -→ R,E is decidable.
Note, with respect to termination, R 1 ∪ R 2 is non-duplicating, this is due to the disjoint theories and the fact that each R i is non-duplicating by assumption. Since R 1 ∪ R 2 is non-duplicating termination is obtained due to the results of [START_REF] Rusinowitch | On Termination of the Direct sum of Term-Rewriting Systems[END_REF], where it is shown that non-duplicating implies termination in the combination of terminating rewrite systems. Next we would like to know that -→ R,E is complete with respect to -→ R/E , i.e., u → ! Ri,Ei v iff u -→ ! Ri/Ei v, which is not true in general. For this to be true we need to know that -→ R,E is E-coherent, which implies the result (see [START_REF] Escobar | Variant Narrowing and Equational Unification[END_REF]). Lemma 2. If there exist terms t 0 , t 1 and t 2 such that t 0 ↔ * E t 2 and t 0 → R,E t 1 then there exists a term t 3 such that t 2 → R,E t 3 .

Proof. If t 0 = t 2 then the result follows. Therefore, let t 0 ↔ + E t 2 , which implies that

t 0 = k 1 ↔ d1=g1 k 2 ↔ d2=g2 k 2 . . . ↔ dn=gn k m = t 2
where each

d l = g l ∈ E 1 ∪ E 2 .
We can now proceed by induction on m, demonstrating at each step there exists a → R,E reduction. Consider a step k l ↔ d l =g l k l+1 and assume that k l → R,E u for some term u. By the assumptions, there exist p, q, σ, δ and l

→ r ∈ R 1 ∪ R 2 such that k l | p = d l σ, k l+1 = k l [g l σ] p , k l | q = E1∪E2 lδ and u = k l [rδ] q .
If p||q (not comparable with respect to the prefix ordering) then the result follows, so we assume that p and q are comparable with respect to the prefix ordering. Without loss of generality assume that k l is an i-term, for i ∈ {1, 2}. We can also assume that one (or both) p or q occur in (k l ) πi . Otherwise, we could just consider the alien subterm which contains both reductions. Now assume that p ≤ q which implies that q = pq ′ , i.e., p is a prefix of q. Since one or both p and q occur in (k l ) πi and p ≤ q, we have that p is a non-variable position in (k l ) πi , which implies d l = g l ∈ E i since the signatures of E 1 and E 2 are disjoint.

We then have two cases: first, the term rooted at q is not an alien subterm and second, the term rooted at q is an alien subterm.

1. If k l | q is not an alien then its is also an i-term, which implies that l → r ∈ R i and k l | q = Ei lδ. In this case the result follows due to the coherence property of → Ri,Ei . That is, since

k l = Ei k l+1 , k l → Ri,Ei u, there exists some u ′ such that k l+1 → Ri,Ei u ′ , which is a reduction in k l+1 .
2. Otherwise, the term rooted at q is an alien and thus a j-term (j = i). If we consider (k l ) πi , then k l | q under the projection π i is a variable y. Since E 1 and E 2 are variable-preserving, the variable y is maintained in the following sequence:

k l = E (k l [d l σ] p ) πi π -1 = E (k l [g l σ] p ) πi π -1 = E k l+1
Therefore, y occurs in (k l [g l σ] p ) πi at some position q ′ and since yπ -1 = E lδ, we have that

k l+1 | q ′ = E lδ, i.e.
, there is a reduction in k l+1 . Now assume that q ≤ p which implies that p = qp ′ . We again have two cases.

1. If both p and q occur in (k l ) πi we can again use the coherence property to show the result.

2. Now assume that the term rooted at p is an alien subterm. In this case the result follows since changing an alien subterm via

E 1 ∪ E 2 will not effect a reduction in the superterm via → R,E . Since (k l | q ) πi = Ei (k l+1 | q ) πi , we have lδ = E k l | q = E (k l | q ) πi π -1 = E (k l+1 | q ) πi π -1 = E k l+1 | q which implies a reduction in k l+1 . Theorem 2. → R,E is E-coherent.
Proof. If t 0 → R,E t 1 and t 0 = E t 2 , then by Lemma 2, there exists a term, t 3 , such that t 2 → R,E t 3 . Thus, t 1 ←→ R1∪R2∪E1∪E2 t 3 . Now the combined system has the properties (normal form variables, E i collapse-free, and disjoint signatures) such that the Church-Rosser result in [START_REF] Jouannaud | Modular Church-Rosser Modulo: The Complete Picture[END_REF] applies. This implies the existence of terms t 4 and t 5 such that

t 1 → * R,E t 4 , t 3 → * R,E t 5 and t 4 = E t 5 .
Therefore, based on Corollary 1 and Theorem 2, u → * R,E v iff u → * R/E v which implies the following:

Theorem 3. t = R∪E s iff t ↓ R,E = E s ↓ R,E

Asymmetry in the Projection of Terms

Now that we have established the modular results for rewriting we can use the well defined normal forms to define projections onto pure terms. Later we will use the bijection defined below to prove that if the original problem has a solution then there exists solutions to the pure subproblems. This is accomplished by mapping the combined solution into two pure solutions. In order for this to work we also need to ensure that equality modulo E and asymmetric restrictions Inria are maintained after the mapping is applied. Let X and Y be disjoint sets of variables that are countably infinite. Let T (Σ, X ) be the set of Σ 1 ∪ Σ 2 -terms over X . We define a bijection

π : (T (Σ, X ) ↓ R,E ) /= E → Y (1)
The bijection π induces two mappings π 1 and π 2 of terms in T (Σ, X ) to terms in T (Σ, Y) as follows. For each x ∈ X , x π1 := π(x). If t = f (t 1 , . . . , t n ) for a 1-symbol f , then t π1 := f (t π1 1 , . . . , t π1 n ). If t is a 2-term then t π1 := y where y = π([s] E ) for the unique → R,E -irreducible term s of t, where [s] E denotes the equivalence class of s modulo E. The mapping π 2 is defined analogously.

Given a substitution σ, σ πi denotes the abstraction defined by σ πi (x) = (σ(x)) πi , for all x is the domain of σ. These two mapping can be seen as projections from mixed terms into pure terms. More informally, we can view an i-abstraction as method for converting a mixed term a pure term by replacing the alien subterms with variables. Recall that we assume that variables are -→ Ri,Ei -irreducible and thus by modularity → R,E -irreducible. As in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] we can also define the inverse, π -1 of π as a substitution that maps the variables y ∈ Y back to terms π -1 (y) and is the identity on all other variables. Note that, π -1 (t πi ) = E t, if t is in R, E-normal form or an i-term with normal form aliens.

Theorem 4. Let s and t be i-pure terms. Let t and σ be in R, E-normal form, such that sσ = ∆ tσ. Then sσ πi = ∆i tσ πi and tσ is in R, E-normal form iff tσ πi is in R i , E i -normal form.

Proof. We can without loss of generality assume that

t is in → R,E -normal form. If (sσ) = ∆i (tσ) then (sσ) * --→ R,E r ←→ E u * ←-- R,E (tσ)
We first show that (sσ) πi ----→

Ri,Ei r πi . Then by symmetry we get that (sσ) πi = ∆i (tσ) πi . It will then remain to show the asymmetric property. Consider (sσ) = s 0 → R,E s 1 → R,E . . . → R,E r. We need to show that this implies that s πi 0 -→ Ri,Ei s πi 1 -→ Ri,Ei . . . -→ Ri,Ei r πi . Since we assume that variables are irreducible the case where s is a variable is trivial. Thus lets assume that s is an i-pure term and consider sσ. Notice since σ is → R,E -reduced the position, p, of the redex in sσ must be a non-variable position in s and thus an i-term. This implies that s 0 → Ri,Ei s 1 or that there exists a → R,E -reduced substitution δ, a position p (corresponding to a position, and thus an i-pure subterm, in s) and rule l → r ∈ R i such that s 0 | p = Ei lδ and s 1 = s 0 [rδ] p .

Let u be the redex in s 0 , then s πi 0 = s πi 0 [u πi ] p and s πi 1 = s πi 0 [(rδ) πi ] p . Since the reduction must occur at a position corresponding to an i-pure term we have that

(s 0 ) πi | p = u πi = Ei (lδ) πi = lδ πi → Ri rδ πi = (rδ) πi which implies that s πi 0 -→ Ri,Ei s πi 1 .
Now since E i is variable-preserving and V ar(r) ⊆ V ar(l), the reduction does not introduce new variables such that under the image of δ new reducible alien subterms are produced. Therefore, we can proceed by induction to show that s πi 0 -→ Ri,Ei s πi 1 -→ Ri,Ei . . . -→ Ri,Ei r πi . Now, we need only show that (tσ) πi is in → Ri,Ei -normal form. Assume that this is not the case, that there exists a position, p in ((tσ) πi ), a rule, l → r, in R i and a E i -matching substitution, θ, such that (tσ) πi | p = Ei lθ. Then, by the definition of π -1 we have

(tσ)| q = E1∪E2 (tσ) πi | p π -1 = Ei lθπ -1 = lθ ′ (tσ)| q = E lθ ′
For some position q in tσ, which exists due to E being collapse-free and variable preserving. However, this contradicts the assumption that tσ was in → R,E -normal form.

Asymmetric Unification with Linear Constant Restriction

We present the combination Algorithm, AsymComb, in Figure 1. Let us first give a rough, intuitive overview of the steps. First, equations are purified using variable abstraction and splitting (steps 1 and 2 ). This ensures that the original problem is separated into pure problems which can be solved by the algorithms for the pure theories. Next, a variable identification is non-deterministically chosen, allowing for the testing all the ways the variables may be equated to other variables. Then, a linear ordering and theory indices are non-deterministically chosen. Note that a shared variable can only "belong" exclusively to one theory. Since we don't know beforehand what variable belongs to which theory the non-deterministic selections allow us to check all the possibilities. In addition, each solution to the original problem will correspond to one or more linear ordering among the variables. Next, the problem is split into two pure problems where the linear ordering defines a linear constant restriction. The pure problems are solved by asymmetric unification algorithms with linear constant restriction. The solutions returned by the sub-algorithms are combined into solutions for the original problem. The Algorithm AsymComb (cf. Figure 1) must also ensure that we only combine a specific type of unifier, which ensures asymmetry.

The notions of identification, theory indexes and linear constant restrictions, have all been used in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] (see Section 2 for definitions). In order to handle the asymmetry restriction we introduce two additional notions, which ensure pure problem solutions having these properties will result in asymmetric combined solutions.

Definition 6. (Injective)

A substitution, σ i , is said to be injective modulo ∆ i if for any two variables x, y in the domain of σ i , we have that xσ i = ∆i yσ i if and only if x = y.

Definition 7. (Theory Preserving)

A substitution σ i , solving an i-pure problem Γ i , is said to be theory preserving if for any variable x of index i in the domain of σ i , xσ i is not a variable of index j = i.

With respect to the combination algorithm this definition basically states that a substitution σ i , which solves an i-pure problem, Γ i , produced by Algorithm AsymComb (cf. Figure 1), is theory-preserving if for all x ∈ Dom(σ i ), xσ i = c where c is a free constant. This is due to the fact that for the pure sub-problems produced by the combination algorithm the only free constants will be those corresponding to shared variables of a different index. Note, the definition of theory-preserving does not restrict σ i from sending an i-variable x to a non-variable i-term whose leafs are j-variables. Thus, if xσ i = t and t is an i-term, then t may contain j-variables. In addition, since the Algorithm AsymComb assigns the variable indexes, it can always check the substitutions returned by the algorithms for the pure theories to ensure that they are injective and theory-preserving. Definition 8. Let σ 1 and σ 2 be unifiers with linear constant restriction for Γ 5,1 and Γ 5,2 such that Γ 5,i is the set of i-pure equations from Γ 4 and < is the corresponding linear ordering. The combined solution σ 1 ⊙ σ 2 is defined by induction on <:

Let x be the least variable with respect to the ordering < from step 4 and let i be its index. Since the solution σ i of Γ 5,i satisfies the constant restriction induced by <, xσ i does not contain any variables of index j = i. We define x(σ 1 ⊙ σ 2 ) to be xσ i .

Let x be an arbitrary variable of index i and let y 1 , . . . , y m be the variables of index j = i occurring in xσ i . Again, due to the constant restriction, the variables y 1 , . . . , y m have to be smaller than x. This implies that y 1 (σ 1 ⊙ σ 2 ), . . . , y m (σ 1 ⊙ σ 2 ) are already defined. The term x(σ 1 ⊙ σ 2 ) is obtained from xσ i by replacing y k by y k (σ 1 ⊙ σ 2 ), and we define x(σ 1 ⊙ σ 2 ) to be xσ i (σ 1 ⊙ σ 2 ).

Inria

Input: Γ 0 , the initial unification problem over the signature Σ 1 ∪ Σ 2 , where we assume the right hand sides of the equations are normalized.

Variable Abstraction

: Let s = ↓ t ∈ Γ 0 .
(a) Right Abstraction: For each alien subterm t 1 of t, let x be a variable not occurring in the current system and let t ′ be the term obtained from replacing t 1 by x in t. Then the original equation is replaced by two equations s = ↓ t ′ and x = ↓ t 1 .

(b) Left Abstraction: For each alien subterm s 1 of s let x be a variable not occurring in the current system and let s ′ be the term obtained from replacing s 1 by x in s. Then the original equation is replaced by two equations s ′ = ↓ t and s 1 = ↓ x.

The output is a system Γ 1 such that all terms are pure.

2. Split non-pure equations: Each non-pure equation of the form s = ↓ t is replaced by two equations s = ↓ x, x = ↓ t where x is always a new variable. The results is a system Γ 2 of pure equations.

3. Variable Identification: Consider all the possible partitions of the set of variables. Each partition produces a new system Γ 3 as follows. The variables in each class of the partition are "identified" with each other by choosing an element of the class as a representative and replacing in the system all occurrences of variables in each class by their representative.

Choose an ordering and Theory index:

For each Γ 3 we consider all the possible strict orderings < on the variables of the system and all mappings ind from the set of variables into the set of indices {1, 2}. Each pair (<, ind) yields a new system Γ 4 .

5. Split the system: Each Γ 4 is split into two systems Γ 5,1 and Γ 5,2 , the first containing only 1-equations and the second only 2-equations. In the system Γ 5,i the variables of index j = i are treated as constants. Each Γ 5,i is now a unification problems with linear constant restriction, where the linear ordering < defines the set V c for each constant c corresponding to an index j = i variable.

6. Compute M i,j : For the initial system Γ 0 let {(Γ 1 5,1 , Γ 1 5,2 ), . . . , (Γ n 5,1 , Γ n 5,2 )} be the output of the decomposition. For i = 1, . . . , n and j = 1, 2, let M i,j = CSAU ∆j (Γ i 5,j ) produced by Algorithm A j , where substitutions that are non-injective and not theory-preserving are discarded.

Output:

For i = 1, . . . , n the set of substitutions σ 1 ⊙ σ 2 such that σ 1 ∈ M i,1 and σ 2 ∈ M i,2 . Figure 1: Algorithm AsymComb Lemma 3. (Baader-Schulz [2]) The combined unifier σ 1 ⊙ σ 2 from Definition 8 is a unifier of Γ 4 . Example 2. Let ∆ 1 = R 1 ∪ E 1 , where R 1 = {e(x, d(x, y)) → y, d(x, e(x, y)) → y} and E 1 = ∅. Let ∆ 2 = R 2 ∪ E 2 , where R 2 = {x ⊕ 0 → x, x ⊕ x → 0, x ⊕ x ⊕ y → y} and E 2 = {x ⊕ y = y ⊕ x, (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)}}. Let ∆ = ∆ 1 ∪ ∆ 2 .
Consider the initial problem Γ 0 consisting of the following:

{x 0 ⊕ x 1 ⊕ x 2 = ↓ x 3 ⊕ x 4 , e(x 1 , d(0, x 5 )) = ↓ x 2 ⊕ x 0 , e(x 1 , d(x 0 , e(x 2 , x 6 ))) = ↓ e(x 7 , x 5 )}
Let us now examine the action of Algorithm AsymComb (cf. Figure 1) on Γ 0 and how it would find a particular asymmetric solution. The first 2 steps produce the set of pure equations Γ 2 :

{x 0 ⊕x 1 ⊕x 2 = ↓ x 3 ⊕x 4 , e(x 1 , d(z 0 , x 5 )) = ↓ z 1 , 0 = ↓ z 0 , z 1 = ↓ x 2 ⊕x 0 , e(x 1 , d(x 0 , e(x 2 , x 6 ))) = ↓ e(x 7 , x 5 )}.
The next step considers the set of variable partitions, one of which is the following partition {{x 0 , x 3 }, {x 2 , x 4 }, {x 5 , z 1 }, {x 1 , z 0 , x 7 }, {x 6 }} Choosing a representative for each set and doing the replacement the Algorithm would produce the following Γ 3 from that partition:

{x 0 ⊕x 1 ⊕x 2 = ↓ x 0 ⊕ x 2 , e(x 1 , d(x 1 , x 5 )) = ↓ x 5 , 0 = ↓ x 1 , x 5 = ↓ x 2 ⊕ x 0 , e(x 1 , d(x 0 , e(x 2 , x 6
))) = ↓ e(x 1 , x 5 )}. The next step considers the possible pairs of variable orderings and theory indexes. One pair that would be produced is the following:

x 6 > x 5 > x 2 > x 1 > x 0 , index-1 = {x 0 , x 1 , x 2 , x 5 } and index-2 = {x 6 }.
Next Γ 4 is produced from that pair and split into pure sets to produce Γ 5,1 and Γ 5,2 . Let us denote a variable, y, being treated as a constant as y. Then, Γ 5,1 is the following set of equations:

{x 0 ⊕ x 1 ⊕ x 2 = ↓ x 0 ⊕ x 2 , 0 = ↓ x 1 , x 5 = ↓ x 2 ⊕ x 0 } and Γ 5,2 is the following set of equations: {e(x 1 , d(x 1 , x 5 )) = ↓ x 5 , e(x 1 , d(x 0 , e(x 2 , x 6 ))) = ↓ e(x 1 , x 5 )}
Next Γ 5,1 is solved with A 1 and Γ 5,2 with A 2 , where the linear constant restriction is obtained via the linear ordering and theory index. The last step is to combine each pair of substitutions (σ 1 , σ 2 ) into a substitution σ, where σ i is an injective and theory-preserving asymmetric with LCR solution to Γ 5,i returned by A i . One such pair is σ 1 = {x 1 → 0, x 5 → x 2 ⊕ x 0 } and σ 2 = {x 6 → d(x 2 , e(x 0 , x 5 ))}. Applying Definition 8 we get the following solution, {x 1 → 0, x 3 → x 0 , x 4 → x 2 , x 5 → x 2 ⊕ x 0 , x 6 → d(x 2 , e(x 0 , x 2 ⊕ x 0 )), x 7 → 0}, which is an asymmetric solution to Γ 0 (existential variables z 0 , z 1 are removed).

Before presenting the proof details lets us briefly point out the main differences between Algorithm AsymComb (cf. Figure 1) and the algorithm of [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF]. While the general framework of the two algorithms is similar there are several key differences. First, we do not consider general theories. Due to the restrictions inherited from the definition of asymmetric unification we must consider theories with specific structure, namely the decomposition. This requires new results for showing the correctness of the algorithm and new results for showing that the required properties for asymmetric unification are maintained. Second, we must identify the specific unifiers which satisfy the asymmetry. We accomplish this by identifying two key properties, theory preservation (Definition. 7) and injectivity (Definition. 6).

Correctness

We show in this section that the Algorithm AsymComb (cf. Figure 1) is both sound and complete for the decision problem. In addition, we show that the algorithm produces a complete set of asymmetric unifiers. Lemma 4. Assume that σ 1 and σ 2 are pure, injective, theory-preserving and R i , E i -normalized unifiers modulo respectively ∆ 1 = R 1 ⊎ E 1 and ∆ 2 = R 2 ⊎ E 2 and they satisfy the same linear constant restriction. Then, the substitution σ = σ 1 ⊙ σ 2 satisfies the following properties: (1) σ is an injective substitution modulo

∆ 1 ∪ ∆ 2 . (2) σ is R, E-normalized.
Proof. We proceed by induction on the linear ordering. Base case: Let v be the smallest variable, say of index i. Then, σ is clearly injective and R, Enormalized for variables smaller or equal to v, since vσ = vσ i is R i , E i -normalized, and so also R, E-normalized.

Inductive case: Assume the the properties holds for variables smaller than a variable y of index i. To show that (1) holds, assume by contradiction that there exists a variable x strictly smaller than y such that xσ = ∆1∪∆2 yσ. Since σ is R, E-normalized for variables smaller than y, we have that xσ = ∆1∪∆2 yσ implies xσ πi = ∆i yσ πi . Since σ is injective for variables smaller than y, there exists a renaming ρ such that xσ πi ρ = xσ i and yσ πi ρ = yσ i . Therefore xσ i = ∆i yσ i , which is a contradiction.

Inria

Consider now the property (2): if yσ is R, E-reducible, then (yσ) πi is R i , E i -reducible, which means that yσ i ρ and yσ i are R i , E i -reducible too, which contradicts the assumption that σ i is an R i , E i -normalized substitution.

Lemma 5. Let Γ 0 be a solvable asymmetric ∆-unification problem, where ∆ = ∆ 1 ∪∆ 2 . Assume there exists a pair (Γ 5,1 , Γ 5,2 ) produced by the Algorithm AsymComb (cf. Figure 1) on Γ 0 and a pair (σ 1 , σ 2 ) such that σ i ∈ CSAU ∆i (Γ 5,i ) for i = 1, 2. Then, there exists pairs (Γ ′ 5,1 , Γ ′ 5,2 ) produced by the Algorithm AsymComb on Γ 0 and a pair (φ 1 , φ 2 ) such that φ i is injective and theory-preserving, φ i ∈ CSAU ∆i (Γ ′ 5,i ) for i = 1, 2, and

φ 1 ⊙ φ 2 ≤ V ar(Γ0) ∆ σ 1 ⊙ σ 2 . Proof. Construct (Γ ′ 5,1 , Γ ′ 5,2 ) and (σ ′ 1 , σ ′ 2 )
: Let Γ 4 be the conjunction of Γ 5,1 and Γ 5,2 . Then there exists a linear ordering, <, and a theory index, ind. From Γ 4 we can construct a new Γ ′ 4 as follows: If there exists x, y in the domain of σ i such that xσ i = ∆i yσ i we add x = y to the variable identification. If there exists variables x, y such that x is an index i variable, y is an index j variable and xσ i = y, we replace all x with y in the variable identification. ind and < remain the same. The result of these steps is a new Γ ′ 4 , which also gives us a new pair (Γ ′ 5,1 , Γ ′ 5,2 ). We can now define the new pair of substitutions To complete the proof, there exists

(σ ′ 1 , σ ′ 2 ) as follows: Let Dom(σ ′ i ) = V ar(Γ ′ 5,i ). ∀x ∈ Dom(σ ′ i ), xσ ′ i = xσ i
φ i ∈ CSAU ∆ (Γ ′ 5,i ) such that φ i ≤ V ar(Γ0) ∆ σ ′ i for i = 1, 2. By the definition of ⊙, we have that φ 1 ⊙φ 2 ≤ V ar(Γ0) ∆ σ ′ 1 ⊙σ ′ 2 = σ ′ , and σ ′ = V ar(Γ0) ∆ σ. Therefore, φ 1 ⊙ φ 2 ≤ V ar(Γ0) ∆ σ 1 ⊙ σ 2 = σ.
Lemma 6. For each asymmetric unifier of a problem Γ 0 , there exists a pair (Γ 5,1 , Γ 5,2 ) computed by the Algorithm AsymComb (cf. Figure 1), where for each Γ 5,i there exist a substitution τ i which asymmetrically solves Γ 5,i .

Proof. We present a very similar proof to the one presented in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF], containing the necessary updates to account for the asymmetry. Let τ be an ∆ 1 ∪ ∆ 2 -asymmetric solution to Γ 0 . Without loss of generality we can assume that τ is a solution to Γ 2 and that τ is normalized on V ar(Γ 2 ).

• Identify Γ 5,1 and Γ 5,2

-We obtain the system Γ 3 by defining a partition of the variables as follows: two variables x and y are in the same class of the partition if xτ = yτ . This also implies that τ is an asymmetric solution to Γ 3 .

-We obtain the system Γ 4 by defining a theory index and linear ordering as follows: * The variable y gets index i if yτ is an i-term. If yτ is a variable then we can arbitrarily define its index as 1. * In order to define the linear ordering we start with the strict partial ordering, y < x iff yτ is a strict subterm of xτ . The partial ordering can then be arbitrarily extended to a linear ordering.

This also implies that τ is an asymmetric solution to Γ 4 , since this step does not modify any equation.

• Define τ i Recall the bijection π : (T (Σ, X ) ↓ R,E ) /= E -→ Y. We add two additional restrictions. First, V ar(Γ 4 ) ⊆ Y. Since τ is assumed to be normalized on V ar(Γ 2 ) we have that for all y ∈ V ar(Γ 4 ), yτ is -→ R,E -irreducible. Second, we need π(yτ ) = y, which is obtained due to the variable identification step. This bijection then induces 2 mappings, π 1 and π 2 , which are defined as described above. These mappings are used to define τ i as follows:

∀y ∈ V ar(Γ 4 ), yτ i = (yτ ) πi (2)
• Show τ i is an asymmetric solution to Γ 5,i Assume s = ↓ t is an equation in Γ 1 5,i . First, this equation must exist in Γ 4 and therefore asymmetrically solvable by τ . That is, sτ = ↓ ∆1∪∆2 tτ . Since s = ↓ t ∈ Γ 1 5,i , it must be an i-equation. These facts combined allow us to apply Theorem 4 to get (sτ ) πi = ↓ ∆i (tτ ) πi . Since s = ↓ t is an i-equation we get that (sτ ) πi = sτ i and (tτ ) πi = tτ i , which implies that τ i is an asymmetric solution to s = ↓ t. Lemma 7. Let Γ 0 be an asymmetric ∆-unification problem. For each asymmetric unifier τ of Γ 0 there exists a pair (Γ 5,1 , Γ 5,2 ) in the output set of the Algorithm AsymComb (cf. Figure 1), and a pair of substitutions (σ 1 , σ 2 ) with each σ i ∈ CSAU ∆i (Γ 5,i ), such that σ = σ 1 ⊙ σ 2 is an injective asymmetric solution to Γ 0 with σ ≤ V ar(Γ0) ∆ τ .

Proof. From Lemma 6 we have that given τ there exists a pair (Γ 1 5,1 , Γ 1 5,2 ) and substitutions (τ 1 1 , τ 1 2 ) such that τ 1 i asymmetrically solves Γ 1 5,i . Now, if τ 1 i is an asymmetric solution to Γ 1 5,i , there exists a substitution τ 2 i produced by the algorithm A i such that τ 2 i ∈ CSAU ∆i (Γ 1 5,i ) and τ 2 i ≤ V ar(Γ5,i) ∆i τ 1 i . Furthermore, as in Lemma 5, by the definition of ⊙, we have that Lemma 9 in the Appendix for an alternate proof of this fact). From Lemma 5, there exists a pair (Γ 2 5,1 , Γ 2 5,2 ) produced by AsymComb and a pair (σ 1 , σ 2 ) such that σ i is injective and theory-preserving,

τ 2 = τ 2 1 ⊙ τ 2 2 ≤ V ar(Γ0) ∆ τ 1 1 ⊙ τ 1 2 = τ (see
σ i ∈ CSAU ∆i (Γ 2 5,i ) and σ = σ 1 ⊙ σ 2 ≤ V ar(Γ0) ∆ τ 2 .
By Lemma 4, σ is an injective asymmetric solution to Γ 4 . Finally, σ ≤

V ar(Γ0) ∆ τ 2 and τ 2 ≤

V ar(Γ0) ∆ τ , and so σ ≤

V ar(Γ0) ∆ τ .

We can now show the the Algorithm AsymComb (cf. Figure 1) is correct, i.e., both sound and complete.

Theorem 5. Let Γ 0 be a combined asymmetric unification problem. Γ 0 is asymmetrically unifiable if and only if the Algorithm AsymComb (cf. Figure 1) returns a combined substitution.

Proof. From Lemma 3, the substitutions returned are unifiers. From Lemma 4 the substitutions are asymmetric. Completeness follows from Lemma 7.

Inria

Now we can consider the complete set of unifiers. Theorem 6. Let Γ 0 be an asymmetric ∆-unification problem. Then, for every τ ∈ CSAU (Γ 0 ), Algorithm AsymComb (cf. Figure 1) produces an injective substitution σ such that σ ≤ V ar(Γ0) ∆ τ .

Proof. For any problem, Γ 0 , the Algorithm AsymComb will try every combination of variable identification, theory index and linear ordering, i.e. every possible pair of sub-problems (Γ 5,1 , Γ 5,2 ). Furthermore, the Algorithm AsymComb will combine every pair, (σ 1 , σ 2 ), of injective and theory preserving solutions such that σ i ∈ CSAU ∆i (Γ 5,i ), i ∈ {1, 2}. Thus, the result follows from Lemma 7.

Obtaining Linear Constant Restriction Algorithms

If one has a general asymmetric unification algorithm an algorithm that respects an LCR can be obtained. The construction is based on the construction given in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] with modifications for asymmetry. Given Γ, an asymmetric unification problem with a linear constant restriction, we construct a general unification problem Γ ′ such that Γ is solvable iff Γ ′ is solvable. < denote the linear ordering. Let X denote the variables of Γ and let C denote the set of all free constants in Γ. Now, we construct Γ ′ as follows: The free constants in Γ are treated as variables in Γ ′ . For each free constant c of Γ we add a new free function symbol f c which has arity

|V c |. Recall that V c = {x ∈ X |x < c}. Γ ′ = Γ ∪ {c = ↓ f c (x 1 , . . . , x n ) |c ∈ C and V c = {x 1 , . . . , x n }} Theorem 7.
The Asymmetric E-unification problem with linear constant restriction, Γ, is solvable iff the general Asymmetric E-unification problem Γ ′ is solvable.

Proof. Let σ be an → R,E normalized, asymmetric solution to Γ. σ ′ is defined on X ∪ C by induction on < as follows:

1. Least element of X ∪ C. • For an arbitrary c ∈ C, where by definition Γ ′ contains the equation

c = ↓ f c (x 1 , . . . , x n ). Then cσ ′ := f c (x 1 σ ′ , . . . , x n σ ′ ).
It remains to be shown that σ ′ is an asymmetric solution to Γ ′ . First, consider the equations of the form c = ↓ f c (x 1 , . . . , x n ), by definition σ ′ solves this equation. In addition, since f c is a new free function symbol it will not match any rule. Thus if there exists a reduction it exists in a variable position. We can then show by induction and the asymmetry of σ that there cannot be a reduction in any of the variable positions. Next consider an equation, s = ↓ t, from Γ. Here the fact that σ ′ solves these equations is shown in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF]. In addition since a reduction in tσ ′ would imply a reduction in tσ, σ ′ is also an asymmetric unifier. Assume that σ ′ is an asymmetric solution to Γ ′ . It is shown in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] that if for all x ∈ Γ we define σ as xσ := (xσ) π1 , where the symbols f c are treated as 2-symbols and the remaining as 1-symbols, then σ is a solution to Γ. Since the projection onto 1-pure terms will not introduce new reductions, σ is also an asymmetric solution.

We can also obtain a complete set of unifiers for the LCR version of the problem if we have a complete set of unifiers for the general asymmetric unification problem. Like the result for the decision problem this result is mostly proven in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] and we need only make some modification for asymmetry and the type of rewriting. We include the construction here for completeness.

Let Γ again denote an asymmetric problem with linear constant restriction and let Γ ′ denote the constructed general problem (see the construction at the beginning of this section). Now we give a slightly modified version of a construction from [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF], showing how a substituation σ ′ from the complete set of unifiers of Γ ′ can be used to define a solution σ to Γ. Without loss of generality, we will assume that all substitutions are → R,E -normalized. We can use a similar bijection method to help define the solutions. Let Σ ′ be the signature of Γ ′ , i.e., it includes the new f c symbols. Let π be a bijection from the set (T (Σ ′ , X ) ↓ R,E )/ = E onto a set of variables Y. In addition, we require that π(cσ ′ ) = c for the free constants c in Σ, which means that Y must contains these free constants which are variables in Γ ′ . This condition is true if cσ ′ = R∪E c ′ σ ′ when c = c ′ . Which is satisfied since σ ′ solves Γ ′ which implies that cσ ′ = ↓ R∪E f c (x 1 σ ′ , . . . , x n σ ′ ) and c ′ σ ′ = ↓ R∪E f c ′ (x 1 σ ′ , . . . , x m σ ′ ). This implies the root symbol of the two terms is different. Now that we have a bijection we can again define the mappings π 1 and π 2 as we have done in Section 3.2. However, for the new mappings we let Σ be the signature of the 1-symbols and let the f c symbols be the 2-symbols. We can now see that the mapping π 1 can be used to define the solution σ to Γ. That is, for all variables, x, in Γ let xσ = (xσ ′ ) π1 . Lemma 8. The set C(Γ) = {σ | σ ′ ∈ CSAU (Γ ′ )}, where σ is constructed from σ ′ as described above, is a complete set of asymmetric unifiers with linear constant restriction of Γ.

Proof. From Proposition 5.3 of [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF] we can conclude that C(Γ) is a complete set of unifiers with linear constant restriction of Γ. However, we need to show that they satisfy the asymmetric restriction. First, recall that Γ ⊂ Γ ′ and let s = ↓ t ∈ Γ. We know that sσ ′ = ↓ R∪E tσ ′ , where the constants of Γ are treated as variables and tσ ′ is in → R,E -normal form. Now, assume there is a reduction in (tσ ′ ) π1 . Theorem 4 shows that a reduction in (tγ) πi implies a reduction in tγ. A simplified version of that proof can be used here. Simplified since the f c functions form a free theory having no corresponding rewrite rules, thus all reductions occur in 1-terms. This implies that if there is a reduction in (tσ ′ ) π1 there is a reduction in tσ ′ which contradicts our assumption that tσ ′ is in → R,E -normal form.

Conclusions

We give the first general method for the asymmetric unification problem in the combination of disjoint equational theories. It remains to be seen if non-disjoint methods can also be extended to the asymmetric unification paradigm.

With respect to efficiency, the combination algorithm provides a significant first step to more efficient methods since, unlike a narrowing approach, we can now combine efficient special purpose asymmetric unification algorithms. In addition, it should be possible to improve the efficiency of the current algorithm. First, efficiency may be improved by adopting some of the methods introduced by Boudet [START_REF] Boudet | Combining Unification Algorithms[END_REF]. Second, It may be possible to identify specific ways of enumerating the variable identifications which do not include redundant/useless partitions. We are currently studying the question of improving the efficiency.

Briefly, the only theories that are currently known to have asymmetric unification algorithms are those with the finite variant property [START_REF] Comon | The Finite Variant Property: How to Get Rid of Some Algebraic Properties[END_REF], in which case a general algorithm known as folding variant narrowing [START_REF] Escobar | Folding Variant Narrowing and Optimal Variant Termination[END_REF] applies. This is a sizable class, including many, but not all, theories of interest to cryptographic protocol analysis, including cancellation of encryption and decryption, Inria Diffie-Hellman exponentiation, exclusive-or, and free Abelian groups. It does not include homomorphic encryption from an Abelian group to itself (see [START_REF] Comon | The Finite Variant Property: How to Get Rid of Some Algebraic Properties[END_REF] for a discussion). In many cases known characterizations of theories with the finite variant property [START_REF] Escobar | Folding Variant Narrowing and Optimal Variant Termination[END_REF][START_REF] Bouchard | On Forward Closure and the Finite Variant Property[END_REF] depend on conditions on E and R that can be checked without further reference to Σ, and so for these cases the finite variant property still holds after the addition of uninterpreted function symbols. Thus general asymmetric unification algorithms exist. Moreover, the earlier mentioned special-purpose unification algorithms for exclusive-or and free Abelian groups [START_REF] Liu | Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis[END_REF][START_REF] Erbatur | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis[END_REF] are also general. In [START_REF] Liu | Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis[END_REF] and [START_REF] Erbatur | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis[END_REF] a general strategy is presented for converting symmetric unification algorithms to asymmetric ones. This opens up an avenue for the development of special-purpose general unification algorithms for theories with and without the finite variant property as well, to which our results would also apply.

There exists an interesting connection between Asymmetric unification and Disunification. Consider a disunification problem s = t in the theory ∆ = E ∪ R over signature Σ. We can simulate this problem using asymmetric unification. First, let f and g be new function symbols added to Σ. Let f (x, x) -→ g(x) be a new rule added to R. Now s = t can be simulated by {s = ↓ u, t = ↓ v, w = ↓ f (u, v)}. Although there is some connection between the two problems they may still be independent and resolving this is an interesting open problem.

4 but not existing in Γ 4 .

 44 and is the identity on all other variables.Show that σ ′1 and σ ′ 2 are theory-preserving and injective unifiers of Γ ′ 5,1 and Γ ′ 5,2 : This follows from the construction of Γ ′ 4 , where variables violating the definitions have been removed.Show that ∀x ∈ V ar(Γ 0 ) xσ = ∆ xσ ′ : First,by the definition of σ ′ for all x ∈ Dom(σ ′ ), xσ ′ = xσ. Therefore, we need only consider the variables removed by the variable identification step. From Definition 8, for any variable x in the initial system replaced by a variable y during the identification step, xσ := yσ. Since any identifications occuring in the definition of Γ 4 must also occur in Γ ′ 4 , xσ ′ := yσ ′ = yσ = xσ. Now consider the variable identifications added to construct Γ ′ If x = y is added because xσ i = yσ i , without loss of generality assume x is replaced by y, then xσ ′ := yσ ′ = yσ = ∆ xσ. Lastly if x is replaced by y because xσ i = y, then xσ ′ := yσ = xσ.

  (a) If the least element is a variable x ∈ X then xσ ′ := xσ. (b) If the least element is a constant c ∈ C then cσ ′ := f c , i.e., f c is a constant. 2. Arbitrary element • For and arbitrary x ∈ X , let c 1 , . . . , c m ∈ C be the free constants occurring in xσ. Then xσ ′ is obtained from xσ by replacing c k by c k σ ′ (k = 1, . . . , m).

  ∀t 1 , t 2 , t 3 if t 1 → R,E t 2 and t 1 = E t 3 then ∃ t 4 , t 5 such that t 2 → * R,E t 4 , t 3 → + R,E t 5 , and t 4 = E t 5 .

RR n°8476

‡ Partially supported by the NSF grant CNS-0905222 § Supported by an ASEE postdoctoral fellowship under contract to the NRL ¶ Naval Research Laboratory University at Albany-SUNY * * Partially supported by the NSF grant CNS-0905286 † † LORIA -INRIA Nancy-Grand Est Résumé :

A Additional Proof Details

In this section we fill in some additional details from Lemma 7. This results is proven in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF], but for completeness we present the proof here with a few modifications to account for notation. Lemma 9. Let τ be a solution to a original problem Γ 0 and let τ = (τ 1 ⊙ τ 2 ). Assume there exists a pair (σ 1 , σ 2 ) such that τ i = ∆i σ i λ i . Then, τ = V ar(Γ0) ∆ σλ where σ = (σ 1 ⊙ σ 2 ) and λ := (λ 1 ∪ λ 2 )π -1 such that (λ 1 ∪ λ 2 ) is the substitution equal to λ i on Z i and the identity on all other variables. Proof. To make things simpler we can, without loss of generality, assume that σ i maps the variables in Γ i to terms containing only variables of index j (which are treated as constants by λ i ) or variables from a fresh set Z i . This can be done as follows, for all x ∈ Dom(σ i ) rename all the variables of index i in xσ i with variables from Z i . We may also assume that the domain of λ i is Z i and V ar(Γ 2 ), Z 1 and Z 2 are pairwise disjoint. We prove τ = V ar(Γ5,1)∪V ar(Γ5,2) ∆ σλ. It then can be extended, as shown in [START_REF] Baader | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures[END_REF], to V ar(Γ 0 ). We prove for any variable z occurring in yσ i that σλ and λ i π -1 coincide modulo ∆.

We proceed by induction on <. Recall that σ = σ i σ for variables of index i. Now without loss of generality lets consider a variables of index 1. Thus on y, σ = σ 1 σ and yσλ = yσ 1 σλ. If y has index 1 then the variables in yσ 1 are of index 2 or from Z 1 .

• First consider the variables of Z 1 and let z ∈ Z 1 . Since these are fresh variables, they are not in the domain of σ, thus zσλ = zλ. By the definition of λ, zλ = zλ 1 π -1 .

Let y be the least variable with respect to <. By the definition yσ 1 does not contain any variables of index 2. Thus, yσ 1 contains variables from Z 1 and for all variables z in yσ 1 , zσλ = zλπ -1 . This implies that yσλ = (yσ 1 )σλ = (yσ 1 )λ 1 π -1 = ∆ yτ 1 π -1 = (yτ ) π1 π -1 = ∆ yτ. Now let y be an arbitrary variable in V ar(Γ 5,1 ). Let y 2 be an element of V ar(Γ 5,2 ) in yσ 1 . This implies that y 2 < y and thus by induction y 2 σλ = ∆ y 2 τ and y 2 τ = ∆ (y 2 τ ) π1 π -1 = y 2 τ 1 π -1 . Since y 2 has index 2 we have that y 2 τ 1 π -1 = y 2 π -1 = y 2 λ 1 π -1 and thus y 2 σλ = ∆ y 2 λ 1 π -1 .

Therefore, for any z occurring in yσ 1 , zσλ = ∆ zλ 1 π -1 and thus