diff --git a/ej-csr/memoria.tex b/ej-csr/memoria.tex index 52bb895..4eca552 100644 --- a/ej-csr/memoria.tex +++ b/ej-csr/memoria.tex @@ -34,6 +34,8 @@ Como la suma presenta la propiedad conmutativa para la suma ($+$) en la regla 7, Como los pares críticos tienen todos como posición $p$ la raíz o el primer argumento de la suma, vamos a seleccionar $\mu_{151}(+) = \emptyset$, por lo tanto $\mu_{151}(*) = \{1\}$ (también se podría haber escogido $\emptyset$). +Respecto a la propiedad $\mu$-LHRV, no hay variables activas en el lado izquierdo de ninguna regla, por lo que se cumple `por vacuidad'. + \subsection{Pares $\mu$-críticos} \begin{figure}[h] @@ -128,6 +130,8 @@ Nota: en esta sección, se utilizará $\vee$ para representar la función ``or'' Del mismo modo que en $\mathcal{R}_{151}$, la función \texttt{or} presenta la propiedad conmutativa, por lo que $\mu_{153}(or)=\emptyset \vee \{1,2\}$. Para que la $\mu$-convergencia no sea idéntica a la convergencia de $\mathcal{R}_{153}$, vamos a escoger $\emptyset$. +La propiedad $\mu$-LHRV se cumple, puesto que que no hay ninguna variable activa en el lado izquierdo de ninguna regla. + \subsection{Pares $\mu$-críticos} Los pares críticos se muestran en la figura \ref{pares153}, y de nuevo descartamos aquellos que $l|_\wedge=or$ y $p \neq \wedge$. Todos los pares son convergentes, pero sólo son $\mu$-críticos del 1 al 4 y el 8. @@ -184,11 +188,43 @@ n & $\sigma(l)[\sigma(r')]_p$ & $\sigma(r)$ \\ \hline \label{mupares153} \end{figure} -\section{SRT $\mathcal{R}_{i}$} -\subsection{Función de reemplazamiento $\mu_{i}$} +\section{SRT $\mathcal{R}_{173}$} +\begin{lstlisting} +(VAR x y) +(RULES + max(x,0) -> x + max(0,y) -> y + max(s(x),s(y)) -> s(max(x,y)) + max(x,y) -> max(y,x) + max(x,x) -> x +) +\end{lstlisting} +\subsection{Función de reemplazamiento $\mu_{173}$} +De nuevo se presenta la propiedad conmutativa para el operador \texttt{max}. En esta ocasión también vamos a escoger $\mu_{173}(max)=\emptyset$. La propiedad $\mu$-LHRV se cumple, puesto que no existen posiciones activas en la parte izquierda de ninguna regla. \subsection{Pares $\mu$-críticos} +\begin{figure}[h] +\begin{center} +\begin{tabular}{|l|c|c|c|} +\hline +$n$ & $l \rightarrow r$ & $l' \rightarrow r'$ & $p$ \\ \hline +1 & $\texttt{max}(x, 0) \rightarrow x$ & $\texttt{max}(0,y') \rightarrow y'$ & $\wedge$ \\ +2 & $\texttt{max}(x,0) \rightarrow x$ & $\texttt{max}(x',y') \rightarrow \texttt{max}(y',x')$ & $\wedge$ \\ +3 & $\texttt{max}(0,y) \rightarrow y$ & $\texttt{max}(x',y') \rightarrow \texttt{max}(y',x')$ & $\wedge$ \\ +4 & $\texttt{max}(0,y) \rightarrow y$ & $\texttt{max}(x',x') \rightarrow x'$ & $\wedge$ \\ +5 & $\texttt{max}(s(x), s(y)) \rightarrow s(\texttt{max}(x,y))$ & $\texttt{max}(x',y') \rightarrow \texttt{max}(y',x')$ & $\wedge$ \\ +6 & $\texttt{max}(x,y) \rightarrow \texttt{max}(y,x)$ & $\texttt{max}(x',x') \rightarrow x'$ & $\wedge$ \\ +7 & $\texttt{max}(x,x) \rightarrow x$ & $\texttt{max}(x', 0) \rightarrow x'$ & $\wedge$ \\ \hline +\end{tabular} +\end{center} +\caption{Reglas escogidas para los pares críticos de $\mathcal{R}_{173}$} +\label{pares173} +\end{figure} + +Como todos los pares críticos tienen como posición $p=\wedge$, todos son pares $\mu$-críticos. + \subsection{$\mu$-confluencia} + \section{SRT $\mathcal{R}_{i}$} \subsection{Función de reemplazamiento $\mu_{i}$} \subsection{Pares $\mu$-críticos}