[obsidian] vault backup: 2023-08-28 22:32:09[

content/mimium.md

@@ -17,3 +17,5 @@ https://github.com/mimium-org/mimium
 「ある係数を入れてフィルターを生成する」みたいな、プログラムを生成する部分評価の仕組みが無いのが結構辛かった
 
 マクロを導入するよりは、多段階計算の方が合いそうという雰囲気
+
+[[mimium新内部表現の構想]]

content/mimium新内部表現の構想.md

@@ -0,0 +1,28 @@
+#memo #mimium #programming-language 
+
+[[音楽プログラミング言語の形式化#mimium と 多段階計算]]
+
+[[多段階計算]]を取り入れたい
+
+## 型定義
+
+a個の実数のタプルである$R_a$
+
+n以下の自然数$I_n$ (ディレイのbounded access用)
+
+$$
+\begin{align}
+\tau ::=& R_a \quad & a \in \mathbb{N}\\
+      |& R_a → R_b \quad &a,b \in \mathbb{N}\\
+      |& I_n \quad &n \in \mathbb{N}
+\end{align}
+$$
+とりあえず1要素のタプルと普通のRは区別しないことにする
+
+$$
+\begin{align}
+e,f ::=& \quad x \quad x \in \mathbb{V}\\
+     |& \quad \lambda x.e\\
+     |& \quad f \; e
+\end{align}
+$$

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

@@ -13,7 +13,7 @@
 [[Coqの勉強]]
 
 
-## mimiumと[[多段階計算]]
+## [[mimium]]と[[多段階計算]]
 
 こういうのが計算できなかった(要するにfixpointの中で`self`を使うと必要な`self`のサイズを確定できない)