Taoufiq Dkaki
email: taoufiq.dkaki@irit.fr

Josiane Mothe
email: josiane.mothe@irit.fr

An energy-based model to optimize cluster visualization

Keywords: graphs, clusterd graphs, graph drawing, visualization, I

Graphs are mathematical structures that provide natural means for complex-data representation. Graphs capture the structure and thus help modeling a wide range of complex real-life data in various domains. Moreover graphs are especially suitable for information visualization. Indeed the intuitive visualabstraction (dots and lines) they provide is intimately associated with graphs. Visualization paves the way to interactive exploratory data-analysis and to important goals such as identifying groups and subgroups among data and helping to understand how these groups interact with each other. In this paper, we present a graph drawing approach that helps to better appreciate the cluster structure in data and the interactions that may exist between clusters. In this work, we assume that the clusters are already extracted and focus rather on the visualization aspects. We propose an energy-based model for graph drawing that produces an esthetic drawing that ensures each cluster will occupy a separate zone within the visualization layout. This method emphasizes the inter-groups interactions and still shows the inter-nodes interactions. The drawing areas assigned to the clusters can be user-specified (prefixed areas) or automatically crafted (free areas). The approach we suggest also enables handling geographically-based clustering. In the case of free areas, we illustrate the use of our drawing method through an example. In the case of prefixed areas, we first use an example from citation networks and then use another example to compare the results of our method to those of the divide and conquer approach. In the latter case, we show that while the two methods successfully point out the cluster structure our method better visualize the global structure.

INTRODUCTION

Automatic graph drawing has been an active research area over the last decades. It has been boosted by the increasing interest for graph structures which provide natural and intuitive ways for complex-data representation. Indeed, Graphs have proven their effectiveness in many fields, such as social network [START_REF]Models and methods in social network analysis[END_REF], software engineering [START_REF] Gansner | An open graph visualization system and its applications to software engineering[END_REF], electronic circuit design [START_REF] Cancho | Topology of technology graphs: Small world patterns in electronic circuits[END_REF], database design [START_REF] Navathe | Vertical partitioning for database design: a graphical algorithm[END_REF] etc... More generally, graphs effortlessly and perfectly model data that can be seen as sets of objects sharing some relationships. The major benefit of such abstract representation is that it easily transforms into a meaningful drawing which can be the core of some information visualization approach and the beginning of some data exploratory analysis process. Visualization paves the way to interactive exploratory data-analysis and to one of its targeted goals: identifying groups and subgroups among data and allowing users to better understand how these groups interact with each other.

Many strategies have been used to draw graphs. Most popular algorithms are based on force-directed methods [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF][START_REF] Kamada | An algorithm for drawing general undirected graphs[END_REF]. They are rather simple but give satisfactory results for graph with few hundreds of nodes. Some methods are also scalable and demonstrate their ability to handle larger graphs [START_REF] Hachul | An Experimental Comparison of Fast Algorithms for Drawing General Large Graphs[END_REF]. These methods are effective to show the cluster structure of a graph when the clusters stem from the core graph structure; that is to say when it can be derived from the edges. However existing methods fail to represent the cluster structure of a graph when this structure is derived from extra-graph properties; for example from nodes attributes.

Finding effective visualization for clustered graphs depends on the application domains and the nature of the clustering. We can distinguish the cases when a prefixed visualization area is associated with each cluster and the cases when the visualization areas are computed. Indeed, in various cases, the spatial constraints are part of the model. This is for example the case of geographic graphs or electronic circuit boards that usually comprise a large number of components which have to fit geographic constraints. This is also the case when the user is asked to make this association.

In this paper, we propose an energy-based model for graph drawing that produces an esthetic drawing that ensures each cluster will occupy a separate zone within the visualization layout. In this work, we assume that the clusters are already calculated and known. Moreover, we consider that clusters can have been obtained independently from the core graphstructure (that is to say edges and nodes), for example from attribute data in an attributed graph or colored graph. We also hypothesize that the drawing areas assigned to the clusters can be user-specified (prefixed areas) or automatically crafted (free areas). Our method seeks good layout for clustered graphs for both prefixed and free areas. Good layouts are generally associated to esthetics and ergonomics [START_REF] Brandes | Layout of Graph Visualizations[END_REF]; our method aims at providing drawings that allow users to investigate and explore the data by properly apprehending the clusters and the inter-clusters interactions while still esthetically showing the internodes connections. We propose a new energy-based method to deal with this problem. Our method modifies the force system proposed in Fruchterman and Reingold [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF] and provides an approach that handles user-selected cluster areas.

The remaining of this paper is organized as follows. In section II we give an overview of graph drawing methods. In section III, we present the structure of clustered graphs, describe our main contributions and extend it to the case of prefixed cluster-areas. Section IV presents three use case examples. In the case of prefixed areas, we first use an example from citation networks [START_REF] Biedl | Graph-Drawing contest report[END_REF] and then use an example from [START_REF] Storey | Graph layout adjustment strategies[END_REF] to compare the results of our method to those of the divide and conquer approach. In the latter case, we show that while the two methods successfully point out the cluster structure our method better visualize the global structure.

II. RELATED WORKS

Graph drawing is a long-standing issue in mathematics and computer science. Indeed, this flourishing domain can be traced back to the sixties and the barycenter method of Tutte [START_REF] Tutte | How to draw a graph[END_REF] although it is in the early eighties that computerized graph drawing really emerged [START_REF] Di Battista | Graph Drawing: Algorithms for the Visualization of Graphs[END_REF] [START_REF] Kobourov | Force-Directed Drawing Algorithms[END_REF]. Different strategies have been proposed to answer the challenge of drawing graphs. Some of these strategies are suitable for general graph structures e.g. orthogonal layout methods [START_REF] Görg | Dynamic graph drawing of sequences of orthogonal and hierarchical graphs[END_REF], circular layout methods [START_REF] Dogrusöz | Circular Layout in the Graph Layout Toolkit[END_REF] while others are only suitable for specific structures such as trees or hierarchy [START_REF] Melancon | Circular drawings of rooted trees[END_REF].

Eades [START_REF] Eades | A heuristic for graph drawing[END_REF] popularized one of the most used general drawing strategies -namely energy-based layout. Energy-based methods view the graph as a mechanical system in which each vertex is seen as a steel ring and each edge as a spring connecting the vertices -rings-at its endpoints. The induced attractive and repulsive forces drive the graph to a minimal energy state. This heuristic paved the way for one of most popular force-directed algorithms [START_REF] Kamada | An algorithm for drawing general undirected graphs[END_REF] [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF]. Kamada and Kawai [START_REF] Kamada | An algorithm for drawing general undirected graphs[END_REF] use adaptable spring forces. The force of each spring is proportional to the graph theoretic distance (shortest-path length) between its endpoints. Fruchterman and Reingold adds electrical charges to each vertex and ends with electrical repulsion forces between vertices [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF]. The authors also add the notion of "cooling temperature" that lowers the amounts of vertices' displacement as the layout becomes finer. Further propositions such as multi-level or multi-scale approaches followed mainly to address the scalability problem. For example [START_REF] Gajer | GRIP: Graph Drawing with Intelligent Placement[END_REF] proposes a multi-scale method based on a vertex filtration, [START_REF] Harel | A fast multi-scale method for drawing large graphs[END_REF] quickly draw a graph in a very high dimensional space plunge it into a 2D or 3D space using principal components analysis. Moreover, [START_REF] Walshaw | A Multilevel Algorithm for Force-Directed Graph Drawing[END_REF] induces a coarser graph by recursively clustering the original graph and draws the obtained graphs in inverse order of the previous clustering process.

The problem of visualizing clustered graphs can be divided into two problems depending on the nature of the clustering. Indeed, algorithms dealing with clustered graphs must differ one from another depending if the graphical areas associated to each cluster are pre-defined (user-defined) or if they are defined by the visualization algorithm it-self.

Many works consider self-organizing cluster areas. The most significant of them [21][22][23] [START_REF] Noack | An Energy Model for Visual Graph Clustering[END_REF][25] [START_REF] Eades | Navigating Clustered Graphs Using Force-Directed Methods[END_REF] either modify the energy function or add 'dummy' nodes and related edges to lay out a "nice" drawing that enhances the visual identification of clusters by ensuring that the nodes belonging to a given cluster are always placed close to each other. Some energy based approaches use more sophisticated strategies to achieve the separation of clusters. For instance, [START_REF] Truong | An energy model for the drawing of clustered graphs[END_REF] use a constraint optimization technique to keep nodes strictly inside non-overlapping rectangular boundaries. IPSep-Cola [START_REF] Dwyer | IPSep-CoLa: An incremental procedure for separation constraint layout of graphs[END_REF] allows separation constraints, which enforce a minimum horizontal or vertical separation between nodes -or clusters. However the underlying linear constraints present some limitations due to the mandatory rectangular shape that the clusters must fit which may end in space waste. Another limitation is related to the decoupling of intra and inter-clusters visualizations which obviously favors the local drawings and prevents appreciating the influence of inter-clusters edges. [START_REF] Noack | An Energy Model for Visual Graph Clustering[END_REF] sets up an approach that clearly displays different clusters of graph by using a new energy model called LinLog which use a cut ratio as a measure for the coupling of two disjoint sets of vertices. Noack proves that a graph having the minimum energy according to LinLog has its clusters properly displayed: each cluster is separated from the remaining graph vertices. The distance of each cluster from each of the remaining graph vertices is inversely proportional to the "coupling". [START_REF] Balzer | Level-of-detail visualization of clustered graph layouts[END_REF] proposes a method based on the "level of detail visualization" to draw a clustered graph where the clusters are created in the hierarchical way. The approach allows users to change their view from a very abstracted to a very detailed visualization. It only modifies the visual representation of the graph without altering its structure. Alternatively, rather than been selforganized, the cluster areas can be geographically constrained as in [START_REF] Rodgers | Graph drawing techniques for geographic visualization[END_REF] What distinguishes the energy-based approach we propose in this paper from the works represented above is how clusters are defined -or uncovered. Many approaches consider clusters as sets of vertices with many internal edges and few edges to outside vertices: the clusters are graph relationship dependent. Under this assumption, clusters are often dense and stronglyconnected graphs components. In other words, the density of clusters is generally greater than the one of the entire graph. This is a quite restricting definition since graph vertices can group together and form clusters not only according to the graph binary relationship but also according to some exogenous or attribute based information . For example, in a collaboration or citation graph, the clusters may be built in relation to gender, age, geography or other similarity relationship among vertices that has nothing to do with the citation or the collaboration relationship. The approaches from the literature do not apply well to this kind of clustered graphs.

