From f89ee4fd3e8ed8e8542833e46808b90a1f7144a8 Mon Sep 17 00:00:00 2001 From: "Tomoya Matsuura(MacBookPro)" Date: Mon, 28 Aug 2023 23:19:07 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-08-28 23:19:07 --- content/mimium新内部表現の構想.md | 58 +++++++++++++++++++++++++++---- 1 file changed, 51 insertions(+), 7 deletions(-) diff --git a/content/mimium新内部表現の構想.md b/content/mimium新内部表現の構想.md index 3e02b277..5537cc2d 100644 --- a/content/mimium新内部表現の構想.md +++ b/content/mimium新内部表現の構想.md @@ -4,25 +4,69 @@ [[多段階計算]]を取り入れたい +とりあえず$W$ Calculusを自然に多段階に拡張してみる ## 型定義 + + a個の実数のタプルである$R_a$ n以下の自然数$I_n$ (ディレイのbounded access用) $$ \begin{align} -\tau ::=& R_a \quad & a \in \mathbb{N}\\ - |& R_a → R_b \quad &a,b \in \mathbb{N}\\ - |& I_n \quad &n \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 \langle \tau \rangle \end{align} $$ とりあえず1要素のタプルと普通のRは区別しないことにする +(そしてよく見るとこれは関数→関数のような高階関数を許してないんだな) +そうか高階関数を考えなければクロージャを考慮する必要もないものな + +## シンタックス $$ \begin{align} -e,f ::=& \quad x \quad x \in \mathbb{V}\\ - |& \quad \lambda x.e\\ - |& \quad f \; e +e,f \; ::=& \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] \end{align} -$$ \ No newline at end of file +$$ + +基本演算(Intrinsic)は直感に任せる + +本来は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} +$$ + +こんな雰囲気で相互再帰させれば、、、いいんか?ダメだな + +ステージの概念さえ導入できれば値レベルで弾けるのかな + +%% +$$ +\frac{\Gamma x = R_a }{\Gamma \vdash x:R} +$$%%