Logical Information Systems

LIS

En chantier


Participants - Objectives - Search directions - Publications - Applications - Protototypes - A little bit of theory - References & links

Participants

Sébastien Ferré
Yoann Padioleau
Olivier Ridoux
(top)

Objectives

Flexibility

File systems based on a hierarchy of directories force a rigid ordering of concerns which is only relaxed by the use of links.  However, even if augmented with links a hierarchy of directories must be searched using tools like du or find.  The problem with such hierarchies is that they enforce an ordering of concerns that was good for its author at creation time, but that is no longer good for another user, nor good for the author at another time.  This observation applies as well to other hierarchies like mail folders, menus, web bookmarks, etc.  It also applies to non-hierarchical organisations like web pages and URLs forming a graph.

The common feature of these organisation is that they enforce a rigid navigation from place to place, each place being reachable from a root place (e.g., a root directory or a home page) by only a few paths.  There is often a single path that is simply an address.  It is noticeable that all these organisations come with browsing tools, like command find or web browsers, that allow for systematic and automatic search through the whole organisation to find things wherever they happen to be.

Our objective is to organize pieces of information so that they do not belong to only one place, and so that there are many paths from a root place to them.  We propose to use as a formal basis for such an organisation Formal Concept Analysis (FCA, [Wille & Ganter]).  This theory offers a notion of concept that serves us as a notion of place, and a notion a labelling of concepts in a concept lattice that serves us as a notion of path.  When this point of view is instanciated to, say, a file system, the result is roughly as if the '/' sign that separates directory names is a commutative operator.  E.g., /a/b is equivalent to /b/a.  Using such a file system, one can do cd bin to search for a binary file without knowing whether to search in /bin or /opt/.../bin or /usr/X11R6/bin or /usr/bin, etc.  The answer to an ls following cd bin will be a list a files being just there, i.e., those in /bin, and a list of directory names that lead to other relevant places, e.g., opt/ and usr/.

So doing, we gain flexibility because of the many ways to navigate progressively towards a place.  Now a place has one address but many paths lead to it.  It is not difficult to design a file system, or any kind of information system, with such a flexibility.  The real challenge is to make it support updating, querying, and navigating at the same time.  E.g., what does mv bin sbin mean in any context?

Expressivity

Being flexible is not enough.  One wants to locate a place by all sorts of properties that are relevant to one's search.  E.g., one wants to do cd author=Jones to explore a repository of bibliographical references.  The answer to a subsequent ls can be a list a co-authors of Jones, or any hint to the user for a better characterization of what he is looking for.  One may also want to do a cd return-type=string to explore a program library.  In this case, answers to a subsequent ls can contain descriptions of argument types, or parts of specification, or whatever is significant, and is explicit in the library.

What is important in our approach is that we want an organisation that is generic in the way pieces of information are described.  We do not want to commit to a class of descriptions.  To achieve this goal we have designed a variant of FCA in which a formal concept relates objects with formulas of an almost arbitrary logic.  It is called Logical Concept Analysis (LCA, [Ferré & Ridoux, ICCS 2000]).  We only expect that the deduction relation of the logic forms a lattice.  Logical Information Systems (LIS) are organisations based on LCA where places are logical concepts, paths are labels in the logical concept lattice, and updates are allowed as well as querying and navigating [Ferré & Ridoux, DOOD 2000].

Here, the challenge is to design an efficient and updatable data-structure that permits the construction and comparison of places and paths.  A second challenge is to give safe means to users for defining and implementing the logics used in descriptions.  We have designed a theory of logical functors that can be assembled to form logics, and their theorem provers, printers, and parsers.

(top)

Search directions

Our search directions follow two tracks.  A formal track studies the structure of LISs, and an operating system oriented track studies the implementation of a LIS as a standard file-system.  The formal track stays firm on the generic logic side but plays with toy prototypes, while the OS oriented track stays firm on the mass-storage realism but plays with simple logics (e.g., attributes).  Our objective is that the two tracks meet at a close horizon.

Other search directions like the component-based design of logical tools, or man-machine dialog have emerged.

The first direction comes from the fact that a LIS must be generic in the logic used in descriptions.  A side-effect is that it is the user's responsibility to design a proper set of logical tools: parser, printer and prover.  However, this task goes beyond the capability of an average user.  So, we are studying the definition of a logic via the use of logical components that we call logical functors.  Each logical functor comes with a parsing component, a printing component, and a proof-procedure components.  Not all compositions of logical functors produce coherent systems, and we are studying the laws of their composition.

