Homeomorphic embedding relations allow us to verify whether a given XML document template is somehow "enclosed" within another one.
Roughly speaking, we consider a simple embedding relation which closely resembles the notion of simulation
HHK95, this relation has been widely used in a number of works about querying, transformation, and verification of semistructured data (cf. {BS02a,BS02b,ABS00,FS98,BMG04}).
We give a definition of homeomorphic embedding,
, which is an adaptation of the one
proposed in Leu02, where (i) a
simpler treatment of the variables is considered, (ii)
function symbols with variable arities are allowed, (iii) the
relative positions of
the arguments of terms are ignored (i.e. f(a,b) is
not distinguised from f(b,a)), and (iv) we ignore the usual diving rule.
Let us illustrate the concept of the Homeomorphic embedding by means of a rather intuitive example.
Consider the following XML document templates (called s1 and s2, respectively):
hpage(surname(Y),status(professor),name(X),teaching)
hpage(name(mario),surname(rossi),status(professor),
teaching(course(logic1),course(logic2))
hobbies(hobby(reading),hobby(gardening)))
Note that s1s2, since the
structure of s1
can be recognized inside the structure of s2, while s2 can be recognized inside the structure of s1.
It is important to have an efficient implementation of homeomorphic embedding because it is used repeatedly during the verification process.