From afdbf4cd519a23277fa9bd97dbc2bea9bf0fdab6 Mon Sep 17 00:00:00 2001
From: "Tomoya Matsuura(MacBookPro)" <me@matsuuratomoya.com>
Date: Sat, 26 Aug 2023 18:27:50 +0900
Subject: [PATCH] [obsidian] vault backup: 2023-08-26 18:27:50[

---
 content/多段階計算.md                     |  3 ++
 content/音楽プログラミング言語の形式化.md | 49 +++++++++++++++++++++++
 2 files changed, 52 insertions(+)

diff --git a/content/多段階計算.md b/content/多段階計算.md
index 7e47d704..1972f3b1 100644
--- a/content/多段階計算.md
+++ b/content/多段階計算.md
@@ -12,6 +12,9 @@ http://www.is.ocha.ac.jp/~asai/jpapers/ppl/asai14.pdf
 メタプログラミングのための時相論理に基づく型付 λ 計算 湯瀬 芳洋 五十嵐 淳
 http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/papers/pdf/lambdaCB-PPL05.pdf
 
+筑波大学　論理と計算（2）
+http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf
+
 λ○: nextとprevを導入
 
 [MetaML](https://www.sciencedirect.com/science/article/pii/S0304397500000530) nextとprevに加えてrunを導入
diff --git a/content/音楽プログラミング言語の形式化.md b/content/音楽プログラミング言語の形式化.md
index 531338bc..e4c01893 100644
--- a/content/音楽プログラミング言語の形式化.md
+++ b/content/音楽プログラミング言語の形式化.md
@@ -11,3 +11,52 @@
 ## 基礎知識
 
 [[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多相じゃないよなあこれは
+