[obsidian] vault backup: 2025-11-29 14:24:51[
Some checks failed
Build / build (push) Failing after 14m46s

This commit is contained in:
2025-11-29 14:24:51 +09:00
parent e1b45839ad
commit d4a58a7eea
2 changed files with 47 additions and 5 deletions

View File

@@ -59,19 +59,47 @@ mimiumはコードを専用のVMバイトコードへコンパイルし実行す
## 多段階計算
多段階計算は、型付きラムダ計算に対して、計算のステージを複数段階に分割する明示的なシンタックスを導入するものである。Lisp系言語のquote/splice機能[@lisp]のように、部分的に計算したコード片を埋め込むようなものを想定しているが、不正な値が埋め込まれないことを型システムとして保証することが特徴である。
実用的な例では、Scala 3でのマクロや、関数型組版処理エンジンSaTysFi[@suwaMLStyleModuleSystem2024]のように、言語内DSLを型安全にライブラリとして実装することを想定しているものがある。
多段階計算は、型付きラムダ計算に対して、計算のステージを複数段階に分割する明示的なシンタックスを導入するものである。Lisp系言語のquote/splice機能[@lisp]のように、部分的に計算したコード片を埋め込むようなものを想定しているが、不正な値が埋め込まれないことを型システムとして保証することが特徴である逆に、通常マクロに期待される型システムの範囲を超えたメタ操作を行うことは許されない。実用的な例では、Scala 3でのマクロや、関数型組版処理エンジンSaTysFi[@suwaMLStyleModuleSystem2024]のように、言語内DSLを型安全にライブラリとして実装することを想定しているものがある。mimiumにおいては、多段階計算はコンパイル時に行う計算シグナルグラフのルーティングの決定と、ランタイム時に行う計算実際のオーディオ処理を区別するのに用いている
### シンタックス
### シンタックスの拡張
図nにmimiumの内部表現Lambda-mmmに多段階計算の体系を加えた新しい内部表現 $\lambda_{Mmmm}$(Multi-stage version of $\lambda_{mmm}$)のシンタックスを定義する。
型にはCode Type $\langle t\rangle$を加える
$$
\begin{align}
\tau ::=
&\quad R \quad &\\
|&\quad I_n \quad &n \in \mathbb{N} \\
|&\quad \tau → \tau &\\
|&\quad \langle \tau \rangle
\end{align}
$$
式にはクオートとスプライスを加える。mem(e)はシングルサンプルのディレイだが、これは遅延時間のデータを保存する必要がないため通常のディレイと区別して使用される。
$$
\begin{align}
e ::=
&\quad R & R \in \mathbb{R} [number]&\\
|&\quad e \ e \quad& [app]&\\
|&\quad \lambda x.e& [abs]&\\
|&\quad let\; x\; =\; e\; in\; e& [let]&\\
|&\quad delay(x,e_{time},v_{bound})&[delay]&\\
|&\quad mem(e) &[mem]&\\
|&\quad feed\ x.e &[feed]&\\
|&\quad `(e) &[quote]&\\
|&\quad $(e) &[splice]&
\end{align}
$$
$$
\begin{align}
v ::=
|&\quad R & R \in \mathbb{R} [number]&\\
|&\quad cls(e,E) &[closure]&\\
|&\quad \langle v \rangle &[code]&\\
\end{align}
$$
### シンタックスシュガー