Verification of the Formal Concept Analysis

RAC   Rev. R. Acad. Cien. Serie A. Mat. VOL.98 (1), 2004, pp. 3–16 Ciencias de la Computaci´on / Computational Sciences Verification of the Formal Concept Analysis Jos´ e Antonio Alonso, Joaqu´ın Borrego, Mar´ıa Jos´ e Hidalgo, Francisco Jes´us Mart´ın–Mateos and Jos´ e Luis Ruiz–Reina Abstract. This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to represent and formally verify some algorithms of this theory. We also develop a method to transform specifications of algorithms based on finite sets into other executable ones, preserving its correctness. We illustrate this method by constructing an executable algorithm to compute an implicational base of the system of implications between attributes of a finite formal context. Verificaci´ on del An´ alisis formal de conceptos Resumen. En este trabajo se realiza una verificaci´on formal de la teor´ıa del An´alisis formal de conceptos. Usamos el sistema PVS para especificar y verificar formalmente los fundamentos matem´aticos de esta teor´ıa. Adem´as, desarrollamos un m´etodo para transformar especificaciones de algoritmos basadas en el uso de conjuntos finitos en otras evaluables, preservando la correcci´on. Ilustramos este m´etodo construyendo un algoritmo evaluable para calcular una base de implicaciones del sistema de implicaciones entre atributos de un contexto formal finito. 1.Introduction Formal Concept Analysis (FCA) is a learning technique for discovering conceptual structures in a large amountof data, developedsince 1982by R. Wille andB. Ganter [6]. Using FCA techniques several systems have been created, making possible interactive exploration of large database [11]. This technique has been applied to a wide variety of issues related to knowledge representation and database exploration: inheritance and interfaces relationships [1], integration of free–text and ontologies [5], management conceptual of emails [3], knowledge and data discovery in medical texts [2], etc. Our goal is to show an experience on formalization, validation and correct implementation of a mathematical concept (FCA) in an automatedreasoningsystem. For that purpose,we will followthe first chapters of the book “Formal Concept Analysis” [6], in which the authors present the mathematical foundations of this theory as well as some algorithms. So far the FCA has been studied in the Mizar system, where a formalization and characterization of the lattice of concepts has been done [9]. In this paper, we show that the PVS theorem prover [8] provides an adequate support for the formalization of FCA. We have two main reasons to tackle this work. First, show that the PVS specification language, in addition to its associated theorem prover, is adequate for achieving a suitable formal verification of the foundations of FCA. The definitions and reasoning in PVS are close to the theory FCA due, mainly, to the Presentado por Luis M. Laita. Recibido: February 27, 2004. Aceptado: October 13, 2004. Palabras clave / Keywords: Formalized Mathematics, Formal Concept Analysis, Formal Methods, PVS, Higher Order Logic Mathematics Subject Classifications: 68T15, 68T30, 03G10 c  2004 Real Academia de Ciencias, Espa˜na. 3 J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Mart´ın–Mateos and J.L. Ruiz–Reina use of the set theory included in PVS. In our work we have also done an extensive use of the available library of finite sets. Second, we explore how we can transform specifications constructed over finite sets, hence not executable, in other executable ones. Although not every definitions in PVS are executable, there are a wide fragment of PVS executable, by generating Common Lisp code [10]. In that sense, we formalize the notions of datarefinementand operationrefinementused byDold [4, 7] and we establishtheir main properties, building thus a framework in which we could relate differents specifications of the same notion. Then, we apply it to obtain executable specifications of the functions of the theory FCA. 2.The PVS system The PVS system combines an expressive specification language with an interactive theorem prover [8]. In this section, we present a brief description of the PVS language and prover, introducingsome of the notions used in this paper. The PVS specification language is built on a classical typed higher–order logic with the basic types bool,nat,int, in addition to the function type constructor [D -> R] and the product type constructor [A, B]. The type system is also augmented with dependent types and abstract data types. In PVS, a set Awith elements of a type Tis identified with its characteristic predicates and thus, the expressions pred[T] and set[T] have the same meaning. A feature of the PVS specification language is predicate subtypes: the subtype  x:T | p(x)  consists of elements of type Tsatisfying p. It uses (A) to indicate the subtype  x:T | A(x)  . Predicate subtypes are used for constraining domains and ranges of functions in a specification and, therefore, for defining partial functions. In general, type-checking with predicate subtypes is undecidable. So, the type-checkergenerates proof obligations, called type correctness conditions(TCCs). This TCCs are either discharged by specialized proof strategies or proved by the user. In particular, for defining a recursive function, it must be ensured that the function terminates. For this reason, in the definition of a recursive function, we have to provide a measure function. This generates a TCC which states that the measure function applied to the recursive arguments decreases with respect to a well–founded ordering. A built-in prelude and loadable libraries provide standard specifications and proved facts on a large number of theories. PVS specifications are packaged as theories that can be parametrized in types and constants. The definitions and theorems of a theory can be used by another theory by importing it. Proofs in PVS are presented in a sequent calculus. The commands of the PVS prover include induction, quantifier instantiation, rewriting and simplification. 3.Formal Concept Analysis in PVS In this section, we briefly describe the FCA foundations. At the same time, we show the formalization we have developedin PVS. The framework in which concepts are placed is known as a formal context: a tuple       , where  is a set of objects,  is a set of attributes and      is a relation such that       means “the object  has the attribute  ”. We illustrate this definition by means of an example from the theory of binary relations. The objects of our example are six binary relations. The attributes are five well known properties of binary relations: reflexive, symmetric, transitive, total and equivalence. A simple format for writing a finite formal context is across table: one row for each object and one column for each attribute, marking a cross in the intersection to show that an object has an attribute. 4 Verification of FCA Reflexive (R) Symetric (S) Transitive (Tr) Total (To) Equivalence (E)   x x x x x   x x   x x x   x x   x x x   x x x In the sequel, we will use this example. In order to specify this notion in PVS, we consider two uninterpreted types, T1 and T2, denoting the type of the objects and the type of the attributes, respectively. We define the type FFCT for representing the general structures over which we will construct the type for representing a finite formal context: FFCT: TYPE = [# obj: finite_set[T1], attrib: non_empty_finite_set[T2], relation: finite_set[[T1, T2]] #] where             is the form for record types in the language of PVS. Then, the finite formal contexts can be represented by the following subtype of FFCT 1: FFC:TYPE =  C:FFCT | LET Ob = obj(C), A = attrib(C), I = relation(C) IN  pair  I: LET (ob, a) = pair IN ob  Ob  a  A  In what follows,        always denotes a finite formal context. 3.1.The lattice of concepts FCA is based on the idea that a concept is an unit consisting of two parts: the extent, which covers all the objects belonging to the concept; and the intent, which compresses all the attributes valid for all those objects. Thus, the derivation operators for a formal context  can be defined as follows:  Given a set  of objects of  , the intent of  , denoted as  ¼ , is the set of their common attributes intent(C)(X: finite_set[T1]): finite_set[T2] = IF X =  THEN attrib(C) ELSE  a: T2 |  (d:(X)): (d, a)  relation(C)  ENDIF  Dually, givena set  of attributes of  , the extent of  , denotedby  ¼ is the set of the objects having all attributes from  . extent(C)(Y: finite_set[T2]): finite_set[T1] = IF Y =  THEN obj(C) ELSE  d: T1 |  (a: (Y)): (d, a)  relation(C)  ENDIF  A pair     is a formal concept of  iff        ¼   and  ¼   . concept?(C)(pair: [finite_set[T1], finite_set[T2]]): bool = LET (X, Y) = pair IN X  obj(C)  Y  attrib(C)  intent(C)(X) = Y  extent(C)(Y) = X 1The syntax of PVS specifications has been modified to increase its readability with a more familiar mathematical notation. 5 J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Mart´ın–Mateos and J.L. Ruiz–Reina The set of all formal concepts of         is denoted as        . In PVS, we define the type representing the concepts of a formal context  and the corresponding accessor functions 2as follow: concept(C): TYPE = (concept?(C)) extent_concept(C)(pair: concept(C)): finite_set[T1] = proj_1(pair) intent_concept(C)(pair: concept(C)): finite_set[T2] = proj_2(pair) Formal concepts can be partially ordered in a natural way: a concept       is a subconcept of       iff      or, equivalently,      . subconcept?(C)(pair1, pair2: concept(C)): bool = extent_concept(C)(pair1)  extent_concept(C)(pair2) We can view the relationship among the concepts of our example by the following diagram. In it, the nodes are the concepts, represented only by their intents, and the arcs represent the subconcept relation. {To} {R, To} {R, S, To} {S, To} { R, Tr, To} {Tr, To} {R, S, Tr, E, To} {S, Tr, To } The main algebraic property of the set of concepts of a formal context  is the following Theorem 1         ,subconcept?  is a complete lattice, in which for every set of formal concepts,            , the supremum and the infimum are given by                   ¾     ¼¼    ¾                      ¾        ¾     ¼¼  where we have denoted intent(C)(extent(C)(Y)) by  ¼¼ and extent(C)(intent(C)(X)) by  ¼¼ : PROOF. 1. The relation is a partial order. We prove this property using the built in relation partial order?, where partial order?[D](rel) is verified if rel is a partial order in D: po_subconcept: LEMMA partial_order?[concept(C)](subconcept?(C)) 2. We define in PVS the expressions to compute the supremum lub fca. For this purpose, we use the Union and the Intersection of an arbitrary set of sets, and we define a function to obtain the set of extents (resp. intents) of a set of concepts, using the built in function image(f)(S), that applies fto the elements of the set S. 2The built in selector proj i(x) selects the i–th element of a tuple. 6 Verification of FCA Union(I:set[set[T]]): set[T] =  x:  (A: (I)): A(x) Intersection(I:set[set[T]]):set[T] =  x:  (A:(I)):A(x) extents_set_concepts(C)(S: set[concept(C)]): set[set[T1]] = image(extent_concept(C))(S) lub_fca(C)(S:set[concept(C)]): concept(C) = (extent(C)(intent(C)(Union(extents_set_concepts(C)(S)))), Intersection(intents_set_concepts(C)(S))) In this specification, we have constrained both the domain and the range of the function lub fca. So, it generates the following TCC ensuring that lub fca satisfies the range constraint given by the predicate subtype concept(C): lub_fca_TCC1: OBLIGATION FORALL (C: FFC, S: set[concept(C)]): concept?(C) (extent(C)(intent(C)(union(extents_set_concepts(C)(S)))), intersection(intents_set_concepts(C)(S))) This TCC is not automatically proved. In order to proveit, we establish that for an arbitrary set         of sets of objects,   ¾   ¼     ¾     ¼ . So,   ¾       ¾   ¼     ¾     ¼ . Then, we have                   ¾     ¼¼     ¾     ¼  and we prove that this is a formal concept of  . 3. Finally, we prove the following result using the built–in predicate least upper bound?, where least upper bound?(rel)(x,S) is satisfied if xis the least upper bound of S: lub_fca_is_lub: LEMMA  (S:set[concept(C)]): least_upper_bound?(subconcept?(C))(lub_fca(C)(S), S) Hence, we have proved that each collection of formal concepts have a supremum, belonging to the lattice. In the same way, we prove the results corresponding to the infimum.  3.2.Implications between attributes In those cases in which we have to classify a large numberof objects with respect to a relative small number of attributes, we could deal with rules or the implications between attributes, i.e, with statements of the form: “every object with attributes       also have attributes  ¼  ¼  ” . Then, we could characterize the intents of concepts of a formal context by a set of rules. In this situation, we study the possible attribute combinations, the attribute logic. Formally, an implication between attributes in        is a pair of subsets of attributes       , denoted as      . The set   is the premise or antecedent of the implication and   its conclusion. In PVS, we use a structure for representing a generalized type of implications implication_gen: TYPE = [# premise: finite_set[T2], conclusion: finite_set[T2] #] 7 J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Mart´ın–Mateos and J.L. Ruiz–Reina and we specify the type of implications between attributes of a context  as the subtype: implication(C): TYPE =  imp:implication_gen | premise(imp)  attrib(C)  conclusion(imp)  attrib(C)  Let us now see the semantic of implications between attributes, specifying it in PVS. A set of attributes  respects or is a model of the implication      if          (i.e.,          ). respects(C)(Z: finite_set[T2], imp: implication(C)): bool = premise(imp)  Z  conclusion(imp)  Z A set of attributes  respects a set of implications  if  respects each implication in  . respects(C)(Z: finite_set[T2], L:set[implication(C)]): bool =  (imp: (L)): respects(C)(Z, imp) An implication      holds in a set of sets of attributes if each of its elements respects      . holds(C)(imp: implication(C), S:set[finite_set[T2]]): bool =  (Z:(S)): respects(C)(Z, imp) An implication      holds in a context  ,or      is an implication of  , if the intent of every object of  respects      . That is, whenever each object having all the attributes in   also has all the attributes in   . holds(C)(imp: implication(C)): bool =  (ob: T1): ob  obj(C) => respects(C)(intent(C)(  ob  ), imp) Then, for each formal context  , we define the set of concepts of  ,concepts(C), the set of implications that holds in  ,holds(C), and the set of models of the implications hold in  ,models(C). concepts(C) =  pair: [finite_set[T1], finite_set[T2]]| concept?(C)(pair)  holds(C) =  imp: implication(C)| holds(C)(imp)  models(C)(S) =  Z: finite_set[T2] | Z  attrib(C)  respects(C)(Z,S)  And we prove the relationship between the models of the implications that hold in  and the concepts of  : Theorem 2 The set of models of the implications that hold in C is the set of the intents of concepts of C. models_holds: THEOREM models(C)(holds(C))=intents_set_concepts(C)(concepts(C)) Letus notethat to specify this result in PVS wehaveusedtheexpressionintents set concepts(C)(S), that obtains the set of intents of the concepts of  . Using this property, we can to obtain the concepts of a finite formal context  from the models of the implications that hold in  , and vice versa. Nevertheless, the number of implications that hold in a context can be very large and contain many trivial implications. Therefore, it is natural to look for a small set of implications from which everything else could be derived: an implicational base. Specifically, an implication      follows (semantically) from a set of implications  in  if each subset of attributes of  respecting  also respects      . So, given formal context  , we look for a set of implications  having the following properties: 8 Verification of FCA  sound: each implication in  holds in  sound(C)(L): bool =  (imp:(L)): holds(C)(imp)  complete: each implication that holds in  follows from  complete(C)(L):bool=  (imp:implication(C)):holds(C)(imp)  follows(C)(imp,L)  non redundant: no implication in  follows from other implications in  non_redundant(C)(L):bool=  (imp:(L)): NOT follows(C)(imp, remove(imp, L)) Guigess and Duquenne [6] have proved that for every context with a finite set of attributes  , there is a sound, complete and non redundant set of implications, called stem base or Duquenne–Guigues–Basis. For this purpose, it defines a pseudo intent as a set of attributes  which is not an intent (  ¼¼    ), but contains the closure (  ¼¼ ) of every proper subset that is also pseudo intent. In our example:   is a pseudo intent, since  ¼¼            is not a pseudo intent, since    ¼¼          ¼            , but the only proper subset of  that is a pseudo intent is  , and  ¼¼        We specify this definition in PVS, providing the cardinal of  as measure function to prove its termination: pseudo_intent?(C)(S: finite_set[T2]): RECURSIVE bool = S   intent(C)(extent(C)(S))   (P: finite_set[T2]): P  S  pseudo_intent?(C)(P) => intent(C)(extent(C)(P)  S MEASURE card(S) Then, we establish the following theorem: Theorem 3 For every finite formal context  , the set of implications       ¼¼   is pseudo intent of   is sound, non redundant and complete (  is called stem base). In our example, the stem base is                                  and a slightly modified version of the stem base is                            obtained by     ¼¼     is pseudo intent of   Let us notethat the specificationinPVS of the notionofpseudointent is moregeneralthanthe definition itself. Therefore, in orderto describethe stem base, we only consider the subsets of the attributes that verify the PVS–definition of pseudo intent: 9 J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Mart´ın–Mateos and J.L. Ruiz–Reina pseudointents(C): set[finite_set[T2]] =  S: finite_set[T2] | S  attrib(C)  pseudo_intent?(C)(S)  stem_base(C): set[implication(C)] = LET fun =  (S:finite_set[T2]): (# premise:= S, conclusion:= intent(C)(extent(C)(S)) #) IN image(fun)(pseudointents(C)) We have proved the stem base properties in PVS in a similar way as they are stated in [6]: stem_base_sound: LEMMA sound(C)(stem_base(C)) stem_base_non_redundant: LEMMA non_redundant(C)(stem_base(C)) stem_base_complete: LEMMA complete(C)(stem_base(C)) The stem base is not the only implicational base, but it plays a special role. Among other reasons, there is not other implicational base with less elements and it can be algorithmically obtained. Moreover, to built the stem base we only need an algorithm to compute the pseudo intents of  . We are going to specify such an algorithm, based on the recursive definition of pseudo intent. Here, we are interested in constructing an abstract and correct specification of this algorithm and later, we will transform it into another executable specification, preserving its correctness. Hence, if gen pseudo intents(C) computes the set of pseudo intents of  , we can compute the stem base, as follows: gen_stem_base(C): set[implication_gen] = LET fun =  (Y: finite_set[T2]): (# premise:= Y, conclusion:= intent(C)(extent(C)(Y)) #) IN image(fun)(gen_pseudo_intents(C)) Let us describethe generationof thepseudointents of        stepwise, accordingto its cardinal:  Step  : generate the pseudo intents of cardinal  :     if  is pseudo intent and     , otherwise.  Step   : generate the pseudo intents of cardinal up to   ,    , from the pseudo intents of cardinal up to    . For this, we introduce a restricted notion of pseudo intent. That is,  is a pseudo intent restricted to a set of sets  if     ¼¼ and for every   ,if    then  ¼¼   .Now, the set    can be defined as follows:                    is a pseudo intent restricted to    . Thus, if subsets card(R,k)is theset             andpseudo restricts(C)(G,S) is       is pseudo intent restricted to S  , the specification of this algorithm in PVS is the following: gen_pseudo_intents(C): set[finite_set[T2]] = gen_pseudo_intents_aux(C)(attrib(C), 0,  ) gen_pseudo_intents_aux(C)(A: finite_set[T2], k:upto(card(A)), S: finite_set[finite_set[T2]]): RECURSIVE set[finite_set[T2]] = LET NS = pseudo_restricts(C)(subsets_card(A,k), S) IN IF k = card(A) THEN S  NS ELSE gen_pseudo_intents_aux(C)(A, k+1, S  NS) ENDIF MEASURE card(A)-k 10 Verification of FCA Finally, we prove the correctness of this specification in PVS, that is, gen pseudo intents(C) builds the set of pseudo intents of  . correct_gen_pseudo_intents: THEOREM gen_pseudo_intents(C) = pseudointents(C) PROOF. The proof of gen pseudo intents(C)  pseudointents(C) is obtained by establishing that if   gen pseudo intents aux(A,k,  ), (i.e,  has been introduced in the step  ), then    and  is pseudo intent. We prove it using card(A)-k as measure–induction. In order to prove pseudointents(C)  gen pseudo intents(C), we establish by induction to, that if        and  has not been introduced in the step  , then  is not a pseudo intent.  4.Executable specifications in FCA The PVS specification language is designed to be expressive rather than executable, since it allows quantification over infinite domains and higher order equalities. However, a wide fragment of PVS is executable, by generating Common Lisp code from PVS, that can be evaluated in the PVS–ground–evaluator [10]. Specifically, the executable expressions are those that do not contain free variables, uninterpreted functions or constants, quantification over infinite domains and equality between higher–order terms. The specifications we have constructed in the previous section use operations over finite sets, which are not executable. Our main goal in this section is to show how to transform the specifications of FCA built so far into their respective executable specifications. Based on the notion of refinement of data types used for Dold [4] and Jones [7] we have done the following:  We have built a theory, REF, establishing the general notions of refinements and its main properties.  We have established a refinement of the theory of finite sets, FS, by the theory of lists, FS-REF.  We have used both theories to refine the theory FCA from the previous section by the theory FCAREF, in which the specifications of the functions are executables.  Finally, we have instantiated the parameters of the theory FCA-REF and we have evaluated some examples, included in the theory FCA-EXAMPLE. We can see the relationship between these theories in the following diagram: FS FCA−REFFS−REF FCA−EXAMPLE REF FCA 4.1.Refinement of data types. Given the types  and  , we say that a data refinement of type  by the type  is a surjective application      . 11