續體

出自Local Chinese Wikipedia
（重新導向自Continuation）
跳至導覽 跳至搜尋

在電腦科學中，續體（英語：continuation，也譯作計算續體、續延、延續性），是實化電腦程式的控制狀態的一種抽象表示。程式在運算過程中給定一個點，其「剩餘將要執行的部分」，即為「續體」。藉助程式語言中的續體特性，程式設計師不但能模組化地自訂迴圈、break陳述句、continue陳述句等基本控制結構；此外還能以更加簡練的方式實現更加複雜的控制結構或計算模式，例如：異常處理、 生成器、協程、回溯、非確定性計算、概率編程[1]、反向傳播演算法、可微分編程等[2]。

概述[編輯]

對一段程式 1 * (2 + 3) - 4 而言，若當前正在計算 2 + 3，這部份則稱為可約表達式（英語：redex; reducible expression）[3]；而其餘的部分 1 * <math>[\cdot]</math> - 4 即是續體。這裡的符號 <math>[\cdot]</math> 被稱為「洞」，表示可約表達式之計算結果將要回填的地方，可視為佔位符。 [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]： 

(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)))

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]。

Scheme語言的1975年最初版本提供了續體算子，即源自Maclisp的用於例外處理的命名catch/throw[27][28]。Steven S. Muchnick（英語：Steven Muchnick）和Uwe F. Pleban在1980年論文《LISP與SCHEME的語意比較》中為Scheme語言介入了基於「續體語意」的指稱語意規定[29][30]。

Daniel P. Friedman、Mitchell Wand（英語：Mitchell Wand）和William Clinger（英語：William Clinger (computer scientist)）基於按照Scheme語言的「續體語意」而編寫的編譯器[31][32]，在1984年為Scheme介入了頭等續體算子call-with-current-continuation（英語：call-with-current-continuation）（簡寫為call/cc）[33][34]，隨後還介入了其約束形式[35]。當前Scheme語言報告中的形式語意描述，沿襲了指稱語意一系著作中所採用的概念和表示法[36][37][38]。

Bruce Duba等人在1991年將頭等續體模組介入到了SML/NJ[39]，CONT簽章具有介面：val callcc : ('a cont -> 'a) -> 'a和val throw : 'a cont -> 'a -> 'b[40]。這裡的'a cont是接受類型參數'a的續體類型，callcc f應用f到當前續體，如果f以實際參數x呼叫這個續體，則如同(callcc f)返回x作為結果。throw k a以實際參數a呼叫續體k；它在本質上將續體強制轉變成為了函式，故而在每次續體呼叫之時重新介入了一個獨立的類型參數'b。

續體傳遞風格[編輯]

主條目：續體傳遞風格

續體的概念主要起源於計算模型研究，比如λ演算[41]、指稱語意[25]和演員模型[42]。這些模型仰仗於編程者或語意工程師書寫數學函式時採用「續體傳遞風格」（continuation-passing style，簡寫為CPS）[43]。續體傳遞風格（CPS）意味著編程中用到的每個函式，都接納並於結束時應用一個表示有關於這個函式呼叫的餘下計算的函式。表達式（英語：Expression (computer science)）的最內部份必須首先求值，將表達式轉換為續體傳遞風格等價者，比如Michael J. Fischer（英語：Michael J. Fischer）在1972年論文《Lambda演算基模》中所舉的例子[41]：將<math display="inline">\;(f\ (g\ (h\ a)))\;</math>變換成<math display="inline">\;(\hat{h}\ (\lambda x\ .\ (\hat{g}\ (\lambda y\ .\ (f\ y))\ x))\ a)\;</math>，具有將表達式「從內至外」翻轉的效果，從而使求值次序以及控制流程變得更加明確。

下面是Standard ML中的高階函式foldr和map的續體傳遞風格實現，和達成一個整數列表的合計函式的簡單用例[44]： 

