52 lines
1.7 KiB
TeX
52 lines
1.7 KiB
TeX
\begin{figure*}[ht]
|
|
\centering
|
|
\begin{tabular}{ccc}
|
|
|
|
\begin{minipage}[b]{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}
|
|
\end{equation*}\textrm{E-DELAY}
|
|
\end{minipage} &
|
|
\begin{minipage}[b]{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}
|
|
\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}
|
|
\end{equation*}\textrm{E-FEED}
|
|
\end{minipage}
|
|
\\
|
|
\begin{minipage}[b]{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 }
|
|
\end{equation*}\textrm{E-IFTRUE}
|
|
\end{minipage}
|
|
&
|
|
\begin{minipage}[b]{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 }
|
|
\end{equation*}\textrm{E-IFFALSE}
|
|
\end{minipage}
|
|
&
|
|
\
|
|
\\
|
|
\multicolumn{3}{c}{
|
|
\begin{minipage}[b]{15cm}
|
|
\centering
|
|
\begin{equation*}
|
|
\frac{E^n \vdash e_1 \Downarrow cls(\lambda x_c.e_c, E^n_c) E^n \vdash e_2 \Downarrow v_2\ E^n_c,\ x_c \mapsto v_2 \vdash e_c \Downarrow v }{E^n \vdash\ e_1\ e_2 \Downarrow v }
|
|
\end{equation*}\textrm{E-APP}
|
|
\end{minipage}
|
|
}
|
|
\\
|
|
|
|
\end{tabular}
|
|
\caption{\label{fig:semantics}{\it Excerpt of the big-step semantics of $\lambda_{mmm}$.}}
|
|
\end{figure*} |