From bd66a03213df8a2ddfbcae121d90c03dfe89541b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?=
 =?UTF-8?q?a?= <me@matsuuratomoya.com>
Date: Thu, 24 Oct 2024 14:48:56 +0900
Subject: [PATCH] [obsidian] vault backup: 2024-10-24 14:48:56[

---
 ...miumのMIRコンパイル過程を真面目に考える.md | 29 +++++++++++++++++--
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/content/mimiumのMIRコンパイル過程を真面目に考える.md b/content/mimiumのMIRコンパイル過程を真面目に考える.md
index 44b540e0..6230efd7 100644
--- a/content/mimiumのMIRコンパイル過程を真面目に考える.md
+++ b/content/mimiumのMIRコンパイル過程を真面目に考える.md
@@ -9,6 +9,7 @@ Stateのこととupvalueを両方処理しなくてはならない
 
 StateSize計算とUpvalue計算の両方をtraitとして切り出す方がいいのかな
 
+
 ## 値
 
 $$
@@ -22,14 +23,36 @@ $$
 \begin{align}
 e \; ::=& \quad x \quad x \in \mathbb{V} \quad & [value]\\
      |& \quad \lambda x.e  \quad & [lambda]\\
-     |& \quad e \; e \quad & [app（globstate]\\
+     |& \quad e \; e \quad & [app（global,stateful)]\\
 	 |& \quad appcls \; e \; e \quad & [appclosure]\\
 	 |& \quad fix \; x.e  \quad & [fixpoint]\\
-     |& \quad feed \; x.e \quad & [feed] \\
+     |& \quad getstate \; e \; I_n \; I_s \quad & [feed] \\
 |& \quad delay \; e \; e & [delay]\\
 \end{align}
 $$
 
 結局[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms|W計算]]のStaged Interpreterと変わらんかもな
 
-そうすると型付けの時点でクロージャ相当の項とグローバル関数適用の項は分かれることになる
\ No newline at end of file
+そうすると型付けの時点でクロージャ相当の項とグローバル関数適用の項は分かれることになる?エフェクトとして考えるのが妥当なのかな
+
+## 型
+
+$$
+\begin{align}
+\tau ::=&\quad R_a \quad & a \in \mathbb{N}\\
+      |&\quad I_n \quad &n \in \mathbb{N} \\\
+      |&\quad \tau → \tau \quad \\
+      % |&\quad \langle \tau \rangle
+\end{align}
+$$
+
+## コンパイル
+
+```ocaml
+let compiler = fun e -> match e with
+  Id(x) -> 
+  | App(e1,e2)->
+  | Feed(x,e) -> 
+
+
+```
\ No newline at end of file