Chapter 4 Examples

This chapter aims to give a more concrete feeling of the use of logic functors. So, we here adopt the point of view of the Application Designer, which have access to a toolbox made of all the logic functors defined in appendices, and coded in Objective Caml as described in Chapter 3. The more relevant aspects of logic functors for the Application Designer are: the syntax, the operations that are defined, and the properties that are satisfied, and under which conditions.

4.1 A Logic for Logical Information Systems

In the introduction of this document, we introduced as a motivating example the description and querying of bibliographic references. In this section, we progressively develop a logic for representing both descriptions and queries. In each version, we give a definition of the logic as a module L, the definition of a description descr, and the definition of a typical query query.

As a starting point, let us consider that each reference can be described by a set of simple attributes. These attributes can be represented as atoms (logic functor Atom)), and sets of attributes can be represented by multisets of atoms (logic functor Multiset), as multisets are more general than sets. Hence the first definition of a logic for descriptions.

module L = Multiset Atom
descr: {TheJungleBook, paper-back, recent}
query: {recent, TheJungleBook}

Now we would like to have valued attributes in descriptions. Values can be either strings, or integers (logic functors Sum, String, Int); and valued attributes can be built as the product of an atom and a value (logic functor Prod). But we need to make the value optional in order to retain simple attributes in descriptions (logic functor Option).

module Val = Option (Sum String Int)
module L = Multiset (Prod Atom Val)
descr: {title is "The Jungle Book", paper-back, year = 1985}
query: title contains "Jungle"
query: {paper-back, year = 1985}

In the latter logic queries are limited in that one cannot express intervals over integers, or the presence of an attribute without specifying its type (simple, string-valued, or integer-valued). This can be solved by applying the abstractors Interval, and Top where appropriate in the definition of the logic.

module Val = Top (Option (Sum String (Interval Int)))
module L = Multiset (Prod Atom Val)
descr: {title is "The Jungle Book", paper-back, year = 1985}
query: title ?
query: {paper-back, year in 1980 .. 1990}

The expressivity of queries is still limited in that disjunction and negation cannot be expressed, and conjunction only applies to different elements of a description. In order to allow full boolean queries, both on description elements and whole descriptions, we apply twice the abstractor Prop: internally and externally to Multiset. As the syntax in functors can be parameterized (not detailed here), we can distinguish internal connectors from external connectors: external connectors are and, or, not, implies, and internal connectors are &, |, !, ->.

module Val = Top (Option (Sum String (Interval Int)))
module L = Prop (Multiset (Prop (Prod Atom Val)))
descr: {title is "The Jungle Book", paper-back, year = 1985}
query: (title contains "Jungle" & ! title contains "Wood") and
       (paper-back or not (year in 1970 .. 1980 | year in 1990 .. 2000))

We now have a convenient logic w.r.t. the expressivity of descriptions and queries. Moreover it is very easy to add value types by simply extending the definition of the sub-logic Val with other concrete domains. But before using this logic for information retrieval we must ensure it satisfies the logic properties cs_subs and cp'_subs. If we call the function L.props () in order to compute the properties of L, we discover that consistency is satisfied, but that completeness requires the property reduced' on the sub-logic starting at Multiset. It happens that the logic functor Bottom helps to ensure this property, so we can try and apply it on top of Multiset.

module Val = Top (Option (Sum String (Interval Int)))
module L = Prop (Bottom (Multiset (Prop (Prod Atom Val))))
  cs_subs requires Prod.reduced' Multiset.sg'
  cp'_subs requires Prod.reduced' Multiset.sg'

Now we get that the property sg' is required on Multiset, and the property reduced' is required on Prod. For the latter case, we can apply the same solution as above (logic functor Bottom). For the former case, it happens the logic functor Single ensures the property sg', so we apply it on top of the functor Prod.

module Val = Top (Option (Sum String (Interval Int)))
module L = Prop (Bottom (Single (Multiset (Prop (Bottom (Prod Atom Val))))))
  cs_entails is ok
  cp'_entails is ok
