Previous Up Next

Chapter 2  Logics and Logic Functors

If an Application Designer has to define a customized logic by the means of composing primitive components, these components should be of a “high-level”, so that the resulting logic subsystem can be proven to be correct. Indeed, if the primitive components are too low-level, proving the correctness of the result is similar to proving the correctness of a program. Thus, we decided to define logical components that are very close to be logics themselves. So doing, we abandon computational expressivity, but we will see that proving correctness is no more than type-checking.

Our idea is to consider that a logic interprets its formulas as functions of their atoms. By abstracting atomic formulas from the language of a logic we obtain what we call a logic functor. A logic functor can be applied to a logic to generate a new logic. For instance, if propositional logic is abstracted over its atomic formulas, we obtain a logic functor called Prop, which we can apply to, say, a logic on integer intervals, Interval(Int), to form propositional logic on intervals, Prop(Interval(Int)).

In Section 2.1 we first define the syntax and the semantics of a logic, which is a classical way of specifying a logic. The (abstract) syntax tells what kind of formulas can be expressed and manipulated, and the semantics tells what meaning can be given to these formulas. Then in Section 2.2 we introduce a set of operations that apply on formulas. These operations are defined as functions working only at the syntactical level, which makes them directly implementable, and constitute the executable version of the logic. In order for these operations to make sense w.r.t. the semantics, properties relating the behaviour of operations with semantics are associated to these operations. The statement of properties on logics requires proofs, combinations of properties play the role of types, and theorems on properties play the role type-checking rules. Finally, in Section 2.3.1, logics are defined as the combination of syntax, semantics, and operations; and logic functors are defined as functions from logics to logics.

2.1  Syntax and Semantics

Syntax is often defined from a signature of atoms and connectors. However, in order to allow for concrete domains and concrete structures, we choose to have a more general definition of syntax. Here we do not bother about the concrete syntax as it is just a matter of pretty-printing and parsing compared to the abstract syntax which consider formulas as set-theoretical structures (e.g., pairs, finite sets, intervals).

Definition 1   An abstract syntax AS is an enumerable set of structures, the element of which are called formulas.


As our logics are mainly designed for information systems, it is useful to distinguish two subsets of syntax: No constraint is put on these two subsets, except they should not be empty: e.g., they can be disjoint or not, they can be equal to AS or not. Wen they are not defined explicitly, they are equal to the full set of fomulas AS. The distinction between TELL-formulas, and ASK-formulas is important w.r.t. logic properties, as shown in Section 2.2, because requirements from information systems may not be the same on them.

Now, it is important to attach a semantics to a logic in order to give a meaning to formulas and operations. Like in description logics, formulas are not interpreted by truth-values, but by sets of interpretations (or individuals). Formulas are given a semantics by linking them to interpretations. These interpretations can be understood as possible objects, and reciprocally, formulas can be understood as expressing a constraint/filter/pattern on possible objects. Moreover, it is possible to define a partial ordering on interpretations, which is useful for instance to define intervals in a generic way.

Definition 2   Given a syntax AS, a semantics S based on AS is a pair (I,⊨,≤), where i ⊨ f reads “i is a model of f”. For every formula f ∈ AS, M(f) = {i ∈ I ∣ i ⊨ f} denotes the set of all models of formula f. For every formulas f, g ∈ AS, an entailment relation is defined as “f entails g” iff M(f) ⊆ M(g).


The entailment relation is never used formally in this report, but we believe it provides a good intuition for the frequent usage in proofs of the inclusion of sets of models.

2.2  Operations and Properties

Operations define the interface through which a logic can be used by programs. Properties are about the adequation of these operations w.r.t. semantics.

The formulas define the language of the logic, the semantics defines its interpretation, and an implementation defines how the logic implements an interface that is common to all logics. This common interface is made of a set of operations, which are defined below. The most important operation is the subsumption. It tests whether a formula is more specific than another. Because of the similarities between our framework and description logics, we reuse their names and notations for operations (e.g., ⊑ for subsumption).

