【问题标题】:Examples of the difference between `prompt/control` and `shift/reset``prompt/control` 和 `shift/reset` 的区别示例
【发布时间】:2021-02-17 15:00:49
【问题描述】:

我不确定我是否理解分隔延续运算符对 prompt/controlreset/shift 之间的区别。我了解一些基本的使用示例,但在这些示例中,它们的行为是相同的。

我在 Dariusz Biernacki 和 Olivier Danvy 的“On the Dynamic Extent of Delimited Continuations”中找到了这个例子:

reset
  (fn () => shift (fn k => 10 + (k 100))
          + shift (fn k’ => 1))

prompt 
  (fn () => control (fn k => 10 + (k 100))
          + control (fn k’ => 1))

我已将其翻译成 Scheme,并使用 racket/control 库在 Racket 中成功运行并获得预期结果:

(reset  (+ (shift   k  (+ 10 (k 100)))
           (shift   kk 1))) 
   ;; ==> 11

(prompt (+ (control k  (+ 10 (k 100)))
           (control kk 1))) 
   ;; ==> 1

他们的解释是,

在第一种情况下,当应用k 时,表达式shift (fn kk => 1) 在功能上可以表示为fn v => 100 + v 的上下文中进行评估,并且在元上下文中可以 表示为(fn v => 10 + v) :: nil;捕获此上下文 并丢弃,中间答案是1;这个中间 答案从元上下文插入到顶部上下文中,即 fn v => 10 + v 应用于1;下一个中间答案是 11;这是最终的答案,因为元上下文是空的。

在第二种情况下,当应用k时,表达式控件 (fn kk => 1) 在由组合产生的上下文中进行评估 fn v => 10 + vfn v => 100 + v(因此可能是 在功能上表示为fn v => 10 + (100 + v)),并在 为空的元上下文;此上下文被捕获并丢弃 中间答案是1;这是最终的答案 因为元上下文是空的。

我被他们定义为“元上下文”的想法弄糊涂了

直观地说,评估上下文表示计算的其余部分,直到
最近的封闭分隔符,元上下文表示所有剩余的计算。

我没有在这里得到“所有剩余计算”的想法,我不确定 为什么在第一个示例中是(fn v => 10 + v) :: nil(为什么是那段代码?)

我想知道是否有更多的例子,可能有更多的细节,关于 这两对运算符之间的差异,可能没有过多使用形式语义, 这真是令人难以置信。

编辑:我还看到两个shift-环绕表达式的顺序确实有所不同:如果我交换它们,那么controlcontrol 的结果都是1 reset.

【问题讨论】:

    标签: scheme ml delimited-continuations


    【解决方案1】:

    首先,让我们回顾一下prompt/controlreset/shift的归约规则。

    (prompt val) => val
    (prompt E[control k expr]) => (prompt ((λk. expr) (λv. E[v])))
    ; E is free from prompt
    
    (reset val) => val
    (reset E[shift k expr]) => (reset ((λk. expr) (λv. (reset E[v]))))
    ; E is free from reset
    

    我们可以看到resetprompt 是一样的。但是,第二条规则略有不同。 reset/shift 对在 E[v] 周围引入了一个重置​​,这限制了 shiftE[v] 中可以捕获的范围

    现在让我们逐步减少这两个表达式。

    首先,shift/reduce

    (reset (+ (shift k (+ 10 (k 100))) (shift kk 1)))
    => (reset ((λk. (+ 10 (k 100))) (λv. (reset (+ v (shift kk 1))))))
    ; Here, E[v] = (+ v (shift kk 1))
    => (reset ((λk. (+ 10 (k 100))) (λv. (reset ((λkk. 1) (λw. (+ v w)))))))
    ; Here, E'[w] = (+ v w)
    ; Because of the reset, `E'[w]` catches only `(+ v w)`
    ; which gets discarded right away.
    => (reset ((λk. (+ 10 (k 100))) (λv. (reset 1))))
    => (reset ((λk. (+ 10 (k 100))) (λv. 1)))
    => (reset (+ 10 ((λv. 1) 100)))
    => (reset (+ 10 1))
    => (reset 11)
    => 11
    

    其次,prompt/control

    (prompt  (+ (control k (+ 10 (k 100))) (control kk 1)))
    => (prompt ((λk. (+ 10 (k 100))) (λv. (+ v (control kk 1)))))
    ; Here, E[v] = (+ v (control kk 1))
    => (prompt ((λkk. 1) (λw. ((λk. (+ 10 (k 100))) (λv. (+ v w))))))
    ; Here, E'[w] = ((λk. (+ 10 (k 100))) (λv. (+ v w)))
    ; Because there is no `prompt` the scope of `E'[w]` is much larger and
    ; everything in it get discarded right away
    => (prompt 1)
    => 1
    

    总之,只有在至少有 2 个 control/shift 运算符和 shift 减少了上下文 E' 可以捕获的范围时才会有区别。

    【讨论】:

      猜你喜欢
      • 1970-01-01
      • 2018-12-09
      • 1970-01-01
      • 2019-03-11
      • 2021-07-04
      • 2015-08-26
      • 2018-10-07
      • 1970-01-01
      • 1970-01-01
      相关资源
      最近更新 更多