quartz-research-note/content/音楽プログラミング言語の形式化.md
Matsuura Tomoya(Windows) 94ce72ba47
All checks were successful
Build / build (push) Successful in 4m2s
[obsidian] vault backup: 2024-11-16 23:44:13[
2024-11-16 23:44:13 +09:00

225 lines
9.0 KiB
Markdown
Raw Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

---
date: "2023-09-20T01:33:51+0900"
---
#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);
```
この辺は、多段階計算を使ったとしても生成したコードの型を変えるみたいなことは出来ないのでは?
```rust
fn hmtx(n:int)-> <[float;n]->[float;n]>{
assert!(n>=2 && n%2 == 0);
if(n==2){
`|list|{
let l = list[0];
let r = list[1];
[l+r, l-r]
}
}else{
`|list:[float]|{
let mixer = interleave
|> |(l1,l2)| {zipwith(l1,l2).map(|(a,b)| a + b)}
|> ~hmtx(n/2);
let upper = list |> mixer;
let lower = list
|> split(_,2)
|>|(l1,l2)| {(l1,l2.map(|a| -a))}
|> mixer;
join(upper,lower)
}
}
}
```
項でインデックスされた型=依存型な気がするのよな
[[多段階計算#依存型との組み合わせ]] 
どのみち、拡張していくとしたら
1. 現状のmimiumのシンタックスのまま再帰とfeedを混ぜてもコンパイル通せるように頑張る
2. 多段階計算導入
3. 依存型導入?
という順番になると思うので、どのみち一旦Rustでのmimiumコンパイラをシンプルに作りに行けばそれでいいのではないか後から拡張するということで
[[継時再帰]]の方をどう定義するか&feedの項とどう使い分けるのかの問題はまだ残されているが…
継時再帰は[[Kronos]]のMeta-Sequencerでも使われてたはずだし、きちんと意味論を定義することはできるのかな
---
VMのインストラクションを考えてるけど。
ワンパスのコンパイラだと、関数呼び出しした時に値がFeedになるかどうかは、Substituteを直接的にするわけじゃないから判別できないのか
となると、やっぱり値に対して性質が決まってるから型として判別した方がいいんじゃないのかつまりfilterの値の方に関してはメモリサイズが不定だよなあ
```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
}
}
```
---
プリミティブとしてはlistとarrayの2種類を持っておき、型強制で`<List 'a>`を`Array 'a` として使えるようにする