[obsidian] vault backup: 2024-10-24 12:19:39[
This commit is contained in:
parent
ba8b2e7196
commit
7cb6e23b52
@ -8,3 +8,28 @@ date: 2024-10-20 12:02
|
||||
Stateのこととupvalueを両方処理しなくてはならない
|
||||
|
||||
StateSize計算とUpvalue計算の両方をtraitとして切り出す方がいいのかな
|
||||
|
||||
## 値
|
||||
|
||||
$$
|
||||
\begin{align}
|
||||
v \; ::= & \quad R \\
|
||||
| & (\lambda x:\tau.e, [\Gamma, x:e],StateStorage(p,Vec)) \quad & [Closure]\\
|
||||
\end{align}
|
||||
$$
|
||||
|
||||
$$
|
||||
\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 appcls \; e \; e \quad & [appclosure]\\
|
||||
|& \quad fix \; x.e \quad & [fixpoint]\\
|
||||
|& \quad feed \; x.e \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と変わらんかもな
|
||||
|
||||
そうすると型付けの時点でクロージャ相当の項とグローバル関数適用の項は分かれることになる
|
Loading…
Reference in New Issue
Block a user