funcional.tex

\section{Paradigma Funcional}

\subsection{Características generales}

\begin{itemize}
  \item Computación expresada a través de la aplicación y composición de funciones.
  \item No hay un estado global.
  \item Los estados intermedios (salidas de las funciones) son pasados directamente a otras funciones como argumentos.
  \item Repetición basada en recursión.
  \item Expresiones tipadas.
  \item Tiene un \xbf{alto nivel de abstracción}: tiende a ser una \xit{especificación ejecutable}.
  \item Es \xbf{declarativo}: la máquina se encarga de buscar el \xit{cómo} y nosotros elegimos el \xit{qué}.
  \item La matemática y razonamiento algebraico tienden a ser más elegantes.
  \item En el pasado: ejecución más lenta. Hoy en día no está tan claro que sea así.
\end{itemize}

\subsection{Fundamentos}

\begin{itemize}
  \item Se enfoca en la transformación de la información, y no tanto en la interacción con el medio.
  \item \xbf{Valores:} entidades (matemáticas) abstractas con ciertas propiedades.
  \item \xbf{Expresiones:} cadenas de símbolos utilizadas para denotar valores. Se dividen en:
    \begin{itemize}
      \item Atómicas: llamadas también formas normales. Ejemplo: \xtt{2, False, (3, True)}.
      \item Compuestas: se \xit{arman} combinando subexpresiones. Ejemplo: \xtt{(1+1), (2==1)}.
    \end{itemize}
    Y pueden estar bien o mal formadas, dependiendo de las reglas sintácticas y de las reglas de asignación de tipos.
  \item \xbf{Funciones:} son valores especiales que representan ``transformaciones de datos''. Nótese que al ser valores, pueden ser argumento de otras funciones, resultado, almacenarse en estructuras de datos, ser estructuras de datos, etc. Llamamos funciones de \xbf{alto orden} a las funciones que trabajan con funciones.
  \item \xbf{Transparencia referencial:} el valor de una expresión depende sólo de los elementos que la constituyen. Esto implica, por ejemplo, que los detalles de ejecución no influencian el comportamiento del programa. Además, existe la posibilidad de demostrar propiedades usando las propiedades de las subexpresiones y métodos de deducción lógica.
  \item \xbf{Ecuaciones orientadas:} tienen la forma $e_1 = e_2$, donde $e_1$ y $e_2$ expresan el mismo valor. Decimos que están orientadas porque se puede utiliza $e_2$ para reemplazar una aparición de $e_1$ en alguna expresión (pero no al revés).
  \item \xbf{Programa funcional:} es un conjunto de ecuaciones que definen una o más funciones. Para usarlo, resolvemos la reducción de la aplicación de una función a sus datos (reducción de una expresión).
\end{itemize}

Decimos que un \xbf{Lenguaje funcional puro} es aquel que es un ``lenguaje de expresiones con transparencia referencial y funciones como valores, cuyo modelo de cómputo es la reducción realizada mediante el remplazo de iguales por iguales''.

\subsection{Tipos}

Toda expresión válida denota un valor. Además, todo valor pertenece a un conjunto, y los tipos denotan conjuntos.
Es decir, toda expresión debería tener un tipo para ser válida.

\paragraph{Asignación de tipos:} se puede realizar de dos formas:

\begin{itemize}
  \item De manera explícita, con la sintaxis \xtt{e :: A}, que dice que la expresión \xtt{e} tiene tipo \xtt{A}.
  \item De manera implícita. Se infiere por el contexto en el cual se usa la expresión.
\end{itemize}

\paragraph{Inferencia de tipos:} dada una expresión \xtt{e}, determinar si tiene tipo o no según las reglas, y cuál es ese tipo.

\paragraph{Chequeo de tipos:} dada una expresión \xtt{e} y un tipo \xtt{A}, determinar si \xtt{e} tipa \xtt{A} (\xtt{e :: A}) según las reglas, o no.

\paragraph{Sistema de tipado fuerte (strong typing):} acepta una expresión si, y solo si, ésta tiene tipo según las reglas.

\paragraph{Sistema de Hindley-Milner} es un sistema de tipos que propone:

\begin{itemize}
  \item Tipos básicos:
    \begin{itemize}
      \item Enteros: \xtt{Int}
      \item Caracteres: \xtt{Char}
      \item Booleanos: \xtt{Bool}
    \end{itemize}
  \item Tipos compuestos:
    \begin{itemize}
      \item Tuplas: \xtt{(A,B)}
      \item Listas: \xtt{[A]}
      \item Funciones: \xtt{(A -> B)}
    \end{itemize}
  \item \xbf{Polimorfismo:} permite que una expresión tenga más de un sólo tipo. El polimorfismo paramétrico soluciona esto usando \xbf{variables de tipos}, ejemplo: \xtt{id :: a -> a}.
\end{itemize}

\subsubsection{Tipos algebraicos} Es un conjunto de valores junto con las operaciones que se les pueden realizar.

\subsubsection{Tipo abstracto (TAD)}

\subsubsection{Pattern matching} Es un mecanismo para acceder a los parámetros con los que fue construido un Tipo Algebraico. \xbf{Pattern} es una expresión utilizando constructores y variables sin repetir. \xbf{Matching} es la operación que dice si una expresión es de la forma de un patrón.

\subsubsection{Tipos algebraicos recursivos} Representan conjuntos inductivos. Al menos un constructor debe tener al menos un parámetro de tipo sí mismo.

\subsection{Currificación}

