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


\section{SRT $\mathcal{R}_{i}$}
\subsection{Función de reemplazamiento $\mu_{i}$}
\subsection{Pares $\mu$-críticos}
\subsection{$\mu$-confluencia}

\section{SRT $\mathcal{R}_{i}$}
\subsection{Función de reemplazamiento $\mu_{i}$}
\subsection{Pares $\mu$-críticos}
\subsection{$\mu$-confluencia}

\end{document}