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 -->
$$<!-- line:87 -->
<!-- line:88 -->
## 実用スモールステップ意味論<!-- line:89 -->
<!-- line:90 -->
アイデア：クロージャ呼び出しとそれ以外の関数呼び出し（グローバルに登録されたものと即時呼び出しされるものとか）を分けよう<!-- line:91 -->
<!-- line:92 -->
OCamlでの疑似コード（未完成）<!-- line:93 -->
<!-- line:94 -->
```Ocaml
type expr = NumLit of float<!-- line:96 -->
| Var of string<!-- line:97 -->
| App of expr * expr<!-- line:98 -->
| Lam of string * expr<!-- line:99 -->
| Delay of int * expr * expr<!-- line:100 -->
| Feed of string * expr<!-- line:101 -->
| Quote of expr<!-- line:102 -->
| Splice of expr<!-- line:103 -->
| Tuple of expr list<!-- line:104 -->
| Proj of expr * int<!-- line:105 -->
type bound = string * value<!-- line:106 -->
and env = bound list<!-- line:107 -->
and value = Real of float<!-- line:108 -->
| OpenFn of string * expr * int<!-- line:109 -->
| Closure of string * expr * env<!-- line:110 -->
| Code of expr<!-- line:111 -->
type state = float list<!-- line:112 -->
type stage = int<!-- line:113 -->
type stateptr = int<!-- line:114 -->
<!-- line:115 -->
let lookup: string->env->value =<!-- line:116 -->
fun name env -> let finder = fun (n,v) -> n == name in<!-- line:117 -->
let (_n,v) = List.find finder env in<!-- line:118 -->
v<!-- line:119 -->
<!-- line:120 -->
<!-- line:121 -->
<!-- line:122 -->
let rec contain_freevars: string -> expr -> env -> bool = <!-- line:123 -->
...<!-- line:124 -->
<!-- line:125 -->
<!-- line:126 -->
let states = ... in<!-- line:127 -->
let stateptr = 0 in<!-- line:128 -->
let rec eval : stage -> expr -> env -> value = <!-- line:129 -->
fun stage e env -> match e with<!-- line:130 -->
| Var(name) -><!-- line:131 -->
lookup env name<!-- line:132 -->
| Lam(x,e) -><!-- line:133 -->
if contains_freevar(e) then OpenFn(x,e,statesize e)<!-- line:134 -->
else Closure(x,e,env)<!-- line:135 -->
| App(ef,ea) -><!-- line:136 -->
let va = eval stage ea env in<!-- line:137 -->
let vf = eval stage ef env in<!-- line:138 -->
match vf with<!-- line:139 -->
| OpenFn(x,e,size)-> let r = eval stage e ((x,va)::env) in<!-- line:140 -->
shift stateptr size;<!-- line:141 -->
r<!-- line:142 -->
| Closure(x,e,cenv) -> eval stage e ((x,va)::cenv)<!-- line:143 -->
| Delay(n,et,ev) -><!-- line:144 -->
let v = eval stage ev env in<!-- line:145 -->
let vt = eval stage et env in<!-- line:146 -->
update_ringbuf state stateptr v vt<!-- line:147 -->
| Feed(x,e)-><!-- line:148 -->
let size = statesize e in<!-- line:149 -->
let last = getstate state stateptr in<!-- line:150 -->
let current = eval stage e ((x,last)::env)<!-- line:151 -->
state[stateptr] := current;<!-- line:152 -->
last<!-- line:153 -->
| Quote(e)-><!-- line:154 -->
rebuild stage+1 e env<!-- line:155 -->
| Splice(e)-><!-- line:156 -->
let v = rebuild stage-1 e env<!-- line:157 -->
match v with<!-- line:158 -->
| Code(e) -> eval e env<!-- line:159 -->
_-> raise<!-- line:160 -->
and rebuild : stage -> expr -> env =<!-- line:161 -->
fun stage e env -> <!-- line:162 -->
if stage == 0 then eval e env<!-- line:163 -->
else Code(e)<!-- line:164 -->
<!-- line:165 -->
<!-- line:166 -->
```