[obsidian] vault backup: 2023-09-08 21:47:38[

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

@@ -12,38 +12,50 @@ $W$ Calculusとmimiumの形式は似ているが、主に2つの違いがある
 
 問題になるのは後者の方だ。
 
-## 型定義
+## 型
 
 
-a個の実数のタプルである$R_a$
 
 n以下の自然数$I_n$ (ディレイのbounded access用)
 
 $$
 \begin{align}
 \tau ::=&\quad R_a \quad & a \in \mathbb{N}\\
-      |&\quad R_a → R_b \quad &a,b \in \mathbb{N}\\
       |&\quad I_n \quad &n \in \mathbb{N} \\
-      |&\quad \langle \tau \rangle
+      |&\quad \tau → \tau \quad &a,b \in \mathbb{N}\\
+      % |&\quad \langle \tau \rangle
 \end{align}
 $$
 とりあえず1要素のタプルと普通のRは区別しないことにする
 (そしてよく見るとこれは関数→関数のような高階関数を許してないんだな)
 そうか高階関数を考えなければクロージャを考慮する必要もないものな
 
-## シンタックス
+## 値
+
+一旦タプルについては考えないことにしよう
 
 $$
 \begin{align}
-e,f \; ::=& \quad x \quad x \in \mathbb{V} \quad & [value]\\
+v \; ::= & \quad R \\
+	| & \quad \lambda x:T.e  \quad & [lambda]\\
+     |& \quad feed \; x.e \quad & [feed] \\
+\end{align}
+$$
+## 項
+
+項
+
+$$
+\begin{align}
+e \; ::=& \quad x \quad x \in \mathbb{V} \quad & [value]\\
      |& \quad \lambda x.e  \quad & [lambda]\\
      |& \quad fix \; x.e  \quad & [fix]\\
      |& \quad feed \; x.e \quad & [feed] \\
-     |& \quad f \; e \quad & [app]\\
-     |& \quad (e_1,e_2) \quad & [product]\\
-     |& \quad \pi_n e \quad n\in \mathbb{N},\; n>0 \quad & [project]\\
-     |& \quad \langle e \rangle \quad & [code] \\
-     |& \quad \textasciitilde e \quad & [escape]
+     |& \quad e \; e \quad & [app]\\
+     %%|& \quad (e_1,e_2) \quad & [product]\\
+     %%|& \quad \pi_n e \quad n\in \mathbb{N},\; n>0 \quad & [project]\\
+     %%|& \quad \langle e \rangle \quad & [code] \\
+     %%|& \quad \textasciitilde e \quad & [escape]
 \end{align}
 $$
 
@@ -52,30 +64,11 @@ $$
 本来はfixの中でfeedを使ったり、feedの中でfixを使うとエラーだが、結局シンタックスレベルでは排除できないので型でエラーとして弾くことにする…？
 いや値レベルでの切り分けは不可能なので、こうする
 
-$$
-\begin{align}
-e,f \; ::=& \quad x \quad x \in \mathbb{V} \quad & [value]\\
-     |& \quad \lambda x.e  \quad & [lambda]\\
-     |& \quad f \; e \quad & [app]\\
-     |& \quad (e_1,e_2) \quad & [product]\\
-     |& \quad \pi_n e \quad n\in \mathbb{N},\; n>0 \quad & [project]\\
-     |& \quad \langle e \rangle \quad & [code] \\
-     |& \quad \textasciitilde e \quad & [escape] \\
-e_{fix} \; ::=& \quad e\\
-		|&  \quad fix \; x.e_{fix}  \quad & [fix]\\
-e_{feed} \; ::=& \quad e\\
-		|&  \quad feed \; x.e_{feed}  \quad & [feed]\\
-\end{align}
-$$
-
-こんな雰囲気で相互再帰させれば、、、いいんか？ダメだな
-ステージの概念さえ導入できれば値レベルで弾けるのかな
 
 
+## 実例
 
+```rust
+fn 
 
-%%
-$$
-\frac{\Gamma x = R_a }{\Gamma \vdash x:R}
-$$%%
-
+```