Our motivation is to propose a method for drawing clustered graph where clusters can be any set of vertices. Under these assumptions, a cluster can be any set of graph vertices. It is even possible to consider clusters containing only pairwise disconnected nodes.

III. CONTRIBUTION

Before describing our method, we provide some definitions we will be using in the paper.

A. Definitions and notations 1) Graphs

A graph consists of a set of nodes and a binary relationship between the nodes that induces a set of edges. A graph ܩ is then a couple ሺܸ, ܧሻ, where ܸ is a finite set of vertices and ܧ ⊆ ܸ ൈ ܸ a finite set of edges.

2) Clustered graphs

3) Further notations

If ܺ is a set, |ܺ| represents the number of elements of ܺ.

If ܺ is a vector ‖|ܺ|‖ represents the Euclidian norm of ܺ.

B. Defining our drawing models

When building a force-directed or energy-based model for graph drawing, one must define its three major components: the initial nodes positioning, the force system that controls how the graph vertices move to meet their final positions and, since the drawing is an iterative process, the stop condition that determines when the system reaches stability).

As said before, the problem deals with finding the best drawing for a clustered graph. This mainly includes that all vertices belonging to the same cluster must be placed in a restricted and exclusive area. The areas associated to the clusters can either be automatically determined or be chosen by the user. The resulting drawing must meet these placement constraints while still optimizing the graph global layout as well as the clusters' local-layouts.

Whatever the types of areas (pre-defined and self-defined areas), the methods we propose for drawing clustered graphs are based on the force directed placement model proposed by Fruchterman and Reingold [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF]. For this reason, we briefly present this algorithm.

1) Fruchterman and Reingold ' algorithm

The force directed placement model proposed in [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF] is one of the most popular methods for graph drawing.

Fruchterman and Reingold ' approach begins with a random initial positioning of the graph vertices. Then, it iterates two steps that consist in 1) computing the attraction and repulsion forces exerted on each vertex and 2) positioning adjustment of vertices that follows this computing. Each couple of vertices v ୧ and v ୨ , exerts on each other two opposite repulsive forces of the same intensity.

f ୰ ൌ మ ฮ୴ ഠ ୴ ഡ ሬሬሬሬሬሬሬሬԦฮ ୴ ഠ ୴ ഡ ሬሬሬሬሬሬሬሬԦ ฮ୴ ഠ ୴ ഡ ሬሬሬሬሬሬሬሬԦฮ
is the repulsive force that v ୧ exerts on v ୨ . K is a constant that depends on the visualization-space size and on the number of displayed vertices K ←ට surface || . K is the optimal distance connected nodes.

Only related vertices (for example v ୧ and v ୨ ) exert attractive and opposite forces of the same intensity on each other (see Fig. 2).

f ୟ ൌ ฮ୴ ഠ ୴ ഡ ሬሬሬሬሬሬሬሬԦฮ మ ୴ ഠ ୴ ഡ ሬሬሬሬሬሬሬሬԦ ฮ୴ ഠ ୴ ഡ ሬሬሬሬሬሬሬሬԦฮ
is the repulsive force that v ୧ exerts on v ୨ . A temperature model is used and a cooling function ensures that the displacement of each vertex is majored by a maximum displacement value that decreases over time. This traduces the idea that, as the layout becomes better the amount and need for adjustment becomes smaller.

The stopping condition is based on energy minimization but rather than computing the energy and finding its minimum or a local minimum, most algorithms perform a fixed number of iterations. ݂ ሺݔሻ: 2) Clustered-graph drawing :the case of self-defined cluster areas.

݊ݎݑݐ݁ݎ ቆ ݔ ଶ ݇ ቇ ݂ ሺݔሻ: ݊ݎݑݐ݁ݎ ቆ ݇ ଶ ݔ ቇ ݐ ൌ ݐ ; ݁ݏ݈݅ܽ݅ݐ݅݊݅# ݁ݎݑݐܽݎ݁݉݁ݐ ݐ
In this section, we focus on the case when areas associated to clusters are defined by the drawing algorithm it-self. When dealing with clustered-graph drawing, the main goal is to find a way to draw vertices from a given cluster near to each other; while vertices from different clusters must be drawn as far as possible from each other. When the clustering is performed directly using the graph relationships (edges), the clusters are generally sets of vertices that form dense sub-graphs [START_REF] Noack | An Energy Model for Visual Graph Clustering[END_REF] relatively to the entire graph. In force-based model such as in [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF], these vertices exert naturally attractive forces on each other making them close in the final graph drawing. The edges relating vertices from different clusters are infrequent which tends to separate the clusters in the final drawing. Since we are also interested in clusters that do not stems from the graph relationship, the force system has to be revisited to create attractive forces between the vertices that compose a given clusters in order to make them closer in the final drawing. Unlike the methods proposed in [EH00, FT04] that create a 'dummy' node for each cluster, we rather add "invisible" edges -that lead to additional attractive forces-between nonconnected nodes of the same cluster. This is intended to keep the nodes of a given cluster close together in the visualization space. We consider that the layout of a cluster is good if it resembles to some extend the layout of that cluster when it is considered as a separated graph. The forces generated by the additional edges must be lowered to prevent them from over affecting the internal layout of clusters. In other words, we want these extra edges to help creating homogenous and separated clusters without over-modifying the relative placement of the cluster nodes. To do so, we adjust the intensity of the additional attractive forces relatively to the one of real edges.

The main differences with the approach used in [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF] are:

1) we distinguish two types of spring forces and add attractive forces between non-connected nodes of a same cluster (some kind of invisible edges) and 2) we increase the repulsive forces between vertices from different clusters. Indeed, our force model is built as a combination of three types of springs and an electrical force (in the next algorithm we will add another electrical force):

-Real springs that link adjacent nodes from a same given cluster, -Invisible springs that link non adjacent nodes from a same cluster (they correspond to invisible links that represents the other criteria making the nodes belonging to the same cluster). These springs are weakened, using an attenuation function ,݊݅_݁ܿݑ݀݁ݎ in order to produce attenuated forces and store less energy, -Real springs that link adjacent nodes from different clusters. These springs link are also weakened, in a different manner using an attenuation function ,ݐݑ_݁ܿݑ݀݁ݎ to produce a different force comparing to real springs that link adjacent nodes from a same cluster, -The repulsive forces that concern vertices from two different clusters are amplified using the function ݄݁݊ܽ݊ܿ݁.

Fig. 4 illustrates the force system we propose. The colors help distinguishing the different kinds of force.

It is Attractive and repulsive forces depend on whether v i and v j belong or not to the same cluster # Reduce the temperature t ൌ coolሺtሻ; Fig. 5. Algorithm 2 : our algorithm for self-defined areas, based on [START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF].

3) Clustered-graph drawing : the case of predefined cluster areas

In this section, we examine the case of user pre-defined areas: each area is associated to a graph cluster. We believe that this is an important issue and to the best of our knowledge, it has not been addressed as a force placement problem in previous works. In our model, the visualization area associated with each cluster is a convex polygon. Nodes of clusters will be placed according to inter-cluster forces and extra-cluster forces. Two types of forces -attractive and repulsive-are defined the same way as in the previous case and the concept of optimal distance is personalized to each cluster. In our model, we distinguish two types of distance: one between vertices belonging to two different clusters -optDist. The other is relevant to vertices of a same cluster -optDistCluster. We hypothesize that the optimal distance between vertices of a given cluster must be smaller than the global optimal distance. We argue that the size the area occupied by a cluster is obviously smaller than the one of the total drawing area. In addition, the density of a cluster is generally higher than the whole graph density. For the reason, we define the ratio between optDist and optDistCluster as larger than 1.

