diff --git a/content/mimium新内部表現の構想.md b/content/mimium新内部表現の構想.md
index d79dba82..3a564364 100644
--- a/content/mimium新内部表現の構想.md
+++ b/content/mimium新内部表現の構想.md
@@ -63,9 +63,11 @@ e_{feed} \; ::=& \quad e\\
 $$
 
 こんな雰囲気で相互再帰させれば、、、いいんか？ダメだな
-
 ステージの概念さえ導入できれば値レベルで弾けるのかな
 
+
+
+
 %%
 $$
 \frac{\Gamma x = R_a }{\Gamma \vdash x:R}
diff --git a/content/多段階計算.md b/content/多段階計算.md
index ab1d9a0a..28f39ad7 100644
--- a/content/多段階計算.md
+++ b/content/多段階計算.md
@@ -27,3 +27,7 @@ http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf
 
 
 [SATySFi の多段階計算入門](https://sankantsu.hatenablog.com/entry/2022/08/19/215024)
+
+## 依存型との組み合わせ
+
+[A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)
diff --git a/content/音楽プログラミング言語の形式化.md b/content/音楽プログラミング言語の形式化.md
index 782bce53..5c22b740 100644
--- a/content/音楽プログラミング言語の形式化.md
+++ b/content/音楽プログラミング言語の形式化.md
@@ -107,4 +107,35 @@ fn lowpass(input,fb){
 
 というか果たしてそんなことはできるのだろうか
 
-あとは、Faustのエラーメッセージで入出力の数が合わないとかのエラーはマクロ展開後に発生するので、マクロを多用するほどエラーが読みづらくなる問題があるが、それは多分多段階計算の方が読みやすくなる・・・はず
\ No newline at end of file
+あとは、Faustのエラーメッセージで入出力の数が合わないとかのエラーはマクロ展開後に発生するので、マクロを多用するほどエラーが読みづらくなる問題があるが、それは多分多段階計算の方が読みやすくなる・・・はず
+
+## 実は無理に多段階計算じゃなくてもいい説
+
+解決方法は実はもう2パターンくらいある気がしてきた。
+
+### 1.あくまでコンパイラの最適化に任せる方向
+
+意味論としては、fixとfeedが混在してても（めちゃくちゃ非効率的とはいえ）コンパイルを通せるような仕組みをとにかく作る。具体的には、fix+feedを使う場合は渡す内部状態変数を固定サイズではなく、例えばリンクドリストで作るようにし、fixを深く実行するほどリンクリストを奥に辿っていき、まだ未確保な場合は適宜メモリをアロケートしてリストを伸ばしていくような形にする。
+
+現実的にはリンクドリストではなく動的ベクターとかで実装する。こうすると、例えば実際には定数で一定の深さまでしか展開されないことが自明な関数は、一回ダミーで1サンプルだけ実行すれば必要なメモリサイズは伺い知れる。
+
+もちろん、ちゃんとやるなら再帰関数の部分の定数畳み込みは実施するようにすればいいし、そうでないとしても、再帰関数が残ったままCのコードをエクスポートするような形でも実行直前に必要なメモリサイズは確定できるということになる。
+
+
+### 2.再帰を有限回しか行えないような意味論を定義する
+
+例えば、Faustでパターンマッチ使って再帰を行う場合は基本的にフィルタの次数とかをnとか、n,mとかで定義して0まで減らしていく、といったのがほとんど。ならばfixは上限の決まったInt型（ディレイの読み出しインデックスに使うのと同じ型）にしてしまえば、最低限必要なメモリサイズはコンパイル時に決定できる。
+
+ただ、そうするとユーザーからは、「なんだかよくわからんけど再帰する関数の第1引数には上限の決まったIntしか使えんらしい」という不条理感が残る
+
+### これら2つではカバーできないケース
+
+再帰の深さによって返したい型が変わるような多相を考えると厳しいかも。
+
+実際、Faustのパターンマッチングでの項書き換えは書き換えを適用するたびに異なる入出力数のノードを返すことができる（だからこそ`take`みたいな関数が定義できるわけだし）
+
+この辺は、多段階計算を使ったとしても生成したコードの型を変えるみたいなことは出来ないのでは？
+
+項でインデックスされた型＝依存型な気がするのよな
+
+[[多段階計算#依存型との組み合わせ]]