1

方案编程语言说

Scheme 允许使用过程捕获任何表达式的延续call/cc。call/cc 必须传递p一个参数的过程。call/cc构造当前延续的具体表示并将其传递给p. 延续本身由过程表示k。每次k应用于一个值时，它都会将该值返回给call/cc应用程序的延续。从本质上讲，这个价值变成了应用的价值call/cc。如果p不调用k就返回，则过程返回的值成为应用程序的值 call/cc。

p就被调用而言，是否有以下两种定义等价的方式call/cc：

  • p不调用就返回k，
  • p 调用k它的其他返回值？

我不确定如何call/cc定义。除了通过调用间接调用外，是否call/cc曾直接调用延续？kpk

两者都call/cc和p不调用 continuation 完全没问题k吗？

4

2 回答 2

1

是的，(call/cc (lambda (k) 1)) <=> (call/cc (lambda (k) (k 1)))。您可以通过使用延续传递样式转换来证明这一点。

关键部分是 is 的 CPScall/cc形式(lambda (k) (lambda (f) ((f k) k)))。并且这两个函数的 CPS 形式是(lambda (c) (lambda (k) (c 1)))和(lambda (c) (lambda (k) (k 1)))。代入和简化，都得到(lambda (k) (k 1)).

我非常喜欢带分隔符的延续，因为它们有：

(reset (1 + (shift (lambda (f) f)))) <=> (lambda (v) (+ 1 v))

这也可以代数证明。

于 2019-08-10T05:02:52.227 回答
1

要解决后续问题的详细信息，我们可以使用来自http://matt.might.net/articles/cps-conversion/的代码 scheme-cps-convert.rkt

> (T-c '(call/cc (λ (k) 1)) 'halt)
'((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2873) ($k2873 1)) halt)
> (T-c '(call/cc (λ (k) (k 1))) 'halt)
'((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2940) (k 1 $k2940)) halt)

减少第一个表达式：

  ((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2873) ($k2873 1)) halt)
= ((λ (k $k2873) ($k2873 1)) (λ (x _) (halt x)) halt)
= (halt 1)

第二个

  ((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2940) (k 1 $k2940)) halt)
= ((λ (k $k2940) (k 1 $k2940)) (λ (x _) (halt x)) halt)
= ((λ (x _) (halt x)) 1 halt)
= (halt 1)

证明它们是相等的，因此在该位置使用 k 或不使用 k 没有区别。

于 2019-08-11T17:39:44.553 回答