tomoyanonymous/quartz-research-note
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Tomoya Matsuura(MacBookPro) 2023-09-08 21:47:38 +09:00
parent e62048276e
commit 71b24eb345
1 changed files with 27 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

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