From f580d37ee92e5ba5cf71c2cd3fe608bc6a1e2262 Mon Sep 17 00:00:00 2001
From: "Tomoya Matsuura(MacBookPro)" <me@matsuuratomoya.com>
Date: Mon, 28 Aug 2023 22:32:09 +0900
Subject: [PATCH] [obsidian] vault backup: 2023-08-28 22:32:09[

---
 content/mimium.md                         |  2 ++
 content/mimium新内部表現の構想.md         | 28 +++++++++++++++++++++++
 content/音楽プログラミング言語の形式化.md |  2 +-
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 content/mimium新内部表現の構想.md

diff --git a/content/mimium.md b/content/mimium.md
index 020b9efd..8e0fca94 100644
--- a/content/mimium.md
+++ b/content/mimium.md
@@ -17,3 +17,5 @@ https://github.com/mimium-org/mimium
 「ある係数を入れてフィルターを生成する」みたいな、プログラムを生成する部分評価の仕組みが無いのが結構辛かった
 
 マクロを導入するよりは、多段階計算の方が合いそうという雰囲気
+
+[[mimium新内部表現の構想]]
\ No newline at end of file
diff --git a/content/mimium新内部表現の構想.md b/content/mimium新内部表現の構想.md
new file mode 100644
index 00000000..3e02b277
--- /dev/null
+++ b/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}
+$$
\ No newline at end of file
diff --git a/content/音楽プログラミング言語の形式化.md b/content/音楽プログラミング言語の形式化.md
index 6e46600d..9dcdd949 100644
--- a/content/音楽プログラミング言語の形式化.md
+++ b/content/音楽プログラミング言語の形式化.md
@@ -13,7 +13,7 @@
 [[Coqの勉強]]
 
 
-## mimiumと[[多段階計算]]
+## [[mimium]]と[[多段階計算]]
 
 こういうのが計算できなかった(要するにfixpointの中で`self`を使うと必要な`self`のサイズを確定できない)