descr: [{title is "The Jungle Book", paper-back, year = 1985}]
query: (title contains "Jungle" & ! title contains "Wood") or
       paper-back and not (year in 1970 .. 1980 | year in 1990 .. 2000)

We finally have a well-defined logic, with a consistent and (partially) complete subsumption. Note how the user is guided in the process of defining its logic as missing requirements are provided for every property that is not satisfied. The syntax of descriptions is slightly changed as the logic functor Single requires to square-bracket formulas occuring in descriptions.

4.2 The Reconstruction of ALC-like Description Logics

Description Logics (DL) are widely used in knowledge representation and information systems [CLN98]. Like our logics, they are based on a notion of subsumption ⊑, and in fact our Initiators can be seen as an impoverished variant of DL. So, an interesting question is to know whether logic functors can be used to reconstruct description logics ? We show in this section that the subsumption test of ALC (without TBox) can be nicely reconstructed. We then generalize it as a combinator, which makes it easy to specialize ALC to concrete domains, more expressive roles, and Closed World Assumption.

The abstract syntax of the logic ALC is defined by:

where A, and r respectively stand for atomic concepts, and roles. These are properly represented by atoms (logic functor Atom). In the semantics of ALC a formula all r C is equivalent to the formula not some r not C, so that we can restrict ourselves to existential quantification. When some object satisfies a formula some r C, this means it is related to another object satisfying C, through a relation satisfying r. So the property some r C can be represented as the product (r,C) of a role, and a complex concept (logic functor Prod): its concrete syntax can easily be customized as (some r C) for readability¹. All other connectors of the language are provided by the logic functor Prop. This leads to the following first attempt of defining the logic ALC with logic functors.

module rec ALC : T = Prop (Sum Atom (Prod Atom ALC))
  cs_subs is ok
  cp_subs requires Prod.reduced Atom.reduced

The Composer produces a new logic ALC from its defining expression. Note the way it is recursively defined in order to account for complex concepts inside quantifiers. The Composer also performs its type-checking, whose result says the subsumption is proved consistent, but not complete because the property reduced could not be proved on the sub-logics built by the functors Prod, and Atom (both arguments of the functor Sum).

The above definition is correct about the syntax, but what about the interpretation domain ? According to the definition of functors (see Appendices), it is recursively defined as

I = Atom ⊎ (Atom × I),

i.e., either a primitive concept (an atom), or a pair made of a primitive role (an atom), and another interpretation. This is not satisfactory because an ALC-interpretation should not be a single atomic concept or single role, but should be a set of atomic concepts and roles. This adaptation to the interpretation domain can be obtained by the logic functor Set, whose side effect is to reduced the need for the property reduced to the weaker property reduced.right.

module rec ALC : T = Prop (Set (Sum Atom (Prod Atom ALC)))
  cs_subs is ok
  cp_subs is ok
descr: tall and
       (some child male) and
       not (some child not tall)
query: (some child male and tall) and
       not (some child not (male implies tall))

This time the interpretation domain is I = P(Atom ⊎ (Atom × I)), and the resulting subsumption prover is proved both consistent and complete by the Composer. In the formulas, the keyword some represents the existential quantifier. The example description d tells someone is tall, has a male child, and has only tall children. The example query q asks whether somebody has a tall male child, and whose male children are all tall. It can be proved in ALC that the description is subsumed by the query: d ⊑_ALC q.

We have showed our logic ALC has the same syntax as ALC, a satisfactory semantics, and proved properties w.r.t. the subsumption prover. However it remains to show whether it is semantically equivalent to the description logic ALC ? In description logics, the semantics of the subsumption relation f ⊑ g is that, for all interpretation I = (Δ_I,.^I), we have f^I ⊆ g^I, where f^I denotes the set of instances of f among the individual domain Δ_I. This inclusion can be successively rewritten as

∀ I: ∀ i ∈ Δ_I: i ∈ f^I ⇒ i ∈ g^I,

∀ i' = ( I,i): i' ⊨ f ⇒ i' ⊨ g,

