The Equivalence of Model-Theoretic and Structural Subsumption in Description Logics

1 Introduction

The nature of extensional semantics for description logics is easily grasped: given a knowledge base, concept terms are interpreted as sets of objects from some universe be­ ing modeled by that knowledge base. Thus, there is a particular world view in the form of a fixed universe that is at the root of an extensional semantic model. In contrast, an intensional semantics implies an interpreta­ tion uncommitted to the specifics of a particular world view. A related contrasting use of terminology is found when we speak of a function being defined intension­ ally as some sort of algorithm or formula, as opposed to extensionally as a set of ordered pairs. Concept algebra&, recently introduced in [Dionne et al., 1992b], pro­ vide the mathematical underpinnings for a first attempt at an intensional semantics for description logics. An element of the univer&al concept algebra is an abstract object that reflects the structural essence of a term of a description logic. The ordering of the terms in this alge­ bra corresponds to subsumption. In fact, the definition of this ordering is actually an abstract specification of structural subsumption used in description logics like K­ REP [Mays et al., 1991], LOOM [MacGregor and Bates, 1987], and CLASSIC [Borgida et al., 1989], in contrast to KRIS [Baader and Hollunder, 1991], which employs a model-based approach. This algebraic model captures the essence of subsumption as a process of structural comparison, and is defined without any use of exten­ sional models.

Bill Woods has argued eloquently for taking a more operational or intensional view of subsumption [Woods, 1991], with several examples that exhibit the confu­ sions that arise through implicit use of quantifiers. His work has motivated our development of concept algebras. Though certainly a broader approach to intensional se­ mantics is called for by Woods, concept algebras are an initial step in that direction. Another motivation for the algebraic approach was the problem of cycles. We've shown that, in elementary description logics support­ ing conjunctions of concepts, recursive definitions can be handled. This model has also been extended to han­ dle disjunctions, while still handling cycles [Dionne et al., 1992a]. Since we have not yet extended our proof of the main theorem of this paper to the model support­ ing disjunction, we will restrict ourselves to the more elementary case.

The class of concept algebras is defined using univer­ sal algebra [Jacobson, 1989]. The signature is specified using the operators for term formation in the description logic, and axioms are specified that must be satisfied by algebras in the class. Three kinds of concept algebras are of particular interest. First, there are free algebras, i.e, algebras of syntactic terms, that are generated by a set of variables that may be defined by a knowledge base, where a knowledge base is simply a set of equa­ tions equating variables with terms of the free algebra. Second, we consider quotients of free algebras by congru­ ences generated by knowledge bases. Finally we consider the univer&al concept algebra, which is given by the solution of a certain set-theoretic equation. The carrier of this algebra is a collection of non-well-founded sets, each representing the structure of a concept description. For each given knowledge base satisfying a certain weak con­ dition, there is a unique homomorphism from the corre­ sponding quotient algebra to the universal concept alge­ bra. The universal concept algebra can be thought of as the collection of all possible concepts. In [Dionne et al., 1992b], we conjectured that this algebra was the most abstract of all the greatest fixed point extensional mod­ els. In this paper, the conjecture is stated formally and proved as a theorem, thus linking this new approach with existing model theories. We claim the novelty of this algebraic approach is that the quotient algebra cor­ responding to a given knowledge base, together with its mapping to the universal concept algebra, elucidates the distinctions between descriptive and greatest fixed point semantics. This coincides with Bernhard Nebel's com­ ment [Nebel, 1990] that in descriptive fixed point models, concept names are a distinguishing feature. In fact, in a new implementation of K-REP two spaces of objects are maintained, a definition space corresponding to the quotient algebra, and a semantic space corresponding to the universal concept algebra. Two concepts might be defined with different names that classify to the same ob­ ject. Their separate definitions are kept in the definition space, yet they point to the same object in the semantic space. We feel this is a first step towards an intensional semantics that will enhance our understanding of how to implement correctly the effect of definitional changes on subsumption relations.

