Raphaël Cauderlier

Catherine Dubois

ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti

The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.

Introduction

FoCaLiZe [START_REF] Pessaux | FoCaLiZe: Inside an F-IDE[END_REF] is an environment for certified programming which allows the user to specify, implement, and prove. For implementation, FoCaLiZe provides an ML like functional language. FoCaLiZe proofs are delegated to the first-order theorem prover Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] which takes Coq problems as input and outputs proofs in Coq format for independent checking. Zenon has recently been improved to handle Deduction modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF], an efficient proof-search technique. However, the Deduction modulo version of Zenon, Zenon Modulo, outputs proofs for the Dedukti proof checker [START_REF] Saillard | Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice[END_REF] instead of Coq [START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF].

In order to benefit from the advantages of Deduction modulo in FoCaLiZe, we extend the FoCaLiZe compiler by a backend to Dedukti called Focalide 3 (see Figure 1). This work is also a first step in the direction of interoperability between FoCaLiZe and other proof languages translated to Dedukti [START_REF] Cousineau | Embedding pure type systems in the lambda-pi-calculus modulo[END_REF][START_REF] Assaf | A Framework for Defining Computational Higher-Order Logics[END_REF][START_REF] Assaf | Translating HOL to Dedukti[END_REF]. This new compilation backend to Dedukti is based on the existing backend to Coq. While the compilation of types and logical formulae is a straightforward adaptation, the translation of FoCaLiZe terms to Dedukti is not trivial because Dedukti lacks local pattern-matching and recursive definitions.

In the following, Section 2 contains a short presentation of Dedukti, Zenon Modulo, and FoCaLiZe. Then Section 3 presents the main features of the compilation to Dedukti. In Section 4, the backend to Dedukti is evaluated on benchmarks. Section 5 discusses related work and Section 6 concludes the paper by pointing some future work.

Presentation of the tools

Dedukti

Dedukti [START_REF] Saillard | Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice[END_REF] is a type checker for the λΠ-calculus modulo, an extension of a pure dependent type system, the λΠ-calculus, with rewriting. Through the Curry-Howard correspondence, Dedukti can be used as a proof-checker for a wide variety of logics [START_REF] Cousineau | Embedding pure type systems in the lambda-pi-calculus modulo[END_REF][START_REF] Assaf | Translating HOL to Dedukti[END_REF][START_REF] Assaf | A Framework for Defining Computational Higher-Order Logics[END_REF]. It is commonly used to check proofs coming from the Deduction modulo provers Iprover Modulo [START_REF] Burel | A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo[END_REF] and Zenon Modulo [START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF].

A Dedukti file consists of an interleaving of declarations (such as O : nat) and rewrite rules (such as [n] plus O n --> n.).

Declarations and rewrite rules are type checked modulo the previously defined rewrite rules. This mechanism can be used to perform proof by reflection, an example is given by the following proof of 2+2 = 4 (theorem two plus two is four below): For correctness, Dedukti requires this rewrite system to be confluent. It does not guarantee to terminate when the rewrite system is not terminating.

Zenon Modulo

Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] is a first-order theorem prover based on the tableaux method. It is able to produce proof terms which can be checked independently by Coq.

Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF] is an extension of Zenon for Deduction modulo, an extension of first-order logic distinguishing computation from reasoning. Computation is defined by a rewrite system, it is part of the theory. Reasoning is defined by a usual deduction system (Sequent Calculus in the case of Zenon Modulo) for which syntactic comparison is replaced by the congruence induced by the rewrite system. Computation steps are left implicit in the resulting proof which has to be checked in Dedukti.

Zenon (resp., Zenon Modulo) accepts input problems in Coq (resp., Dedukti) format so that it can be seen as a term synthesizer: its input is a typing context and a type to inhabit, its output is an inhabitant of this type. This is the mode of operation used when interacting with FoCaLiZe because it limits ambiguities and changes in naming schemes induced by translation tools between languages.

FoCaLiZe and its compilation process

This subsection presents briefly FoCaLiZe and its compilation process (for details please see [START_REF] Pessaux | FoCaLiZe: Inside an F-IDE[END_REF] and FoCaLiZe reference manual). More precisely we adress here the focalizec compiler that produces OCaml and Coq code.

