Denis Lugiez
email: denis.lugiez@lif.univ-mrs.fr

Stéphane Martin
email: stephane.martin@lif.univ-mrs.fr

Peer to Peer Optimistic Collaborative Editing on XML-like Trees

Keywords: Peer to Peer, Concurrent Processes, Collaborative Editing, Optimistic reconciliation, XML

Collaborative editing consists in editing a common document shared by several independent sites. Conflicts occurs when different users perform simultaneous uncompatible operations. Centralized systems solve this problem by using locks that prevent some modifications to occur and leave the resolution of conflicts to users. Optimistic peer to peer (P2P) editing doesn't allow locks and uses a Integration Transformation IT that reconciliates conflicting operations and ensures convergence (all copies are identical on each site). Two properties TP1 and TP2, relating the set of allowed operations Op and the transformation IT, have been shown to ensure convergence. The choice of the set Op is crucial to define an integration operation that satisfies TP1 and TP2. Many existing algorithms don't satisfy these properties and are incorrect. No algorithm enjoying both properties is known for strings and little work has been done for XML trees in a pure P2P framework. We focus on editing XML-like trees, i.e. unranked-unordered labeled trees also considered in the Harmony project. We show that no transformation satisfying TP1 and TP2 exists for a first set of operations but that TP1 and TP2 hold for a richer set of operations, provided that some decoration is added to the tree. We show how to combine our approach with any convergent editing process on strings to get a convergent process. We have implemented our transformation using a P2P algorithm inspired by Ressel et al. whose correctness relies on underlying partial order structure generated by the dependence relation on operations.

Introduction

Collaborative edition is a concurrent process that allows separate users -sites-to work on the same data called a collaborative object using a set of defined operations. Distinct authors working on the same article, shared calendar, on-line encyclopedia are example of such processes. This activity can be centralized by a distinguished site that coordinates and resolves the conflicts that can arise from concurrent access to the same resource -for instance two sites want to insert two distinct character at the same position in a word-, like in the subversion system (svn). A more liberal approach relies on a peer to peer process (in short P2P) where the set of users in not fixed in advance and where no central site coordinates the process. Therefore conflict resolution is much more complex, especially when one has an optimistic approach that considers that each operation is meaningful and must be taken into account. A simpler solution that relies on priority attributed to users and undoing conflicting operations can lead to a situation where only the operations of one user are performed and all other operations are discarded, which is the opposite of a cooperative work. Therefore a main issue in collaborative edition is to ensure convergence (i.e. each user gets the same copy of the shared data) in the optimistic framework. The Integration Transformation approach uses a operator IT that combines concurrent operations to get a new operation merging the effect of these concurrent operations to resolve the conflicts. Convergence is proved when this transformation enjoys two properties TP1 and TP2. The problem is hard for linear structures like words and most algorithms proposed [START_REF] Ressel | An integrating, transformation-oriented approach to concurrency control and undo in group editors[END_REF][START_REF] Suleiman | Serialization of concurrent operations in a distributed collaborative environment[END_REF][START_REF] Li | Ensuring content and intention consistency in real-time group editors[END_REF] are non-trivial. Unfortunately recent works [START_REF] Imine | Formal design and verification of operational transformation algorithms for copies convergence[END_REF] show that these algorithm don't have the convergence property. Furthermore, few results have been obtained for tree-like structures in a pure P2P optimistic framework which is the basis for collaborative edition on XML-documents (the solution in [START_REF] Oster | Supporting collaborative writing of XML documents[END_REF] uses time-stamp, i.e. a central server). In this paper we concentrate on labeled unranked-unordered trees, called XML-like trees-which are already considered in the Harmony project [START_REF] Pierce | Bringing Harmony to optimism: A synchronization framework for heterogeneous tree-structured data[END_REF] and also provides a close approximation to XML-documents (in many applications, the ordering on siblings on XML document is not relevant). Our first results states that no IT transformation can exist for a first basic set of operations. Then we refine the data structure and we give a rich set of operations that allows to define an IT transformation satisfying TP1 and TP2. The proof has been automated with the Vote system [START_REF] Imine | Conception Formelle d'Algorithmes de Réplication Optimiste[END_REF] which uses Spike, a theorem prover based on term rewriting. Then we show how to combine this data structure with another date structure for which a convergent algorithm exists to get convergence for the composed data structure. This results allows collaborative editing on a complex data structure combining a tree-like structure and other basic structure like words.

Section 2 gives the basic definitions, section 3 describes the main basic data structures words and trees. Then we give the negative results for these collaborative objects in section 4. The new tree-like collaborative object is given in section 5 as well as an integration transformation that ensures convergence. Combination of convergent algorithm are given in Section 6 and Section 7 discusses implementation issues.

The Framework

Collaborative Editing and Convergence

A collaborative object consists of a type (calendar, XML document,. . . ) that defines the set of states, a set Op of operations and an operator Do that applies an operation op to a state s (i.e. an element of the type) to get another state op(s) that is denoted by Do(s, op). For instance, the collaborative object word consists of Σ * the set of words on an alphabet Σ, operations InsCh(p,c) to insert character c at position p, and DelCh(p) to delete the character at position p and Do operation simply applies these deletion or insertion to the current state (which is some word). A sequence of operations is called an history and denoted by [op 1 ; op 2 ; . . . ; op n ] and we use the notation [op 1 ; op 2 ; . . . ; op n ](s) to denote Do(. . . , Do(Do(s, op 1 ), op 2 ), . . . , op n ) (apply op 1 first, then op 2 ,. . . ).

Collaborative editing is a special kind of concurrent programming on a shared collaborative object shared by distinct sites. Centralized systems like svn have a system of locks that prevent conflicts1 , but pure P2P systems have no centralization process that enforce each site to have the same data. The optimistic approach assumes that no operation is lost and the main issue is to ensure convergence, i.e. all sites eventually have the same copy of the shared object.