In the next section we discuss some related works. This is followed by a brief section describing the descrip­ tion logic we are discussing. Then, there is a section reviewing [Dionne et al., 1992b] covering the formal de­ finitions of concept algebras and of homomorphisms be­ tween them. In Section 5 we outline the construction of extensional greatest fixed point models. Next is Section 6, which contains the main result: a theorem relating the universal concept algebra to the class of extensional greatest fixed point models. The paper ends with re­ marks on intensional semantics and prospects for han­ dling negations.

2 Related Work

Various fixed point models have been investigated in [Nebel, 1990]. The problem of cyclic definitions, in roughly the same subset of description logics that we discuss here, was first solved in [Baader, 1990]. Baader views concept descriptions as automata, and couches subsumption questions in terms of language acceptance.

A use of non-well-founded sets similar to ours is made in [Rounds, 1991]. There the emphasis is on merging relational data bases, situation theory, and feature log­ ics. Our main emphasis is on subsumption of terms and the incremental maintenance of a network of terms. Our work is restricted to description logics, with emphasis placed on issues particular to them. The "complex ob­ jects" appearing in [Rounds, 1991] have both intensional and extension&l aspects, and both least upper bounds and greatest lower bounds of complex objects are examined, including a detailed explanation of how Aczel's So­ lution Lemma is used to compute the least upper bound. In our implementation we are never required actually to compute least upper bounds, since subsumption is com­ puted directly. Although our situation is, on the surface, less complex, it does not seem to be a special case of the results presented in [Rounds, 1991]. Nevertheless, the use of non-well-founded set theory to handle recursive definitions is similar.

Another algebraic approach [Brink and Schmidt, 1992], involves an equational algebra of relations act­ ing on a boolean algebra of sets, similar to the notion of a module. Though more general than concept algebras, since roles are treated as first class citizens, the details of subsumption, which amounts to equational reasoning in their algebra, are not yet worked out. Even though cycles are not considered, this work is similar to con­ cept algebras, in that the view is algebraic as opposed to model-theoretic.

3 The Representation Language

As in [Dionne et al., 1992b], we are only considering a small subset of K-REP [Mays et al., 1991], a description logic based knowledge representation language. Table 1 shows the constructs in this language, together with their abstract form and set-theoretic semantics. Though we have developed concept algebras for a larger model that includes disjunctions, and are currently pursuing nega­ tion, we restrict ourselves here to the original model. This is the model for which we prove the conjecture originally stated in [Dionne et al., 1992b]. Note that our "allsome" operator combines two operators that are normally kept separate in most description logics. The "some" operator by itself would act as a join homomor­ phism (see [Brink and Schmidt, 1992]), and one attempt at extending concept algebras to handle negations in­ volves separating the two out to make use of the clas­ sical relationship between negation and existential and universal quantification.

We assume the reader is familiar with description log­ ics. The point we wish to emphasize is that concepts are organized into an ordered structure (in this model a meet-semilattice, in [Dionne et al., 1992a] a distributive lattice), by a process called classification, whose main component is structural subsumption. One concept term subsumes another if: 1) all of its primitive components are contained in the other, 2) its roles are a subset of the roles of the other, and 3) the value restriction of each of its roles subsumes the value restriction of the other concept's role. Later this subsumption ordering will be rigorously stated in terms of the ordering of elements in the universal concept algebra.

4 Concept Algebras

Consider the signature E containing a set P of constants, a set !R of unary operators, a binary operator /\, and a constant T. Let E be the following set of axioms with respect to this signature:

We call the class of algebras for this signature E that satisfy the axioms E , concept algebra&. Using A, a partial order ~ can be imposed on a concept algebra (p ~ q iff pAq = q). The constants in Pare meet-irreducible prim­ itives and each R E ~ defines a meet homomorphism on the algebra.

Given X= {z11 ·· · , z,.} , A[X] = A[z1, ... , z,.] is the free concept algebra generated by X. A[] = A[0] is the initial concept algebra.

