-

2.1 Notations and basi denitions 22 Mamoun Filali 2 Sometimes assumptions are also alled pre onditions.

As an example, the following statement whi h onsists in (assumes), assumptions2 a on lusion (shows) and a proof s ript (proof) establishes that the union of proof has the format: so alled de larativ e style [18℄ whi h is loser to the usual mathemati al reatwo hierar hies (see se tion 2.2) is also a hierar hy. A basi statement of the soning than the pro edural format. Let us mention that, basi ally, Isar supports natural dedu tion but also supports al ulational reasoning [7℄. 24 Mamoun Filali }" In the following, we give the formal denitions that will be used. ∗} " Tree {h H i e r a r h y . Maximal ( h ) = {ROOT( h ) }}" , ∈ that will allow us to say that the re onstru tion an pro eed starting from the With respe t to phylogeneti trees, we just mention the following equality leaves, while the statement of the re onstru tion theorem is over the root. A tually, for a phylogeneti tree we have: Moreover, we t, ROOT(t) = S Leaves(t). will rely on the following result about the union of phylogeneti trees: t1 {a,e,b} t2 {x,y} {x,y,a,e,b,u,v,w} {a,e,b} {u,v,w} {a} {e} {b} t0 {x} {x} {y} {a} {e} {b} {u} {v} {w} logeneti tree: where domSigma spe ies the set of trees whi h an be joined to form a phyt2 = {{x, y, a, e, b, u, v, w}, {x, y}, {x}, {y}

, {a, e, b}, {a}, {e}, {b}, {u, v, w}, {u}, {v}, {w}} Leaves(t2) = {{x}, {y}, {a}, {e}, {b}, {u}, {v}, {w}} ROOT(t2) = {x, y, a, e, b, u, v, w}

R1(t2) = {{x, y}, {a, e, b}, {u, v, w}} assumes pre : " PreGraft ( h , gp , g ) " proof . . . qed shows " Mutation ( gp ,ROOT( g ) ) P_tr ( h ) " ∈ ( r e o n s t r u t (GP) (ROOT( t ) ) = t ) " ⇒ main drawba k is to break the underlying natural onuen e. For instan e, with dened through the list of its subtrees, or through a map of its subtrees from a GP. t Phylo . G e n e r a t i v e P a r t i t i o n ( t ,GP) "∀ ∀ ∈ fun tion is a urryed version of Re onstru t. " r e o n s t r u t (GP) s . R e o n s t r u t (GP, s ) " , λ The theorem hara terizing the re onstru tion is stated as follows: neti trees (2.2). su h representations, inserting a subtree after a tually removing it, does not yield frameworks [9, 1, 4, 13℄. In fa t, in su h frameworks a tree is usually re ursively Sigma ( image ( e . R e o n s t r u t (GP, e ) ) (GP s ) ) λ 2.6 Dis ussion set based onstru tion is not admitted by most of the type theory based logi al theorem g e n e r a t i v e _ p a r t i t i o n _ r e o n s t r u t i o n : in order to not distinguish between trees of whi h subtrees are identi al but not A Me hanization of Phylogeneti Trees 29 the original tree. Su h a onuen e is fundamental for establishing naturally our This theorem is established thanks to the indu tion theorem over phylogee l s e { s } ) " ( i f ( f i n i t e s ) ( s ’ GP( s ) . s ’ s ) then ∧ ∀ ∈ ⊂ given index type. We have tried to work with ea h of these representations. Their " R e o n s t r u t (GP, s ) = be dened as either a singleton node or as the Sigma of its subtrees. Su h a In this se tion, we dis uss the denition of phylogeneti trees that has been at ea h all. The ondition of the if expression ensures it. The re onstru t shows re onstru tion result. Otherwise, we would have to introdu e modulo relations study, we onsider a restri ted version: grafting o urs at singleton nodes only. suggests, the graft operation onsists in grafting a tree at a given node. In this proof . . . qed in the same order. elaborated. With respe t to the stru tural point of view: a phylogeneti tree an re def R e o n s t r u t "measure ( (GP, s ) . a r d s ) " λ ( hints simp add : psubset_ ard_mono ) In our setting, the graft operation models the growth of a tree. As its name 3 The graft operation

