[obsidian] vault backup: 2023-08-28 02:22:00[
This commit is contained in:
@ -13,12 +13,11 @@
|
||||
[[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)
|
||||
@ -27,15 +26,13 @@ fn filterbank(N,input,lowestfreq, margin,Q,filter){
|
||||
return 0
|
||||
}
|
||||
}
|
||||
|
||||
```
|
||||
|
||||
仮に多段階計算だとしてちょっと型を明示してみる
|
||||
まあ〜書きづらいよな
|
||||
|
||||
```rust
|
||||
|
||||
fn gen_filterbank(N:int,lowestfreq:float, margin:float,Q:float,filter:float->float)-> <float->float> {
|
||||
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
|
||||
@ -52,7 +49,7 @@ fn gen_filterbank(N:int,lowestfreq:float, margin:float,Q:float,filter:float->flo
|
||||
}
|
||||
}
|
||||
|
||||
fn filterbank(input:float, N:int,lowestfreq:float, margin:float,Q:float,filter:float->float)-> float{
|
||||
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)
|
||||
}
|
||||
```
|
||||
@ -60,3 +57,47 @@ fn filterbank(input:float, N:int,lowestfreq:float, margin:float,Q:float,filter:f
|
||||
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要素のタプルとして見える
|
||||
|
||||
という前から考えていたこととも繋がるのでは?
|
||||
|
||||
|
||||
|
||||
問題はそれをユーザーに意識させずに書かせる方法かあ、結局Faustはそれができているからこそ強いわけで(いや、Faustのパターンマッチは意味論破壊してるからしてるから結局2段階なのか)
|
||||
|
||||
```rust
|
||||
fn lowpass(input,fb){
|
||||
(1-fb)*input + fb*self
|
||||
}
|
||||
```
|
||||
|
||||
|
Reference in New Issue
Block a user