From cbccaf98186f2509ae1729eebbfbecc5555877e4 Mon Sep 17 00:00:00 2001 From: "Tomoya Matsuura(MacBookPro)" Date: Sat, 9 Sep 2023 00:26:30 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-09-09 00:26:30 --- content/mimium新内部表現の構想.md | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/content/mimium新内部表現の構想.md b/content/mimium新内部表現の構想.md index aad2183e..0f96a5e2 100644 --- a/content/mimium新内部表現の構想.md +++ b/content/mimium新内部表現の構想.md @@ -67,6 +67,21 @@ $$ ## 実例 +```rust +fn cascade_f(order:int,fb,x)->float{ + letrec cascade = if(order>0){ + |x|{ + cascade(N-1)(x) *(1-fb) + self*fb + } + }else{ + |x| x + } + cascade(x) +} +``` + +まあ、ともあれコピーキャプチャのクロージャでも問題ないってことですね + ```rust fn cascade(order:int,fb)->(float->float){ if(order>0){ @@ -203,13 +218,12 @@ feedの項に対する加算とか乗算の計算は簡約がしづらいなあ ただ、例えばFeedの項の中に関数が残っちゃうような可能性もあるため、Feedのhistoryの中にLambdaの項が保存されるような状況が回避できない。 -型付規則の中でfeed x.eのeがプリミティブしか取れないようにすればいいのかね。そうするとValueはCopyトレイトを実装できて、feedの中に実際にはラムダが入ってたとしても、簡約後は必ずValueになっていると +型付規則の中でfeed x.eのeがプリミティブというか、Boxedにならないものしか取れないようにすればいいのかね。そうするとValueはCopyトレイトを実装できて、feedの中に実際にはラムダが入ってたとしても、簡約後は必ずValueになっていると ## 型（改正版） というわけで型の定義再訪 - $$ \begin{align} \tau_p ::=&\quad R_a \quad & a \in \mathbb{N}\\ @@ -224,6 +238,8 @@ $$ $$ \frac{\Gamma, x:\tau^a \vdash e:\tau^b}{\Gamma \vdash \lambda x.e:\tau^a \to \tau^b }\\ - +\\ \frac{\Gamma, x : \tau_p^a \vdash e: \tau_p^a }{\Gamma \vdash feed\ x.e:\tau_p^a} $$ + +タプルとかレコードもできるけど、関数をタプルの要素にしたりはできない（できないでもないけど、「そういう型をとれるタプル」と「そういうのできないタプル」を分けて考える必要がある）、って感じでユーザーにはややこしいですねえ \ No newline at end of file