main.tex

\documentclass[12pt]{article}
% pre\'ambulo
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\usepackage[spanish,activeacute]{babel}
\usepackage{mathtools}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{url}
\usepackage{tikz}
\usepackage{graphicx}
\usepackage{algorithm}
\usepackage[noend]{algpseudocode}
\graphicspath{ {images/} }
\usetikzlibrary{arrows,positioning}
\tikzset{
    %Define standard arrow tip
    >=stealth',
    %Define style for boxes
    punkt/.style={
           rectangle,
           rounded corners,
           draw=black, very thick,
           text width=5em,
           minimum height=4em,
           text centered},
    % Define arrow style
    pil/.style={
           ->,
           thick,
           shorten <=2pt,
           shorten >=2pt,}
}
\setlength{\parskip}{\baselineskip}
\usepackage[style=numeric-comp,backend=bibtex]{biblatex}
\bibliography{refs.bib}

\title{Dise\~no y verificaci\'on formal de programas moleculares en el modelo d\'ebil de Amos}
\author{Sergio Rodr\'iguez Calvo}
\date{Septiembre de 2017}


\begin{document}
    \maketitle
    \thispagestyle{empty}
    \begin{center}
      Departamento de Ciencias de la Computaci\'on e
      Inteligencia Artificial \\
      Universidad de Sevilla
      \end{center}
  % cuerpo del documento
  % abstract
  \bf{Abstract. }\rm
    \emph{En el presente trabajo se pretende estudiar el dise'no y la verificaci'on formal
    de dos programas moleculares en el modelo d'ebil de Amos, que resuelven el problema de la generaci'on
    de permutaciones; y el problema del camino hamiltoniano en su versi'on dirigida y sin
    nodos distinguidos. En concreto, el presente trabajo se centra en reescribir, as'i como, completar algunos detalles
    de las demostraciones, que se encuentran el trabajo original \cite{Mario-deJesus}.
    El desarrollo de este trabajo tiene como objetivo ser entregado como trabajo final de la asignatura de
    Computaci'on Bioinspirada.}

\section{Introducci'on}

En la d'ecada de los cincuenta comienza a ser evidente que existe una analog'ia entre algunos procesos
matem'aticos y ciertos procesos biol'ogicos. Un organismo vivo puede ser visto como el resultado de
aplicar una serie de operaciones bioqu'imicas sobre una cadena de 'acido desoxirribonucleico (ADN).

Posteriormente, en la decada de los noventa, se demostr'o que se pueden usar ciertos procesos biol'ogicos
para atacar la resolubilidad de problemas matem'aticos dif'iciles. Estos problemas tambi'en son conocidos
como computacionalmente intratables, y son aquellos que su soluci'on algor'itmica toma una cantidad de
recursos exponenciales en el tama'no del dato de entrada.

Esta resolubilidad est'a relacionada con la potencia de c'alculo y la densisdad de almacenamiento de los
ordenadores convencionales.

En la propia d'ecada de los cincuenta ya se introdujo el concepto te'orico de computaci'on a nivel molecular.
En los ordenadores convencionales la paralelizaci'on y la miniaturizaci'on son un objetivo importante, y la
computaci'on molecular puede suponer un paso m'as en este sentido.

Sobre todo, a partir de que en la d'ecada de los ochenta, cuando se demostr'o la existencia de un l'imite en la potencia
de c'alculo y, tambi'en, en la miniaturizaci'on de los componentes electr'onicos empleados en los ordenadores convencionales.

Por 'ultimo, se enumeran las principales ventajas del uso de la computaci'on molecular:

\begin{itemize}
	\item Sustituci'on de la luz por reacciones qu'imicas, lo que implica un ahorro del consumo energ'etico.
	\item El uso de interruptores moleculares permite, seg'un se estima, disponer de m'as de mil procesadores
    en el mismo espacio que un procesador convencional.
	\item Se estima que los interruptores moleculares pueden aumentar cien mil millones de veces la capacidad
    de procesamiento respecto a los ordenadores convencionales.
	\item Se estima que se podr'ia reproducir la capacidad de cien ordenadores en el tama'no de un grano de sal fina.
\end{itemize}

\section{Modelo d'ebil de Amos}

Antes de introducir el Modelo d'ebil de Amos, se necesita previamente conocer los detalles y principios
de la computaci'on molecular, as'i como, los distintos modelos previos a este, los cuales se pueden encontrar
en el documento original del profesor del departamento de Ciencias de la Computaci'on de la Universidad
de Sevilla, Mario de Jes'us P'erez Jim'enez \cite{Mario-deJesus}.

El Modelo d'ebil de Amos consiste en un modelo de computaci'on basada en ADN, esto es, que utiliza como sustrato
computacional el ADN, y en el cual se realizan filtrados sobre el sustrato anterior. En este caso, no existe
memoria de acceso aleatorio como en la computaci'on cl'asica. Para almacenar el sustrato, al igual que en otros
modelos de computaci'on molecular, se utiliza un tubo de ensayo que contendr'a la muestra.

Dicho tubo es un multiconjunto finito de cadenas del alfabeto $\sum_{ADN} = \{A, C, G, T\}$.

A nivel abstracto, en el Modelo d'ebil de Amos las operaciones que se pueden realizar sobre los tubos
son las siguientes:

\begin{itemize}
    \item \textbf{Quitar (\textit{T},\{$ \gamma_{1},...,\gamma_{n} $\}):} Dado un tubo, \textit{T}, y un n'umero finito
    de cadenas, $ \gamma_{1},...,\gamma_{n} $, de $ \sum $, devuelve el tubo obtenido de T eliminando
    todas aquellas cadenas que contengan, al menos, una ocurrencia de alguna de las cadenas
    $ \gamma_{1},...,\gamma_{n} $.
    \item \textbf{Copiar (\textit{T},\{$ \textit{T}_{1},...,\textit{T}_{n} $\}):} Dado un tubo, \textit{T}, y un numero
    natural $ \textit{k} \geq 2 $, devuelve \textit{k} tubos, $\textit{T}_{1},...,\textit{T}_{n}$, que son
    copias exactas de \textit{T}.
    \item \textbf{Uni'on (\{$ \textit{T}_{1},...,\textit{T}_{n} $\}):} Dados los tubos
    $\textit{T}_{1},...,\textit{T}_{n}$, con $ \textit{k} \geq 2 $, devuelve un tubo \textit{T}, cuyo contenido
    es la uni'on de los tubos $\textit{T}_{1},...,\textit{T}_{n}$ como multiconjuntos.
    \item \textbf{Selecci'on (\textit{T}):} Dado un tubo, \textit{T}, selecciona aleatoriamente un elemento de \textit{T}
    en el caso en que $\textit{T} \neq \emptyset$; en caso contratio, devuelve \textbf{NO}.
\end{itemize}

Estas operaciones ser'an instrucciones moleculares primitivas del modelo d'ebil. Adem'as, cabe destacar que
en este modelo la 'unica operaci'on molecular que implementa paralelismo masivo es \textit{quitar}.

El primer problema, el de la generaci'on de permutaciones, ser'a abordado previo al problema del camino hamiltoniano
, ya que, ser'a necesario para el modelado y resoluci'on del segundo problema.

\subsection{Problema de la generaci'on de permutaciones}

En esta secci'on se muestra como abordar desde el punto de vista de la computaci'on molecular la resolubilidad
del problema de la generaci'on de permutaciones. Antes, se define en qu'e consiste una permutaci'on para, a
continuaci'on, abordar el problema.

Una permutaci'on la definimos como \textit{dado un numero natural, $n \geq 1$, una permutaci'on de orden n es una
aplicaci'on biyectiva del conjunto finito \{1,...,n\} en s'i mismo}.

\begin{figure}[h]
\centering
\includegraphics[scale=0.6]{permutaciones}
\caption{Ejemplo de permutaci'on considerada como funci'on biyectiva. En este caso, para $n = 3$.}
\end{figure}

Una vez tenemos definido qu'e es una permutaci'on vamos a introducir el problema de generaci'on de
permutaciones, que consiste en, \textit{dado un n'umero natural, $n \geq 2$, generar todas las permutaciones
 de orden n}.

\subsubsection{Dise'no del programa molecular}

En primer lugar, hay que definir el modelo mediante el cual se pretende representar el problema con los
elementos que tenemos en la computaci'on molecular. Esto es, definir por un lado el alfabeto:
$ \sum = \{(p_{i},c_{j}) : 1 \leq i,j \leq n\} $, donde $p_{i}$ y $c_{j}$ son dos oligos que codificar'an
respectivamente la posici'on $i$-'esima en la permutaci'on y el n'umero \textit{j}.

A continuaci'on, se necesita definir el tubo de entrada, $T_{0}$, para poder comenzar el experimento, es decir,
aplicar las operaciones abstractas de la secci'on anterior seg'un un determinado algoritmo. En este caso,
se trata de un multiconjunto de entrada con un n'umero finito de mol'eculas y que codifican todas las
posibles sucesiones para una longitud \textit{n}. Formalmente ser'ia:

\begin{equation*}
  T_{0} = \{\{ \sigma \in \sum_{}^n : \exists x_{1},..., \exists x_{n} (\sigma = (p_{1},x_{1}),
  (p_{2},x_{2}),..., (p_{n},x_{n})) \}\}
\end{equation*}

En la f'ormula anterior, $ \sigma $, es una codificaci'on concreta, tal que,
$ \sigma = p_{1}x_{1}...p_{n}x_{n} $.

La idea aqu'i es generar todas las posibles permutaciones, utilizando un tubo inicial, $ T_{0} $,
que contiene la codificaci'on de todas las posibles soluciones de longitud $ n $. El programa sigue los
 siguientes pasos hasta $ n - 1 $ veces:

 \begin{itemize}
     \item Un primer filtro sobre $ T_{0} $ para seleccionar las moleculas, $ \sigma $, tal que:
        \begin{equation*}
            \forall r > 1 ( (\sigma)_{1} \neq (\sigma)_{r} )
        \end{equation*}
           Esto es, para todas las posiciones, $r$, mayores que 1, devolver todas aquellas codificaciones, tal que,
           el n'umero que ocupa la posici'on $r$-'esima sea distinto del n'umero de la primera posici'on.
     \item Un segundo filtro respecto del paso anterior donde se seleccionan las moleculas, $ \sigma $, tal que:
     \begin{equation*}
         \forall r > 2 ( (\sigma)_{1} \neq (\sigma)_{r} \land (\sigma)_{2} \neq (\sigma)_{r} )
     \end{equation*}
           Esto es, del conjunto resultante del paso anterior, para todas las posiciones, $r$, mayores que dos,
           devolver todas aquellas codificaciones, tal que, el n'umero que ocupa la posici'on $r$-'esima sea distinto
            de el n'umero de la posici'on primera y de la posici'on segunda a la vez.
 \end{itemize}}

 La notaci'on, $ (\sigma)_{r} $, representa el n'umero que ocupa la posici'on \textit{r-'esima} en la
 sucesi'on de longitud $ n $ codificada por $ \sigma $. Es decir, $ (\sigma)_{r} = x_{r} $ para todo $ r $
 $ (1 \leq r \leq n) $.

El algoritmo a seguir en el programa molecular, basado en la idea de filtrar sobre un determinado tubo $ T_{0} $
de entrada, es el siguiente:

\begin{algorithmic}
    \Require $T_{0}$
    \For {$j\leftarrow1$ in $n - 1$}
        \State copiar($T_{0}, \{T_{1},...,T_{n}\}$)
        \For {$i\leftarrow1$ in $n$}
            \State quitar($T_{i}, \{p_{j}r : r \neq i\} \cup \{p_{k}i : j + 1 \leq k \leq n\} $)
        \EndFor
        \State uni'on($\{T_{1},...,T_{n}\},T_{0}$)
    \EndFor
    \Return $T_{0}$
\end{algorithmic}

Este algoritmo presenta una complejidad $O(n^2)$, es decir, orden cuadr'atico en $n$. Por tanto, el n'umero de
operaciones moleculares es $n^2$.

\subsubsection{Metodolog'ia para verificar formalmente programas con bucle principal}

En esta secci'on, se explica una metogolog'ia para verificar formalmente que un programa con  bucle
principal satisface una propiedad.

Se representa el bucle principal como una f'ormula y se busca que dicha f'ormula satisfaga las siguientes propiedades:

\begin{itemize}
    \item La f'ormula es verdadera antes de comenzar el bucle.
    \item La f'ormula es invariante, es decir, que es verdadera tambi'en al finalizar el bucle.
    \item La veracidad indica que satisface la propiedad requerida.
\end{itemize}}

Adem'as, se necesita probar la correcci'on y completitud.

Con la demostraci'on de la correci'on se pretende demostrar las propiedades de una f'ormula, la cual modela
el programa. Tal y como se describi'o previamente. Consiste en un teorema (invarianza) y un corolario (correci'on), donde se prueba
que toda mol'ecula del tubo de salida codifica una valoraci'on que hace verdadera dicha f'ormula.

Con la demostraci'on de la completitud se pretende demostrar las propiedaes de la f'ormula, la cual modela el
programa. Tal y como se describi'o previamente. Consiste, tambi'en, en un teorema (invarianza) y un corolario (completitud), donde se prueba
que toda mol'ecula del tubo de salida, y que codifica una valoraci'on que hace verdadera la f'ormula,
aparecer'a en el tubo de salida.

\subsubsection{Verificaci'on formal del programa molecular}

Para realizar la verificaci'on formal es necesario etiquetar cada uno de los tubos que se van a obtener
a los largo del algoritmo descrito anteriormente. Por tanto, el algoritmo va a ser reescrito de la
siguiente forma:

\begin{algorithmic}
    \Require $T_{0}$
    \For {$j\leftarrow1$ in $n - 1$}
        \State copiar($T^{j-1}_{0}, \{T^{j}_{1},...,T^{j}_{n}\}$)
        \For {$i\leftarrow1$ in $n$}
            \State $\bar{T}^{j}_{i}$ \leftarrow quitar($T^{j}_{i}, \{p_{j}r : r \neq i\} \cup \{p_{k}i : j + 1 \leq k \leq n\} $)
        \EndFor
        \State uni'on($\{\bar{T}_{1},...,\bar{T}_{n}\},T^{j}$)
    \EndFor
    \Return $T_{n - 1}$
\end{algorithmic}

Antes de continuar, hay que aclarar la notaci'on a emplear a partir de aqu'i. $A_{\sigma,j}$ ser'a el conjunto
$\{\sigma_{1},...,\sigma_{j}\}$, es decir, n'umero en cada posici'on $j$-'esima, para $(1 \leq j \leq n)$, en cada
$\sigma \in T_{0}$. Esto es, un conjunto que contiene todos los n'umeros que contienen una determinada codificaci'on, $\sigma$,
desde 1 hasta la posici'on j en cada caso, y estos, son diferentes entre s'i.

Esta notaci'on que se acaba de describir ser'a necesaria para la correci'on formal del programa que se
acaba de reescribir, y que se utiliza en la siguiente formula:

\begin{equation*}
  \theta(j) \equiv \forall \sigma \in T^{j} (|A_{\sigma,j}| = j \land \forall r ( j + 1 \leq r \leq n \longrightarrow
  (\sigma)_{r} \notin A_{\sigma,j} ))
\end{equation*}

La formula, $\theta(j)$, expresa que toda molecula del tubo $T^{j}$ codifica una sucesi'on de longitud $n$ tal que
los $j$ primeros t'erminos son distintos entre s'i y, adem'as, distintos de los restantes t'erminos de la sucesi'on.

A continuaci'on, se van a exponer una serie de teoremas con los que se pretende realizar la verificaci'on formal,
tomando el algoritmo que se ha reescrito en este apartado.

\textbf{Teorema 1.1.} $\forall j (1 \leq j \leq n-1 \longrightarrow \theta(j))$. Es decir, la formula $\theta$ es un invariante del
bucle principal. Esto es, que $\theta$ no cambia a lo largo de las transformaciones que sufre el tubo en el bucle principal.

Dicho de otro modo, para todo valor $j$, comprendido entre $1$ y $n-1$ ambos inclusive, se cumple $\theta(j)$, por tanto, $\theta(j)$
no var'ia a lo largo de la ejecuci'on del algoritmo.

Se va a realizar la demostraci'on por inducci'on d'ebil sobre $j$, y esta es:

En primer lugar, se tiene que demostrar para $j = 1$. Sea $\sigma \in T^{1}$. Existe $x \in \{1,...,n\}$ tal que
$\sigma \in \bar{T}_{x}^{1} = quitar(T_{x}^{1}, \{p_{1}r : r \neq x\} \cup \{p_{k}x : 2 \leq k \leq n\})$.

Entonces $A_{\sigma,1} = \{(\sigma)_{1}\} = \{x\}$, es decir, $|A_{\sigma,1}| = 1$. Ademas, si $2 \leq k \leq n$, entonces
$\sigma \in \bar{T}_{x}^{1} \Longrightarrow (\sigma)_{1} = x \land (\sigma)_{k} \neq x \Longrightarrow (\sigma)_{k}
 \notin A_{\sigma,1}$

Esto 'ultimo quiere decir, que $\sigma$ existe en el tubo resultado de realizar la eliminaci'on de los elementos que cumplen
la condici'on descrita previamente, que llamaremos tubo complementario. Por tanto, se tiene que el conjunto de valores $A_{\sigma,1}$
contiene el elemento $x$ y ese elemento no est'a en la posiciones siguientes en el resto de codificaciones de $\sigma$.

A continuaci'on, suponemos cierto para $j$, y tenemos que $j < n - 1 (j \geq 1)$. Se va a demostrar para $j+1$.

Sea $\sigma \in T^{j+1}$. Y sea $x \in \{1,...,n\}$ tal que

\begin{equation*}
    \sigma \in \bar{T}_{x}^{j+1} = quitar(T_{x}^{j+1}, \{p_{j+1}r : r \neq x\} \cup \{p_{k}x : j + 2 \leq k \leq n\})
\end{equation*}

Entonces, se verifica que

\begin{equation*}
    \sigma \in T_{x}^{j+1} = T^{j} \land (\sigma)_{j+1} = x \land \forall k (j + 2 \leq k \leq n \longrightarrow (\sigma)_{k} \neq x)
\end{equation*}

De la hipotesis de inducci'on se tiene que

\begin{equation*}
    |A_{\sigma,j}| = j \land \forall r (j + 1 \leq r \leq n \longrightarrow (\sigma)_{k} \notin A_{\sigma,j})
\end{equation*}

Teniendo presente que

\begin{equation*}
    A_{\sigma,j+1} = A_{\sigma,j} \cup \{(\sigma)_{j+1}\}
\end{equation*}

y

\begin{equation*}
    (\sigma)_{j+1} \notin A_{\sigma,j}
\end{equation*}

Resulta que $ |A_{\sigma,j+1}| = j + 1 $.

Finalmente si $j + 2 \leq k \leq n $, entonces $(\sigma)_{k} \notin A_{\sigma,j}$ y $(\sigma)_{k} \neq x = (\sigma)_{j+1}$.
Por tanto, se tiene que

\begin{equation*}
    (\sigma)_{k} \notin A_{\sigma,j+1}
\end{equation*}

\textbf{Corolario 1.2.} \textit{(Correci'on del programa) Toda mol'ecula del tubo de salida codifica una permutaci'on de
orden n}.

La demostraci'on es, sea $\sigma \in T^{n-1}$. Como la f'ormula $\theta(n-1)$ es verdadera resulta que
$|A_{\sigma,n-1}| = n - 1 \land \forall r (n - 1 + 1 \leq r \leq n \longrightarrow (\sigma)_{r} \notin A_{\sigma,n-1})$.
Como $A_{\sigma,n} = A_{\sigma,n-1} \cup \{(\sigma)_{n}\}$, concluimos que $|A_{\sigma,n}| = n$. Por tanto, la mol'ecula
$\sigma$ codifica una permutaci'on de orden $n$.

Para establecer la completitud del programa, se va a considerar la siguiente f'ormula:

\begin{equation*}
  \delta(j) \equiv \forall \sigma \in T^{0} (|A_{\sigma,n}| = n \longrightarrow \sigma \in T^{j})
\end{equation*}

Esto es, la f'ormula $\delta(j)$ expresa que toda mol'ecula del tubo $T^{i}$ codifica una sucesi'on de longitud $n$ tal que
los $j$ primeros t'erminos son distintos entre s'i y, adem'as, distintos de los restantes t'erminos de la sucesi'on.

\textbf{Teorema 1.3.} $\forall j (1 \leq j \leq n-1 \longrightarrow \delta(j))$. Es decir, la formula $\delta$ es un invariante del
bucle principal. Esto es, que $\delta$ no cambia a lo largo de las transformaciones que sufre el tubo en el bucle principal.

La demostraci'on, por inducci'on d'ebil sobre $j$, es, sea $\sigma \in  T^{0}$ tal que $|A_{\sigma,n}| = n$. Entonces
la m'olecula $\sigma$ codifica una permutaci'on de orden $n$. Se tiene que $\sigma \in T_{(\sigma)_{1}}^{1}$ y
$\forall r (2 \leq r \leq n \longrightarrow (\sigma)_{r} \neq (\sigma)_{1})$.

Luego, $\sigma \in quitar(T_{(\sigma)_{1}}^{1}, \{p_{1}r : r \neq (\sigma)_{1}\} \cup \{p_{k}(\sigma)_{1} : 2 \leq k \leq n\})$.
Por tanto

\begin{equation*}
  \sigma \in \bar{T}_{(\sigma)_{1}}^{1} \subseteq T^{1}
\end{equation*}

Sea $j < n - 1 (j \geq 1)$ y supongamos que el resultado es cierto para j.

Sea $\sigma \in T^{0}$ tal que $|A_{\sigma,n}| = n$. De la hip'otesis de inducci'on resulta que $\sigma \in T^{j}$. Luego

\begin{equation*}
  \sigma \in T^{j+1}_{(\sigma)_{j+1}}
\end{equation*}

y

\begin{equation*}
  \forall r (j + 2 \leq r \leq n \longrightarrow (\sigma)_{r} \neq (\sigma)_{j+1})
\end{equation*}

De donde se deduce que

\begin{equation*}
  \sigma \in \bar{T}_{(\sigma)_{j+1}}^{j+1} \subseteq T^{j+1}
\end{equation*}

\textbf{Corolario 1.4.} \textit{(Completitud del programa) Toda mol'ecula del tubo de ensayo inicial que codifica una
permutaci'on de orden n, est'a contenida en el tubo de salida}.

Por 'ultimo, basta tener presente que al finalizar la ejecuci'on del programa molecular, la f'ormula $\delta(n - 1)$ es
verdadera, y que el tubo de salida del programa es $T^{n-1}$.

\subsection{Problema del camino hamiltoniano en versi'on dirigida sin nodos distinguidos}

En este secci'on se muestra como abordar desde el punto de vista de la computaci'on molecular la resolubilidad
del problema del camino hamiltoniano en su versi'on digidia y sin nodos distinguidos.

El problema del camino hamiltoniano en su versi'on dirigida y sin nodos distinguidos consiste en
dado un grafo dirigido, determinar si existe un camino simple que pasa por todos los nodos del grafo. O lo
que es lo mismo, si el grafo posee un ciclo hamiltoniano.

Dicho de otro modo, un camino hamiltoniano es una sucesi'on ordenada de nodos donde estos
no se repiten y, adem'as, existen aristas que permiten llegar de uno a otro nodo de dicha sucesi'on.

\begin{figure}[h]
\centering
\includegraphics[scale=0.5]{hamiltoniano}
\caption{Ejemplo de camino hamiltoniano sobre un grafo.}
\end{figure}

Por tanto, dicho lo anterior, este problema presenta una conexi'on respeceto del problema anterior,
el problema de la generaci'on de permutaciones. Ya que, resolver este problema equivale a considerar un camino como
una sucesi'on de permutaciones, siempre y cuando, sea un camino v'alido del grafo $G$.

\subsubsection{Dise'no del programa molecular}

Para dar soluci'on a este problema en el modelo d'ebil de Amos, partimos de un $G = (V,E)$, tal que, $G$ es un grafo
dirigido con $V = \{1,...,n\}$ nodos.

Se debe definir en primer lugar el alfabeto $\sum = \{(p_{i},c_{j}) : 1 \leq i,j \leq n\}$. Donde, $p_{i}$ y $c_{j}$, son
dos oligos que codifican respectivamente la posici'on $i$-'esima del camino, y el nodo $j$. Es decir, el nodo $j$ est'a
en la posici'on $i$-'esima del camino.

Como punto de partida, se necesita un tubo de ensayo inicial, $T_{0}$. Este problema necesita de todas las permutaciones
de orden $n$, por tanto, el tubo de ensayo inicial es igual que el utilizado en el problema de la generaci'on de permutaciones
y una notaci'on parecida. Esto es:

\begin{equation*}
  T_{0} = \{\{ \sigma \in \sum_{}^n : \exists x_{1},..., \exists x_{n} (\sigma = (p_{1},x_{1}),
  (p_{2},x_{2}),..., (p_{n},x_{n})) \}\}
\end{equation*}

En este caso, la notaci'on es la siguiente: si se tiene $\sigma = p_{1}x_{1}p_{2}x_{2}...p_{n}x_{n} \in T_{0}$, entonces
para cada $r$ $(1 \leq r \leq n)$ se notar'a
$(\sigma)_{r} = x_{r}$ y $\sigma_{r} = ((\sigma)_{1},(\sigma)_{2},...,(\sigma)_{r})$. Es decir, si $\sigma$ codifica un
camino del grafo, entonces $x_{r}$, de $\sigma_{r} = (x_{1},x_{2},...,x_{r})$, ser'a el nodo $r$-'esimo del camino.

Hay que tener en cuenta que si $\sigma$ codifica una determinada permutaci'on de orden $n$ y, adem'as, codifica
un camino del grafo, 'este ser'a hamiltoniano.

Los pasos a seguir para resolver este problema, partiendo de un tubo inicial $T_{0}$ con todas las posibles
permutaciones de orden $n$, e iterando $n - 1$ veces, son los siguientes:

\begin{itemize}
    \item Se seleccionan las mol'eculas, $\sigma$, tales que $\sigma_{2}$ es un camino de $G$.
    \item De 'estas, se seleccionan las moleculas, $\sigma$, tales que $\sigma_{3}$ es un camino de $G$,
    verificando la condici'on $((\sigma)_{2},(\sigma)_{3} \in E)$.
\end{itemize}}

El algoritmo ser'a el siguiente:

\begin{algorithmic}
    \Require $T_{0}$
    \For {$i\leftarrow1$ in $n - 1$}
        \State $T_{0} \leftarrow quitar(T_{0}, \{jp_{i+1}k : (j,k) \notin E\})$
    \EndFor
    \State $seleccionar(T_{0})$
\end{algorithmic}

La complejidad de este algoritmo es $O(n)$, es decir, tiene un orden de complejidad lineal.

\subsubsection{Verificaci'on formal del programa molecular}

Para realizar la verificaci'on formal es necesario etiquetar cada uno de los tubos que se van a obtener
a los largo del algoritmo descrito anteriormente. Por tanto, el algoritmo va a ser reescrito de la
siguiente forma:

\begin{algorithmic}
    \Require $T_{0}$
    \For {$i\leftarrow1$ in $n - 1$}
        \State $T_{i} \leftarrow quitar(T_{i-1}, \{jp_{i+1}k : (j,k) \notin E\})$
    \EndFor
    \State $seleccionar(T_{n-1})$
\end{algorithmic}

Para poder realizar la verificaci'on formal se va considerar la siguiente f'ormula:

\begin{equation*}
  \theta(i) \equiv \forall \sigma \in T_{i-1} \forall r (1 \leq r \leq i \longrightarrow ((\sigma)_{r},(\sigma)_{r+1}) \in E)
\end{equation*}

Esta f'ormula, $\theta(i)$, viene a decir que para toda molecula $\sigma$ del tubo $T_{i-1}$ se verifica que
$\sigma_{i}$ es un camino del grafo $G$.

A continuaci'on, se van a exponer una serie de teoremas con los que se pretende realizar la verificaci'on formal,
tomando el algoritmo que se ha reescrito en este apartado.

\textbf{Teorema 2.1.} $\forall i (2 \leq i \leq n \longrightarrow \theta(i))$. Es decir, la f'ormula $\theta$ es un invariante del
bucle principal.

La demostraci'on, por inducci'on d'ebil sobre $i$ es: sea $\sigma \in T_{1}$. Puesto que
$T_{1} = quitar(T_{0}, {jp_{2}k : (j,k) \notin E})$, se deduce que $((\sigma)_{1},(\sigma)_{2}) \in E$.

Sea $i$ tal que $2 \leq i < n$ y supongamos cierto el resultado para $i$.

Sea $\sigma \in T^{i}$ y eniendo presente que $T_{i} = quitar(T_{i-1}, {jp_{i+1}k : (j,k) \notin E})$, resulta que
$\sigma \in T_{i-1}$ y $((\sigma)_{i},(\sigma)_{i+1}) \in E$. De la hipotesis de inducci'on se deduce que
$\forall r (1 \leq r < i \longrightarrow ((\sigma)_{r},(\sigma)_{r+1}) \in E)$. Por tanto, $\sigma_{i+1}$ es un camino del grafo $G$.

\textbf{Corolario 2.2.} \textit{(Correcci'on del programa) Toda mol'ecula del tubo de salida codifica un camino hamiltoniano
del grafo G}.

La demostraci'on es, sea $\sigma \in T_{n-1}$. Como la f'ormula $\theta(n)$ es verdadera resulta que
$\forall r (1 \leq r < n \longrightarrow ((\sigma)_{r},(\sigma)_{r+1}) \in E)$. Por tanto, $\sigma_{n}$ es un camino de $G$.
Teniendo presente que la mol'ecula $\sigma$ codifica una permutaci'on de orden $n$, concluimos que $\sigma$ codifica
un camino hamiltoniano del grafo $G$.

Para establecer la completitud del programa molecular dise'nado, consideremos la siguiente f'ormula:

\begin{equation*}
  \delta(i) \equiv \forall \sigma \in T_{0} ([\forall r (1 \leq r < n \longrightarrow ((\sigma)_{r},(\sigma)_{r+1})
   \in E)] \longrightarrow \sigma \in T_{i-1})
\end{equation*}

Es decir, la formula $\delta(i)$ expresa que toda molecula del tubo inicial que codifica un camino hamiltoniano
de $G$ pertenece al tubo $T_{i-1}$.

\textbf{Teorema 2.3.} $\forall i (2 \leq i \leq n \longrightarrow \delta(i))$. Es decir, la f'ormula $\delta$ es un invariante del
bucle principal.

La demostraci'on, por inducci'on d'ebil sobre $i$ es: sea $\sigma \in T_{0}$ tal que $\sigma$ codifica un camino
hamiltoniano de $G$. Entonces $\forall r (1 \leq r \leq n \longrightarrow ((\sigma)_{r},(\sigma)_{r+1}) \in E)$. Luego,
$\sigma \in quitar(T_{0}, \{jp_{2}k : (j,k) \notin E\}) = T_{1}$.

Sea $i$ tal que $2 \leq i < n$ y supongamos cierto el resultado para $i$.

Sea $\sigma \in T_{0}$ tal que $\sigma$ codifica un camino hamiltoniano de $G$. Por hipotesis de inducci'on se tiene que
$\sigma \in T_{i-1}$. Luego, $\sigma \in quitar(T_{i-1},\{jp_{i+1}k : (j,k) \notin E\}) = T_{i}$.

\textbf{Corolario 2.4.} \textit{(Completitud del programa) Toda mol'ecula del tubo de ensayo inicial codifica un camino
 hamiltoniano de G, est'a en el tubo de salida}.

Para la demostraci'on basta tener presente que la f'ormula $\delta(n)$ es verdadera y que el tubo de salida del
programa es $T_{n-1}$.

% bibliography
\printbibliography

\end{document}