Establece una correspondencia entre cada función de múltiples parámetros, y una de alto orden que retorna una función intermedia que completa el trabajo. Es decir, por cada \xtt{f'} definida como:
\begin{lstlisting}[language=Haskell]
f' :: (a,b) -> c
f' (x,y) = e
\end{lstlisting}

siempre se puede escribir

\begin{lstlisting}[language=Haskell]
f :: a -> (b -> c)
(f x) y = e
\end{lstlisting}

O sea, que hay una correspondencia entre los tipos \xtt{(a,b) -> c} y \xtt{a -> (b -> c)}. Y se pueden hacer funciones \xtt{curry :: ((a,b) -> c) -> (a -> (b -> c))} y \xtt{uncurry :: (a -> (b -> c)) -> ((a,b) -> c)} que transformen funciones de un tipo al otro.

\xit{Nota:} tener en cuenta que decir si algo está currificado o no puede ser una cuestión de interpretación. El ejemplo canónico es la función \xtt{distance :: (Int, Int) -> Int} que calcula la distancia euclidea de un punto al origen. Uno podría querer currificar el primer parámetro, pero entonces quizás sería menos obvio que la función espera un punto.

\subsection{Haskell}

\subsubsection{Repaso}

\begin{itemize}
  \item La evaluación consiste en aplicar ecuaciones (orientadas de izquierda a derecha).
  \item Definición de funciones por casos.
  \item Tipos básicos: \xtt{Int}, \xtt{Bool}, \xtt{Float}, \xtt{Pares}, \xtt{Listas}, \xtt{Funciones}, etc.
  \item No toda evaluación termina.
  \item Utiliza evaluación \xit{Lazy o Normal}: una subexpresión se evalua sólo si es necesario.
  \item Polimorfismo paramétrico.
  \item Alto orden
  \item Currificación
\end{itemize}

\subsubsection{Esquemas de recursión}

\subsubsection{Monadas}

Una mónada es un tipo paramétrico \xtt{M a} con operaciones

\begin{lstlisting}[language=Haskell]
return :: a -> M a
(>>=) :: M a -> (a -> M b) -> M b
\end{lstlisting}

que satisfacen las siguientes leyes

\begin{lstlisting}[language=Haskell]
return x >>= k              = k x
m >>= \x -> return x        = m
m >>= \x -> (n >>= \y -> p) = (m >>= \x -> n) >>= \y -> p
    (siempre que x no aparezca en p)
\end{lstlisting}

El objetivo de la Mónada es incorporar \xit{efectos} a un valor.
\begin{itemize}
  \item El tipo \xtt{M a} incorpora la información necesaria.
  \item \xtt{return x} representa a \xtt{x} con \xit{efecto nulo}.
  \item \xtt{($>>=$)} \xit{secuencia} efectos con \xit{dependencia} de datos.
\end{itemize}

Es una forma de abstraer comportamientos específicos en un cómputo. Cada mónada se diferencia de las demás por sus operaciones adicionales:
\begin{itemize}
  \item \xtt{Maybe} tiene \xtt{fail}
  \item \xtt{State} tiene \xtt{incrementar}
  \item \xtt{Output} tiene \xtt{imprimir}
  \item etc.
\end{itemize}

Haskell define una clase para las mónadas

\begin{lstlisting}[language=Haskell]
class Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b
\end{lstlisting}

Por ejemplo, para definir \xtt{Maybe} como una mónada se escribe

\begin{lstlisting}[language=Haskell]
instance Monad Maybe where
  return x = Just x
  m >>= k = case m of
    Nothing -> Nothing
    Just x -> k x
\end{lstlisting}

\paragraph{Funciones generales}

Pueden definirse muchas funciones de uso general usando sólo la interfase de mónadas
\begin{lstlisting}[language=Haskell]
liftM :: Monad m => (a -> b) -> m a -> m b
liftM f mx = do
  x <- mx
  return (f x)

liftM2 :: Monad m => (a -> b -> c) -> m a -> m b -> m c
liftM2 f mx my = do x <- mx
  y <- my
  return (f x y)
\end{lstlisting}

Estas funciones pueden usarse para definir funciones específicas para la aplicación, por ejemplo:

\begin{lstlisting}[language=Haskell]
(</>) :: Monad m => m Float -> m Float -> m Float
(</>) = liftM2 (/)

eval :: Monad m => E -> m Float
eval (Cte n) = return n
eval (Div e1 e2) = eval e1 </> eval e2
\end{lstlisting}

\subsection{Lambda cálculo}

Fue introducido por \xit{Alonzo Church} en 1934, y presenta un modelo de computación basado en \xbf{funciones}.

La formulación original es sin tipos, pero posteriormente (1941) se introduce el \xbf{Lambda cálculo tipado}, que es el que vamos a estudiar.

Empezamos con el Lambda cálculo tipado con expresiones booleanas y luego lo vamos extendiendo con otras construcciones.

\subsubsection{Expresiones de tipos}

Denotan los diferentes \xbf{tipos}. Por ejemplo, en el Lambda cálculo tipado con expresiones booleanas (de ahora en más $\lambda^b$) tenemos:

\[ \sigma, \tau ::= Bool|\sigma\to\tau \]

dónde,
\begin{itemize}
  \item $Bool$ es el tipo de los booleanos,
  \item $\sigma\to\tau$ es el tipo de las funciones de tipo $\sigma$ en $\tau$,
  \item con $\sigma$ y $\tau$ dos tipos (no necesariamente distintos).
\end{itemize}

\subsubsection{Términos}

Denotan las posibles expresiones que podemos construir. Por ejemplo, en $\lambda^b$ tenemos:

\[ M ::= true \vert false \vert \ifte{M}{P}{Q} \vert \app{M}{N} \vert \abs{x}{\sigma}{M} \vert x \]

dónde,
\begin{itemize}
  \item $true$ y $false$ son las constantes de verdad,
  \item \ifte{M}{P}{Q} es el condicional,
  \item \app{M}{N} es la aplicación de la función denotada por el término $M$ al argumento $N$,
  \item \abs{x}{\sigma}{M} es una función cuyo parámetro formal es $x$ y cuyo cuerpo es $M$.
  \item $x$ es una variable de términos.
\end{itemize}

Ejemplo: $\app{(\abs{f}{Bool \to Bool}{f\ true})}{(\abs{y}{Bool}{y})}$

\subsubsection{Sustitución}

Dentro de un término, una variable puede estar \xbf{libre} o \xbf{ligada}. Decimos que $x$ ocurre libre si no se encuentra bajo el alcance de una ocurrencia de $\lambda x$. En caso contrario, está ligada. Formalmente, tenemos que:

\begin{align*}
FV(x) &\eqdef \{x\} \\
FV(true) = FV (false) &\eqdef \emptyset \\
FV(\ifte{M}{P}{Q}) &\eqdef FV(M) \cup FV(P) \cup FV(Q) \\
FV(\app{M}{N}) &\eqdef FV(M) \cup FV(N) \\
FV(\abs{x}{\sigma}{M}) &\eqdef FV(M)\ \backslash\ \{x\} \\
\end{align*}

Luego, el proceso de sustitución $M\{x \from N\}$ consiste en sustituir todas las ocurrencias \xit{libres} de $x$ en el término $M$ por el término $N$. Esto se utiliza para darle semántica a la aplicación de funciones.

Cuando realizamos este proceso, asumimos que la variable ligada se renombró de tal manera que no ocurre libre en $N$. Por ejemplo,

\[ \sust{\abs{z}{\sigma}{x}}{x\from z} = \abs{z}{\sigma}{z}\]

está mal, ya que convertimos la función constante \abs{z}{\sigma}{x} en la función identidad. Entonces, deberíamos haber utilizado:

\[ \sust{\abs{w}{\sigma}{x}}{x\from z} = \abs{w}{\sigma}{z}\]

Una vez que entendemos esto, podemos definir el concepto de $\alpha-equivalencia$. Decimos que dos términos $M$ y $N$ son $\alpha-equivalentes$ si difieren solamente en el nombre de sus variables ligadas. Ejemplo: $\abs{z}{Bool}{z} =_{\alpha} \abs{y}{Bool}{y}$, pero $\abs{x}{Bool}{y} \neq_{\alpha} \abs{x}{Bool}{z}$.

En los casos de sustitución que haya conflictos, podemos renombrar apropiadamente para que ande todo.

\subsubsection{Sistema de tipado}

Es un sistema formal de deducción (o derivación) que utiliza axiomas y reglas de tipado para caracterizar un subconjunto de los términos llamados \xit{tipados}. Es decir, es un sistema mediante el cual podemos deducir el tipo de un término.

Sin embargo, el objetivo del sistema de tipos de lambda cálculo es asegurar que si un término es cerrado, está bien tipado y termina, entonces evalúa a un valor (a menos que se mantengan formas normales que no sean valores para representar errores).

La correctitud del sistema de tipos se basa en el progreso y la preservación. El progreso indica que si se tiene un término $M$ cerrado y bien tipado, entonces es un valor, o existe un $M'$ tal que el primero evalúa en el segundo. La preservación se refiere a que el progreso preserva tipos.

En resumen:

\begin{itemize}
  \item Corrección = Progreso + Preservación.
  \item \xbf{Progreso}: si $M$ es cerrado y bien tipado entonces
    \begin{itemize}
      \item $M$ es un valor
      \item o bien existe $M'$ tal que $M \to M'$.
    \end{itemize}
    Esto quiere decir que la evaluación no puede trabarse para términos cerrados y bien tipados que no son valores.
  \item \xbf{Preservación}: si $\Gamma \rhd M : \sigma$ y $M \to N$, entonces $\Gamma \rhd N : \sigma$. Es decir que la evaluación preserva tipos.
\end{itemize}

Ahora presentamos algunas nociones.

Un \xit{contexto de tipado} $\Gamma$ es un conjunto de pares $\{x_1:\sigma_1,\dots,x_n:\sigma_n\}$ donde cada $x_i$ es distinto. Los $x_i$ representan las variables y los $\sigma_i$ sus tipo asignados.

Un \xit{juicio de tipado} es una expresión de la forma $\Gamma \rhd M : \sigma$ que significa que el término $M$ tiene tipo $\sigma$ asumiendo el contexto de tipado $\Gamma$. Estos juicios se generan utilizando \xit{axiomas y reglas de tipado}. Ejemplo de axioma:

\[\deriv{}{\Gamma \rhd true : Bool}{T-True}\]

Ejemplo de regla:

\[\deriv{\Gamma, x : \sigma \rhd M : \tau}{\Gamma \rhd \abs{x}{\sigma}{M}:\sigma\to\tau}{T-Abs}\]

\vspace{0.5em}
Entonces, $M$ es \xit{tipable}  si $\Gamma \rhd M : \sigma$ puede derivarse usando los axiomas y reglas de tipados, para algún $\Gamma$ y $\sigma$.

\paragraph{Propiedades básicas:}

\begin{itemize}
  \item \xbf{Unicidad de tipos}: si $\Gamma \rhd M : \sigma$ y $\Gamma \rhd M : \tau$ son derivables, entonces $\sigma = \tau$.
  \item \xbf{Weakening+Strenghening}: si $\Gamma \rhd M : \sigma$ es derivable y $\Gamma \cap \Gamma'$ contiene a todas las variables libres de $M$, entonces $\Gamma' \rhd M : \sigma$.
  \item \xbf{Sustitución}: si $\Gamma,x:\sigma \rhd M : \tau$ y $\Gamma \rhd N : \sigma$ son derivables, entonces $\Gamma \rhd \sust{M}{x\from N} : \tau$ es derivable.
\end{itemize}

\subsubsection{Semántica operacional}

Habiendo definido la sintaxis de $\lambda^b$, nos interesa formular cómo se evalúan o ejecutan los términos. Esto se puede hacer de varias formas: operacional, denotacional y axiomática. Nosotros vamos a usar \xit{operacional}.

La semántica operacional consiste en interpretar a los \xit{términos como estados} de una máquina abstracta y definir una \xit{función de transición} que indica, dado un estado, cuál es el estado siguiente. De esta forma, el \xit{significado} de un término $M$ es el estado final que alcanza la máquina empezando desde $M$. Hay principalmente dos formas de definir la función de transición:

\begin{itemize}
  \item \xbf{Small-step}: la función de transición describe un paso de computación.
  \item \xbf{Big-step}: la función de transición, en un paso, evalúa el término a su resultado.
\end{itemize}

Al igual que con el Sistema de tipado, vamos a usar axiomas y reglas para formular \xbf{juicios de evaluación} $M\to N$ que indican que el término $M$ reduce, en un paso, al término $N$. Ejemplo de axioma:

\[\deriv{}{\ifte{true}{M_2}{M_3} \to M_2}{E-IfTrue}\]

Ejemplo de regla:

\[\deriv{M_1 \to M_1'}{\ifte{M_1}{M_2}{M_3} \to \ifte{M_1'}{M_2}{M_3}}{E-If}\]

