258 lines
No EOL
12 KiB
TeX
258 lines
No EOL
12 KiB
TeX
\documentclass{article}
|
|
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage{listings}
|
|
\usepackage[spanish]{babel}
|
|
\usepackage{url}
|
|
\usepackage{amssymb}
|
|
\usepackage{amsmath}
|
|
|
|
\title{Confluencia en CSR\\Trabajo práctico}
|
|
\author{Carlos S. Galindo Jiménez}
|
|
|
|
\begin{document}
|
|
\maketitle
|
|
|
|
\section{SRT $\mathcal{R}_{151}$}
|
|
\begin{lstlisting}
|
|
(VAR x y z)
|
|
(RULES
|
|
+(x,0) -> x # 1
|
|
+(x,s(y)) -> s(+(x,y)) # 2
|
|
+(0,y) -> y # 3
|
|
+(s(x),y) -> s(+(x,y)) # 4
|
|
*(k,0) -> 0 # 5
|
|
*(k,s(y)) -> +(k,*(k,y)) # 6
|
|
+(x,y) -> +(y,x) # 7
|
|
+(+(x,y),z) -> +(x,+(y,z)) # 8
|
|
)
|
|
\end{lstlisting}
|
|
|
|
\subsection{Función de reemplazamiento $\mu_{151}$}
|
|
|
|
Como la suma presenta la propiedad conmutativa para la suma ($+$) en la regla 7, para cumplir la propiedad $\mu$-LHRV, $\mu_{151}(+)$ debe ser o $\{1,2\}$ o $\emptyset$, puesto que si se escogiera sólo una de las dos posiciones, una de las variables estaría activa en la parte izquierda de la regla, pero no en la parte derecha. En el primer caso no hay restricciones para $\mu_{151}(*)$, pero en el segundo, dada la regla 6, $2 \notin \mu_{151}(*)$, porque $y$ estaría activo en la parte izquierda, pero inactivo en la parte derecha de la regla.
|
|
|
|
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]
|
|
\begin{center}
|
|
\begin{tabular}{| c | c | c |}
|
|
\hline
|
|
$l \rightarrow r$ & $l' \rightarrow r'$ & $p$ \\ \hline
|
|
$x + 0 \rightarrow x$ & $0 + y' \rightarrow y'$ & $\wedge$\\
|
|
$x + 0 \rightarrow x$ & $s(x') + y' \rightarrow s(x' + y')$ & $\wedge$\\
|
|
$x + 0 \rightarrow x$ & $x' + y' \rightarrow y' + x'$ & $\wedge$\\
|
|
$x + 0 \rightarrow x$ & $ (x' + y') + z' \rightarrow x' + (y' + z')$ & $\wedge$\\
|
|
$x + s(y) \rightarrow s(x + y)$ & $0 + y'\rightarrow y'$ & $\wedge$\\
|
|
$x + s(y)\rightarrow s(x + y)$ & $s(x') + y\rightarrow s(x' + y')$ & $\wedge$\\
|
|
$x + s(y)\rightarrow s(x + y)$ & $x' + y' \rightarrow y' + x'$ & $\wedge$\\
|
|
$x + s(y)\rightarrow s(x + y)$ & $(x' + y') + z' \rightarrow x' + (y' + z')$ & $\wedge$\\
|
|
$0+y\rightarrow y$ & $x'+y'\rightarrow y'+x'$ & $\wedge$\\
|
|
$s(x)+y\rightarrow s(x+y)$ & $x'+y'\rightarrow y'+x'$ & $\wedge$\\
|
|
$x+y\rightarrow y+x$ & $(x' + y') + z' \rightarrow x' + (y' + z')$ & $\wedge$\\
|
|
\hline
|
|
$(x+y)+z\rightarrow x+(y+z)$ & $x'+0\rightarrow x'$ & 1\\
|
|
$(x+y)+z\rightarrow x+(y+z)$ & $x'+s(y)\rightarrow s(x'+y)$ & 1\\
|
|
$(x+y)+z\rightarrow x+(y+z)$ & $0+y'\rightarrow y'$ & 1\\
|
|
$(x+y)+z\rightarrow x+(y+z)$ & $s(x')+y'\rightarrow s(x'+y')$ & 1 \\
|
|
$(x+y)+z\rightarrow x+(y+z)$ & $x'+y'\rightarrow y'+x'$ & 1\\
|
|
$(x+y)+z\rightarrow x+(y+z)$ & $(x'+y')+z' \rightarrow x'+(y'+z')$ & 1\\ \hline
|
|
\end{tabular}
|
|
\end{center}
|
|
\caption{Parejas de reglas que dan lugar a pares críticos de $\mathcal{R}_{151}$}
|
|
\label{pares151}
|
|
\end{figure}
|
|
|
|
De los pares críticos de la figura \ref{pares151}, hay que descartar todos aquellos cuyo elemento $\wedge$ sea la suma y $p\neq \wedge$. Los pares restantes son el conjunto de los pares $\mu$-críticos. Todos ellos son convergentes, excepto el primero, que es trivial (0, 0).
|
|
|
|
\subsection{$\mu$-confluencia}
|
|
|
|
\begin{figure}[h]
|
|
\begin{center}
|
|
\begin{tabular}{r|c|c}
|
|
n & $\sigma(l)[\sigma(r')]_p$ & $\sigma(r)$ \\ \hline
|
|
1 & $0$ & $0$ \\
|
|
2 & $s(x' + 0)$ & $s(x')$ \\
|
|
3 & $0 + x$ & $x$ \\
|
|
4 & $x'+(y'+0)$ & $x' + y'$ \\
|
|
5 & $s(y)$ & $s(0 + y)$ \\
|
|
6 & $s(x' + s(y))$ & $s(s(x') + y)$ \\
|
|
7 & $s(y)+x$ & $s(x+y)$ \\
|
|
8 & $x'+(y'+s(y))$ & $s((x'+y')+y)$ \\
|
|
9 & $y+0$ & $y$ \\
|
|
10& $y+s(x)$ & $s(x+y)$ \\
|
|
11& $x'+(y'+y)$ & $y+(x'+y')$ \\ \hline
|
|
\end{tabular}
|
|
\end{center}
|
|
\caption{Pares $\mu$-críticos de $\mathcal{R}_{151}$}
|
|
\label{mupares151}
|
|
\end{figure}
|
|
|
|
$\mathcal{R}_{151}$ no es ortogonal, puesto que posee pares $\mu$-críticos no triviales (ver figura \ref{mupares151}). Por lo tanto habría que probar la $\mu$-confluencia a través de la $\mu$-convergencia de los pares $\mu$-críticos y la $\mu$-terminación de $\mathcal{R}_{151}$.
|
|
|
|
Tal y como se indica en la proposición 1, un SRT localmente $\mu$-confluente y $\mu$-terminante es $\mu$-confluente. En este caso, $\mathcal{R}_{151}$ no es $\mu$-terminante (comprobado con la herramienta \textsc{MuTerm}), por lo que es necesario analizar la $\mu$-convergencia de cada uno de los pares $\mu$-críticos para ver si puede ser localmente $\mu$-confluente.
|
|
|
|
\begin{enumerate}
|
|
\item Trivial
|
|
\item $s(x'+0) \hookrightarrow s(x')$, $\mu$-convergente
|
|
\item $0+x \hookrightarrow x$, $\mu$-convergente
|
|
\item $x'+(y'+0) \hookrightarrow x'+y'$, $\mu$-convergente
|
|
\item $s(y) \hookleftarrow s(0+y)$, $\mu$-convergente
|
|
\item $s(x'+s(y)) \hookrightarrow s(s(x'+y)) \hookleftarrow s(s(x')+y)$, $\mu$-convergente
|
|
\item $s(y)+x \hookrightarrow s(y+x) \hookrightarrow s(x+y)$, $\mu$-convergente
|
|
\item $x'+(y'+s(y)) \hookrightarrow (x'+y')+s(y) \hookrightarrow s((x'+y')+y)$, $\mu$-convergente
|
|
\item $y+0 \hookrightarrow y$, $\mu$-convergente
|
|
\item $y+s(x) \hookrightarrow s(x)+y \hookrightarrow s(x+y)$, $\mu$-convergente
|
|
\item $x'+(y'+y) \hookrightarrow (x'+y')+y \hookleftarrow y+(x'+y')$, $\mu$-convergente
|
|
\end{enumerate}
|
|
|
|
Puesto que todos los pares $\mu$-críticos son $\mu$-convergentes, $\mathcal{R}_{151}$ es localmente $\mu$-confluente.
|
|
|
|
\section{SRT $\mathcal{R}_{153}$}
|
|
|
|
\begin{lstlisting}
|
|
(VAR x y z)
|
|
(RULES
|
|
or(x,T) -> T
|
|
or(x,F) -> x
|
|
or(or(x,y),z) -> or(x,or(y,z))
|
|
or(x,y) -> or(y,x)
|
|
)
|
|
\end{lstlisting}
|
|
|
|
Nota: en esta sección, se utilizará $\vee$ para representar la función ``or''.
|
|
|
|
\subsection{Función de reemplazamiento $\mu_{153}$}
|
|
|
|
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.
|
|
|
|
\begin{figure}[h]
|
|
\begin{center}
|
|
\begin{tabular}{|l|c|c|c|}
|
|
\hline
|
|
$n$ & $l \rightarrow r$ & $l' \rightarrow r'$ & $p$ \\ \hline
|
|
1 & $x \vee T \rightarrow T$ & $(x' \vee y') \vee z' \rightarrow x' \vee (y' \vee z')$ & $\wedge$ \\
|
|
2 & $x \vee T \rightarrow T$ & $x' \vee y' \rightarrow y' \vee x'$ & $\wedge$ \\
|
|
3 & $x \vee F \rightarrow x$ & $(x' \vee y') \vee z' \rightarrow x' \vee (y' \vee z')$ & $\wedge$ \\
|
|
4 & $x \vee F \rightarrow x$ & $x' \vee y' \rightarrow y' \vee x'$ & $\wedge$ \\
|
|
5 & $(x \vee y) \vee z \rightarrow x \vee (y \vee z)$ & $x' \vee T \rightarrow T$ & 1 \\
|
|
6 & $(x \vee y) \vee z \rightarrow x \vee (y \vee z)$ & $x' \vee F \rightarrow x'$ & 1 \\
|
|
7 & $(x \vee y) \vee z \rightarrow x \vee (y \vee z)$ & $(x' \vee y') \vee z' \rightarrow x' \vee (y' \vee z')$ & 1 \\
|
|
8 & $(x \vee y) \vee z \rightarrow x \vee (y \vee z)$ & $x' \vee y' \rightarrow y' \vee x'$ & $\wedge$ \\
|
|
9 & $(x \vee y) \vee z \rightarrow x \vee (y \vee z)$ & $x' \vee y' \rightarrow y' \vee x'$ & 1 \\ \hline
|
|
\end{tabular}
|
|
\end{center}
|
|
\caption{Reglas escogidas para los pares críticos de $\mathcal{R}_{153}$}
|
|
\label{pares153}
|
|
\end{figure}
|
|
|
|
\subsection{$\mu$-confluencia}
|
|
|
|
De nuevo, como en el caso anterior, $\mathcal{R}_{153}$ no es ortogonal, por lo tanto hemos de estudiar su $\mu$-terminación y la $\mu$-convergencia de sus pares $\mu$-críticos.
|
|
|
|
La $\mu$-terminación se puede estudiar fácilmente con la herramienta \textsc{MuTerm}, y el resultado es que el problema es infinito.
|
|
|
|
El estudio de la $\mu$-convergencia de los pares $\mu$-críticos de la figura \ref{mupares153} es el siguiente:
|
|
|
|
\begin{enumerate}
|
|
\item $x' \vee (y' \vee T) \hookrightarrow x' \vee T \hookrightarrow T$, $\mu$-convergente
|
|
\item $T \vee x \hookrightarrow x \vee T \hookrightarrow T$, $\mu$-convergente
|
|
\item $x' \vee (y' \vee F) \hookrightarrow x' \vee y'$, $\mu$-convergente
|
|
\item $F \vee x \hookrightarrow x \vee F \hookrightarrow x$, $\mu$-convergente
|
|
\setcounter{enumi}{7}
|
|
\item $z \vee (x \vee y) \hookrightarrow (x \vee y) \vee z \hookleftarrow x \vee (y \vee z)$, $\mu$-convergente
|
|
\end{enumerate}
|
|
|
|
\begin{figure}[h]
|
|
\begin{center}
|
|
\begin{tabular}{r|c|c}
|
|
n & $\sigma(l)[\sigma(r')]_p$ & $\sigma(r)$ \\ \hline
|
|
1 & $x' \vee (y' \vee T)$ & $T$ \\
|
|
2 & $T \vee x$ & $T$ \\
|
|
3 & $x' \vee (y' \vee F)$ & $x' \vee y'$ \\
|
|
4 & $F \vee x$ & $x$ \\
|
|
8 & $z \vee (x \vee y)$ & $x \vee (y \vee z)$ \\ \hline
|
|
\end{tabular}
|
|
\end{center}
|
|
\caption{Pares $\mu$-críticos de $\mathcal{R}_{153}$}
|
|
\label{mupares153}
|
|
\end{figure}
|
|
|
|
\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}
|
|
|
|
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:
|
|
|
|
\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}
|
|
|
|
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} |