[obsidian] vault backup: 2025-12-01 09:32:34

This commit is contained in:
2025-12-01 09:32:34 +09:00
parent 81b0bb35a5
commit 449c752bd6
2 changed files with 33 additions and 10 deletions

View File

@@ -64,7 +64,7 @@ mimiumはコードを専用のVMバイトコードへコンパイルし実行す
図nにmimiumの内部表現Lambda-mmmに多段階計算の体系を加えた新しい内部表現 $\lambda_{Mmmm}$(Multi-stage version of $\lambda_{mmm}$)のシンタックスを定義する。 図nにmimiumの内部表現Lambda-mmmに多段階計算の体系を加えた新しい内部表現 $\lambda_{Mmmm}$(Multi-stage version of $\lambda_{mmm}$)のシンタックスを定義する。
型にはCode Type $`t$を加える 型にはCode Type $`t$を加える。(一般的な多段階計算言語では$\langle\tau\rangle$
$$ $$
\begin{align} \begin{align}
\tau ::= \tau ::=
@@ -76,7 +76,7 @@ $$
\end{align} \end{align}
$$ $$
式にはクオート($`e$)とスプライス($\$e$)を加える。これはMetaMLなど代表的な多段階計算言語における$.<e>.$と$\textasciitilde e$に対応するものである。mem(e)はシングルサンプルのディレイだが、これは遅延時間のデータを保存する必要がないため通常のディレイと区別して使用される。 式にはクオート($`e$)とスプライス($\$e$)を加える。これはMetaMLなど代表的な多段階計算言語における$.\langle e\rangle.$と$\textasciitilde e$という記法に対応するものである。
$$ $$
\begin{align} \begin{align}
e ::= e ::=
@@ -87,11 +87,11 @@ e ::=
|&\quad e.n \quad& n \in \mathbb{N}\ [proj]&\\ |&\quad e.n \quad& n \in \mathbb{N}\ [proj]&\\
|&\quad \lambda x.e& [abs]&\\ |&\quad \lambda x.e& [abs]&\\
|&\quad let\; x\; =\; e_1\; in\; e_2& [let]&\\ |&\quad let\; x\; =\; e_1\; in\; e_2& [let]&\\
|&\quad delay(x,e_{time},v_{bound})&[delay]&\\
|&\quad mem(e) &[mem]&\\
|&\quad feed\ x.e &[feed]&\\
|&\quad `e &[quote]&\\ |&\quad `e &[quote]&\\
|&\quad $e &[splice]& |&\quad $e &[splice]&\\
|&\quad delay(n,e_{time},v_{bound})&[delay]&\\
|&\quad mem(e) &[mem]&\\
|&\quad feed\ x.e &[feed]&
\end{align} \end{align}
$$ $$
@@ -105,7 +105,10 @@ v ::=
$$ $$
セマンティクスをどこまで書くか、タプルを入れるか delay,mem,feedは信号処理用のプリミティブである。mem(e)はシングルサンプルのディレイだが、これは遅延時間のデータを保存する必要がないため通常のディレイと区別して使用される。これら3つのプリミティブはステージ1に束縛された組み込み関数のように扱われ、ステージ評価で現れるとエラーになる。
また、多段階計算において重要な、`run`プリミティブを用いて一つ上のステージで定義されたものをその場で使用する越段階埋め込みCross-Stage Persistenceはmimiumでは実装されていない。一方、コンパイル時に計算した数値などをランタイムで使用するために、プリミティブをコード型へ持ち上げる`lift`関数はプリミティブとして用意されている。mimiumの型システムは現時点でジェネリクスを搭載していないため、各基本型毎に異なる名前の組み込み関数floatに対するlift_fなどが用意される。
操作的意味論 操作的意味論
@@ -151,10 +154,10 @@ fn dsp(){
fn cascade(n,gen){ fn cascade(n,gen){
if (n>0.0){ if (n>0.0){
let multiplier = 1.0-(1.0/(n*3)) |> lift_f let multiplier = 1.0-(1.0/(n*3)) |> lift_f
`{|rate| rate + ($gen)(rate/3)* 0.5 * rate* $multiplier `|rate| rate + gen!(rate/3)* rate* $multiplier
|> $cascade(n - 1.0 ,gen) } |> $cascade(n - 1.0 ,gen)
}else{ }else{
`{|rate| ($gen)(rate)} `|rate| gen![]()(rate)
} }
} }
#stage(main) #stage(main)