提示/控制和移位/重置之间的差异示例

问题描述

我不确定我是否理解分隔的连续运算符对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包围的表达式的顺序确实有所不同:如果我将它们交换,则两个表达式的结果都是1 controlreset

解决方法

首先,让我们回忆一下 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] 周围引入了重置,它限制了 shift

内的 E[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 (shift 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 减少了上下文 {{1} }.