quartz-research-note/content/lambda-mmm(実用版).md

date

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(x,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}

実用スモールステップ意味論

アイデア：クロージャ呼び出しとそれ以外の関数呼び出し（グローバルに登録されたものと即時呼び出しされるものとか）を分けよう

OCamlでの疑似コード（未完成）

type expr = NumLit of float
          | Var of string
          | App of expr * expr
          | Lam of string * expr
          | Delay of int * expr * expr
          | Feed of string * expr
          | Quote of expr
          | Splice of expr
          | Tuple of expr list
          | Proj of expr * int
type bound = string * value
and env = bound list
and value = Real of float
           | OpenFn of string * expr * int
           | Closure of string * expr * env
           | Code of expr
type state = float list
type stage = int
type stateptr = int

let lookup: string->env->value =
 fun name env -> let finder = fun (n,v) -> n == name in
 let (_n,v) = List.find finder env in
 v



let rec contain_freevars: string -> expr -> env -> bool = 
 ...


let states = ... in
let stateptr = 0 in
let rec eval : stage -> expr -> env -> value = 
  fun stage e env -> match e with
| Var(name) ->
  lookup env name
| Lam(x,e) ->
  if contains_freevar(e) then OpenFn(x,e,statesize e)
  else Closure(x,e,env)
| App(ef,ea) ->
  let va = eval stage ea env in
  let vf = eval stage ef env in
  match vf with
   | OpenFn(x,e,size)-> let r = eval stage e ((x,va)::env) in
   shift stateptr size;
   r
   | Closure(x,e,cenv) -> eval stage e ((x,va)::cenv)
| Delay(n,et,ev) ->
 let v = eval stage ev env in
 let vt = eval stage et env in
 update_ringbuf state stateptr v vt
| Feed(x,e)->
 let size = statesize e in
 let last = getstate state stateptr in
 let current = eval stage e ((x,last)::env)
 state[stateptr] := current;
 last
| Quote(e)->
  rebuild stage+1 e env
| Splice(e)->
  let v = rebuild stage-1 e env
  match v with
  | Code(e) -> eval e env
  _-> raise
and rebuild : stage -> expr -> env =
fun stage e env -> 
 if stage == 0 then eval e env
 else Code(e)