Requests and computations. Each site generate local requests that consists of some operation op to execute on the shared object plus additional information (site identifier, operation number, history,. . . ).

Each local request is broadcast to all other sites and we assume that no messages is lost and that the execution ordering doesn't exchange messages. Requests generated and received by each site are queued and extracted from the queue to be executed, i.e. the operation is performed on the current copy of the collaborative object. Local requests are linearly ordered and the execution of requests respects this ordering. Therefore requests can be causally related or concurrent (requests generated independently by distinct sites)

The causality relation and concurrent request. Let r i 1 be generated by site i and r j 2 generated by site j. The causality relation ≻ is defined by r i 1 ≻ r j 2 iff either i = j and r i 1 is generated before r j 2 or i = j and the request r i 1 is executed on site j before r j 2 . The relation ≻ is a partial order and we say that two requests r and r ′ are concurrent, denoted by r r ′ , iff r ≻ r ′ and r ′ ≻ r. In the following, we identity a request and the operation it conveys, and we extend ≻ to operations.

Concurrency may lead to conflicts: For instance two distinct sites insert different characters at the same position. These conflicts are solved using a transformational approach. Assume that a site s has performed operation op and that it receives an request containing operation op ′ that has been issued by another site s ′ concurrently to op (i.e. op op ′ ). Instead of executing op ′ , the site s executes IT (op ′ , op), the transformation of operation op ′ according to op. Meanwhile site s ′ , which has executed op ′ and receives a request to execute op will execute IT (op, op ′ ).

The convergence property states that all sites share the same copy of the collaborative object after they have processed all requests.

The Integration Transformation and the Convergence Theorem