Cuando dado un término $M$, no existe $N$ tal que $M\to N$, decimos que $M$ no puede reducirse más y está en \xbf{forma normal}.

Lo último que nos falta agregar es un conjunto de \xbf{Valores} que denota las expresiones que pueden ser un resultado válido de un cómputo. Para $\lambda^b$, tenemos que $V ::= true \vert false$.

\paragraph{Propiedades básicas:}

\begin{itemize}
  \item \xbf{Determinismo del juicio de evaluación en un paso}: si $M \to M'$ y $M \to M''$, entonces $M'= M''$.
  \item Todo valor está en forma normal, pero no vale el recíproco.
  \item Si un termino está en forma normal pero no es un valor, entonces decimos que es un \xbf{estado de error}.
\end{itemize}

\noindent
El \xbf{Juicio de evaluación en muchos pasos} $\toto$ es la clausura reflexiva, transitiva de $\to$. Es decir, la menor relación tal que:

\begin{itemize}
  \item Si $M\to M'$, entonces $M\toto M'$.
  \item $M\toto M$, para todo $M$.
  \item Si $M \toto M'$ y $M' \toto M''$, entonces $M \toto M''$.
\end{itemize}

\paragraph{Propiedades de evaluación en muchos pasos:}

\begin{itemize}
  \item \xbf{Unicidad de formas normales}: si $M \toto U$ y $M \toto V$, entonces $U=V$.
  \item \xbf{Terminación}: para todo $M$ existe una forma normal $N$ tal que $M \toto N$.
  \item Si un término está bien tipado, y termina, entonces evalúa a un valor.