There is no constraint, except for their types, on what operations can do. So, we define for each operation properties that relate the semantics and the operations of a logic.

For each operation, we explain its purpose, its type, its default definition, and we define a set of properties that apply to it. Properties may receive several definitions corresponding to different scopes: one point of the operation domain, the entire operation domain, and intermediate domains based on TELL, and ASK. The properties of default definition are given beside them.

2.2.1  Top ⊤

The purpose of the top is to return the most general formula of the logic. It usually is a ASK-formula, and not a TELL-formula. It may be undefined. When defined, its expected meaning is that it has every interpretation as a model.
type:
AS ∪ {undef}.

defined:
 
   def⊤=def ⊤ ≠ undef

complete:
 
   cp⊤=def def⊤⇒ M(⊤) = I

default:
⊤d =def undef
   cp⊤d

2.2.2  Bottom ⊥

The purpose of the bottom is to return the least general formula of the logic. It usually is neither a TELL-formula, nor a ASK-formula. So, when defined, its role is mainly to make possible the proof of some properties. Its expected meaning is that it has no model.
type:
AS ∪ {undef}.

defined:
 
   def⊥=def ⊥ ≠ undef

consistent:
 
   cs⊥=def def⊥⇒ M(⊥) = ∅

default:
⊥d =def undef
   cs⊥d

2.2.3  Subsumption ⊑

The purpose of subsumption is to test whether a formula is more specific than another. This is the most useful operation as it is used in information systems to compute answers to a query q. An object o is such an answer if its description d(o) is subsumed by the query q (d(o) ⊑ q). Its expected meaning is to be equivalent to the inclusion of sets of models.
type:
AS × AS → bool.

consistent in (f:AS,g:AS):
 
   cs⊑(f,g) =def f ⊑ g ⇒ M(f) ⊆ M(g)
   cs⊑=def ∀ f,g ∈ AS: cs⊑(f,g)

complete in (f:AS,g:AS):
 
   cp⊑(f,g) =def M(f) ⊆ M(g) ⇒ f ⊑ g
   cp⊑=def ∀ f,g ∈ AS: cp⊑(f,g)
   cp'⊑=def ∀ d ∈ TELL, x ∈ ASK: cp⊑(d,x)

default:
f ⊑d g =def false
    cs⊑d
In order to avoid false positives (an answer that should not be an answer), information systems usually require consistency cs⊑. To avoid false negatives (missed answers) it is sufficient to have the partial completeness cp'⊑, which is true is more logics than full completeness, and allows for more efficient implementations. This is where the motivation for distinguishing TELL-formulas, and ASK-formulas.

2.2.4  Conjunction ⊓

The purpose of conjunction is to sum up the information of 2 formulas in one, i.e. to return the most general formula that is subsumed by the two argument formulas. It can be partially defined. When the two argument formulas are incompatible, it should return the contradiction, if defined. Its expected meaning is to be equivalent to the intersection of sets of models.
type:
AS × AS → AS ∪ {undef}.

defined in (f:AS,g:AS):
 
   def⊓(f,g) =def f ⊓ g ≠ undef
   def⊓=def ∀ f,g ∈ AS: def⊓(f,g)
   defst⊓=def ∀ f,g ∈ AS: M(f) ∩ M(g) ≠ ∅ ⇒ def⊓(f,g)

consistent in (f:AS,g:AS):
 
   cs⊓(f,g) =def def⊓(f,g) ⇒ M(f ⊓ g) ⊆ M(f) ∩ M(g)
   cs⊓=def ∀ f,g ∈ AS: cs⊓(f,g)

complete in (f:AS,g:AS):
 
   cp⊓(f,g) =def def⊓(f,g) ⇒ M(f ⊓ g) ⊇ M(f) ∩ M(g)
   cp⊓=def ∀ f,g ∈ AS: cp⊓(f,g)

default:
f ⊓d g =def undef
   cs⊓d cp⊓d