Graft {x,y,a,n1,n2,b,u,v,w} {x,y} {a,n1,n2,b} {u,v,w} {x} {y} {a} {n1,n2}{b} {u} {v} {w} assumes gp_tr : assumes g : " g Phylo " ∈ e l s e image ( Mutation ( gp ,ROOT( g ) ) ) (GP( n ) ) ) " assumes p r e : " P r e G r a f t ( h , gp , g ) " proof . . . qed assumes gp_h : " G e n e r a t i v e P a r t i t i o n ( h ,GP) " n h . GP( Mutation ( gp ,ROOT( g ) ) ( n ) ) = "∀ ∈ ( i f n Leaves ( h ) then { Mutation ( gp ,ROOT( g ) ) ( n ) } ∈ assumes h : "h Phylo " ∈ theorem g e n e r a t i v e _ p a r t i t i o n _ g r a f t _ p h y l o : assumes gp_g : " G e n e r a t i v e P a r t i t i o n ( g ,GP) " shows " G e n e r a t i v e P a r t i t i o n ( G r a f t ( h , gp , g ) ,GP) " of spa e, we do not detail them.

Mutation; then it is a phylogeneti transformation. of a so alled anoni al tree whi h onsists of a root and a set of leaves: Sin e we have: upd inherits the property of upd(l, N ) = Mutation({l}, N ), Moreover, in order to simplify the proof obligations for establishing that onditions that should be established by the update fun tion. Due to the la k "upd ( l ,N) . S . i f l S then S { l } N e l s e S" , λ λ ∈ − ∪ a generative relation is preserved after a graft, we have elaborated su ien t We have established the preservation of the generative relation for the graft assumes g r _ t r : assumes N: n t . N n = " "∀ ∈ ∩ ∅ proof . . . qed lemma g e n e r a t i v e _ r e l a t i o n _ g r a f t _ p h y l o : assumes gp2 : " G e n e r a t i v e R e l a t i o n ( Canoni (N) ,GR) " shows " G e n e r a t i v e R e l a t i o n ( G r a f t ( { l } , Canoni (N) ) ( t ) ,GR) " assumes N_e : "N f i n i t e (N) " =6 ∅ ∧ assumes t : " t Phylo " ∈ assumes gp1 : " G e n e r a t i v e R e l a t i o n ( t ,GR) " assumes up : "{ l } t " ∈ assumes gr_m : n . GR( n ) n n sym (GR( n ) ) " "∀ ⊆ × ∧ assumes t e r m i n a l : " T e r m i n a l ( t ) " n t . l n r_upd ( l , N) ( n ) (GR( n ) ,GR( upd ( l , N) ( n ) ) ) " "∀ ∈ ∈ ⇒

(1,[1,0,0,0]) (1,[1,1,2,0]) (2,[1,0,0,0]) (2,[1,1,0,0]) (0,[0,0,0,0]) S0

(0,[1,1,0,0]) (0,[1,1,2,2])(0,[1,1,2,0]) S1

S2

S3 (site,[x,y,z,t]) internal node tag (3,[1,1,2,0]) (site,[x,y,z,t]) collected visit tag message. In su h a ase, this step generates a leaf with respe t to the ontrol le tor when a pro ess performs a omputation step without multi- asting a new self provides a simple riterion for termination dete tion [8℄: a omputation is tagged messages are in fa t leaves of the phylogeneti tree superposed to the the elements in the maximum of the olle ted visit ve tors5: The re onstru tion of the ontrol tree an only start when the global omproblem, espe ially, thanks to a olle tor pro ess[12℄. However, the en oding itterminated when the number of olle ted leaves is equal to one plus the sum of diusing omputation ( and re orded in the auxiliary variable auxTree). putation is terminated. Several distributed algorithms an solve the termination o w of the omputation. Then, with respe t to phylogeneti trees, the olle ted We introdu e a olle tor pro ess to gather ve tors: a ve tor is sent to the ol6 The negative o urren e is due to the fa t that the parameter of Sigma, onsidered as a onstru tor, 7 It is interesting to remark that the analysis of the algorithm of [5℄ is reported to be in orre t is a set of trees. in [15℄. biology of existing tools from algebra is just beginning. To the best of our knowledge, the me hanization of these works has not been onsidered yet. We think ous works have been published. Among the more re ent, we an ite [16℄ who With respe t to the formalization of trees and biology related results, numerorre tness but also for the orre tness of their proposed proofs7. that our work ould be reused as a starting point for establishing algorithms onsider the problem of tree in lusion in a ategori al setting. [11℄ reviews basi network models for reasoning about biology; he noti es that appli ations to 36 Mamoun Filali Referen es

References