

![0_image_0.png](0_image_0.png)

We can now introduce the notion of unfolding of an ALUNI interpretation.

Definition 5.8 Let S be an object-oriented schema, ψ(S) its translation in ALUNI and I
a finite interpretation of ψ( S ). We call unfolded version of I the interpretation obtained from I as follows: For each individual v that is part of a bad cycle, unfold the bad cycle into an (infinite) tree having v as root, by generating new individuals only for the instances of RecType and SetType. For a nonnegative integer m, we call m-unfolded version of I,
denoted as I m , the interpretation obtained by truncating at depth m each infinite tree generated in the process of unfolding. Example 5.6 (cont.) Figure 10 shows the unfolded version of the model in Figure 9. Notice that only the bad cycle has been unfolded to an infinite tree, and that all arcs labeled with a3 lead to o2 , which is an instance of AbstractClass and has not been duplicated.

The correctness of ψ( S ) is sanctioned by the following proposition.

Proposition 5.9 For every object-oriented schema S of depth m, there exist mappings:

1. as from instances of S into finite interpretations of ψ ( S ) and αν from active values of instances of S into domain elements of the finite interpretations of ψ(S) such that:
For each legal instance I of S, α S ( J ) is a finite model of ψ ( S ), and for each type expression T of S and each v E V T , v E T I if and only if av(v) E (ψ(T))αs(I)
2. Bs from finite interpretations of ψ ( S ) into instances of S and By from domain elements of the m-unfolded versions of the finite interpretations of ψ(S) into active values of instances of S , such that: For each finite model I of ψ(S), β S ( I ) is a legal instance of S , and for each concept ψ ( T ), which is the translation of a type expression T of S and each d E A T Im , d E (ψ(T)) Tm  if and only if βv(d) E T βs(I)
(1) Given a database instance I we define an interpretation α S ( I ) of ψ( S ) as Proof.

follows: