\documentclass[a4paper]{article}

\usepackage[utf8]{inputenc}
\usepackage[spanish]{babel}
\usepackage{amsmath}
\usepackage{amssymb}

\author{Carlos S. Galindo Jiménez}
\title{FLA - Tarea 5}

\begin{document}
\maketitle
Las reglas que componen $E$ son las siguientes:

\begin{align}
&f(0) \rightarrow 0 \\
&g(0) \rightarrow 0 \\
&f(g(X)) \rightarrow g(X) \\
&(X = X) \rightarrow \texttt{True}
\end{align}

Para diferenciar las variables, a cada nivel de profundidad cada variable $A$ se renombra a $A_i$, donde $i$ es el nivel actual de profundidad. El término inicial es:

$$f(Z)=Z$$

Desde aquí se pueden realizar varias combinaciones, con la siguiente nomenclatura: $p$ es la posición, $E_i: l_i \rightarrow r_i$ es la regla i-ésima y $\sigma$ es el unificador mediante el cual el término original $t$ se convierte  en $s=(t[r_i]_p)\sigma$. $\sigma$ es el mgu de $t|_p$ y $l_i$. La columna ``Hoja'' indica $\checkmark$ si es hoja y resulta en \texttt{True}, $\times$ si falla, `-' si tiene hijos y `$\sim$' si tiene hijos que resultan en \texttt{True} pero su exploración es simplemente reescritura.

\begin{center}
\begin{tabular}{| l | l | l | l | c | c |} \hline
n & i & p & $\sigma$ & $s$ & Hoja \\ \hline
1 & 1 & 1 & $Z/0$ & $0 = 0$ & $\checkmark$ \\
2 & 1 & 1.1 & $Z/f(0)$ & $f(0) = f(0)$ & $\checkmark$ \\
3 & 1 & 2 & $Z/f(0)$ & $f(0) = 0$ & $\sim$ \\ \hline
4 & 2 & 1 & $\nexists$ & - & $\times$ \\
5 & 2 & 1.1 & $Z/g(0)$ & $f(0)=g(0)$ & $\sim$ \\
6 & 2 & 2 & $Z/g(0)$ & $f(g(0))=0$ & $\sim$ \\ \hline
7 & 3 & 1 & $Z/g(X_1)$ & $g(X_1)=g(X_1)$ & $\checkmark$ \\
8 & 3 & 1.1 & $Z/f(g(X_1))$ & $f(g(X_1))=f(g(X_1))$ & $\checkmark$ \\
9 & 3 & 2 & $Z/f(g(X_1))$ & $f(f(g(X_1))) = g(X_1)$ & - \\ \hline
\end{tabular}
\end{center}

Una vez desarrollado el primer nivel, todas aquellos estados que no hayan concluido de forma positiva o negativa tienen que sufrir el mismo procedimiento. Para simplificar el árbol, vamos a simplificar todos aquellos que no tengan variables en un solo paso, por lo que el número 3 sería $f(0)=0 \rightarrow 0=0 \rightarrow \texttt{True}$, y del mismo modo lo serían el 5 y 6. En las siguientes tablas vamos a omitir las posiciones para las cuales no existe un unificador $\sigma$ válido.

En las siguientes tablas vamos a explorar las posibilidades que ofrece el caso 9. La nomenclatura para los casos hijos será $9.i$, para cada hijo de 9, y así sucesivamente.

$$f(f(g(X_1)))=g(X_1)$$