When the conjunction is totally undefined (default behaviour), it is both consistent and complete. The need for making conjunction more defined usually comes from property proofs, especially about reducedness (Section 2.2.8). Defining conjunction can also be useful for compacting queries or other combinations of formulas.

2.2.5  Disjunction ⊔

The purpose of disjunction is to generate the most general formulas whose models are all models of either argument formulas. Its expected meaning is to be equivalent to the union of models, as shown by consistency and completeness properties.
type:
AS × AS → P(AS).

consistent in (f:AS,g:AS):
 
   cs⊔(f,g) =def ∪h ∈ f ⊔ gM(h) ⊆ M(f) ∪ M(g)
   cs⊔=def ∀ f,g ∈ AS: cs⊔(f,g)

complete in (f:AS,g:AS):
 
   cp⊔(f,g) =def ∪h ∈ f ⊔ gM(h) ⊇ M(f) ∪ M(g)
   cp⊔=def ∀ f,g ∈ AS: cp⊔(f,g)

default:
f ⊔d g =def {f, g}
   cs⊔d cp⊔d

2.2.6  Lower ordering ≤

The purpose of lower ordering is to test whether a formula starts before another formula, according to the partial ordering on interpretations. The simplest example is probably intervals on integers, where interpretations are integers, and the partial ordering is the natural one. The interval [1,5] starts before the interval [3,4] because the lowest model of the latter is smaller than the lowest model of the former.
type:
AS × AS → bool.

consistent in (f:AS,g:AS):
 
   cs≤(f,g) =def f ≤ g ⇒ ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j
   cs≤=def ∀ f,g ∈ AS: cs≤(f,g)

complete in (f:AS,g:AS):
 
   cp≤(f,g) =def (∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j) ⇒ f ≤ g
   cp≤=def ∀ f,g ∈ AS: cp≤(f,g)

default:
f ≤d g =def false
   cs≤d

2.2.7  Upper ordering ⋜

The purpose of the upper ordering is to test whether a formula ends before another formula, according to the partial ordering on interpretations. In the above example, the interval [3,4] ends before the interval [1,5].
type:
AS × AS → bool.

⋜ is consistent in (f:AS,g:AS):
 
   cs⋜(f,g) =def f ⋜ g ⇒ ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j
   cs⋜=def ∀ f,g ∈ AS: cs⋜(f,g)

⋜ is complete in (f:AS,g:AS):
 
   cp⋜(f,g) =def (∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j) ⇒ f ⋜ g
   cp⋜=def ∀ f,g ∈ AS: cp⋜(f,g)

default:
f ⋜d g =def false
   cs⋜d

2.2.8  Syntax vs. Semantics

Some properties are not related to one operation, but to the syntax or to the set of all operations. Before defining a list of such properties, we first need to extend the definitions of syntax and subsumption to sets of formulas.

Definition 3   Given P(X) denotes the powerset of X:
all descriptors are features:
 
   df =def TELL ⊆ ASK

satisfiable in f:AS:
f has a model.
   st(f) =def M(f) ≠ ∅
   st =def ∀ f ∈ AS: st(f)
   st' =def ∀ d ∈ TELL: st(d)

singleton in f:AS:
f has one and only one model.
   sg(f) =def |M(f)| = 1
   sg =def ∀ f ∈ AS: sg(f)
   sg' =def ∀ d ∈ ASK: sg(d)

reduced in (F:AS*, G:AS*):
 
   reduced(F,G) =def closed⊓(F) closed⊔(G) ⇒
      (∩f ∈ FM(f) ⊆ ∪g ∈ GM(g) ⇒ F ⊑* G)
   reduced =def ∀ F,G ∈ AS*: reduced(F,G)
   reduced' =def ∀ F ∈ TELL*, G ∈ ASK*: reduced(F,G)
   reduced.left =def ∀ F ∈ AS*, g ∈ AS: reduced(F,{g})
   reduced.right =def ∀ f ∈ AS, G ∈ AS*: reduced({f},G)
   reduced.top =def ∀ g ∈ AS: reduced(∅,{g})
   reduced.bot =def ∀ f ∈ AS: reduced({f},∅)
   reduced.bot' =def ∀ d ∈ TELL: reduced({d},∅)

