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

[obsidian] vault backup: 2024-10-24 14:48:56[

Browse Source
This commit is contained in:
松浦 知也 Matsuura Tomoya 2024-10-24 14:48:56 +09:00
parent 7cb6e23b52
commit bd66a03213
1 changed files with 26 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
content/mimiumのMIRコンパイル過程を真面目に考える.md
View File

@ -9,6 +9,7 @@ Stateのこととupvalueを両方処理しなくてはならない
StateSize計算とUpvalue計算の両方をtraitとして切り出す方がいいのかな StateSize計算とUpvalue計算の両方をtraitとして切り出す方がいいのかな
## 値 ## 値
$$ $$
@ -22,14 +23,36 @@ $$
\begin{align} \begin{align}
e \; ::=& \quad x \quad x \in \mathbb{V} \quad & [value]\\ e \; ::=& \quad x \quad x \in \mathbb{V} \quad & [value]\\
|& \quad \lambda x.e \quad & [lambda]\\ |& \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 appcls \; e \; e \quad & [appclosure]\\
|& \quad fix \; x.e \quad & [fixpoint]\\ |& \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]\\ |& \quad delay \; e \; e & [delay]\\
\end{align} \end{align}
$$ $$
結局[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms|W計算]]のStaged Interpreterと変わらんかもな 結局[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms|W計算]]のStaged Interpreterと変わらんかもな
そうすると型付けの時点でクロージャ相当の項とグローバル関数適用の項は分かれることになる そうすると型付けの時点でクロージャ相当の項とグローバル関数適用の項は分かれることになる?エフェクトとして考えるのが妥当なのかな
## 型
$$
\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) ->
```