A KB is a set of n possibly mutually recursive defini­ tions

where ti E A[z11 ··· , z,.] . We can then let =.o. be the least congruence on A[X] that contains !::!, and then de­ fine A.o.[X] to be the quotient algebra A[X]/ ==.,o.. This is a standard construction (see [Jacobson, 1989] and [Dionne et al., 1992b] for details). Let ?r,o. : A[X] --+ A.o.[X] be the canonical projection homomorphism that sends each term to its congruence class.

For each KB, !::!, we will be interested in three relations on A[X]:

The algebra A.o.[X] captures descriptive semantics in the sense that names with structurally similar definitions are not necessarilly identified.

Definition 4.1 Given two term& s1, S'J E A[X], we &ay s1 de&criptively nb&ume& S'J, written 111 ;;;J.o. S'J 1 iff 1f.O.S1 ~A.o.(X) 'lr.O.S'J.

We next wish to construct an algebra that provides an intensional semantics for terms and that is used to define structural subsumption. There will be no variables in this algebra, and the interesting sets of equations with cycles in them have unique solutions in this semantic algebra. The universal concept algebra is the greatest fixed-point solution of the equation

where (P <wP) is the collection of finite subsets of P, and (~--=-..c) is the collection of partial functions from ~ to <w C with finite domain.

A concept definition is· composed of a collection of primitives conjoined with a collection of role definitions. Each element of C is an ordered pair whose first com­ ponent is a set of primitives from P, and whose second component is a set of ordered pairs, each arising from one of the role definitions. This set can just be represented as a partial function on ~. defined for each role in the concept's definition. Note that if we were working within standard Zermelo-Fraenkelset theory (ZFC) the only so­ lution to the above equation would be C = 0! However, a nontrivial solution C that corresponds to our intuitions exists in a consistent extension of ZFC, namely, Aczel's theory of non-well-founded sets (roughly sets that can contain themselves as members). This is how circularity of concept definitions can be supported.

To see that C is a concept algebra, we must interpret the operators of E:

Technically, to define the meet operation on C, one must do a bit more than write down this recursive definition, because it is not entirely clear that this definition leads to a well defined function. However, the recursive defini­ tion can readily be translated into a simultaneous system of equations, to which the Solution Lemma [Aczel, 1988] can be applied, and this allows us to assert the exis­ tence and uniqueness ofthe meet operation (see [Rounds, 1991]). With respect to f)., let us define what is meant by a good set of definitions.

Definition 4.2 A &et of definition& /). i& good if each z, appear& only once on the left hand &ide, and each equa­ tion Zi = t, i& of the form Zi = (1\i Ps,i )1\(f\~c(Ri,lc &s,lc)) where Pi,j E P and &i,lc E A[ X] 'Vi, j, k. In other word& each equation i& compo&ed of a conjunction of a conjunc­ tion of primitive&, and a conjunction of role term& that may or may not contain variable&.

Theorem 4.3 There ezi&t& a unique concept algebra ho­ momorphi&m A6[z1, ... , z,.] ~ C if/). i& a good set of definition&

The proof appears in [Dionne et al., 1992b]. It uses Aczel's Solution Lemma, along with some basic theorems of universal algebra (see [Aczel, 1988; Jacobson, 1989]).

Thus, we have the following picture:

Now we can define &tructural &ub&umption:

Definition 4.4 Given two term& &1, &'J E A[X], we &ay 8 1 structurally &ub&ume& 8'J, written 11 ta 8'J, iff (rt'a o ?1"6)81 ~c (rt'6 o ?1"6)82.