Note that reduced.left entails reduced.top, and that reduced.right entails reduced.bot, which entails reduced.bot'. Note also that reduced(∅,∅) is always true (provided the interpretation domain is not empty).

2.2.9  Comments

Properties are rather technical, because they have been introduced progressively in order to prove some properties on logics and logic functors. This assumes we have a starting point, i.e. some initial properties we are interested in. Indeed, in the context of information systems, we need to answer queries. In Section 2.2.3 we already show that consistency cs⊑ and partial completeness cp'⊑ are required on subsumption in order to answer queries correctly.

As our logics are built by composing sub-logics by logic functors, it is important to understand that the properties required on each sub-logics will not be the same, and will depend on each logic functor. For instance, a logic functor may enforce a property even if it is not satisfied by sub-logics. The other way round, some properties may be required on sub-logics, even if it is not so in the built logic. This explains why we introduce much more properties than needed on the logics used in information systems.

Operations ⊓, ⊔, ⊤, ⊥ are all defined on the syntax of some logic, but they are not necessarily connectives of the logic, simply because the connectives of a logic are part of the syntax, and may be different from these operations. Similarly, the syntax and the semantics may define negation or quantifiers, though they are absent from the set of operations.

Note that some operations (conjunction, tautology, and contradiction) can be only partially defined (by using undef) if it is convenient, and that their properties apply only on the domain where they are defined. So it is easy to make them satisfy these properties, like consistency and completeness, by keeping them undefined. Reducedness counterbalances this triviality by requiring these operations to be defined enough. And this property is required in some logic functors in order to achieve subsumption completeness, which is crucial as said above.

2.3  Logics and Logic Functors

In this section we formally define the class of logics, and then the class of logic functors, which are functions from logics to logics.

2.3.1  Logics

A logic is the association of an abstract syntax, a semantics, an implementation, and a type made of a set of properties. The class of all logics is denoted by L.

Definition 4   A logic L is a tuple (ASL,SL,PL,TL), where ASL is (the abstract syntax of) a set of formulas, SL is a semantics based on ASL, PL is an implementation, i.e. a set of operations, based on ASL, and TL is the type of the logic, i.e., a set of properties that are satisfied by operations w.r.t. semantics.

When necessary, the satisfaction relation ⊨ of a logic L will be written ⊨L, the interpretation domain I will be written IL, the models M(f) will be written ML(f), and each operation op will be written opL.


2.3.2  Logic functors

We have just defined logics. Logic functors take logics as parameters and return a logic. Logic functors also have a syntax, a semantics, a set of operations, and a type, but they are all abstracted over one or more logics that are considered as formal parameters. For instance, the logic functor Prop(X) is the propositional logic, whose atoms have been abstracted by the formal parameter X, and can thus be replaced by more complex formulas. Then the classic propositional logic is reconstructed by applying the Composer to the expression Prop(Atom); and the composed logic Prop(Interval(Int)) replaces the classic atoms by intervals on integers. This process is very similar to the composition of mathematic expressions from operations (e.g., +,−,×), or complex programming types from basic types (e.g., int, bool) and type constructors (e.g., array, list). It is also possible to define a new logic functor as a parameterized composition of existing functors. We call such a functor a combinator: e.g., λ X.Prop(Interval(X)).

We formally define the class of logic functors. Given L the class of logics, the class of logic functors F includes all functions from tuples of logics to logics. The special case of logic functors with arity 0 corresponds to the class of logics L. The notation F/n is used to say that F is a logic functor with arity n, i.e., expecting n logics in order to produce a logic.

Let AS be the class of all syntaxes, S be the class of all semantics, P be the class of all sets of operations, and T the class of all logic types. The syntax of a logic functor is simply a function from the syntaxes of the logic functors which are its arguments, to the syntax of the resulting logic.

