From 2300df106d2fdd51b293d547ddee3f4daf9d582f Mon Sep 17 00:00:00 2001 From: Carlos Galindo Date: Mon, 12 Nov 2018 18:52:10 +0100 Subject: [PATCH] Tarea 5 --- tarea5/memoria.tex | 155 +++++++++++++++++++++++++++++++++++ tarea5/memoria_corregida.tex | 63 ++++++++++++++ 2 files changed, 218 insertions(+) create mode 100644 tarea5/memoria.tex create mode 100644 tarea5/memoria_corregida.tex diff --git a/tarea5/memoria.tex b/tarea5/memoria.tex new file mode 100644 index 0000000..f7c9617 --- /dev/null +++ b/tarea5/memoria.tex @@ -0,0 +1,155 @@ +\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} \ No newline at end of file diff --git a/tarea5/memoria_corregida.tex b/tarea5/memoria_corregida.tex new file mode 100644 index 0000000..c5ac9ad --- /dev/null +++ b/tarea5/memoria_corregida.tex @@ -0,0 +1,63 @@ +\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: +\begin{itemize} + \item $t\rightsquigarrow s$ es un paso de narrowing + \item $p$ es la posición del redex, y no puede ser una variable + \item $E_i: l_i \rightarrow r_i$ es la regla i-ésima + \item $\sigma$ es el $mgu(t|_p,l_i)$ +\end{itemize} + +$$s=(t[r_i]_p)\sigma$$ + +% TODO: p no puede ser la de una variable +% TODO: un final tiene que acabar en true, no en A = A +\begin{center} +\begin{tabular}{| l | l | l | l | c |} \hline +n & i & p & $\sigma$ & $s$ \\ \hline +1 & 1 & 1 & $Z/0$ & $0 = 0$ \\ +2 & 2 & 1 & $\nexists$ & - \\ +3 & 3 & 1 & $Z/g(X_1)$ & $g(X_1)=g(X_1)$ \\ \hline \hline +1.1 & 4 & $\wedge$ & $X/0$ & \texttt{True} \\ +3.1 & 4 & $\wedge$ & $X/g(X_1)$ & \texttt{True} \\ +3.2 & 2 & 1 & $X_1/0$ & $0=g(0)$ \\ +3.3 & 2 & 2 & $X_1/0$ & $g(0)=0$ \\ \hline \hline +3.2.1 & 2 & 2 & $\emptyset$ & $0=0$ \\ +3.2.1.1 & 4 & $\wedge$ & $X/0$ & \texttt{True} \\ +3.3.1 & 2 & 1 & $\emptyset$ & $0=0$ \\ +3.3.1.1 & 4 & $\wedge$ & $X/0$ & \texttt{True} \\ \hline +\end{tabular} +\end{center} + +De los 4 finales obtenidos (1.1, 3.1, 3.2.1.1 y 3.3.1.1) podemos obtener los cuatro unificadores: + +\begin{description} + \item [1.1] $\sigma_1=\{Z/0\}$ + \item [3.1] $\sigma_2=\{Z/g(X_1)\}$ + \item [3.2.1.1] $\sigma_3=\{Z/g(0)\}$ + \item [3.3.1.1] $\sigma_4=\{Z/g(0)\}$ +\end{description} +\end{document} \ No newline at end of file