[obsidian] vault backup: 2025-12-19 16:28:14[

content/多段階計算と増分関数型リアクティブプログラミングによる信号処理のライブコーディング.md

@@ -97,18 +97,64 @@ $$
 \begin{align}
 v ::=
 	  |&\quad R & R \in \mathbb{R} [number]&\\
-      |&\quad cls(e,E) &[closure]&\\
+	  |&\quad openFn(x,e,statesize) &[closure]&\\
+      |&\quad closure(x,e,E) &[closure]&\\
       |&\quad \langle e \rangle &[code]&\\
 \end{align}
 $$
 
 
-delay,mem,feedは信号処理用のプリミティブである。mem(e)はシングルサンプルのディレイだが、これは遅延時間のデータを保存する必要がないため通常のディレイと区別して使用される。これら3つのプリミティブはステージ1に束縛された組み込み関数のように扱われ、ステージ０評価で現れるとエラーになる。
+delay,mem,feedは信号処理用のプリミティブである。mem(e)はシングルサンプルのディレイだが、これは遅延時間のデータを保存する必要がないため通常のディレイと区別して使用される。これら3つのプリミティブはステージ1に束縛された組み込み関数のように扱われ、ステージ0評価で現れるとエラーになる。
 
 また、多段階計算において重要な、`run`プリミティブを用いて一つ上のステージで定義されたものをその場で使用する越段階埋め込み（Cross-Stage Persistence）はmimiumでは実装されていない。一方、コンパイル時に計算した数値などをランタイムで使用するために、プリミティブをコード型へ持ち上げる`lift`関数はプリミティブとして用意されている。mimiumの型システムは現時点でジェネリクスを搭載していないため、各基本型毎に異なる名前の組み込み関数（floatに対するlift_fなど）が用意される。
 
 
-操作的意味論
+### 操作的意味論
+
+```ocaml
+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)
+ 
+
+```
+
+mimiumでは、
 
 グローバルな関数呼び出しとそれ以外の呼び出しの区別。式に自由変数があるかないかを区別する必要がある。それを表示的意味論に落とし込めるのか