cap2.tex

\cleardoublepage
\chapter{Semántica operacional}
						
$\\$

En el anterior capítulo hemos visto cómo dar un valor semántico al lenguaje While mediante el punto de vista de la semántica denotacional. Centrémonos ahora en la semántica operacional. La distinción fundamental que hacíamos de este enfoque es la siguiente:
\begin{itemize}
    \item Semántica operacional \textit{natural}, que describe cómo se han obtenido los resultados generales de las ejecuciones.
    \item Semántica operacional \textit{estructural}, que describe cómo se ha obtenido cada paso en la ejecución.
\end{itemize}
Para ambos tipos de semántica operacional, el valor semántico de cada expresión será especificado por un \textit{sistema de transiciones}, compuesto de dos configuraciones distintas:
\begin{itemize}
    \item[] $\langle S, s\rangle$, que denota que la expresión $S$ se ejecutará desde el estado $s$.
    \item[] $s$, que denota un estado terminal. Las \textit{configuraciones terminales} tendrán esta forma.
\end{itemize}
Finalmente, es necesaria una \textit{relación de transición} que describa cómo tiene lugar la ejecución. La diferencia entre las dos semánticas se encuentra principalmente en ésta. De hecho, veremos que ambos tipos de semántica son, en cierto sentido, equivalentes.

\section{Semántica operacional natural}


\subsection{Sistema de transiciones}

