200 lines
No EOL
8.9 KiB
TeX
200 lines
No EOL
8.9 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$).
|
|
|
|
\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}
|
|
|
|
\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$.
|
|
|
|
\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}_{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}
|
|
|
|
\section{SRT $\mathcal{R}_{i}$}
|
|
\subsection{Función de reemplazamiento $\mu_{i}$}
|
|
\subsection{Pares $\mu$-críticos}
|
|
\subsection{$\mu$-confluencia}
|
|
|
|
\end{document} |