tomoyanonymous/ifc-2024-lambdammm
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

written

Browse Source
This commit is contained in:
松浦 知也 Matsuura Tomoya
2024-07-11 09:25:51 +00:00
parent 1eb1783760
commit 08f9d0684f
2 changed files with 107 additions and 36 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
src/semantics.tex
View File

@@ -2,36 +2,36 @@
\centering
\begin{tabular}{ccc}
\begin{minipage}[b]{5cm}
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_1 \Downarrow v_1\ E^{n-v_1} \vdash e_2 \Downarrow v_2}{E^n \vdash\ delay\ e_1\ e_2 \Downarrow v_2}
\frac{E^n \vdash e_1 \Downarrow v_1 \ n>v_1 \ E^{n-v_1} \vdash e_2 \Downarrow v_2}{E^n \vdash\ delay\ n\ e_1\ e_2 \Downarrow v_2}
\end{equation*}\textrm{E-DELAY}
\end{minipage} &
\begin{minipage}[b]{5cm}
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{}{E^n \vdash\ \lambda x.e \Downarrow cls(\lambda x.e , E^n) }
\end{equation*}\textrm{E-LAM}
\end{minipage}&
\begin{minipage}[b]{5cm}
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{ E^{n-1} \vdash e \Downarrow v_1\ E^n, x \mapsto v_1 \vdash e \Downarrow v_2 }{E^n \vdash\ feed\ x\ e \Downarrow v_2}
\frac{ E^{n-1} \vdash e \Downarrow v_1\ E^n, x \mapsto v_1 \vdash e \Downarrow v_2 }{E^n, x \mapsto v_2\ \vdash\ feed\ x\ e \Downarrow v_1}
\end{equation*}\textrm{E-FEED}
\end{minipage}
\\
\begin{minipage}[b]{5cm}
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_c \Downarrow n \quad n > 0\ E^n \vdash e_t\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t else e_t \Downarrow v }
\frac{E^n \vdash e_c \Downarrow n \quad n > 0\ E^n \vdash e_t\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }
\end{equation*}\textrm{E-IFTRUE}
\end{minipage}
&
\begin{minipage}[b]{5cm}
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_c \Downarrow n \quad n \leqq0\ E^n \vdash e_e\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t else e_t \Downarrow v }
\frac{E^n \vdash e_c \Downarrow n \quad n \leqq0\ E^n \vdash e_e\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }
\end{equation*}\textrm{E-IFFALSE}
\end{minipage}
&