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

110 lines
3.9 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters

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.

#programming-language #research
## 先行例
[[Faust]]
[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms]]
## 基礎知識
[[Coqの勉強]]
## [[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のエラーメッセージで入出力の数が合わないとかのエラーはマクロ展開後に発生するので、マクロを多用するほどエラーが読みづらくなる問題があるが、それは多分多段階計算の方が読みやすくなる・・・はず