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

63 lines
1.2 KiB
Markdown
Raw Normal View History

#programming-language #research
## 先行例
[[Faust]]
[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms]]
## 基礎知識
[[Coqの勉強]]
## mimiumと多段階計算
こういうのが計算できなかった
```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> {
// 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{
~(gen_filterbank(N,lowestfreq,margin,filter))(input)
}
```
filter同士の足し算を`+`の`infix`でやりたいよねえ
let多相じゃないよなあこれは