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

3.9 KiB
Raw Blame History

#programming-language #research

先行例

Faust

The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms

基礎知識

Coqの勉強

mimium多段階計算

こういうのが計算できなかった(要するにfixpointの中でselfを使うと必要なselfのサイズを確定できない)

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
    }
}

仮に多段階計算だとしてちょっと型を明示してみる まあ〜書きづらいよな

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多相じゃないよなあこれは

ていうかこれそもそも普通に高階関数じゃダメなんだろうか?

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のパターンマッチは意味論破壊してHygienicとはいえマクロになってるから結局2段階なのか

fn lowpass(input,fb){
	(1-fb)*input + fb*self
}

Faustとかと比べたときのメリット

マクロ部分の生成段階も含めてCやC++のコードとして生成できるのなら、juceのprepareToPlayのような関数内でのDSPグラフのパラメトリックな変形フィルターの次数を変えるとかが実現できるかもそこまでのことが求められてるかというと微妙な気もするが・・・

というか果たしてそんなことはできるのだろうか

あとは、Faustのエラーメッセージで入出力の数が合わないとかのエラーはマクロ展開後に発生するので、マクロを多用するほどエラーが読みづらくなる問題があるが、それは多分多段階計算の方が読みやすくなる・・・はず