\end{itemize}

\subsubsection{Extensiones}

La versión más usada en la materia del Lambda Cálculo es $\lambda^{bn}$: que tiene $Bool$, $Nat$ y funciones, pero existen varias extensiones que aportan nuevas herramientas.

Cuando definimos una extensión del Cálculo $\lambda$ tenemos que re-definir (o indicar qué es lo que se agrega):
\begin{itemize}
  \item Expresiones válidas
  \item Tipos
  \item Reglas de tipado
  \item Valores
  \item Reglas de semántica
\end{itemize}

\paragraph{Lambda Cálculo $\lambda^{bn}$}

Este es el más común de todos. Las expresiones válidas son:

\[ M ::= x \vert true \vert false \vert \ifte{M}{M}{M} \vert \abs{x}{\sigma}{M} \vert \app{M}{M} \vert 0 \vert succ(M) \vert pred(M) \vert iszero(M) \]

Los tipos:

\[ \sigma ::= Bool \vert Nat \vert \sigma\to\rho \]

Las reglas de tipado:

\[\deriv{}{\Gtipa{true}{Bool}}{T-True}\quad\quad \deriv{}{\Gtipa{false}{Bool}}{T-False}\quad\quad \deriv{x:\sigma\in\Gamma}{\Gtipa{x}{\sigma}}{T-Var}\]

\[\deriv{}{\Gtipa{0}{Nat}}{T-Zero}\quad\quad \deriv{\Gtipa{M}{Nat}}{\Gtipa{iszero(M)}{Bool}}{T-IsZero}\]

\[\deriv{\Gtipa{M}{Nat}}{\Gtipa{succ(M)}{Nat}}{T-Succ}\quad\quad \deriv{\Gtipa{M}{Nat}}{\Gtipa{pred(M)}{Nat}}{T-Pred}\]

\[\deriv{\Gtipa{M}{Bool}\quad \Gtipa{P}{\sigma}\quad \Gtipa{Q}{\sigma}}{\Gtipa{\ifte{M}{P}{Q}}{\sigma}}{T-If}\]

\[\deriv{\Gamma,x :\sigma \rhd M : \tau}{\Gtipa{\abs{x}{\sigma}{M}}{\sigma\to\tau}}{T-Abs}\quad\quad \deriv{\Gtipa{M}{\sigma\to\tau}\quad \Gtipa{N}{\sigma}}{\Gtipa{\app{M}{N}}{\tau}}{T-App}\]

Los valores:

\[ V ::= true \vert false \vert \abs{x}{\sigma}{M} \vert \underline{n} \]

donde \underline{n} abrevia $succ^n(0)$.\\

Las reglas de semántica:

\[\deriv{M_1 \to M_1'}{\ifte{M_1}{M_2}{M_3}\to\ifte{M_1'}{M_2}{M_3}}{E-If}\]

\[\deriv{}{\ifte{true}{M_2}{M_3} \to M_2}{E-IfTrue}\quad\quad \deriv{}{\ifte{false}{M_2}{M_3} \to M_3}{E-IfFalse}\]

\[\deriv{M_1 \to M_1'}{succ(M_1) \to succ(M_1')}{E-Succ}\quad\quad \deriv{M_1 \to M_1'}{pred(M_1) \to pred(M_1')}{E-Pred}\]

\[\deriv{}{pred(0) \to 0}{E-PredZero}\quad\quad \deriv{}{pred(succ(\underline{n}))\to \underline{n}}{E-PredSucc}\]

\[\deriv{}{iszero(0) \to true}{E-IsZeroZero}\quad\quad \deriv{}{iszero(succ(\underline{n}))\to false}{E-IsZeroSucc}\]

\[\deriv{M_1 \to M_1'}{iszero(M_1) \to iszero(M_1')}{E-IsZero}\]

\[\deriv{M_1 \to M_1'}{\app{M_1}{M_2} \to \app{M_1'}{M_2}}{E-App1 o $\mu$}\quad\quad \deriv{M_2 \to M_2'}{\app{V_1}{M_2} \to \app{V_1}{M_2'}}{E-App2 o $\nu$}\]

\[\deriv{}{\app{\abs{x}{\sigma}{M}}{V} \to \sust{M}{x\from V}}{E-AppAbs o $\beta$}\]

\paragraph{Registros}

Llamada $\lambda^{\dots r}$. Permite utilizar descriptores de campos de la pinta: $\{nombre: String, edad: Nat\}$.

Agregamos al conjunto de tipos:

\[\sigma ::= \dots \vert \{I_i : \sigma_i^{\ i \in 1..n}\}\]

Y al conjunto de expresiones:

\[M ::= \dots \vert \{I_i = M_i^{\ i \in 1..n}\} \vert M.I\]

Informalmente:
\begin{itemize}
  \item El registro $\{I_i = M_i^{\ i \in 1..n}\}$ evalúa a $\{I_i = V_i^{\ i \in 1..n}\}$ donde $V_i$ es el valor al que evalúa $M_i$, $i \in 1..n$.
  \item $M.I$: evaluar $M$ hasta que arroje $\{I_i = V_i^{\ i \in 1..n}\}$, luego proyectar el campo correspondiente.
\end{itemize}

Entonces, las reglas de tipado son:

\[\deriv{\Gamma \rhd M_i : \sigma_i\quad \forall i \in I = \{1..n\}}{\Gamma \rhd \{I_i = M_i^{\ i \in 1..n}\}:\{I_i : \sigma_i^{\ i \in 1..n}\}}{T-Rcd}\]

\[\deriv{\Gamma \rhd M : \{I_i : \sigma_{i}^{\ i \in 1..n}\}\quad j\in 1..n}{\Gamma \rhd M.I_j : \sigma_j}{T-Proj}\]

Los valores se expanden a:

\[V :: \dots \vert \{I_i = V_i^{\ i \in 1..n}\}\]

