5_application_languages.tex

\section{Lenguajes Aplicativos}
  \subsection{Gramáticas}
    \[\begin{array}{rcl@{\hspace{1cm}}l}
      \expr &::= && \text{término lambda, o expresión} \\
          &|& \var & \text{variable} \\
          &|& \expr \expr & \text{aplicación, el primero es el operador y el segundo el operando} \\
          &|& \lambda \var.\expr & \text{abstracción o expresión lambda} \\
          &|& \natconst | \boolconst \\
          &|& -\expr \ |\ \expr + \expr  \ |\ \expr * \expr \ |... & \text{operadores aritméticos}\\
          &|& \expr\geq \expr  \ |\ \expr\leq \expr \ |\ \expr< \expr \ | ... & \text{operadores relacionales}\\
          &|& \expr\wedge \expr  \ |\ \expr\vee \expr \ |\ \neg\expr & \text{operadores lógicos} \\
          &|& \ife \expr\thene \expr\elsee \expr \\
          &|& \la \expr, ... \expr \ra \\
          &|& \expr . \natconst \\
          &|& \textbf{letrec}\var \equiv \lambda \var.\expr\ \textbf{in}\ \expr&\text{(Eval. Eager)} \\
          &|& \textbf{rec}\ \expr& \text{(Eval. Normal)} \\
          &|& \textbf{error}\ |\ \textbf{typeerror} \\
          \natconst & ::= & 0\ |\ 1\ |\ 2\ | .... \\
          \boolconst & ::= & \textbf{true}\ | \ \textbf{false}
    \end{array}\]

    \textbf{Formas canónicas}
    \[
      \begin{array}{llllll}
      \cnf & ::= & \intcnf\  |\  \boolcnf\ |\ \funcnf \ | \tuplecnf \\
      \intcnf & ::= & ...\ | \ -2\ | \ -1\ | \ 0\ |\ 1\ |\ 2\ | ... \\
      \boolcnf & ::= & \boolconst \\
      \funcnf & ::= & \lambda \var.\expr \\
      \tuplecnf & ::= & \la \la cnf \ra, ..., \la cnf \ra \ra
      \end{array}
    \]
  
  \subsection{Evaluación}
    \subsubsection{Compartido entre Normal y Eager}
      \PN Para todas las formas canónicas vale: \ov{z \Rightarrow z}
      \begin{itemize}
        \item \textbf{Aritméticos y relacionales:} $\oplus\in \{+,-,*,=,\neq,\leq,\geq,...\}, \ \oslash \in \{/, mod\}$
        \begin{itemize}
          \setlength{\columnsep}{.0cm}
          \begin{multicols}{3}
            \item $\begin{array}{c}
              \underline{\ \ e\ \Rightarrow\ \lfloor i\rfloor\ \ }\\
              -e\ \Rightarrow\ \lfloor -i\rfloor
              \end{array}
              $
            \item $\begin{array}{c}
              \underline{e\ \Rightarrow\ \lfloor i\rfloor\qquad e'\ \Rightarrow\ \lfloor i'\rfloor}\\
              e \oplus e'\ \Rightarrow\ \lfloor i\oplus i'\rfloor
              \end{array}
              $
            \item $\begin{array}{c}
              \underline{e\ \Rightarrow\ \lfloor i\rfloor\qquad e'\ \Rightarrow\ \lfloor i'\rfloor}\\
              e \oslash e'\ \Rightarrow\ \lfloor i\oslash i'\rfloor
              \end{array}
              $
              
              \[i'\neq 0\]
            \end{multicols}
          \end{itemize}
        \item \textbf{Booleanos:}
          \begin{itemize}
            \setlength{\columnsep}{.4cm}
            \begin{multicols}{3}
            \item $\begin{array}{c}
              \underline{\ \ e\ \Rightarrow\ \lfloor b\rfloor\ \ }\\
              \neg e\ \Rightarrow\ \lfloor \neg b\rfloor
              \end{array}
              $
            \item $\begin{array}{c}
              \underline{\ \ e\ \Rightarrow\ \textbf{true}\ \qquad e_0\ \Rightarrow\ z }\\
              \textbf{if}\ e\ \textbf{then}\ e_0\  \textbf{else}\ e_1\ \Rightarrow\ z
              \end{array}
              $
            \item $\begin{array}{c}
              \underline{\ \ e\ \Rightarrow\ \textbf{false}\ \qquad e_1\ \Rightarrow\ z }\\
              \textbf{if}\ e\ \textbf{then}\ e_0\  \textbf{else}\ e_1\ \Rightarrow\ z
              \end{array}
              $
            \end{multicols}
          \end{itemize}
        \item \textbf{Definiciones locales y patrones:} $\textbf{let}\ p_1 \equiv e_1, \ldots, p_n \equiv e_n\ \textbf{in}\ e = (\lambda p_1\ldots\lambda p_n.e) e_1 \ldots e_n$
          \[\begin{array}{c}
            \underline{e\ \Rightarrow\  z' \qquad e'/v \to z'\ \Rightarrow\ z} \\
            \textbf{let } v \equiv e \textbf{ in } e' \ \Rightarrow\ z
            \end{array}\]
        \item \textbf{Recursión:} Equivalencia entre la recursión Normal y Eager
          \[
            \letrecin{f \equiv \lambda v.e'}{e} \qquad  \equiv \qquad (\lambda f . e) \ \textbf{rec}(\lambda f . \lambda v. e')
          \]
      \end{itemize}
    
    \subsubsection{Normal}    
      \begin{itemize}
        \item \textbf{Funciones:}
          \begin{prooftree}
            \AxiomC{$e \bigstep \lambda v.e''$}
            \AxiomC{$(e''/v\to e') \bigstep z$} \RightLabel{(aplicación)}
            \BinaryInfC{$e e' \bigstep z$}
          \end{prooftree}
        \item \textbf{Booleanos:}
          \begin{itemize}
            \item $e \wedge e' = \IF{e}{e'}{false}$
            \item $e \vee e' = \IF{e}{true}{e'}$
            \item $e \Rightarrow e' = \IF{e}{e'}{true}$
          \end{itemize}
        \item \textbf{Tuplas:}
          \begin{multicols}{2}
            \vspace{3mm}
            $\begin{array}{c}
              \underline{\qquad \qquad \qquad \qquad \qquad \qquad}\\
              \la e_1, ..., e_n \ra \Rightarrow \la e_1, ..., e_n\ra
              \end{array}$
            $\begin{array}{c}
              \underline{\ \ e \Rightarrow \langle e_1,...,e_n\rangle\qquad e_k \Rightarrow z}  \ \ \text{ para } k \leq n \\
              e.\lfloor k\rfloor \Rightarrow\ z
              \end{array}$
          \end{multicols}
          \item \textbf{Recursión:}
            \[\begin{array}{c}
              \underline{ e\ (\textbf{rec}\ e) \Rightarrow z }\\
               \textbf{rec}\ e\Rightarrow \ z
              \end{array}\]
      \end{itemize}
        
    \subsubsection{Eager}
      \begin{itemize}
        \item \textbf{Funciones:}
          \begin{prooftree}
            \AxiomC{$e \bigstep \lambda v.e''$} 
            \AxiomC{$e' \bigstep z'$}
            \AxiomC{$(e''/v\to z') \bigstep z$} 
            \RightLabel{(aplicación)}
            \TrinaryInfC{$e e' \bigstep z$}
          \end{prooftree}
        \item \textbf{Booleanos:} $\owedge \in \{\wedge, \vee, \Rightarrow,...\}$
          \[\begin{array}{c}
          \underline{e\ \Rightarrow\ \lfloor b\rfloor\qquad e'\ \Rightarrow\ \lfloor b'\rfloor}\\
          e \owedge e'\ \Rightarrow\ \lfloor b \owedge b'\rfloor
          \end{array}\]
        \item \textbf{Tuplas:}
          \begin{multicols}{2}
            $\begin{array}{c}
              \underline{\ \ e_1 \Rightarrow z_1 \quad ... \quad \ e_n \Rightarrow z_n } \\
              \langle e_1,...,e_n\rangle\ \Rightarrow\ \langle z_1,...,z_n\rangle
            \end{array}$
            $\begin{array}{c}
              \underline{\ \ e \Rightarrow \langle z_1,...,z_n\rangle} \qquad \qquad \qquad \qquad \\
              e.\lfloor k\rfloor \Rightarrow\ z_k \qquad \ \text{ para } k \leq n
            \end{array}$
          \end{multicols}
        \item \textbf{Recursión:}
          \[\begin{array}{c}
            \underline{\qquad e/(f\mapsto \lambda v.\letrecin{f \equiv \lambda v.e'}{e'})
            \Rightarrow z\qquad } f \neq v\\
            \letrecin{f \equiv \lambda v.e'}{e} \Rightarrow \ z
          \end{array}\]
      \end{itemize}

  \subsection{Semántica denotacional}
    \subsubsection{Compartido entre Normal y Eager}
      \PN $V$: es el conjunto de valores, de la misma forma que a las formas canónicas las llamamos también valores en su momento.
      \PN $D$: es el conjunto de resultados, que incluyen valores y otras cosas, en este caso, sólo se agrega bottom.
      \begin{multicols}{2}
        \begin{eqnarray*}
          D &=& (V + \{\textbf{error}, \textbf{typeerror}\})_\bot \\
          V &\simeq& V_{int} + V_{bool} + V_{fun} + V_{tuple} \\
          \phi &\in& \ V \rightarrow\ V_{int} + V_{bool} + V_{fun} + V_{tuple} \\
          \psi &\in& \ V_{int} + V_{bool} + V_{fun} + V_{tuple} \rightarrow V \\ \\
          \text{ Donde } && V_{int} = \mathbb{Z} \\
          && V_{bool} = \mathbb{B} \\
          && V_{fun} \text{ y } V_{tuple} \text{ se definen para cada semántica} \\
        \end{eqnarray*}
        \begin{eqnarray*}
          \\ \\ 
          \iota_{norm} &=& \iota_{\bot} . \iota_{0} \in V \rightarrow D \\
          err &=& \iota_{\bot} . (\iota_{1} \ error) \in D \\
          tyerr &=& \iota_{\bot} . (\iota_{1} \ typeerror) \in D \\ \\
          \iota_{int} &=& \psi . \iota_{0} \in V_{int} \rightarrow V \\
          \iota_{bool} &=& \psi . \iota_{1} \in V_{bool} \rightarrow V \\
          \iota_{fun} &=& \psi . \iota_{2} \in V_{fun} \rightarrow V \\
          \iota_{tuple} &=& \psi . \iota_{3} \in V_{tuple} \rightarrow V \\
        \end{eqnarray*}
      \end{multicols}

      \PN Si $f\in V\rightarrow D$ entonces $f_{*}\in D\rightarrow D$ y
      \PN si $\ell \in \{int, bool, fun, tuple\}, f \in V_{\ell} \rightarrow D$ entonces se definen:
      \[\begin{array}{lllllll}
        f_* & (\iota_{norm}\ z) &=& f\ z\\
        f_* & (err) &=& err & \qquad \qquad f_{\ell} (\iota_{\ell}\ z) &=& f\ z \\
        f_* & (tyerr) &=& tyerr & \qquad \qquad f_{\ell} (\iota_{\ell'}\ z) &=& tyerr, \ \text{si } \ell \neq \ell'\\
        f_* & (\perp) &=& \perp
      \end{array}\]

      \begin{eqnarray*}
        \se{0}\eta &=& \iota_{norm}(\iota_{int} 0) \\
        \se{\textbf{true}}\eta &=& \iota_{norm}(\iota_{bool} T) \\ \\
        \se{-e}\eta &=& (\lambda i \in V_{int}. \iota_{norm}(\iota_{int} -i))_{int*}(\se{e}\eta) \\
        \se{\neg e}\eta &=& (\lambda b \in V_{bool}. \iota_{norm}(\iota_{bool} \neg b))_{bool*}(\se{e}\eta) \\ \\
      \end{eqnarray*}
      \begin{eqnarray*}
        \se{e_0+e_1}\eta &=& (\lambda i \in V_{int}.\ (\lambda j \in V_{int}. \iota_{norm}(\iota_{int} i+j))_{int*}(\se{e_1}\eta))_{int*}(\se{e_0}\eta) \\
        \se{e_0/e_1'}\eta &=& (\lambda i \in V_{int}. \ (\lambda j \in V_{int}. \ \left\lbrace 
        \begin{array}{lll}
          err & j = 0 \\
          \iota_{norm}(\iota_{int} i/j) & c.c
        \end{array}\right)_{int*} (\se{e_1}\eta))_{int*} (\se{e_0}\eta) \\
        \se{\IF{e}{e_0}{e_1}}\eta &=& (\lambda b \in V_{bool}. \ \left\lbrace 
        \begin{array}{lll}
          \se{e_0} & si b \\
          \se{e_1} & c.c \\
        \end{array}\right)_{bool*} (\se{e}\eta) \\ \\
        \se{\textbf{let} \ v \equiv e \textbf{ in } e'}\eta &=& (\lambda z \in V. \se{e'}[\eta | v : z])_{\ast}(\se{e}\eta) \\ \\
        \se{error}\eta &=& err \\
        \se{typeerror}\eta &=& tyerr
      \end{eqnarray*}

    \subsubsection{Normal}
      \PN $V_{fun} = D \rightarrow D \qquad V_{tuple} = D^{*}$
      \begin{eqnarray*}
        \Env &=& \var \to  D \\
        \llbracket\_\rrbracket &\in& \expr \to  Env \to  D \\
        \llbracket v \rrbracket\eta &=& \eta v \\
        \llbracket e_0\, e_1\rrbracket\eta &=& (\lambda f \in V_{fun}. f(\se{e_1}\eta))_{fun*} (\se{e_0}\eta) \\
        \llbracket\lambda x.e\rrbracket\eta &=& \iota_{norm}(\iota_{fun}(\lambda d \in D. \se{e}[\eta|x:d])) \\
        \se{\la e_1, ..., e_n \ra}\eta &=& \iota_{norm}(\iota_{tuple} \la \se{e_1}\eta, ..., \se{e_n}\eta \ra) \\
        \se{e.[k]}\eta &=& (\lambda t \in V_{tuple}. \ \left\lbrace 
        \begin{array}{lll}
          t.k & si \ k \leq \# t \\
          tyerr & c.c \\
        \end{array}\right)_{tuple*} (\se{e}\eta) \\
        \se{\textbf{rec}\  e} \eta &=& (\lambda f \in  V_{fun}.\ Y f)_{fun*} (\se{e}\eta ) \\
        \text{donde} && Y f = \sqcup_{i \geq 0} f^{i} \underline{\bot}
      \end{eqnarray*}
        
    \subsubsection{Eager}
      \PN $V_{fun} = V \rightarrow D \qquad V_{tuple} = V^{*}$
      \begin{eqnarray*}
        Env &=& \var \to V \\
        \llbracket\_\rrbracket &\in& \expr \to Env \to D \\
        \llbracket v\rrbracket\eta &=& \iota_{norm}(\eta v) \\
        \llbracket e_0\, e_1\rrbracket\eta &=& (\lambda f \in V_{fun}. f_{*} (\se{e_1}\eta))_{fun*} (\se{e_0}\eta) \\
        \llbracket\lambda x.e\rrbracket\eta &=& \iota_{norm}(\iota_{fun}(\lambda z \in V. \se{e}[\eta|x:z])) \\
        \se{\la e_1, ..., e_n \ra}\eta &=& (\lambda z_1 \in V. ... (\lambda z_n \in V . \iota_{norm}(\iota_{tuple} \la z_1, ..., z_n\ra))_{*} (\se{e_n}\eta) ...)_{*} (\se{e_1}\eta) \\
        \se{e.[k]}\eta &=& (\lambda t \in V_{tuple}. \ \left\lbrace 
        \begin{array}{lll}
          \iota_{norm} t.k & si \ k \leq \# t \\
          tyerr & c.c \\
        \end{array}\right)_{tuple*} (\se{e}\eta) \\ \\
        \se{\letrecin{v \equiv \lambda u.e}{e'}}\eta &=& \se{e'} [\eta |v:\iota_{fun} Y_{V_{fun}} F] \\
        \text{donde} && F\ f\ z = \se{e}[\eta| v: \iota_{fun} f | u:z] \\
        && Y_{V_{fun}} F = \sqcup_{i \geq 0} F^{i} \underline{\bot}
      \end{eqnarray*}