quartz-research-note/content/音楽プログラミング言語の形式化.md

#programming-language #research 


## 先行例

[[Faust]]


[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms]]

## 基礎知識

[[Coqの勉強]]


## [[mimium]]と[[多段階計算]]

[[mimium新内部表現の構想]]での検討材料

こういうのが計算できなかった(要するにfixpointの中で`self`を使うと必要な`self`のサイズを確定できない)

```rust
fn filterbank(N,input,lowestfreq, margin,Q,filter){
    if(N>0){
        return filter(input,lowestfreq+N*margin,Q)
                +  filterbank(N-1,input, lowestfreq,margin,Q,filter)
    }else{
        return 0
    }
}
```

仮に多段階計算だとしてちょっと型を明示してみる
まあ〜書きづらいよな

```rust
fn gen_filterbank(N:int,lowestfreq:float, margin:float,Q:float,filter:(float,float,float)->float)-> <(float,float,float)->float> {
	// level:0
    if(N>0){
        < //level:1
        |x| {
        filter(x,~(lowestfreq+N*margin),~(Q))
             + ~( //level:0
		       gen_filterbank(N-1,x, lowestfreq,margin,Q,filter)
		       )
        }
        >
                
    }else{
         <|x|{0}>
    }
}

fn filterbank(input:float, N:int,lowestfreq:float, margin:float,Q:float,filter:(float,float,float)->float)-> float{
	~(gen_filterbank(N,lowestfreq,margin,filter))(input)
}
```

filter同士の足し算を`+`の`infix`でやりたいよねえ
let多相じゃないよなあこれは

ていうかこれそもそも普通に高階関数じゃダメなんだろうか？

```rust
fn gen_filterbank(N,lowestfreq, margin,Q,filter)->(float->float){
	|input|{
	    if(N>0){
	        return filter(input,lowestfreq+N*margin,Q)
	                +  gen_filterbank(N-1,lowestfreq,margin,Q,filter)(input)
	    }else{
	        return 0
	    }
    }
}
```

いやーこれでもif文が展開されるのは実行時だから意味ないのか

---

あー、つまり

- ステージ0ではfixpointが使えてfeedが使えない
- ステージ1ではfeedが使えてfixpointが使えない

みたいな定義ができればいいんじゃなかろうか（というか、fixpointが使えるステージとfeedが使えるステージが交互に繰り返し出てくる、とかになればいけるのか？）

ステージ0でfixpointを使ったものを評価しきってステージ1に行く時には再帰は有限回の計算に展開されていることになる・・・のでは？

これ、同じように

- ステージ0でn個の要素数のものとして評価されたリストはステージ1からn要素のタプルとして見える

という前から考えていたこととも繋がるのでは？（というか、これが[[Kronos]]でやっている高階ラムダ計算というか、System F$\omega$なのか？）



問題はそれをユーザーに意識させずに書かせる方法かあ、結局Faustはそれができているからこそ強いわけで（いや、[Faustのパターンマッチ](https://ccrma.stanford.edu/~jos/aspf/Pattern_Matching_FAUST.html)は意味論破壊してHygienicとはいえマクロになってるから結局2段階なのか）

```rust
fn lowpass(input,fb){
	(1-fb)*input + fb*self
}
```

### Faustとかと比べたときのメリット

マクロ部分の生成段階も含めてCやC++のコードとして生成できるのなら、juceの`prepareToPlay`のような関数内でのDSPグラフのパラメトリックな変形（フィルターの次数を変えるとか）が実現できるかも（そこまでのことが求められてるかというと微妙な気もするが・・・）

というか果たしてそんなことはできるのだろうか

あとは、Faustのエラーメッセージで入出力の数が合わないとかのエラーはマクロ展開後に発生するので、マクロを多用するほどエラーが読みづらくなる問題があるが、それは多分多段階計算の方が読みやすくなる・・・はず

## 実は無理に多段階計算じゃなくてもいい説

解決方法は実はもう2パターンくらいある気がしてきた。

### 1.あくまでコンパイラの最適化に任せる方向

意味論としては、fixとfeedが混在してても（めちゃくちゃ非効率的とはいえ）コンパイルを通せるような仕組みをとにかく作る。具体的には、fix+feedを使う場合は渡す内部状態変数を固定サイズではなく、例えばリンクドリストで作るようにし、fixを深く実行するほどリンクリストを奥に辿っていき、まだ未確保な場合は適宜メモリをアロケートしてリストを伸ばしていくような形にする。

現実的にはリンクドリストではなく動的ベクターとかで実装する。こうすると、例えば実際には定数で一定の深さまでしか展開されないことが自明な関数は、一回ダミーで1サンプルだけ実行すれば必要なメモリサイズは伺い知れる。

もちろん、ちゃんとやるなら再帰関数の部分の定数畳み込みは実施するようにすればいいし、そうでないとしても、再帰関数が残ったままCのコードをエクスポートするような形でも実行直前に必要なメモリサイズは確定できるということになる。


### 2.再帰を有限回しか行えないような意味論を定義する

例えば、Faustでパターンマッチ使って再帰を行う場合は基本的にフィルタの次数とかをnとか、n,mとかで定義して0まで減らしていく、といったのがほとんど。ならばfixは上限の決まったInt型（ディレイの読み出しインデックスに使うのと同じ型）にしてしまえば、最低限必要なメモリサイズはコンパイル時に決定できる。

ただ、そうするとユーザーからは、「なんだかよくわからんけど再帰する関数の第1引数には上限の決まったIntしか使えんらしい」という不条理感が残る

こっちは筋が悪いかなー
### これら2つではカバーできないケース

再帰の深さによって返したい型が変わるような多相を考えると厳しいかも。

実際、Faustのパターンマッチングでの項書き換えは書き換えを適用するたびに異なる入出力数のノードを返すことができる（だからこそ`take`みたいな関数が定義できるわけだし）

要素数が$2^n$なアダマール積の定義とか

```java
bus(n) = par(i,n,_); // There is si.bus(n) in the \FL s

// hmtx(2) = _,_ <: +,-; // scalar butterfly
hmtx(2) = _,_ <: (bus(2):>_),(_,*(-1):>_) ; // prettier drawing
hmtx(n) = bus(n) <: (bus(n):>bus(n/2)) , // vector butterfly
	((bus(n/2),(bus(n/2):par(i,n/2,*(-1)))) :> bus(n/2)) : (hmtx(n/2) , hmtx(n/2));

process = hmtx(16);
```

この辺は、多段階計算を使ったとしても生成したコードの型を変えるみたいなことは出来ないのでは？

項でインデックスされた型＝依存型な気がするのよな

[[多段階計算#依存型との組み合わせ]]　

どのみち、拡張していくとしたら

1. 現状のmimiumのシンタックスのまま再帰とfeedを混ぜてもコンパイル通せるように頑張る
2. 多段階計算導入
3. 依存型導入？

という順番になると思うので、どのみち一旦Rustでのmimiumコンパイラをシンプルに作りに行けばそれでいいのではないか？後から拡張するということで

[[継時再帰]]の方をどう定義するか&feedの項とどう使い分けるのかの問題はまだ残されているが…

継時再帰は[[Kronos]]のMeta-Sequencerでも使われてたはずだし、きちんと意味論を定義することはできるのかな？