fun foldr' f b l = let
    fun cf ([], k) = k b
      | cf (a :: r, k) = cf (r, fn x => k (f (a, x)))
    in
        cf (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

所有CPS函式比如這裡的cf，都接受一個額外的實際參數比如這裡的k，它被稱為續體。在CPS函式呼叫中的所有實際參數，必須要麼是一個λ表達式比如這裡fn x => k (f (a, x))，它將續體k應用於函式f的部份應用，要麼是一個變數比如這裡的l和r，而不能是更複雜的表達式。當CPS函式已經計算出來其結果值的時候，它通過以結果值作為實際參數呼叫續體函式來返回它，比如這裡的cf ([], k) = k b，在計算的任何步驟中只要直接返回結果值就會終止整個計算。一個函式比如這裡的foldr'，要呼叫CPS函式比如這裡的cf，就必須提供一個函式比如這裡的fn x => x，用來接受它所呼叫的CPS函式的結果值。

對於輸入[e1, e2, …, en]，這裡的sum函式等價於將函式複合(fn x => x)∘(fn x => e1 + x)∘(fn x => e2 + x)∘…∘(fn x => en + x)，應用於0之上，它得到(e1 + (e2 + (… + (en + 0)…)))。此外，建立在惰性求值和柯里化之上的Haskell提供了函式複合算子。

下面是在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 (factorial n)
  (if (= n 0)
    1
    (* n (factorial (- n 1)))))

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

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

(define (factorial& 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))

對於函數式程式設計者而言，以續體傳遞風格表達代碼使得在直接風格中隱含的一些事物顯露出來：中介值或臨時值都被指定了名字[45]，實際參數求值的次序變為顯見；隨之而來，過程返回變成了對續體的呼叫，而尾呼叫變成將傳遞給這個呼叫者的續體不加修改的傳遞給被呼叫過程。

這裡翻轉條件表達式的方式類似於Smalltalk中遵循邱奇布林值編碼的條件執行控制結構： 

result := a > b
  ifTrue: [ 'greater' ]
  ifFalse: [ 'less or equal' ]

注意在CPS版本的代碼中，使用的函式原語（functional primitive）[46]，比如這裡的*&、+&、-&、=&和sqrt&，自身也是CPS而非直接風格，所以要使得上述例子在Scheme系統中執行，就必須寫出這些函式原語的CPS版本，例如=&定義為： 

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

一般編程在寫CPS函式之時，經常不採用CPS函式原語，比如將前面的階乘函式寫為： 

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

要在REPL或直接風格函式中呼叫CPS函式，必須提供接受CPS函式計算結果的一個續體，比如恆等函式： 

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

採用續體傳遞風格使函數式程式設計者能獲得以任意方式操縱控制流程的表達能力，代價是手工維護控制續體通常是高度複雜的任務。終極解決方案是用Scheme寫一組轉換常式，將Scheme的直接風格表達式（英語：Expression (computer science)）轉換成CPS表達式[47]，下面的例子僅將直接風格函式原語轉換成CPS函式原語： 

(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))

這裡的reverse函式反轉LISP列表所用的單向鏈結串列，其首次應用將原來尾部元素反轉到了首部，接著取出這個元素應用並再次應用reverse函式將餘下諸元素反轉成原來次序。apply（英語：apply）函式的應用(apply f args)，以args列表的諸元素作為實際參數呼叫f函式。

函式eval和通用函式（英語：UTM theorem）apply[48]，是傳統元迴圈求值器的兩大中心構件[49]。Daniel P. Friedman和Mitchell Wand（英語：Mitchell Wand），借鑑了John C. Reynolds（英語：John C. Reynolds）的擴充了續體的直譯器[50]，在1984年論文《續體與協程》中，介入了基於CEK（英語：CEK Machine）（控制、環境和續體）的元迴圈直譯器[51]，並在其著作《程式語言的本質（英語：Essentials of Programming Languages）》中發展出了「續體傳遞直譯器」。

以當前續體呼叫[編輯]

主條目：以當前續體呼叫（英語：call-with-current-continuation）

非形式化描述[編輯]