Thus, structural subsumption is given by the ordering on C. We now explicitly state the ordering on C, to both relate it to 1\ and the actual implementation in K­ REP. Given C1 = (Q1, !c.) where Q1 ~ P and /c 1 E (~-=--.c) and similarly for C2 = (Q:11 /c,}, we say that <"' c1 ~c c'l, if Q1 ~ Q'l, and dom(fcl) ~ dom(fc,), and 'VR E dom(fcJ , fc,(R) ~c fc,(R). This is exactly the test for subsumption of concepts stated earlier in the section on K-REP. Notice also that when C1 ~c c'l, if one inspects c1 1\ c'l, that Q1 u Q'l = Q'l and since dom(fc 1 ) ~ dom(fc, ), that fc 1 "c, reduces to the second and third cases. The third case corresponds to /c 1 (R) ~c /c,(R), and thus C1 ~c C2 iffC1/\C2 = C2.

The algorithm for computing subsumption, essentially constructs apg-like objects1 for each term of A[X] in which we are interested. Let 1) be the collection of these objects. This construction corresponds to the map I mpa in the diagram below. Each apg in 1) then describes a unique set in C via the unnamed arrow. The testing of subsumption is actually testing the presence of a Hoare simulation between the objects in C. With respect to our implementation we now have the following commutative diagram.

1 apgs (accessible pointed graphs) are pictures of non-well­ founded sets {see [Acsel, 1988])

(Our new implementation of K-REP creates two spaces of objects representing concepts. The definition &pace corresponds to Aa [X], and the &emantic &pace cor­ responds to C. Thus the definition space allows for mul­ tiple definitions that might map to the same object in the semantic space).

The fact that rt'a preserves order proves the following theorem:

Theorem 4.5 De&criptive &ub&umption implies struc­ tural &ub&umption.

This shows us that descriptive subsumption is weaker than structural subsumption, and agrees with Proposi­ tion 5.2 (page 133) in [Nebel, 1990].

5 Extensional Greatest Fixed Point Models

In this section we will define extensional, i.e., model­ theoretic, subsumption. We need to do this carefully in order to have the necessary notation to carry out the proof to be given in the next section.

If B is a concept algebra and a : X -+ B, then 0:: A[ X] -+ B is the unique homomorphism that extends the definition of a on X to the free algebra A(X]. The effect of applying 0: to a term s E A[X] is to substitute in 6 for occurences of variables corresponding to values from B specified by a: X-+ B.

From a formal point of view, a knowledge base

i& a function /).:X -+ A[ X], where /).:z:i = t,. The func­ tion /). induces a transformation Kll a: Bx -+ Bx de­ fined by Kll,Ba = 0: o !)., for all a: X__:. B. A fixed point of Kll,B is exactly what is meant by a solution in the concept algebra B to the system of equations