The FoCaLiZe (http://focalize.inria.fr) environment provides a set of tools to formally specify and implement functions and logical statements together with their proofs. A FoCaLiZe specification is a set of algebraic properties describing relations between input and output of the functions implemented in a FoCaLiZe program. For implementing, FoCaLiZe offers a pure functional programming language close to ML, featuring a polymorphic type system, recursive functions, data types and pattern-matching. Statements belong to first-order logic. Proofs are written in a declarative style and can be considered as a bunch of hints that the automatic prover Zenon uses to produce proofs that can be verified by Coq for more confidence [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF].

FoCaLiZe developments are organized in program units called species. Species in FoCaLiZe define types together with functions and properties applying to them. At the beginning of a development, types are usually abstract. A species may inherit one or several species and specify a function or a property or implement them by respectively providing a definition or a proof. The FoCaLiZe language has an object oriented flavor allowing (multiple) inheritance, late binding and redefinition. These characteristics are very helpful to reuse specifications, implementations and proofs.

A FoCaLiZe source program is analyzed and translated into OCaml sources for execution and Coq sources for certification. The compilation process between both target languages is shared as much as possible. The architecture of the FoCaLiZe compiler is shown in Figure 1. The FoCaLiZe compiler integrates a type checker, inheritance and late binding are resolved at compile-time (OO on Figure 1), relying on a dependency calculus described in [START_REF] Pessaux | FoCaLiZe: Inside an F-IDE[END_REF]. The process for compiling proofs towards Coq is achieved in two steps. First the statement is compiled with a hole for the proof script. The goal and the context are transmitted to Zenon. Then when the proof has been found, the hole is filled with the proof output by Zenon.

From FoCaLiZe to Focalide

As said previously, Focalide is adapted from the Coq backend. In particular it benefits from the early compilation steps. In this section, we brievly describe the input language we have to consider and the main principles of the translation and then focus on the compilation of pattern-matching and recursive functions. A more detailed and formal description can be found in [START_REF] Cauderlier | Object-Oriented Mechanisms for Interoperability between Proof Systems[END_REF].

Input language

Focalide input language is simpler than FoCaLiZe, in particular because the initial compilation steps get rid of object oriented features (see Figure 1). So for generating code to Dedukti, we can consider that a program is a list of type definitions, well-typed function definitions and proved theorems. A type definition defines a type à la ML, in particular it can be the definition of an algebraic datatype in which value constructors are listed together with their type. When applied, a function must receive all its parameters. So partial application must be named. FoCaLiZe supports the usual patterns found in functional languages such as OCaml or Haskell. In particular patterns are linear and tried in the order they are written. A logical formula is a regular first order formula where an atomic formula is a Boolean expression. Its free variables correspond to the functions and constants introduced in the program.

Translation

Basic types such as int are mapped to their counterpart in the target proof checker. However there is no standard library in Dedukti, so we defined the Dedukti counterpart for the different FoCaLiZe basic types. It means defining the type and its basic operations together with the proofs of some basic properties.

The compilation of types is straightforward. It is also quite immediate for most of the expressions, except for pattern-matching expressions and recursive functions because Dedukti, contrary to Coq, lacks these two mechanisms. Thus we have to use other Dedukti constructions to embed their semantics. The compilation of pattern-matching expressions and recursive functions is detailed in next sections. Other constructs of the language such as abstractions and applications are directly mapped to the same construct in Dedukti.

The statement of a theorem is compiled in the input format required by Zenon Modulo, which is here Dedukti itself [START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF].

Compilation of pattern-matching

Pattern-matching is a useful feature in FoCaLiZe which is also present in Dedukti. However pattern-matching in Dedukti is only available at toplevel (rewrite rules cannot be introduced locally) and both semantics are different. FoCaLiZe semantics of pattern-matching is the one of functional languages: only values are matched and the first branch that applies is used. In Dedukti however, reduction can be triggered on open terms and the order in which the rules are applied should not matter since the rewrite system is supposed to be confluent.

To solve these issues, we define new symbols called destructors, using toplevel rewrite rules and apply them locally.

If C is a constructor of arity n for some datatype, the destructor associated with C is λa, b, c. match a with | C(x 1 , . . . , x n ) ⇒ b x 1 . . . x n | ⇒ c. We say that a pattern-matching has the shape of a destructor if it is a fully applied destructor.

Each FoCaLiZe expression is translated into an expression where each patternmatching has the shape of a destructor. This shape is easy to translate to Dedukti because we only need to define the destructor associated with each constructor. It is done in two steps: we first serialize pattern-matching so that each patternmatching has exactly two branches and the second pattern is a wildcard, and we then flatten patterns so that the only remaining patterns are constructors applied to variables. Serialization and flattening terminate and are linear; moreover they preserve the semantics of pattern-matching.

Compilation of recursive functions

Recursion is a powerful but subtle feature in FoCaLiZe. When certifying recursive functions, we reach the limits of Zenon and Zenon Modulo because the rewrite rules corresponding to recursive definitions have to be used with parsimony otherwise Zenon Modulo could diverge.

In FoCaLiZe backend to Coq, termination of recursive functions is achieved thanks to the high-level Function mechanism [START_REF] Dubois | Termination proofs for recursive functions in focalize[END_REF]. This mechanism is not available in Dedukti. Contrary to Coq, Dedukti does not require recursive functions to be proved terminating a priori. We can postpone termination proofs.

As we did in a previous translation of a programming language in Dedukti [START_REF] Cauderlier | Objects and subtyping in the λΠ-calculus modulo[END_REF], we express the semantics of FoCaLiZe by a non-terminating Dedukti signature.

In FoCaLiZe, recursive functions can be defined by pattern-matching on algebraic types but also with regular conditional expressions. For example, if lists are not defined but axiomatized, we might define list equality as follows:

let rec list_equal ( l1 , l2 ) = ( is_nil ( l1 ) && is_nil ( l2 )) || (~is_nil ( l1 ) && ~is_nil ( l2 ) && head ( l1 ) = head ( l2 ) && list_equal ( tail ( l1 ) , tail ( l2 )))

In Dedukti, defining a recursive function f by a rewrite rule of the form [x] f x --> g (f (h x)) x. is not a viable option because it breaks termination and no proof of statement involving f can be checked in finite time.

What makes recursive definitions (sometimes) terminate in FoCaLiZe is the use of the call-by-value semantics. The idea is that we have to reduce any argument of f to a value before unfolding the recursive definition.

For efficiency reasons, we approximate the semantics by only checking that the argument starts with a constructor. This is done by defining a combinator CBV of type A:Type -> B:Type -> (A -> B) -> A -> B which acts as application when its last argument start with a constructor but does not reduce otherwise. Its definition is extended when new datatypes are introduced by giving a rewrite rule for each constructor. Here is the definition for the algebraic type nat whose constructors are O and S:

[B , f ] CBV nat B f O --> f O . [B ,f , n ] CBV nat B f ( S n ) --> f ( S n ).
Local recursion is then defined by introducing the fixpoint combinator Fix of type A:Type -> B:Type -> ((A -> B) -> (A -> B)) -> A -> B defined by the rewrite rule [A, B, F, x] Fix A B F x --> CBV A B (F (Fix A B F)) x. This does not trivially diverge as before because the term Fix in the right-hand side is only partially applied so it does not match the pattern Fix A B F x.

If f is a FoCaLiZe recursive function, we get the following reduction behaviour: f alone does not reduce, f v (where v is a value) is fully reduced, and f x (where x is a variable or a non-value term) is unfolded once.

The size of the code produced by Focalide is linear wrt. the input, the operational semantics of FoCaLiZe is preserved and each reduction step in the input language corresponds to a bounded number of rewriting steps in Dedukti, so the execution time for the translated program is only increased by a linear factor.

Experimental results

We have evaluated Focalide by running it on different available FoCaLiZe developments. When proofs required features which are not yet implemented in Focalide, we commented the problematic lines and ran both backends on the same input files; the coverage column of Figure 2 indicates the percentage of remaining lines.

FoCaLiZe ships with three libraries: the standard library (stdlib) which defines a hierarchy of species for setoids, cartesian products, disjoint unions, orderings and lattices, the external library (extlib) which defines mathematical structures (algebraic structures and polynomials) and the user contributions (contribs) which are a set of concrete applications. Unfortunately, none of these libraries uses pattern-matching and recursion extensively. The other developments are more interesting in this respect; they consist of a test suite for termination proofs of recursive functions (term-proof), a pedagogical example of FoCaLiZe features with several examples of functions defined by pattern-matching (ejcp) and a specification of Java-like iterators together with a list implementation of iterators using both recursion and pattern-matching.

Results4 in Figures 2 and3, show that on FoCaLiZe problems the user gets a good speed-up by using Zenon Modulo and Dedukti instead of Zenon and Coq. Proof-checking is way faster because Dedukti is a mere type-checker which features almost no inference whereas FoCaLiZe asks Coq to infer type arguments of polymorphic functions; this also explain why generated Dedukti files are bigger than the corresponding Coq files. Moreover, each time Coq checks a file coming from FoCaLiZe, it has to load a significant part of its standard library which often takes the majority of the checking time (about a second per file). In the end, finding a proof and checking it is usually faster when using Focalide. These files have been developed prior to Focalide so they do not yet benefit from Deduction modulo as much as they could. The Coq backend going through Zenon is not very efficient on proofs requiring computation because all reduction steps are registered as proof steps in Zenon leading to huge proofs which take a lot of time for Zenon to find and for Coq to check. For example, if we define a polymorphic datatype type wrap ('a) = | Wrap ('a), we can define the isomorphism f : 'a -> wrap('a) by let f (x) = Wrap(x) and its inverse g : wrap('a) -> 'a by let g(y) = match y with | Wrap (x) -> x. The time taken for our tools to deal with the proof of (g • f) n (x) = x for n from 10 to 19 is given in Figure 4; as we can see, the Coq backend becomes quickly unusable whereas Deduction modulo is so fast that it is even hard to measure it. The closest related work is a translation from a fragment of Coq kernel to Dedukti [START_REF] Assaf | A Framework for Defining Computational Higher-Order Logics[END_REF]. Pattern-matching is limited in Coq kernel to flat patterns so it is possible to define a single match symbol for each inductive type, which simplifies greatly the compilation of pattern-matching to Dedukti. To handle recursion, filter functions playing the role of our CBV combinator are proposed. Because of dependent typing, they need to duplicate their arguments. Moreover, we define the CBV operator by ad-hock polymorphism whereas filter functions are unrelated to each other. Compilation techniques for pattern-matching to enriched λ-calculi have been proposed, see e.g. [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF][START_REF] Klop | Rewriting Techniques for Analysing Termination and Complexity Bounds of SAFE Programs[END_REF][START_REF] Kahl | Basic Pattern Matching Calculi: A Fresh View on Matching Failure[END_REF]. We differ mainly in the treatment of matching failure.

A lot of work has also been done to compile programs (especially functional recursive definitions [START_REF] Giesl | Automated termination proofs for haskell by term rewriting[END_REF]14]) to rewrite systems. The focus has often been on termination preserving translations to prove termination of recursive functions using termination checkers for term rewrite systems. However, these translations do not preserve the semantics of the programs so they can hardly be adapted for handling translations of correctness proofs.

Conclusion

We have extended the compiler of FoCaLiZe to a new output language: Dedukti. Contrary to previously existing FoCaLiZe outputs OCaml and Coq, Dedukti is not a functional programming language but an extension of a dependently-typed λ-calculus with rewriting so pattern-matching and recursion are not trivial to compile to Dedukti.

However, we have shown that ML pattern-matching can easily and efficiently be translated to Dedukti using destructors. We plan to further optimize the compilation of pattern-matching, in particular to limit the use of dynamic error handling. For recursion, however, efficiency comes at a cost in term of normalization because we can not fully enforce the use of the call-by-value strategy without loosing linearity. Our treatment of recursive definitions generalizes directly to mutual recursion but we have not implemented this generalization.

Our approach is general enough to be adapted to other functional languages because FoCaLiZe language for implementing functions is an ML language without specific features. FoCaLiZe originality comes from its object-oriented mechanisms which are invisible to Focalide because they are statically resolved in an earlier compilation step. Moreover, it can also easily be adapted to other rewriting formalisms, especially untyped and polymorphic rewrite engines because features specific to Dedukti (such as higher-order rewriting or dependent typing) are not used.

