Tarea 5
This commit is contained in:
Carlos Galindo
parent
82980f85d3
commit
2300df106d
GPG key ID:
83E68706DEE119A3
2 changed files with 218 additions and 0 deletions
155
tarea5/memoria.tex
Normal file
155
tarea5/memoria.tex
Normal file
|
|
@ -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}
|
||||
63
tarea5/memoria_corregida.tex
Normal file
63
tarea5/memoria_corregida.tex
Normal file
|
|
@ -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}
|
||||
Loading…
Reference in a new issue