The idea behind the use of two different optimal distances is to preserve a "satisfactory" display inside the area related to one given cluster. In fact, we consider that the layout of a cluster is "satisfactory" if it almost resembles the layout of that cluster when it is considered separately from the rest of the graph nodes while it still shows the influence of those nodes. When having optDistCluster < optDist, the influence of internal-nodes are considered as more important than the one of external-nodes. Note that we could have proposed a more personalized optimal distance computation so that each cluster ܥ would have its own optimal distance ܭ ൌ ට ௌ௨ | | . However, this latter idea is not optimal as the distances between nodes in different clusters cannot be easily compared. Instead, we use only two different values one for the global graph and one for the clusters. We use

ݐݏ݅ܦݐ ൌ ܭ ீ ൌ ඨ ݂݁ܿܽݎݑܵ |ܸ| and ݎ݁ݐݏݑ݈ܥݐݏ݅ܦݐ ൌ ܭ ൌ 1 |ܲ| ඨ ݂݁ܿܽݎݑܵ ܥ ܥ| |
ܭ is obtained averaging ܭ

We also offer another way to differentiate the influence of intra and extra-cluster vertices by enhancing intra-cluster interactions and by reducing extra-cluster ones. We achieve this goal using the functions: ݊݅_݁ܿݑ݀݁ݎሺሻ, ሺሻݐݑ_݁ܿݑ݀݁ݎ and ݄݁݊ܽ݊ܿ݁ሺሻ.

Moreover, to actively keep nodes of clusters inside their cluster area, we define repulsive forces between nodes and the border of the cluster area they belong to. We call these forces frontier forces (݂ ). The strength of such repulsive forces is formulated according to the distance between the nodes and the border of the clusters they belong to. It must be sufficiently strong when the distance to the border is small. In order to achieve this goal, we consider that the nodes are charged particles and that the borders of a visualization area are also electrically charged. The induced repulsive forces follow the electrical force principles. There is no need that this kind of force operates beyond a considered strip along the cluster border. In our model, the maximum displacement possible for a vertex is governed by the temperature and the cooling function. The width of the strip we consider is then two times this maximum displacement, that is to say (2 * ݐሻ.

Still, because of the discrete placement of nodes, in some special cases, the strength of cumulative forces exercised on a given node may push it outside the cluster frontier. We use the same strategy as in Fruchterman and Reingold model to return the vertex to its associated area.

In this context of fixed and none porous areas, it is no more necessary to add the "invisible" edges to stick together the vertices of a given cluster. However, we maintained them in the proposed solution to better handle the incidence of extracluster influences. We also consider that this force has to be rapidly lowered to reach and stick to zero as the vertex reaches a distance of 2 times the value of the threshold.

Let ݂ be the frontier force and ݀ the distance between a node and the border of its cluster. ݂ is defined as:

݂ ሺ݀ሻ ൌ ൝ 0 ݂ܫ ݀ 2 ݄ݐ ݇ ݀ ଶ
where ݄ݐ ൌ ሻݐ݈ሺܿ is the maximum possible displacement for any vertex, ݇ is the optimal distance in cluster context.

For simplification reasons, the frontier force exercised on a given node is determined by its nearest frontier point.

The Fig. 7 shows the principle of our model. The distance between two vertices belonging to two different clusters is split in three parts: ݀ ଵ , ݀ ଶ and ݀ ଷ . ݀ ଶ which is the distance between the two clusters is handled differently from the two other distances. We use a function to alter this distance (lower it) in order to manage the attractive force that depends on. In some sort, we curve the space between clusters zones so that we can handle the strength of inter-clusters forces. This is suitable when the clusters are too far from each other for example in geographic visualization. Note that this strength reduction is also the reason of using a multilevel optimal distance.

IV. EVALUATION AND RESULTS

In this section, we provide and discuss three examples to show the practicability of our models.

A. First example: a clustered collaboration network

This first example presents a collaboration network where the vertices represent researchers that have been associated to eight different clusters. How these clusters have been obtained is out of the scope. First we perform a drawing of the related graph using Fruchterman and Reingold algorithm (Fig. 3). As we can see, the resulting drawing is quite pleasant but it does not clearly show the clustered structure of the graph in eight clusters. The two next figures (Fig. 10 and Fig. 11) present the resulting drawing for the same graph when using our methods. Fig. 10 shows the results when the self-defined area approach is applied (Algorithm 2 in Fig 5 ) while Fig. 11 is related to predefined-area approach (Algorithm 3 Fig. 8). As we can see the cluster structure is clearly presented and the global aesthetic of the two graphs is still quite pleasant.

B. Second example: a citation network

This second example is intended to show that the predefined area drawing we suggest can be used to help appreciating the correlation between the clustering and the binary relationships inherent to the graph structure. The graph we present in this section represents the citations network in the context of graph drawing [START_REF] Biedl | Graph-Drawing contest report[END_REF]. The graph consists in 311 vertices and 647 edges. Each vertex represents a paper published in the International Symposium on Graph Drawing from 1994 to 2000.

We perform an authority analysis [START_REF] Dkaki | Passage Retrieval Using Graph Vertices Comparison[END_REF][30] [START_REF] Blondel | A measure of similarity between graph vertices[END_REF] and obtain an authority score for each vertex. Table 1 shows the top authority scores. This authority score is used to generate eight clusters. Each cluster is composed of papers that have similar authority scores. Actually, the clustering results from the fragmentation of the authority scores into eight segments of the same amplitude. Each cluster is then associated to a prefixed area where the areas are organized as horizontal strips or layers of the same width and positioned on the top of each other's. Clusters on the top of the drawing correspond to nodes that have best authority scores. The resulting drawing (Fig. 12) confirms that citations mainly go from nodes in lower layers to nodes in higher layers. It also shows that papers that obtain high authority scores do not cite each other's. C. third example: a short comparison This third example is intended to compare the results of our method to those of a divide-and-conquer approach.

[10] presents a divide-and-conquer approach to generate visually structured layouts for clustered graphs. The proposed algorithm partitions a graph into sub graphs and composes them to form the resulting layout. To position each vertex, the divide-and-conquer approach uses a composite force that includes intra-forces, progressively increasing inter-cluster forces and gradually decreasing meta forces. The authors propose an example and draw it as follows: Fig. 14 shows the drawing our method outputs.

The two drawings presented in Fig. 13 and Fig. 14 show that while the two methods successfully point out the cluster structure, our method better acknowledges the global structure of the graph. The results we obtained show the potential of our model in dealing with metric values such as authority scores. This work can also help dealing with geographic graph visualization when graphs vertices are grouped according to some of their geographic properties such as the authors' countries or locations in scientific citation networks. Such graph drawing approach will help to understand the implications -if any-of geographic characteristics over the vertices relationships.

  A clustered graph ܩ is a triplet ܩሺܸ, ,ܧ ܲሻ where V is a finite set of vertices, ܧ ⊆ ܸ ൈ ܸ a finite set of edges and ܲ is a partition over ܸ. ܲ⊂c ሺܸሻ the power set of V, ⋃ ܥ ൌ ܸ and ∀ ܥ , ܥ two elements of ܸ, ܲ ܥ ∩ ܥ ൌ ∅ The number of elements in ܲ corresponds to the number of clusters in .ܩ The Fig. 1 illustrates the structure of clustered graphs -the graph in this figure contains three clusters.

Fig. 1 .

 1 Fig. 1. Illustration of the structure of a clustered graph

Fig. 2 .

 2 Fig. 2. The sets of attractive and repulsive forces exercised within a graph of three vertices and two edges. Attractive forces are in green and repulsive ones are in red

Fig. 3

 3 Fig.3shows a pseudo code of Fruchterman and Reingold ' algorithm.

#Fig. 3 .

 3 Fig. 3. Algorithm 1 : Fruchterman and Reingold ' algorithm.

Fig. 4 .##

 4 Fig. 4. Attractive and repulsive forces depend on whether vi and vj belong or not to the same cluster

Fig. 6 .

 6 Fig. 6. The strength of frontier forces over the distance to the frontier. This strength rapidly decrease as the distance separating a vertex from its cluster-frontier reach 2*t

Fig. 7 .#

 7 Fig. 7. The sets of exercised attractive (green) and repulsive (red) and frontier (black) Fig. 8 presents the algorithm we propose. surface ←W * L; # W and L are the width and length of the frame G ←ሺV,E,Pሻ; # The vertices are assigned random initial positions # # ݁݀݅ݏ݊݅ ݄݁ݐ ܽ݁ݎܽ ݕ݄݁ݐ ݈ܾ݃݊݁ ݐ ݄ܶ݁ ݏ݁݅ݎܽ݀݊ݑܾ ݂ ݄݁ܽܿ݁ ݐ݈݊݁݉݁݁ ݂ ݁ݎܽ # ݔ݁ݒ݊ܿ ݏ݁݊݃ݕ݈ ܭ ீ ൌ ඨ ݂݁ܿܽݎݑܵ |ܸ| ܭ ൌ 1 |ܲ| ඨ ݂݁ܿܽݎݑܵ ܥ ܥ| | ݂ ሺ,ݔ ݇ሻ: ݊ݎݑݐ݁ݎ ቆ ݔ ଶ ݇ ቇ ݂ ሺ,ݔ ݇ሻ: ݊ݎݑݐ݁ݎ ቆ ݇ ଶ ݔ ቇ ݂ ௧ ሺݔሻ: ݂݅ ሺݔ ൏ 2 * ݐሻ: ݊ݎݑݐ݁ݎ ቆ ܭ ଶ ݔ ଶ ቇ :݁ݏ݈݁ ݊ሺ0ሻݎݑݐ݁ݎ ݐ ൌ ݐ ; ݁ݏ݈݅ܽ݅ݐ݅݊݅# ݁ݎݑݐܽݎ݁݉݁ݐ ݐ ∆ሺ,ݑ ݒሻ: ifሺu in clusterሺvሻሻ: ߜ←v.pos -u.pos; # δ is the difference vector else: ߜ←v.pos -frontሺvሻ.pos curveሺfrontሺvሻ.pos-frontሺuሻ.posሻ frontሺuሻ.posሻ-u.pos; returnሺߜሻ; :ሻݒሺݐ݊ݎ݂_ݐ frontሺvሻ← nesrest_pointሺv,clusterሺvሻ.boundaryሻ ߜ←v.pos -v.front.pos;# δ is the difference vector returnሺߜሻ; for i ← 0 to :ݏ݊݅ݐܽݎ݁ݐܫܾ݊ # Compute the repulsive forces on vertices for v in V:

Fig. 8 .

 8 Fig.8. Algorithm 3: Our algorithm in the case of pre-defined areas based on[START_REF] Fruchterman | Graph drawing by force-directed placement[END_REF]

Fig. 9 . 1 Fig. 10 .

 9110 Fig. 9. Graph drawing based on algorithm 1

  Graphs with Low Bend Numbers GD 94, 286 Garg, .... On the Compuational Complexity of Upward and Rectilinear Planarity Testing GD 95, 419 Papakostas, ... Issues in Interactive Orthogonal Graph Drawing GD 95, 99 Bruss, ... Fast Interactive 3-D Graph Visualization GD 94, 388 Frick, ... A Fast Adaptive Layout Algorithm for Undirected Graphs GD 95, 8 Alt, ... Universal 3-Dimensional Visibility Representations for Graphs GD 97, 52 Papakostas, ... Incremental Orthogonal Graph Drawing in Three Dimensions GD 95, 234 Fekete, ... New Results on a Visibility Representation of Graphs in 3D Top authority papers from the International Symposium on Graph Drawing from 1994 to 2000

Fig. 12 .

 12 Fig. 12. Drawing of the citation network where vertices are grouped according to their authority score and placed into corresponding layers

Fig. 13 .

 13 Fig.[START_REF] Kobourov | Force-Directed Drawing Algorithms[END_REF]. The grah example as it have been drawn by the divide-and-conquer methode in[START_REF] Storey | Graph layout adjustment strategies[END_REF]

Fig. 14 .

 14 Fig. 14. The grah example given in [10] as it have been drawn our prefixed areas related method V. CONCLUSION In this paper, we have introduced a new energy-based model for clustered graph drawing. Two aspects of the drawing corresponding to self-defined and pre-defined cluster related drawing areas have been addressed; a distinct solution has been proposed for each one of them.

TABLE I .

 I AUTHORITY SCORES OF GD PAPERS[1994][1995][1996][1997][1998][1999][2000]

	Paper	Paper title
	GD 96, 139 Eades,
	...

Two Algorithms for Three Dimensional Orthogonal Graph Drawing. GD 94, 1 Cohen, ... Three-Dimensional Graph Drawing


Beniamino Accattoli

This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.

Proof nets and the call-by-value λ -calculus

In this paper we show how to refine the three actors of the play (the CBV λ -calculus, the translation and the proof nets presentation) in order to get a perfect match between terms and proof nets. Technically, we show that the new translation is a strong bisimulation 1 , and since strong bisimulations preserve reductions length (in both directions), the normalization mismatch vanishes.

, is a subcalculus of the value substitution calculus λ vsub studied in [5], which is a CBV λ -calculus with explicit substitutions. Such a kernel is as expressive as the full calculus, and can be thought as a sort of CPS representation of λ vsub .

 for more details) and rather focus on proof nets. Our two contributions are:

