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.