在Scheme語言中，每當一個Scheme表達式被求值的時候，就會有一個續體想要這個表達式的結果。續體表示了這個計算的全部抑或預設的未來。例如，如果這個表達式被求值於頂層，那麼續體將接受這個結果，將它列印到螢幕上，提示下一次輸入，進行求值，周而復始。多數時候續體包括使用者代碼所指定的動作，比如在接受這個結果的續體中，向它乘以儲存在一個局部變數中的值再加上7，並將答案給予頂層續體來列印它。通常情況下編程者不用過多考慮那些隱藏在幕後的無處不在的續體。

Scheme語言為需要顯式的處理續體的場合，提供了實化控制流程的算子call-with-current-continuation（英語：call-with-current-continuation）（簡寫為call/cc），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]，也可以採用操作語意中小步語意的方式來定義，即使用在上下文<math>\,C\,</math>之下的歸約（英語：Operational_semantics#Reduction_semantics）規則[55][56]：

<math>

\begin{align} C[\operatorname{callcc} (\lambda k.\, e)] &\;\to\; C[(\lambda k.\, e)(\lambda x.\, C[x])] \\ C[\operatorname{throw} (\lambda x.\, k)\, v] &\;\to\; (\lambda x.\, k)\, v \end{align} </math> 這裡的callcc擷取的當前續體是<math>\,\lambda x.\, C[x]\,</math>，其中<math>\,x\,</math>是不被<math>\,C\,</math>所繫結的變數。下面是這種callcc在類似OCaml的假設語言中的用例[57]： 

2 * callcc (fun k -> 1 + (throw k 0));;

使用具有上下文C = 2 * [ ]的callcc規則，對整個程式也就是這個表達式進行歸約： 

⇒ 2 * (fun k -> 1 + (throw k 0)) (fun x -> 2 * x) 	 	 	 	 	 	 	 	 	 
⇒ 2 * (1 + (throw (fun x -> 2 * x) 0))

接著使用具有上下文C = 2 * (1 + [ ])的throw規則，繼續進行歸約： 

⇒ (fun x -> 2 * x) 0 ⇒ 2 * 0 ⇒ 0

Scheme程式語言範例[編輯]

立即返回[編輯]

下面的例子中，使用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)，進而執行(iterator yield)，它將取用遍歷返回值續體繫結到形式參數yield之上；然後開始遍歷列表的元素進行迭代的(for-each (lambda (item) ……) lst)，在求值(set! yield (……))的第二個實際參數之時，進行每一次迭代步驟(call/cc (lambda (resume) ……))，其中的(set! iterator resume)，將繫結到變數resume上的當前續體，重新繫結到函式名字iterator之上用於以後恢復執行，最後執行暫停表達式(yield item)返回當前列表專案。