Introduction

A key feature of linear logic (LL) is that it is a refinement of intuitionistic logic, i.e. of λ -calculus. In particular, one β -reduction step in the λ -calculus corresponds to the sequence of two cut-elimination steps in linear logic, steps which are of a very different nature: the first is multiplicative and the second is exponential. The Curry-Howard interpretation of this fact is that λ -calculus can be refined adding a constructor t[x/u] for explicit substitutions, and decomposing a β -step (λ x.t)u → β t{x/u} into the sequence (λ x.t)u → m t[x/u] → e t{x/u}.

Another insight due to linear logic is that proofs can be represented graphically-by the so-called proof nets-and the reformulation of cut-elimination on proof netstakes a quite different flavour with respect to cut-elimination in sequent calculus. The parallel nature of the graphical objects makes the commutative cut-elimination steps, which are the annoying burden of every proof of cut-admissibility, (mostly) disappear.

These two features of LL have influenced the theory of explicit substitutions in various ways [START_REF] Kesner | Resource operators for lambda-calculus[END_REF][START_REF] Di | Proof Nets And Explicit Substitutions[END_REF], culminating in the design of the structural λ -calculus [START_REF] Accattoli | The Structural λ -Calculus[END_REF], a calculus isomorphic (more precisely strongly bisimilar) to its representation in LL proof nets [START_REF] Accattoli | Jumping Boxes[END_REF][START_REF] Accattoli | Jumping around the box: graphical and operational studies on λ -calculus and Linear Logic[END_REF]. Such a calculus can be seen as an algebraic reformulation of proof nets for λ -calculus [START_REF] Danos | La Logique Linéaire appliqué à l'étude de divers processus de normalisation (principalement du λ -calcul)[END_REF][START_REF] Regnier | Lambda-calcul et réseaux[END_REF], and turned out to be simpler and more useful than previous calculi with explicit substitutions.

Girard's seminal paper on linear logic [START_REF] Girard | Linear Logic[END_REF] presents two translations of λ -calculus into LL. The first one follows the typed scheme (A ⇒ B) n =!A n ⊸ B n , and it is the one to which the previous paragraphs refer to. It represents the ordinary-or call-by-name (CBN)-λ -calculus. The second one, identified by (A ⇒ B) v =!(A v ⊸ B v ), was qualified as boring by Girard and received little attention in the literature [START_REF] Maraist | Call-by-name, Call-by-value, Call-by-need and the Linear lambda Calculus[END_REF][START_REF] Pravato | The call-by-value λcalculus: a semantic investigation[END_REF][START_REF] Danos | Reversible, Irreversible and Optimal lambda-Machines[END_REF][START_REF] Fernández | Call-by-Value lambda-Graph Rewriting Without Rewriting[END_REF][START_REF] Fernández | Labelled Lambda-calculi with Explicit Copy and Erase[END_REF][START_REF] Mackie | Encoding Strategies in the Lambda Calculus with Interaction Nets[END_REF]. Usually, it is said to represent Plotkin's call-by-value (CBV) λ β v -calculus [START_REF] Plotkin | Call-by-Name, Call-by-Value and the lambda-Calculus[END_REF]. These two representations concern typed terms only, but it is well-known that they can be extended to represent the whole untyped calculi by considering linear recursive types (o =!o ⊸ o for call-by-name and and o =!(o ⊸ o) for call-by-value).

Surprisingly, the extension of the CBV translation to the untyped calculus λ β v -calculus introduces a violent unexpected behavior: some normal terms in λ β v map to (recursively typed) proof nets without normal form (see [START_REF] Accattoli | A linear analysis of call-by-value λ -calculus[END_REF] for concrete examples and extensive discussions). This fact is the evidence that there is something inherently wrong in the CBV translation.

1. Graphical syntax and algebraic formalism: it is far from easy to realize a strong bisimulation between terms and nets, as it is necessary to take care of many delicate details about weakenings, contractions, representation of variables, administrative reduction steps, and so on. The search for a strong bisimulation may seem a useless obsession, but it is not. Operational properties as confluence and termination then transfer immediately from graphs to terms, and viceversa. More generally, such a strong relationship turns the calculus into an algebraic language for proof nets, providing an handy tool to reason by structural induction over proof nets.

2. Correctness criterion: we provide a characterization of the proof nets representing λ vker based on graph-theoretical principles and which does not refer to λ vker , that is, we present a correctness cri- terion. Surprisingly, the known criteria for the representation of the call-by-name λ -calculus (with explicit substitutions) fail to characterize the fragment encoding the call-by-value λ -calculus. Here we present a simple and non-standard solution to this problem. We hack the usual presentation of proof nets so that Laurent's criterion for polarized nets [START_REF] Laurent | Polarized Proof-Nets: Proof-Nets for LC[END_REF][START_REF] Laurent | Polarized proof-nets and λ µ-calculus[END_REF][START_REF] Laurent | Étude de la polarisation en logique[END_REF]-the simplest known correctness criterion-captures the fragment we are interested in. The hacking of the syntax consists in using boxes for `-links rather than for !-links. An interesting point is that the fragment we deal with is not polarized in Laurent's sense, despite it is polarized in the Lamarche/intuitionistic sense.