Definition 5   A logic functor F is a tuple (ASF,SF,PF,TF) where


In order to illustrate this abstract notion of logic functor, and prepare examples given in next sections, we shortly describe a few logic functors (the detailed description of our logic functors are available in the appendices). We classify them according to their role in the composition of logics:
Initiators
are 0-ary functors representing various concrete domains
Constructors
define the structure of formulas and interpretations

Abstractors
extend the abstract syntax without changing the interpretation domain

Adaptors
help to ensure some properties are satisfied
Given some logics L1,...,Ln, the type of the composed logic L = F(L1,...,Ln) is computed by TF from TL1,...,TLn (Definition 5). Concretely TF is a set of theorems relating the properties of the logics L1,...,Ln to the properties of the logic L. These theorems have all the form
property  of   L ⇐ conjunction  of  properties  of   L1,...,Ln.
Similarly, properties on logics are considered as type assignments, Li : properties, so that proving that L has some property is simply to type-check it. This type-checking problem can be represented by a set of (possibly recursive) equations on types, which is solved by classical techniques of fixpoint iteration on finite domains [DP90]. The type-checking is performed automatically by the Composer. The possible recursivity comes from the fact that a logic can be defined in a recursive way, as illustrated in the next Section. More details on this type-ckecking are given in Section 2.4.

2.4  Type Checking

If a logic can be defined in a non-recursive way, then it can be seen as a tree. Its nodes and leaves are logic functors, and the arity of each node is the arity of the logic functor. Each sub-tree corresponds to a sub-logic. The type of the built logic can then easily be synthesized starting from the type of the leaves, which are both logic functors and logics, and going upward, each functor computing the type of the sub-logic it defines from the type of its argument logics. This means that every logic functor F is equiped with a function mapping the types of its arguments to the type of the built sub-logic. This function is the concretization or implementation of the type TF of the logic functor. We will abuse notation by using TF both as the type and the function. In the case a logic functor expects no argument, this function reduces to a constant type.

The difficulty comes with recursive definitions as in such a case we obtain a rooted graph instead of a tree, where the root is the leftmost logic functor in the definition. This root is the only entry point of the graph.

Each functor Fi used in the definition of a logic defines a sub-logic Li according to the equation
Li = Fi(Li1,...,Lin).
According to Definition 5, this entails an equation on the type of sub-logics:
TLi = TFi(TLi1,...,TLin).
The types of all sub-logics can be gathered in a type T = (TLi)i ∈ I, which is a function from sub-logic indices to logic types (I → T). Then type functions TFi can be adapted to apply on the global type T, and gathered in a global type function TF, such that
TF(T)(i) = TFi(Ti1,...,Tin),
where n is the arity of Fi, and i1, ..., in are the indices of the sub-logics that are the arguments of the functor Fi.

The function TF is a map on the domain defined by the type (I → T), which can be ordered in the following way.

Definition 6   Let S,T ∈ (I → T) be global types. We say S contains T, and we note S ⊑T T, iff for all i ∈ I, we have S(i) ⊇ T(i). The maximal global type according to this order is the function that maps every index i to the full set of logic properties, which is denoted by ⊥T.


Now, as every property on every sub-logic is equated to a conjunction of properties on other sub-logics, it follows that the function TF is order-preserving w.r.t. the ordering ⊑T. Indeed, suppose S ⊑T T. This means every property present in T is also present in S. So, if a property p is present in TF(T), then this implies all properties p depends on are in T, and so are also in S. Hence, the property p is also in TF(S). Hence TF(S) ⊑T TF(T). With the fact that the domain of global types is finite, we can conclude that the fixpoint of TF is defined, and can easily be computed by applying iteratively TF on the maximal global type ⊥T until reaching the fixpoint μ(TF) [DP90]. The type of the built logic is then defined by μ(TF)(0), where 0 is the index of the root functor.

Previous Up Next