baco
/
l-c2019
mirror of https://gitlab.com/baco/l-c2019.git
1
0
Fork 0
Code Issues Releases Wiki Activity

Change letrec-in commands into only one

This commit is contained in:
Dionisio E Alonso 2019-06-20 19:29:44 -03:00
parent f2cc93170e
commit 50cdb101b2
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
docs/Iswim_cheatsheet.tex
View File

@ -36,8 +36,7 @@
\newcommand\If[3]{\ensuremath{\kw{if}\,{#1}\,\kw{then}\,{#2}\,\kw{else}\,{#3}}}
\newcommand\While[2]{\ensuremath{\kw{while}\,{#1}\,\kw{do}\,{#2}}}
\newcommand\NewVar[3]{\ensuremath{\kw{newvar}\,{#1}\coloneqq{#2}\,\kw{in}\,{#3}}}
\newcommand\In{\,\kw{in}\,}
\newcommand\LetRec{\kw{letrec}\,}
\newcommand\LetRec[3]{\ensuremath{\kw{letrec}\,{#1}\equiv{#2}\,\kw{in}\,{#3}}}
\newcommand\Rec{\kw{rec}\,}
\newcommand\Val{\kw{val}\,}
\newcommand\MkRef{\kw{ref}\,}
@ -84,7 +83,7 @@
\(\kw{error}\) & \multicolumn{2}{c|}{} & \multicolumn{2}{c|}{\(\textit{err}\)} \\\hline
\(\kw{typeerror}\) & \multicolumn{2}{c|}{} & \multicolumn{2}{c|}{\(\textit{tyerr}\)} \\\hline
\makecell{\(\langle e_0, \dots, e_{n-1}\rangle\)\\\\\(e.\lfloor k\rfloor\)} & {\AxiomC{\(e \underset{N}{\Rightarrow} \langle e_0, \dots, e_{n-1}\rangle\)}\AxiomC{\(e_k \underset{N}{\Rightarrow} z\)}\RightLabel{\scriptsize{(\(k<n\))}}\BinaryInfC{\(e.\lfloor k\rfloor \underset{N}{\Rightarrow} z\)}\DisplayProof} & \makecell{\AxiomC{\(e_0 \underset{E}{\Rightarrow} z_0\)}\AxiomC{\(\ldots\)}\AxiomC{\(e_{n-1} \underset{E}{\Rightarrow} z_{n-1}\)}\TrinaryInfC{\(\langle e_0, \ldots, e_{n-1}\rangle \underset{E}{\Rightarrow} \langle z_0, \ldots, z_{n-1}\rangle\)}\DisplayProof \\\\ \AxiomC{\(e \underset{E}{\Rightarrow} \langle z_0, \ldots, z_{n-1}\rangle\)}\RightLabel{(\(k<n\))}\UnaryInfC{\(e.\lfloor k\rfloor \underset{E}{\Rightarrow} z_k\)}\DisplayProof} & \makecell[l]{\(\iota_\textit{\underline{tuple}}\langle\llbracket e_0\rrbracket\eta, \dots, \llbracket e_{n-1}\rrbracket\eta\rangle\)\\\\\(\left(\lambda t.\, \begin{cases}t_k & k< |t| \\ \textit{tyerr} & \text{c.c.}\end{cases}\right)_\textit{tuple *}(\llbracket e\rrbracket\eta)\)} \textsuperscript{\ref{types}} & \makecell[l]{\((\lambda z_0 \in V.\, (\lambda z_1 \in V.\, \ldots\)\\\(\quad (\lambda z_{n-1} \in V.\, \iota_\textit{\underline{tuple}} \langle z_0, \ldots, z_{n-1}\rangle)_*(\llbracket e_{n-1}\rrbracket\eta)\)\\\(\ldots)_*(\llbracket e_1\rrbracket\eta))_*(\llbracket e_0\rrbracket\eta)\)\\\\\(\left(\lambda t.\, \begin{cases}\iota_\textit{norm}t_k & k< |t| \\ \textit{tyerr} & \text{c.c.}\end{cases}\right)_\textit{tuple *}(\llbracket e\rrbracket\eta)\)} \textsuperscript{\ref{types}} \\\hline
\makecell{\(\LetRec v\equiv\lambda u.\, e \In e'\)\\\textsuperscript{(\textit{E})}\\\(\Rec e\)\\\textsuperscript{(\textit{N})}} & {\AxiomC{\(e\,(\Rec e) \underset{N}{\Rightarrow} z\)}\UnaryInfC{\(\Rec e \underset{N}{\Rightarrow} z\)}\DisplayProof} & \makecell{{\AxiomC{\((e'/_{v \mapsto \lambda u.\, e^*_0}) \underset{E}{\Rightarrow} z\)}\UnaryInfC{\(\LetRec v\equiv\lambda u.\, e \In e' \underset{E}{\Rightarrow} z\)}\DisplayProof}\\\\{donde \(e^*_0 = \LetRec v\equiv\lambda u.\, e \In e\)}} & \makecell{\((\lambda f \in V_\textit{fun}.\, Y_D\, f)_\textit{fun *}(\llbracket e\rrbracket\eta)\)\\\\\(Y_D\, f = \bigsqcup_i f^i\dbot\)} & \makecell{\(\llbracket e'\rrbracket[\eta | v: \iota_\textit{fun} g]\)\\\\\(F\,f\,z = \llbracket e\rrbracket[\eta | v: \iota_\textit{fun} f | u: z]\)\\\(g = Y_{V_\textit{fun}}\, F = \bigsqcup_i F^i\dbot\)} \\\hline
\makecell{\LetRec{v}{\lambda u.\, e}{e'}\\\textsuperscript{(\textit{E})}\\\(\Rec e\)\\\textsuperscript{(\textit{N})}} & {\AxiomC{\(e\,(\Rec e) \underset{N}{\Rightarrow} z\)}\UnaryInfC{\(\Rec e \underset{N}{\Rightarrow} z\)}\DisplayProof} & \makecell{{\AxiomC{\((e'/_{v \mapsto \lambda u.\, e^*_0}) \underset{E}{\Rightarrow} z\)}\UnaryInfC{\(\LetRec{v}{\lambda u.\, e}{e'} \underset{E}{\Rightarrow} z\)}\DisplayProof}\\\\{donde \(e^*_0 = \LetRec{v}{\lambda u.\, e}{e}\)}} & \makecell{\((\lambda f \in V_\textit{fun}.\, Y_D\, f)_\textit{fun *}(\llbracket e\rrbracket\eta)\)\\\\\(Y_D\, f = \bigsqcup_i f^i\dbot\)} & \makecell{\(\llbracket e'\rrbracket[\eta | v: \iota_\textit{fun} g]\)\\\\\(F\,f\,z = \llbracket e\rrbracket[\eta | v: \iota_\textit{fun} f | u: z]\)\\\(g = Y_{V_\textit{fun}}\, F = \bigsqcup_i F^i\dbot\)} \\\hline
\end{longtable}
}
@ -104,10 +103,10 @@
\(v\) & & \(\iota_\textit{norm}\langle\sigma, \eta v\rangle\) \\\hline
\(e\, e'\) & {\AxiomC{\(\sigma, e \Rightarrow \lambda v.\, e_0, \sigma'\)} \AxiomC{\(\sigma', e' \Rightarrow z', \sigma''\)} \AxiomC{\(\sigma'', (e_0/_{v \mapsto z'}) \Rightarrow z, \sigma'''\)} \TrinaryInfC{\(\sigma, e\, e' \Rightarrow z, \sigma'''\)} \DisplayProof} & \((\lambda \langle\sigma', f\rangle \in \Sigma\times V_\textit{fun}.\, f_\textit{*}(\llbracket e'\rrbracket\eta\sigma'))_\textit{fun *}(\llbracket e\rrbracket\eta\sigma)\) \\\hline
\(\lambda v.\, e\) & \textsuperscript{\ref{canonic}} & \(\iota_\textit{norm}\langle\sigma, \iota_\textit{fun}(\lambda \langle\sigma', z\rangle.\, \llbracket e\rrbracket[\eta | v: z]\sigma')\rangle\) \\\hline
\(\LetRec v \equiv \lambda u.\, e \In e'\) & \textsuperscript{\ref{appl}} & \makecell{\(\llbracket e'\rrbracket[\eta | v: \iota_\textit{fun} g]\sigma\) \\ \(F\, f\, \langle\sigma', z\rangle = \llbracket e\rrbracket[\eta| v: \iota_\textit{fun} f | u: z]\sigma'\) \quad \(g = Y_\textit{fun}F\)} \\\hline
\LetRec{v}{\lambda u.\, e}{e'} & \textsuperscript{\ref{appl}} & \makecell{\(\llbracket e'\rrbracket[\eta | v: \iota_\textit{fun} g]\sigma\) \\ \(F\, f\, \langle\sigma', z\rangle = \llbracket e\rrbracket[\eta| v: \iota_\textit{fun} f | u: z]\sigma'\) \quad \(g = Y_\textit{fun}F\)} \\\hline
\(e; e'\) & {\AxiomC{\(\sigma, e \Rightarrow z, \sigma'\)} \AxiomC{\(\sigma', e' \Rightarrow z', \sigma''\)} \BinaryInfC{\(\sigma, e; e' \Rightarrow z', \sigma''\)}\DisplayProof} & \((\lambda \langle\sigma', z\rangle.\, \llbracket e'\rrbracket\eta\sigma')_\textit{*}(\llbracket e\rrbracket\eta\sigma)\) \\\hline
\NewVar{v}{e}{e'} & {\AxiomC{\(\sigma, e \Rightarrow z, \sigma'\)} \AxiomC{\([\sigma' | r: z], (e'/_{v \mapsto r}) \Rightarrow z', \sigma''\)} \RightLabel{donde \(r = \textit{new}(\sigma')\)} \BinaryInfC{\(\sigma, \NewVar{v}{e}{e'} \Rightarrow z', \sigma''\)}\DisplayProof} & \makecell{\(\llbracket e'\rrbracket[\eta | v: \iota_\textit{ref} r][\sigma' | r: z]\); donde \(r = \textit{new}(\sigma')\) \\---\\ por: \(\left(\lambda\langle\sigma'', z\rangle\right.\, \llbracket e'\rrbracket[\eta | v: z]\sigma'')_\textit{*}\llbracket\MkRef e\rrbracket\eta\sigma\),\quad con: \(\llbracket\MkRef e\rrbracket\eta\sigma = \iota_\textit{norm}\langle[\sigma' | r: z], \iota_\textit{ref} r\rangle\)} \footnote{sup. \(\llbracket e\rrbracket\eta\sigma \notin \{\textit{err}, \textit{tyerr}, \bot\}\)} \\\hline
\While{e}{e'} & \makecell{{\AxiomC{\(\sigma, e \Rightarrow \textit{False}, \sigma'\)}\UnaryInfC{\(\sigma, \While{e}{e'} \Rightarrow \langle\rangle, \sigma'\)}\DisplayProof} \\\\ {\AxiomC{\(\sigma, e \Rightarrow \textit{True}, \sigma'\)}\AxiomC{\(\sigma', e'; \While{e}{e'} \Rightarrow z'. \sigma''\)}\BinaryInfC{\(\sigma, \While{e}{e'} \Rightarrow z, \sigma''\)}\DisplayProof}} & \makecell{\(\llbracket\LetRec w \equiv \lambda v.\, \If{e}{e' ; w\,v}{\textit{skip}} \In w\langle\rangle\rrbracket\eta\sigma = g\, \langle\sigma, \iota_\textit{tuple}\langle\rangle\rangle\) \\---\\ \(F\,h\,\langle\sigma, z\rangle = \left(\lambda \langle\sigma', b\rangle.\, \begin{cases} \left(\lambda\langle\sigma'', z'\rangle.\, \iota_\textit{norm}\langle\sigma'', h\, \langle\sigma'', z\rangle\rangle\right)_\textit{*}\left(\llbracket e'\rrbracket\tilde\eta\sigma'\right) & b \\ \iota_\textit{norm}\langle\sigma', \iota_\textit{tuple}\langle\rangle\rangle & \neg b \end{cases}\right)_\textit{bool *}\left(\llbracket e\rrbracket\tilde\eta\sigma\right)\)\\\(g = Y_\textit{fun}\,F \qquad \tilde\eta = [\eta | w: \iota_\textit{fun} h | v: z]\)} \\\hline
\While{e}{e'} & \makecell{{\AxiomC{\(\sigma, e \Rightarrow \textit{False}, \sigma'\)}\UnaryInfC{\(\sigma, \While{e}{e'} \Rightarrow \langle\rangle, \sigma'\)}\DisplayProof} \\\\ {\AxiomC{\(\sigma, e \Rightarrow \textit{True}, \sigma'\)}\AxiomC{\(\sigma', e'; \While{e}{e'} \Rightarrow z'. \sigma''\)}\BinaryInfC{\(\sigma, \While{e}{e'} \Rightarrow z, \sigma''\)}\DisplayProof}} & \makecell{\(\llbracket\LetRec{w}{\lambda v.\, \If{e}{e' ; w\,v}{\textit{skip}}}{w\langle\rangle}\rrbracket\eta\sigma = g\, \langle\sigma, \iota_\textit{tuple}\langle\rangle\rangle\) \\---\\ \(F\,h\,\langle\sigma, z\rangle = \left(\lambda \langle\sigma', b\rangle.\, \begin{cases} \left(\lambda\langle\sigma'', z'\rangle.\, \iota_\textit{norm}\langle\sigma'', h\, \langle\sigma'', z\rangle\rangle\right)_\textit{*}\left(\llbracket e'\rrbracket\tilde\eta\sigma'\right) & b \\ \iota_\textit{norm}\langle\sigma', \iota_\textit{tuple}\langle\rangle\rangle & \neg b \end{cases}\right)_\textit{bool *}\left(\llbracket e\rrbracket\tilde\eta\sigma\right)\)\\\(g = Y_\textit{fun}\,F \qquad \tilde\eta = [\eta | w: \iota_\textit{fun} h | v: z]\)} \\\hline
\end{longtable}
\end{document}