\begin{center}
\begin{tabular}{| l | l | l | l | c | c |} \hline
n & i & p & $\sigma$ & $s$ & Hoja \\ \hline
9.1 & 1 & 1.1.1.1 & $X_1/f(0)$ & $f(f(g(0)))=g(f(0))$ & $\sim$ \\
9.2 & 1 & 2.1 & $X_1/f(0)$ & $f(f(g(f(0))))=g(0)$ & $\sim$ \\ \hline
9.3 & 2 & 1.1.1 & $X_1/0$ & $f(f(0))=g(0)$ & $\sim$ \\
9.4 & 2 & 1.1.1.1 & $X_1/g(0)$ & $f(f(g(0)))=g(g(0))$ & $\sim$ \\
9.5 & 2 & 2 & $X_1/0$ & $f(f(g(0)))=0$ & $\sim$ \\
9.6 & 2 & 2.1 & $X_1/g(0)$ & $f(f(g(g(0))))=g(0)$ & $\sim$ \\ \hline
9.7 & 3 & 1.1 & $X_1/X_2$ & $f(g(X_2))=g(X_2)$ & - \\
9.8 & 3 & 1.1.1.1 & $X_1/f(g(X_2))$ & $f(f(g(g(X_2))))=g(f(g(X_2)))$ & - \\
9.9 & 3 & 2.1 & $X_1/f(g(X_2))$ & $f(f(g(f(g(X_2)))))=g(g(X_2))$ & - \\ \hline
\end{tabular}
\end{center}

Para el tercer nivel, la búsqueda se ramifica aún más, puesto que 9.7, 9.8 y 9.9 pueden continuar:

\begin{center}
\begin{tabular}{| l | l | l | l | c | c |} \hline
n & i & p & $\sigma$ & $s$ & Hoja \\ \hline
9.7.1 & 1 & 1.1.1 & $X_2/f(0)$ & $f(g(0))=g(f(0))$ & $\sim$ \\
9.7.2 & 1 & 2.1 & $X_2/f(0)$ & $f(g(f(0)))=g(0)$ & $\sim$ \\ \hline
9.7.3 & 2 & 1.1 & $X_2/0$ & $f(0)=g(0)$ & $\sim$ \\
9.7.4 & 2 & 1.1.1 & $X_2/g(0)$ & $f(g(0))=g(g(0))$ & $\sim$ \\
9.7.5 & 2 & 2 & $X_2/0$ & $f(g(0))=0$ & $\sim$ \\
9.7.6 & 2 & 2.1 & $X_2/g(0)$ & $f(g(g(0)))=g(0)$ & $\sim$ \\ \hline
9.7.7 & 3 & 1 & $X_2/X_3$ & $g(X_3)=g(X_3)$ & $\checkmark$ \\
9.7.8 & 3 & 1.1.1 & $X_2/f(g(X_3))$ & $f(g(g(X_3)))=g(f(g(X_3)))$ & - \\
9.7.9 & 3 & 2.1 & $X_2/f(g(X_3))$ & $f(g(f(g(X_3))))=g(g(X_3))$ & - \\ \hline
9.8.1 & 1 & 1.1.1.1.1 & $X_2/f(0)$ & $f(f(g(g(0))))=g(f(g(f(0))))$ & $\sim$ \\
9.8.2 & 1 & 2.1.1.1 & $X_2/f(0)$ & $f(f(g(g(f(0)))))=g(f(g(0)))$ & $\sim$ \\ \hline
9.8.3 & 2 & 1.1.1.1 & $X_2/0$ & $f(f(g(0)))=g(f(g(0)))$ & $\sim$ \\
9.8.4 & 2 & 1.1.1.1.1 & $X_2/g(0)$ & $f(f(g(0)))=g(f(g(g(0))))$ & $\sim$ \\
9.8.5 & 2 & 2.1.1 & $X_2/0$ & $f(f(g(g(0))))=g(f(0))$ & $\sim$ \\
9.8.6 & 2 & 2.1.1.1 & $X_2/g(0)$ & $f(f(g(g(g(0)))))=g(f(0))$ & $\sim$ \\ \hline
9.8.7 & 3 & 1.1 & $X/g(X_3),X_2/X_3$ & $f(g(g(X_3)))=g(f(g(X_3)))$ & - \\
9.8.8 & 3 & 1.1.1.1.1 & $X_2/f(g(X_3))$ & $f(f(g(g(g(X_3)))))=g(f(g(f(g(X_3)))))$ & - \\
9.8.9 & 3 & 2.1 & $X_2/X_3$ & $f(f(g(g(X_3))))=g(g(X_3))$ & - \\
9.8.10 & 3 & 2.1.1.1 & $X_2/f(g(X_3))$ & $f(f(g(g(f(g(X_3))))))=g(g(X_3))$ & - \\ \hline
\end{tabular}
\begin{tabular}{| l | l | l | l | c | c |} \hline
9.9.1 & 1 & 1.1.1.1.1.1 & $X_2/f(0)$ & $f(f(g(f(g(0)))))=g(g(f(0)))$ & $\sim$ \\
9.9.2 & 1 & 2.1.1 & $X_2/f(0)$ & $f(f(g(f(g(f(0))))))=g(g(0))$ & $\sim$ \\ \hline
9.9.3 & 2 & 1.1.1.1.1 & $X_2/0$ & $f(f(g(f(0))))=g(g(0))$ & $\sim$ \\
9.9.4 & 2 & 1.1.1.1.1.1 & $X_2/g(0)$ & $f(f(g(f(0))))=g(g(g(0)))$ & $\sim$ \\
9.9.5 & 2 & 2.1 & $X_2/0$ & $f(f(g(f(g(0)))))=g(0)$ & $\sim$ \\
9.9.6 & 2 & 2.1.1 & $X_2/g(0)$ & $f(f(g(f(g(g(0))))))=g(g(0))$ & $\sim$ \\ \hline
9.9.7 & 3 & 1.1 & $X/f(g(X_3)),X_2/X_3$ & $f(g(f(g(X_3))))=g(g(X_3))$ & - \\
9.9.8 & 3 & 1.1.1.1 & $X_2/X_3$ & $f(f(g(g(X_3))))=g(g(X_3))$ & - \\
9.9.9 & 3 & 1.1.1.1.1.1 & $X_2/f(g(X_3))$ & $f(f(g(f(g(g(X_3))))))=g(g(f(g(X_3))))$ & - \\
9.9.10 & 3 & 2.1.1 & $X_2/f(g(X_3))$ & $f(f(g(f(g(f(g(X_3)))))))=g(g(g(X_3)))$ & - \\ \hline
\end{tabular}
\end{center}

