[obsidian] vault backup: 2024-11-24 19:25:41[

content/lambda-mmm(実用版).md

@@ -0,0 +1,84 @@
+---
+date: 2024-11-23 08:05
+---
+
+#mimium 
+
+元々のLambda-mmmは実際に使われているmimiumでの中間表現と比べて以下のような差がある
+
+- タプルなど構造化された型がない（実際にはVMの命令にワードサイズの情報を付加しているのでこれは結構重要）
+- letで宣言された変数に対しては代入ができる（部分的に参照型が使われている）
+- delayやfeedの項を終端の値として扱う意味論（コンパイル時の正規化作業）と、実際の評価に使われる意味論が混ざっている
+
+## 型
+
+$$
+\begin{align}
+\tau ::=
+		& \quad unit &\\
+	  |&\quad R \quad &\\
+      |&\quad I_n \quad &n \in \mathbb{N} \\
+      |& \quad \tau * \tau \quad &\\
+      |&\quad \tau → \tau &\\
+      % |&\quad \langle \tau \rangle
+\end{align}
+$$
+
+## 値
+
+$$
+\begin{align}
+v ::=
+	  &\quad unit & \\
+	  |&\quad R & R \in \mathbb{R} \\
+      |&\quad v * v \quad &\\
+      |&\quad \lambda x.e \\
+      |&\quad delay(e,e_{time},v_{bound})\\
+      |&\quad feed\ x.e
+\end{align}
+$$
+## 項
+
+$$
+\begin{align}
+e_p ::=
+	  &\quad unit & \\
+	  |&\quad R & R \in \mathbb{R} \\
+
+e ::=
+	  &\quad e_p & \\
+	  |&\quad e,e & [tuple]\\ 
+      |&\quad x\quad &[var]\\
+      |&\quad \lambda x.e &[abs]\\
+	 .|&\quad let\; x\; =\; e\; in\; e &[let]\\
+      |&\quad e\; e &[app]\\
+      |&\quad delay(e,e_{time},e_{bound}) &[delay]\\
+      |&\quad feed\; x.e &[feed]
+\end{align}
+$$
+
+## 評価環境（正規化時）
+
+$$
+\begin{align}
+E ::= &\; ()\\
+    &|\; E :: (x,v)
+\end{align}
+$$
+
+## 正規化の操作的意味論
+
+$$
+\begin{gathered}
+	&\frac{E \vdash e_{bound} \Downarrow v_{bound} }
+			{E \vdash delay\; e\;e_{time}\; e_{bound} \Downarrow delay\; e \; e_{time}\; v_{bound} } &\textrm{[E-DELAY]} \\\\
+
+&\frac{}{E^n \vdash\ \lambda x.e \Downarrow cls(\lambda x.e , E^n) }\ &\textrm{[E-LAM]} \\
+
+&\frac{ E^{n-1} \vdash e \Downarrow v_1\ E^n, x \mapsto v_1 \vdash e \Downarrow v_2 }{E^n, x \mapsto v_2\ \vdash\ feed\ x\ e \Downarrow v_1}\ &\textrm{[E-FEED]} \\
+
+&\frac{E^n \vdash e_c \Downarrow n \quad n > 0\ E^n \vdash e_t\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }\ &\textrm{[E-IFTRUE]}\\
+&\frac{E^n \vdash e_c \Downarrow n \quad n \leqq0\ E^n \vdash e_e\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }\ &\textrm{[E-IFFALSE]}\\
+&\frac{E^n \vdash e_1 \Downarrow cls(\lambda x_c.e_c, E^n_c) E^n \vdash e_2 \Downarrow v_2\ E^n_c,\ x_c \mapsto v_2 \vdash e_c \Downarrow v }{E^n \vdash\ e_1\ e_2 \Downarrow v }\ &\textrm{[E-APP]}
+\end{gathered}
+$$

content/mimiumグローバル環境評価について.md

@@ -12,6 +12,21 @@ date: 2024-07-23 14:42
 
 importとか考え出したらグローバル環境は特別あつかいした方が良さそうだけど、現状では別にいいのか？
 
+---
+
+## 「弱い正規化」を導入しよう
+
+
+IFCで発表した操作的意味論では、delayやfeedのステップごとに実行までを定義した。
+
+しかし、delayとfeedをそれ以上簡約しない値だと捉えると、ラムダを全部評価すれば正規系として[[Faust]]のSignal APIに変換できる形になる。
+
+また、それに加えて入出力で関数をパラメーターに取ったり返却するものだけをあらかじめ簡約すれば、それを命令型に変換した時に可読性をキープすることもできる（Cコードにするとか）
+
+VMでクロージャを評価した結果が関数（クロージャのインスタンス）だった場合、それをラムダに戻すことは可能か？ upvalueで名前の情報失ってるから無理か
+
+
+
 
 
 

content/private

@@ -1 +1 @@
-Subproject commit 915e83a7ee9d1e2e6faffc66695914487d86595f
+Subproject commit 17814c87f8cd2c87df53adf9d6702973f592c1e9