"提示/控制"和"移位/重置"之间的区别示例

Question

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

我在"；关于定界连续的动态范围"；，Dariusz Biernacki和Olivier Danvy:

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的上下文中以及在可以表示为表示为CCD_ 7；该上下文被捕获并丢弃，中间答案为CCD_ 8；这个中间体答案从元上下文插入顶部上下文。，将CCD_ 9应用于CCD_；下一个中间答案是11；并且这是最终的答案，因为元上下文是空的。

在第二种情况下，当应用k时，表达式控件(fn kk => 1)是在合成的上下文中评估的CCD_ 14和CCD_在功能上表示为fn v => 10 + (100 + v)(空的元上下文；该上下文被捕获并丢弃中间答案为CCD_ 17；这是最后的答案因为元上下文是空的。

我被"；元上下文"；他们将其定义为

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

我没有想到"所有剩余的计算"；给，我不确定为什么在第一个例子中是(fn v => 10 + v) :: nil(为什么是那段代码？(

我想知道是否还有更多的例子，可能有更多的细节这两对运算符之间的差异可能没有过多地使用形式语义，这真是太夸张了。

edit:我还看到两个shift包围的表达式的顺序确实有区别：如果我交换它们，那么control和reset的结果都是1。

Answer 1

首先，让我们回顾一下prompt/control和reset/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

我们可以看到reset和prompt是相同的。然而，第二条规则有着微妙的不同。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 (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'可以捕获的内容的范围时，才有区别。