FLA/tarea5/memoria_corregida.tex
Carlos Galindo 2300df106d
Tarea 5
2018-11-12 18:52:10 +01:00

63 lines
No EOL
1.9 KiB
TeX

\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}