Y las reglas de semántica operacional son:

\[\deriv{j \in 1..n}{\{I_i = V_i^{\ i \in 1..n}\}.I_j \to V_j}{E-ProjRcd}\]

\[\deriv{M \to M'}{M.I \to M'.I}{E-Proj}\]

\[\deriv{M_j \to M_j'}{\{I_i = V_i^{\ i \in 1..j-1}, I_j = M_j, I_i = M_i^{\ i \in j+1..n}\} \to \{I_i = V_i^{\ i \in 1..j-1}, I_j = M_j', I_i = M_i^{\ i \in j+1..n}\}}{E-Rcd}\]

\paragraph{Declaraciones locales}

Esta extensión nos ayuda a mejorar la legibilidad. Agregamos a las expresiones:

\[M ::= \dots \vert let\ x : \sigma = M\ in\ N\]

Informalmente, $let\ x : \sigma = M\ in\ N$ evalúa $M$ a un valor $V$, liga la variable $x$ a $V$ y evalúa $N$.
Esta extensión no agrega tipos nuevos.

Las reglas de tipado son:

\[\deriv{\Gamma \rhd M : \sigma_1\quad \Gamma, x: \sigma_1 \rhd N : \sigma_2}{\Gamma \rhd let\ x : \sigma_1 = M\ in\ N : \sigma_2}{T-Let}\]

Y la semántica operacional:

\[\deriv{M_1 \to M_1'}{let\ x : \sigma = M_1\ in\ M_2 \to let\ x : \sigma = M_1'\ in\ M_2}{E-Let}\]

\[\deriv{}{let\ x : \sigma = V_1\ in\ M_2 \to \sust{M_2}{x \from V_1}}{E-LetV}\]

\paragraph{Referencias}

En la extensión anterior $let\ x : Nat = \underline{2}\ in\ M$
\begin{itemize}
  \item $x$ es una variable declarada con valor 2.
  \item El valor de $x$ permanece \xit{inalterado} a lo largo de la evaluación de $M$.
  \item En este sentido, $x$ es \xit{inmutable}: no existe una operación de asignación.
\end{itemize}

En programación imperativa pasa todo lo contrario: todas las variables son mutables.
Entonces, vamos a extender Cálculo Lambda Tipado con variables mutables (y lo llamamos $\lambda^{bnru}$, pero la $r$ es de referencias).

Las operaciones básicas que vamos a manejar son:
\begin{itemize}
  \item Alocación (reserva de memoria): $ref\ M$ genera una referencia fresca cuyo contenido es el valor de $M$.
  \item Derreferenciación (lectura): $!x$ sigue la referencia $x$ y retorna su contenido.
  \item Asignación: $x := M$ almacena en la referencia $x$ el valor de $M$.
\end{itemize}

Estas 3 operaciones son \xbf{comandos}: expresiones que no interesan por su valor, sino por su \xbf{efecto}. Entonces, decimos que se evalúan para causar un efecto, y lo expresamos con un nuevo valor $unit$.

En este momento nos estamos alejando de lo que sería un lenguaje funcional puro, en el que las expresiones son puras en el sentido de carecer de efectos.

Los tipos de $\lambda^{bnru}$ son:

\[\sigma ::= Bool \vert Nat \vert \sigma\to\rho \vert Unit \vert Ref\ \sigma \]

Las expresiones nos quedan:

\[M ::= x \vert \abs{x}{\sigma}{M} \vert \app{M}{N} \vert unit \vert ref\ M \vert !M \vert M := N \vert l \]

Notar que $Unit$ es un tipo unitario: el único valor posible de una expresión de ese tipo es $unit$. Cumple un rol similar a $void$ en C o Java. Por otro lado, $Ref \sigma$ es el tipo de las referencias a valores de tipo $\sigma$, y l son las direcciones, que representan a las referencias.

En primer lugar, podemos introducir una forma de evaluar varias expresiones en \xbf{secuencia}:

\[M_1; M_2 \eqdef \app{(\abs{x}{Unit}{M_2})}{M_1}\quad x\notin FV(M_2)\]

Entonces, la evaluación de $M_1; M_2$ consiste en primero evaluar $M_1$  y luego $M_2$. Este comportamiento funciona debido a las reglas de evaluación definidas previamente para $\lambda^{bn}$.

El conjunto de valores ahora incluye también a las direcciones:

\[V ::= true \vert false \vert 0 \vert \underline{n} \vert unit \vert \abs{x}{\sigma}{M} \vert l \]

Y las reglas de tipado:

\[\deriv{}{\Gamma \rhd unit : Unit}{T-Unit}\quad\quad \deriv{\Gtipa{M_1}{\sigma}}{\Gtipa{ref\ M_1}{Ref\ \sigma}}{T-Ref}\]

\[\deriv{\Gtipa{M_1}{Ref\ \sigma}}{\Gtipa{!M_1}{\sigma}}{T-DeRef}\quad\quad \deriv{\Gtipa{M_1}{Ref\ \sigma}\quad \Gtipa{M_2}{\sigma}}{\Gtipa{M_1 := M_2}{Unit}}{T-Assign}\]

Para formalizar la semántica operacional, primero debemos preguntarnos: ¿Qué es una referencia? Rta: Es una abstracción de una porción de memoria que se encuentra en uso. Entonces debemos formalizar el concepto de memoria o \xit{store}:

\begin{itemize}
  \item Usaremos direcciones (simbólicas) o ``locations'' $l, l_i \in \mathcal{L}$ para representar referencias, con lo que el \xit{store} no es más que una función parcial de direcciones a valores.
  \item Usamos las letras $\mu, \mu'$ para referirnos a stores.
  \item Notación:
    \begin{itemize}
      \item $\mu[l \mapsto V]$ es el store resultante de pisar $\mu(l)$ con $V$.
      \item $\mu\ {\scriptstyle \medoplus}\ (l \mapsto V)$ es el store extendido resultante de ampliar $\mu$ con una nueva asociación $l \mapsto V$ (asumimos $l \notin Dom(\mu)$).
    \end{itemize}
  \item Además, $\Gtipa{l}{?}$ depende de los valores que se almacenen en la dirección $l$. Esta situación es parecida a las variables libres, con lo que precisamos un ``contexto de tipado'' para direcciones: $\Sigma$ función parcial de direcciones a tipos. Con esto, armamos un nuevo juicio de tipado: $\GStipa{M}{\sigma}$.
  \item Y los juicios de evaluación, en vez de ser de la forma $M \to M'$, ahora son  $M \vert \mu \to M' \vert \mu'$. Que se lee como: ``Teniendo la expresión $M$, el store $\mu$ reduce la expresión a $M'$, y nos queda el store $\mu'$''.
