if Ato(P1) ∩ Ato(P2) = ∅ and P1 and P2 respe
t ea
h other's hidden atoms.

The following example shows that the onditions given for ⊕ are not enough to

```
guarantee 
          ompositionality in the 
                                ase of stable models and further restri
                                                                    tions on
                                                                           

program 
        omposition be
                    ome ne
                           essary.
                                 

```

Example 4.9 Consider normal logi program modules P1 = h{a ← b.}, {b}, {a}, ∅i and P2 = h{b ← a.}, {a}, {b}, ∅i both of whi
h have stable models ∅ and {**a, b**} by symmetry. The omposition of P1 and P2 is P1 ⊕P2 = h{a ← b. b ← a.}, ∅, {**a, b**}, ∅i and SM(P1 ⊕ P2) = {∅}, that is, {**a, b**} is not a stable model of P1 ⊕ P2. 

We dene the positive dependen y graph of an smodels program module P =
hR, I, O, Hi as Dep+(P**) = Dep**+(R). Given that P1 ⊕ P2 is dened, we say that P1 and P2 are mutual ly dependent if and only if Dep+(P1 ⊕ P2) has an SCC S su
h that S ∩ Ato(P1) 6= ∅ and S ∩ Ato(P2) 6= ∅, that is, S is shared by P1 and P2 .

Denition 4.10 The join P1 ⊔ P2 of two smodels program modules P1 and P2 is P1 ⊕ P2, provided P1 ⊕ P2 is dened and P1 and P2 are not mutual ly dependent.

Example 4.11 Consider modules Hn and R
n from Example 4.2. Sin e Hn and R
n respe t ea h other's hidden atoms and are not mutual ly dependent, their join Hn ⊔ R
n = hR ∪ R′, I, O ∪ O′, {**c, d, e**}i is dened. 

```
The 
    onditions in Denition 4.10 impose no restri
                                      tions on positive dependen
                                                          ies
                                                            

```

inside modules or on negative dependen ies in general. It is straightforward to show that ⊔ has the following properties:
(i) Identity: P ⊔ h∅, ∅, ∅, ∅i = h∅, ∅, ∅, **∅i ⊔** P = P for all modules P.

(ii) Commutativity: P1 ⊔P2 = P2 ⊔P1 for all modules P1 and P2 su
h that P1 ⊔P2 is dened.

(iii) Asso iativity: (P1 ⊔ P2) ⊔ P3 = P1 ⊔ (P2 ⊔ P3) for all modules P1, P2 and P3 su h that all pairwise joins are dened.

The equality  = used above denotes synta
ti
al equality. Also note that P ⊔ P is usually undened, whi h is a dieren e with respe t to ∪ for whi
h it holds that P ∪P = P for all programs P . Furthermore, 
onsidering the join P1 ⊔P2 , sin
e ea
h atom is dened in exa tly one module, the sets of rules in P1 and P2 are distin
t, that is, R1 ∩ R2 = ∅, and also, At(P1 ⊔ P2) = At(P1) ∪ At(P2), Atv(P1 ⊔ P2) = Atv(P1) ∪ Atv(P2), and Ath(P1 ⊔ P2**) = At**h(P1) ∪ Ath(P2).

Having the semanti s of an individual smodels program module now dened, we may hara terize the properties of the semanti s under program omposition using the notion of ompatibility.

Denition 4.12 Given smodels program modules P1 and P2 su
h that P1 ⊕ P2 is dened, we say that interpretations M1 ⊆ At(P1) and M2 ⊆ At(P2) are 
ompatible if and only if M1 ∩ Atv(P2) = M2 ∩ Atv(P1).

We use natural join ⋊⋉ to 
ombine 
ompatible interpretations.