Tras completar la tercera expansión, tenemos 10 ecuaciones, correspondientes a las generadas mediante la regla 3. Como la expansión no tiene fin, vamos a realizar una última expansión, considerando sólo la regla de reescritura 3.

\begin{center}
\begin{tabular}{| l | l | c | c |} \hline
n & p & $s$ & Hoja \\ \hline
9.7.8.1 & 1 & $g(g(X_4))=g(f(g(X_4)))$ & - \\
9.7.8.2 & 1.1.1.1 & $f(g(g(g(X_4))))=g(f(g(f(g(X_4)))))$ & - \\
9.7.8.3 & 2.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
9.7.8.4 & 2.1.1.1 & $f(g(g(f(g(X_4)))))=g(f(g(g(X_4))))$ & - \\ \hline
9.7.9.1 & 1 & $g(f(g(X_4)))=g(g(X_4))$ & - \\
9.7.9.2 & 1.1.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
9.7.9.3 & 1.1.1.1.1 & $f(g(f(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
9.7.9.4 & 2.1.1 & $f(g(f(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline \hline
9.8.7.1 & 1 & $g(g(X_4))=g(f(g(X_4)))$ & - \\
9.8.7.2 & 1.1.1.1 & $(f(g(g(g(X_4)))))=g(f(g(f(g(X_4)))))$ & - \\
9.8.7.3 & 2.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
9.8.7.4 & 2.1.1.1 & $f(g(g(f(g(X_4)))))=g(f(g(g(X_4))))$ & - \\ \hline
9.8.8.1 & 1.1 & $f(g(g(g(X_4))))=g(f(g(f(g(X_4)))))$ & - \\
9.8.8.2 & 1.1.1.1.1.1 & $f(f(g(g(g(g(X_4))))))=g(f(g(f(g(f(g(X_4)))))))$ & - \\
9.8.8.3 & 2.1 & $f(f(g(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
9.8.8.4 & 2.1.1.1 & $f(f(g(g(g(X_4)))))=g(f(g(g(X_4))))$ & - \\
9.8.8.5 & 2.1.1.1.1.1 & $f(f(g(g(g(f(g(X_4)))))))=g(f(g(f(g(g(X_4))))))$ & - \\ \hline
9.8.9.1 & 1.1 & $f(g(g(g(X_4))))=g(g(X_4))$ & - \\
9.8.9.2 & 1.1.1.1.1 & $f(f(g(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
9.8.9.3 & 2.1.1 & $f(f(g(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline
9.8.10.1 & 1.1 & $f(g^3(f(g(X_4))))=g(g(X_4))$ & - \\
9.8.10.2 & 1.1.1.1.1 & $f(f(g^3(X_4)))=g(g(X_4))$ & - \\
9.8.10.3 & 1.1.1.1.1.1.1 & $f(f(g(g(f(g(g(X_4)))))))=g(g(f(g(X_4))))$ & - \\
9.8.10.4 & 2.1.1 & $f(f(g(g(f(g(f(g(X_4))))))))=g(g(g(X_4)))$ & - \\ \hline \hline
9.9.7.1 & 1 & $g(f(g(X_4)))=g(g(X_4))$ & - \\
9.9.7.2 & 1.1.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
9.9.7.3 & 1.1.1.1.1 & $f(g(f(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
9.9.7.4 & 2.1.1 & $f(g(f(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline
9.9.8.1 & 1.1 & $f(g(g(X_4)))=g(g(X_4))$ & - \\
\end{tabular}
\begin{tabular}{| l | l | c | c |}
9.9.8.2 & 1.1.1.1.1 & $f(f(g^3(X_4)))=g(g(f(g(X_4))))$ & - \\
9.9.8.3 & 2.1.1 & $f(f(g(g(f(g(X_4))))))=g(g(g(X_4)))$ & - \\ \hline
9.9.9.1 & 1.1 & $f(g(f(g(g(X_4)))))=g(g(f(g(X_4))))$ & - \\
9.9.9.2 & 1.1.1.1 & $f(f(g^3(X_4)))=g(g(f(g(X_4))))$ & - \\
9.9.9.3 & 1.1.1.1.1.1.1 & $f(f(g(f(g^3(X_4)))))=g(g(f(g(f(g(X_4))))))$ & - \\
9.9.9.4 & 2.1.1 & $f(f(g(f(g(g(X_4))))))=g^3(X_4)$ & - \\
9.9.9.5 & 2.1.1.1.1 & $f(f(g(f(g(g(f(g(X_4))))))))=g(g(f(g(g(X_4)))))$ & - \\ \hline
9.9.10.1 & 1.1 & $f(g(f(g(f(g(X_4))))))=g^3(X_4)$ & - \\
9.9.10.2 & 1.1.1.1 & $f(g(g(f(g(X_4)))))=g^3(X_4)$ & - \\
9.9.10.3 & 1.1.1.1.1.1 & $f(f(g(f(g(g(X_4))))))=g^3(X_4)$ & - \\
9.9.10.4 & 1.1.1.1.1.1.1.1 & $f(f(g(f(g(f(g(g(X_4))))))))=g^3(f(g(X_4)))$ & - \\
9.9.10.5 & 2.1.1.1 & $f(f(g(f(g(f(g(f(g(X_4)))))))))=g^4(X_4)$ & - \\ \hline
\end{tabular}
\end{center}

Como se puede observar, se van generando expresiones más complejas, a la vez que se van generanndo otras más simples, que en dos o tres niveles se instanciarán a $X_i/0$, $X_i/f(0)$ o $X_i/g(0)$ y generarán otra hoja con resultado \texttt{True}. Este ciclo continuará de forma infinita, y posiblemente a estas alturas se pudiera simplificar buscando repeticiones.
\end{document}