The Integration function IT takes two operations op 2 issued by site 2 and op 1 issued by site 1 and returns a operation IT (op 2 , op 1 ) ∈ Op that site 1 executes. Meanwhile site 2 executes IT (op 1 , op 2 ). This integration function IT is extended to integrate an operation with a set of concurrent operations (see [START_REF] Imine | Conception Formelle d'Algorithmes de Réplication Optimiste[END_REF]). The classical properties required for ensuring convergence are:

-T P A main issue in collaborative editing is, given a collaborative object, design an IT function that satisfies TP1 and TP2. A related issue is to design the most expressive set of operations, such that there exists an IT satisfying TP1 and TP2. The larger the set of operations, the better but extending the set of operations results in a combinatorial explosion when proving TP1 and TP2. At the present time, no set of operations has been designed to handle XML-like documents in a pure P2P approach.

An Abstract Description of Editing Algorithm

Each site has a set of local variables i, s, h, . . . site identifier, current state of the shared object, history,. . . and an environment E is a set of values of these variables (for all sites). A request is a tuple of values i, opnb, op, . . . (site identifier, operation numbering, operation,. . . . The set of environment is Env and the set of request is Req.

Local transitions are described by a transition function ϕ l : Op × Env → Env that given an operation op ∈ Op, a current environment E computes the new environment E ′ corresponding to the execution of op. The request r l sent to other sites is the value of some of the local variables. This process is described as ϕ l .!r l .

An external request r e is followed by a local computation ϕ e : Req×Env → Env updating the local variables (using the IT function but possibly other functions). This process is described as ?r e .ϕ e . A collaborative editing algorithm on a collaborative object is described by Env, Req, ϕ l , ϕ e (assuming that transformations like IT and possibly other functions are already defined).

Each site performs a non deterministic choice between the two processes and repeats this computation until all messages are processed. A computation is a sequence of ϕ l (op, E).!r l and ?r e .ϕ e (E) that results from an interleaving of the computations on each site respecting the causality relation.

Words and Tree-like Data Structures

In this section, we recall some known facts on words and set up a first approach for XML-like trees.

The collaborative object word is given by the set of words on a finite alphabet Σ and the operations InsCh(p, c) that inserts a character c ∈ Σ at position p ∈ P os, DelCh(p) that deletes the character at position p ∈ P os and Nop() where P os is the set of positions i.e. sequences of integers. Several Transformations IT have been defined but none satisfies both T P 1 and T P 2 (see section 4). Some variants of this object use slightly a more elaborated data type and operations to keep track of operations performed at a given position or for a given character.

The tree data structure that we define is already used in the Harmony project [START_REF] Pierce | Bringing Harmony to optimism: A synchronization framework for heterogeneous tree-structured data[END_REF]. Let N be a set of names, the set T of unordered unranked edge labeled trees is defined by the grammar:

T ::= {} //Empty tree | {n 1 (T ), ..., n m (T )} n i ∈ N , n i = n j if i = j //Set of tree
The definition ensures that two edges issued from the same node have different labels: i.e. a given label occurs at most once on siblings. Trees are unordered i.e., for any permutation σ, we have that

{n 1 (t 1 ), . . . , n m (t m )} = {n σ(1) (t σ(1) ), . . . , n σ(m) (t σ(m) )}.
In figures, we draw {} as a node, and we add a root node to a tree {n 1 (t 1 ), . . . , n m (t m )}. A path is a sequence of names, ǫ is the empty path and p.p ′ is the concatenation of paths p and p ′ . The set of paths is written P. The projection of tree t along a path p, written t |p , is defined by t |ǫ = t and t |n.p = t |n |p , n ∈ Σ, p ∈ P. We write p 1 ⊳ p 2 , when a path p 1 is a prefix of another path p 2 .

The operations that we consider are:

-Add(p, n) : Add a edge labeled n at end of path p.

Add(n ′ .p, n)({n 1 (t 1 ), ..., n q (t q )}) = {n 1 (t 1 ), ..., n q (t q ), n ′ (Add(p, n)({}))} if n ′ ∈ Dom(t) Add(n i .p, n)({n 1 (t 1 ), ..., n i (t i ), ..., n q (t q )}) = {n 1 (t 1 ), ..., n i (Add(p, n)(t i )), ..., n q (t q )} Add(ǫ, n)(t) = t, if n ∈ Dom(t) Add(ǫ, n)({n 1 (t 1 ), ..., n q (t q )}) = {n 1 (t 1 ), ..., n q (t q ), n({})} Example : t ′ =
Exp ::= op(y 1 , . . . , y p ) | if Cond then Exp else Exp2 fi op ∈ Op Cond ::= x ⊲⊳ y | Cond ∧ Cond | ¬Cond
where ⊲⊳ denotes = or ⊳, x, y are variables or expressions p.n. This grammar capture the natural definitions of any operation on trees from the basic operations of Op excepting iteration and recursion which are out of scope in our framework.

Theorem 2. There is no definition of IT (op 1 , op 2 ) from Op such that IT satisfies T P 1.

We can restore T P 1 and T P 2 using a stronger notion of deletion (See Appendix 8.3). Let Del 2 be the operation deleting the entire subtree and let Op ′ = {Nop(), Add(p, n), Del 2 (p, n)} p ∈ P, n ∈ Σ. Theorem 3. There is a IT for Op ′ that satisfies T P 1 and T P 2.

Unordered Unranked Trees Revisited

In collaborative edition each site is identified by its number and numbers the operations that it performs. This ordering is linear and unambiguous. When a tree is constructed from the empty tree, one can uniquely label each edge by the site number and the numbering of the operation that has created this edge. Since we can also add labels like those of XML-documents, we have a data structure that corresponds to unordered XML documents where the edges are labeled by an item occurring once in the tree.

The Data Structure

A identifier is either one of the reserved names doc (for document) or mem (for memory) or a pair of natural numbers (site, nbop) where the site denotes a site number and nbop denotes an operation number. ID denotes the set of identifiers. A label l is an element of a set of labels L (for instance section, paragraph,. . . ).

We consider trees defined as in section 3 on the set of names N = L × ID assuming that each identifier occurs once in the tree.

T ::= {} | {(l 1 , id 1 )(T ), ..., (l m , id m )(T )}
where each id i 's occurs once in the whole tree. Example 2. From now on, ⊕ denotes the union of multisets. Actually, we use this operation only for disjoint sets, computing a set (not a multiset). We define two projection operations:

The projection t | id of t in id is defined by {} | id i = {} and {(l 1 , id 1 )(t 1 ), ..., (l i , id i )(t i ), ..., (l m , id m )(t m )} | id i = t i {(l 1 , id 1 )(t 1 ), ..., (l m , id m )(t m )} | id = t 1| id ⊕ ... ⊕ t m| id and the second projection t ⌈ id i is defined by {} ⌈ id i = {} and {(l 1 , id 1 )(t 1 ), ..., (l i , id i )(t i ), ..., (l m , id m )(t m )} ⌈ id i = {(l i , id i )(t i )} {(l 1 , id 1 )(t 1 ), ..., (l m , id m )(t m )} ⌈ id = {t 1⌈ id , ..., t m⌈ id } Example 3. Let t be as above, then:

t | 3;1 = {(0491543545, 4; 1)({})} t ⌈ 3;1 = {(Home, 3; 1)({(0491543545, 4; 1)({})})}
Each tree can be transformed into an (unordered) XML tree by the tree morphism defined by ϕ({}) = {} and ϕ({(l 1 , id 1 )(t 1 ), . . . , (l m , id m )(t m )}) = {(l 1 )(ϕ(t 1 )), . . . , (l m )(ϕ(t m ))}

Gluing Memory and Tree in a Single Tree

As already mentioned, the collaborative object that we use consists in two parts: one is a tree that represents the document that we edit and the other one is a memory where we keep some previous parts of the document that have been erased. The memory is needed because solving conflicts may require to fetch parts of the trees in the memory to update the document part (this comes from the move operation Mv). To get a uniform definition for operations, we represent the memory and the document in a single tree, so-called well-formed tree. A well-formed tree is a tree of the form {(⊥, data)(t d ), (⊥, mem)(t m )} where ⊥ is some new label.

The Set of Operations Op. Firstly, we define two auxiliary functions:

-Erase(id, t) deletes the node having identifier id in t.

Erase(id, {}) = {} Erase(id, {(l 1 , id 1 )(t 1 ), ..., (l q , id q )(t q )}) = {(l 1 , id 1 )(Erase(id, t 1 )), ..., (l q , id q )(Erase(id, t q ))} Erase(id, {(l 1 , id 1 )(t 1 ), ..., (l id , id)(t id ), ..., (l q , id q )(t q )}) = {(l 1 , id 1 )(t 1 ), . . . , (l i-1 , id i-1 )(t i-1 , (l i+1 , id i+1 )(t i+1 ), . . . , (l q , id q )(t q )} -AddT ree(id, s, t) adds s under identifier id in t (performing union of s and of the subterm in t).

AddT ree(id p , t ′ , {}) = {} AddT ree(id p , t ′ , {(l 1 , id 1 )(t 1 ), ..., (l q , id q )(t q )}) = {(l 1 , id 1 )(AddT ree(id p , t ′ , t 1 )), ..., (l q , id q )(AddT ree(id p , t ′ , t q ))} AddT ree(id, t ′ , {(l 1 , id 1 )(t 1 ), ..., (l id , id)(t i d), ..., (l q , id q )(t q )}) = {(l 1 , id 1 )(t 1 ), ..., (l id , id)(t id ⊕ t ′ ), ..., (l q , id q )(t q )} Let Op = {Add(id p , n, id), Del(id), Mv(id, id p ), Ren(id, n), Nop()}, where id ∈ ID \ {data, mem}, id p ∈ ID, n ∈ Σ be the new set of operations.

-Add(id p , id): Add a edge labeled noV alue with identifier id under a node whose identifier is id p .

Add(id p , id)(t) = AddT ree(id p , {(id, NoV alue)({})}, t)

-Del(id): Delete a node id and store deleted subtree in memory.

Del(id)(t) = AddT ree(mem, t | id , Erase(id, t))

-Mv(id, id p ): Move node id under node id p Mv(id, id p )(t) = AddT ree(id p , t ⌈ id , Erase(id, t))

-Ren(id, n): Change label of node id Ren(id, l)({}) = {} Ren(id, l)({(l 1 , id 1 )(t 1 ), ..., (l q , id q )(t q )}) = {(l 1 , id 1 )(Ren(id, l)(t 1 )), ..., (l q , id q )(Ren(id, l)(t q ))} Ren(id, l)({(l 1 , id 1 )(t 1 ), ..., (n ′ , id)(t i ), ..., (l q , id q )(t q )}) = {(l 1 , id 1 )(t 1 ), ..., (n, id)(t i ), ...(l q , id q )(t q )} -Nop(): Do nothing. Nop()(t) = t

Besides basic operations for adding and deleting edges, we add two useful operations, one for renaming labels (change a \section to a \subsection for instance) and another one for moving parts of a tree (let's move the \theorem before the \corollary for instance). This last operation is the reason why we need a memory part in the tree.

Proposition 2. Let t be a well-formed tree, let op ∈ Op, then op(t) is a well-formed tree.

Remark 1. By definition an identifier id is created once since it is equal to (site, nbop) where site is the number of the site which has created it and nbop is the numbering of the creation operation. Therefore if the edge corresponding to this identifier is created, and deleted later on, it cannot be re-created (since the numbering or the site number is different). An edge can be created at the "same" place 2 , but with a different identifier.

The IT Transformation

Theorem 4. The transformation IT defined in figure 1 satisfies TP1 and TP2.

Proof. The proof relies on a highly combinatorial case analysis and was double checked using the Vote tool [START_REF] Imine | Conception Formelle d'Algorithmes de Réplication Optimiste[END_REF].

IT (Add(idp, id), Add(id ′ p , id ′ )) = Add(idp, id),

IT (Add(idp, id), Del(id ′ )) = 8 < : N op() if id = id ′ Add(mem, id) if idp = id ′ Add(idp, id) otherwise IT (Del(id), Add(id ′ p , id ′ )) = Del(id) IT (Del(id), Del(id ′ )) = Del(id) IT (Ren(id1, l1), Ren(id2, l2)) =  N op() if s2 < s1 ∧ id1 = id2 Ren(id1, l1) otherwise. IT (Ren(id1, l1), op) = Ren(id1, l1) if op = Ren IT (op, Ren(id1, l1)) = op if op = Ren IT (M v(id1, idp), M v(id2, id ′ p )) =  N op(), if s2 < s1 ∧ id1 = id2 M v(id1, idp) otherwise IT (M v(id1, idp), Del(id ′ )) = 8 < : M v(id1, mem) if idp = id ′ N op() if id1 = id ′ M v(id1, idp) otherwise IT (M v(id1, id2), op) = M v(id1, id2) if op = M v, Del IT (op, M v(id1, id2)) = op if op = M v IT (op1, N op()) = op1 IT (N op(), op2) = N op();
where idp, id ′ p ∈ ID, id ∈ ID \ {data, mem}. Composition of Trees and Words. Let (T, Op T , Do T ) be the collaborative object obtained from trees and the set of operations defined in section 5. Let Dom(t) be the set of identifier occurring in t ∈ T . Let Data = (D, Op D , Do D , ) be another collaborative object. We assume that d 0 ∈ D is the default initial value for elements of type D. Let δ : ID → D be a labelling function that associates to each id ∈ ID some element d = δ(id) of Data. A labeled tree is a pair t, δ and T (D) denotes the set of labeled trees. For instance the labelling can associate to each identifier id a string that can be the information stored at the terminal node of the edge labeled by id, we call this data structure XML-like trees. We define the collaborative object T (Data), the trees parameterized by Data, as follows:

-The set of states is T (D), -The set Op of operations is composed of op id for id ∈ ID, op id ∈ Op D , and op where op ∈ Op T .

-The Do function is defined by Do((t, δ), op id ) = (t, δ ′ ) where the labelling δ is identical to δ except that δ ′ (id) = op(δ(id)). Do((t, δ), op) = (t ′ , δ ′ ) where t ′ = Do(t, op) and δ ′ is identical to δ except that δ(id) = d 0 (the default value of D) if id is an identifier not occurring in t.

Composition of Convergent Algorithms. Let A T be a convergent collaborative editing algorithm for T defined by Env T , Req T , ?r T e .ϕ T e , ϕ T l .!r T l and let let A D be a convergent collaborative editing algorithm for Data defined by Env D ,Req D , ?r D e .ϕ D e , ϕ D l .!r D l . We define a collaborative editing algorithm for T (D) by composing both algorithm in a product-like way. Environments have the form E T , E D where E T ∈ Env T and E D is a partial function ID → Env D . The function is defined for id ∈ Dom(s) where s ∈ E T is the state of the collaborative object. Similarly requests have the form r T , ⊥ or ⊥, r D where ⊥ stands for undefined, r T ∈ Req T and r D is a pair (id, r) with id ∈ ID, r ∈ Req D . The set of environment is denoted by Env, the set of requests is denoted by Req. The composition is defined by Let XML-like documents be labeled unranked-unordered trees decorated with strings. Since convergent algorithms for words exist (more complex than algorithms using IT , see [START_REF] Li | Commutativity-based concurrency control in groupware[END_REF][START_REF] Imine | Conception Formelle d'Algorithmes de Réplication Optimiste[END_REF] for instance) and since the transformation IT of section 5 is TP1 and TP2, we have: Theorem 6. There exists a convergent editing algorithm for XMLlike documents.

-Local computation φ l : Op, Env → Env where φ l (op, E T , E D ) = ϕ T l (op, E T ) and r l = r T l , ⊥ if op ∈ Op T φ l (op, E T , E D ) = ϕ D l (
The algorithm follows the lines given at section 2.3. It is similar to [START_REF] Ressel | An integrating, transformation-oriented approach to concurrency control and undo in group editors[END_REF][START_REF] Lushman | Proof of correctness of Ressel's adOPTed algorithm[END_REF], but we replace the explicit vector dependency by sending the set of (minimal dependencies) of the operation sent by the site. This amounts to giving an slightly modified version of the translate function that computes the integration of an operation with respect to a set of dependencies. Therefore the set of sites is not fixed in advance and can evolve during the editing process. As mentioned in [START_REF] Lushman | Proof of correctness of Ressel's adOPTed algorithm[END_REF], the correctness of this algorithm relies on the partial ordering structure underlying the set of requests.

The implementation has been done in Java and performs well in practice. Examining random execution of the algorithm shows that most of the computations are implicitly independent: operations on nodes of distinct identifiers don't interfere. The operations that may cause actual conflicts are renaming of labels (on the same identifier). In many other cases, the integration IT (op, op ′ ) returns op.

We plan to investigate further the algorithm and its properties to give theoretical bases for a set of optimizations that can improve its efficiency. For instance, we have proved that integrating an operation with pairwise disjoint operations always return the same operation, therefore some memoization techniques could be used to save computation time.

Conclusion

We have proposed a first approach to deal with XML-like trees in a P2P Collaborative Editing framework using a rich set of operations and a transformation enjoying the key properties to ensure convergence (when none of existing algorithms for words achieve this goal). We are currently investigating several issues. The first one is to deal with ordered unranked trees but, since this case contains the word case, the problem is hard and the existence of a simple integration transformation is still pending. Another issue is to deal with typing issues, where the relevant notion of type is regular tree languages for unordered-unranked tree languages (that generalizes DTD and XML-Schemas to this data-structure) like in [START_REF] Martin | A logic your typechecker can count on: Unordered tree types in practice[END_REF]. The first results in this direction shows that requiring to use transformations that respect types strongly restrict the class of well-typed trees. Finally, trees have a structure which is inherently concurrent (branches are independent up to their common root) and can be exploited to improve the computational aspects of our algorithm. -Base case n = 1. The result is obvious (the only substitution is the identity. -Inductive step. We assume that for all op, op 1 , .

]))) = IT (IT (op, op 1 ), IT (op 2 , op 1 ) = IT (IT (op, op 2 ), IT (op 1 , op 2 ) (by T P 2) = IT ( IT (IT * (op, [op 1 , . . . , op n-2 ]), IT * (op n-1 , [op 1 , . . . , op n-2 ])), IT (IT * (op n , [op 1 , . . . , op n-2 ]), IT * (op n-1 , [op 1 , . . . , op n-2 ])))) = IT * (op, [op 1 , . . . , op n-2 , op n-1 , op n ]) • σ(n) = n, n -1.
Then σ can be composed as three substitutions σ 1 , σ 2 , σ 3 : σ 1 exchanges n -1 and σ(n) and leave other element unchanged (hence

σ 1 (n) = n since σ(n) = n). σ 2 exchanges n-1 and n. σ 3 (n) = n and σ 3 is such that σ(i) = σ 3 (σ 2 (σ 1 (i))).
By the first case

IT * (op, [op 1 , . . . , op n ]) = IT * (op, [op σ 1 (1) , . . . , op σ 1 (n) ])
By the second case

IT * (op, [op σ 1 (1) , . . . , op σ 1 (n) ]) = IT * (op, [op σ 2 (σ 1 (1)) , . . . , op σ 2 (σ 1 (n)) ])
By the first case again

IT * (op, [op σ 2 (σ 2 (σ 1 (1)) , . . . , op σ 2 (σ 1 (n)) ]) = IT * (op, [op σ 3 (σ 2 (σ 2 (σ 1 (1))) , . . . , op σ 3 (σ 2 (σ 1 (n))) ]) Therefore IT * (op, [op 1 , . . . , op n ]) = IT * (op, [op σ(1) , . . . , op σ(n) ]) Proposition 3.
Proof.

Proof of Theorem 2

======= We prove that no IT exists for our first set of operations on trees. ¿¿¿¿¿¿¿ 1.3

Proof. We assume that T P 1 holds and we prove that IT (op

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  Add(Henri.P hone, 0491835469)(t) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Fig. 1 .

 1 Fig. 1. The Transformation IT

  op id , E D (id)) and r l = ⊥, (id, r D l ) if op = op id ∈ Op D -Computation following external requests φ e : Req, Env → Env where φ e (r e , E T , E D ) = ϕ T e (r T e , E T ) if r e = r T e , ⊥ and φ e (r e , E T , E D ) = ϕ D e (r D e , E D (id)) if E = E T , E D , r e = ⊥, (id, r D e ) The initial state is the empty tree, labeled by d 0 and the current state is the tree which is the current state s T computed by A T and for each id ∈ Dom(s T ) the labelling is the state computed by A D . Theorem 5. If A D and A T are convergent, then their composition is convergent.

Appendix 8 . 1

 81 Proof of Theorem 2 ¡¡¡¡¡¡¡ main.tex Proof. The proof is by induction on n.

  1 property states an equality on states [op 1 ; IT (op 2 , op 1 )](t) = [op 2 ; IT (op 1 , op 2 )](t)

		op1	t1	IT (op2, op1)	t ′ 1
	t	op2	t2	IT (op1, op2)	t ′ 2	T P 1 implies t ′ 1 = t ′ 2
		-T P 2 property states an identity of operations:
		IT (IT (op, op 1 ), IT (op 2 , op 1 )) = IT (IT (op, op 2 ), IT (op 1 , op 2 ))
	Theorem 1 ([10]). If IT satisfies TP1 and TP2 then the conver-
	gence property holds.

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

		P at		. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	Henri
			. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .		. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	P hone . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Cellular	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Home . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	Address 45 Emile Caplant Street
	0691543545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .		. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	0491543545

  . . , op n-1 , σ permutation of {1, . . . , n -1} we have IT * (op, [op 1 , . . . , op n-1 ]) = IT * (op, [op σ(1) , . . . , op σ(n-1) ]). Let op, op 1 , . . . , op n ∈ Op and let σ be a permutation of {1, . . . , n}. (op, [op 1 , . . . , op n-1 , op n ]) • σ exchanges n and n -1 and σ(i) = i for i = n, n -1. IT * (op, [op σ(1) , . . . , op σ(n) ]) = IT * (op, [op 1 , . . . , op n-2 , op n , op n-1 ]) = IT ( IT (op, [op 1 , . . . , op n-2 ]), IT * (op n , [op 1 , . . . , op n-2 ])), IT (IT * (op n-1 , [op 1 , . . . , op n-2 ]), IT

We distinguish several cases:

• σ(n) = n. Then σ is a permutation of {1, . . . , n -1}. IT * (op, [op σ(1) , . . . , op σ(n) ]) = IT * (op, [op σ(1) , . . . , op σ(n-1) , op n ]) = IT ( IT * (

op, [op σ(1) , . . . , op σ(n-1) ]), IT * (op n , [op σ(1) , . . . , op σ(n-1) ]) = IT ( IT * (op, [op σ1 , . . . , op n-1 ]), IT * (op n , [op 1 , . . . , op n-1 ])) (by induction hypothesis) = IT * * (op, [op 1 , . . . , op n-2 , op n ]), IT * (op n-1 , [op 1 , . . . , op n-2 , op n ])) = IT ( IT (IT * * (op n , [op 1 , . . . , op n-2

  1 , op 2 ) can't be defined on an operation of Op. Let t 1 = op 1 (t), t 2 = op 2 (t), t ′ 1 = op ′ 2 (t 1 ) with op ′ 2 = IT (op 2 , op 1 ), t ′ 2 = op ′ 1 (t 2 ) with op ′ 1 = IT (op 1 , op 2 ). We assume that IT (op 1 , op 2 ) is another operation of Op. The extension to a boolean combination of operation is straightforward. Nop() : Trivial because t 1 = t 2 • op ′ 1 = Add( , ) Then there is at least one more edge on t ′ 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Any possible operation leaves t 2 unchanged. We have r under m on t 1 and under n on t ′ 2 . • op ′ 1 = Add( , ) The number of edges on t ′ 1 and on t ′ 2 are different. • op ′ 1 = Del( , ) same case op ′ 2 = Del( , ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	-op ′ 2 = Nop() • op ′ 1 = Del(x, y) we get : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . n m (x = n, y = r) or (x = ǫ, y = n) or . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . r m In all case t ′ 1 = t ′ 2 -op ′ 2 = Add( , ) • op ′ 1 = Nop() . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 = • op ′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . n r (x = ǫ, y = m)

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . t ′ 1 = m r or or we return on Nop() case.

• op ′ 1 = Nop() : The number of nodes are different, therefore t ′ 1 = t ′

a user can be in conflict with the master copy, but conflict resolution is under user's responsibility

P at Henri

Add(Henri, P hone)(t ′ ) = t ′ since Henri.P hone already exists.

-Nop() : Do nothing. Nop()(t) = t -Del 1 (p, n): Replace a edge labeled n at end of path p by the set of its successors.

Del 1 (n ′ .p, n)(t) = t, if n ∈ Dom(t) Del 1 (n i .p, n)({n 1 (t 1 ), ..., n i (t i ), ..., n q (t q )}) = {n 1 (t 1 ), ..., n i (Del 1 (p, n)(t i )), ..., n q (t q )} Del 1 (ǫ, n)(t) = t, if n ∈ Dom(t) Del 1 (ǫ, n i )({n 1 (t 1 ), ..., n i (t i ), ..., n q (t q )}) = {n 1 (t 1 ), ..., n q (t q )} ⊕ t i Del 2 (n ′ .p, n)(t) = t, if n ∈ Dom(t) Del 2 (n i .p, n)({n 1 (t 1 ), ..., n i (t i ), ..., n q (t q )}) = {n 1 (t 1 ), ..., n i (Del 2 (p, n)(t i )), ..., n q (t q )} Del 2 (ǫ, n)(t) = t, if n ∈ Dom(t) Del 2 (ǫ, n i )({n 1 (t 1 ), ..., n i (t i ), ..., n q (t q )}) = {n 1 (t 1 ), ..., n q (t q )} Let Op be the set of operations {Nop(), Add(p, n), Del 2 (p, n)} p ∈ P, n ∈ Σ and let IT be defined by:

The IT function is defined by:

Proof of TP1 and TP2 with Strong Deletion Theorem 7. IT satisfies T P 1 and T P 2.

We perform a case analysis on op 1 and op 2 :

We prove :

We perform an induction on path length. (a) Empty path :

-If n, n ′ ∈ Dom(t) and n = n ′ Add(ǫ, n ′ )(Add(ǫ, n)({n 1 (T 1 ), ..., n q (T q )})) = {n 1 (T 1 ), ..., n q (T q ), n({}), n ′ ({})} Add(ǫ, n ′ )(Add(ǫ, n)({n 1 (T 1 ), ..., n q (T q )})) = {n 1 (T 1 ), ..., n q (T q ), n ′ ({}), n({})} which are equal.

We obtain : = {n 1 (T 1 ), ..., n q (T q ), n({})} Because we use the third choice of function Add(ǫ, n)(t) and first operation add n({}).

We have {n 1 (T 1 ), ..., n q (T q ), n ′ ({})} Third we use the second case of definition

By definition :

), ..., n q (T q , n(Add(p ′′ , n ′ )({})} therefor n ∈ dom(t |p ) and Add(p, n) do nothing. so (2) = {n 1 (T 1 ), ..., m 1 (T ′ 1 ), ...n q (T q ), n(Add(p

We have t |p = {n 1 (T 1 ), ..., m 1 (T ′ 1 ), ..., n q-1 (T q-1 )} Two cases occurs, by recurrence definition :

We have two non-empty paths then :

We have

We have by definition :

by Del(n, p) in (1) . and Del(n, p) do nothing in (2) Therefore

We take : t | p ′ = {n 1 (T 1 ), ..., n ′ (T ), ..., n q-1 (T q-1 )} We have :

(1)

|p = {n 1 (T 1 ), ..., n q-2 (T q-2 )} -else : same demo of 1f.

idem for op

We have p'=p.n.p"; We take t |p = {n 1 (T 1 ), ..., n(T ), ..., n q-1 (T q-1 )}

|p = {n 1 (T 1 ), ..., n q-1 (T q-1 )} first time : Del(p, n)(t) |p {n 1 (T 1 ), ..., n(Del(p ′′ , n ′ )(T )), ..., n q-1 (T q-1 )} therefore (2) |p = {n 1 (T 1 ), ..., n q-1 (T q-1 )} -idem for p ′ .n ′ ⊳ p ′ -else: same 1f we have two independant subtree. 5. case Nop() is trivial.

Proving TP2 IT (IT (Op, Op 1 ), IT (Op 2 , Op 1 )) (1) = IT (IT (Op, Op 2 ), IT (Op 1 , Op 2 )) (2) We will explore every case :

Because (a) give a Add() or a Nop() the second argument of (b) is a Add or a Nop.

IT (IT (Add(p, n), Del(p 2 , n 2 )), IT (Del(p 1 , n 1 ), Del(p 2 , n 2 ))) (2) • If p 1 = p 2 and n 1 = n 2 (1) = IT (IT (Add(p, n), Del(p 1 , n 1 )), Nop()) (2) = IT (IT (Add(p, n), Del(p 1 , n 1 )), Nop())

By hypothese :

We have

) because the first argument will be a 'Del' and the second will be a 'Add'. (2)

Proof of Theorem 4

The proof is similar to the previous proof and has been checked by Vote using the following specification: %VOTE file for proving TP1/TP2 on XML like trees type node(mem,data),lbl(novalue),nat; observator %test node existence bool exist(node); %relation between son and father bool childof(node, node); %returns the label of a node lbl getLbl(node); auxiliary %returns tree if there is a path between nodes bool childofp(node, node); operation %add a node n, if it doesn't exists, %it becomes a son of p that must exist not(exist(n)) and exist(p) and (n!=mem) and (n!=data) : Add(node p,node n) %delete an existing node that must be different %from the two initial nodes mem and data exist(n) and (n!=mem) and (n!=data) : Del(node n); %site t moves node n under node p if n exists and is different %from mem and data exist(n) and exist(p) and (n!=mem) and (n!=data) and (n != p): Move(node n, %site t renames a node n with label l if n exists and is %different from mem and data exist(n) and (n!=mem) and (n!=data): Ren(node n,lbl l,nat t); transform %definition of the IT transformation T(Add(p1,n1),Del(n2)) = if (p1==n2) then return Add(mem,n1) else return Add(p1, n1) endif; T(Ren(n1,l1,s1), Del(n2)) = if (n1==n2) then return nop else return Ren(n1,l1,s1) endif; T(Ren(n1,l1,s1),Ren(n2,l2,s2))= if (n1==n2 and s1 > s2) then return nop else return Ren(n1,l1,s1) endif;

T(Move(n1,p1,s1),Move(n2,p2,s2)) = if (n1==n2 and s1 > s2) then return nop else return Move(n1,p1,s1) endif; T(Move(n1,p1,s1 We give the proof of the combination theorem.

Proof. Given a sequence of computations Comp i.e. a sequence of expressions φ l (E).!r l or r e .φ e (E) respecting causality, we extract Comp T and Comp id the respective computations of A T and A D for each id: Π T (φ l ( E T , E D ).!r l ) = ϕ T l (E T ).!r T l if r l = r T l , ⊥ Π id (φ l ( E T , E D ).!r l ) = ϕ D l (E D (id)).!r D l if r l = ⊥, (id, r D l ) Π T (?r e .φ e ( E T , E D ) =?r T e .ϕ T l (E T ) if r e = r T e , ⊥ Π id (?r e .φ e ( E T , E D ) =?r D e .ϕ D e (E D (id)) if r e = ⊥, (id, r D e ) and for all other cases Π T (. . .) = Π id (. . .) = 0 where 0 is the null process that does nothing. By construction Comp T respects the causality relations restricted to the operations of Op T . The same holds for Comp id . the causality relation (but the reverse doesn't necessarily holds). Therefore Comp T is a legal computation of A D and by the convergence of A D each site has he same state s T . For each id ∈ Dom(s T ), the sequence Comp id is legal computation of A id , therefore each site has the same state s id .


Hardness of new boron-rich chalcogenides

Keywords: boron-rich chalcogenides, hardness, bulk modulus

Hardness of bulk polycrystalline boron-rich chalcogenides, rhombohedral B 12 S and B 12 Se, has been predicted using contemporary theoretical models and experimentally studied by microindentation. Both chalcogenides exhibit Vickers hardness of about 33 GPa exceeding that of boron carbide and hence belong to a family of (super)hard phases.

Two new boron-rich chalcogenides, rhombohedral B 12 S and B 12 Se, have been recently synthesized by direct reactions of the elements at high pressures and high temperatures, and their crystal structures have been refined by synchrotron X-ray diffraction study combined with ab initio calculations [START_REF] Cherednichenko | High-pressure synthesis of boron-rich chalcogenides B 12 S and B 12 Se[END_REF]. In the present Letter we report the hardness of these compounds from theoretical and experimental studies.

Vickers hardness (H V ) of boron-rich chalcogenides were predicted using two contemporary theoretical models of hardness i.e. thermodynamic model developed for the particular case of boron-rich solids [START_REF] Mukhanov | Thermodynamic model of hardness: Particular case of boron-rich solids[END_REF] and Lyakhov-Oganov model [START_REF] Lyakhov | Evolutionary search for superhard materials: Methodology and applications to forms of carbon and TiO 2[END_REF]. The thermodynamic model is based on the crystal structure and thermodynamic properties, while Lyakhov-Oganov approach considers the strength of covalent bonding, degree of ionicity and directionality, as well as topology of the crystal structure. The results are summarized in Table 1. Note that bulk modulus of B 12 Se estimated from thermodynamic model is in reasonable agreement with the experimental value [START_REF] Cherednichenko | Equations of state of new boron-rich selenides B 6 Se and B 12 Se[END_REF].

Stoichiometric boron-rich chalcogenides B 12 X (X = S, Se) have been synthesized according to the method described elsewhere [START_REF] Cherednichenko | High-pressure synthesis of boron-rich chalcogenides B 12 S and B 12 Se[END_REF]. Polycrystalline bulks for hardness measurements have been produced in a toroid-type apparatus by crystallization from a melt at 2.6 GPa. According to X-ray diffraction study (TEXT 3000 Inel, CuKα1 radiation) the recovered bulks contain well-crystallized single-phase boron-rich chalcogenides with lattice parameters identical to the literature data [START_REF] Cherednichenko | High-pressure synthesis of boron-rich chalcogenides B 12 S and B 12 Se[END_REF].

The recovered samples (cylinders 4-mm diameter and 3-mm height) were hot mounted in carbonfiber reinforced resin, and were planar ground with diamond 500 grit and subsequently polished with 9-μm and 1-μm diamond suspensions. Mechanical polishing was followed by vibropolishing with 0.04-μm SiO 2 colloidal solution that ensured the minimal sample surface damage.

Microstructure of the polished samples was studied using TESCAN MIRA3 Field Emission scanning electron microscope (SEM) in secondary electron and backscatter modes. It was found that all samples are homogeneous and their average grain size varies from 0.2 to 2 µm; the residual porosity was not observed.

Microhardness measurements have been performed using a Mitutoyo HM-220B Microhardness

Testing Machine under loads from 1 to 20 N and 15 seconds dwell time; five indentations have been made at each load. The values of Vickers and Knoop (H K ) hardness were determined from the residual imprints upon indentation and were calculated following the standard definitions (for details see [START_REF] Solozhenko | Mechanical properties of boron phosphides[END_REF]).

The measured Vickers hardness of boron-rich sulfide B 12 S decreases with the load and at 10 N reaches the asymptotic value H V = 32(3) GPa (Fig. 1a) that is in perfect agreement with the value predicted in the framework of thermodynamic model of hardness (see Table 1). The load dependence of the measured Knoop hardness is presented in Fig. 1b; the asymptotic value of H K = 26(2) GPa is achieved already at 5 N load.

The measured Vickers hardness of boron-rich selenide B 12 Se as a function of load is presented in Fig. 2a; the asymptotic value of 33(2) GPa is attained at 8 N. This H V value is also in good agreement with B 12 Se hardness calculated in the framework of thermodynamic model (see Table 1).

Load dependence of Knoop hardness (Fig. 2b) is characterized by the asymptotic value

H K = 22(2)
GPa that is somewhat low and demonstrates abnormal lag to the Vickers hardness value. This can be attributed to a low fracture toughness and related cleavage of the material under Knoop indenter (see Inset in Fig. 2b).

Thus, boron-rich chalcogenides B 12 S and B 12 Se exhibit experimental Vickers hardness of about 33 GPa that is higher than that of boron carbide B 4 C, a conventional superabrasive. Both theoretical models used work properly, however, the thermodynamic model appears to be more reliable since the hardness values calculated using Lyakhov-Oganov model are slightly underestimated.

The author thanks Dr. V.A. Mukhanov for the fabrication of bulk samples, and Dr. V. Bushlya for sample polishing and SEM study. This work was financially supported by the European Union's Horizon 2020 Research and Innovation Programme under the Flintstone2020 project (grant agreement No 689279).

Fig. 1 Fig. 2

 12 Fig. 1 Vickers (a) and Knoop (b) microhardness of bulk boron-rich sulfide B 12 S vs load. Insets: SEM images of the imprints formed by Vickers and Knoop indenters under 8 N loads.

Table 1 X

 1 -ray densities (ρ), bulk moduli (B 0 ) and Vickers hardness (H V ) of boron-rich chalcogenides

		Lattice parameters (Å) [1] ρ (g/cm 3 )	T *	B 0 (GPa) exp.	T *	H V (GPa) LO †	exp.
	B 12 S	a = 5.8196 c = 11.9653	2.34	154	--	31	27	32(3)
	B 12 Se	a = 5.9385 c = 11.9144	2.90	147	155(2) [4]	30	29	33(2)

* Thermodynamic model

[2]

† Lyakhov-Oganov model

[START_REF] Lyakhov | Evolutionary search for superhard materials: Methodology and applications to forms of carbon and TiO 2[END_REF]