We have tested Focalide on existing FoCaLiZe libraries and have found it a decent alternative to the Coq backend whose adoption can enhance the usability of FoCaLiZe to a new class of proofs based on computation.

As Dedukti is used as the target language of a large variety of systems in the hope of exchanging proofs; we want to experiment the import and export of proofs between logical systems by using FoCaLiZe and Focalide as an interoperability platform.

Fig. 1 .

 1 Fig. 1. FoCaLiZe Compilation Scheme

  -> nat . def plus : nat -> nat -> nat . [ n ] plus O n --> n [m , n ] plus ( S m ) n --> S ( plus m n ). equal : nat -> nat -> Type . refl : n : nat -> equal n n . def two_plus_two_is_four : equal ( plus ( S ( S O )) ( S ( S O ))) ( S ( S ( S ( S O )))). [ ] two_plus_two_is_four --> refl ( S ( S ( S ( S O )))).

Fig. 3 .

 3 Fig. 3. Time (in seconds) comparison of Focalide with the Coq backend

Fig. 4 .

 4 Fig. 4. Time comparison (in seconds) for computation-based proofs

The files can be obtained from http://deducteam.inria.fr/focalide

Acknowledgements This work has been partially supported by the BWare project (ANR-12-INSE-0010) funded by the INS programme of the French National Research Agency (ANR).


Mehwish Alam
email: alam@lipn.univ-paris13.frthi-nhu-nguyen.le

Thi Nhu

Nguyen Le

Amedeo Napoli
email: amedeo.napoli@loria.fr

LatViz: A New Practical Tool for Performing Interactive Exploration over Concept Lattices

Keywords: Lattice Visualization, Interactive Exploration, Web of Data, Formal Concept Analysis

With the increase in Web of Data (WOD) many new challenges regarding exploration, interaction, analysis and discovery have surfaced. One of the basic building blocks of data analysis is classification. Many studies have been conducted concerning Formal Concept Analysis (FCA) and its variants over WOD. But one fundamental question is, after these concept lattices are obtained on top of WOD, how the user can interactively explore and analyze this data through concept lattices. To achieve this goal, we introduce a new tool called as LatViz, which allows the construction of concept lattices and their navigation. LatViz proposes some remarkable improvements over existing tools and introduces various new functionalities such as interaction with expert, visualization of Pattern Structures, AOC posets, concept annotations, filtering concept lattice based on several criteria and finally, an intuitive visualization of implications. This way the user can effectively perform an interactive exploration over a concept lattice which is a basis for a strong user interaction with WOD for data analysis.

Introduction

In the last decade, there has been a huge shift from the Web of Documents to the Web of Data (WOD). Web of Documents represents data in the form of HTML pages which linked with other HTML pages through hyperlinks. This web of documents has evolved into WOD where all the information contained is represented in the form of entity and relations allowing the semantics to be embedded in the representation of the this data. This data are in the form of a (node-arc) labeled graph belonging to several domains such as newspapers, publications, biomedical data etc. The growth in the publication of data sources in WOD has made it an important source of data, which has led towards many challenges pertaining to effective utilization of this data. WOD mainly represents data in the form of Resource Description Framework (RDF) 1 . There are several ways such as data dumps and SPARQL queries to access this data, which can be utilized for many purposes, one of which is visualization and interactive exploration for data analysis purposes. Several visualization tools have been developed for this purpose, one of which is LODLive2 [START_REF] Camarda | Lodlive, exploring the web of data[END_REF], where user can choose data-sets such as DBpedia and Freebase and specify an entity as a starting point for browsing the node-arc labeled graph. Another tool based on graphical display is RelFinder [START_REF] Heim | Interactive relationship discovery via the semantic web[END_REF], where given several entities the tool automatically finds the paths connecting these entities. The major drawback of LODLive is that after two hops the number of nodes increase and it is hard to visualize the data. Moreover, these tools are good for getting an insight into what RDF graph contains but they are not built for the purpose of knowledge discovery.

In order to provide the user with the ability to perform data analysis and knowledge discovery over such kind of data, there is a need to perform classification, where the obtained classes are further made available to the user for exploration and subjective interpretation. In the current study we use Formal Concept Analysis as the basis for classification. Several studies have already been conducted using FCA and its variants over RDF graphs or its generalization to knowledge graphs. Out of these studies so far RV-Xplorer [START_REF] Alam | RV-Xplorer: A way to navigate lattice-based views over RDF graphs[END_REF] is the only tool that actually allows interactive exploration of clustered RDF data [START_REF] Alam | Interactive exploration over RDF data using formal concept analysis[END_REF]. The purpose of this paper is to enhance the functionalities discussed in the previous two studies. In this study we introduce a new tool LatViz which increases the interpretability of a concept lattice by remarkably improving the user interaction with the concept lattice as compared to existing tools. Various new functionalities have been introduced such as the visualization of Pattern Structures and AOC-posets, concept annotation, filtering concept lattice and pattern concept lattice based on several criteria and finally, an intuitive visualization of implications. This way the user can effectively perform an interactive exploration over a concept lattice which in turn gives a basis for a strong user interaction with WOD for knowledge discovery purposes. In this paper, we detail the important interaction operations implemented in LatViz. In the rest of this paper we refer to "user" as an "expert" as (s)he needs to have some basic knowledge about the lattice structure.

The paper is structured as follows: Section 2 introduces a motivating example, Section 3 introduces the background required for understanding the rest of the paper while Section 4 introduces some of the important functionalities of LatViz. Then in Section 5, we discuss some of the related tools already developed and finally Section 6 details the future perspectives of the current work.

Motivating Example

Let us consider that an expert is searching for papers published by a particular team in conferences or journals related to his/her field of research. In order to locate the papers of his/her interest (s)he has to search for specific keywords or authors in the local portal. For getting the view of which kind of papers are contained (s)he has to run a broad query and then narrow down his/her query to obtain papers on specific keywords or authors or group of keywords or authors. The expert will end up running several queries to get what (s)he wants. Moreover, if the expert wants to know the collaborations of the team with other members of the research community outside the team, as well as the diversity and the specialization of the team members, this cannot be directly obtained by simple querying. To obtain such kind of knowledge there is a need to introduce a support for data analysis. Based on this scenario, we show how the expert can be guided thanks to an adapted visualization tool to obtain such information of interest with the help of concept lattices.

Preliminaries

Pattern Structures

In this section we provide a brief introduction to pattern structures [START_REF] Ganter | Pattern structures and their projections[END_REF]. A pattern structure is a triple pG, pD, Ű q, δq, where G is the set of objects, pD, Ű q is a meet-semilattice of descriptions D equipped with a similarity measure Ű , and δ : G Ñ D maps an object to its description. More intuitively, a pattern structure is a set of objects with their corresponding descriptions, where similarity between descriptions is computed thanks to Ű . This similarity operator Ű is idempotent, commutative and associative. The derivation operators can be defined as:

