A Galois connection is stated between a knowledge base and queries over this knowledge. Queries are stated as conjunctions. Both the knowledge and queries are represented by certain graphs. This Galois connection gives rise to lattices of pattern concepts implicitly contained in the theory (all derivable facts) over the knowledge base. The formal foundation for browsing such lattices and a realisation in terms of a prototype tool is outlined. Data types may be assigned to individual columns of tables in the database. A type assignment corresponds to an extension of the query language and incorporates additional knowledge into the process of concept creation. Type and derivation support in the tool may be provided by pluggable modules. In the examples in this paper, only the numeric type and concrete, stored relations are featured.
The paper presents a prototype of a FCA browser for knowledge bases and its formal foundation. The browser allows interactive access to the content of a database. Via a command-line interface, concept lattices over relational data can be traversed. Each concept intent corresponds to a logical formula (or query) in one or more free variables, using relational expressions over function terms with variables where the functions range over primitive and user-de ned data sorts.
Each extent is the corresponding table of results. There is one concept lattice
for each set of free variables; the user can cross over into di erent lattices during
navigation (thus changing variables in the result set). We will see that each
concept lattice arises from a suitably de ned pattern structure [
The formalisation of FCA navigation includes concrete (stored) and abstract (computed) relations derived by domain-speci c conditional logical rules and/or relational algebra operations (SQL). Domain knowledge rules need to capture { derived relations (e.g. computing relatives based on a network of parent-child relationships); { domain-speci c interpretations of object attributes, incl. common taxonomies and discretizations (e.g. age range of legal childhood, adulthood, retirement in social insurance databases etc.) { representation invariants abstracting from syntactic and computational details of the representation incl. relational algebra, and independent of the speci c database platform. While representations are typically realised imperatively, occassionally such invariants are required to manipulate and transform queries or tables for the purpose of navigation.
We call these rules abstract, in particular, because they are independent of speci c sets of concrete relation tables, and hence remain invariant across different concrete databases for the given domain and also across updates of the same database. Although our browser prototype does not include an inference engine, such a module can be interfaced easily by storing the results of external reasoning steps as special tables accessible to the browser, on-the- y. Here we focus on the connection with FCA lattices.
For the purpose of this paper, we interpret many-sorted logics in an
algebraiccategorical framework { a view that has gained wide acceptance in the semantics
of programming languages, abstract data types, knowledge representation and
behaviour speci cation over several decades. It goes back to universal algebra
[
The paper is organised as follows. In Section 2 we review relevant existing work on many-sorted structures and logics and summarise our notation; section 3 presents some technical advanced many-sorted structures that form the basis for our FCA-centric approach to patterns and queries; section 4 focuses on the browser, both in terms of the core algorithm and the user interface for navigation. Finally Section 5 provides some links to related work. 2
In this section we brie y summarise basic notations and formalisation used in
the rest of the paper. The algebraic-categorical view of abstract data types and
data analysis has developed in line with model theory: syntax is captured in
signatures limiting the construction of well-sorted terms and atomic formulae over
algebras (data and functions) or structures (algebras plus relations) as models.
Terms are sorted to represent data of primitive sorts abstractly, independent of
a speci c interpretation by a data domain. For example attributes, arithmetic
or logical operators appearing in logical formulae or database queries may be
sorted, as in the example below, where Anne is a constant of sort person, age
is a numeric attribute of an object and Parent is a binary predicate on sort
person. For exible abstract many-sorted de nitions we permit so-called
ordersorted models, i.e., where sorts are partially ordered. bool and int are assumed
to be built in primitive sorts. object is a built-in maximal sort.
sort int < number, person < object
Anne,Bob,Chris,Dora,Emily: ! person
+ : number number ! number
< : number number ! bool
age: object ! int
Parent: person person
female,male: person
As we will see later, the sort order abstracts from a corresponding subset
relationship between corresponding data domains. We also allow so-called `mix x'
notation for function and predicate symbols as known from platforms realising
algebraic-categorical forms of many-sorted type or logical speci cations, such
as OBJ3 [
c0 Anne Dora Emily male
c0 Bob Chris age c0
c1 Anne 59 Bob 31 Chris 27 Dora 7 Emily 3
META table column type Parent c0 Parent c1 male c0 female c0 age c0 age c1 person person person person person number a many-sorted signature is a triple = (S; F; P ) where S is a nite partial order (of elements called sort symbols or sorts for short), F = (Fu;s)u2S ;s2S is a pairwise disjoint family of sets of symbols (called function symbols) and P = (Pu)u2S is a family of pairwise disjoint sets of symbol (called predicate symbols). For f 2 Fu;s (or p 2 Pu) we set dom(f ) = u (or dom(p) = u, respectively) and cod(f ) = s (read 'domain' and 'codomain' respectively). As usual for abstract types and many-sorted logics, signature morphism remap sorts, function and predicate symbols preserving domains, codomains and sort order. We use T ;s to denote the set of well-formed terms of sort s and A the set of well-formed atoms p(t1; : : : ; tn) for p 2 Pu; u = s1 sn; ti 2 T ;si (1 i n).
Elimination of junk. Many-sorted approaches are interesting to us as they reduce the search space for inferencing and navigation: ill-sorted terms and formulae can be recognised e ciently, and in fact eliminated syntactically. This reduces the search space signi cantly and eliminates massive amounts of socalled 'junk data' in terms of ill-sorted elements, in particular in queries and auxiliary formulae occuring in searches.
Example database. Before we formalise concrete models, let us look at a example database as a concrete model in terms of sets and tables.
A database table corresponds to (a) a relation interpreting a corresponding predicate symbol, or (b) a function from a set of columns (arguments) to a column (result), or (c) a set of attributes mapping the rows (object keys) to attributes, thus encoding functions similar not unlike (b). For example in Fig. 1, the table named Parent contains all pairs (p; p0) such that P arent(p; p0) is valid, while the table age maps persons to their ages. Column are representing attributes including selectors of components in tuples. For example c0 in the age table selects the person component of the table rows etc. Queries supported by the database are constrained by the signature and the logical connectives permitted in the structure of formulae outside the algebraic structure captured by the signatures. For concrete databases and in our prototype implementation, we assume the existence of a META table (see Fig. 1) which represents the signature information relevant for the tables in the database. The remaining signature (outside the data base) represents operators on data types in the tables or relations that can be computed from the data base using queries. Many-sorted structures. Given a many-sorted signature , a -structure D = h(Ds)s2S ; F ; Ri has a family of carrier sets Ds (aka domains) sorted and ordered by S and families of sets of functions and relations compatible with the prescribed domains and codomains of functions and predicate symbols in . The partial order of sorts is interpreted as subsorting: Ds Dt if s t. Functions are total on their domains.1 For readability in concrete examples we also denote Ds by sD (the interpretation of sort s in D). Likewise, for f 2 Fu;s (p 2 Pu) we denote the corresponding function in D by fD (or pD respectively). It is well-known that the term structure T := h(Ts)s2S ; F; P i with empty relations forms the free -structure. Homomorphisms between -structures are weak, i.e. preserve de nedness but not necessarily unde nedness of relations. They are called strong if they also preserve unde nedness.
The formal structure underlying the database in Fig. 1 has for example: personD = fAnne; Bob; Chris; Dora; Emilyg;
AnneD = Anne; : : : ; EmilyD = Emily; numberD = f3; 7; 27; 31; 59; :::g; ParentD = f(Anne; Bob); (Anne; Chris); (Bob; Dora); (Bob; Emily)g; ageD = fAnne 7! 59; Bob 7! 31; Chris 7! 27; Dora 7! 7; Emily 7! 3g Many-sorted logics. For the rest of the paper, let be a xed signature and D a -structure. We assume each sort in includes a distinguished equality predicate =s with the obvious interpretation in D. For sorted terms and formulae 1 Note that the underlying algebra D = hD; F i, with the unsorted carrier D the union of the Ds, is partial, as is the underlying unsorted structure. with variables we use a many-sorted family (Vs)s2S of at most countably in nite and pairwise disjoint sets of variable symbols that are disjoint from function symbols in F . We denote by (V ) the extended signature that adds variables as constant function symbols to . The (V ) term structure now contains all well-sorted terms with variables. -formulae are built using well-sorted atoms p(t; :::) for predicate symbols p in , conjunction, implication and existential quanti ers over sorted variables constrained to prenex normal form (i.e. not occurring under conjunction or implication but ranging over the entire formula at hand). We denote by F ree( ) the free variables of a formula , call closed i F ree( ) = ;, denote by At the set of all -atoms, and by Cl the set of -formulae. Formulae are evaluated over a -structure as usual, by recursively 'translating' function symbols into function application, predicate symbols into relations in D and interpreting conjunction, implication and existential quanti cation logically. We use ID to denote the corresponding interpretation of closed terms and fomulae and write D j= to denote that is valid in the model D. For terms or formulae with variables (F ree( ) = fx1; : : : ; xng) we write ID( [a1=x1; : : : ; an=xn]) to denote the corresponding evaluation under the assignment of the ai to xi.
age: [31,59]
x
age: [
Parent
age: [
P 0 (1) (2) where and 0 are two -formulae of the form (1) above, s.t. F ree( ) = F ree( 0). We denote this lattice by L ;u (or Lu for short when is xed), where xi 2 Vsi (1 i n) and u = s1 sn. (Because formulae are equivalent under renaming of free variables, the sorts of variables only matter.) The top element >Lu corresponds to the tautology 9y1 : : : 9yn : x1 =s1 y1 ^ ^ xn =sn yn. In particular single-sort patterns with jF ree( )j = 1 de ne subdomains of some Ds (with fxg = F ree( )). Elements of Ls represent logical subdomains of the given sort, i.e., subdomains expressible in logical formulae over .
For the structural representation of (1) we use a tuple (X; ; (G; )) determined as follows: For each sort s 2 S, the free variables of sort s occuring in (1) are collected in the set Xs, and X := (Xs)s2S . Correspondingly, the bound variables of sort s are collected in the domain Gs of the many-sorted structure G. For each relation symbol p 2 Pu, we have G j= p(y1; : : : ; yk) i p(y1; : : : ; yk) is an atom in . For each s 2 S, s is a mapping on Ds. For each x 2 Ds, s(x) is a formula equivalent to the conjunction of all domain-speci c conditions i on x. In particular, s(x) := > if no conditions on x occur in (1). Finally, is a family of mappings s : Xs ! Ds, where s(x) is the unique v such that x =s v occurs in . We call such a tuple a windowed structure, and the pair (G; ) an augmented structure. For technical reasons, we allow arbitrary sets for the domains of G. Figure 2 shows a formula and next to it the associated windowed structure, which may be drawn as a graph.
Entailment is formalized by homomorphisms. Their de nition re ects the nestedness of structures. A homomorphism f : (G1; 1) ! (G2; 2) of augmented structures is a homomorphism f : G1 ! G2 of many-sorted structures such that ( D)s(f (v)) ) s(v) for all s 2 S and v 2 Gs. A homomorphism f : (X1; 1; G1) ! (X2; 2; G2) exists in the case X1 X2 and is then a homomorphism f : G1 ! G2 which preserves free variables, that is f 1 = 2 XX12 , where XX12 is the subset embedding.
Within the scope of this paper, we represent a knowledge base by an augmented structure := (D; ), where D is a -structure representing a database and and ( )s(g) is the most speci c equivalence class of formulae in Ls characterising the object g. The solution set of a conjunctive query over , represented by a windowed structure (X; ; G), is Hom(G; ) . The solution set can be regarded a subset of Hom(X; ), if we regard X as a trivial augmented structure (the details are omitted). More generally, we de ne a table to be a pair (X; ), where X is a many-sorted family of variables and Hom(X; ). By Tab( ) we denote the set of all tables over . The order on Tab( ) in which the in mum is the join is given by (X1; 1) (X2; 2) :() X2 X1 ^ 1 XX21 2.
Given many-sorted, augmented or windowed structures S1 and S2, we say that S1 generalizes S2 and denote this by S1 . S2, if a homomorphism f : S1 ! S2 exists. Generalization is a preorder, and we call S1 and S2 hom-equivalent, if S1 . S2 and S2 . S1. It is not di cult to see that the product Qi2I Gi of a family (Gi)i2I of many-sorted structures is an in mum in the generalization preorder(recall however that an in mum in a preorder is not unique). In ma of augmented or windowed structures are realized by products:
Qi2I (Gi; i) := (Qi2I Gi; ;
where s(v) := Vi2I ( i)s(v) ; Qi2I (Xi; i; Gi) := (Ti2I Xi; h ii ; Qi2I Gi; where h ii(x) := ( i(x))i2I : Galois Connection The following operations de ne a Galois connection between (W; .) and (Tab( ); ): (X; ; G)0 := (X; Hom(G; )
); (X; )0 := (X; h( ) 2 i ; ) =
Y (X; ; ): 2 Proof. We only show operations are order-reversing, extensivity is easier to see. If (X1; 1; G1) . (X2; 2; G2), then there is by de nition ' 2 Hom(G1; G2) with 2 XX12 = ' 1. Thus Hom(G2; ) 2 XX12 = Hom(G2; ) ' 1 Hom(G1; ). So ( )0 in (3) is order-reversing.
Let (X1; 1) (X2; 2). Then for all 2 1 we have XX21 2 2, and thus Q 2 2 (X; ; ) . (X2; XX21 ; ) . (X; ; ). So Q 2 2 (X; ; ) . Q 2 1 (X; ; ), and ( )0 in (4) is order-reversing. tu The Galois connection gives rise to the complete lattice L , or to L [X] if restricted to queries with F ree( ) = Ss2S Xs:
L := f(T; W ) j T 2 Tab( ); W 2 W; T 0 = W; W 0 = T g
L [X] := f(T; W ) 2 L j 9 : T = (X; )g We hold that only formulas represented by connected patterns (as in Fig. 2) qualify as concept descriptions, and thus only components of powers of qualify as concept intents (cf. (4)). The implemented algorithm is still immature and will therefore only brie y be considered in the next section. (3) (4) (5) (6) #(concepts) DB relations +constants +numeric comparison x:person 9 12 18 x,y:person 26 59 85 In the order 0; 1; 2; : : : , powers are computed and decomposed into their components, which are paired up with morphisms designating the subjects of the query (cf. h( ) 2 i in (4)), translated into SQL, paired up with result tables returned by a MySQL server, and then compared (using the order on Tab( )) to eliminate equivalent patterns and build the concept lattice(s). The algorithm terminates when a power
k does not produce new patterns. Table 1 shows the number of generated concepts for queries in one and two free variables of type person, for di erent settings of query expressiveness. The "naive" algorithm did not terminate in reasonable time even for some of the small examples. This is due to combinatorial explosion of patterns in higher powers of and hardness of query optimization. More e cient algorithms are expected to make use of the fact that graph nodes are tuples over
. shown by pressing a key. If a list of neighbors is shown, each concept in the list can be highlighted and examined in the subwindow below the dashed line before it is selected (see Fig.3). The intent is shown as a formula; free variables are listed before the colon, all other variables are existence quanti ed. The concepts computed are the 103 concepts listed in the right column of Table 1. 5
The Galois connection between -theories (sets of -formulae closed under derivation) and categories of models (here -structures) is folklore in model theory and celebrated in textbooks on algebraic and logical speci cation for data and behaviour. In this paper we use a more restricted connection for formal concept navigation on a knowledge base, focusing on queries (formulae) and their result sets (structures). The abstraction of the representation of data and knowledge bases in such theories renders access to a powerful mathematical tools. Details of a mapping from such data and knowledge bases to theories and structures can be found elsewhere.
The second author used a many-sorted theory construction [
If we extend the de nition of pattern structure in [
A := d
( ) The set A of partial assignments corresponds to the table (X; ) with X := T 2A dom( ) and := f jX j 2 Ag; the windowed structures 0 and A are hom-equivalent. However, the empty tables (X; ;),X 6= V , have no representation in this approach; in this, the produced lattice may di er from L .
A relational context family can be de ned as a pair ((Ki)i2I ; (Rj )j2J ), where
each Ki =: (Gi; Mi; Ii) is a formal context and each Rj is a binary relation on
Gi1 Gi2 for some i1; i2 2 I. The concept lattice for Ki is denoted by B(Ki).
The relational context family corresponds to a many-sorted relational structure
with sort set I and family of relations (Rj )j2J . The concept lattices B(Ki),
i 2 I, correspond to the lattices of domain logical formulas. Relational Concept
Analysis, as described in [
This paper introduced a novel approach to model queries over relational data { both stored and computed { in terms of FCA lattices. In logical terms, abstract patterns are represented by certain many-sorted formulae with variables. The underlying implication lattices of the formulae and certain structures computed over the database form a Galois connection, as we showed, suitable for navigation of a solution space to the query. Changes in the query are translated into changes to the underlying lattice. Navigation thus includes intra-lattice and inter-lattice moves available to the user exploring domain knowledge over a database in terms of its concrete relation tables and tacit knowledge about these tables. A prototype browser was implemented to evaluate these concepts and was described in the paper.