The FunDL family of description logics replace roles with partial functions (features) and have a concept constructor called a path functional dependency (PFD) that can be used to capture a variety of equality-generating dependencies commonly part of conceptual designs as well as schemata of object-relational data sources. Recent work has considered replacing the PFD concept constructor with a more general path description dependency (PDD) in which inverse features are now allowed in characterizing feature path reachability in interpretations. This leads to a circumstance in which the value of a feature path for a given entity might be set-valued. This work has focused on cases in which feature path agreement is based exclusively on either a set intersection semantics or a non-empty set equality semantics. In this paper, we consider a mixed mode case for PDDs in which individual component feature paths can be assigned either of these options. Our main results are that this flexibility makes logical consequence undecidable in general, but that restricting an arbitrary mixed-mode for PDDs to conform to a mode-typing assignment on features re-obtains EXPTIME completeness for logical consequence.
Given a query over a conceptual ontological design for some domain, there are many circumstances in which reasoning about equality generating dependencies is essential in finding an eficient plan over available backend structured data sources such as relational databases, e.g., in resolving identity issues for entities in an underlying domain [1, 2], or in determining when explicit duplicate elimination in query plans is not required [3]. The FunDL family of description logics [4] has been developed largely for this purpose and therefore replace roles with partial functions (features) to better align with the ubiquitous notion of an attribute or column value and have a concept constructor called a path functional dependency (PFD) that can be used to capture a variety of equality-generating dependencies needed to resolve identity issues or are commonly part of schemata for structured data sources such as keys and (relational) functional dependencies.
Recent work [5] has introduced a new dialect for FunDL called set-ℒℱ ℐ that replaces the PFD concept constructor with a more general path description dependency (PDD) in which inverse features are now allowed in characterizing feature path reachability in interpretations, leading to a circumstance in which the value of a feature path for a given entity might be set-valued. This work has explored alternative semantics for PDDs, with a focus on cases in which feature path agreement is based exclusively on either a set intersection semantics or a non-empty set equality semantics, showing in both cases that allowing more general PDDs in place of PFDs does not change the complexity of logical consequence in any of the Boolean complete FunDL dialects, which remain EXPTIME complete in the worst case.
The primary incentive for set-ℒℱ ℐ stems from an outline of future work in [6] which recognized the need for plural entities in formally capturing JSON arrays, in particular, for the more general expressiveness of PDDs to capture how such array entities can be identified.
The following inclusion dependencies are derived from a running example in [5] and illustrate this (where also CLIENT-FRIEND ⊑ CLIENT is assumed):
CLIENT-FRIEND ⊑ CLIENT : firstname ∩, (phone-dom− .phone-ran.dialnum)∩ → id ∩ CLIENT-FRIEND ⊑ CLIENT : (phone-dom− .phone-ran.dialnum)≈ → id ≈ Feature path reachability in the dependencies corresponds to four path descriptions (PDs): “firstname ”, “phone-dom− .phone-ran.dialnum” and “id ”. The first and last are PDs that also qualify as path functions (PFs) since their interpretations will be partial functions. The first dependency employs a PDD on its right-hand-side with set intersection semantics (indicated by the “∩” superscript on PDs) to express a key or uniqueness condition for any client that is also a friend: among all clients, they will have a unique combination of a first name and the dial number of any of their phones . The second employs a PDD on its right-hand-side with non-empty set equality semantics (indicated by the “≈ ” superscript on PDs) to also express a key or uniqueness condition: among all clients with at least one phone, they have a unique set of dial numbers.
Including both dependencies in a TBox has so far not been possible since this requires two distinct modes for the PD “phone-dom− .phone-ran.dialnum” in a PDD that appeal to both set intersection and non-empty set equality semantics for PD agreement, a circumstance now enabled by introducing annotated PDs in which a superscript arbitrates between a choice of semantics. Indeed, our primary concern in this paper is to study logical consequence for a new member of the FunDL family called set-ℒℱ ℐ in which PDDs now allow annotated PDs as components. Our main results are that, unlike earlier work, this flexibility makes logical consequence undecidable in general, but that restricting an arbitrary mixed-mode for PDDs to conform to a mode-typing assignment on features re-obtains EXPTIME completeness for logical consequence for all members of the FunDL family.
The remainder of the paper proceeds as follows. Section 2 introduces the relevant definitions, previous results and open questions regarding set-ℒℱ ℐ that have motivated this paper. Section 3 shows the undecidability of entailment in set-ℒℱ ℐ when a mixed semantics for path agreements is used. Section 3.1 shows how decidability can be regained by imposing a mild typing discipline on path agreements. Section 4 concludes the paper and outlines directions for further investigation.
In this section we define the description logic set-ℒℱ ℐ. We start with defining primitive features and concepts, and how they are interpreted: Definition 1 (Vocabulary of set-ℒℱ ℐ). Let F and PC be sets of feature names and primitive concept names, respectively. Semantics is defined with respect to a structure ℐ = (△ℐ , · ℐ ), where △ℐ is a domain of objects or entities and · ℐ an interpretation function that fixes the interpretations of primitive concept names ∈ PC to be subsets of △ℐ and feature names ∈ F to be partial functions ℐ : △ℐ → △ℐ .
The primitive syntax and semantics is now extended to Path Descriptions and (eventually) to Concept Descriptions: Definition 2 (Path Descriptions in set-ℒℱ ℐ). A path description is defined by the grammar
Pd ::= id | . Pd | − . Pd, for ∈ F, where − is called the inverse of , with the stipulation that substrings of the form . − and − . do not appear in any path description Pd. Let ℐ be an interpretation. Then the interpretations of path descriptions Pd are functions Pdℐ : 2△ℐ → 2△ℐ over the powerset of △ℐ defined as follows, where ⊆ △ ℐ : ⎧ if Pd = “ id”, ⎪ Pdℐ () = ⎨ Pd1ℐ ({ ℐ () | ∈ }) if Pd = “. Pd1”,
⎪⎩ Pd1ℐ ({ | ℐ () ∈ }) if Pd = “ − . Pd1”. ::= A
Aℐ ⊆ △ ℐ △ℐ ∖ ℐ 1ℐ ∩ 2ℐ 1ℐ ∪ 2ℐ { | ℐ () ∈ ℐ }
Path Descriptions that do not contain inverse features are called path functions. Before we define concept descriptions of set-ℒℱ ℐ, we need the notion of path description agreement; this agreement is parameterized by how the results of applying a path description on a pair of objects are compared. We define and explore three possibilities here, the set equality, the non-empty set equality, and the set intersection based agreements. Formally: Definition 3 (Path Description Agreement). Let ℐ be an interpretation and 1 and 2 be two △ℐ elements. We say that 1 and 2 ∼ -agree on Pd, written Pd(1) ∼ Pd(2), if • Pdℐ ({1}) = Pdℐ ({2}) (set equality), when ∼ is “=”, • Pdℐ ({1}) = Pdℐ ({2}) ̸= ∅ (non-empty set equality), when ∼ is “≈ ”, and • Pdℐ ({1}) ∩ Pdℐ ({2}) ̸= ∅ (set intersection), when ∼ is “∩”.
We use the Path Description Agreements (defined above) to define the logic set-ℒℱ ℐ as follows: Definition 4 (Concept Descriptions, Subsumptions, and TBoxes in set-ℒℱ ℐ). A concept description is constructed from primitive concepts using Boolean concept constructors ⊓, ⊔, and ¬, value restrictions on features ∀., unqualified existential restrictions on features and inverse features ∃ and ∃ − , and the path description dependency (PDD) of the form
: Pd∼1 1 , ..., Pd∼ → Pd∼ .
The semantics of all the derived concept descriptions is defined in Figure 1 where GD(Pd()) is • true (unconstrained), when ∼ is “=”, and • Pdℐ () ̸= ∅ (non-empty), when ∼ is “≈ ” or “∩”.
A subsumption is an expression of the form 1 ⊑ 2, where the are concepts, and where PDDs occur only in 2 but not within the scope of negation.1 A terminology (TBox) consists of a finite set of subsumptions, and a posed question is a single subsumption. An interpretation ℐ satisfies a subsumption 1 ⊑ 2 if 1ℐ ⊆ 2ℐ and is a model of , written ℐ |= , if it satisfies all subsumptions in . Given a terminology and posed question , the logical consequence problem asks if is satisfied in all models of , written |= . □
Observe that the proposed logic lacks qualified existential restrictions. Indeed, entailment for partial-ℒℱ ℐ with qualified existential restrictions over inverse features was shown in [ 9] to be 1Violating this latter condition leads immediately to undecidability [7, 8]. undecidable, which will therefore also be the case with set-ℒℱ ℐ. However, for a feature , one can substitute the subsumption ⊑ ∃. with two subsumptions ⊑ ∃ and ∀. ⊑ , which completely characterizes the behaviour of the qualified existential restriction. Note that an analogous substitution for ⊑ ∃ − ., namely ⊑ ∃ − and ∀. ⊑ , will only partially capture the behaviour of an existential restriction for inverse features, a limitation needed to regain decidability of entailment. In the remainder of the paper, we allow using ∃Pd. to serve as a shorthand for applying the above substitutions systematically on Pd by splitting the Pd to individual features and introducing auxiliary primitive concepts.
One may wonder if the additional guards GD(Pd()) and GD(Pd()) imposed on the consequent path descriptions in a PDD are needed with the {∩, ≈} adornments. Consider the following pair of subsumptions, for each 0 < ≤ , ≥ 2:
⊑ : ()∩ → ( − .)∩ and ∀.⊤ ⊑ .
It is easy to see that these pairs of subsumptions entail ⊑ ∃ − .. In the absence of the guards in the PDD semantics one can add subsumptions ⊓ ⊑ ⊥ for ̸= that will force every individual to have a distinct predecessor for each . This leads immediately to undecidability without guards since it allows one to simulate qualified existential restrictions over inverse features [ 9]. Note that including the guards with a PDD ensures that a right-hand-side will not “force” path existence.
The above definition of PDDs can be specialized in several ways, some of which have been considered in the past.
1. In [5] we have considered the set intersection semantics for set-ℒℱ ℐ, a semantics in which the ∼ agreements in all PDDs were defined as “ ∩” (non-empty set intersection). However, we have required that all the path descriptions involved in any PDD must exist before the PDD applies, i.e., the semantics was defined as ( : Pd1, ..., Pd → Pd)ℐ = { | ∀ ∈ ℐ : Pdℐ ({}) ̸= ∅ ∧ Pdℐ ({}) ̸= ∅ ∧
(⋀︀=1 Pdℐ ({}) ∩ Pdℐ ({}) ̸= ∅) → Pdℐ ({}) ∩ Pdℐ ({}) ̸= ∅}.
Under the set intersection semantics, the logical consequence problem for partial-ℒℱ ℐ, and consequently its derivative set-ℒℱ ℐ, is EXPTIME-complete. We have shown that the problem is in EXPTIME by constructing a two-tree model and then reducing to the satisfiability of an Ackermann formula encoding the logical consequence problem. Completeness then follows from EXPTIME-hardness of the implication problem for the {D1 ⊓ D2, ∀.D1} and {⊤, ⊤ : Pf1, Pf2 → Pf} fragments of FunDL [10]. 2. Also in [5], we have considered the set equality semantics for set-ℒℱ ℐ, a semantics in which the ∼ agreements in all PDDs were defined as “ =”, ( : Pd1, ..., Pd → Pd)ℐ = { | ∀ ∈ ℐ : (⋀︀=1 Pdℐ ({}) = Pdℐ ({})) → Pdℐ ({}) = Pdℐ ({})}.
We have shown that under the set equality semantics, the ability to assert equality of non-existent paths in a PDD’s precondition allows us to create nominal-like concepts which leads immediately to undecidability.
EXPTIME-complete (new)
Undecidable (new) EXPTIME-complete (new) 3. To regain decidability under the set equality semantics, we preclude the equality of empty sets by a non-empty set equality semantics defined as follows, which brings the complexity back to EXPTIME-complete. The proof for non-empty set equality semantics is essentially the same as the one for set intersection semantics [5].
In this paper we consider the remaining possibilities (some of which were posed as open problems). 4. We have conjectured that mixing the set intersection and non-empty set equality semantics, both of which are decidable, could lead to undecidability. In this paper, we show that allowing combinations of the EXPTIME-complete semantics in the PDs leads to undecidability by reduction of the unconstrained tiling problem. Note that for path functions there is no diference between the set intersection agreements and non-empty set agreements; hence we omit the type of the agreement in the remaining constructions for path functions. 5. Curiously, we can restrict arbitrary mixed semantics by virtue of fixing the type of semantics for each feature and inverse feature − , which generalizes to PDs. In Section 3.1, we show that adopting such typed mixed semantics allows us to regain EXPTIME-completeness. We summarize the complexity results for set-ℒℱ ℐ based on various combinations of set intersection and set equality-based semantics in Figure 2.
In this section, we show that allowing both non-empty set equality and set intersection semantics simultaneously in the PDDs leads to undecidability by reduction of a tiling problem that allows one to simulate runs of a Turing Machine on an empty input tape, a problem that is known to be undecidable [11]. An instance of the tiling problem is a triple (, , ), consisting of a set of tile types and , ⊆ × two binary relations. A solution to is a function : N × N → such that, for < , we have ((, ), ( + 1, )) ∈ and ((, ), (, + 1)) ∈ . This tiling solution covers an infinite triangle of successive longer and longer tapes (instantaneous descriptions) and this way simulates a run of a given Turing Machine2. We construct a terminology along with a posed question, denoted (, , ), for a given tiling problem , in the following steps.
Theorem 5. An instance (, , ) of the unconstrained tiling problem admits a solution if and only if (, , ) ̸|= A ⊑ : → id for a (, , ) TBox corresponding to the instance (, , ). Proof (sketch): Given a tiling problem (, , ) we construct a TBox (, , ) that utilizes pairwise disjoint primitive concepts A, B, and C to serve as grid points and an auxiliary diagonal primitive concept D. We assume that the features , , ℎ, and are total, and the inverse − is total on A, B, C, and D. These are captured by (, , ) subsumptions 2The reduction is essentially the same as for the classical tiling of a full quadrant, but starts with an empty tape.
↑ ↖ A ↑ A ↑ A ↑ A ↑ A
→ ← → ← → ←
D ↑ ↖ B ↑
B ℎ → ← ℎ C ↑ ↑
D ↑ ↖ →
B ℎ → ← ℎ C → ← A ↑ ↑ ↑ → ←
B ℎ → ← ℎ C → ← A → ←
D
→ D ℎ → ↑ ↖
D → ↑ ↖
B
(and ∀.B ⊑ B, ∀.C ⊑ C)
(
A ⊓ B ⊑ ⊥, A ⊓ C ⊑ ⊥, A ⊓ D ⊑ ⊥, B ⊓ C ⊑ ⊥, B ⊓ D ⊑ ⊥, C ⊓ D ⊑ ⊥.
To show the non-entailment we need to construct a counterexample to the posed question, A ⊑ : → id that satisfies all subsumptions in (, , ). We construct the TBox (, , ) for an instance of a tiling problem (, , ) in such a way that the counterexample will correspond to a solution to this tiling problem. In what follows we list all the subsumptions needed in (, , ) to achieve this goal. The subsumption
A ⊑ D : → ( − .)∩ (and B ⊑ D : → ( − .ℎ)∩, C ⊑ D : → ( − .)∩), stating that A and D that agree on must ∩-agree on − . (and that B and D that agree on must ∩-agree on − .ℎ and C and D that agree on must ∩-agree on − ., respectively), the subsumption A ⊑ D : ( − .)≈ → id (and B ⊑ D : ( − .ℎ)≈ → id , C ⊑ D : ( − .)≈ → id ), stating that A and D above must ≈ -disagree on those paths, in order not to equate an A object with an D object (and similarly for B and D, and C and D, respectively), together with subsumption extending the A (and similarly B and C, respectively) class memberships along predecessors and subsumptions ensuring those predecessors–with respect to a particular class membership–are unique,
D ⊑ D : → id , A ⊑ A : → id ,
(and B ⊑ B : → id , C ⊑ C : → id ),
force this counterexample to look like the first three top rows in Figure 3 (with the exception of class
membership of the final two objects in the third row). Note that the A object’s predecessors are also
A objects due to (
The now existing horizontal right neighbours of the object A in the 3rd row are assigned concept membership using the following subsumptions:
A ⊑ ¬B : →
B ⊑ ¬D : →
(and B ⊑ ¬C : ℎ → , C ⊑ ¬A : → );
(and C ⊑ ¬D : → , A ⊑ ¬D : → ),
i.e., the right (.− ) neighbour of A must be B, etc. In particular, the object D at the end of row 2 must
have exactly two incoming features, one from an B and second from a D objects. This completes the
construction of the top three rows in Figure 3. To replicate this process for row 4 in Figure 3 we use the
second subsumptions in (
To complete the left part(s) of the grid–the squares below A, B, and C objects we use the following subsumptions:
A ⊑ B : . →
(and B ⊑ C : .ℎ → ℎ, C ⊑ A : . → );
Analogously, the 3rd subsumptions in (
A ⊔ B ⊔ C ⊑ ⊔∈ T, T ⊓ A ⊑ (T ⊓ B) : → id , T ⊓ B ⊑ (T ⊓ C) : ℎ → id , T ⊓ C ⊑ (T ⊓ A) : → id , ∀(, ) ∈/ , ∀.(T ⊓ A) ⊓ T ⊑ ⊥, ∀.(T ⊓ B) ⊓ T ⊑ ⊥, ∀.(T ⊓ C) ⊓ T ⊑ ⊥, ∀(, ) ∈/ .
In summary, a TBox (, , ) containing all the subsumptions (
The existence of a non-terminating computation of a given Turing machine starting with an empty tape can now be witnessed by the existence of a tiling using the standard encoding of instantaneous descriptions of the TM’s computations as rows in the tiling overlayed over Figure 3; the computation steps then correspond to the consecutive rows of tiles. Note that tiling of the infinite triangle is suficient as the TM’s head can move at most one cell to the right for every step of the computation. □
Alternatively, to tile a full quadrant, we can use the vertical -antichains as columns (as above) and
diagonals starting from the left-most A-labelled column as rows. This needs a slight adjustment to the
horizontal tiling subsumptions (
We observe from the previous section that inconsistent semantics for two instances of the same PD leads to undecidability. In this section, we show that under a restricted form of the mixed semantics, called the typed mixed semantics, set-ℒℱ ℐ regains EXPTIME-completeness. The idea of enforcing a type restriction is to make the semantics of path agreements consistent among PDs ending with the same (inverse) feature. This type restrictions preserves the two-tree property of set-ℒℱ ℐ under the set intersection and non-empty set equality semantics.
Definition 6 (Type Restriction). Let be a set-ℒℱ ℐ TBox and a posed question. Let end(Pd) denote the last (inverse) feature of Pd. We say that and are type restricted if for any pair of PDs Pd∼1 1 and Pd∼2 2 in ∪ , we have ∼ 1, ∼ 2 ∈ {≈ , ∩} and
end(Pd∼1 1 ) = end(Pd∼2 2 ) implies ∼ 1=∼ 2 .
The typed mixed semantics immediately follow from the syntactic type restriction on all PDs in the TBox and posed question.
Theorem 7. Let be a set-ℒℱ ℐ TBox and a posed question, where ∪ are type restricted. Then the logical consequence problem |= is complete for EXPTIME.
Proof (sketch): To establish the EXPTIME bound, we reduce the logical consequence problem to checking the unsatisfiability of an Ackermann formula [ 12] in a similar fashion as in [5]. First, we show that if there exists a counterexample ℐ for |= , then we can construct a two-tree counterexample by unravelling ℐ. Note that under the imposed type discipline, there is only one form of path agreement applicable to any symmetric pair of individuals in the two-tree unravelling of ℐ and therefore there is no longer any need feature agreements that go beyond the symmetric agreements generated by PDDs. Since we can check the (un)satisfiability of the constructed Ackermann formula in EXPTIME [ 13], the same bound applies to the logical consequence problem for set-ℒℱ ℐ. □
The paper explores the computational complexity of logical consequence for a new member of the FunDL family of descriptions logics called set-ℒℱ ℐ. This new dialect introduces a PDD concept constructor for capturing a richer variety of equality generating dependencies under arbitrary combinations of set intersection semantics and non-empty set equality semantics for path agreements in component path descriptions. In particular, the paper shows that an unconstrained option for choosing either semantics makes logical consequence undecidable. This is in contrast to the two cases where one or the other semantics is chosen exclusively for a given TBox which has been shown decidable in earlier work. The paper then proposes a typing discipline on path agreements to regain decidability, thereby accommodating some form of mixed-mode semantics for PDDs occurring in a given TBox.
There are four main directions for further inquiry: 1. Adding arbitrary PDL-style test concepts [14] in path descriptions. In the case of PDDs this means adding concepts of the form (1, 2)?, stating that for a path agreement to hold, the paths from the two objects, and , in the PDD constructor must simultaneously pass through an individual that belongs to 1 and 2, respectively. We conjecture that adding such test concepts to path descriptions in set-ℒℱ ℐ will not change the computational properties of the logic. 2. Studying additional or alternative notions of path agreement in set-ℒℱ ℐ. For example, the set intersection semantics of path agreements can be generalized by requiring the intersection to be of a certain cardinality (e.g., at least two or a majority of paths agree). We conjecture that such extensions will again lead to undecidability of entailment. 3. Studying set-ℒℱ ℐ fragments with preferable computational properties, such as various Horn fragments. This direction suggests the use of (perhaps limited) PDDs in FunDL-Lite logics [4]. 4. Using PDD constructs in plural entity identification . While our introductory example has already sketched such a use case, the full consequences of using path descriptions in place of path functions are yet to be explored. [10] D. Toman, G. Weddell, On Attributes, Roles, and Dependencies in Description Logics and the Ackermann Case of the Decision Problem, in: Description Logics 2001, CEUR-WS vol.49, 2001, pp. 76–85. [11] J. Hopcroft, J. Ullman, Introduction to Automata Theory, Languages and Computation, Addison
Wesley, 1979. [12] W. Ackermann, Uber die Erfullbarkeit gewisser Zahlausdrucke, Mathematische Annalen 100 (1928) 638–649. [13] M. Fürer, Alternation and the Ackermann Case of the Decision Problem, L’Enseignement Math.
27 (1981) 137–162. [14] M. J. Fischer, R. E. Ladner, Propositional dynamic logic of regular programs, J. Comput. Syst. Sci. 18 (1979) 194–211.