A l :" ę gPA δpgq f or A Ď G d l :" tg P G|d Ď δpgqu f or d P D
Each element in D is referred to as a pattern. The subsumption order over these patterns is given as: c Ď d ô c [ d " c. The operator p.q l makes a Galois connection. Then, a pattern concept of a pattern structure pG, pD, Ű q, δq is a pair pA, dq where A Ď G and d P D such that A l " d and A " d l , where A is called the concept extent and d is called the concept intent. Pattern concept lattices are defined in the same way as concept lattices in standard FCA.

Interval Pattern Structures. Interval Pattern Structures were first introduced in [START_REF] Kaytoue | numerical pattern mining with formal concept analysis[END_REF] for dealing with numerical data instead of binary data. Consider two descriptions δpg 1 q " xrl 1 i , r 1 i sy and δpg 2 q " xrl 2 i , r 2 i sy, with i P r1..ns where n is the number of intervals used for the description of entities. The similarity operation [ and the associated subsumption relation Ď between descriptions are defined as the convex hull of two descriptions as follows: δpg 1 q [ δpg 2 q " xrminpl 1 i , l 2 i q, maxpr 1 i , r 2 i qsy Following the definition of a pattern concept discussed previously a interval pattern concept lattice can be built. Pattern structures have also been introduced to deal with graphical data [START_REF] Ganter | Pattern structures and their projections[END_REF].

Web of Data and its Classification

Web of Data (WOD) is represented in the form of entity and relationships. A standard representation of WOD represents data in the form of RDF (Resource Description Framework) triples written as xsubject, predicate, objecty. Here, subject can be a URI or a blank node, predicate can be a URI and object can be a URI, a blank node or a literal. Several RDF triples connect together to form an RDF graph. Table 1 shows an example of RDF triple store from DBLP where each row represents one triple. The subject is the title of the paper, predicates are the relations such as dc:subject and dc:creator (interpreted as "has keyword" and " has author" respectively) and the objects are the keywords and the authors. The triple t 1 is read as "paper s 1 has keyword Pattern Structures". In order to allow interactive data exploration over RDF data, an initial set of restrictions is posed by the expert by defining the task requirement based on which a SPARQL query is created by the expert to obtain the specific data. Then the most important step for interactive data exploration is to perform classification of RDF data. Finally, the expert is allowed to interact with the obtained classification. In the rest of this paper, we further improve the functionalities of the existing tools by introducing several new interactive operations in a new tool called LatViz.

LatViz for Interactive Exploration of Concept Lattices

User Interface

The display of LatViz resembles Conexp3 , which provides basic functionalities for building a concept lattice. LatViz implements two algorithms for building a concept lattice from a binary context, one of which is introduced in [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF]. Another, efficient algorithm for building a concept lattice is AddIntent [START_REF] Van Der Merwe | Addintent: A new incremental algorithm for constructing concept lattices[END_REF]. Demo of LatViz is available on-line through this link: http://latviz.loria.fr/latviz/.

The concept lattice for the scenario in section 2 was created by mapping the RDF data to a formal context K " pG, M, Iq. Based on Table 1, the subjects of the triples were considered as the set of objects G, the objects in the RDF triples i.e., keywords and authors were considered as the set of attributes M . In this example, the RDF triples were created from the publications of the Knowledge Discovery (KDD) team in LORIA. The number of objects in the context are 343 and attributes are 1516. Figure 1 shows a complete concept lattice built using LatViz. The information about a concept can be displayed by selecting the concept. Very often huge concept lattices are obtained based on the context size. LatViz provides several interactive operations allowing for reduction of exploration space of the expert. To-date this is the most interactive tool having many unique functionalities such as handling numeric data with the help of interval pattern structures, AOC-posets, filtering concept lattice and implications which provides support for data analysis. Other functionalities such as annotating the lattice, display of a concept lattice etc. are discussed in many contexts but are not yet directly implemented in the commonly used tools. In the following we detail each of these functionalities for data analysis.

AOC-Posets

AOC-poset is a partially ordered set of the attribute and object concepts, first introduced in [START_REF] Osswald | A logical approach to data-driven classification[END_REF]10]. If pG, M, Iq is a formal context then according to the definition in [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF], an object concept is defined as pg 2 , g 1 q such that g P G, i.e. pg 2 , g 1 q is the "lower" concept whose extent includes g. Dually, an attribute concept is defined as pm 1 , m 2 q where m P M , i.e. pm 1 , m 2 q is the "highest" concept whose intent includes m. The object and attribute concept are referred to as introducers in [START_REF] Berry | Hermes: a simple and efficient algorithm for building the AOC-poset of a binary relation[END_REF]. Once an attribute is introduced in a concept it is inherited from top to bottom while, dually, an introduced object is "inherited" from bottom to top. During this study, we implement the Hermes Algorithm introduced in [START_REF] Berry | Hermes: a simple and efficient algorithm for building the AOC-poset of a binary relation[END_REF] for building AOC-Poset from binary context. AOC-posets have been successfully applied to several domain one of which is to classify linguistic data [START_REF] Osswald | A logical approach to data-driven classification[END_REF]. In the current study we compute AOC Posets of RDF data. Figure 2 shows the AOC Posets of the concept lattice in Figure 1, where object and attribute concepts are shown in green while the other concepts are translucent and the pink color shows the selected concept.

Displaying Concept Lattice Level-wise

AOC-Posets actually reduce exploration space but still a huge number of concepts remain to be observed. LatViz allows the creation of concept lattice levelwise by interaction. When an expert clicks on the top concept, LatViz computes and the first level. After that the expert can select the concept for continuing the exploration, then LatViz computes the next level for that concept. In Figure 3, the top image shows the first level of the concept lattice built by selecting the top concept. Then the expert can view the contents of each concept on mouseover. In the running example, expert locates the concept with all the papers of Amedeo Napoli (i.e., K#2), which shows that the total number of documents written by Amedeo Napoli are 152. On selecting this concept, the next level of the lattice originating from the selected concept is computed (shown in the bottom image in Figure 3).

Display Sub/Super Concepts of a Concept

In case of huge concept lattices sometimes it is hard to keep track of the ordering relations between the concepts. LatViz allows the expert to only highlight sub-/super concepts of a concept. For example, if the expert wants to display all the publications along with the collaborations of the author Amedeo Napoli, (s)he can highlight the associated sub-lattice of the attribute concept of "Amedeo Napoli". Figure 4 shows the highlighted sub-lattice in brown. An expert can highlight the super-concepts connected to a concept. If the expert is looking for all the papers having some keywords common with the paper Knowledge Organization and Information Retrieval Using Galois Lattices having one or more of the keywords in the intent of the concept then (s)he can highlight the sub-lattice of super concepts associated to it (see Figure 5).

Display/Hide the Sub-lattice

This functionality was partially implemented in RV-Xplorer [START_REF] Alam | RV-Xplorer: A way to navigate lattice-based views over RDF graphs[END_REF] to reduce the interaction space of the expert. Here the expert can only show the part of the concept lattice in which (s)he is interested. The expert can locate the interesting concept by navigation, containing some intent or extent. If an intent is interesting and the expert marks the concept as interesting then only the sub-concepts of this concept are shown to the expert as the intents are inherited from top to bottom. Dually, if an extent is interesting for the expert then all the super concepts are shown to the expert as the extent is inherited bottom-top. Previously, the expert highlighted the sub-lattice of the concept containing all the papers of Amedeo Napoli, now if the expert is interested in only the papers of Amedeo Napoli on Knowledge Representation then (s)he can navigate downwards and only see this part of concept lattice by marking it interesting (see Figure 6). Similarly, we previously highlighted all the super concepts of the concept having the paper entitled Knowledge Organization and Information Retrieval Using Galois Lattices in the extent, Figure 7 only shows the associated sub-lattice to have a clearer view (see Figure 7).

Interval Pattern Structures

In the running scenario, we extracted three attributes for the papers i.e., year of publications, rank of the conference in which the paper was published and finally the number of pages. The ranks of the conferences were considered based on COmputing Research and Education (CORE) rankings4 . The ranks were A*, A, B, C and other which were coded as 1, 2, 3, 4 and 5 respectively. The final concept lattice generated for the last five years of publications of Knowledge Discovery Team is shown in Figure 8.

Lattice Filtering Criteria

There are two categories of filtering provided by LatViz; one is for the concept lattice created with the binary data and the other one is provided for the pattern concept lattice built with the help of interval pattern structures.

Filtering Concept Lattice. After a concept lattice is built by applying FCA, expert is allowed to set several filtering criteria such as stability, lift, extent size, intent size and finally specific object or attribute names. Let us consider that in the running example, the expert is looking for the papers published by Amedeo Napoli on the topic of pattern structures and FCA. A filter on the number of attributes in the intent is set to 3. The filtered concept lattice obtained over the complete lattice in Figure 1 is shown in Figure 9. It further shows the authors with who Amedeo Napoli has worked i.e., Sergei O. Kuznetsov and Mehdi Kaytoue. This part of concept lattice shows the community of authors working with Amedeo Napoli on the topic of pattern structures.

Filtering Pattern Concept Lattice. Interval Pattern Concept can also be filtered by specifying the number of attributes to be considered, the upper and the lower limits for the intervals in the intent of each attribute along with stability, lift and extent size. Let us consider the pattern concept lattice in Figure 8, it can be seen that the concept lattice is hard to interpret. To make it more readable based on what an expert wants, (s)he is allowed to specify filters. For example, if the expert is looking for a paper published in a conference of a rank 1-4 in the year 2012 -2015 and has the number of pages not less than 2 and no more than 42 then the respective filters can be set for the values of all three attributes. The filtered pattern concept lattice will then only contain the part of lattice needed by the user. Figure 8 shows the concept containing group of papers published from 2014-2015 in conferences with rank 2 having number of pages 2-42.

Attribute Implications

One of the many proposed visualization techniques for implications includes table-based views. It keeps each column for rule ID, LHS and RHS of the rule, support and confidence measures. These views were used because of the simplicity of storage. However, while expert interaction it is not very convenient to obtain interesting rules at a simple glance as the number of rules can be too many. Another way of visualizing association rules are Matrix Views, where rows represent the LHS and columns represent the RHS of the rules. Support and confidence are displayed by different colors in the intersection of the LHS and RHS. In case of a formal context, the number of objects/attributes can be very big leading to problems in displaying the matrix. By carefully taking into account the above drawbacks, we finally settle on visualizing implications with the help of scatter plots, where the x-axis shows the increasing support and the y-axis shows the increasing lift (as we are considering implications the confidence of the rule is always 100%). Such kind of display helps the expert to single-out the rules (s)he wants to visualize based on the values of support and lift. Figure 11 shows implications of the running example, x-axis keeps the support in percentage and y-axis keeps lift. The number on top of the circle shows the number of rules existing in the same point in plot. On mouse over, expert can view the implications.

Related Tools

In [START_REF] Alam | Interactive exploration over RDF data using formal concept analysis[END_REF], the authors focus mainly on interactive data exploration over RDF data for interactive knowledge discovery. It clusters RDF triples based on RDF Schema and then allows interactive exploration with the help of RV-Xplorer (Rdf View eXplorer) [START_REF] Alam | RV-Xplorer: A way to navigate lattice-based views over RDF graphs[END_REF]. It is a tool for visualizing views over RDF graphs mainly for identifying interesting parts of data and allow data analysis. It has also been extended for clustering SPARQL query answers. To-date there have been many other tools developed for reducing the effort of expert in observing and interpreting a concept lattice. Many of the tools have been developed for more specific purposes. CREDO [START_REF] Carpineto | Exploiting the potential of concept lattices for information retrieval with CREDO[END_REF] and FooCA [START_REF] Koester | Conceptual knowledge retrieval with FooCA: Improving web search engine results with contexts and concept hierarchies[END_REF] are the Web Clustering Engines [START_REF] Carpineto | A survey of web clustering engines[END_REF] which take the answers from queries posed against search engines and create a concept lattice which is then displayed to the expert for interaction. CREDO allows only limited interaction, however, FooCA allows the expert edit the context and iteratively build the concept lattice. CEM [START_REF] Cole | CEM -A conceptual email manager[END_REF] is an email manager which allows quick search through the e-mails and usually deals with smaller concept lattices. Camelis [START_REF] Ferré | Camelis: a logical information system to organise and browse a collection of documents[END_REF] is a system based on FCA for the organization of documents allowing several navigation operations. Another set of tools such as Sewelis [START_REF] Ferré | Reconciling faceted search and query languages for the semantic web[END_REF] and Sparklis [START_REF] Ferré | SPARKLIS: a SPARQL endpoint explorer for expressive question answering[END_REF] allows navigation/interaction over knowledge graphs. Many other tools such as Galicia5 , ConExp and ToscanaJ6 are developed for academic purposes. LatViz takes the basic functionalities of ConExp and takes it to the another level by providing visualization for many algorithms introduced over time to increase the readability. Moreover, it re-uses the source-code for building concept lattice with the help of the algorithm in [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF] from ToscanaJ [START_REF] Becker | The ToscanaJ suite for implementing conceptual information systems[END_REF]. It can not only be applied to WOD but it has been extended for interpreting any kind of data.

Discussion and Future Improvements

LatViz is a tool built for allowing expert interaction for data analysis purposes. It provides many new functionalities for reducing the exploration space of the expert and enable him to interpret the results. As a future perspective, we also want to implement other variations of pattern structures such as Pattern Structures introduced for structured set of attributes discussed in [START_REF] Alam | Revisiting pattern structures for structured attribute sets[END_REF] and Heterogeneous Pattern Structures [START_REF] Codocedo | A proposition for combining pattern structures and relational concept analysis[END_REF]. We also want to extend the implementation of implications to association rules. Finally, we also want to take into account matrix factorization.

Fig. 1 :

 1 Fig. 1: Complete lattice built from the papers of KDD-Team in LORIA Nancy.

Fig. 2 :

 2 Fig. 2: AOC-Posets.

Fig. 3 :

 3 Fig. 3: Top image shows the first level of the concept lattice, the bottom image shows the second level built by interaction.

Fig. 4 :

 4 Fig.4: The sub-lattice highlighted for the author "Amedeo Napoli".

Fig. 5 :

 5 Fig. 5: Highlighting the super lattice of a concept.

Fig. 6 :

 6 Fig. 6: Showing only sub-lattice of the interesting concept.

Fig. 7 :

 7 Fig. 7: Showing only super-lattice of the interesting concept.

Fig. 8 :

 8 Fig. 8: Interval pattern concept lattice for publications.

Fig. 9 :

 9 Fig. 9: Filtered concept lattice obtained from binary context.

Fig. 10 :

 10 Fig. 10: Filtered Pattern Concept Lattice.

Fig. 11 :

 11 Fig. 11: Attribute implications for the running example.

Table 1 :

 1 RDF triples about papers with their authors and keywords from DBLP.

	tid Subject Predicate Object
	t1 s1	dc:subject Pattern Structures
	t2 s1	dc:creator author1
	t3 s2	dc:subject Formal Concept Analysis
	t4 s2	dc:creator author2
	t5 s1	rdf:type Publication
	t6 o21	rdf:type Author
	. . .	. . .	. . .	. . .

http://www.w3.org/RDF/

http://en.lodlive.it/

http://conexp.sourceforge.net/

http://portal.core.edu.au/conf-ranks/

https://sourceforge.net/projects/galicia/

http://toscanaj.sourceforge.net/


Mehwish Alam

Thi Nhu

Nguyen Le

Amedeo Napoli

Interactive Exploration over Concept Lattices with LatViz

In this demo paper, we introduce LatViz, a new tool which allows the construction, the display and the exploration of concept lattices. LatViz proposes some remarkable improvements over existing tools and introduces various new functionalities focusing on interaction with experts, such as visualization of pattern structures (for dealing with complex non-binary data), AOC-posets (the irreducible elements of the lattice), concept annotations, filtering based on various criteria and visualization of implications. This way the user can effectively perform interactive exploratory knowledge discovery as often needed in knowledge engineering, and especially in ontology engineering.

INTRODUCTION

For facing the analysis of large amounts of complex data, there is a need for knowledge discovery and especially classification, where the resulting classes can be made available to the user for exploration, interpretation, and knowledge representation. In this research work, we use Formal Concept Analysis (FCA [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF]), as a basis for classification. The purpose of this demo paper is to introduce LatViz, a new tool for drawing concept lattices and allowing interactive exploration. LatViz provides many new functionalities, such as the visualization of pattern structures and AOC-posets, concept annotation, concept lattice filtering, and visualization of implications. This way a user can effectively perform an interactive exploration over a concept lattice built from complex data from the web of data (RDF data), numerical or graph data.

A demo of LatViz is available on-line through http:// latviz.loria.fr/. Moreover, a companion paper will be issued in July 2016 [START_REF] Alam | Latviz: A new practical tool for performing interactive exploration over concept lattices[END_REF].

FUNCTIONALITIES OF LATVIZ

LatViz provides basic functionalities for building a concept lattice, and implements two main algorithms for building a concept lattice from a binary context. Facilities are also present for dealing with the so-called "pattern structures", that generalize FCA in the sense that any kind of data can be processed, e.g. numbers, sequences, trees and graphs [START_REF] Ganter | Pattern structures and their projections[END_REF]. This is a noticeable ability of LatViz, as most of the tools for displaying concept lattices can only work on binary data. At present, LatViz can work on complex data types such as numbers and RDF data [START_REF] Alam | Revisiting pattern structures for structured attribute sets[END_REF][START_REF] Alam | RV-Xplorer: A Way to Navigate Lattice-Based Views over RDF Graphs[END_REF]. An example of pattern concept lattice based on intervals is shown in Figure 1 (30 hotels ˆ4 numerical attributes).

LatViz provides several interactive operations for reducing the exploration space of the expert. One is the display of the so-called AOC-posets, i.e. sets of "Attribute-and Object-Concepts" [START_REF] Berry | Hermes: a simple and efficient algorithm for building the AOC-poset of a binary relation[END_REF], where only irreducible elements of the concept lattice are shown. For example, a concept lattice including 31 concepts with a related AOC poset only including 20 concepts is shown in Figure 2. This set of irreducible elements can be seen as the core of the concept lattice and includes the whole set of information attached to the concept lattice.

LatViz allows the creation of a concept lattice level-wise by interaction, i.e. "breadth-first display strategy". When an expert clicks on the top concept, LatViz computes and displays the first level. After that the expert can select a given concept for continuing the exploration, then LatViz computes the next level for that concept (see Figure 3). Dually, it is possible to apply a "depth-first display strategy", allowing the expert to only highlight sub/super concepts of a selected concept. In this way, the expert can only examine the part of the concept lattice in which (s)he is interested. Then, there can be a "top-down" or a "bottom-up exploration" depending on the interest of the expert. Actually, each concept is based on two main facets, the intent which is the set of attribute and the extent which is the set of objects related to a concept. The top-down exploration materializes the interest on intents (attributes are inherited top-down) while the bottom-up exploration focuses on extents (extents are inherited bottom-up). One important functionality, especially useful for information retrieval, is the possibility of using filtering. When a concept lattice is explored, expert is allowed to set several filtering criteria such as stability and lift (concept interest measures), extent size, intent size and finally specific object or attribute names. A concept lattice can also be filtered by specifying the number of attributes to be considered, the upper and the lower limits for the intervals in the intent of each attribute along with stability, lift and extent size.

For example, we considered a data table about hotels with 30 hotels and 4 attributes, namely "service", "overall", "rooms", and "sleep quality". For each attribute we have a rating between 1 (minimal) and 5 (maximal). The filtering constraints and the resulting concept lattice are displayed on Figures 4 and5. It should be noticed that the initial concept lattice includes 5444 concepts while the filtered one only includes 15! Finally, LatViz proposes to visualize implications (rules with a confidence of 100%) with the help of scatter plots, where along the x-axis rules are ranked by increasing support and along the y-axis rules are ranked by increasing lift (as confidence is constant). Such kind of display helps the expert to single-out the rules w.r.t. support and lift, but other measures can be easily used if needed.

LatViz is still a tool under development and an experiment with potential users is actually running for understanding potential limitations and improvements. Moreover, other functionalities should still be implemented such as: scaling procedures, facilitating and extending the use of pattern structures (e.g. sequences, trees, graphs), introducing new interest measures for concepts, alternative display of implication and association rules, and the so-called nested line diagrams which are based on particular decompositions of the data tables.

TECHNICAL DATA

LatViz can be tested at http://latviz.loria.fr/ with instructions at http://latviz.loria.fr/about.html. The requirements for users are standard: to be able to access one of the following browsers: Chrome, Firefox, IE (version 9 or after), Opera, and to have a network connection to a remote server.

Figure 1 :

 1 Figure 1: The full lattice (30 hotels ˆ4 attributes).

Figure 4 :

 4 Figure 4: Filtering on "service", "overall", and "sleep quality" attributes.

Figure 5 :

 5 Figure 5: The filtered concept lattice.

Figure 2 :

 2 Figure 2: The concept lattice of teams. The concepts of the AOC poset are emphasized.

Figure 3 :

 3 Figure 3: The display of a large concept lattice level by level.

Laboratoire d'Informatique de Paris-Nord, Université Paris 13, Paris, France, email: alam@lipn.univ-paris13.fr

LORIA (CNRS -Inria Nancy Grand Est -Université de Lorraine) BP 239, Vandoeuvre-les-Nancy, F-54506, France, email: thi-nhunguyen.le@loria.

fr 3 LORIA (CNRS -Inria Nancy Grand Est -Université de Lorraine) BP 239, Vandoeuvre-les-Nancy, F-54506, France, email: amedeo.napoli@loria.fr


Mehwish Alam
email: alam@lipn.univ-paris13.frthi-nhu-nguyen.le

Thi Nhu

Nguyen Le

Amedeo Napoli
email: amedeo.napoli@loria.fr

Steps Towards Interactive Formal Concept Analysis with LatViz

Keywords: Lattice Visualization, Interactive Exploration, Web of Data, Formal Concept Analysis

With the increase in Web of Data (WOD) many new challenges regarding exploration, interaction, analysis and discovery have surfaced. One of the basic building blocks of data analysis is classification. Many studies have been conducted concerning Formal Concept Analysis (FCA) and its variants over WOD. But one fundamental question is, after these concept lattices are obtained on top of WOD, how the user can interactively explore and analyze this data through concept lattices. To achieve this goal, we introduce a new tool called LatViz, which implements several algorithms for constructing concept lattices and allows further navigation over lattice structure. LatViz proposes some remarkable improvements over existing tools and introduces various new functionalities such as interaction with expert, visualization of Pattern Structures, AOC posets, concept annotations, filtering concept lattice based on several criteria and finally, an intuitive visualization of implications. This way the user can effectively perform an interactive exploration over a concept lattice which is a basis for a strong user interaction with WOD for data analysis.

Introduction

In the last decade, there has been a huge shift from the Web of Documents to the Web of Data (WOD). Web of Documents represents data in the form of HTML pages which are linked with other HTML pages through hyperlinks. This web of documents has evolved into WOD where all the information contained is represented in the form of entities and relations allowing the semantics to be embedded in the representation of these data. These data are in the form of a (node-arc) labeled graph belonging to several domains such as newspapers, publications, biomedical data etc. The growth in the publication of data sources in WOD has made it an important source of data, which has led towards many challenges pertaining to effective utilization of this data. WOD mainly represents data in the form of Resource Description Framework (RDF) 1 . There are several ways such as data dumps and SPARQL queries to access these data, which can be utilized for several applications, one of which is visualization and interactive exploration for data analysis purposes. Several visualization tools have been developed for this purpose, one of which is LODLive2 [START_REF] Valerio Camarda | Lodlive, exploring the web of data[END_REF], where the user can choose data-sets such as DBpedia and Freebase and specify an entity as a starting point for browsing the node-arc labeled graph. Another tool based on graphical display is RelFinder [START_REF] Heim | Interactive relationship discovery via the semantic web[END_REF], where given several entities the tool automatically finds the paths connecting these entities. The major drawback of LODLive is that after two hops the number of nodes increase and it is hard to visualize the data. Moreover, these tools are good for getting an insight into what RDF graph contains but they are not built for the purpose of knowledge discovery.

In order to provide the user with the ability to perform data analysis and knowledge discovery over such kind of data, there is a need to perform classification, where the obtained classes are further made available to the user for exploration and subjective interpretation. In the current study we use Formal Concept Analysis as the basis for classification. Several studies have already been conducted using FCA and its variants over RDF graphs or its generalization to knowledge graphs. Out of these studies so far RV-Xplorer [START_REF] Alam | RV-Xplorer: A way to navigate lattice-based views over RDF graphs[END_REF] is the only tool that actually allows interactive exploration of clustered RDF data [START_REF] Alam | Interactive exploration over RDF data using formal concept analysis[END_REF]. The purpose of this paper is to enhance the functionalities discussed in the previous studies. In this study we introduce a new tool LatViz which increases the interpretability of a concept lattice by remarkably improving the user interaction with the concept lattice as compared to existing tools. Various new functionalities have been introduced such as the visualization of Pattern Structures and AOC-posets, concept annotation, filtering concept lattice and pattern concept lattice based on several criteria and finally, an intuitive visualization of implications. This way the user can effectively perform an interactive exploration over a concept lattice which in turn gives a basis for a strong user interaction with WOD for knowledge discovery purposes. In this paper, we detail the important interaction operations implemented in LatViz. In the rest of this paper we refer to "user" as an "expert" as (s)he having basic knowledge about the lattice structure.

The paper is structured as follows: Section 2 introduces a motivating example. Section 3 introduces some of the important functionalities of LatViz, while in Section 4, we discuss some of the related tools already developed and finally Section 5 details the future perspectives of the current work.

Motivating Example

Let us consider that an expert is searching for papers published by a particular team in conferences or journals related to his/her field of research. In order to locate the papers of his/her interest (s)he has to search for specific keywords or authors in the local portal. For getting the view of which kind of papers are contained (s)he has to run a broad query and then narrow down his/her query to obtain papers on specific keywords or authors or group of keywords or authors. The expert will end up running several queries to get what (s)he wants. Moreover, if the expert wants to know the collaborations of the team with other members of the research community outside the team, as well as the diversity and the specialization of the team members, this cannot be directly obtained by simple querying. To obtain such kind of knowledge there is a need to introduce a support for data analysis. Based on this scenario, we show how the expert can be guided thanks to an adapted visualization tool to obtain such information of interest with the help of concept lattices.

3 LatViz for Interactive Exploration of Concept Lattices

User Interface

The display of LatViz resembles Conexp 3 , which provides basic functionalities for building a concept lattice. LatViz implements two algorithms for building a concept lattice from a binary context, one of which is introduced in [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF]. Another, efficient algorithm for building a concept lattice is AddIntent [START_REF] Van Der Merwe | Addintent: A new incremental algorithm for constructing concept lattices[END_REF]. A demo of LatViz is available on-line through http://latviz.loria.fr/latviz/.

The concept lattice for the scenario in section 2 was created by mapping the RDF data to a formal context K " pG, M, Iq. The subjects of the triples were considered as the set of objects G, the objects in the RDF triples i.e., keywords and authors were considered as the set of attributes M . In this example, the RDF triples were created from the publications of the Knowledge Discovery (KDD) team in LORIA. The number of objects in the context are 343 and attributes are 1516. Very often huge concept lattices are obtained based on the context size. LatViz provides several interactive operations allowing for reduction of exploration space of the expert. To-date this is the most interactive tool having many unique functionalities such as handling numeric data with the help of interval pattern structures, AOC-posets, filtering concept lattice and implications which provides support for data analysis. Other functionalities such as annotating the lattice, level-wise display of a concept lattice etc. are discussed in many contexts but are not yet directly implemented in the commonly used tools. In the following we detail each of these functionalities for data analysis.

AOC-Posets

AOC-poset is a partially ordered set of the attribute and object concepts, first introduced in [START_REF] Osswald | A logical approach to data-driven classification[END_REF][START_REF] Petersen | A set-theoretical approach for the induction of inheritance hierarchies[END_REF]. The object and attribute concept are referred to as introducers in [START_REF] Berry | Hermes: a simple and efficient algorithm for building the aoc-poset of a binary relation[END_REF]. Once an attribute is introduced in a concept it is inherited from top to bottom while, dually, an introduced object is "inherited" from bottom to top. During this study, we implement the Hermes Algorithm introduced in [START_REF] Berry | Hermes: a simple and efficient algorithm for building the aoc-poset of a binary relation[END_REF] for building AOC-Poset from binary context. Figure 1 show the highlighted AOC-Posets of the concept lattice built for the running scenario.

Displaying Concept Lattice Level-wise

AOC-Posets actually reduce exploration space but still a huge number of concepts remain to be observed. LatViz allows the creation of concept lattice levelwise by interaction. When an expert clicks on the top concept, LatViz computes and displays the first level. After that the expert can select the concept for continuing the exploration, then LatViz computes the next level for that concept. In Figure 2, the top image shows the first level of the concept lattice built by selecting the top concept. Then the expert can view the contents of each concept on mouseover. In the running example, expert locates the concept with all the papers of Amedeo Napoli (i.e., K#2), which shows that the total number of documents written by Amedeo Napoli are 152. On selecting this concept, the next level of the lattice originating from the selected concept is computed (shown in the bottom image in Figure 2).

Display Sub/Super-Concepts of a Concept

In case of huge concept lattices sometimes it is hard to keep track of the ordering relations between the concepts. LatViz allows the expert to only highlight sub/super-concepts of a concept. For example, if the expert wants to display all the publications along with the collaborations of the author Amedeo Napoli, (s)he can highlight the associated sub-lattice of the attribute concept of "Amedeo Napoli". Figure 3 shows the highlighted sub-lattice in brown. An expert can highlight the super-concepts connected to a concept. If the expert is looking for all the papers having some keywords common with the paper Knowledge Organization and Information Retrieval Using Galois Lattices having one or more of the keywords in the intent of the concept then (s)he can highlight the sub-lattice of super-concepts associated to it (see Figure 4).

Display/Hide the Sub-lattice

This functionality was partially implemented in RV-Xplorer [START_REF] Alam | RV-Xplorer: A way to navigate lattice-based views over RDF graphs[END_REF] to reduce the interaction space of the expert. Here the expert can only show the part of the concept lattice in which (s)he is interested. The expert can locate the interesting concept by navigation, containing some intent or extent. If an intent is interesting and the expert marks the concept as interesting then only the sub-concepts of this concept are shown to the expert as the intents are inherited from top to bottom. Dually, if an extent is interesting for the expert then all the super-concepts are shown to the expert as the extent is inherited bottom-top. Previously, the expert highlighted the sub-lattice of the concept containing all the papers of Amedeo Napoli, now if the expert is interested in only the papers of Amedeo Napoli on Knowledge Representation then (s)he can navigate downwards and only see this part of concept lattice by marking it interesting (see Figure 5). Similarly, we previously highlighted all the super-concepts of the concept having the paper entitled Knowledge Organization and Information Retrieval Using Galois Lattices in the extent, Figure 6 only shows the associated sub-lattice to have a clearer view (see Figure 6).

Interval Pattern Structures

Interval Pattern Structures were first introduced in [START_REF] Kaytoue | Revisiting numerical pattern mining with formal concept analysis[END_REF] for dealing with numerical data. Consider two descriptions δpg 1 q " xrl 1 i , r 1 i sy and δpg 2 q " xrl 2 i , r 2 i sy, with i P r1..ns where n is the number of intervals used for the description of entities. The similarity operation [ and the associated subsumption relation Ď between descriptions are defined as the convex hull of two descriptions as follows: δpg 1 q [ δpg 2 q " xrminpl 1 i , l 2 i q, maxpr 1 i , r 2 i qsy. Based on this similarity measure interval pattern concept lattice can be built. In the running scenario, three numerical attributes for the papers were used i.e., year of publications, rank of the conference and the number of pages. The ranks of the conferences were con-sidered based on COmputing Research and Education (CORE) rankings 4 . The ranks were A*, A, B, C and other which were coded as 1, 2, 3, 4 and 5 respectively. The final concept lattice generated for the last five years of publications of Knowledge Discovery Team is shown in Figure 7.

Lattice Filtering Criteria

There are two categories of filtering provided by LatViz; one is for the concept lattice created with the binary data and the other one is provided for the pattern concept lattice built with the help of interval pattern structures.

Filtering Concept Lattice. After a concept lattice is built by applying FCA, expert is allowed to set several filtering criteria such as stability, lift, extent size, intent size and finally specific object or attribute names. Let us consider that in the running example, the expert is looking for the papers published by Amedeo Napoli on the topic of pattern structures and FCA. A filter on the number of attributes in the intent is set to 3. The filtered concept lattice obtained over the complete lattice is shown in Figure 8. It further shows the authors with who Amedeo Napoli has worked i.e., Sergei O. Kuznetsov and Mehdi Kaytoue. This part of concept lattice shows the community of authors working with Amedeo Napoli on the topic of pattern structures. Filtering Pattern Concept Lattice. Interval Pattern Concept Lattices can also be filtered by specifying the number of attributes to be considered, the upper and the lower limits for the intervals in the intent of each attribute along with stability, lift and extent size. Let us consider the pattern concept lattice in Figure 7 which is hard to interpret. To make it more readable based on what an expert wants, (s)he is allowed to specify filters. For example, if the expert is looking for a paper published in a conference of a rank 1-4 in the year 2012 -2015 and has the number of pages not less than 2 and no more than 42 then the respective filters can be set for the values of all three attributes. The filtered pattern concept lattice will then only contain the part of lattice needed by the user. Figure 7 shows the concept containing group of papers published from 2014-2015 in conferences with rank 2 having number of pages 2-42.

Attribute Implications

One of the many proposed visualization techniques for implications includes table-based views. The columns in the table represent rule ID, LHS and RHS of the rule, support and confidence measures. These views were used because of the simplicity of storage. However, as the number of rules can be too many it is not very evident for the expert to focus on interesting rules at a simple glance. Another way of visualizing association rules are Matrix Views, where rows represent the LHS and columns represent the RHS of the rules. Support and confidence are displayed by different colors in the intersection of the LHS and RHS. In case of a formal context, the number of objects/attributes can be very big leading to problems in displaying the matrix. By carefully taking into account the above drawbacks, we finally settle on visualizing implications with the help of scatter plots, where the x-axis shows the increasing support and the y-axis shows the increasing lift (as we are considering implications the confidence of the rule is always 100%). Such kind of display helps the expert to single-out the rules (s)he wants to visualize based on the values of support and lift. Figure 10 shows implications of the running example, x-axis keeps the support in percentage and y-axis keeps lift. The number on top of the circle shows the number of rules existing in the same point in the plot. On mouse over, expert can view the implications.

Related Tools

In [START_REF] Alam | Interactive exploration over RDF data using formal concept analysis[END_REF], the authors focus mainly on interactive data exploration over RDF data for interactive knowledge discovery. It clusters RDF triples based on RDF Schema and then allows interactive exploration with the help of RV-Xplorer (Rdf View eXplorer) [START_REF] Alam | RV-Xplorer: A way to navigate lattice-based views over RDF graphs[END_REF]. It is a tool for visualizing views over RDF graphs mainly for identifying interesting parts of data and allow data analysis. It has also been extended for clustering SPARQL query answers. To-date there have been many other tools developed for reducing the effort of expert in observing and interpreting a concept lattice. Many of the tools have been developed for more specific purposes. CREDO [START_REF] Carpineto | Exploiting the potential of concept lattices for information retrieval with CREDO[END_REF] and FooCA [START_REF] Koester | Conceptual knowledge retrieval with FooCA: Improving web search engine results with contexts and concept hierarchies[END_REF] are the Web Clustering Engines [START_REF] Carpineto | A survey of web clustering engines[END_REF] which take the answers from queries posed against search engines and create a concept lattice which is then displayed to the expert for interaction. CREDO allows only limited interaction, however, FooCA allows the expert to edit the context and iteratively build the concept lattice. CEM [START_REF] Cole | CEM -A conceptual email manager[END_REF] is an email manager which allows quick search through the e-mails and usually deals with smaller concept lattices. Camelis [START_REF] Ferré | Camelis: a logical information system to organise and browse a collection of documents[END_REF] is a system based on FCA for the organization of documents allowing several navigation operations. Another set of tools such as Sewelis [START_REF] Ferré | Reconciling faceted search and query languages for the semantic web[END_REF] and Sparklis [START_REF] Ferré | SPARKLIS: a SPARQL endpoint explorer for expressive question answering[END_REF] allows navigation/interaction over knowledge graphs. Many other tools such as Galicia 5 , ConExp and ToscanaJ 6 are developed for academic purposes. LatViz takes the basic functionalities of ConExp and takes it to the another level by providing visualization for many algorithms introduced over time to increase the readability. Moreover, it re-uses the source-code for building concept lattice with the help of the algorithm in [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF] from ToscanaJ [START_REF] Becker | The ToscanaJ suite for implementing conceptual information systems[END_REF]. It can not only be applied to WOD but it has been extended for interpreting any kind of data.

Discussion and Future Improvements

LatViz is a tool built for allowing expert interaction for data analysis purposes. It provides many new functionalities for reducing the exploration space of the expert and enable him to interpret the results. As a future perspective, we also want to implement other variations of pattern structures such as Pattern Structures introduced for structured set of attributes discussed in [START_REF] Alam | Revisiting pattern structures for structured attribute sets[END_REF] and Heterogeneous Pattern Structures [START_REF] Codocedo | A proposition for combining pattern structures and relational concept analysis[END_REF]. We also want to extend the implementation of implications to association rules. Finally, we also want to take into account matrix factorization.

Fig. 1 :

 1 Fig. 1: AOC-Posets.

Fig. 2 :

 2 Fig. 2: Top image shows the first level of the concept lattice, the bottom image shows the second level built by interaction.

Fig. 3 :

 3 Fig.3: The sub-lattice highlighted for the author "Amedeo Napoli".

Fig. 4 :

 4 Fig. 4: Highlighting super-concepts of a concept.

Fig. 5 :

 5 Fig. 5: Showing only sub-lattice of the interesting concept. Fig. 6: Showing only super-concepts of the interesting concept.

Fig. 7 :

 7 Fig. 7: Interval pattern concept lattice for publications.

Fig. 8 :

 8 Fig. 8: Filtered concept lattice obtained from binary context.

Fig. 9 :

 9 Fig. 9: Filtered Pattern Concept Lattice.

Fig. 10 :

 10 Fig. 10: Attribute implications for the running example.

http://www.w3.org/RDF/

http://en.lodlive.it/

https://sourceforge.net/projects/galicia/

http://toscanaj.sourceforge.net/


Kaveh Mohamadabadi

Hervé Simon

Christophe Coillot

Christophe Goze-Bac

Geneviève Pourroy

Superparamagnetic nanoparticle detection using gradiometer induction sensors for intraoperative localization tumor tool

come

Superparamagnetic nanoparticle detection using gradiometer induction sensors for intraoperative localization tumor tool.

MOHAMADABADI Kaveh, SIMON Hervé , COILLOT Christophe , GOZE-BAC Christophe, POURROY Geneviève

Abstract

Our study concerns nano-objects consisting in an iron oxide core of 10(±2) nm or 20(±5) nm size, which exhibit superparamagnetic behavior, whose shell is constituted of dendrons carrying a dye. The characterization of the magnetic properties of these nanoobjects together with their relaxivity into MRI will be presented in this poster. Their detection in an intraoperative context requires an instrument able to detect the extremely weak magnetic signature of the superparamagnetic nanoparticle in a noisy environment. A magnetic probe based on an AC magnetic field excitation of the nano-object coupled to an inductive gradiometer sensor has been designed to achieve this measurement. A conductive layer surrounding the probe is used to provide a shielding, thanks to the eddy current which will limit the leakage magnetic field outside of the probe. The principle of the probe and its ability to measure the magnetic signature of the magnetic nano-objects will be discussed.

Theory of operation

When the ferromagnetic particle has a critical small size, then it can consist of a single uniformly magnetized domain. In other words, it will show the superparamagnetic behavior. In this case, this small enough particle or nanoparticle can be considered as a magnetic dipole Therefore, the nanoparticle material changes the direction and magnitude of the magnetic field. As a result, this distortion of magnetic field can be used as a criterion to detect the nanoparticle material.

The sensor consists of two parts: an excitation coil to produce uniform, time-varying magnetic field inside itself and two pickup coils. Both pickup coils are accommodated inside the excitation coil with the specific distance and they are reverse-coupled in series.

Modeling Excitation coil:

the excitation coil can be assumed as a finite solenoid. As a result, the magnetic field produced by this coil can be formulated in below:

where 𝐷, 𝐿 and 𝑛, are the diameter, the length and the turn number of the solenoid respectively. 𝐼 𝑓 is the current as a function of frequency and 𝑥 is the distance from the center of the solenoid.

Gradiometer:

Based on the Faraday's law, if the magnetic field lines pass through the pickup coil then the output signal depends on the rate of change of flux density.

Since the nanoparticle has a small size then it can be assumed as a magnetic dipole. This magnetic dipole then can generate the magnetic flux density (𝐵) as follows:

The excitation coil or outer coil has 200 turns in four layers of lacquered copper wire, 0.14 mm in diameter, 6mm in length and 9mm for the inner diameter. Each pickup (inner) coil of the first order gradiometer has also 50 turns in four layers with the identical wire diameter, 2mm in length and 6mm for inner diameter. Note that here due to the sensor configuration , three coils are magnetically linked together and the mutual inductances are more complex.

Read-out electronic

A high pass filter, will act to remove the low frequency signals and the bias on the output of the amplifier stage. Afterward a multiplier which is also known as the phase sensitive detector (PSD) or mixer, multiply the output of the AC amplifier by the external reference signal. By feeding the PSD output into a low pass filter the AC part of the signal is strongly attenuated. Thus, the output of the lock-in amplifier can be expressed as:

Equivalent magnetic noise

Results