As a general reference on ordered sets, we suggest [Davey and Priestley, 1990]. Let L and M be complete lattices. A function from L to M is Scott continuous if it preserves sup's of directed subsets of L. Iff: L -+ Lis Scott continuous, then the Tarski-Scott Fixed Point The­ orem asserts that f has a least fixed point, and this least fixed point is given by V n>o(f" ..L). However, extensional subsumption is defined using greatest fixed points, so we need a dual notion of continuity. A function from L to M is dually Scott continuous if it preserves inf's of filtered subsets of L. The Tarski-Scott Fixed Point Theorem im­ ples that, iff: L -+ L is dually Scott continuous, then f has a greatest fixed point, and this greatest fixed point is given by An>o(F'T).

To build an extensional greatest fixed point model in the context of a knowledge base~: X-+ A[ X], we start with a universe U. Then we interpret the primitives as subsets of U and the roles as binary relations on U. Using these interpretations, and guided by Table 1, we endow the power set B = 'lf' with a concept algebra structure. Of course, B is a complete lattice under is set inclusion. Furthermore, each of the concept algebra operators turns out then to have a dually Scott continuous interpretation as an operation on B. Since B is a complete lattice, so also is the set Bx, ordered pointwise. Since the opera­ tions on B are dually Scott continuous, it follows that K 6 ,a: Bx -+ BX is also dually Scott continuous. Hence, KLl,B has a greatest fixed point {3: X -+ B. The exten­ sional greatest fixed point model for A[X] is then the homomorphism

It is conventional to denote by sM = {Js the subset of U assigned to a term s by an extensional greatest fixed point model M .

Definition 5.1 Given two terms s1 , s2 E A[X], we say s 1 extensionally subsumes s 2 (written s1 2Ll s2} iff, for all extensional greatest fixed point models M, sf 2 s~.

The remainder of this section is devoted to a closer look at a fixed extensional greatest fixed point model {3: A[X]-+ B. Note that the maximum element of Bx is the function f3o: X-+ B given by f3oz = U, for all z EX. If we inductively define f3n: X -+ B by f3n+l = KLl,Bf3n for each nonnegative integer n, it follows that f3o 2: f3t > f32 2: · · ·, and f3 = Anew f3n· Upon realizing that BA X~ ordered pointwise, is a complete lattice, it is not hard to prove the following proposition.

In keeping with our conventions, the unique homomor­ phism extending ~:X -+A[ X] is 6.: A[X]-+ A[ X].

Proposition 5.3 For all nonnegative integers n, fJn+l = rJn 0 6..

Proof. This follows easily by considering the commu­ tative diagram

0

Corollary 5.4 For all nonnegative integers k, fJ Anew(rJn ° 6_Jc).

6 Concept Algebras and Greatest Fixed Point Models

In this section we will prove Theorem 6.3, which as­ serts that structural subsumption is equivalent to model­ theoretic subsumption. This theorem was first posed as a conjecture in [Dionne et al., 1992b]. Roughly speaking, it states that structural subsumption in the algebra C is the most abstract of all the greatest fixed point models. By "most abstract" we mean that if a subsumption holds inC, then it holds in all greatest fixed point models, and conversely. In fact it appears that a stronger statement can be made about finite models, which we will discuss later as a new conjecture.

Let ~:X-+ A[ X] be some fixed knowledge base that is a good set of definitions. To simplify notation, let p be the intensional model described in Section 4 that corresponds to ~- Thus, p = I()Ll o 'Kfl : A[X] -+ C. When the homomorphism p is restricted to the set X of knowledge base variables, we obtain p: X -+ C, which gives the unique solution in C to the system of equations ~ = {z1 = t1, ... , Zn = tn}· Since pis the unique fixed point of KLl,C, it follows that p = p o ~- By considering the diagram

we see that p = p o 6..

For each t E A[X], let depth t be the length of the longest role chain in t. (Note that depth t is a purely syntactic notion that is independent of ~- One could not similarly define the depth of an element of A6 [X] because in that algebra there may be infinite role chains.)

Most of this section is devoted to the proof of the next proposition, which is fairly technical. Its proof can be skipped on a first reading. The proof of the proposition is based on the following algebraic fact: since A[X] is a free algebra, each term in it has a unique decomposition in the sense that, for each t E A[X], there exist uniquely determined sets Qt ~ P and Vi ~ X and a uniquely determined finite partial function Ft E ~___:__. A[X] such <., that

Thus, the fact that ~ is a good set of definitions can be stated succinctly as (Vz )(VLl., = 0).

Proposition 6.1 Let M = {3: A[ X] -+ B be an exten­ sional greatest fixed point model, where B = 'lf'. For each integer n, let the homomorphi1m /3n: A[X] -+ 8 be defined as in Section 5. For all nonnegative inte­ gers n and k, if t, t' E A[X] sati&fy pt = pt' and k = max{ depth t', max{ depth ~z I z E X}}, then /Jn+k+lt ~ /i.t' ·

Proof. We will use a double induction on nand lc. Case 1: n = k = 0. Given t, t' E A[X], we need to show that {31t ~ /Jot'. Since depth t' = 0, it must be that

Note that Pot' = 1\ Qt· since /Joz = T, and pt = pt' implies p(~t) = p(~t'). Since k = 0,

Now we have p(lit) =

from which it follows that p(&t) =

where Gt(R) =

So, p(flt) = p(flt') implies

Therefore /J1t = /Jo(~t) = /Jo[AQt A 1\.,ev, (AQ£~..,) · · ·] ~ /Jo(AQt·) =/Jot'

Case 2: Suppose the proposition is true if n = 0 and Vk < j. Consider the case k = j, n = 0. We need to show that /3; +1 t ~ /Jot'. As in the base case,

and similarly for t'. Again, we have that pt = pt' implies p(lit) = p(lit'). So, p(~t) =

and p(flt') =

A/\{R (Gt·R) IRE domFt· uu.,'EV,, domF£~,.,·}),

where Gt' is defined the same way as Gt. Note that: max{ depth Gt·(R), max{ depth ~z' I z' E Vi·}} < j Thus, separating the action of p on t, t' into its primi­ tive and role components allows us to use the induction hypothesis, so that {3;+1t =

Case 3: n = m, k = 0 where the proposition is true for all n < m. We need to show that /Jm+l ~ /3mt'. The action of p on t and t' are the same as in the previous cases, so we'll just sketch the main argument. Observe that /Jm+1t =

Since k = 0, application of the induction hypothesis yields

Case 4: n = m, k = j where the proposition is true for all n < m and k < j. We need to see that /Jm+i+lt ~ /3mt'. We have /Jm+i+lt =

Therefore, by the induction hypothesis, /Jm+Hlt ~

This proves Proposition 6.1. D

Lemma 6.2 Let ,B be the greate&t fized point of KA,B for an arbitrary algebra 8 of &ets corresponding to 1ome model. For all t, t' E A[X] pt = pt' implies {3t = /3t'.

Proof. Suppose that pt = pt'. By the preceding propo­ sition,

The reverse inequality is proved similarly. D

Proof. The proof in the "if" direction is a direct conse­ quence of a Stone-like representation theorem, that every meet-semilattice is isomorphic to a meet-semilattice of sets (see pp. 82 of [Davey and Priestley, 1990]). It is easy to see that this implies that C is isomorphic to an extensional greatest fixed point model.

For the "only if" direction, suppose we have an ar­ bitrary greatest fixed point model M = {J: A[ X] --+ B, where B = 'i" . To prove that &t ta 8'J =? &t 2a sl, 'V8t, 82 E A[X], we argue as follows:

Since M is arbitrary, this implies &t 2a 82, and this proves Theorem 6.3. 0

It appears that more can be said about the "only if" direction of this proof. Namely that if two terms do not subsume one another in the universal concept algebra C, then it appears that one can construct a finite model that exhibits this failure. The intuition comes from ob­ serving that if one concepts fails to subsume another, then it is for one of three reasons. Either they disagree on primitives, or the subsuming concepts roles are not a subset of the subsuming concepts roles, or they disagree on some value restriction. The third case eventually re­ duces to either the first or the second, and even in the cyclic cases, that clearly give rise to infinite chains, some finite piece is sufficient. However this reasoning is hardly a proof and since we've proved one conjecture already we'll finish with another.

Conjecture 6.4 Given two term& 81 1 82 E A[X]

81 ta s2 iff s1 2a 82 iff sfA 2 8~ V finite model& M.

7 Conclusion

This paper has shown that structural subsumption as computed in the universal concept algebra, and sub­ sumption in all greatest fixed point models, are essen­ tially the same. Therefore, for purposes of subsumption testing, one need not appeal to extensional models. This appears to be a first step towards intensional semantics, in the larger sense, as advocated in [Woods, 1991]. Con­ cepts are seen as just descriptions. Their relationships, via subsumption, to other concepts is a structural com­ parison process. Each concept in K-REP gives rise to two objects: a definitional one in A a [X] and a semantic one in C.

Currently we are working on extending concept alge­ bras, which now include disjunctions (see [Dionne et al., 1992a]), to include negation while still handling cycles. One approach might make use of the fact that a finite distributive lattice is a Heyting algebra, in which one can define negation in terms of disjunction. Another ap­ proach would be to use boolean algebras, in which case normalization in the presence of cycles is problematic.