The use of boxes for `-links may look terribly ad-hoc. Section 6 tries to argue that it is not. Moreover, Section 7 presents an account of the technical points concerning the representations of terms with proof nets, and how they have been treated in the literature.

Terms

In this section we introduce the calculus which will be related to proof nets, called the value substitution kernel λ vker [2]. Its syntax is:

t, s, u, r ::= x | λ x.t | vs | t[x/u] v ::= x | λ x.t
where t[x/u] is an explicit substitution and values are noted v. Note that the left subterm of an application can only be a value. The rules of λ vker are:

(λ x.t)u → m t[x/u] t[x/vL] → e t{x/v}L
where L is a possibly empty list of explicit substitutions [x 1 /u 1 ] . . . [x k /u k ] (and the fact that in the lhs of → e L appears inside [ ] while in the rhs it appears outside { } is not a typo). The calculus is confluent [START_REF] Accattoli | A linear analysis of call-by-value λ -calculus[END_REF]. The peculiarity of the value substitution kernel is that iterated applications as (tu)s are not part of the language. The idea is that they are rather represented as (xs)[x/tu] with x fresh. The calculus containing iterated applications is called the value substitution calculus λ vsub , and it has been studied in [5, 2]. In [2] it is shown that λ vsub can be represented inside λ vker (mapping iterated applications (tu)s to (xs)[x/tu], as before) and that a term t and its representation t k are equivalent from the point of view of termination (formally t is strongly (resp. weakly) normalizing iff t k is, and the same is true with respect to weaki.e. not under lambda-reduction). If one is interested in observing termination (as it is usually the case) than λ vsub and λ vker are observationally equivalent (via • k ). As pointed out to us by Frank Pfenning, the map • k is reminiscent of the notion of A-reduction in the theory of CPS-translations [START_REF] Flanagan | The Essence of Compiling with Continuations[END_REF][START_REF] Sabry | Reasoning about Programs in Continuation-Passing Style[END_REF]. The idea is then that λ vker (and thus proof nets) is essentially the language of A-normal forms associated to λ vsub . However, the study of the precise relationship with A-normal forms is left to future work.

The calculus λ vsub has been related to Herbelin and Zimmermann's λ CBV [15] in [5]. In turn, λ CBV is related to Plotkin's λ β v in [START_REF] Herbelin | An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form[END_REF], where it is shown that the equational theory of λ β v is contained in the theory of λ CBV .

The rest of the paper shows that λ vker can be seen as an algebraic language for the proof nets used to interpret the call-by-value λ -calculus.

Proof nets: definition

Introduction. Our presentation of proof nets is non-standard in at least four points (we suggest to have a quick look to Figure 3):

1. Hypergraphs: we use hypergraphs (for which formulas are nodes and links-i.e. logical rulesare hyperedges) rather than the usual graphs with pending edges (for which formulas are edges and links are nodes). We prefer hypergraphs because in this way contraction can be represented in a better way (providing commutativity, associativity, and permutation with box borders for free) and at the same time we can represent cut and axiom links implicitly (similarly to what happens in interaction nets).

`-boxes:

We put boxes on `-links and not on !-links. This choice is discussed in Section 6, and it allows to use a very simple correctness criterion-i.e. Laurent's criterion for polarized netswithout losing any property.

3. Polarity: we apply a polarized criterion to a setting which is not polarized in the usual sense.

4. Syntax tree: since we use proof nets to represent terms, we will dispose them on the plane according to the syntax tree of the corresponding terms, and not according to the corresponding sequent calculus proof (also the orientation of the links does not reflect the usual premise-conclusion orientation of proof nets).

Nets. Nets are directed and labelled hyper-graphs G = (V (G), L(G)), i.e., graphs where V (G) is a set of labelled nodes and L(G) is a set of labelled and directed hyperedges, called links, which are edges with 0,1 or more sources and 0,1 or more targets2 . Nodes are labelled with a type in {e, m}, where e stays for exponential and m for multiplicative, depicted in blue and brown, respectively. If a node u has type e (resp. m) we say that it is a e-node (resp. m-node). We shall consider hyper-graphs whose links are labelled from {!, d, w, `, ⊗}. The label of a link l forces the number and the type of the source and target nodes of l, as shown in Figure 1 (the types will be discussed later, and the figure also contains the -link, which is not used to define nets: it will be used later to define the correction graph). Note that every link (except ) has exactly one connection with a little circle: it denotes the principal node, i.e. the node on which the link can interact. Remark the principal node for tensor and !, which is not misplaced. Moreover, every `-link has an associated box, i.e., a sub-hyper-graph of G (have a look to Figure 3). The sources (resp. targets) of a net are the nodes without (resp. outgoing) incoming links; a node which is not a source nor a target is internal. Formally:

Definition 3.1 (net). A net G is a quadruple (|G|, B G , fv(G), r G ), where |G| = (V (G), L(G)
) is an hypergraph whose nodes are labelled with either e or m and whose hyperedges are {!, d, w, `, ⊗}-links and s.t.:

• Root: r G ∈ V (G) is a source e-node of G, called the root of G.
• Conclusions: fv(G) is the set of targets of G, also called free variables of G, which are targets of {d, w}-links (and not of ⊗-links).

• Multiplicative: m-nodes have exactly one incoming and one outgoing link.

• Exponential: an e-node has at most one outgoing link, and if it is the target of more than one link then they all are d-links. Moreover, an e-node cannot be isolated.

• Boxes: For every `-link l there is a net box(l), called the box of l (B G is the set of boxes of G and box(l) ∈ B G ), with a distinguished free variable x, called the variable of l, and s.t.:

-Border: the root r box(l) and the free variable x are the e-nodes of l, and any free variable = x of box(l) is not the target of a weakening.

-Nesting: for any two `-boxes box(l 1 ) and box(l

2 ) if / 0 = I := box(l 1 ) ∩ box(l 2 ), box(l 1 ) ⊆ box(l 2 )
, and box(l 2 ) ⊆ box(l 1 ) then all the nodes in I are free variables of both box(l 1 ) and box(l 2 ).

-Internal closure: any link l of G having as target an internal e-node of box(l) is in box(l).

-Subnet: the nodes and the links of box(l) belong to G and the `-links in box(l) inherit the boxes from G.

Some (technical) comments on the definition. In the border condition the fact that the free variables = x are not (the target) of a weakening means that weakenings are assumed to be pushed out of boxes as much as possible (of course the rewriting rules will have to preserve this invariant). The internal closure condition is a by-product of collapsing contractions on nodes, which is also the reason of the unusual formulation of the nesting condition: two boxes that are morally disjoint can in our syntax share free variables, because of an implicit contraction merging two of their conclusions. Terminology about nets. The level of a node/link/box is the maximum number of nested boxes in which it is contained3 (a `-link is not contained in its own box). Two links are contracted if they share an e-target. Note that the exponential condition states that only derelictions (i.e. d-links) can be contracted. In particular, no link can be contracted with a weakening. A free weakening in a net G is a weakening whose node is a free variable of G. Sometimes, the figures show a link in a box having as target a contracted e-node x which is outside the box: in those cases x is part of the box, it is outside of the box only in order to simplify the representation.

