Formal Verification of Programs in Molecular Models with Random Access Memory

Fo mal Ve i ica ion o P og ams in Molecula Models wi h Random Access Memo y MARIO J. PÉREZ-JIMÉNEZ FERNANDO SANCHO-CAPARRINI Dp o. Ciencias de la Compu ación e In eligencia A i icial Uni e sidad de Se illa, E.T.S. Ingenie ía In o má ica A da. Reina Me cedes, s/n – 41012 Se illa, Spain E-mail: {Ma io.Pe ez,Fe nando.Sancho}@cs.us.es Abs ac Fo mal e i ica ion o molecula p og ams is a i s s ep o- wa ds hei au oma ic p ocessing by means o easoning sys- ems (ACL2, PVS, e c). In his pape a sys ema ic me hod o es ablish e i ica ions o hese p og ams wi hin molecula mod- els wi h memo y, ha is, molecula compu ing models whe e some ope a ions modi ying he inne s uc u e o molecules ex- is , is p oposed. The me hod p esen ed in his wo k is applied o ele an p oblems o he design o molecula p og ams sol ing some well-known nume ical NP-comple e p oblems: he Gene - a ing Co e Families p oblem, he Se Co e ing p oblem and he Minimal Se Co e Selec ion P oblem. M. J. Pé ez-Jiménez e al. (Eds.): Recen Resul s in Na u al Compu ing, pp. 205–229 c The Au ho s c Fénix Edi o a 206 Fo mal Ve i ica ion o P og ams in Molecula Models... 1 In oduc ion Since he i s esul in molecula compu ing a he end o 1994 [1], some solu ions o se e al NP-comple e p oblems in his amewo k ha e been o e ed. In 1995 he i s molecula models appea ed. They a e uni e sal models, ha is, wi h he same compu a ional powe as Tu ing Machines. Since hen, i appea s he possibili y o designing molecula p og ams ha ing as inpu he ins ance o he p oblem o sol e (un il hen, molecula compu ing was limi ed o sol e pa icu- la ins ances, wi h no desc ip ion o molecula ope a ions in gene al cases). Howe e , his b ings abou he necessi y o a g ea e lexibili y in he design o he p og ams and he necessi y o a o mal e i ica ion o he ac ha hose p og ams e ec i ely sol e he p oblem o which hey we e designed. Usually, he i s s ep o sol e a conc e e p oblem in compu ing models is o encode he inpu o he p oblem in o he ype o da a ha he model deals wi h (in his case, encoding will be made by means o ubes con aining DNA molecules); nex s ep consis s in applying a i- ni e sequence o basic ope a ions o he model o he inpu da a o ge an ou pu encoding he solu ion o he p oblem. The goal o his pape is he p esen a ion o a me hodology o es ab- lish a o mal e i ica ion o p og ams in molecula models wi h mem- o y. The me hod is applied o molecula p og ams sol ing se e al well- known nume ical NP-comple e p oblems: he Gene a ing Co e Families p oblem, he Se Co e ing p oblem, and he Minimal Se Co e p oblem. The p oblems we sol e in his wo k a e associa ed wi h a ini e am- ily, F, o subse s o a ini e se . And hey a e he ollowing ones: (1) gene a e e e y o de ed pai (F0, B)such ha F0is a sub amily o F and B=∪F0; (2) gene a e all pai wise disjoin sub amilies o F. The pape is o ganized as ollows: in sec ion 2 a me hodology o es ablish a o mal e i ica ion o p og ams in molecula models wi h memo y is gi en. Sec ion 3 summa izes he main cha ac e is ics o he molecula model we use in his wo k: he S icke Model. Sec ions 4 and 5 apply his me hodology o wo nume ical p oblems. The main eason why we ha e chosen he abo e p oblems is because he e exis s a quali a i e di e ence in he way hei o mal e i ica ion ha e been es ablished. On one hand, all he molecules o he inpu ube a e kep M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 207 (possibly modi ied) along he execu ion o he p og am; on he o he hand, a il e ing p ocess is made, hence some molecules a e h own away because hey do no encode any o he alid solu ions o he p ob- lem. 2 A Me hodology o Ve i ica ion o P og ams wi hin Models wi h Memo y Le Pbe a p og am wi hin a molecula model designed o sol e a p ob- lem X. Le us suppose ha he p og am Phas a main loop FOR o WHILE (we will say ha Pis a FOR o WHILE p og am). To e i y (X, P)we will sea ch o mulas, in he a iables o he p og am, ha a e in a ian o he main loop and such ha , a he end o he execu- ion, can help us o deduce he soundness and comple eness o P o he p oblem X. The execu ion o he p og am Pcan be in e p e ed as he e olu ion o e ime o a ce ain popula ion. A he beginning o he execu ion he popula ion consis s o a mul ise o molecules o ming he inpu ube o P. E e y molecule ep esen s an elemen , hus, in he o iginal popu- la ion cloned membe s can exis . E e y s ep o he main loop akes one uni o ime. Hence, h oughou he execu ion an elemen o he pop- ula ion can die ( ha is, i can be h own away) o i can su i e. I he molecula compu ing model has andom access memo y ( ha is, i he inne s uc u e o he molecules can be modi ied) hen he molecules su i ing all he s eps can be o wo kinds: hose whose inne s uc u e has been al e ed and hose ha emain wi h no modi ica ions. The s udy o in a ian o mulas o he main loop needs a de ailed s udy o e e y molecule in he inpu ube. Fi s we p oceed o a e- labelling o he ubes used in he p og am in o de o indi idualize hem and o dis inguish and cha ac e ize he ele an ubes along he execu ion. Second, a unc ion showing he e olu ion o e e y molecule, σ, in e e y s ep, i, o he main loop is de ined. This unc ion can be unde ined o some alues (σ, i). This will be in e p e ed as he ac ha he molecule σdoes no su i e a e he execu ion o i- h s ep o he loop. The me hodology we p opose o e i y (X, P)consis s o he ol- lowing s ages: 208 Fo mal Ve i ica ion o P og ams in Molecula Models... 1. Re-labelling o he ubes o he p og am P, o indi idualize hem along he execu ion. 2. A de ailed ollow-up o he e olu ion o e e y molecule along he p ocess, using a unc ion ha we will name STEP . 3. Sea ching in a ian o mulas o he main loop based on he STEP unc ion p ope ies. 4. Deducing he Soundness (e e y molecule in he ou pu ube en- codes a alid solu ion o he p oblem) and he Comple eness (e e y molecule in he inpu ube encoding a alid solu ion o he p ob- lem mus be in he ou pu ube) o he p og am based on in a ian o mulas a e he execu ion o he p og am. 3 The S icke Model The s icke model was in oduced by S. Roweis, E. Win ee e al [6] as an abs ac model o molecula compu ing based on DNA, wi h an- dom access memo y. In his model he in o ma ion is ep esen ed in a di e en way om ha used in he Adleman-Lip on pa adigm. An (n, k, m)-memo y s and, wi h n≥k·m, consis s o a s and o nbases subdi ided in o knon-o e lapping subs ands each o which is mbases long. A s icke associa ed wi h an (n, k, m)-memo y s and is mbases long and complemen a y o exac ly one o he ksubs ands o he mem- o y s and. I a s icke is annealed o i s ma ching subs and on a mem- o y s and, hen he pa icula subs and is said o be on, i no i is said o be o . An (n, k, m)-memo y complex is an (n, k, m)-memo y s and along wi h i s annealed s icke s (i any). The (n, k, m)-memo y complexes ep esen bi s ings o {0,1}k, o his eason, i is usual o iden i y hem ei he as bina y unc ions (σ:{1, ..., k} −→ {0,1}, such ha σ(i) = 1 i and only i he i- h subs and is on), o as subse s o {1, ..., k}by means o hei cha ac e is ic unc ions. Wi hin he s icke model, a ube is a ini e mul ise (a collec ion whe e elemen s can be epea ed) o memo y complexes. In his pape we use he ollowing ope a ions o he s icke model o e ubes: M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 209 •Combine(T1, T2): gi en wo es ubes T1and T2 his ope a ion p oduces a new ube, deno ed by T1∪T2, he mul ise union o T1 and T2. •Sepa a e(T, i): gi en a es ube Tand a na u al numbe i, wi h 1≤i≤k, his ope a ion p oduces wo new ubes, +(T, i) = {{σ∈T:σ(i) = 1}} and −(T, i) = {{σ∈T:σ(i) = 0}}. We usually w i e (T1, T2)←sepa a e(T, i) o indica e ha T1= +(T, i)and T2=−(T, i). •Se (T, i): gi en a es ube Tand a na u al numbe i, wi h 1≤ i≤k, his ope a ion p oduces a new ube, Se (T, i), whe e he i h subs and o each memo y complex in Tis u ned on. •Read(T): gi en a es ube T his ope a ion eads he con en o ube T. To achie e ha , one memo y complex has o be isola ed om Tand i s annealed s icke s de e mined, o else i has o be epo ed ha he ube Tcon ains no memo y complexes. No e ha , in his model, he ope a ions Sepa a e and Se a e he only ones implemen ing a massi e pa allelism. Also, only ope a ion Se can modi y inne s uc u e o he molecules o a ube. A(k, l)-lib a y, wi h 1≤l≤k, consis s o all memo y complexes wi h ksubs ands, whe e he i s lsubs ands a e ei he on o o , in all possible ways, whe eas he las k−lsubs ands a e o . In he s icke model a p og am, P, is a ini e sequence o molecula ope a ions ha can be w i en in a simple way by means o obo ic ope a ions (such as loops, condi ionals, e c.). 4 The Gene a ing Co e Families P oblem The Gene a ing Co e Families p oblem is he ollowing: Le A={1, . . . , p}. Le F={B1, . . . , Bq}be a ini e amily o subse s o A. De e mine all o de ed pai s (F0, B), whe e F0is a sub amily o Fand B=SF0. 210 Fo mal Ve i ica ion o P og ams in Molecula Models... 4.1 Design o a P og am in he S icke Model To sol e his p oblem we conside as he inpu ube, T0, a (p+q, q)- lib a y encoding all possible sub amilies o F. I ρis a memo y complex wi h p+qsubs ands ( om now on, we will say ha ρis a molecule), we will no e: ρq= (ρ(1), . . . , ρ(q)) ρp= (ρ(q+ 1), . . . , ρ(q+p)) We can in e p e ha molecule ρencodes an o de ed pai , (Fρ, Aρ), whe e Fρis a sub amily o Fand Aρis a subse o A, acco ding o he ollowing: Fρ={Bk∈ F : 1 ≤k≤q∧ρ(k) = 1} Aρ={s∈A: 1 ≤s≤p∧ρ(q+s) = 1} De ini ion 1. Le ρbe a molecule and le be such ha 1≤ ≤q+p. We will say ha ∈ρ( esp. /∈ρ) i and only i ρ( ) = 1 ( esp. ρ( ) = 0). I ρis a molecule, hen we ha e: [Fρ={xj k: 1 ≤k≤q∧1≤j≤ k∧k∈ρ} De ini ion 2. A molecule ρis consis en i and only i Aρ=SFρ. A molecula p og am sol ing he Gene a ing Co e Families p oblem is he ollowing: P ocedu e Co e Inpu : T0(whe e T0is a (p+q, q)-lib a y) o i= 1 o qdo (T+ i, T− i)←sepa a e(T0, i) o j= 1 o ido se (T+ i, q +xj i) end o T0←combine(T+ i, T− i) end o Whe e, o each i(1 ≤i≤q)we deno e by i he ca dinali y o he se Bi, and Bi={x1 i, . . . , x i i}. The numbe o molecula ope a ions in his p og am is o he o de o O(q·p). M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 211 4.2 Fo mal Ve i ica ion In o de o es ablish a o mal e i ica ion o his molecula p og am we p oceed o a e-labelling o he used ubes: P ocedu e Co e Inpu : T0(whe e T0isa(p+q, q)-lib a y) o i= 1 o qdo (T+ i, T− i)←sepa a e(Ti−1, i) T∗ i,0←T+ i o j= 1 o ido T∗ i,j ←se (T∗ i,j−1, q +xj i) end o Ti←combine(T∗ i, i, T− i) end o Ob iously, his p og am is equi alen o he abo e one in he ollowing sense: bo h ha e he same inpu ubes, T0, and p oduce ou pu ubes (T0and Tq, espec i ely) wi h he same con en . We wan o no e ha he seman ic o his p og am is e y close o he seman ic o he p oblem i sol es. Hence, he p oblems ha ap- pea when ying o es ablish i s o mal e i ica ion a e mainly due o he use o molecula ope a ions ha modi y he inne s uc u e o he molecules (i.e. se ope a ion), making i ha de he analysis o hei ack along he execu ion. Nex , we de ine a unc ion, namely STEP, ha cap u es he e olu- ion o each molecule a e he execu ion o a s ep o he main loop. De ini ion 3. Le ibe such ha 1≤i≤q. Le ρ∈Ti−1. We de ine STEP(ρ, i)as ollows: STEP(ρ, i) = ρ , i i /∈ρ ρ∪(q+Bi),i i∈ρ Whe e q+Bi={q+xj i: 1 ≤j≤ i}. No e ha i τ=STEP (ρ, i) hen ρq=τqand ρ⊆τ. Mo eo e , he unc ion STEP is a o al unc ion; ha is, i is de ined o e all possible inpu da a. 212 Fo mal Ve i ica ion o P og ams in Molecula Models... Lemma 1. ∀i(1 ≤i≤q→ ∀ ρ∈Ti−1(ST EP(ρ, i)∈Ti)) P oo . Le ibe such ha 1≤i≤q, and le ρ∈Ti−1. •I i /∈ρ, hen ρ∈ −(Ti−1, i) = T− i⊆Ti, and since STEP(ρ, i) = ρ, we deduce ha STEP(ρ, i)∈Ti. •I i∈ρ, we de ine ecu si ely ρ(j), o each 0≤j≤ ias ollows: –ρ(0) =ρ. –ρ(j+1) =ρ(j)∪ {q+xj+1 i}. Le us see ha ∀j(0 ≤j≤ i→ρ(j)∈T∗ i,j). By induc ion on j. –The case j= 0 is i ial because ρ(0) =ρ∈+(Ti−1, i) = T+ i=T∗ i,0. –Le j < isuch ha ρ(j)∈T∗ i,j. F om de ini ion o ρ(j+1) we deduce ha ρ(j+1) ∈se (T∗ i,j, q +xj+1 i) = T∗ i,j+1. Since ρ( i)=STEP(ρ, i), we ob ain ha STEP(ρ, i)∈T∗ i, i⊆Ti. De ini ion 4. Le σ∈T0. We de ine ecu si ely σi, wi h 0≤i≤q, as ollows: σi=σ , i i= 0 STEP(σi−1, i),i 1≤i≤q F om Lemma 1 i ollows ha σi∈Ti, o each 0≤i≤q. Lemma 2. Fo each i,jsuch ha 1≤i≤qand 1≤j≤ iwe ha e ∀τ∈T∗ i,j ∃ρ∈T+ i(τ=ρ∪(q+Bj i)), whe e Bj i={x1 i, . . . , xj i}. P oo . Fo a gi en i, he p oo can be deduced by induc ion on j ollow- ing he seman ic s uc u e o he p og am. Co olla y 1. Le ibe such ha 1≤i≤q. Then o e e y molecule τ∈T∗ i, i he e exis s a molecule ρ∈Ti−1 e i ying i∈ρand STEP (ρ, i) = τ. P oo . Le ibe such ha 1≤i≤q. Le τ∈T∗ i, i. F om Lemma 2 (wi h j= i) we deduce ha he e exis s ρ∈T+ i= +(Ti−1, i)such ha τ=ρ∪(q+Bj i). Then, ρ∈Ti−1and i∈ρ. Hence, STEP(ρ, i) = τ. M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 213 4.3 Soundness o he P og am We ha e o p o e ha e e y molecule in he ou pu ube, Tq, encodes a alid solu ion o he p oblem. Tha is, i τ∈Tq, hen τqencodes a sub amily, Fτ, o Fand τpencodes a subse , Aτ, o A, such ha Aτ= SFτ. In o he wo ds, we ha e o p o e ha e e y molecule, τ, in he ou pu ube, Tq, is consis en . To p o e he soundness o he p og am we conside he ollowing o mula θ(i) ∀τ∈Ti[∀k(1 ≤k≤i∧k∈τ→(q+Bk)⊆τ)∧ ∧ ∀ s(1 ≤s≤p∧(q+s)∈τ→ ∃ k∈τ(1 ≤k≤i∧s∈Bk))] Tha is, he o mula θ(i)(wi h i > 0) means ha a e he execu ion o he i- h s ep o main loop, all molecules, τ, e i ying Aτ=S{B ∈ Fτ: 1≤ ≤i}a e in he ube Ti. Fo he case i= 0 we suppose ha B0=∅. Theo em 1. The o mula θ(i)is an in a ian o he main loop. Tha is, ∀i(0 ≤i≤q→θ(i)) P oo . By induc ion on i. The case i= 0 is i ial. Le i < q be such ha he o mula θ(i)is ue. Le τ∈Ti+1 =T∗ i+1, i+1 ∪T− i+1. •I τ∈T− i+1, hen τ∈Ti∧i+ 1 /∈τ. In his case we ha e τ∈Ti and i+ 1 /∈τ. As τ∈Ti, om he induc ion hypo hesis we ob ain ha (a) ∀k(1 ≤k≤i∧k∈τ→(q+Bk)⊆τ) (b) ∀s(1 ≤s≤p∧(q+s)∈τ→ ∃ k∈τ(1 ≤k≤i∧s∈Bk))] Ha ing in mind ha i+ 1 /∈τwe ha e (a’) ∀k(1 ≤k≤i+ 1 ∧k∈τ→(q+Bk)⊆τ) F om (b)we di ec ly ob ain (b’) ∀s(1 ≤s≤p∧(q+s)∈τ→ ∃ k∈τ(1 ≤k≤i+ 1 ∧s∈ Bk))] So, he o mula θ(i+ 1) is ue. •I τ∈T∗ i+1, i+1 , om Co olla y 1 we deduce ha he e exis s ρ∈Ti such ha ρ∈Ti e i ying i+ 1 ∈ρand STEP(ρ, i + 1) = τ. Then τ=ρ∪(q+Bi+1). 220 Fo mal Ve i ica ion o P og ams in Molecula Models... Inpu : T0 T−1,0←T0;T−1,1← ∅;T0,1←T0;T∗ 0,1← ∅ Fo i←0 o q−1do Ti,i+2 ← ∅ Fo j←i o 0do T+ i,j ←+(Ti−1,j, i + 1) Ti,j+1 ←combine(T+ i,j, T∗ i,j+1) T∗ i,j ← −(Ti−1,j, i + 1) Ti,0←T∗ i,0 i Tq−1,1is nonemp y Read Tq−1,1 else Read Tq−1,2 else Read Tq−1,3 . . . else Read Tq−1,q Ob iously, his p og am is equi alen o he abo e one in he ollowing sense: bo h ha e he same inpu ubes, T0, and p oduce ou pu ubes (T0, . . . , Tq, and Tq−1,0, . . . , Tq−1,q espec i ely) such ha he con en s o he ubes Tiand Tq−1,i ( o i= 0, . . . , q) a e he same. This p og am p oduces i+ 1 ubes (Ti,i+1, . . . , Ti,0)a e he execu- ion o he i- h s ep o he main loop, as Figu e 1 illus a es. T T T T T T T T TT T T T T T 0 0,0 0,1 1,0 1,1 1,2 2,0 2,1 2,2 2,3 3,0 3,1 3,2 3,3 3,4 Combine Combine Combine Combine Combine Combine - ++ + + + -+ + + + + - - - - - -- - i=1 i=3 i=2 i=0 Sepa a e Sepa a e Sepa a e Sepa a e 1 2 3 4 Figu e 1. Labelled me ge-bina y ee. Tha is, he execu ion o his p og am can be desc ibed as a oo ed di- ec ed g aph wi h dep h q ha we will call as labelled me ge-bina y ee wi h dep h q, and ha can be de ined as ollows: M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 221 De ini ion 5. A g id wi h dep h h,Gh= (Vh, Eh), is he ollowing di- ec ed g aph: Vh={(i, j) : 0 ≤i≤h∧0≤j≤i} Eh={((i, j),(i+ 1, j)),((i, j),(i+ 1, j + 1)) : 0 ≤i < h ∧0≤j≤i} De ini ion 6. A labelled me ge-bina y ee wi h dep h his a uple (Gh, L, {Fi: 0 ≤i≤h−1}, B, T0, l) whe e: •Ghis a g id wi h dep h h. •Lis a nonemp y se (i s elemen s will be called labels). •Fo each i(wi h 0≤i≤h−1) Fiis a unc ion om L o L×L (we will no e Fi= (F− i, F+ i)). •Bis a bina y unc ion om L×L o L. •T0belongs o L( ha is, T0is a label). •lis a unc ion om Vh o L, called he labelling unc ion, de ined by ecu sion (using T0, Fiand B), as ollows:            l(0,0) = T0 l(i+ 1,0) = F− i(l(i, 0)) l(i+ 1, i + 1) = F+ i(l(i, i)) l(i+ 1, j) = B(F− i(l(i, j −1)), F+ i(l(i, j))) wi h 0≤i < h and 1≤j≤i. In he execu ion o he designed molecula p og am a labelled me - ge-bina y ee wi h dep h qis ob ained, whe e: (a) The labels a e he ubes. (b) Fo each i(wi h 0≤i≤q−1) we ha e Fi(T) = sepa a e(T, i+1). So, F− i(T) = −(T, i + 1) and F+ i(T) = +(T, i + 1) 222 Fo mal Ve i ica ion o P og ams in Molecula Models... (c) The bina y unc ion, B, is he combine molecula ope a ion (ca- lled me ge oo). (d) T0is he inpu es – ube o he sub ou ine. This combina o ics s uc u e allows us o design a sub ou ine sol ing a mo e gene al so ing p oblem, whe e he seman ic o he sub ou ine is e y close o he seman ic o he p oblem ([3]). To es ablish he o mal e i ica ion o he sub ou ine, in connec ion wi h he Minimal Se Co e Selec ion p oblem, we ha e o p o e speci i- cally ha : •E e y molecule, σ, in he ou pu ube, Tq−1, (wi h 1≤ ≤q), e i ies |σ|= (Soundness). •E e y molecule, σ, in he inpu ube, T0, such ha |σ|= (wi h 1≤ ≤q), is in he ou pu ube Tq−1, (Comple eness). The execu ion o he sub ou ine can be seen as an e olu ion o a popula- ion o elemen s. Ini ially, he popula ion is de e mined by he mul ise o molecules in he inpu ube, T0. E e y molecule is an indi idual, and epea ed ones can exis a he same ime (so cloned membe s can be ali e simul aneously in his popula ion). E e y s ep o he main loop can be in e p e ed as a ime uni . A e a lapse, he popula ion is ans o med in o ano he one, bu , in his case, he e is no dea h o mu a ion in elemen s, since his sub ou ine is, basically, a il e ing p ocedu e. We conside he ollowing o mulas: ψ(i, 0) ≡ ∀σ(σ∈Ti,0↔σ∈T0∧ ∀k(1 ≤k≤i+ 1 →k /∈σ)) ψ(i, j + 1) ≡ ∀σ(σ∈Ti,j+1 ↔(σ∈Ti−1,j ∧i+ 1 ∈σ)∨ ∨(σ∈Ti−1,j+1 ∧i+ 1 /∈σ)) θ(i)≡ ∀j(0 ≤j≤i+ 1 →ψ(i, j)) Theo em 5. The o mula θ(i)is an in a ian o he main loop. Tha is, ∀i(0 ≤i≤q−1→θ(i)). P oo . By induc ion on i. •The esul is ue o i= 0. The o mula ψ(0,0) is ue because M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 223 σ∈T0,0⇐⇒ σ∈T∗ 0,0=−(T−1,0,1) = −(T0,1) ⇐⇒ σ∈T0∧1/∈σ⇐⇒ σ∈T0∧ ∀ k(1 ≤k≤0+1→k /∈σ). The o mula ψ(0,1) is ue because σ∈T0,1⇐⇒ σ∈T+ 0,0∪T∗ 0,1=T+ 0,0= +(T−1,0,1) ⇐⇒ σ∈ T−1,0∧1∈σ⇐⇒ (σ∈T−1,0∧1∈σ)∨(σ∈T−1,1∧1/∈σ). •Le i < q −1such ha he o mula θ(i)is ue. Le us see ha he o mula θ(i+ 1) is ue; ha is, ∀j(0 ≤j≤i+ 2 →ψ(i+ 1, j). –Fo j= 0 we ha e he ollowing: σ∈Ti+1,0⇐⇒ σ∈T∗ i+1,0⇐⇒ σ∈ −(Ti,0, i + 2) ⇐⇒ σ∈ Ti,0∧i+ 2 /∈σ⇐⇒ σ∈T0∧ ∀ k(1 ≤k≤i+ 1 →k /∈ σ)∧i+ 2 /∈σ⇐⇒ σ∈T0∧ ∀ k(1 ≤k≤i+ 2 →k /∈σ). –Le j≤i+ 2 such ha j > 0and le us see ha ψ(i+ 1, j)is ue. Indeed: σ∈Ti+1,j ⇐⇒ σ∈T+ i+1,j−1∪T∗ i+1,j ⇐⇒ σ∈+(Ti,j−1)∪ −(Ti,j, i+2) ⇐⇒ (σ∈Ti,j−1∧i+2 ∈σ)∨(σ∈Ti,j ∧i+2 /∈σ). Nex , we desc ibe he ace o e e y molecule in he inpu ube along he execu ion o he sub ou ine. Fo his, i σ∈T0is gi en, we will w i e σ= (i1, . . . , i ) o no e ha 1≤i1<· · · < i ≤qand ∀j(1 ≤j≤ →σ(ij) = 1) ∧ ∀ ∀j(1 ≤ ≤q∧ij6= →σ( ) = 0) Tha is, he molecule σ= (i1, . . . , i )∈T0encodes in a na u al way he sub amily F0={Bi1, . . . , Bi }o F. P oposi ion 1. Le σ= (i1, . . . , i )∈T0, whe e 1≤i1< i2<· · · < i ≤ q. Then (1) ∀j(1 ≤j≤ →σ∈Tij−1,j). (2) ∀ (1 ≤ ≤q−i →σ∈Ti + −1, ). (3) σ∈Tq−1, . 224 Fo mal Ve i ica ion o P og ams in Molecula Models... P oo . 1. By induc ion on j. •Fi s , we conside he case j= 1. –I i1= 1 hen Ti1−1,1=T0,1=T0. So, σ∈Ti1−1,1. –I i1>1 hen we p o e ha ∀s(1 ≤s<i1→σ∈ Ts−1,0). Indeed: ∗Le sbe such ha 1≤s < i1. Then, σ∈T0∧ ∀ k(1 ≤ k≤s−1 + 1 →k /∈σ). As s−1≥0 he o mula ψ(s−1,0) is ue, so we deduce ha σ∈Ts−1,0. F om 1≤i1−1< i1we ob ain ha σ∈T(i1−1)−1,0. As i1∈σwe ha e σ∈+(Ti1−2,0, i1). Then σ∈Ti1−2,0,i1∈ σ, and he o mula ψ(i1−1,1) is ue. Hence, σ∈Ti1−1,1. •Le jbe such ha 1≤j < . Le us suppose ha σ∈Tij−1,j. We ha e o p o e ha σ∈Tij+1−1,j+1. –I ij+1 −1 = ij( ha is, ij+1 =ij+ 1), om induc ion hypo hesis we ha e σ∈Tij−1,j and ij+1 ∈σ. Tha is, σ∈Tij−1,j and ij+1 ∈σ. As o mula ψ(ij+1 −1, j+1) ≡ ψ(ij, j + 1) is ue, we deduce ha σ∈Tij+1−1,j+1. –I ij+1 −1> ijwe p o e ha ∀ (1 ≤ ≤ij+1 −ij−1→ σ∈Tij+ −1,j), by induc ion on . ∗We ha e σ∈Tij−1,j and ij+ 1 /∈σ. As o mula ψ(ij, j)is ue (and j > 0) we ob ain ha σ∈Tij,j. Tha is, σ∈Tij+1−1,j. So, he esul is ue o = 1. ∗Le be such ha < ij+1 −ij−1and le us suppose he esul holds o . Then, σ∈Tij+ −1,j. As ij< ij+ + 1 < ij+1, we ha e ij+ + 1 /∈σ. Ha ing in mind ha he o mula ψ(ij+ , j)is ue, we conclude ha σ∈Tij+ ,j. Tha is, σ∈Tij+( +1)−1,j. Now, le us see ha σ∈Tij+1−1,j+1. Applying he abo e ela ion o =ij+1 −ij−1,σ∈Tij+(ij+1−ij−1)−1,j = Tij+1−2,j. As ij+1 ∈σand he o mula ψ(ij+1 −1, j + 1) is ue we deduce ha σ∈Tij+1−1,j+1. 2. By induc ion on . M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 225 •Fo = 1 we ha e ha 1≤q−i , ha is, i + 1 ≤q. F om (1) we ob ain ha σ∈Ti −1, . Bu i +1 /∈σ. As o mula ψ(i , ) is ue we conclude ha σ∈Ti , . Tha is, σ∈Ti +1−1, . •Le be such ha 1≤ <q−i , and le us suppose ha σ∈Ti + −1, . As i < i + + 1 ≤qwe ha e i + + 1 /∈ σ. Taking in o accoun ha he o mula ψ(i + , )is ue (because i + ≤q−1), we conclude ha σ∈Ti + , . Tha is, σ∈Ti +( +1)−1, . 3. Applying he esul ob ained in (2), conside ing =q−i , we deduce ha σ∈Ti +(q−i )−1, =Tq−1, . Nex we will p o e ha he gene a ed ubes a e i- h s ep o he main loop, {Ti,0, Ti,1, . . . , Ti,i+1}, o m a pa i ion o he ini ial es ube, T0. This con i ms ha he sub ou ine uns a il e ing p ocedu e whe e no s and dies along he execu ion. P oposi ion 2. ∀i(0 ≤i≤q−1→T0=S0≤j≤i+1 Ti,j). P oo . Le us i s p o e ha ∀i(0 ≤i≤q−1→T0⊆S0≤j≤i+1 Ti,j). By induc ion on i. •Le σ∈T0. Then (σ∈T0∧1∈σ)∨(σ∈T0∧1/∈σ). So, (σ∈T0∧1∈σ) =⇒(σ∈T−1,0∧1∈σ) =⇒σ∈T0,1 (σ∈T0∧1/∈σ) =⇒σ∈T0,0 Hence σ∈T0,1∪T0,0⊆S0≤j≤1T0,j. •Le i < q −1be such ha T0⊆S0≤j≤i+1 Ti,j. Le σ∈T0. F om induc ion hypo hesis, he e exis s jsuch ha 0≤j≤i+ 1 and σ∈Ti,j. Then (σ∈Ti,j ∧i+ 2 ∈σ)∨(σ∈Ti,j ∧i+ 2 /∈σ). –Le us suppose ha σ∈Ti,j and i+ 2 ∈σ. As o mula ψ(i+1, j +1) is ue we deduce ha σ∈Ti+1,j+1 ⊆S0≤s≤i+2 Ti+1,s. –Le us suppose ha σ∈Ti,j and i+ 2 /∈σ 226 Fo mal Ve i ica ion o P og ams in Molecula Models... ∗I j= 0 hen σ∈Ti,0and i+ 2 /∈σ. Bu σ∈Ti,0=⇒σ∈ T0∧ ∀ k(1 ≤k≤i+ 1 →k /∈σ). So, σ∈T0∧ ∀ k(1 ≤ k≤i+ 2 →k /∈σ). As o mula ψ(i+ 1,0) is ue, we deduce ha σ∈Ti+1,0⊆S0≤s≤i+2 Ti+1,s. ∗I j > 0, aking in o accoun ha σ∈Ti,j ∧i+ 2 /∈σ and he o mula ψ(i+ 1, j)is ue, we conclude ha σ∈ Ti+1,j. Tha is, σ∈S0≤s≤i+2 Ti+1,s. Now, le us see ha ∀i(0 ≤i≤q−1→S0≤j≤i+1 Ti,j ⊆T0). Fo ha , i is enough o p o e ha ∀i∀j(0 ≤i≤q−1∧0≤j≤i+1 →Ti,j ⊆T0). By induc ion on i. •The esul holds o i= 0. Indeed: T0,0=T∗ 0,0=−(T−1,0,1) = −(T0,1) ⊆T0 T0,1=T+ 0,0∪T∗ 0,1=T+ 0,0= +(T−1,0,1) = +(T0,1) ⊆T0 •Le i < q −1be such ha ∀j(0 ≤j≤i+ 1 →Ti,j ⊆T0). Le us see ha ∀j(0 ≤j≤i+ 2 →Ti+1,j ⊆T0). –I j= 0 hen Ti+1,0=T∗ i+1,0=−(Ti,0, i+2) = −(Ti,0, i+2) h.i. ⊆ T0. –I j > 0(and j≤i+ 2) hen we ha e: Ti+1,j =T∗ i+1,j−1∪ T∗ i+1,j = +(Ti,j−1, i + 2) ∪ −(Ti,j, i + 2) ⊆Ti,j−1∪Ti,j. Taking in o accoun ha j≤i+ 1 =⇒Ti,j−1∪Ti,j ⊆T0 j=i+ 2 =⇒Ti,j−1∪Ti,j =Ti,i+1 ∪Ti,i+2 =Ti,i+1 ⊆T0 we conclude ha Ti+1,j ⊆T0. P oposi ion 3. ∀i(0 ≤i≤q−1→ ∀ ∀s(0 ≤ < s ≤i+ 1 → Ti, ∩Ti,s =∅)). P oo . By induc ion on i. •The esul holds o i= 0 because T0,0∩T0,1=T∗ 0,0∩T0,1=−(T−1,0,1) ∩+(T−1,0,1) = ∅. M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 227 •Le i < q −1be such ha ∀ ∀s(0 ≤ < s ≤i+ 1 →Ti, ∩ Ti,s =∅). Le , s be such ha 0≤ < s ≤i+ 2. Le us see ha Ti+1, ∩Ti+1,s =∅. –Le us suppose ha s=i+ 2. I he e exis s τ∈Ti+1, ∩Ti+1,i+2 hen τ∈Ti+1,i+2 =⇒(τ∈Ti,i+1 ∧i+ 2 ∈τ)∨ (τ∈Ti,i+2 ∧i+ 2 /∈τ) =⇒(τ∈Ti,i+1 ∧i+ 2 ∈τ) Bu τ∈Ti+1,0=⇒τ∈T0∧ ∀ k(1 ≤k≤i+ 2 →k /∈τ), and i+ 2 ∈τ. So, > 0. Then, τ∈Ti+1, =⇒τ∈Ti, −1. Hence, Ti,i+1 ∩Ti, −16=∅. This con adic s ou assump ion. –Le us suppose ha = 0 and 1≤s≤i+ 1. I he e exis s τ∈Ti+1,0∩Ti+1,s hen τ∈Ti+1,0=⇒τ∈T0∧ ∀ k(1 ≤k≤i+ 2 →k /∈τ) =⇒τ∈Ti,0∧ ∀ k(1 ≤k≤i+ 2 →k /∈τ) τ∈Ti+1,s =⇒(τ∈Ti,s−1∧ ≤ i+ 2 ∈τ)∨ (τ∈Ti,s ∧i+ 2 /∈τ) So, τ∈Ti,0∩Ti,s. This con adic s he induc ion hypo esis (because 0< s ≤i+ 1). –Le us suppose ha > 0and 1≤s≤i+ 1. I he e exis s τ∈Ti+1, ∩Ti+1,s hen τ∈Ti+1, =⇒(τ∈Ti, −1∧i+ 2 ∈τ)∨ (τ∈Ti, ∧i+ 2 /∈τ) τ∈Ti+1,s =⇒(τ∈Ti,s−1∧i+ 2 ∈τ)∨ (τ∈Ti,s ∧i+ 2 /∈τ) I i+ 2 ∈τ hen Ti, −1∩Ti,s−16=∅, which con adic s he induc ion hypo hesis. I i+2 /∈τ hen Ti, ∩Ti,s 6=∅, which con adic s he induc ion hypo hesis. 228 Fo mal Ve i ica ion o P og ams in Molecula Models... Co olla y 6. Tq−1,0=∅. P oo . Le us suppose ha Tq−1,06=∅. Then he e exis s σ= (i1, . . . , i ) ∈Tq−1,0, wi h > 0. F om P oposi ion 1.(3) we ha e σ∈Tq−1, . So, Tq−1,0∩Tq−1, 6=∅, which con adic s P oposi ion 3. Finally, we es ablish he soundness and he comple eness o he de- signed sub ou ine ha sol es he Minimal Se Co e Selec ion p oblem. Theo em 6. (Soundness) E e y s and, σ, in he inal es – ube, Tq−1, (wi h 1≤ ≤q), e i ies ha i s leng h is . Tha is, ∀ (1 ≤ ≤q→ ∀σ∈ Tq−1, (|σ|= )). P oo . Le be such ha 1≤ ≤q. Le σ∈Tq−1, . F om P oposi ion 2 we ob ain ha σ∈T0. F om P oposi ion 1.(3), we ha e σ∈Tq−1,|σ|. F om P oposi ion 3 we conclude ha |σ|= . Theo em 7. (Comple eness) E e y s and, σ, in he ini ial es – ube, T0, wi h leng h is in he ou pu ube, Tq−1, . Tha is, ∀σ∈T0(|σ|= → σ∈Tq−1, ). Mo eo e , ∀σ∈T0∃! (1 ≤ ≤q∧σ∈Tq−1, ). P oo . Le σ∈T0such ha |σ|= . F om P oposi ion 1.(3) we can deduce ha σ∈Tq−1, . In he o he hand, om P oposi ion 3 (wi h i=q−1) he e exis s jsuch ha 0≤j≤i+ 1 and σ∈Tq−1,j. F om Co olla y 1 we ob ain j > 0, and om P oposi ion 3 we conclude ha j is unique. 7 Conclusions A me hodology o es ablish he o mal e i ica ion o FOR o W HILE p og ams wi hin molecula compu ing models wi h andom access me- mo y has been p esen ed. The sea ch o in a ian o mulas o he main loop needs a de ailed s udy o he e olu ion o e e y molecule along he execu ion o he p og am. A unc ion called ST EP has been in oduced o cap u e he e olu ion o he molecules a e one s ep o he main loop. These solu ions a e applied o sol e some nume ical NP-comple e p oblems: he Gene a ing Co e Families p oblem, he Se Co e ing p ob- lem and he Minimal Se Co e Selec ion P oblem. The p oblems we M. J. PÉREZ-JIMÉNEZ, F. SANCHO-CAPARRINI 229 ha e chosen in his pape p esen some in e es ing and di e en cha - ac e is ics wi h espec o he STEP unc ion. We hink ha he s udy o he o mal e i ica ion o molecula p o- g ams is a necessa y s ep o hei au oma ic p ocessing by means o easoning sys ems (we a e cu en ly wo king on ACL2 and PVS). Acknowledgemen The suppo o his esea ch h ough he p ojec TIC2002-04220-C03- 01 o he Minis e io de Ciencia y Tecnología o Spain, co inanced by FEDER unds, is g a e ully acknowledged. Re e ences [1] Adleman, L. Molecula Compu a ion o Solu ions o Combina o- ial P oblems, Science,268 (1994), 1021–1024. [2] Ga ey, M. R.; Johnson, D. S. Compu e s and in ac abili y, W. H. F eeman and Company, New Yo k, 1979. [3] Pé ez-Jiménez, M. J.; Sancho-Capa ini, F. Sol ing Knapsack P ob- lems in a S icke Based Model, in Jonoska, N.; Seeman, N. (eds.), DNA Compu ing, LNCS 2340 (2002), 161–171. [4] Hoa e, C. A. R. An axioma ic basis o compu e p og amming, Communica ions o he ACM,12 (1969), 576–583. [5] Pé ez-Jiménez, M. J.; Sancho-Capa ini, F. Minimal Se Co e P oblem: On a DNA solu ion o selec ion s age, in Ma ín-Vide, C.; P˘aun, Gh. (eds.), P e-P oceedings o Wo kshop on Memb ane Com- pu ing, RGML Repo 17/01 (2001), 251–258. [6] Roweis, S.; Win ee, E.; Bu goyne, R.; Chelyapo , N.; Goodman, M.; Ro hemund, P.; Adleman, L. A S icke –Based Model o DNA Compu a ion, Jou nal o Compu a ional Biology,5, 4 (1998), 615–629.