M'(f) ⊆ M'(g) where M'(f) = {( I,i) ∣ i ∈ f^I}.

The last proposition is similar to our semantics of subsumption, as defined by the properties cs_⊑, and cp_⊑, except it applies on a different domain of interpretations I' = {( I,i) ∣ i ∈ Δ_I}. This implies that if we can find a pair of maps ϕ: I' → I, and ϕ': I → I' that preserve the satisfaction relation ⊨ between interpretations and formulas, then the two interpretations can be said equivalent, and ALC equivalent to ALC for the subsumption test.

Definition 7 Let I = P(Atom ⊎ (Atom × I)) be the interpretation domain of ALC, and let I' = {( I,i) ∣ i ∈ Δ_I} be the interpretation domain of ALC w.r.t. subsumption. A first map from I' to I is defined by

ϕ(( I,i))	=	{A ∈ Atom ∣ i ∈ A^I}
	∪	{(r,j) ∈ Atom × I ∣ ∃ i' ∈ Δ_I: (i,i') ∈ r^I j = ϕ(( I,i'))}.

A second map from I to I' is defined by

ϕ'(i)	=	( I(i),i)
	s.t.	Δ_I(i) = {i} ∪ ∪{Δ_I(j) ∣ (r,j) ∈ i}
		A^I(i) = {j ∈ Δ_I(i) ∣ A ∈ j}, for all A ∈ Atom
		r^I(i) = {(j,k) ∈ Δ_I(i) × Δ_I(i) ∣ (r,k) ∈ j}, for all r ∈ Atom.

The idea behind these maps is that I-interpretations are trees, where nodes are labelled by sets of atomic concepts, and edges are labelled by roles. I-interpretations can be arbitrary graphs instead of trees but, in the subsumption test, only one individual i₀ is considered at a time, only individuals accessible from i₀ are taken into account, and there is no way in ALC to say that 2 roles point to the same individual. Hence I'-interpretations can also be seen as trees, and we obtain the following theorem.

Theorem 8 For every formula in AS_ALC = AS_ALC, we verify

i ⊨ f ϕ'(i) ⊨ f, for all i ∈ I

i' ⊨ f ϕ(i') ⊨ f, for all i' ∈ I'

The proof is obtained by induction on the structure of formulas, and the interesting cases are the atomic and existentially quantified concepts.

Variations on the logic ALC

A major advantage of logic functors is that, starting from a composed logic, it is easy to adapt or extend it as it only requires changing the definition of the logic, and type-checking the result. This is in contrast with the usual approach where most often such an extension requires a full paper for presenting the new syntax, semantics, subsumption algorithm, and correctness proofs. We present in the following 3 extensions of the logic ALC: (1) concrete domains in addition to atoms, (2) complex roles (negation, conjunction, and disjunction in roles), and (3) application of the Closed World Assumption on descriptions. All these extensions are defined in one line, and require no proof from the user as they are performed automatically by the Composer.

In order to factorize these extensions, we define a combinator that define once for all the general structure of the logic ALC.

module GenALC (A : T) (R : T) (Rec : T) : T = Prop (Set (Sum A (Prod R Rec)))
module rec ALC : T = GenALC Atom Atom ALC

Unfortunately, in OCaml, recursivity cannot be used when defining a functor, but only when defining a module. This is why the additional argument Rec appears in the definition of GenALC. Then, when defining a logic, this argument is simply replaced by the name of the logic being defined.

4.2.1 Concrete Domains

In many applications, it can be useful to have concrete domains, such as integers or strings, in addition to the abstract atoms [HS01].

module rec ALC1 : T = GenALC (Sum Atom (Sum String Int)) Atom ALC1
  cs_subs is ok
  cp_subs is ok
descr: tall and
       (some name is "Peter") and
       (some age 39) and
       (some child (some name is "Arthur") and (some age 16))
query: (some name contains "Peter" or contains "Paul") and
       (some child (some age 20) or (some name any))

In ALC1, atomic concepts can now be strings, substrings, and integers in addition to classic atoms. The subsumption operation of this logic is automatically proved consistent and complete by the composer. The description d tells somebody is tall, has a name “Peter”, is aged 39, and has a child, who has a name “Arthur”, and is aged 16. The query q asks for people whose name contains “Peter” or “Paul”, and who has a child, who has a name or whose age is 20. It can be proved that d ⊑_ALC1 q.

4.2.2 Complex Roles

In previous logics, boolean operations only apply on concepts, not on roles. However papers in the litterature consider the use of negation, conjunction, and disjunction on roles [LS00]. The conjunction enables us to tell that 2 objects are related by 2 kinds of relations (e.g., friend and cousin). The disjunction helps to express undetermined or general relation (e.g., like in “father or mother is a doctor”). The negation solves the problem of expressing axioms like “Mary likes all cats” [LS00], which can be represented by all (not likes) not cat, and is opposite to all likes cat (“Mary likes only cats”).

module rec ALC2 : T = GenALC (Sum Atom (Sum String Int)) (Prop (Set Atom)) ALC2
  cs_subs is ok
  cp_subs is ok
descr: (some (cousin and friend) doctor and (some name is "Jack")) and
       not (some (not likes) cat) and
       (some has cat)
query: (some (likes or friend) doctor) and
       (some likes cat)

In ALC2 (which extends ALC1), roles can now be arbitrary boolean combinations of atoms. The subsumption operation of this logic is automatically proved consistent and complete by the composer. The description d tells somebody has some cousin and friend, who is a doctor and has name “Jack”, likes all cats, and has some cat. The query q asks for people, who likes a doctor, or has a doctor as a friend, and who likes a cat. It can be proved that d ⊑_ALC2 q.

4.2.3 Closed World Assumption

Let us consider the following description and queries in the above logic ALC1.

descr: (some name is "Peter") and not female
query: not female
query: not (some name is "Arthur")

The description is subsumed by the first query, but not by the second. This is annoying because in information systems, we like the ability to retrieve all objects not satisfying some property. Here, we get a answer to a negative query, only when this negation is explicitly stated in the description. This is known as the “Open World Assumption”, as opposed to the “Closed World Assumption”, which is usually desired in information systems. Under the latter setting, everything not said in the description is considered as false. This is usually realised through non-monotonic reasoning, which has already been introduced in description logics [DNR97]

In fact, it is possible to combine explicit and implicit negation in the same monotonic logic by using the epistemic logic AIK [Lev90]. The principle is to bracket descriptions with a modality meaning “All I know”, and query atoms with a modality meaning “I know”. We have generalized this principle as the epistemic extension, which can then be applied on various logics [Fer06]. This epistemic extension is realized through the logic functor Single, whose neat result is to enforce the property sg' (hence its name).

So, we first apply the functor Single on the logic ALC1. Then, as we need negation both inside and outside the scope of modalities, we apply again the functor Prop on the result. Finally we insert the logic functor Bottom in order to get the right properties on the subsumption operation.

module rec ALC3 : T = Prop (Bottom (Single ALC1))
  cs_subs is ok
  cp'_subs is ok
descr: [(some name is "Peter") and not female]
query: !(not female)
query: not !(some name is "Arthur")

Note we loose the full completeness of subsumption, but we still have completeness for subsumption between TELL-formulas and ASK-formulas, which is what counts in information systems. The square brackets denote the modality “All I know”, and the exclamation mark denotes the modality “I know”. The first query can be read “I know he is not a female”, and second can be read “I do not know he has name Arthur”. Both queries now subsume the description, which solves our problem. If we further assume we have a complete knowledge, i.e. everything I do not know is false, then the external negation can be read as usual negation, and the internal negation can be read as opposition. Then the first query reads “he is male (the opposite of female)”, and the second query reads “he has not name Arthur”.

1: Every logic functor comes with a parser and a printer for the concrete syntax, which can easily be customized. Syntactic sugar for the quantifier all can also be obtained.