Typing. Nets are typed using a recursive type o =!(o ⊸ o), that we rename e =!(e ⊸ e) =!(e ⊥ `e) because e is a mnemonic for exponential. Let m = e ⊸ e = e ⊥ `e, where m stays for multiplicative.

Note that e =!m and m =!m ⊸!m. Links are typed using m and e, but the types are omitted by all figures except Figure 1 because they are represented using colors and with different shapes (m-nodes are brown and dot-like, e-nodes are white-filled cyan circles). Let us explain the types in Figure 1. They have to be read bottom-up, and thus negated (to match the usual typing for links) if the conclusion of the logical rule is the bottom node of the link, as it is the case for the {w, d, ⊗}-links, while ! and `have their logical conclusion on the top node, and so their type does not need to be negated.

Induced !-boxes. Note that a !-link is always applied to something (m-nodes cannot be conclusions), and there is not so much freedom for this something: either it is a dereliction link or a `with its box. Note also that in both cases we get (what would usually be) a valid content for a !-box. For the dereliction case it is evident, and for the `case it is guaranteed by the definition of net: the content of a `-box ends on e-nodes. Hence, any !-link has an associated box, induced by `-boxes, which needs not to be represented explicitly.

The translation. Nets representing terms have the general form in Figure 2.a, also schematized as in Figure 2.b. The translation • from terms to nets is in Figure 3 (the original boring translation is sketched in Fig. 6, page 12). A net which is the translation of a term is a proof net. Note that in some cases there are various connections entering an e-node, that is the way we represent contraction. In some cases the e-nodes have an incoming connection with a perpendicular little bar: it represents an arbitrary number (> 0) of incoming connections. The net corresponding to a variable is given by a ! on a dereliction and not by an (exponential) axiom, as it is sometimes the case. The reason is that an axiom (in our case a node, because axioms are collapsed on nodes) would not reflect on nets some term reductions, as x[x/v] → e v, for which both the redex and the reduct would be mapped on the same net.

The translation • is refined to a translation • X , where X is a set of variables, in order to properly handle weakenings during cut-elimination. The reason is that an erasing step on terms simply erases a subterm, while on nets it also introduces some weakenings: without the refinement the translation would not be stable by reduction. The clause defining t X∪{y} when y / ∈ fv(t) is the first on the second line of Figure 3, the definition is then completed by the following two clauses: t / 0 := t and t X∪{y} := t X if y ∈ fv(t). α-equivalence. To circumvent an explicit and formal treatment of α-equivalence we assume that the set of e-nodes and the set of variable names for terms coincide. This convention removes the need to label the targets of t X with the name of the corresponding free variables in t or X . Actually, before translating a term t it is necessary to pick a well-named α-equivalent term t ′ , i.e. a term where any two different variables (bound or free) have different names.

' & $ % x = if x ∈ fv(t), λ x.t = if x / ∈ fv(t), λ x.t = if x ∈ fv(u), xu = if x / ∈ fv(u), xu = ! d ! t `! t w `⊗ u d ⊗ u d if y / ∈ fv(t), if x ∈ fv(t), (λ x.t)u = if x / ∈ fv(t), (λ x.t)u = if x ∈ fv(t), t[x/u] = if x / ∈ fv(t), t[x/u] = t X∪{y} = t X w ⊗ u t `... { fv(t)∩fv(u) ⊗ u t w `... { fv(t)∩fv(u) t u . . . { fv(t)∩fv(u) t w u . . . { fv(t)∩fv(u)
Remark 3.2. The translation of terms to nets is not injective. By simply applying the translation it is easily seen that the following pairs of terms have the same net:

t[x/s][y/u] ∼ vo CS t[y/u][x/s] if x / ∈ fv(u) & y / ∈ fv(s) v u[x/s] ∼ vo 1 (v u)[x/s] if x / ∈ fv(v) t[x/s[y/u]] ∼ vo 2 t[x/s][y/u] if y / ∈ fv(t) (1)
Let ≡ vo be the reflexive, transitive, and contextual closure of

∼ vo CS ∪ ∼ vo 1 ∪ ∼ vo 2 .
In the proof of Lemma 5.1, we will use the fact that if t ≡ vo s then t and s are mapped on the same net. We also claim-without proving it-that ≡ vo is exactly the quotient induced on terms by the translation to nets.

Paths. A path τ of length k ∈ N from u to v, noted τ : u → k v, is an alternated sequence u = u 1 , l 1 , . . . , l k , u k+1 = v of
nodes and links s.t. the link l i has source u i and target u i+1 for i ∈ {1, . . . , k}. A cycle is a path u → k u with k > 0.

Correctness. The correctness criterion is based on the notion of correction graph, which is-as usual for nets with boxes-obtained by collapsing every box at level 0 into a generalized axiom link. Definition 3.3 (correction graph). Let G be a net. The correction graph G 0 of G is the hyper-graph obtained from G by collapsing any `-box at level 0 into a -link applying the rule in Fig. 2.c.

Definition 3.4 (correctness). A net G is correct if:

• Source: G 0 has exactly one e-source (the root of G).

• Acyclicity: G 0 is acyclic.

• Recursive correctness: the interior of every box is correct.

As usual an easy induction on the translation shows that the translation of a term is correct, i.e. that: Lemma 3.5. Every proof net is correct.

Proof nets: sequentialization

In this section we show how to extract a term t from every correct net G in such a way that t translates back to G, i.e. we show that every correct net is a proof net. The proof of this fact is based on the notion of kingdom, along the lines of the proof for polarized nets, see [START_REF] Laurent | Étude de la polarisation en logique[END_REF] (pp. 57-63).

Definition 4.1 (Kingdom). Let G be a correct net and x / ∈ fv(G) one of its e-nodes. The kingdom king(x) of x is the set of links defined by induction on the link l of source x:

• l is a !-link: king(x) is given by l plus the d-link or the `-box on the m-target of l.

• l is a ⊗-link: king(x) is given by l plus the d-link or the `-box on the m-target of l plus king(y), where y is the e-target of l.

The main property of king(x) is that it is the smallest subnet of root x, as we shall soon prove 4 . To state this fact precisely we need the notion of subnet. Definition 4.2 (subnet). Let G be a correct net. A subnet H of G is a subset of its links s.t. it is a correct net and satisfying:

• Internal closure: if x is an internal e-node of H then any link of G of target x belongs to H.

• Box closure:

-Root: if a `-link l belongs to H then its box does it too.

-Free variables: if a free variable of a box B of G is internal to H then B ⊆ H.

The following lemma is essentially obvious, and usually omitted, but in fact it is used in the proof of Lemma 4.5.

Lemma 4.3. Let G be a correct net, H a subnet of G, x an internal e-node of H. Then there exists a subnet K of H having x as root and s.t. it is a subnet of G.

Proof. It is enough to show that there is a subnet of H of root x, since it is obvious that any subnet of K is a subnet of G. By induction on the length of the maximum path from x to a free variable of K.

To properly describe kingdoms we need the following definition. Definition 4.4 ((free/ground) substitution). Let G be a correct net. A substitution is an e-node which is the target of a {w, d}-link (or, equivalently, which is not the target of a ⊗-link) and the source of some link. A substitution x is ground if it is a node of G 0 (i.e. it is not internal to any `-box 5 ), and it is free if it is ground and there is no ground substitution of G to which x has a path (in G 0 ).

Lemma 4.5 (kingdom). Let G be a correct net and x /

∈ fv(G) one of its e-nodes. king(x) is the kingdom of x, i.e., the smallest subnet of G rooted at x. Moreover, it has no free substitutions, no free weakenings, and whenever y ∈ fv(king(x)) is internal to a subnet H of G then king(x) ⊆ H.

Proof. Let H be a correct subnet of G rooted at x. We show by induction on the length of the maximum path from x to a free variable of G that king(x) ⊆ H and that king(x) is correct. Let l be the link of source x. Cases:

• Base case: l is a !-link. By the conclusion condition H has to contain the d-link i or the `-link on the m-target of l. In the case of a `-link the box closure condition implies that the whole box B is in H, hence king(x) ⊆ H. In the case of a d-link correctness is obvious, in the case of a `box it follows by the correctness of the interior of the box, guaranteed by the recursive correctness condition. Moreover, no free substitutions and no free weakenings belong to king(x) (boxes cannot close on weakenings). Pick y ∈ fv(king(x)), which in the d-link case is the target of i and in the other case is a free variable of the `-box B. If y is internal to H then the conditions for a subnet guarantee that i or B are in H. Then clearly king(x) ⊆ H.

• Inductive case: l is a ⊗-link. As in the previous case H has to contain the d-link or the `-box on the m-target of l. Moreover, by lemma 4.3 H contains a subnet K rooted in the e-target y of l. By inductive hypothesis king(y) is the kingdom of y, therefore we get king(y) ⊆ K ⊆ H. Hence king(x) ⊆ H. By i.h. we also get that king(y) is correct, hence y is its only e-source and x is the only e-source of king(x). Acyclicity follows by correctness of G. Recursive correctness follows from the box closure condition and correctness of G. Moreover, by i.h. king(y)-and so king(x)-has no free substitutions and no free weakenings. The part about free variables uses the i.h. for the free variables of king(y) and the conditions for a subnet as in the previous case for the other free variables.

Lemma 4.6 (substitution splitting). Let G be a correct net with a free substitution x. Then 1. The free variables of king(x) are free variables of G.

G \ king(x) is a subnet of G.

Proof. 1) Suppose not. Then there is a free variable y of king(x) which is not a free variable of G. There are two possible cases:

• y is a substitution. Then x has a path to a substitution in G 0 , against the definition of free substitution, absurd.

• y is the distinguished free variable of a `-box B. Thus, y is internal to some `-box B and so it is not a node of G 0 . By Lemma 4.5 we get that king(x) ⊆ B and so x is not a node of G 0 , against the definition of free substitution, absurd.

2) By point 1 the removal of king(x) cannot create new e-sources. Being a substitution, x is the target of some link. Therefore the removal of king(x) cannot remove the root of G. It is also clear that the removal cannot create cycles, and the box closure condition for subnets guarantees that the recursive correctness of G implies the one of G \ king(x).

Lemma 4.7. Let G be a correct net with a ground substitution. Then G has a free substitution.

Proof. Consider the following order on the elements of the set S g of ground substitutions of G: z ≤ y if there is a path from z to y in G 0 . Acyclicity of G 0 implies that S g contains maximal elements with respect to ≤, if it is non-empty. Note that a maximal element of S g is a free substitution in G. Now, if G has a ground substitution x then S g is non-empty. Thus, G has a free substitution.

The next lemma is used in the proof of the sequentialization theorem.

Lemma 4.8 (kingdom characterization). Let G be a correct net. Then G = king(r G ) iff G has no free substitutions nor free weakenings.

Proof. ⇒) By Lemma 4.5. ⇐) By lemma 4.5 we get that king(r G ) ⊆ G. If the two do not coincide then by the internal closure condition for subnets, the multiplicative condition on nets, and the fact that they share the same root, we get that G contains a ground substitution x on a free variable of king(r G ). By lemma 4.7 G contains a free substitution, absurd.

Theorem 4.9 (sequentialization). Let G be a correct net and X be the set of e-nodes of its free weakenings. Then there is a term t s.t. t X = G (and fv(G) = fv(t) ∪ X ).

Proof. By induction on the number of links. By the root and conclusion conditions the minimum number of links is 2 and the two links are necessarily a !-link on top of a d-link. Let x be the e-node of the d-link.

Then x = G. We now present each inductive case. After the first one we assume that the net has no free weakening.

• There is a free weakening l of e-node y. Then G ′ = G \ {l} is still a correct net and by i.h. there exist t s.t.

t X\{y} = G ′ . Then t X = G.
• There is a free substitution x. Then by Lemma 4.5 and Lemma 4.6 king(x) and G \ king(x) are correct subnets of G. By the i.h. there exist s and u s.t. s = king(x) and

u {x} = G \ king(x) (note that if x ∈ fv(u) then u {x} = u / 0 = u). Then u[x/s] = G.
• No free substitution: by lemma 4.8 G = king(r G ). In case the root link l of G is:

a !-link over a d-link: base case, already treated.

a !-link over a `-link: let H be the box of the `-link and x its distinguished free variable.

By definition of a net the set of free weakenings of H either is empty or it contains only x. If x is (resp. is not) the node of a free weakening then by i.h. there exists t s.

Proof nets: dynamics

The rewriting rules are in Figure 4. Let us explain them. First of all, note that the notion of cut in our syntax is implicit, because cut-links are not represented explicitly. A cut is given by a node whose incoming and outgoing connections are principal (i.e. with a little square on the line).

The rule → m is nothing but the usual elimination of a multiplicative cut, except that the step also opens the box associated with the `-link.

The two → e rules reduce the exponential redexes. Let us explain how to read them. For the graph noted H in Figure 4 there are two possibilities: either it is simply a dereliction link (a d-link) or it is a ẁith its box, so there is no ambiguity on what to duplicate/erase. Every pair of short gray lines denotes

' & $ % ⊗ `→m w ! H . . . m 1 m k → e w w . . . m 1 m k . . . x d d ! H . . . m 1 m k → e H 1 H k . . . . . . m 1 m k
Figure 4: proof nets cut-elimination rules the sequence (of length m i , with i ∈ {1, . . . , k}) of boxes closing on the corresponding links. The rule has two cases, one where ! is cut with k ∈ {1, 2, . . .} derelictions and one where it is cut with a weakening. In the first case the sub-graph H is copied k times (if k = 1 no copy is done) into H 1 , . . . H k and each copy enters in the m i boxes enclosing the corresponding (and removed) dereliction. Moreover, the k copies of each target of H are contracted together, i.e. the nodes are merged. In the case of a cut with a weakening, H is erased and replaced by a set of weakenings, one for every target of H. Note that the weakenings are also pushed out of all boxes closing on the targets of H6 . This is done to preserve the invariant that weakening are always pushed out of boxes as much as possible. Such invariant is also used in the rule: the weakening is at the same level of H. Last, if the weakenings created by the rule are contracted with any other link then they are removed on the fly (because by definition weakenings cannot be contracted). Now, we establish the relationship between terms and nets at the level of reduction. Essentially, there is only one fact which is not immediate, namely that → e actually implements the → e rule on terms, as it is proved by the following lemma. Lemma 5.1 (substitution). Let t = s[x/vL] then t X → e s{x/v}L X for any set of names X ⊇ fv(t).

Proof. First of all observe that t and s[x/v]L both reduce to s{x/v}L and by remark 3.2 both translate to the same net. Hence it is enough to prove that s[x/v]L X → e s{x/v}L X . We prove it by induction on the number k of substitutions in L. If k = 0 then the proof is by induction on the number n of free occurrences of x in s. Cases:

• n = 0) In s[x/v
] X the bang associated to v is cut with a weakening. The elimination of the cut gets a net G ′ without the !-link and the `-box associated to v, leaving a free weakening for every free variable of the box, i.e. of every free variable of v: then G ′ is exactly s{x/v} X∪fv(v) = s X∪fv(v) .

• n > 1) Write s = C[x] for some occurrence of x. Now, consider u = C[y][y/v][x/v] and note that:

' & $ % a) (λ x.t)u → m t[x/u] ⊗ u t `... { fv(t)∩fv(u) → m t u . . . { fv(t)∩fv(u) b) w ⊗ ! d w ⊗ ! d `! d c) ⊗ ! d
' & $ % x = λ x.t = t u = t[x/u] = ! t ! `⊗ u d t . . . { fv (t)∩fv(u) t u . . . { fv(t)∩fv(u)
Figure 6: the ordinary CBV translation from terms to nets.

Actually, the translation is more than a strong bisimulation: the reduction graphs 7 of t and t are isomorphic, not just strongly bisimilar. An easy but tedious refinement of the proof of Theorem 5.2 proves: Theorem 5.4 (dynamic isomorphism). Let t be a term and X a set of variables containing fv(t). The translation induces a bijection φ between the redexes of t and the redexes of t X s.t. R : t → a t ′ if and only if φ (R) : t X → a t ′ X , where a ∈ {m, e}.

A nice by-product of the strong bisimulation approach is that preservation of correctness by reduction comes for free, since any reduct of a proof-net is the translation of a term.

Corollary 5.5 (preservation of correctness). Let G be a proof net and G

→ G ′ . Then G ′ is correct.
The original boring translation. For the sake of completeness, Figure 6 sketches the ordinary CBV translation from λ -terms (possibly with iterated applications) to proof nets (including the case for explicit substitutions and using a traditional syntax with boxes on !). An easy computation shows that the term t = δ (yz)δ , where δ = λ x.xx maps to a net without normal form, while t is a λ β v -normal form (see [2] for more details). This mismatch is the motivation behind our work.

Motivating `-boxes

The two encodings of λ -calculus can be seen as fragments of Intuitionistic Multiplicative and Exponential Linear Logic (IMELL). Let us stress that in IMELL what we noted ⊗ and `correspond to the right and left rules for the linear implication ⊸, and not to the left and right rules for ⊗ (the four rules for ⊗ and ⊸ are collapsed in LL but not in Intuitionistic LL, in particular our `acts on the output of the term, i.e. on the right of the sequent, and corresponds to the right rule for ⊸).

Our argument is that in IMELL there is no correctness criterion unless the syntax is extended with boxes for both ! and ⊸ (our `), as we shall explain in the next paragraphs. The fragment of IMELL encoding the CBN λ -calculus is a special case where the box for ⊸ needs not to be represented. The fragment encoding the CBV λ -calculus is a special case where the box for ! needs not to be represented. So, the two encodings are dual with respect to the use of boxes, and then there is nothing exotic in our use of `-boxes.

The difficulty of designing a correctness criterion for IMELL is given by the presence of weakenings, which break connectedness. In most cases weakenings simply prevent the possibility of a correctness criterion. The fragment encoding the CBN λ -calculus, and more generally Polarized Linear Logic, are notable exceptions. For the encoding of the CBN λ -calculus there exist two correctness criteria. Let us show that none of them works for the CBV λ -calculus.

The first is the Danos-Regnier criterion, in the variant replacing connectedness with the requirement that the number of connected components of every switching graph is 1 + #w, where #w is the number of weakenings at level 0 (after the collapse of !-boxes) [START_REF] Regnier | Lambda-calcul et réseaux[END_REF]. In our case this criterion does not work: the net in Fig. 5.b verifies the requirement while it does not represent any proof or term. The second criterion is Olivier Laurent's polarized criterion, because the CBN encoding is polarized. In its original formulation it cannot be applied to the encoding of the CBV λ -calculus, because such a fragment is not polarized (there can be a weakening as a premise of a tensor, which is forbidden in polarized logic). Our re-formulation of Laurent's criterion rejects the net in Figure 5.b (because the two `-links form a cycle), but without using `-boxes it would accept the net in Figure 5.c, which is not correct 8 .

Thus, the known criteria do not work and there is no criteria for IMELL. The usual way to circumvent problems about correctness is to add some information to the graphical representation, under the form of boxes (as we did) or jumps (i.e. additional connections). It is well known that in these cases various criteria can be used, but this extra information either is not canonical or limits the degree of parallelism. Another possible solution is to modify the logical system adding the mix rules. However, such rules are debatable, and also give rise to a bad notion of subnet (for details see [START_REF] Accattoli | Jumping around the box: graphical and operational studies on λ -calculus and Linear Logic[END_REF], pp. 199-201).

Let us stress that our counter-examples to the known criteria do not rely on the exponentials (i.e. non-linearity): it is easy to reformulate them in Intuitionistic Multiplicative Linear Logic (IMLL) with units 9 , for which then there is no correctness criterion.

In the case studied in this paper the use of `-boxes does not affect the level of parallelism in a sensible way. Indeed, in IMELL the parallelism given by proof nets concerns the left rules (of ⊗ and ⊸, plus contractions and weakenings) and cuts: in our case there is no ⊗ (remember our ⊗ and `rather correspond to the rules for ⊸), our technical choices for variables keep the parallelism for contraction and weakenings, and the parallelism of the left rule for ⊸ (our ⊗) and cuts is preserved (it is given by the equations in (1), page 6).

Proof nets: the literature on term representations

When relating λ -terms and proof nets a number of technical choices are possible:

1. Explicit substitutions: proof nets implement a β -step by two cut-elimination steps. This refined evaluation can be seen on the calculus only if the syntax is extended with explicit substitutions.

2.

Variables: to properly represent variables it is necessary to work modulo associativity and commutativity of contractions, neutrality of weakening with respect to contraction, and permutations of weakenings and contractions with box-borders. In the literature there are two approaches: to explicitly state all these additional congruences or to use a syntax naturally quotienting with respect to them. Such a syntax uses n-ary ?-links collapsing weakening, dereliction and contractions and delocalizing them out of boxes. It is sometimes called nouvelle syntaxe.

3. Axioms: various complications arise if proof nets are presented with explicit axiom and cut links. They can be avoided by working modulo cuts on axioms, which is usually done by employing an interaction nets presentation of proof nets.

4. Exponential cut-elimination: the cut-elimination rules for the exponentials admit many presentations. Essentially, either they are big-step, i.e. an exponential cut is eliminated in one shot (making many copies of the !-premise of the cut), or they are small-step, with a rule for each possible ?-premise (weakening, dereliction, contraction, axiom, box auxiliary port).

We now list the works in the literature which are closer in spirit to ours, i.e. focusing on the representation of λ -calculi into proof nets (and for space reasons we omit many other interesting works, as for instance [START_REF] Mackie | Encoding Strategies in the Lambda Calculus with Interaction Nets[END_REF], which studies the representation of strategies, not of calculi). The first such works were the Ph.D. thesis of Vincent Danos [START_REF] Danos | La Logique Linéaire appliqué à l'étude de divers processus de normalisation (principalement du λ -calcul)[END_REF] and Laurent Regnier [START_REF] Regnier | Lambda-calcul et réseaux[END_REF], which focused on the call-by-name (CBN) translation. Danos and Regnier avoid explicit substitutions, use n-ary contractions, explicit axioms, and big-step exponential rules, see also [START_REF] Danos | Proof-nets and the Hilbert space[END_REF]. They characterize the image of the translation using the variant on the Danos-Regnier correcteness criterion which requires that any switching graph has #w + 1 connected components, where #w is the number of weakenings. In [START_REF] Danos | Reversible, Irreversible and Optimal lambda-Machines[END_REF] Danos and Regnier use the CBV translation 10 . Both translations are injective.

In [START_REF] Laurent | Polarized proof-nets and λ µ-calculus[END_REF][START_REF] Laurent | Étude de la polarisation en logique[END_REF] Olivier Laurent extends the CBN translation to represent (the CBN) λ µ-calculus. He does not use explicit substitutions nor n-ary ?-links, while he employs explicit axiom links and smallstep exponential rules. His work presents two peculiar points. First, the translation of λ µ-terms is not injective, because-depending on the term-the µ-construct may have no counterpart on proof nets. This induces some mismatches at the dynamic level. Second, Laurent finds a simpler criterion, exploiting the fact that the fragment encoding (the CBN) λ µ-calculus is polarized. In [START_REF] Laurent | Étude de la polarisation en logique[END_REF] Laurent also show how to represent the CBV λ µ-calculus. However, such a representation does not use the same types of the boring translation, as A → B maps to ?!(A ⊸ B), and not to !(A ⊸ B).

Lionel Vaux [START_REF] Vaux | λ -calcul différentiel et logique classique: interactions calculatoires[END_REF] and Paolo Tranquilli [START_REF] Tranquilli | Nets Between Determinism and Nondeterminism[END_REF][START_REF] Tranquilli | Intuitionistic differential nets and lambda-calculus[END_REF] study the relationship between the differential λcalculus and differential proof nets. Vaux also extends the relationship to the classical case (thus encompassing a differential λ µ-calculus), while Tranquilli refines the differential calculus into a resurce calculus which better matches proof nets. They do not use explicit substitutions, nor n-ary contractions, while they use interaction nets (so no explicit axioms and cut link) and small-step exponential rules. Both Tranquilli and Vaux rely on the Danos-Regnier criterion, despite the fragment encoding their calculi is polarized and can be captured using Laurent's criterion by using boxes for coderelictions; in the context of λ -calculus such boxes do not reduce the parallelism of the representation.

Delia Kesner and co-authors [START_REF] Di | Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract)[END_REF][START_REF] Di | Proof Nets And Explicit Substitutions[END_REF][START_REF] Kesner | Resource operators for lambda-calculus[END_REF]] study the relationship with explicit substitutions (in the CBN case). The main idea here is that explicit substitutions correspond to exponential cuts. They use explicit axiom links and small-step exponential rules, but they do not employ n-ary contractions (and so they need additional rules and congruences). Because of explicit substitutions the translation is not injective: now different terms may map to the same proof net, as in this paper. They do not deal with correctness.

In none of these works the translation is a strong bisimulation. In [START_REF] Accattoli | Jumping Boxes[END_REF] the author and Stefano Guerrini use a syntax inspired by proof nets (and extended with jumps) to represent the CBN λ -calculus with explicit substitutions. That work is the only one employing (the equivalent of) n-ary ?-links and (the equivalent of) small-step exponential rules. In [START_REF] Accattoli | Jumping Boxes[END_REF] the correctness criterion is a variation over Lamarche's criterion for essential nets, which relies in an essential way on the use of jumps. A reformulation in the syntactic style of this paper of both [START_REF] Accattoli | Jumping Boxes[END_REF] and of Danos and Regnier's proof nets for the CBN λ -calculus can be found in [START_REF] Accattoli | Jumping around the box: graphical and operational studies on λ -calculus and Linear Logic[END_REF], together with a detailed account of the strong bisimulation.

Here, hypergraphs allow us to use n-ary ?-links and collapse axioms and cut links (as if we were using interaction nets). More precisely, we represent n-ary ?-links by allowing e-nodes to have more than one incoming link. This choice overcomes some technicalities about gluing and de-gluing of ?links. Such technicalities are always omitted, but they are in fact necessary to properly define subnets and cut-elimination. We also employ big-step exponential rules and explicit substitutions.

Figure 1 :

 1 Figure 1: links.

Figure 2 :

 2 Figure 2: various images.

Figure 3 :

 3 Figure 3: the translation from terms to nets.

Figure 5 :

 5 Figure

A strong bisimulation between two rewriting systems S and R is a relation ≡ between S and R s.t. whenever s ≡ r then for every step from s → S s ′ there is a step r → R r ′ s.t. s ′ ≡ r ′ , and viceversa (for s, s ′ ∈ S and r, r ′ ∈ R).

An hyper-graph G can be understood as a bipartite graph B G , whereV 1 (B G ) is V (G) and V 2 (B G ) is L(G), and the edges are determined by the relations being a source and being a target of an hyperedge.

Here the words maximum and nested are due to the fact that the conclusions of `-boxes may belong to two not nested boxes, because of the way we represent contraction.

We call kingdom of x the net in def. 4.1, but at this point nothing guarantees that it is the smallest subnet of root x.

Note that our collapsed representation of contractions and cuts does not allow to simply say that x is a node at level 0: indeed the conclusion of a `-box can have level > 0 and yet belong to G 0 .

Note that, for the sake of a simple representation, the figure of the weakening cut-elimination rule is slightly wrong: it is not true that the links l 1 , . . . , l j having as target a given conclusion x i of H are all inside m i boxes, because each one can be inside a different number of boxes.

Reduction graphs, which are the graphs obtained considering all reductions starting from a given object, are not nets.

The net in Figure5.c would be rejected by the original version of the criterion, which is based on a different orientation. But the original orientation cannot be applied to our fragment.

Just replace each sequence of a ! over a dereliction with an axiom, and the weakenings with ⊥-links.

Proof nets and the call-by-value λ -calculus

Let us point out that[START_REF] Danos | Reversible, Irreversible and Optimal lambda-Machines[END_REF] presents an oddity that we believe deserves to be clarified. The authors show that an optimized geometry of interaction for the proof nets of the CBV-translation is isomorphic to Krivine' s abstract machine (KAM): this is quite puzzling, because the KAM is CBN, while they use the CBV translation.

Acknowledgements. To Stefano Guerrini, for introducing me to proof nets, correctness and the representation of λ -terms, and to Delia Kesner, for helping with the financial support of this work.

u → C[v][x/v] → C[v]{x/v} = s{x/v}

The difference between G ′ = u X and G = s[x/v] X is that one of the occurrences of x in G has been separated from the others and cut with a copy of v. Consider the step G → H which reduces the cut on x in G and the sequence G ′ → H ′ y → H ′ y,x which first reduces the cut on y in G ′ and then reduces in H ′ the (unique) residual of the cut on x in G ′ . By the definition of reduction in nets H = H ′ y,x . Now by i.h. applied to u and y we get that -If s = w[y/u] then either x ∈ u or x ∈ w. In the first case by remark 3.2 we get that s

Strong bisimulations preserve reduction lengths, so they preserve divergent/normalizing reductions, and termination properties in general.

Technical digression about confluence. For confluence the point is slightly more delicate, since in general it is preserved only modulo the quotient induced by the strong bisimulation. But mild additional hypothesis allow to transfer confluence. Given two rewriting systems (S 1 , →) and (S 2 , ) and a strong bisimulation ≡ (defined on all terms of S 1 and S 2 ), to transfer confluence from S 1 to S 2 it is enough to ask that if s 1 ≡ s 2 and s 1 → s ′ 1 then there is a unique s ′ 2 s.t. s 2 s ′ 2 and s 2 ≡ s ′ 2 , see [START_REF] Accattoli | Jumping around the box: graphical and operational studies on λ -calculus and Linear Logic[END_REF] (pp. 83-86) for more details. It is easily seen that in our case the translation enjoys this property in both directions.

These observations (and confluence of λ vker ) prove:

Corollary 5.3. Let t ∈ λ vker and X a set of variables. Then t is weakly normalizing/strongly normalizing/a normal form/without a normal form iff t X is. Moreover, proof nets are confluent.