The second direction comes from the observation that queries and answers are both logical formulas.  This makes it possible to envisage a true symetrical dialog between a user and a machine in which each party queries and informs the other party.  As the domain of each application is represented in the logic selected for descriptions, it could be possible to perform a translation from natural language to logical syntax, and back, in a practical way. This may be a bonus for end-user applications.

(top)

Publications

(top)

Slides

(top)

Applications

We envisage applications in end-user services like (address | phone | cook | ...)-books, catalogues, encyclopedia, etc.

We also envisage applications in more technical applications for the researcher, e.g., documentation, bibliography, the software engineer, e.g., software repository, etc.  In the first case, descriptions may give institutional information on the source, the author, ..., and informal information about each piece of information (e.g., (good|bad) article).  In the software environment case, descriptions may give institutional information on the software project, ..., informal information (e.g., for lack of formal models) about requirements that are satisfied by each piece of software, or formal information like types or results of the application of formal methods.

It is really important that the overall design of LIS is generic in the logic used in descriptions for being able to accomodate these very different levels of description.

(top)

Prototypes

We currently have prototyped a note-book application, a cook-book, and a repository of bibliographical references.  These prototypes are based on a generic logical shell in which the proof procedure of the logic of interest can be plugged in.  These prototypes support the formal track.

We also have prototyped a man page navigator, and a browser of urban resources.  Both were based on a non-generic logical file-system implemented as an NFS server.  These prototypes support the operating system track.

(top)

A little bit of theory

Formal Concept Analysis [Wille & Ganter, see also Davey & Priestley]

A formal context I relates objects O and descriptions D which are subsets of a set of attributes A.

A function s (usually called \sigma) relates sets of objects and their greatest common description:

s(os)={a | for all o in os, a in I(o)}.
Note that
s(os)=intersection(I(o) | o in os).

A function t (usually called \tau) relates sets of attributes and objects that are described by these sets:

t(as)={o | for all a in as, a in I(o)}.
Note that
t(as)=union(o | as subset I(o)).

Functions s and t form a Galois connection: i.e.,

os subset t(as) iff as subset s(os).

Pairs (e,i) in OxA such that

s(e)=i and t(i)=e
are called formal concepts.

The e part is called the extension, and the i part the intension.  Formal concepts form a complete lattice ordered by inclusion of extensions,

(e,i)<(e',i') iff e subset e' ,
or, symetrically, by containment of intensions,
(e,i)<(e',i') iff i contains i' .

Formal concepts can be labelled by objects and attributes as follows:

label(o)=(t(s({o}),s({o})) and label(a)=(t({a}),s(t({a}))).
Note that many a's or o's may label the same formal concepts.

Logical Concept Analysis [ICCS 2000]

Let L be some logic and |= is deduction relation.

A logical context I relates objects O to logical descriptions D that are formulas of L.

A function s relates sets of objects to their common description:

s(os)=disjunction(I(o) | o in os).

A function t relates logical formulas to sets of objects whose descriptions entail them:

t(d)=union(o | I(o) |= d).

Functions s and t form a Galois connection: i.e.,

os subset t(d) iff s(os) |= d.

Pairs (e,i) in OxD such that

s(e)=i and t(i)=e
are called formal concepts.

The e part is called the extension, and the i part the intension.  Formal concepts form a complete lattice ordered by inclusion of extensions,

(e,i)<(e',i') iff e subset e'
or, symetrically, by deduction of intensions,
(e,i)<(e',i') iff i' |= i' .

Formal concepts can be labelled by objects and logical formulas as follows:

label(o)=(t(s({o}),s({o})) and label(d)=(t({d}),s(t({d}))).
Note that many d's or o's may label the same formal concepts, but note also that depending on the logic, there may be even infinitely many d's that label the same formal concept.

Even if not f |= g one says that

f contextually entails g iff t(g) includes t(f).
An important result is that contextual deduction and concept ordering are isomorphic.

Logical Information System [DOOD 2000]

A LIS permits the storage, updating and retrieval of objects equipped with logical descriptions.  The designation of object is made via logical formulas using the deduction relation of the logic.

An object o with description d belongs to the concept it labels.  So, label(o) is the place of o.  All formulas f such that label(f)=label(o) are possible names (paths) for the place.

The listing of a place label(f) contains the objects that belong to it, and formulas that may lead to other places in the following sense:

f' in listing(label(f)) only if
exists o', I(o') |= (f' and f), and not t(f ) included in t(f').
To preserve the completeness of navigation (i.e., no object is arbitrarily dissimulated by the system), all objects such as o' must be covered by an  f'.

Formulas such as  f' above are called increments.  Efficiently computing concise, yet precise, increments is one of the most important issues of LIS.

(top)

References & links


.
.
.
.

(top)
.