diff --git a/ej-csr/memoria.tex b/ej-csr/memoria.tex index 4eca552..0db7b2f 100644 --- a/ej-csr/memoria.tex +++ b/ej-csr/memoria.tex @@ -224,15 +224,35 @@ Como todos los pares críticos tienen como posición $p=\wedge$, todos son pares \subsection{$\mu$-confluencia} +De los pares $\mu$-críticos, el 1, 4 y 7 son triviales, por lo que $\mathcal{R}_{173}$ no es $\mu$-ortogonal. El resto de los pares son $\mu$-convergentes: -\section{SRT $\mathcal{R}_{i}$} -\subsection{Función de reemplazamiento $\mu_{i}$} -\subsection{Pares $\mu$-críticos} -\subsection{$\mu$-confluencia} +\begin{enumerate} + \item[2.] $\texttt{max}(0,x) \hookrightarrow x$ + \item[3.] $\texttt{max}(y,0) \hookrightarrow y$ + \item[5.] $\texttt{max}(s(y),s(x)) \hookrightarrow s(\texttt{max}(y,x)) \hookleftarrow s(\texttt{max}(x,y))$ + \item[6.] $x \hookleftarrow \texttt{max}(x,x)$ +\end{enumerate} -\section{SRT $\mathcal{R}_{i}$} -\subsection{Función de reemplazamiento $\mu_{i}$} +Por tanto ya sólo quedaría comprobar la $\mu$-terminación de $\mathcal{R}_{173}$ en la herramienta \textsc{MuTerm}, que indica que no es $\mu$-terminante. Por lo tanto, $\mathcal{R}_{173}$ es localmente $\mu$-confluente. + +\section{SRT $\mathcal{R}_{163}$} +\begin{lstlisting} +(VAR x y z) +(RULES + +(+(x, y), z) -> +(x, +(y, z)) + +(x, +(y, z)) -> +(+(x, y), z) +) +\end{lstlisting} +\subsection{Función de reemplazamiento $\mu_{163}$} +Este SRT ha sido escogido por ser uno de los pocos en el rango 151-175 que no define la propiedad conmutativa para sus operaciones. Desafortunadamente, define la propiedad asociativa para la operación $+$, lo cual limita de forma similar las opciones disponibles de $\mu_{163}(+)$. Para intentar obtener un SRT que NO sea $\mu$-confluente, vamos a limitar $\mu_{163}(+)$ a $\emptyset$. \subsection{Pares $\mu$-críticos} +Puesto que $\mathcal{R}_{163}$ se compone únicamente de 2 reglas, sólo existe una posibilidad dada la función $\mu_{163}$ escogida. El par crítico resultante es: +$$(x' + (y' + y)) + z, (x'+y')+(y+z)$$ \subsection{$\mu$-confluencia} +La $\mu$-confluencia de nuevo requiere de la $\mu$-congruencia del par $\mu$-crítico y la $\mu$-terminación del sistema de reescritura. + +Respecto a la $\mu$-congruencia del par $\mu$-crítico, no se puede llegar a un término común $u$ que pueda ser $\mu$-derivado de $l$ y $r$ ($l \hookrightarrow^* u \wedge r \hookrightarrow^* u$), puesto que $r$ no es derivable y $l$ sólo se podría derivar a $x' + ((y' + y) + z)$. + +Por tanto, podemos determinar que el sistema de reescritura $\mathcal{R}_{163}$ no es $\mu$-confluente. \end{document} \ No newline at end of file