\end{itemize}

Entonces, las reglas de tipado nos terminan quedando:

\[\deriv{}{\GStipa{unit}{Unit}}{T-Unit}\quad\quad \deriv{\GStipa{M_1}{\sigma}}{\GStipa{ref\ M_1}{Ref\ \sigma}}{T-Ref}\]

\[\deriv{\GStipa{M_1}{Ref\ \sigma}}{\GStipa{!M_1}{\sigma}}{T-DeRef}\quad\quad \deriv{\GStipa{M_1}{Ref\ \sigma}\quad \GStipa{M_2}{\sigma}}{\GStipa{M_1 := M_2}{Unit}}{T-Assign}\]

\[\deriv{\Sigma(l) = \sigma}{\GStipa{l}{Ref\ \sigma}}{T-Loc}\]

Y la semántica operacional:

\[\deriv{M_1 \vert \mu \to M_1' \vert \mu'}{\app{M_1}{M_2} \vert \mu \to \app{M_1'}{M_2} \vert \mu'}{E-App1}\quad\quad \deriv{M_2 \vert \mu \to M_2' \vert \mu'}{\app{V_1}{M_2} \vert \mu \to \app{V_1}{M_2'} \vert \mu'}{E-App2}\]

\[\deriv{}{\abs{x}{\sigma}{V} \vert \mu \to \sust{M}{x \from V} \vert \mu}{E-AppAbs}\]

Notar que hasta ahora las reglas no modifican el store.

\[\deriv{M_1 \vert \mu \to M_1' \vert \mu'}{!M_1 \vert \mu \to !M_1' \vert \mu'}{E-Deref}\quad\quad \deriv{\mu(l) = V}{!l \vert \mu \to V \vert \mu}{E-DerefLoc}\]

\[\deriv{M_1 \vert \mu \to M_1' \vert \mu'}{M_1 := M_2 \vert \mu \to M_1' := M_2 \vert \mu'}{E-Assign1}\quad\quad \deriv{M_2 \vert \mu \to M_2' \vert \mu'}{V := M_2 \vert \mu \to V := M_2' \vert \mu'}{E-Assign2}\]

\[\deriv{}{l := V \vert \mu \to unit \vert \mu[l \mapsto V]}{E-Assign}\]

\[\deriv{M_1 \vert \mu \to M_1' \vert \mu'}{ref\ M_1 \vert \mu \to ref\ M_1' \vert \mu'}{E-Ref}\quad\quad \deriv{l \notin Dom(\mu)}{ref\ V \vert \mu \to l \vert \mu\ {\scriptstyle \medoplus}\ (l \mapsto V)}{E-RefV}\]

\paragraph{Preservación y progreso}

Habíamos visto antes que \xit{Corrección = Preservación + Progreso}. Sin embargo, al introducir el sistema de tipos para las direcciones ($\Sigma$) rompimos ambos conceptos.

Esto se puede ver teniendo en cuenta que $\GStipa{M}{\sigma}$ y $M \vert \mu \to M' \vert \mu'$ implican $\GStipa{M'}{\sigma}$. Pero si suponemos, por ejemplo, que: $M = !l, \Gamma = \emptyset, \Sigma(l) = Nat, \mu(l) = true$, entonces $\GStipa{M}{Nat}$ y $M \vert \mu \to true \vert \mu$, pero $\GStipa{true}{Nat}$ no vale.

Para la \xit{preservación}, precisamos una noción de compatibilidad entre el store y el contexto de tipado para store. Entonces, debemos tipar los stores. Con este objetivo introducimos un nuevo juicio de tipado: $\Gamma|\Sigma \rhd \mu$, y se define del siguiente modo: $\Gamma|\Sigma \rhd \mu$ sii
\begin{enumerate}
  \item $Dom(\Sigma) = Dom(\mu)$ y
  \item $\GStipa{\mu(l)}{\Sigma(l)}$ para todo $l \in Dom(\mu)$.
\end{enumerate}

Y tenemos una nueva formulación de \xit{preservación}. Si pasa:
\begin{itemize}
  \item $\GStipa{M}{\sigma}$
  \item $M \vert \mu \to N \vert \mu'$
  \item $\Gamma|\Sigma \rhd \mu$
\end{itemize}
implica que existe $\Sigma' \supseteq \Sigma$ tal que $\Gamma|\Sigma' \rhd N : \sigma$ y $\Gamma|\Sigma' \rhd \mu'$. Donde el $\Sigma'$ se utiliza ya que $\Sigma$ puede haber crecido en dominio por posibles reservas de memoria.

Para el \xit{progreso}. Si $M$ es cerrado y bien tipado (i.e. $\emptyset|\Sigma \rhd M : \sigma$, para algún $\Sigma, \sigma$) entonces:
\begin{itemize}
  \item $M$ es un valor,
  \item  o bien para cualquier store $\mu$ tal que $\emptyset|\Sigma \rhd \mu$, existe $M'$ y $\mu'$ tal que $M \vert \mu \to M' \vert \mu'$
\end{itemize}

\paragraph{Recursión}

Una ecuación recursiva es aquella que tiene la pinta $f = \dots f \dots f \dots$ (se usa a sí misma en la definición). Esta extensión permite construir funciones recursivas.

Agregamos a las expresiones:

\[M ::= \dots \vert fix\ M\]

No se precisan nuevos tipos, pero sí una regla de tipado:

\[\deriv{\Gtipa{M}{\sigma_1 \to \sigma_1}}{\Gtipa{fix\ M}{\sigma_1}}{T-Fix}\]

No hay valores nuevos. La semántica operacional es:

\[\deriv{M_1 \to M_1'}{fix\ M_1 \to fix\ M_1'}{E-Fix}\quad\quad \deriv{}{fix\ (\abs{x}{\sigma}{M}) \to \sust{M}{x\from fix\  (\abs{x}{\sigma}{M})}}{E-FixBeta}\]

\subsubsection{Inferencia de tipos}

Es un procedimiento que consiste en transformar términos \xit{sin} información de tipos en términos \xbf{tipables}. Para ello, debemos inferir la información de tipos faltante. Esto trae como beneficios:

\begin{itemize}
  \item El programador puede obviar algunas declaraciones de tipos.
  \item En general, evita la sobrecarga de tener que declarar y manipular \xit{todos} los tipos.
  \item Todo ello sin impactar la perfomance del programa: la inferencia de tipos se realiza en tiempo de compilación.
\end{itemize}

\paragraph{Función de borrado}

Llamamos \erase{\cdot} a la función que dado un término \xit{elimina} las anotaciones de tipos de las abstracciones. Ejemplo: $\erase{\abs{x}{Nat}{\abs{f}{Nat\to Nat}{f\ x}}} = \stabs{x}{\stabs{f}{f\ x}}$

Entonces queremos, dado un término $U$ \xit{sin} anotaciones de tipos, hallar un término estándar $M$ tal que:
\begin{itemize}
  \item $\Gamma \rhd M : \sigma$, para algún $\Gamma$ y $\sigma$, y
  \item $\erase{M} = U$
\end{itemize}

Notar que este problema es más difícil que el chequeo de tipos para un término estándar $M$ que hacíamos utilizando los axiomas y reglas del sistema de tipado.

\paragraph{Variables de tipos}

Para poder escribir una \xit{única} expresión que englobe muchas soluciones de inferencia vamos a usar variables de tipo.

Dichas variables las vamos a representar con la letra ``\xit{s}''. Si tenemos una expresión que utiliza \xit{s}, basta con sustituir \xit{s} por cualquier expresión de tipos para arrojar una solución válida.

\paragraph{Sustitución de tipos}

Es una función $S$ o $T$ que mapea variables de tipo en expresiones de tipo. Entonces, nuestra función de sustitución $S$ puede aplicarse a:
\begin{itemize}
  \item Una expresión de tipos $\sigma$ (escribimos $S\sigma$)
  \item Una término $M$ $\sigma$ (escribimos $SM$)
  \item Un contexto de tipado  $\Gamma = \{x_1:\sigma_1,\dots,x_n:\sigma_n\}$ (escribimos $S\Gamma$) y se define como $S\Gamma \eqdef \{x_1:S\sigma_1,\dots,x_n:S\sigma_n\}$
\end{itemize}

Notas sobre la sustitución:

\begin{itemize}
  \item El conjunto $\{t\ |\ St \neq t\}$ se llama \xbf{soporte} de $S$. Este conjunto representa las variables que $S$ ``afecta''.
  \item Usamos la notación $\{\sigma_1/t_1,\dots,\sigma_n/t_n\}$ para la sustitución con soporte $\{t_1,\dots,t_n\}$.
  \item La sustitución cuyo soporte es $\emptyset$ es la sustitución identidad (\xit{Id}).
\end{itemize}

\paragraph{Instancia de un juicio de tipado}

Un juicio de tipado $\Gamma' \rhd M' : \sigma'$ es una instancia de $\Gamma \rhd M : \sigma$ si existe una substitución de tipos $S$ tal que $S\Gamma \subset \Gamma'$, $M' = SM$ y $\sigma' = S\sigma$. Como propiedad: si $\Gamma \rhd M : \sigma$ es derivable, entonces cualquier instancia del mismo también lo es.

\paragraph{Función de inferencia \w{\cdot}}

Entonces, queremos definir una función \w{\cdot} que dado un término $U$ sin anotaciones verifica:
\begin{itemize}
  \item \xbf{Corrección:} $\w{U} = \Gamma \rhd M : \sigma$ implica
    \begin{itemize}
      \item $\erase{M} = U$
      \item $\Gamma \rhd M : \sigma$ es derivable
    \end{itemize}
  \item \xbf{Completitud:} si $\Gamma \rhd M : \sigma$ es derivable y $\erase{M} = U$, entonces
    \begin{itemize}
      \item \w{U} tiene éxito y,
      \item produce un juicio $\Gamma' \rhd M' : \sigma'$ tal que $\Gamma \rhd M : \sigma$ es instancia del mismo. Se dice que \w{\cdot} computa un \xbf{tipo principal}.
    \end{itemize}
\end{itemize}

\subsubsection{Unificación}

La idea de nuestro algoritmo de inferencia va a ser analizar un término (sin anotaciones de tipo) a partir de sus subtérminos. El problema es que, una vez obtenida la información inferida de los subtérminos, debemos:
\begin{itemize}
  \item \xbf{Consistencia:} determinar si la información de cada subtérmino es consistente.
  \item \xbf{Síntesis:} sintetizar la información del término original a partir de la información de los subtérminos. Esto involucra \xit{compatibilizar} o \xit{unificar} la información de tipos cuando dos subtérminos tienen una misma variable.
\end{itemize}

El proceso de determinar si existe una sustitución $S$ tal que dos expresiones de tipos $\sigma$, $\tau$ son unificables (i.e. $S\sigma = S\tau$) se llama \xbf{unificación}.

\paragraph{Algunas propiedades de sustituciones}

\begin{itemize}
  \item \xbf{Composición:} $(S \circ T)(\sigma) = S(T(\sigma))$
  \item \xbf{Igualdad:} $S = T$ si tienen el mismo soporte y $St = Tt$ para todo $t$ en el soporte de $S$
  \item $S \circ Id = Id \circ S = S$
  \item $S \circ (T \circ U) = (S \circ T) \circ U$
  \item Una sustitución $S$ es \xbf{más general} que $T$ si existe $U$ tal que $T = U \circ S$.
\end{itemize}

\paragraph{Unificador más general (MGU)}

Una ecuación de unificación es una expresión de la forma $\sigma_1 \uni \sigma_2$. Una sustitución $S$ es una solución de un conjunto de ecuaciones de unificación $\{\sigma_1 \uni \sigma_1', \dots, \sigma_n \uni \sigma_n'\}$ si $S\sigma_i = S\sigma_i'$.

Una sustitución $S$ es un \xbf{MGU} de $\{\sigma_1 \uni \sigma_1', \dots, \sigma_n \uni \sigma_n'\}$ si
\begin{itemize}
  \item Es solución de $\{\sigma_1 \uni \sigma_1', \dots, \sigma_n \uni \sigma_n'\}$
  \item Es más general que cualquier otra solución de $\{\sigma_1 \uni \sigma_1', \dots, \sigma_n \uni \sigma_n'\}$
\end{itemize}

\paragraph{Algoritmo de unificación de Martelli-Montanari}

\begin{teo}
  Si $\{\sigma_1 \uni \sigma_1', \dots, \sigma_n \uni \sigma_n'\}$ tiene solución, existe un MGU y además es único salvo renombre de variables.
\end{teo}

El algoritmo de Martelli-Montanari es un algoritmo de unificación no-determinístico. Consiste en reglas de simplificación que reescriben conjuntos de pares de tipos a unificar (\xit{goals}).

\[G_0 \unito G_1 \unito_{S_1} \unito G_2 \unito \dots \unito_{S_k} G_n\]

Las secuencias que terminan en el goal vacío son exitosas. Si la secuencia es exitosa el MGU es $S_k \circ \dots \circ S_1$.

Las reglas de este algoritmo son:

\begin{enumerate}
  \item \xbf{Descomposición:} $\{\sigma_1\to\sigma_2 \uni \tau_1\to\tau_2\} \cup G \unito \{\sigma_1 \uni \tau_1, \sigma_2 \uni \tau_2\} \cup G$
  \item \xbf{Eliminación de par trivial:} $\{s \uni s\} \cup G \unito G$
  \item \xbf{Swap:} si $\sigma$ no es una variable, $\{\sigma \uni s\} \cup G \unito \{s \uni \sigma\} \cup G$
  \item \xbf{Eliminación de variable:} $\{s \uni \sigma\} \cup G \unito_{\sigma/s} G[\sigma/s]$
  \item \xbf{Falla:} $\{\sigma \uni \tau\} \cup G \unito \text{falla}$, con $(\sigma, \tau) \in T \cup T^{-1}$ y $T = \{(Bool, Nat),$ ${(Nat, \sigma_1 \to \sigma_2)}$, ${(Bool, \sigma_1 \to \sigma_2)}$$\}$,
  \item \xbf{Occur check:} si $s \neq \sigma$ y $s \in FV(\sigma)$, entonces $\{s \uni \sigma\} \cup G \unito \text{falla}$
\end{enumerate}

\begin{teo}
  Propiedades del algoritmo
  \begin{itemize}
    \item El algoritmo de Martelli-Montanari siempre termina
    \item Sea $G$ un conjunto de pares
      \begin{itemize}
        \item Si $G$ tiene un unificador, el algoritmo termina exitosamente y retorna un MGU.
        \item Si $G$ no tiene unificador, el algoritmo termina con \xtt{falla}.
      \end{itemize}
    \item Tanto la unificación como la inferencia se pueden hacer en tiempo lineal. Pero el tipo asociado a un término sin anotaciones puede ser exponencial en el tamaño del término.
  \end{itemize}
\end{teo}

\subsubsection{Algoritmo de inferencia}

El algoritmo que vamos a presentar se basa en definir \w{U} por recursión sobre la estructura de $U$, y utiliza el algoritmo de unificación para ir sintetizando la información de las subexpresiones de $U$.

Presentamos las reglas para los casos comunes:

\paragraph{Caso constantes y variables}

\begin{align*}
  \w{0} &\eqdef \emptyset \rhd 0 : Nat \\
  \w{true} &\eqdef \emptyset \rhd true : Bool \\
  \w{false} &\eqdef \emptyset \rhd false : Bool \\
  \w{x} &\eqdef \{x:s\} \rhd x : s \text{, con $s$ variable fresca} \\
\end{align*}

\paragraph{Caso succ}

\[\w{succ(U)} \eqdef S\Gamma \rhd S\ succ(M) : Nat\]

donde
\begin{itemize}
  \item $\w{U} = \Gamma \rhd M : \tau$
  \item $S = MGU\{\tau \uni Nat\}$
\end{itemize}

El caso de $pred$ es similar.

\paragraph{Caso iszero}

\[\w{iszero(U)} \eqdef S\Gamma \rhd S\ iszero(M) : Bool\]

donde
\begin{itemize}
  \item $\w{U} = \Gamma \rhd M : \tau$
  \item $S = MGU\{\tau \uni Nat\}$
\end{itemize}

\paragraph{Caso ifThenElse}

\[\w{\ifte{U}{V}{W}} \eqdef S\Gamma_1 \cup S\Gamma_2 \cup S\Gamma_3 \rhd S(\ifte{M}{P}{Q}) : S\sigma\]

donde
\begin{itemize}
  \item $\w{U} = \Gamma_1 \rhd M : \rho$
  \item $\w{V} = \Gamma_2 \rhd P : \sigma$
  \item $\w{W} = \Gamma_3 \rhd Q : \tau$
  \item $S = MGU\{\sigma \uni \tau, \rho \uni Bool\} \cup \{\sigma_1 \uni \sigma_2 \vert x:\sigma_1 \in \Gamma_i, x:\sigma_2 \in \Gamma_j, i\neq j\}$
\end{itemize}

\paragraph{Caso abs}

\[\w{\lambda x.U} \eqdef \Gamma' \rhd \abs{x}{\tau'}{M} : \tau'\to\rho\]

donde
\begin{itemize}
  \item $\w{U} = \Gtipa{M}{\rho}$
  \item $\tau' = \begin{cases}
          \alpha & \text{ si } x:\alpha \in \Gamma \\
          s \text{ variable fresca} &  \text{ en otro caso}
       \end{cases}$
  \item $\Gamma' = \Gamma \ominus \{x\}$
\end{itemize}

\paragraph{Caso app}

\[\w{\app{U}{V}} \eqdef S\Gamma_1 \cup S\Gamma_2 \rhd S(\app{M}{N}) : St \]

donde
\begin{itemize}
  \item $\w{U} = \Gamma_1 \rhd M : \tau$
  \item $\w{V} = \Gamma_2 \rhd N : \rho$
  \item $t$ variable fresca
  \item $S = MGU\{\tau \uni \rho\to t\} \cup \{\sigma_1 \uni \sigma_2 \vert x:\sigma_1 \in \Gamma_1, x:\sigma_2 \in \Gamma_2\}$
\end{itemize}

\paragraph{Conclusiones de las reglas de inferencia}

\begin{itemize}
  \item Los llamados recursivos devuelven un contexto, un término anotado y un tipo. No podemos asumir nada sobre ellos.
  \item Cuando la regla tiene tipos iguales, unificar.
  \item Si hay contextos repetidos en las premisas, unificarlos.
  \item Cuando la regla liga variables:
  \begin{itemize}
    \item Obtener su tipo del $\Gamma$ obtenido recursivamente.
    \item Si no figuran: variable fresca.
    \item Sacarlas del $\Gamma$ del resultado (y del que se vaya a unificar), ya que ya no son variables libres.
  \end{itemize}
  \item Decorar los términos según corresponda.
  \item Si la regla tiene restricciones adicionales, se incorporan como posibles casos de falla.
\end{itemize}