mimium
元々のLambda-mmmは実際に使われているmimiumでの中間表現と比べて以下のような差がある
- タプルなど構造化された型がない（実際にはVMの命令にワードサイズの情報を付加しているのでこれは結構重要）
- letで宣言された変数に対しては代入ができる（部分的に参照型が使われている）
- delayやfeedの項を終端の値として扱う意味論（コンパイル時の正規化作業）と、実際の評価に使われる意味論が混ざっている
型
\begin{align}<!-- line:16 -->
\tau ::=<!-- line:17 -->
& \quad unit &\\<!-- line:18 -->
|&\quad R \quad &\\<!-- line:19 -->
|&\quad I_n \quad &n \in \mathbb{N} \\<!-- line:20 -->
|& \quad \tau * \tau \quad &\\<!-- line:21 -->
|&\quad \tau → \tau &\\<!-- line:22 -->
% |&\quad \langle \tau \rangle<!-- line:23 -->
\end{align}<!-- line:24 -->
$$<!-- line:25 -->
<!-- line:26 -->
## 値<!-- line:27 -->
<!-- line:28 -->
$$<!-- line:29 -->
\begin{align}<!-- line:30 -->
v ::=<!-- line:31 -->
&\quad unit & \\<!-- line:32 -->
|&\quad R & R \in \mathbb{R} \\<!-- line:33 -->
|&\quad v * v \quad &\\<!-- line:34 -->
|&\quad \lambda x.e \\<!-- line:35 -->
|&\quad delay(x,e_{time},v_{bound})\\<!-- line:36 -->
|&\quad feed\ x.e<!-- line:37 -->
\end{align}<!-- line:38 -->
$$<!-- line:39 -->
ディレイは定数や関数を入力としては受け取らない（常に変数を参照する）<!-- line:40 -->
<!-- line:41 -->
## 項<!-- line:42 -->
<!-- line:43 -->
$$<!-- line:44 -->
\begin{align}<!-- line:45 -->
e_p ::=<!-- line:46 -->
&\quad unit & \\<!-- line:47 -->
|&\quad R & R \in \mathbb{R} \\<!-- line:48 -->
<!-- line:49 -->
e ::=<!-- line:50 -->
&\quad e_p & \\<!-- line:51 -->
|&\quad e,e & [tuple]\\ <!-- line:52 -->
|&\quad x\quad &[var]\\<!-- line:53 -->
|&\quad \lambda x.e &[abs]\\<!-- line:54 -->
.|&\quad let\; x\; =\; e\; in\; e &[let]\\<!-- line:55 -->
|&\quad e\; e &[app]\\<!-- line:56 -->
|&\quad delay(e,e_{time},e_{bound}) &[delay]\\<!-- line:57 -->
|&\quad feed\; x.e &[feed]<!-- line:58 -->
\end{align}<!-- line:59 -->
$$<!-- line:60 -->
<!-- line:61 -->
## 評価環境（正規化時）<!-- line:62 -->
<!-- line:63 -->
$$<!-- line:64 -->
\begin{align}<!-- line:65 -->
E ::= &\; ()\\<!-- line:66 -->
&|\; E :: (x,v)<!-- line:67 -->
\end{align}<!-- line:68 -->
$$<!-- line:69 -->
<!-- line:70 -->
## 正規化の操作的意味論<!-- line:71 -->
<!-- line:72 -->
$$<!-- line:73 -->
\begin{gathered}<!-- line:74 -->
&\frac{E \vdash e_{bound} \Downarrow v_{bound} }<!-- line:75 -->
{E \vdash delay\; e\;e_{time}\; e_{bound} \Downarrow delay\; e \; e_{time}\; v_{bound} } &\textrm{[E-DELAY]} \\\\<!-- line:76 -->
<!-- line:77 -->
&\frac{}{E^n \vdash\ \lambda x.e \Downarrow cls(\lambda x.e , E^n) }\ &\textrm{[E-LAM]} \\<!-- line:78 -->
<!-- line:79 -->
&\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}\ &\textrm{[E-FEED]} \\<!-- line:80 -->
<!-- line:81 -->
&\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 }\ &\textrm{[E-IFTRUE]}\\<!-- line:82 -->
&\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 }\ &\textrm{[E-IFFALSE]}\\<!-- line:83 -->
&\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 }\ &\textrm{[E-APP]}<!-- line:84 -->
\end{gathered}<!-- line:85 -->
$$<!-- line:86 -->