\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[spanish]{babel}
\usepackage{amssymb}
\usepackage{amsmath}

\newcommand{\car}{\curvearrowright}
\newcommand{\lrh}{\leftrightharpoons}

\title{Funcionalidades complejas de lenguajes imperativos}
\author{Carlos S. Galindo Jiménez}

\begin{document}
	\maketitle
	\begin{enumerate}
		\item \texttt{halt}, concluye la ejecución, y la memoria debe ser conservada. Ejemplo: \texttt{x:=0; halt; y:=0;} termina con \texttt{x -> 0}
		$$exp(\texttt{halt}) \car K | \sigma_n \lrh \sigma_n$$
		\item \texttt{and-then}, ``and'' con cortocircuito. Sólo evalúa el segundo argumento si el primero es cierto. Para este fin se puede emplear una estructura similar a la utilizada para los condicionales, sólo que limitamos las expresiones al tipo booleano.
		\begin{align*}
		exp(BE \texttt{ and-then } BE', Env) \car K \lrh \\
		exp(BE, Env) \car \texttt{and-then} \car exp(BE', Env) \car K
		\end{align*}
		$$val(true) \car \texttt{and-then} \car exp(BE', Env) \car K \lrh exp(BE', Env) \car K$$
		$$val(false) \car \texttt{and-then} \car exp(BE', Env) \car K \lrh val(false) \car K$$

		\item \texttt{exp++}, incrementa un valor después de accederlo. Se debe depositar en lo alto de la pila el valor solicitado, y encima de éste, incrementar el valor en memoria. En este caso, vamos a restringir \texttt{exp} a ser una variable, puesto que otras expresiones no están guardadas en un entorno o en memoria.
		\begin{align}
		exp(X\texttt{++}, Env) \car K | Mem \lrh \\
		val(Mem[Env[X]]) \car \texttt{++} \car exp(X = X + 1, Env) \car K | Mem \lrh^* \\
		val(V) \car \texttt{++} \car \exp(X = X + 1, Env) \car K | Mem\lrh \\
		exp(X = X + 1, Env) \car val(V) \car K | Mem \lrh \\
		exp(X + 1, Env) \car writeTo(Env[X]) \car val(V) \car K | Mem \lrh \\
		val(V) \car K | Mem
		\end{align}
		Para leer la expresión, como se detalla en las ecuaciones anteriores, habría que obtener el valor ($V$) de $X$, tal y como se indica en los pasos 2 y 3. A continuación, debemos invertir el orden del incremento y el valor en la pila (paso 4). Finalmente, se evalúa la expresión $X + 1$ y se guarda en $X$ (5), quedando en el último paso el valor y el resto de la pila.
	\end{enumerate}
\end{document}