63 lines
1.3 KiB
Markdown
63 lines
1.3 KiB
Markdown
#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>)-> floÏat{
|
|
~(gen_filterbank(N,lowestfreq,margin,filter))(input)
|
|
}
|
|
```
|
|
|
|
filter同士の足し算を`+`の`infix`でやりたいよねえ
|
|
let多相じゃないよなあこれは
|
|
|