在下一次執行(generate-digit)之時，(call/cc iterator)將iterator所繫結的續體應用於當前取用遍歷返回值續體之上，從而在上次迭代的(set! yield (call/cc ……))之處恢復執行，這個函式的實際參數求值完畢，它的執行將新傳入的取用遍歷返回值續體繫結到變數yield上，此後繼續這一次的迭代步驟。在遍歷了列表的元素之後迭代結束，最終執行(yield 'stop-iteration)，返回一個約定的文字（英語：Literal (computer programming)）常數。

協程[編輯]

call/cc還可以表達其他複雜的原始運算比如協程[58]。下面的代碼使用續體達成協程即協同運作式多工的使用者級執行緒： 

(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和新澤西Standard ML之外，一些程式語言直接支援頭等續體比如：

參見[編輯]

參照與注釋[編輯]

  1. ↑ https://link.springer.com/chapter/10.1007/978-3-642-03034-5_17
  2. ↑ https://dl.acm.org/doi/10.5555/3327546.3327682
  3. ↑ Klop, J. W. Term Rewriting Systems (PDF). Papers by Nachum Dershowitz and students. Tel Aviv University: 12. [14 August 2021]. （原始內容存檔 (PDF)於15 August 2021）. 
  4. ↑ Kenichi Asai & Oleg Kiselyov. Introduction to programming with shift and reset. 2011. 
  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] （English）. 
  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） （English）. 
  9. ↑ Chapter 6. Control Structures. Chez Scheme Version 10 User's Guide. Cisco Systems, Inc. 2025-10 [2025-11-16] （English）. 
  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] （English）. 
  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）. Now suppose we define an expression to be serious if there is any possibility that its evaluation might not terminate. Then a sufficient condition for order-of-application independence is that a program should contain no serious operands or declaring expressions. ……
    Nevertheless, there is a method for transforming an arbitrary program into one which meets our apparently restrictive condition. …… 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.     
  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 <math>\mathcal{E}</math>' has functionality:
      <math>\mathcal{E}</math>' : Exp → U → K → A
    so that <math>\mathcal{E}</math>'⟦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
      <math>\mathcal{C}</math>⟦γ⟧(ρ) = θ
    where <math>\mathcal{C}</math> 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 <math>\mathcal{P}</math> for this function to distinguish it from the <math>\mathcal{C}</math> 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 γ
      <math>\mathcal{P}</math>⟦γ⟧(ρ)(θ) = θ∘<math>\mathcal{C}</math>⟦γ⟧(ρ)
    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. <math>\mathcal{C}</math>⟦γ⟧(ρ)) 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 <math>\mathcal{P}</math> thus has the functionality
      <math>\mathcal{P}</math> : [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
      σ1' = θ(σ0).
    If we now want to find the effect of performing the command γ with θ as its continuation, we should use the state transformation θ' = <math>\mathcal{P}</math>⟦γ⟧(ρ)(θ) so that the final state would be:
      σ1' = <math>\mathcal{P}</math>⟦γ⟧(ρ)(θ)(σ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' = <math>\mathcal{P}</math>⟦γ⟧ρθσ0
    (note that we shall always retain the text brackets ⟦ ⟧).     
  26. ↑ 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 <math>\mathcal{C}</math>⟦Γ⟧ρθσ 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].     
  27. ↑ 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)))     
  28. ↑ 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
      <math>\mathcal{E}</math>⟦catch <id> <exp>⟧ = (apply call/cc(abs<id><math>\mathcal{E}</math>⟦<exp>⟧))     
  29. ↑ 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. 
  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
      <math>\mathcal{E}</math>⟦(CATCH id exp)⟧ =
        λρ.λκ.λσ. tie(λ⟨α⟩σ'.
          <math>\mathcal{E}</math>⟦exp⟧(ρ[α/id])κ(update α κ σ'))1σ
    and
      <math>\mathcal{E}</math>⟦(THROW id exp)⟧ =
        λρ.λκ. ρ⟦id⟧ ≠ ? → <math>\mathcal{E}</math>⟦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. ↑ 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. 
  32. ↑ 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.     
  33. ↑ 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. 
  34. ↑ 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. ……
    Table 1 presents our domains and some useful functions on them. ……
      K = Env × [V → C] Continuations ……
      pair, lson, rson — primitives for pairings ……
      send = λκv.rson κv ……
    The other unusual feature of the domains is the treatment of continuations. A continuation consists not only the usual [V → C] (the "sequel") but also an environment, which is intended to keep fluid variables. …… In order to hide the internal structure of these continuations as much as possible, we introduce a number of help functions. We use "send" to supply a value to the sequel inside a continuation. ……
    Tables 3 presents the meanings of the operations on the domains. ……
      call/cc = const(λvκ1.v(λvκ2.send κ1v)κ1) ……
    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".     
  35. ↑ 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.     
  36. ↑ 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.     
  37. ↑ 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.     
  38. ↑ 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]).     
  39. ↑ Bruce Duba, Robert Harper, David MacQueen. Typing first-class continuations in ML (PDF). 1991 [2021-10-11]. （原始內容存檔 (PDF)於2022-01-29）. 
  40. ↑ Standard ML of New Jersey — The CONT signature. 1998. 
  41. ↑ 41.0 41.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.     
  42. ↑ 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. 
  43. ↑ 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. 
  44. ↑ CS312. Continuations. Cornell University. 2006. 
    CS3110. Continuations and CPS Conversion. Cornell University. 2014. 
    Brandon Wu. SML Help — Continuation Passing Style. 2022. 
  45. ↑ 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).     
  46. ↑ 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. 
  47. ↑ 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. 
  48. ↑ 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 <math>apply</math>. There is an S-function <math>apply</math> with the property that if <math>f</math> is an S-expression for an S-function <math>f'</math> and <math>args</math> is a list of arguments of the form <math>(arg_{1}, \cdots , arg_{n})</math>, where <math>arg_{1}, \cdots , arg_{n}</math> are arbitrary S-expressions, then <math>apply[f ; args]</math> and <math>f'[arg_{1}, \cdots , arg_{n}]</math> are defined for the same values of <math>arg_{1}, \cdots , arg_{n}</math>, and are equal when defined. 
  49. ↑ 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）. 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. 
  50. ↑ Matthias Felleisen, Daniel P. Friedman. Control Operators, the SECD-Machine, and the Lambda-Calculus. Department of Computer Science, Indiana University. 1986. 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. 
  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. 「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. ……
    (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. ↑ Andrew W. Appel（英語：Andrew W. Appel）. Compiling with Continuations (PDF). Cambridge University Press. 1992. What follows is a straightforward continuation semantics written in Standard ML. ……
    The first compilers that used continuation-passing style (CPS) as an intermediate language [83, 54] represented the CPS using Scheme [69] notation — in those compilers, a CPS expression was just a Scheme program satisfying certain syntactic properties. In the Standard ML of New Jersey compiler (and in this book) we use a more specialized representation. ……
    After the language-specific optimizations and representation decisions have been made, the program being compiled is converted into continuation-passing style. This is done by a recursive traversal over the source-language abstract syntax tree; in Standard ML of New Jersey, we traverse the lambda-language expression that’s a simplified version of the abstract syntax tree.     
  54. ↑ Olivier Danvy（英語：Olivier Danvy）, Andrzej Filinski. Representing control: A study of the CPS transformation (PDF). Mathematical Structures in Computer Science, Volume 2, Issue 4, pp. 361–391. 1992. The CPS transformation permits a simple definition of generalized escape constructs like Scheme's call/cc. Such operators are often perceived to eliminate the need for explicit CPS programs. However, sometimes then greater generality of "genuine" CPS actually needed to express an algorithm (e.g., to implement backtracking (Mellish and Hardy 1984)). Our investigation of the CPS transform leads naturally to the introduction of two new control operators, shift and rest, which allow the additional power of general CPS to be exploited in direct style programs. 
  55. ↑ Andrew K. Wright, Matthias Felleisen. A syntactic approach to type soundness (PDF). Inf. Comput., 115 (1): 38–94. 1994. A context C is is an expression with one subexpression replaced by a hole, denoted [ ]. The expression C[e] results from placing an expression e in the hole of C; this operation may involve capture of the free variables of e by C. 
  56. ↑ Robert Harper（英語：Robert Harper (computer scientist)）. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press. 2016. A variant of structural dynamics, called contextual dynamics, is sometimes useful. …… The main idea is to isolate instruction steps as a special form of judgment, called instruction transition, and to formalize the process of locating the next instruction using a device called an evaluation context. 
  57. ↑ Xavier Leroy（英語：Xavier Leroy）. Control structures in programming languages From goto to algebraic effects. 2025. 
  58. ↑ 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. 
  59. ↑ cl-cont. [2021-10-11]. （原始內容存檔於2012-03-30）. 
  60. ↑ Factor handbook » The language » Continuations. 
  61. ↑ Control.Monad.Cont. 
  62. ↑ S. B. Wample, R. E. Griswold（英語：Ralph Griswold）. Co-expression in Icon* (PDF). The Computer Journal, Volume 26, Issue 1, Pages 72–78. 1983. 
  63. ↑ kotlin-stdlib/kotlin.coroutines/Continuation. 
  64. ↑ R Documentation — callCC {base} — Call With Current Continuation. 
  65. ↑ class Continuation. 
  66. ↑ GNU Smalltalk Library Reference - Base classes — Continuation. 
  67. ↑ Eggs Unlimited (release branch 5) — F-operator. 

延伸閱讀[編輯]

外部連結[編輯]


取自「https://arolstar52-zhtest.hf.space/index.php?title=续体&oldid=1749348」