85 lines
2.5 KiB
Markdown
85 lines
2.5 KiB
Markdown
|
---
|
|||
|
|
date: 2024-11-23 08:05
|
|||
|
|
---
|
|||
|
|
|
|||
|
|
#mimium
|
|||
|
|
|
|||
|
|
元々のLambda-mmmは実際に使われているmimiumでの中間表現と比べて以下のような差がある
|
|||
|
|
|
|||
|
|
- タプルなど構造化された型がない（実際にはVMの命令にワードサイズの情報を付加しているのでこれは結構重要）
|
|||
|
|
- letで宣言された変数に対しては代入ができる（部分的に参照型が使われている）
|
|||
|
|
- delayやfeedの項を終端の値として扱う意味論（コンパイル時の正規化作業）と、実際の評価に使われる意味論が混ざっている
|
|||
|
|
|
|||
|
|
## 型
|
|||
|
|
|
|||
|
|
$$
|
|||
|
|
\begin{align}
|
|||
|
|
\tau ::=
|
|||
|
|
& \quad unit &\\
|
|||
|
|
|&\quad R \quad &\\
|
|||
|
|
|&\quad I_n \quad &n \in \mathbb{N} \\
|
|||
|
|
|& \quad \tau * \tau \quad &\\
|
|||
|
|
|&\quad \tau → \tau &\\
|
|||
|
|
% |&\quad \langle \tau \rangle
|
|||
|
|
\end{align}
|
|||
|
|
$$
|
|||
|
|
|
|||
|
|
## 値
|
|||
|
|
|
|||
|
|
$$
|
|||
|
|
\begin{align}
|
|||
|
|
v ::=
|
|||
|
|
&\quad unit & \\
|
|||
|
|
|&\quad R & R \in \mathbb{R} \\
|
|||
|
|
|&\quad v * v \quad &\\
|
|||
|
|
|&\quad \lambda x.e \\
|
|||
|
|
|&\quad delay(e,e_{time},v_{bound})\\
|
|||
|
|
|&\quad feed\ x.e
|
|||
|
|
\end{align}
|
|||
|
|
$$
|
|||
|
|
## 項
|
|||
|
|
|
|||
|
|
$$
|
|||
|
|
\begin{align}
|
|||
|
|
e_p ::=
|
|||
|
|
&\quad unit & \\
|
|||
|
|
|&\quad R & R \in \mathbb{R} \\
|
|||
|
|
|
|||
|
|
e ::=
|
|||
|
|
&\quad e_p & \\
|
|||
|
|
|&\quad e,e & [tuple]\\
|
|||
|
|
|&\quad x\quad &[var]\\
|
|||
|
|
|&\quad \lambda x.e &[abs]\\
|
|||
|
|
.|&\quad let\; x\; =\; e\; in\; e &[let]\\
|
|||
|
|
|&\quad e\; e &[app]\\
|
|||
|
|
|&\quad delay(e,e_{time},e_{bound}) &[delay]\\
|
|||
|
|
|&\quad feed\; x.e &[feed]
|
|||
|
|
\end{align}
|
|||
|
|
$$
|
|||
|
|
|
|||
|
|
## 評価環境（正規化時）
|
|||
|
|
|
|||
|
|
$$
|
|||
|
|
\begin{align}
|
|||
|
|
E ::= &\; ()\\
|
|||
|
|
&|\; E :: (x,v)
|
|||
|
|
\end{align}
|
|||
|
|
$$
|
|||
|
|
|
|||
|
|
## 正規化の操作的意味論
|
|||
|
|
|
|||
|
|
$$
|
|||
|
|
\begin{gathered}
|
|||
|
|
&\frac{E \vdash e_{bound} \Downarrow v_{bound} }
|
|||
|
|
{E \vdash delay\; e\;e_{time}\; e_{bound} \Downarrow delay\; e \; e_{time}\; v_{bound} } &\textrm{[E-DELAY]} \\\\
|
|||
|
|
|
|||
|
|
&\frac{}{E^n \vdash\ \lambda x.e \Downarrow cls(\lambda x.e , E^n) }\ &\textrm{[E-LAM]} \\
|
|||
|
|
|
|||
|
|
&\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]} \\
|
|||
|
|
|
|||
|
|
&\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]}\\
|
|||
|
|
&\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]}\\
|
|||
|
|
&\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]}
|
|||
|
|
\end{gathered}
|
|||
|
|
$$
|