La relación de transición $\langle S, s\rangle \rightarrow s'$ se puede leer como que, la ejecución de $S$ desde el estado $s$ terminará y el nuevo estado será $s'$. Está determinada por las siguientes reglas\footnote{Nótese que las variables $S_1, S_2, s, s', s''$, etc. son libres.}:  


\begin{sist*}[$\nn{While}_\nn{ns}$]\mbox{}
\begin{itemize}
    \item[] $[\text{ass}_{\text{ns}}]$

        \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \AxiomC{}
                \UnaryInfC{ $\langle x:= a, s\rangle \rightarrow s[x\mapsto \fc{A}{a}s]$}
              \DisplayProof
        \end{center}

    \item[] $[\text{skip}_{\text{ns}}]$ 
        \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \AxiomC{}
                \UnaryInfC{$\la{\n{skip}}{s}\rightarrow s$}
                  \DisplayProof
        \end{center}

    \item[][$\text{comp}_{\text{ns}}$]
        \begin{center}
              \centerAlignProof
                
              \quad
              \centerAlignProof
                \AxiomC{$\la{S_1}{s} \to s'$}
                \AxiomC{$\la{S_2}{s'} \to s''$}
                \BinaryInfC{$\la{S_1; S_2}{s} \to s''$}
              \DisplayProof
        \end{center}
\newpage
\item[][$\text{if}^{\text{tt}}_{\text{ns}}$]


\begin{center}
      \centerAlignProof
        
      \quad
      \centerAlignProof
        \AxiomC{$\la{S_1}{s} \to s'$}
        \UnaryInfC{$\la{\n{if}\ b\ \n{then}\ S_1\ \n{else}\ S_2}{s} \to s'$}
      \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s = \mathbf{tt}$
\end{center}
\item[] [$\text{if}^{\text{ff}}_{\text{ns}}$]

\begin{center}
      \centerAlignProof
       
      \quad
      \centerAlignProof
        \AxiomC{$\la{S_2}{s} \to s'$}
        \UnaryInfC{$\la{\n{if}\ b\ \n{then}\ S_1\ \n{else}\ S_2}{s} \to s'$}
      \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s = \mathbf{ff}$
\end{center}
\item[][$\text{while}^{\text{tt}}_{\text{ns}}$]

\begin{center}
      \centerAlignProof
        
      \quad
      \centerAlignProof
        \AxiomC{$\la{S}{s} \to s'$}
        \AxiomC{$\la{\n{while}\ b\ \n{do}\ S}{s'} \to s''$}
        \BinaryInfC{$\la{\n{while}\ b\ \n{do}\ S}{s} \to s''$}
      \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s = \mathbf{tt}$
\end{center}
\item[] [$\text{while}^{\text{ff}}_{\text{ns}}$]

\begin{center}
      \centerAlignProof
       
      \quad
      \centerAlignProof
        \AxiomC{}
        \UnaryInfC{$\la{\n{while}\ b\ \n{do}\ S}{s} \to s$}
      \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s = \mathbf{ff}$
\end{center}
\end{itemize}
\end{sist*}

Aclaremos un poco la terminología:

\begin{definition}
Una \textit{regla} en general tiene la forma general
\begin{center}
      \centerAlignProof
       
      \quad
      \centerAlignProof
        \AxiomC{$\la{S_1}{s_1}\rightarrow s'_1 \dots \la{S_n}{s_n}\rightarrow s'_n $}
    \UnaryInfC{$\la{S}{s}\rightarrow s'$}
      \DisplayProof
      \quad
      \centerAlignProof
    $\text{ si } \varphi$
\end{center}
donde los términos que aparecen encima y bajo la línea son, respectivamente, las \textit{premisas} y la \textit{conclusión}, y donde $\varphi$ es la \textit{condición}. Cuando empleamos las reglas anteriores para obtener una transición $\la{S}{s}\rightarrow s'$, obtenemos un \textit{árbol de derivación}. Una regla sin premisas se llama \textit{axioma}.
\end{definition}

Consideremos el problema de construir un árbol de derivación para una expresión $S$ y un estado $s$. El método general consiste en partir de la `raíz' y encontrar las `hojas', es decir, el paso inicial consiste en buscar una regla de modo que su conclusión tenga la ejecución $\la{S}{s}$ en su parte izquierda. Los pasos inductivos son:
\begin{itemize}
    \item Si la regla encontrada es un axioma, entonces podemos determinar el estado terminal y terminamos.
    \item Si la regla encontrada no es un axioma, entonces el siguiente paso consiste en buscar un árbol de derivación para sus premisas. 
\end{itemize}
Nótese que, en cada paso, las condiciones para aplicar cada regla tienen que ser verificadas. En el futuro demostraremos algo que parece falso a primera vista: que en el lenguaje While hay a lo sumo un árbol de derivación posible para cada ejecución $\la{S}{s}$.


\begin{definition}
Decimos que una ejecución de la expresión $S$ desde el estado $s$, $\la{S}{s}$, \textit{termina} si existe un estado $s'$ tal que $\la{S}{s}\rightarrow s'$. Si tal estado no existe entonces decimos que la ejecución \textit{cicla}. Para una expresión $S$, decimos que \textit{siempre termina} si $\la{S}{s}$ termina para cada elección de $s$ y que \textit{siempre cicla} si $\la{S}{s}$ cicla para cada elección de $s$.
\end{definition}

\begin{example}
Podemos tratar de determinar si las siguientes expresiones terminan o ciclan siempre:
\begin{enumerate}
    \item $\n{while} \, \neg(\n{x}=1) \, \n{do} \, (\n{y} := \n{y} \times \n{x}; \n{x} := \n{x} - 1)$.
    \item $\n{while} \, 1 \leq \n{x} \, \n{do} \, (\n{y} := \n{y} \times \n{x}; \n{x} := \n{x} - 1)$.
    \item $\n{while true do skip}$.
\end{enumerate}
La primera para si se inicializa $x$ con un valor mayor o igual que $1$ y cicla en caso contrario: nótese que si $\n{x}<1$ decrecerá continuamente, luego es imposible que la condición del bucle llegue a no cumplirse.\\ \\
La segunda para siempre. Es parecida a la anterior salvo por el hecho de que la condición del bucle hace que, para $\n{x}<1$, se pare. \\ \\
La tercera dejaría intacta la configuración inicial. Sin embargo, la ejecución cicla pese a no realizar ninguna acción. Esto es porque la condición del bucle es siempre cierta.
\end{example}

\subsection{Propiedades}

El sistema de transición nos da un entorno en el que estudiar las propiedades de las expresiones. Veamos a continuación una definición precisa de un concepto que introdujimos al final de la introducción:
\begin{definition}
Dos expresiones $S_1, S_2$ se dicen \textit{semánticamente equivalentes} si para cada par $s, s' \in \mathbf{State}$, 
$$\la{S_1}{s}\rightarrow s' \text{ si y solo si } \la{S_2}{s}\rightarrow s'.$$
\end{definition}

\begin{lema}\label{lemans}
\normalfont $\n{while } b \n{ do } S$ \textit{es semánticamente equivalente a} $\n{if } b \n{ then } (S; \n{while } b \n{ do } S)\n{ else skip}$.
\end{lema}
\begin{proof}
Dividimos la prueba en dos implicaciones:


\noindent\textit{Parte 1.} Supongamos que se cumple $\la{\n{while } b \n{ do } S}{s}\rightarrow s''$. Entonces existe un árbol de derivación para él, $T$. $T$ puede tener dos formas en función de la regla que hayamos aplicado: o bien hemos aplicado la regla o el axioma [$\text{while}^{\text{ff}}_{\text{ns}}$]. Veamos cada caso:
\\

\noindent$(a)$ Si hemos aplicado la regla [$\text{while}^{\text{tt}}_{\text{ns}}$], $T$ es de la forma:
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
      \AxiomC{$\dots$}
      \UnaryInfC{$\la{S}{s}\rightarrow s'$}
      \AxiomC{$\dots$}
      \UnaryInfC{$\la{\n{while}\ b\ \n{do}\ S}{s'} \to s''$}
    \BinaryInfC{$\la{\n{while } b \n{ do } S}{s}\rightarrow s''$}[$\text{while}^{\text{tt}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
      \end{center}

con $\fc{B}{b}s = \mathbf{tt}$. Ahora bien, notemos que:
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
      \AxiomC{$\dots$}
      \UnaryInfC{$\la{S}{s}\rightarrow s'$}
      \AxiomC{$\dots$}
      \UnaryInfC{$\la{\n{while}\ b\ \n{do}\ S}{s'} \to s''$}
    \BinaryInfC{$\la{S;\n{while } b \n{ do } S}{s}\rightarrow s''$}$[\text{comp}_{\text{ns}}]$
      \DisplayProof
      \quad
      \centerAlignProof
      \end{center}
Usando que $\fc{B}{b}s = \mathbf{tt}$, podemos aplicar:
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
    \AxiomC{$\la{S;\n{while } b \n{ do } S}{s}\rightarrow s''$}
    \UnaryInfC{$\la{\n{if}\ b\ \n{then}\ (S;\n{while } b \n{ do } S)\ \n{else}\ \n{skip}}{s} \to s''$}[$\text{if}^{\text{ff}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
      \end{center}
Y por tanto, $\la{\n{if}\ b\ \n{then}\ (S;\n{while } b \n{ do } S)\ \n{else}\ \n{skip}}{s} \to s''$.
\\

\noindent $(b)$ Si hemos aplicado la regla  [$\text{while}^{\text{ff}}_{\text{ns}}$], $T$ es de la forma:
\begin{center}
      \centerAlignProof
       
      \quad
      \centerAlignProof
        \AxiomC{}
        \UnaryInfC{$\la{\n{while}\ b\ \n{do}\ S}{s} \to s$}
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
es decir, necesariamente $s=s''$ y $\fc{B}{b}s = \mathbf{ff}$. Usando el axioma $[\text{skip}_{\text{ns}}]$, directamente obtenemos que 
\begin{center}
      \centerAlignProof
       
      \quad
      \centerAlignProof
        \AxiomC{}
        \UnaryInfC{$\la{\n{skip}}{s}\rightarrow s''$}$[\text{skip}_{\text{ns}}]$
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
Pero entonces, 
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
        \AxiomC{$\la{\n{while}\ b\ \n{do}\ S}{s} \to s$}
        \AxiomC{$\la{\n{skip}}{s}\rightarrow s''$}
        \BinaryInfC{$\la{\n{if}\ b\ \n{then}\ (S;\n{while } b \n{ do } S)\ \n{else}\ \n{skip}}{s} \to s''$}[$\text{if}^{\text{ff}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
y por tanto obtenemos el resultado.
\\

\noindent\textit{Parte 2.} Supongamos ahora que se cumple $\la{\n{if}\ b\ \n{then}\ (S;\n{while } b \n{ do } S)\ \n{else}\ \n{skip}}{s} \to s''$. Entonces, tenemos un árbol de derivación $T$ y, de nuevo, podemos distinguir qué forma tendrá según las reglas que hayamos aplicado:
\\

\noindent $(a)$ Si hemos aplicado la regla [$\text{if}^{\text{tt}}_{\text{ns}}$], $T$ es de la forma:
\begin{center}
      \centerAlignProof
        
      \quad
      \centerAlignProof
      \AxiomC{$\dots$}
        \UnaryInfC{$\la{S; \n{while } b \n{ do } s}{s} \to s''$}
        \UnaryInfC{$\la{\n{if}\ b\ \n{then}\ (S;\n{while } b \n{ do } S)\ \n{else}\ \n{skip}}{s} \to s''$}[$\text{if}^{\text{tt}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
y con $\fc{B}{b}s = \mathbf{tt}$. Ahora bien, solo hemos podido obtener la premisa anterior mediante $[\text{comp}_{\text{ns}}]$, por tener una expresión de la forma $S_1; S_2$ en la ejecución. Entonces deducimos que $T$ es:
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
        \AxiomC{$\dots$}
        \UnaryInfC{$\la{S}{s}\rightarrow s'$}
        \AxiomC{$\dots$}
        \UnaryInfC{$\la{\n{while } b \n{ do } S}{s'}\rightarrow s''$}
        \BinaryInfC{$\la{S; \n{while } b \n{ do } s}{s} \to s''$}[$\text{comp}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
Pero entonces notemos que, usando la hipótesis $\fc{B}{b}s = \mathbf{tt}$:
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
        \AxiomC{$\dots$}
        \UnaryInfC{$\la{S}{s}\rightarrow s'$}
        \AxiomC{$\dots$}
        \UnaryInfC{$\la{\n{while } b \n{ do } S}{s'}\rightarrow s''$}
        \BinaryInfC{$\la{\n{while}\ b\ \n{do}\ S}{s} \to s''$}[$\text{while}^{\text{tt}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
y obtenemos el resultado.
\\

\noindent $(b)$ Si hemos usado la regla [$\text{if}^{\text{ff}}_{\text{ns}}$], deducimos que $\fc{B}{b}s = \mathbf{ff}$ y que por tanto tenemos un árbol de derivación para $\la{\n{skip}}{s}\rightarrow s''$ y, por tanto, que $s=s''$. Pero usando  [$\text{while}^{\text{ff}}_{\text{ns}}$], tenemos el resultado (el razonamiento ha sido análogo al apartado $(b)$ de la Parte 1).

\end{proof}



\begin{example}
Veamos que $S_1; (S_2; S_3)$ y $(S_1; S_2); S_3$ son semánticamente equivalentes. Si suponemos que $\la{S_1; (S_2; S_3)}{s}\rightarrow s'$, entonces es porque en su árbol de derivación hemos empleado [$\text{comp}_{\text{ns}}$] a las premisas $\la{S_1}{s}\rightarrow s''$ y $\la{S_2;S_3}{s''}\rightarrow s'$. A su vez, la segunda premisa proviene del mismo modo de las premisas $\la{S_2}{s''}\rightarrow t$ y $\la{S_3}{t}\rightarrow s'$. Es decir, tenemos las siguientes hojas:
\begin{itemize}
    \item[(a)] $\la{S_1}{s}\rightarrow s''$.
    \item[(b)] $\la{S_2}{s''}\rightarrow t$.
    \item[(c)] $\la{S_3}{t}\rightarrow s'$.
\end{itemize}
Ahora, combinando (a) y (b) con [$\text{comp}_{\text{ns}}$], obtenemos $\la{S_1;S_2}{s}\rightarrow t$ y, combinando esto con (c) de la misma forma, obtenemos que $\la{(S_1; S_2);S_3}{s}\rightarrow s'$, como queríamos ver. La otra implicación es análoga.

Notemos, por otro lado, que en general $S_1;S_2$ y $S_2; S_1$ no son semánticamente equivalentes: si tratásemos de hacer lo mismo que antes, obtendríamos las hojas $\la{S_1}{s}\rightarrow s''$ y $\la{S_2}{s''}\rightarrow s'$ por un lado y $\la{S_2}{s}\rightarrow s''$ y $\la{S_1}{s''}\rightarrow s'$ por otro, y en general no hay forma de combinar cada par de premisas para obtener la conclusión deseada.
\end{example}
\begin{example}\textbf{}
Podemos expandir el sistema $\text{While}_\text{ns}$ el siguiente modo: añadimos dos reglas que permitan dar una semántica de la expresión $\n{for }x:= a_1 \n{ to } a_2\n{ do }S$, es decir, 
\begin{itemize}
    \item[] 
\begin{center}
      \centerAlignProof
      [$\text{for}_{\text{ns}}^{\text{tt}}$]
      \quad
      \centerAlignProof
        \AxiomC{$\la{x:= a_1;S}{s}\rightarrow s'$}
        \AxiomC{$\la{\n{for } \n{x}:= \n{x}+\n{1 to } a_2 \n{ do }S}{s'}\to s''$}
        \BinaryInfC{$\la{\n{for } \n{x}:= a_1\n{ to } a_2 \n{ do }S}{s}\to s''$}
        \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{a_1\leq a_2}s = \mathbf{tt}$
\end{center}
 \item[] 
\begin{center}
      \centerAlignProof
      [$\text{for}_{\text{ns}}^{\text{ff}}$]
      \quad
      \centerAlignProof
        \AxiomC{}
        \UnaryInfC{$\la{\n{for } \n{x}:= a_1\n{ to } a_2 \n{ do }S}{s}\to s[\n{x}\mapsto \fc{A}{a_1}]s$}
        \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{a_1\leq a_2}s = \mathbf{ff}$
\end{center}
\end{itemize}
Pero debemos tener un especial cuidado con este tipo de reglas, por ejemplo, podemos descuidar que en $a_1$ aparezca la variable $\n{y}$, a saber, que $a_1$ contenga $\n{y} + 3$, y que por otro lado en $S$ tengamos $\n{y}=5$. Del mismo modo, podríamos tener que la variable $\n{x}$ ya aparece del mismo modo como $\n{x} = 4$, por ejemplo. Si $\n{x}$ apareciera en $a_2$ entonces también tendríamos este problema.
\end{example}

Aunque no lo demostraremos, se puede observar que el sistema $\text{While}_\text{ns}$ es \textit{Turing-completo}, es decir, en él podemos simular cualquier computación posible en una máquina de Turing. Por tanto, se podía pensar que podemos introducir reglas para ciertas expresiones en función de su correlato en $\text{While}_\text{ns}$ (que existe, por lo anterior). Sin embargo, si quisiéramos introducir $\n{for }x:= a_1 \n{ to } a_2\n{ do }S$ como un bucle $\n{while ... do ...}$, acabaríamos teniendo apariciones de $\n{while ... do ...}$ en las reglas asociadas a $\n{for }x:= a_1 \n{ to } a_2\n{ do }S$, lo que difiere de la semántica operacional que hemos visto hasta ahora.
\\

\begin{example}
Podríamos extender el lenguaje While con dos reglas para la expresión $\n{repeat } S \n{ until } b$:
\begin{itemize}
    \item[] 
\begin{center}
      \centerAlignProof
      [$\text{repeat}_{\text{ns}}^{\text{tt}}$]
      \quad
      \centerAlignProof
        \AxiomC{$\la{S}{s}\rightarrow s'$}
        \UnaryInfC{$\la{\n{repeat } S \n{ until } b}{s}\rightarrow s'$}
        \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s' = \mathbf{tt}$
\end{center}
    \item[] 
\begin{center}
      \centerAlignProof
      [$\text{repeat}_{\text{ns}}^{\text{ff}}$]
      \quad
      \centerAlignProof
        \AxiomC{$\la{S}{s}\rightarrow s'$}
        \AxiomC{$\la{\n{repeat } S \n{ until } b}{s'}\rightarrow s''$}
        \BinaryInfC{$\la{\n{repeat } S \n{ until } b}{s}\rightarrow s''$}
        \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s' = \mathbf{ff}$
\end{center}
\end{itemize}
\end{example}
\begin{prop}
Son semánticamente equivalentes:
\begin{itemize}
    \item $\n{repeat } S \n{ until } b$.
    \item $S; \n{if } b \n{ then skip else } (\n{repeat } S \n{ until } b)$.
\end{itemize}
\end{prop}
\begin{proof}

\noindent\textit{Parte 1.} Supongamos que $\la{\n{repeat } S \n{ until } b}{s}\rightarrow s'$. Solo tenemos las siguientes posibilidades:
\\

\noindent\textit{(a)} Si hemos aplicado la regla [$\text{repeat}_{\text{ns}}^{\text{tt}}$], tenemos:
\begin{center}
      \centerAlignProof
      [$\text{repeat}_{\text{ns}}^{\text{tt}}$]
      \quad
      \centerAlignProof
        \AxiomC{$\la{S}{s}\rightarrow s'$}
        \UnaryInfC{$\la{\n{repeat } S \n{ until } b}{s}\rightarrow s'$}
        \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s' = \mathbf{tt}$
\end{center}
Ahora bien, por otro lado, podemos aplicar el axioma [$\text{skip}_{\text{ns}}$] para obtener directamente que $\la{\n{skip}}{s'}\rightarrow s'$. Ahora, como $\text{ si }\fc{B}{b}s' = \mathbf{tt}$, podemos aplicar la regla [$\text{if}^{\text{tt}}_{\text{ns}}$]:
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
        \AxiomC{$\la{\n{skip}}{s'}\rightarrow s'$}
        \UnaryInfC{$\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s'} \to s'$}[$\text{if}^{\text{tt}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
Y, entonces, 
        \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \AxiomC{$\la{S}{s} \to s'$}
                \AxiomC{$\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s'} \to s'$}
                \BinaryInfC{$\la{S; \n{if } b \n{ then skip else } (\n{repeat } S \n{ until } b)}{s} \to s'$}[$\text{comp}_{\text{ns}}$]
              \DisplayProof
        \end{center}
Luego obtenemos el resultado.
\\

\noindent\textit{(b)} Si hemos aplicado la regla [$\text{repeat}_{\text{ns}}^{\text{ff}}$], tenemos:
\begin{center}
      \centerAlignProof
      [$\text{repeat}_{\text{ns}}^{\text{ff}}$]
      \quad
      \centerAlignProof
        \AxiomC{$\la{S}{s}\rightarrow s''$}
        \AxiomC{$\la{\n{repeat } S \n{ until } b}{s''}\rightarrow s'$}
        \BinaryInfC{$\la{\n{repeat } S \n{ until } b}{s}\rightarrow s'$}
        \DisplayProof
      \quad
      \centerAlignProof
        $\text{ si }\fc{B}{b}s' = \mathbf{ff}$
\end{center}
Ahora, usando que $\text{ si }\fc{B}{b}s' = \mathbf{ff}$, 
\begin{center}
      \centerAlignProof
      \quad
      \centerAlignProof
        \AxiomC{$\la{\n{repeat } S \n{ until } b}{s''}\rightarrow s'$}
        \UnaryInfC{$\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s''} \to s'$}[$\text{if}^{\text{ff}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}

Pero entonces, 
\begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \AxiomC{$\la{S}{s} \to s''$}
                \AxiomC{$\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s''} \to s'$}
                \BinaryInfC{$\la{S; \n{if } b \n{ then skip else } (\n{repeat } S \n{ until } b)}{s} \to s'$}[$\text{comp}_{\text{ns}}$]
              \DisplayProof
\end{center}
\noindent\textit{Parte 2.} Supongamos que $\la{S;\n{ if } b \n{ then } \n{skip } \n{else } \n{repeat } S \n{ until } b}{s}\to s'$. La única posibilidad es haber aplicado la regla $[\text{comp}_{\text{ns}}]$
\begin{center}
    \centerAlignProof
    \quad
    \centerAlignProof
    \AxiomC{$\la{S}{s} \to s_0$}
    \AxiomC{$\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s_0} \to s'$}
    \BinaryInfC{$\la{S;\n{if } b \n{ then } \n{skip } \n{else } \n{repeat } S \n{ until } b}{s}\to s'$}
    \DisplayProof
\end{center}
para algún $s_0 \in \textbf{State}$. Para la transición $\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s_0} \to s'$ tenemos dos posibilidades
\\ \\
\noindent\textit{(a)} Si $\fc{B}{b}s_0 = \textbf{tt}$ entonces únicamente existe la posibilidad de que se haya derivado de $[\text{if}^\nn{tt}_\nn{ns}]$:
\begin{center}
    \centerAlignProof
    \quad
    \centerAlignProof
    \AxiomC{$\la{skip}{s_0} \to s' $}
    \UnaryInfC{$\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s_0} \to s'$}
    \DisplayProof
\end{center}
y la única forma de que sea cierto $\la{skip}{s_0} \to s'$ es que $s_0 = s'$. Como se verifica $\la{S}{s} \to s_0$ entonces se verifica $\la{S}{s} \to s'$ y se puede aplicar la regla $[\text{repeat}^\nn{tt}_\nn{ns}]$:
\begin{center}
    \centerAlignProof
    \quad
    \centerAlignProof
    \AxiomC{$\la{S}{s} \to s' $}
    \UnaryInfC{$\la{\n{repeat } S \n{ until } b}{s} \to s'$}
    \DisplayProof
\end{center}
obteniendo el resultado pues ya se sabe que $\la{S}{s} \to s_0$.
\\ \\
\noindent\textit{(b)}  Si $\fc{B}{b}s_0 = \textbf{ff}$ entonces solo cabe la posibilidad de que haya partido de $[\text{if}^\nn{ff}_\nn{ns}]$:

\begin{center}
    \centerAlignProof
    \quad
    \centerAlignProof
    \AxiomC{$\la{\n{repeat } S \n{ until } b}{s_0} \to s'$}
    \UnaryInfC{$\la{\n{if}\ b\ \n{then skip else}\ (\n{repeat } S \n{ until } b)}{s_0} \to s'$}
    \DisplayProof
\end{center}
teniendo así $\la{\n{repeat } S \n{ until } b}{s_0} \to s'$ y entonces se puede deducir
\begin{center}
    \centerAlignProof
    \quad
    \centerAlignProof
    \AxiomC{$\la{S}{s} \to s_0$}
    \AxiomC{$\la{\n{repeat } S \n{ until } b}{s_0} \to s'$}
    \BinaryInfC{$\la{\n{repeat } S \n{ until } b}{s} \to s'$}
    \DisplayProof
\end{center}
mediante $[\text{repeat}^\nn{ff}_\nn{ns}]$ pues $\fc{B}{b}s_0 = \textbf{ff}$. \\
\end{proof}


Para poder demostrar que una propiedad como la anterior se verifica en árboles sencillos y compuestos, emplearemos la demostración por \textit{inducción sobre reglas}, que se compone de dos pasos:
\begin{enumerate}
    \item Primero comprobamos que la propiedad se verifica para los axiomas del sistema.
    \item Para cada regla, suponiendo que las premisas verifican la propiedad , comprobamos que también se cumple para la conclusión (siempre y cuando se verifiquen las condiciones de la regla).
\end{enumerate}
El siguiente resultado nos dice que, en general, hay \textit{una} manera de deducir una configuración mediante las reglas del sistema de transición $\nn{While}_\nn{ns}$:

\begin{theorem}\label{determinismo}
El sistema de transiciones $\nn{While}_{\nn{ns}}$ es determinista, es decir, para cada $S \in \mathbf{Stm}$, $s, s', s'' \in \mathbf{State}$,  
$$\la{S}{s}\rightarrow s' \text{ y } \la{S}{s}\rightarrow s'' \text{ implica que } s'= s''.$$
\end{theorem}
\begin{proof}
Para simplificar la demostración, vamos a definir una propiedad sintáctica de las reglas del sistema $\nn{While}_\nn{ns}$. Decimos que dos reglas son \textit{independientes entre sí} cuando no es posible obtener una mediante la aplicación de la otra. Notemos que este es el caso de nuestro sistema: las reglas $[\nn{while}_\nn{ns}^\nn{tt}]$ y $[\nn{while}_\nn{ns}^\nn{ff}]$ son independientes entre sí porque ambas tienen premisas distintas (suponemos que $\mathbf{tt}$ y $\mathbf{ff}$ son distintos). Entonces, como cada regla es independiente de la otra (y evidentemente, cada regla es determinista), deducimos que, en caso de que tengamos $\la{S}{s}\rightarrow s'$ y $\la{S}{s}\rightarrow s''$, necesariamente tendremos que haber aplicado la misma única regla posible en los dos casos para llegar a las respectivas configuraciones. Es fácil convencerse entonces de que, por inducción sobre las reglas, la propiedad deseada se cumple\footnote{Obviamente, esa demostración no es intercambiable con la demostración formal por inducción estructural. Podría demostrarse el caso general del que hemos hablado, a saber, formalizando lo que significa precisamente la independencia de dos reglas.}. 
\end{proof}
\begin{example} Podemos añadir una semántica $\n{forVar}\ x\ \n{do}\ S$ que ejecute la sentencia $S$ siempre que $x$ sea distinto de $0$ y lo incremente en $1$ en cada iteración. Veamos que sería semánticamente equivalente a $\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)$.
\\ \\
Primero, definimos la semantica de $\n{forVar}\ x\ \n{do}\ S$:
        \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \AxiomC{}
                \LeftLabel{$[\text{for}^0]$ }
                \RightLabel{si $\fc{A}{x}s = 0$}
                \UnaryInfC{$\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s$}
              \DisplayProof
        \end{center}
        
        \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \LeftLabel{$[\text{for}^{\ne 0}]$ }
                \RightLabel{si $\fc{A}{x}s \ne 0$}
                \AxiomC{ $\la{S; x := x+1}{s} \to s'$ }
                \AxiomC{$\la{\n{forVar}\ x\ \n{do}\ S}{s'} \to s_1$}
                \BinaryInfC{$\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s_1$}
              \DisplayProof
        \end{center}

\noindent Veamos que $\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s_1$ implica $\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s}\to s_1 $.\\
Para empezar, sabemos que $\fc{A}{x}s = 0$ si y solo si $\fc{B}{\neg (x=0) }s = \mathbf{ff}$, dividimos la demostración en dos pasos:

\begin{enumerate}
    \item Si $x=0$ tenemos por $[\text{for}^0]$ que:
    \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \AxiomC{$\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s$}
              \DisplayProof
        \end{center}
        
    Como $\fc{B}{\neg (x=0) }s = \mathbf{ff}$ por la regla [$\text{while}^{\text{ff}}_{\text{ns}}$] sabemos que:

    \begin{center}
          \centerAlignProof
       
          \quad
          \centerAlignProof
            \AxiomC{$\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s} \to s$}
          \DisplayProof
          \quad
          \centerAlignProof
    \end{center}    
    
    \item Si $ x\ne0$, entonces suponemos ciertas las siguientes premisas:
    \begin{enumerate}[label=\alph*)]
        \item  \AxiomC{$\la{S; x := x+1}{s} \to s_2$} \DisplayProof
        \item   \AxiomC{$\la{\n{forVar}\ x\ \n{do}\ S}{s_2} \to s'$} \DisplayProof
    \end{enumerate}
    
    
    pues la transición $\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s'$ solo puede haber provenido de:
    
    \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                
                \AxiomC{ $\la{S; x := x+1}{s} \to s_2$ }
                \LeftLabel{$[\text{for}^{\ne 0}]$}
                \AxiomC{$\la{\n{forVar}\ x\ \n{do}\ S}{s_2} \to s'$}
                \BinaryInfC{$\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s'$}
              \DisplayProof
        \end{center}
    Podemos aplicar la hipótesis de inducción sobre $\la{\n{forVar}\ x\ \n{do}\ S}{s_2} \to s'$ y por lo tanto tenemos que $\la{\n{forVar}\ x\ \n{do}\ S}{s_2} \to s'$ implica que $\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s_2} \to s' $, luego podemos costruir el siguiente árbol de derivación:
    
    \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                
                \AxiomC{ $\la{S; x := x+1}{s} \to s_2$ }
                \LeftLabel{ [$\text{while}^{\text{tt}}_{\text{ns}}$]}
                \AxiomC{$\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s_2} \to s'$}
                \BinaryInfC{$\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s} \to s'$}
              \DisplayProof
        \end{center}
\end{enumerate}
Supongamos ahora que $\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s}\to s'$. Entonces, distinguimos los siguientes casos:
\begin{enumerate}
    \item Si hemos aplicado [$\text{while}^{\text{ff}}_{\text{ns}}$], entonces 
    \begin{center}
      \centerAlignProof
       
      \quad
      \centerAlignProof
        \AxiomC{}
        \UnaryInfC{$\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s} \to s'$}[$\text{while}^{\text{ff}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
y además deducimos que $s=s'$ y que $x \neq 0$. Pero entonces tenemos que, directamente:
\begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \AxiomC{}
                \LeftLabel{$[\text{for}^0]$ }
                \RightLabel{}
                \UnaryInfC{$\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s$}
              \DisplayProof
        \end{center}
es decir, obtenemos la implicación deseada.
    \item Si hemos aplicado [$\text{while}^{\text{tt}}_{\text{ns}}$], 
\begin{center}
      \centerAlignProof
        
      \quad
      \centerAlignProof
        \AxiomC{$\la{(S; x:=x+1)}{s} \to s'$}
        \AxiomC{$\la{\n{while}\  \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s'} \to s''$}
        \BinaryInfC{$\la{\n{while}\ \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s} \to s''$}[$\text{while}^{\text{tt}}_{\text{ns}}$]
      \DisplayProof
      \quad
      \centerAlignProof
\end{center}
y además deducimos que $x \neq 0$. Si aplicamos hipótesis de inducción sobre $\la{\n{while}\  \neg (x=0)\ \n{do}\ (S; x:=x+1)}{s'} \to s''$, obtenemos que $\la{\n{forVar}\ x\ \n{do}\ S}{s'} \to s''$. Pero entonces, juntando las premisas anteriores,  
  \begin{center}
              \centerAlignProof
              \quad
              \centerAlignProof
                \LeftLabel{$[\text{for}^{\ne 0}]$ }
                \RightLabel{}
                \AxiomC{ $\la{S; x := x+1}{s} \to s'$ }
                \AxiomC{$\la{\n{forVar}\ x\ \n{do}\ S}{s'} \to s''$}
                \BinaryInfC{$\la{\n{forVar}\ x\ \n{do}\ S}{s} \to s''$}
              \DisplayProof
        \end{center}
luego obtenemos el resultado.
\end{enumerate}
\end{example}
\subsection{Expresiones}

Finalmente, podemos definir el valor semántico de cada $S \in \mathbf{Stm}$ mediante una aplicación
$\mc{S}_\nn{ns}: \mathbf{Stm} \rightarrow (\mathbf{State}\hookrightarrow\mathbf{State})$, donde
\begin{align*}
    \mc{S}_\nn{ns}[[S]]:  \mathbf{State} & \hookrightarrow  \mathbf{State} \\
                     s               & \mapsto          \begin{cases} s' \text{, si } \la{S}{s}\to s' \\ 
                        \nn{indefinido} \text{, en otro caso}
                        \end{cases}
\end{align*}
El determinismo de $\nn{While}_\nn{ns}$ implica que está bien definida. Además, es parcial porque, como vimos, la expresión $\n{while true do skip}$ siempre entra en bucle, es decir, $ \mc{S}_\nn{ns}[[\n{while true do skip}]]s = \mathrm{indefinido}$, para cada $s \in \mathbf{State}$.


\begin{example}
Podemos definir, por ejemplo, una semántica de paso largo para $\mathbf{Aexp}$ mediante la relación de transición $\la{a}{s}\rightarrow_A z$, donde $\la{a}{s}$ significa que $a \in \mathbf{Aexp}$ se evalúa en $s\in \mathbf{State}$ y $z\in \Z$ es un estado final:
\begin{sist*}[$\mathbf{Aexp}_\nn{ns}$]\mbox{}
\begin{itemize}
    \item[]
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \RightLabel{$\text{ si } n \in \mathbf{Num}$}
    \UnaryInfC{$\la{n}{s}\rightarrow_A \fc{N}{n}$}
\end{prooftree}
    \item[]
    
\begin{prooftree}
    \AxiomC{}
    \RightLabel{$\text{ si } x \in \mathbf{Var}$}
    \UnaryInfC{$\la{x}{s}\rightarrow_A s x$}
\end{prooftree}

\item[]
 \begin{prooftree}
    \AxiomC{$\la{a_1}{s}\rightarrow_A z_1$}
    \AxiomC{$\la{a_2}{s}\rightarrow_A z_2$}
    \LeftLabel{}
    \RightLabel{}
    \BinaryInfC{$\la{a_1 \n{ op } a_2}{s}\rightarrow_A z_1 * z_2$}
\end{prooftree}
$\text{donde } \n{op} \text{ se refiere a } \oplus, \ominus, \otimes \text{ y } * \text{ a } +, -, \times$.
\end{itemize}
\end{sist*}
\end{example}

\begin{prop}
Sean $a \in \mathbf{Aexp}$, $s \in \mathbf{State}$, $z \in \Z$. Entonces $\la{a}{s}\rightarrow_A z$ si y solo si $\fc{A}{a}s =z$.
\end{prop}
\begin{proof}
La demostración es por inducción estructural. Los casos base son:
\begin{itemize}
    \item Si $a = n$, entonces $\la{a}{s}\rightarrow_A \fc{N}{n} = \fc{A}{n}s$.
    \item Si $a = x$, entonces $\la{a}{s}\rightarrow_A sx = \fc{A}{x}s$.
\end{itemize}
Resumimos los casos inductivos en:
\begin{itemize}
    \item Si $a = a_1 \n{ op } a_2$, entonces, empleando la última regla de $\mathbf{Aexp}_\nn{ns}$, tenemos que $\la{a_i}{s}\rightarrow_A z_i$ si y solo si (por hipótesis de inducción) $\fc{A}{a_i}s = z_i$, con $i = 1, 2$. Pero entonces sabemos que $\fc{A}{a_1 \n{ op }a_2}S = \fc{A}{a_1}s * \fc{A}{a_2}s = z_1 * z_2 = z$.
\end{itemize}
\end{proof}

\begin{example}
Siguiendo el ejemplo anterior, podemos definir un sistema de transiciones para expresiones booleanas como sigue. Definimos $\la{b}{s}\rightarrow_B X$, donde $\la{b}{s}$ indica que $b$ se evalúa en el estado $s$ y donde $X\in Bool$. 
\begin{sist*}[$\mathbf{Bexp}_\nn{ns}$]\mbox{}
\begin{itemize}
    \item[]
    \begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \UnaryInfC{$\la{\n{true}}{s}\rightarrow_B \mathbf{tt}$}
\end{prooftree}
\item[]
    \begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \UnaryInfC{$\la{\n{false}}{s}\rightarrow_B \mathbf{ff}$}
\end{prooftree}
    \item[]
 \begin{prooftree}
    \AxiomC{$\la{a_1}{s}\rightarrow_A z_1$}
    \AxiomC{$\la{a_2}{s}\rightarrow_A z_2$}
    \LeftLabel{}
    \RightLabel{}
    \BinaryInfC{$\la{a_1 = a_2}{s}\rightarrow_B X$}
    \end{prooftree}
    donde $X$ es el booleano correspondiente (véase la definición de $\fc{B}{\cdot}$).

\item[]
\begin{prooftree}
    \AxiomC{$\la{a_1}{s}\rightarrow_A z_1$}
    \AxiomC{$\la{a_2}{s}\rightarrow_A z_2$}
    \LeftLabel{}
    \RightLabel{}
    \BinaryInfC{$\la{a_1 \leq s a_2}{s}\rightarrow_B X$}
        \end{prooftree}
    donde $X$ es el booleano correspondiente (de nuevo, empleando la definición de $\fc{B}{\cdot}$).
\item[]\begin{prooftree}
    \AxiomC{$\la{a_1}{s}\rightarrow_A z_1$}
    \AxiomC{$\la{a_2}{s}\rightarrow_A z_2$}
    \LeftLabel{}
    \RightLabel{}
    \BinaryInfC{$\la{a_1 \leq s a_2}{s}\rightarrow_B X$}
    \end{prooftree}
        donde $X$ es el booleano correspondiente.
\item[]
\begin{prooftree}
    \AxiomC{$\la{b}{s}\rightarrow_B X$}
    \LeftLabel{}
    \RightLabel{}
    \UnaryInfC{$\la{\neg b}{s}\rightarrow_B X'$}
    \end{prooftree}
    donde $X'$ es el booleano correspondiente (negación de $X$).


\item[]
\begin{prooftree}
    \AxiomC{$\la{b_1}{s}\rightarrow_B X$}
    \AxiomC{$\la{b_2}{s}\rightarrow_B Y$}
    \LeftLabel{}
    \RightLabel{}
    \BinaryInfC{$\la{b_1 \land b_2}{s}\rightarrow_B Z$}
    \end{prooftree}
donde $Z$ es el booleano correspondiente (conjunción de $X$ e $Y$).   
\end{itemize}
\end{sist*}
\end{example}
El siguiente resultado es análogo al último que dimos antes:
\begin{prop}
Sean $b \in \mathbf{Bexp}$, $s \in \mathbf{State}$ y $X \in Bool$. Entonces $\la{b}{s}\rightarrow_B X$ si y solo si $\fc{B}{b}s = X$.
\end{prop}
\begin{proof}
Por inducción estructural. Véase la demostración del anterior teorema y la definición de $\fc{B}{\cdot}$. La demostración es análoga.
\end{proof}

\section{Semántica operacional estructural}

\subsection{Sistema de transiciones}

Ahora nos centramos en los pasos concretos de la ejecución de un programa. Para ello, definimos una relación de transición $\la{S}{s} \dto \gamma$ como:
\begin{itemize}
    \item Si $\gamma$ es de la forma $\la{S'}{s'}$, entonces la ejecución de $S$ desde $s$ no se completa y sigue en $\la{S'}{s'}$.
    \item Si $\gamma$ es de la forma $s'$, entonces la ejecución finaliza en el estado $s'$.
\end{itemize}
La nueva relación de transición queda determinada por el conjunto de reglas:

\begin{sist*}[$\nn{While}_\nn{sos}$]\mbox{}
\begin{itemize}
    \item[] $[\text{ass}_{\nn{sos}}]$
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \UnaryInfC{ $\la{x:=a}{s} \dto s[x\mapsto \fc{A}{a}s]$}
\end{prooftree}
    \item[]$[\text{skip}_{\nn{sos}}]$
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \UnaryInfC{$\la{\n{skip}}{s} \dto s$}
\end{prooftree}
    \item[]$[\text{comp}_{\nn{sos}}^1]$
\begin{prooftree}
    \AxiomC{$\la{S_1}{s} \dto \la{S_1'}{s'}$}
    \LeftLabel{}
    \UnaryInfC{ $\la{S_1; S_2}{s} \dto \la{S_1'; S_2}{s'}$}
\end{prooftree}
    \item[]$[\text{comp}_{\nn{sos}}^2]$
\begin{prooftree}
    \AxiomC{$\la{S_1}{s} \dto s'$}
    \LeftLabel{}
    \UnaryInfC{ $\la{S_1; S_2}{s} \dto \la{S_2}{s'}$}
\end{prooftree}
    \item[]$[\text{if}^{\nn{tt}}_{\nn{sos}}]$
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \RightLabel{si $\fc{B}{b}s = \textbf{tt}$}
    \UnaryInfC{$\la{\n{if}\ b\ \n{then}\ S_1\ \n{else}\ S_2}{s} \dto \la{S_1}{s}$}
\end{prooftree}
    \item[]$[\text{if}_{\nn{sos}}^\nn{ff}]$
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \RightLabel{si $\fc{B}{b}s = \textbf{ff}$}
    \UnaryInfC{$\la{\n{if}\ b\ \n{then}\ S_1\ \n{else}\ S_2; s}{s} \dto \la{S_2}{s}$}
\end{prooftree}

    \item[] $[\nn{while}_\nn{sos}]$
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{}
    \RightLabel{}
    \UnaryInfC{$\la{\n{while }b\n{ do }S}{s}\dto \la{\n{if }b\n{ then }(S; \n{while }b\n{ do }S)\n{ else skip}}{s}$}
\end{prooftree}    
\end{itemize}
\end{sist*}
Notemos que podríamos haber incluido, por ejemplo, dos reglas para la semántica de $\n{while }b \n{ do }S$:
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{$[\nn{while}_\nn{sos}^\nn{ff}]$}
    \RightLabel{ si $\fc{B}{s}= \mathbf{ff}$}
    \UnaryInfC{$\la{\n{while }b\n{ do }S}{s}\dto s$}
\end{prooftree}    
y
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{$[\nn{while}_\nn{sos}^\nn{tt}]$}
    \RightLabel{ si $\fc{B}{s}= \mathbf{tt}$}
    \UnaryInfC{$\la{\n{while }b\n{ do }S}{s}\dto \la{S;\n{while }b\n{ do }S}{s}$}
\end{prooftree}    
\begin{definition}
Se dirá que $\la{S}{s}$ está \textit{bloqueada} si no existe $\gamma$ tal que $\la{S}{s} \dto \gamma$. Una secuencia de derivación es finita cuando llega a un bloqueo o a un estado final:
\[
    \gamma_0 \dto \gamma_1 \dto ... \dto \gamma_k
\]
donde $\gamma_0 = \la{S}{s}$,  $\gamma_i \dto \gamma_{i+1}$ para $i\in\{0, ..., k-1\}$ y $\gamma_k$ es una configuración bloqueada.
\end{definition}

Normalmente escribiremos $\gamma_0 \dto^i \gamma$ si hay $i$ pasos en la ejecución de $\gamma_0$ a $\gamma$. Si hay finitos pasos, denotamos $\gamma_0 \dto^* \gamma$. $\gamma_0 \dto^i \gamma$ y $\gamma_0 \dto^* \gamma$ no tiene por qué ser secuencias de derivación, solo si $\gamma$ es configuración final o de bloqueo.

\begin{definition}
La ejecución $\la{S}{s}$ de la expresión $S$ en un estado $s$:
\begin{enumerate}
    \item \textit{Termina} si existe una única secuencia de derivación finita comenzando en $\la{S}{s}$.

    \item \textit{Termina con éxito} si $\la{S_1}{s} \dto ^* s'$ para algún estado $s'$.
    
    \item \textit{Cicla} si existe una secuencia de derivación infinita comenzando en $\la{S}{s}$.
\end{enumerate}
Nótese que estas definiciones son mutuamente excluyentes si y solo si las secuencias de derivacion son únicas. Por comodidad, las definimos de este modo porque, si extendemos el lenguaje, no nos tendremos que preocupar.
\end{definition}

\begin{example}\label{examplerepeat}
Supongamos que queremos extender $\nn{While}_\nn{sos}$ con la expresión $\n{repeat }S \n{ until }b$. Podemos añadir la regla:
\begin{prooftree}
        \AxiomC{}
        \LeftLabel{$[\nn{repeat}_\nn{sos}]$}
        \RightLabel{}
        \UnaryInfC{$\la{\n{repeat }S\n{ until }b}{s}\dto \la{S; \n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s}$}
\end{prooftree}
La idea es que la expresión $\n{repeat }S\n{ until }b$ sea equivalente a $S;\n{ while }\neg b\n{ do } S$. Se definirá posteriormente el concepto de equivalencia semántica y se demostrará este resultado.
\end{example}

\subsection{Propiedades}

El método de demostración principal consiste en hacer \textit{inducción sobre la longitud de las secuencias de derivación} (finitas) que se estudian, es decir, si queremos demostrar una propiedad acerca de nuestro sistema de transiciones:
\begin{itemize}
    \item Demostramos que la propiedad se cumple para secuencias de derivación de longitud 0 (en ocasiones nos encontraremos que se cumple la propiedad de forma vacía).
    \item Demostramos que si la propiedad se cumple para secuencias de longitud (a lo sumo) $k$, entonces se cumple para secuencias de longitud $k+1$.
\end{itemize}
A modo de ejemplo de este método, veamos el siguiente resultado:

\begin{lema}\label{lemasos1}
Si $\la{S_1;S_2}{s}\dto^k s''$, entonces existen $s'\in \mathbf{State}$, $k_1, k_2 \in \N$ tales que $k = k_1 + k_2$ y $$\la{S_1}{s}\dto^{k_1}s' \quad \text{ y }\quad \la{S_2}{s'}\dto^{k_2}s''.$$
\end{lema}
\begin{proof}
Si $k=0$, entonces $\la{S_1;S_2}{s}\dto^0 s''$ implica (vacuamente) el resultado, porque $\la{S_1;S_2}{s}$ y $s''$ son distintos. Supongamos que el resultado se cumple para longitudes menores o iguales que $k$. Veamos que se sigue para $k+1$. Por tanto, tenemos la premisa $\la{S_1;S_2}{s}\dto^{k+1} s''$, es decir, que existe una configuración $\gamma$ tal que
$$\la{S_1;S_2}{s}\dto \gamma \dto^{k} s''$$
Por tanto, distinguimos dos casos según la regla que hemos aplicado a $\la{S_1;S_2}{s}$ para llegar a $\gamma$:
\begin{itemize}
    \item[(a)] Si hemos aplicado [$\nn{comp}^1_\nn{sos}$], tenemos que
\begin{prooftree}
    \AxiomC{$\la{S_1}{s} \dto \la{S_1'}{s'}$}
    \LeftLabel{$[\text{comp}_{\nn{sos}}^1]$}
    \UnaryInfC{ $\la{S_1; S_2}{s} \dto \la{S_1'; S_2}{s'}= \gamma$}
\end{prooftree}
luego $\la{S_1'; S_2}{s'} \dto^k s''$. Entonces, como esta derivación es de longitud $k$, podemos aplicar hipótesis de inducción, esto es, existen $s_0 \in \mathbf{State}$ y $k_1, k_2 \in \N$ con $k = k_1 + k_2$ y 
$$\la{S_1'}{s'}\dto^{k_1}s_0 \quad \text{ y }\quad \la{S_2}{s_0}\dto^{k_2}s''.$$
Ahora bien, como tenemos la premisa $\la{S_1}{s} \dto \la{S_1'}{s'}$ y $\la{S_1'}{s'}\dto^{k_1}s_0$, entonces tenemos que $\la{S_1}{s}\dto^{k_1 + 1}s_0$. Por otro lado, también tenemos $\la{S_2}{s_0}\dto^{k_2}s''$ y que $(k_1 + 1) + k_2 = (k_1 + k_2)+1 = k+1$. Es decir, hemos obtenido la conclusión deseada. Por tanto, hemos probado el resultado para este caso.

\item[(b)] Si hemos aplicado [$\nn{comp}^2_\nn{sos}$], tenemos que
\begin{prooftree}
    \AxiomC{$\la{S_1}{s} \dto s'$}
    \LeftLabel{[$\nn{comp}^2_\nn{sos}$]}
    \UnaryInfC{ $\la{S_1; S_2}{s} \dto \la{S_2}{s'}= \gamma$}
\end{prooftree}
Entonces deducimos que $\la{S_2}{s'} \dto^{k}s''$. Simplemente tomando $k_1 := 1$ y $k_2 := k$ vemos que $k_1+k_2 = k+1$ y que tenemos el resultado.
\end{itemize}
\end{proof}

\begin{example}
Por otro lado, $\la{S_1;S_2}{s}\dto^* \la{S_2}{s'}$ no implica necesariamente que $\la{S_1}{s}\dto^* s'$. Por ejemplo, podemos tomar $S_1 := \n{skip}$, $S_2 := \n{while }\neg(\n{x}=1)\n{ do } \n{x}:=\n{x}+1$ y $s\n{x} = 3$, $s'\n{x} = s[\n{x}\mapsto 2]$.
\end{example}


El siguiente lema viene a decir que la ejecución de una expresión es independiente de cualquier enunciado que se ejecute después:

\begin{lema}\label{lemasos2}
Si $\la{S_1}{s}\dto^k s'$, entonces $\la{S_1;S_2}{s}\dto^k \la{S_2}{s'}$.
\end{lema}
\begin{proof}
Por inducción sobre la longitud de las derivaciones. En caso de $k=0$, la premisa es falsa y el resultado se tiene directamente. Supongamos que se cumple el resultado para longitudes $\leq k$ y veámoslo para $k+1$. Nuestra suposición es que $\la{S_1}{s}\dto^{k+1} s'$. Entonces tenemos que hay cierta configuración $\gamma$ con 
$$\la{S_1}{s}\dto \gamma \dto^k s'$$
y además, notemos que $\gamma = \la{S}{s''}$ porque $k\leq 1$. Pero entonces, aplicando la hipótesis de inducción a $\la{S}{s''} \dto^k s'$, tenemos que $\la{S;S_2}{s''}\dto^k \la{S_2}{s'}$. 

Por otro lado, de $\la{S_1}{s}\dto \la{S}{s''}$ podemos deducir que:
\begin{prooftree}
    \AxiomC{$\la{S_1}{s} \dto \la{S}{s''}$}
    \LeftLabel{$[\text{comp}_{\nn{sos}}^1]$}
    \UnaryInfC{ $\la{S_1; S_2}{s} \dto \la{S; S_2}{s''}$}
\end{prooftree}
Es decir, sabemos que $\la{S_1; S_2}{s} \dto \la{S; S_2}{s''}$ y que $\la{S;S_2}{s''}\dto^k \la{S_2}{s'}$. Basta componer ambas derivaciones para ver que $\la{S_1; S_2}{s}\dto^{k+1} \la{S_2}{s'}$, como queríamos.
\end{proof}

\begin{theorem}\label{teosos}
El sistema de transiciones $\nn{While}_\nn{sos}$ es determinista, es decir, para cualesquiera $S, s, \gamma, \gamma'$ tenemos que
$$\la{S}{s}\dto \gamma \text{ y } \la{S}{s}\dto \gamma' \text{ implica que } \gamma = \gamma'$$
\end{theorem}
\begin{proof}
Véase la demostración del Teorema \ref{determinismo}.
\end{proof}

\begin{definition}
Dos expresiones $S_1, S_2$ se dicen \textit{semánticamente equivalentes} si, para cada $s \in \mathbf{State}$, 
\begin{itemize}
    \item Si $\gamma$ es estado final o bloqueado, entonces $\la{S_1}{s}\dto^* \gamma$ si y solo si $\la{S_2}{s} \dto^*\gamma$. Nótese que las longitudes de las derivaciones no tienen por qué coincidir.
    \item La\footnote{La unicidad viene dada por el determinismo de $\nn{While}_\nn{sos}$.} secuencia de derivación empezando en $\la{S_1}{s}$ es infinita si y solo si lo es la que empieza en $\la{S_2}{s}$.
\end{itemize} 
\end{definition}

\begin{example}
Veamos que $S$ y $S; \n{skip}$ son semánticamente equivalentes. Supongamos que $\la{S}{s}\dto^*s'$, es decir, existe $k\in\N$ tal que $\la{S}{s}\dto^*s'$. Entonces, el Lema \ref{lemasos2} nos dice que dado $\la{S}{s}\dto^k s'$ se tiene
\[
    \la{S; \n{skip}}{s}\dto^k \la{ \n{skip}}{s'}
\]
Por la regla $[\nn{skip}_\nn{sos}]$ se deduce $\la{ \n{skip}}{s'} \dto s'$ y entonces
\[
    \la{S;  \n{skip}}{s} \dto^* s'
\]
Supongamos ahora que $\la{S; \n{skip}}{s}\dto^*s''$, entonces existe $k\in\N$ tal que  $\la{S; \n{skip}}{s}\dto^k s''$. Por el Lema \ref{lemasos1} se tiene la existencia de $s'\in\textbf{State}$ y $k_1,k_2\in\N$ tal que $k = k_1 + k_2$ y
\[
    \la{S}{s}\dto^{k_1} s'\ \ y\ \ \la{\n{skip}}{s'}\dto^{k_2} s''
\]
La secuencia $\la{\n{skip}}{s'}\dto^{k_2} s''$ es cierta si y solo si $k_2 = 1$ y $s' = s''$ pues solo se puede aplicar $[\nn{skip}_\nn{sos}]$, se deduce entonces
\[
    \la{S}{s}\dto^{k_1} s''
\]
es decir, $\la{S}{s}\dto^{*} s''$.
\end{example}

\begin{example} Definimos en \ref{examplerepeat} la sentencia $\n{repeat }S\n{ until }b$ y dejamos por hacer la demostración de su equivalencia con $S;\n{ while }\neg b\n{ do } S$. Hay que probar que para cada $s, s'\in\textbf{State}$ sucede que
\[
    \la{\n{repeat }S\n{ until }b}{s} \dto^* s' \Longleftrightarrow \la{S;\n{ while }\neg b\n{ do } S}{s} \dto^* s'
\]
$\Longrightarrow)$ Supongamos que  
\[
    \la{\n{repeat }S\n{ until }b}{s} \dto^* s'
\]
Sabemos por la regla $[\nn{repeat}_\nn{sos}]$
\[
    \la{\n{repeat }S\n{ until }b}{s} \dto^* s'  \implies \la{S;\n{ if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s} \dto^* s'
\]
y por el lema \ref{lemasos1} existen $k_1, k_2\in\N$ tal que
\[
    \la{S}{s} \dto^{k_1} s''
\]
y
\[
    \la{\n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s''} \dto^{k_2} s'
\]
Dividimos en casos en función del valor booleano de $b$:
\begin{itemize}
    \item $\fc{B}{b}s'' = \textbf{tt}$. Usando el axioma $[\nn{if}^\nn{tt}_{sos}]$ seguido de $[\nn{skip}_\nn{sos}]$ se tiene
    \begin{eqnarray*}
        \la{\n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s''} &\overset{[\nn{if}^\nn{tt}_{sos}]}{\dto}& \la{\n{skip}}{s''} \\
        &\overset{[\nn{skip}_\nn{sos}]}{\dto}& s''
    \end{eqnarray*}
    de lo que se deduce, por determinismo, que  $s' = s''$.
    Desarrollemos ahora $\la{S;\n{ while }\neg b\n{ do } S}{s}$. Por el lema \ref{lemasos2}, como sabemos que $\la{S}{s} \dto^{k_1} s''$, deducimos que
    \[
        \la{S;\n{ while }\neg b\n{ do } S}{s} \dto^{k_1} \la{\n{while }\neg b\n{ do } S}{s''}
    \]
    Aplicando $[\nn{while}_{sos}]$ deducimos $\la{\n{if }\neg b\n{ then } S;\n{ while }\neg b\n{ do }S\n{ else skip}}{s''}$ y como $\fc{B}{\neg b} = \textbf{ff}$ entonces
    \begin{eqnarray*}
            \la{\n{if }\neg b\n{ then } S;\n{ while }\neg b\n{ do }S\n{ else skip}}{s''} \dto &\overset{[\nn{if}^\nn{ff}_{sos}]}{\implies}& \la{\n{skip}}{s''} \\
            &\overset{[\nn{skip}_\nn{sos}]}{\implies}& s''
    \end{eqnarray*}
    concluyendo que $\la{S;\n{ while }\neg b\n{ do } S}{s} \dto^* s'$, como queríamos probar.
    \item $\fc{B}{b}s'' = \textbf{ff}$. Aplicando $[\nn{if}_\nn{ff}]$ se tiene
    \begin{eqnarray*}
        \la{\n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s''} &\overset{[\nn{if}^\nn{tt}_{sos}]}{\dto}& \la{\n{repeat }S\n{ until }b}{s''}
    \end{eqnarray*}
    y esta última sentencia $\dto^* s'$, por determinismo. Por hipótesis de inducción se deduce de $$\la{\n{repeat }S\n{ until }b}{s''} \dto^* s'$$ que
    \[
        \la{S;\n{ while }\neg b\n{ do } S}{s''} \dto^* s'
    \]
    y por el lema \ref{lemasos2} y aplicando $[\nn{while}_\nn{sos}]$
    \begin{eqnarray*}
        \la{S;\n{ while }\neg b\n{ do } S}{s}  \dto^* \la{\n{ while }\neg b\n{ do } S}{s''} \dto \la{\n{if }\neg b\n{ then } S;\n{ while }\neg b\n{ do }S\n{ else skip}}{s''}
    \end{eqnarray*}
    Dado que $\fc{B}{\neg b}s'' = \textbf{tt}$ se tiene 
    \[
        \la{\n{if }\neg b\n{ then } S;\n{ while }\neg b\n{ do }S\n{ else skip}}{s''} \dto \la{S;\n{ while }\neg b\n{ do } S}{s''} \dto^* s'
    \]
    cocluyendo el resultado $\la{S;\n{ while }\neg b\n{ do } S}{s} \dto^* s'$.
\end{itemize}
$\Longleftarrow)$ Suponemos $\la{S;\n{ while }\neg b\n{ do } S}{s} \dto^* s'$. Nuevamente por el lema \ref{lemasos1} se tienen $k_1, k_2\in\N$ y $s''\in\State$ tal que
\[
    \la{S}{s} \dto^{k_1} s''\ \ \ y\ \ \ \la{\n{while }\neg b\n{ do } S}{s''} \dto^{k_2} s'
\]
De $[\nn{while}_\nn{sos}]$ se tiene
\[
    \la{\n{while }\neg b\n{ do } S}{s''} \dto \la{\n{if }\neg b\n{ then } S;\n{ while }\neg b\n{ do }S\n{ else skip}}{s''}
\]
Se divide en casos según $\fc{B}{b}s''$:
\begin{itemize}
    \item Si $\fc{B}{b}s'' = \textbf{tt}$ ($\fc{B}{\neg b}s'' = \textbf{ff}$) entonces se aplica $[\nn{if}_\nn{sos}^\nn{ff}]$ y $[\nn{skip}_\nn{sos}]$ para deducir 
    \[
        \la{\n{if }\neg b\n{ then } S;\n{ while }\neg b\n{ do }S\n{ else skip}}{s''} \dto \la{\n{skip}}{s''} \dto s''
    \]
    y como $\la{\n{while }\neg b\n{ do } S}{s''} \dto^k_1 s'$, por determinismo debe suceder $s' = s''$. Veamos que la sentencia del $\n{repeat}$ lleva al estado $s'$. Aplicamos la regla $[\nn{repeat}_\nn{sos}]$ para obtener
    \[
        \la{\n{repeat }S\n{ until }b}{s} \dto \la{S; \n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s}
    \]
    Ahora como $\la{S}{s} \dto^{k_1} s''$ aplicando el lema \ref{lemasos2} se consigue que 
    \[
        \la{S;\n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s} \dto^{k_1} \la{\n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s''}
    \]
    Y ahora como $\fc{B}{b}s'' = \textbf{tt}$ se consigue mediante $[\nn{if}_\nn{sos}^\nn{tt}]$ y $[\nn{skip}_\nn{sos}]$
    \[
        \la{\n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s''} \dto \la{\n{skip}}{s''} \dto s''
    \]
    Dado que $s' = s''$ se consigue finalmente
    \[
         \la{\n{repeat }S\n{ until }b}{s} \dto^* s'
    \]
    \item Si $\fc{B}{b}s'' = \textbf{ff}$ ($\fc{B}{\neg b}s'' = \textbf{tt}$) entonces toca aplicar la regla $[\nn{if}_\nn{sos}^\nn{tt}]$
    \begin{eqnarray*}
        \la{\n{if }\neg b\n{ then } S;\n{ while }\neg b\n{ do }S\n{ else skip}}{s''} &\dto& \la{S; \n{while }\neg b\n{ do }S}{s''} \\
        &\dto^*& s'
    \end{eqnarray*}
    Donde en el último paso se ha aplicado determinismo.
    Volvemos a aplicar lo mismo de antes para el $\n{repeat}$
    \begin{eqnarray*}
        \la{\n{repeat }S\n{ until }b}{s} &\overset{[\nn{repeat}_\nn{sos}]}{\dto}& \la{S; \n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s} \\
        &\overset{\ref{lemasos2}}{\dto}& \la{\n{if }b\n{ then skip else }(\n{repeat }S\n{ until }b)}{s''} \\
        &\overset{[\nn{if}_\nn{sos}^\nn{ff}]}{\dto}& \la{\n{repeat }S\n{ until }b}{s''}
    \end{eqnarray*}
    Por hipótesis de inducción se tiene que
    \[
        \la{\n{repeat }S\n{ until }b}{s''} \dto^* s' \Longleftrightarrow \la{S; \n{while }\neg b\n{ do }S}{s''} \dto^* s'
    \]
    de donde se deduce que $\la{\n{repeat }S\n{ until }b}{s''} \dto^* s'$ y finalmente
    \[
         \la{\n{repeat }S\n{ until }b}{s} \dto^* s'
    \]
\end{itemize}
\end{example}
\subsection{Expresiones}

Análogamente a como hicimos en la semántica de paso largo, podemos definir el valor semántico de las expresiones mediante una función parcial $\mc{S}_\nn{sos}: \mathbf{Stm}\rightarrow (\mathbf{State}\hookrightarrow\mathbf{State})$, donde
\begin{align*}
    \mc{S}_\nn{sos}[[S]]:  \mathbf{State} & \hookrightarrow  \mathbf{State} \\
                     s               & \mapsto          \begin{cases} s' \text{, si } \la{S}{s}\dto^* s' \\ 
                        \n{indefinido} \text{, en otro caso}
                        \end{cases}
\end{align*}
Notemos que esta función está bien definida precisamente por el determinismo que vimos en el anterior apartado. La ejecución de $\la{S}{s}$ para una expresión $S$ dada una configuración inicial $s\in\textbf{State}$ puede dar lugar a tres casos
\begin{itemize}
    \item Que termine, y entonces existe $s'\in\textbf{State}$ tal que
    \[
        s\in\textbf{State} \dto^* s'
    \]
    y entonces $\mc{S}_\nn{sos}[[S]]s = s'$
    \item Que se quede bloqueada, y entonces no queda otra que $\mc{S}_\nn{sos}[[S]]s = \n{indefinido}$.
    \item Que cicle, ocurriendo nuevamente que $\mc{S}_\nn{sos}[[S]]s = \n{indefinido}$.
\end{itemize} 
La equivalencia semántica coincide $\mc{S}_\nn{sos}$ en el sentido de la siguiente proposición: \\

\begin{prop} Si $S_1$ y $S_2$ son semánticamente equivalente entonces
\[
        \mc{S}_\nn{sos}[[S_1]] = \mc{S}_\nn{sos}[[S_2]]
\] 
\begin{proof} Hay que probarlo particularizando en cada $s\in\textbf{State}$ \\ \\
Supongamos que $S_1$ y $S_2$ son semánticamente equivalentes. Se distinguen dos casos
\begin{itemize}
    \item Existe un estado final $s'\in\textbf{State}$ tal que
    \[
        \la{S_1}{s}\dto^* s'\ \ y\ \ \la{S_2}{s} \dto^* s'
    \]
    y trivialmente
    \[
        \mc{S}_\nn{sos}[[S_1]]s = s' =  \mc{S}_\nn{sos}[[S_2]]s
    \]
    \item Ambas secuencias son infinitas, es decir
    \[
        \la{S_1}{s}\text{ es infinita si y solo si } \la{S_2}{s} \text{ es infinita}
    \]
    y entonces
    \[
        \mc{S}_\nn{sos}[[S_1]]s = \n{indefinido} =  \mc{S}_\nn{sos}[[S_2]]s
    \]
\end{itemize}
\end{proof}
\end{prop}
\noindent La implicación contraria no es cierta, pues si $S_1$ es una sentencia que cicla y $S_2$ es una sentencia que se bloquea, $ \mc{S}_\nn{sos}[[S_1]] = \n{indefinido} = \mc{S}_\nn{sos}[[S_2]]$ pero $S_1$ y $S_2$ no son semánticamente equivalentes.

\section{Teorema de equivalencia}

Hasta ahora hemos presentado por separado los dos sistemas de transiciones para $\nn{While}$, y hemos visto que tienen comportamientos, en general, distintos. Sin embargo, si vemos la semántica de paso largo como una extensión de la de paso corto, podemos convencernos que son esencialmente los mismo. De hecho, tienen el mismo poder expresivo. Más precisamente, el resultado clave de esta sección es:

\begin{theorem}[De equivalencia]\label{theq}
Consideremos el lenguaje $\nn{While}$. Para cada $S \in \mathbf{Stm}$, $\mc{S}_\nn{ns}[[S]] = \mc{S}_\nn{sos}[[S]]$.
\end{theorem}
\begin{proof}
La demostración se divide en dos pasos, cada uno consiste en demostrar uno de los siguientes lemas:
\begin{lema}
Para cada $S \in \mathbf{Stm}$, dados $s, s' \in \mathbf{State}$, $\la{S}{s}\rightarrow s'$ implica que $\la{S}{s}\dto^* s'$.
\end{lema}
\begin{proof}
La demostración vuelve a ser rutinaria, es decir, por inducción en la forma del árbol de derivación. Los casos base son:
\begin{itemize}
    \item[($\nn{ass}_\nn{ns}$)] Si suponemos que $\la{x:=a}{s}\to s$, el axioma $[\nn{ass}_\nn{sos}]$ nos da el resultado.
    \item[($\nn{skip}_\nn{ns}$)] Análogo.
\end{itemize}
Los casos inductivos son:
\begin{itemize}
    \item[($\nn{comp}_\nn{ns}$)]  Supongamos que $\la{S_1;S_2}{s}\to s''$. Esto necesariamente se ha deducido de las premisas $\la{S_1}{s}\to s'$ y $\la{S_2}{s'}\to s''$ y, aplicando la hipótesis de inducción, $\la{S_1}{s}\dto^*s'$ y $\la{S_2}{s'}\dto^* s''$. Por el Lema \ref{lemasos2}, $\la{S_1;s_2}{s}\dto^* \la{S_2}{s'}\dto^* s''$.
    \item[($\nn{if}_\nn{ns}^\nn{tt}$)] Supongamos que hemos obtenido $\la{\n{if }b \n{ then }S_1\n{ else }S_2}{s}\to s'$ a partir de $\fc{B}{b}s = \mathbf{tt}$ y $\la{S_1}{s}\to s'$. Pero entonces, aplicando $[\nn{if}_\nn{sos}^\nn{tt}]$, $\la{\n{if }b \n{ then }S_1\n{ else }S_2}{s}\dto \la{S_1}{s}$ y, por la hipótesis de inducción en $\la{S_1}{s}\to s'$, $\la{S_1}{s}\dto^* s'$.
    \item[($\nn{if}_\nn{ns}^\nn{ff}$)] Análogo.
    \item[($\nn{while}_\nn{ns}^\nn{tt}$)] Supongamos que $\la{\n{while }b \n{ do }S}{s}\to s''$ se ha deducido de las premisas $\fc{B}{b}s = \mathbf{tt}$, $\la{S}{s}\to s'$ y $\la{\n{while }b \n{ do }S}{s'}\to s''$. La hipótesis de inducción en las dos últimas nos da que $\la{S}{s}\dto^* s'$ y que $\la{\n{while }b \n{ do }S}{s'}\dto^* s''$. Por el Lema \ref{lemasos2}, 
    $$\la{S_1;\n{while }b \n{ do }S}{s} \dto^* \la{\n{while }b \n{ do }S}{s'}\dto^* s''$$
    Juntando ésto y aplicando en orden $[\nn{while}_\nn{sos}^\nn{tt}]$ y $[\nn{if}_\nn{sos}^\nn{tt}]$, 
    $$\la{\n{while }b \n{ do }S}{s} \dto \la{\n{if }b\n{ then }(S; \n{while }b \n{ do }S) \n{ else skip}}{s} \dto \la{S;\n{while }b \n{ do }S}{s}\dto^* s''$$
    \item[($\nn{while}_\nn{ns}^\nn{ff}$)] Análogo.
\end{itemize}
\end{proof}

\begin{lema}
Para cada $S \in \mathbf{Stm}$, dados $s, s' \in \mathbf{State}$ y $k \in \N$, $\la{S}{s}\dto^k s'$ implica que $\la{S}{s}\to s'$.
\end{lema}
\begin{proof}
Se demuestra por inducción en la longitud de las secuencias de derivación. El caso base es $k=0$ y, como la premisa es falsa, la implicación es cierta directamente.
\\

Supongamos que el resultado se cumple si $k \leq k_0$ y veamos que es cierto para $k_0 +1$. Tenemos que distinguir casos en función de la regla que ha sido aplicada para obtener el primer paso de la derivación $\la{S}{s}\dto^{k_0+1}s'$.
\begin{itemize}
    \item[($\nn{ass}_\nn{sos}$)] Es evidente porque no requiere ninguna premisa. Además, $k_0 = 0$ (se obtiene la derivación en un paso).
    \item[($\nn{skip}_\nn{sos}$)] Análogo.
    \item[($\nn{comp}_\nn{sos}^{1, 2}$)] Supongamos que $\la{S_1;S_2}{s}\dto^{k_0+1}s''$. Por el Lema \ref{lemasos1}, existen un estado $s'$ y enteros $k_1 + k_2 = k_0 + 1$ tales que 
    $$\la{S_1}{s}\dto^{k_1}s' \quad \text{ y } \quad \la{S_2}{s'}\dto^{k_2}s''.$$
    Como $k_1, k_2 \leq k_0$, podemos aplicar la hipótesis de inducción en cada caso, y obtenemos que $\la{S_1}{s}\to s'$ y $\la{S_2}{s'}\to s''$. Aplicando $[\nn{comp}_\nn{ns}]$, obtenemos que $\la{S_1;S_2}{s}\to s''$.
    \item[($\nn{if}_\nn{sos}^\nn{tt}$)] Supongamos que el primer paso es de la forma:
    $$\la{\n{if }b\n{ then }S_1\n{ else }S_2}{s}\dto \la{S_1}{s} \dto^{k_0} s'$$
    es decir, con $\fc{B}{b}s = \mathbf{tt}$. Aplicando la hipótesis de inducción a la segunda secuencia, $\la{S_1}{s} \to s'$, luego basta aplicar $[\nn{if}_\nn{ns}^\nn{tt}]$ para tener el resultado.
    \item[($\nn{if}_\nn{sos}^\nn{ff}$)] Análogo.
    \item[($\nn{while}_\nn{sos}$)] Supongamos que tenemos:
    $$\la{\n{while }b \n{ do }S}{s}\dto \la{\n{if }b \n{ then }(S; \n{while }b\n{ do }S)\n{ else skip}}{s} \dto^{k_0}s''$$
    Aplicando la hipótesis de inducción al segundo paso, $\la{\n{if }b \n{ then }(S; \n{while }b\n{ do }S)\n{ else skip}}{s} \to s''$. Por el Lema \ref{lemans}, tenemos el resultado.
\end{itemize}
\end{proof}

Entonces, dados $S \in \mathbf{Stm}$, $s\in \mathbf{State}$, por los dos lemas se tiene que $\mc{S}_\nn{ns}[[S]] = s'$ si y solo si $\mc{S}_\nn{sos}[[S]] = s'$. Pero entonces obtenemos que, si una de las dos funciones está definida en un estado o no, la otra lo estará también y coincidirá con ella o no estará definida, respectivamente. Es decir, ambas funciones coinciden.
\end{proof}