ISWIM

ISWIM
編程範型	函數式, 指令式
設計者	彼得·蘭丁
釋出時間	1966年，60年前
範疇	詞法
受影響於
	ALGOL 60、Lisp
影響語言
	PAL、SASL、ML、NPL、Lucid、Haskell

ISWIM（「If you See What I Mean」的首字母縮寫），是一種抽象的電腦程式語言或程式語言家族，它由彼得·蘭丁設計，主要描述在他1966年於ACM通訊發表的文章《接下來的700種程式語言》之中^[1]。ISWIM是具有函數式核心的指令式編程語言，它構成自加了語法糖的叫做「應用表達式」（AE）的擴充λ演算，從而具有高階函數和詞法範疇變量。ISWIM的操作語意，可以使用Landin的SECD機和傳值呼叫來定義^[2]。

ISWIM增加了強力控制機制即對應J算子（英語：J operator）的程式點算子pp^[3]。沒有進行過直接實現ISWIM的嘗試，但是Arthur Evans的PAL^[4]，和John C. Reynolds（英語：John C. Reynolds）的Gedanken^[5]，取得了Landin的多數概念，這兩者都是動態型別語言。Robin Milner的LCF（英語：Logic for Computable Functions） ML，可視為等價於沒有J算子，而有類型推論的ISWIM。另一條演化路線是去掉指令式特徵如J算子並加以單賦值限制，從而成為純函數式語言並進一步切換為惰性求值，這導致了SASL、NPL、Hope、KRC、Miranda和Haskell。此外從ISWIM還衍生出數據流程編程語言Lucid。

語法

ISWIM在定義結構之時，為了看起來更像數學表示法，放棄了ALGOL的稱為陳述式括號（brackets）的begin……end，轉而採用了越位規則和基於縮排的範疇。ISWIM程式基於了一個單一表達式，它由where子句或let子句、條件表達式和函數定義所限定（英語：Qualification principle）。ISWIM在表示法上的特色，是與CPL一起，最早使用where子句進行局部定義，尤其是let子句（英語：Let expression）適合表達ALGOL 60的巢狀（英語：Nested function）的塊結構而為後繼者語言所承襲。

應用表達式利用三種括號和逗號作為語法糖：採用花括號（braces）包圍算子，採用方括號（brackets）包圍運算元或運算元列表，為了作「同時」或「平行」的定義，而在λ和.之間採用圓括號（parentheses）包圍識別碼列表。列表採用逗號分隔其中的元素。

λ演算中的應用（英語：Function application）項(λx.M)N適用β-歸約(λx.M)N $\to$ M[x:=N]，它在應用表達式中表示為{λx.M}[N]，對應的ISWIM表示為：M where x = N或let x = N; M；應用項(M N)及其關聯的命名抽象項M ≡ λx.L，在應用表達式中要一起表示為{λM.(M N)}[λx.L]，它對應的ISWIM表示為：M(N) where M(x) = L或let M(x) = L; M(N)。

AE

邏輯ISWIM

{λf.f(b+2c)+f(2b-c)}
[λx.x(x+a)]

{λ(f,b,c).f(b+2c)+f(2b-c)}
[λx.x(x+a),
  u/(u+1),
  v/(v+1)]

{λf.f(6)}
[Yλf.λn.if(n=0)(1,nf(n-1))]

{λ(f,g).f(g(a))+g(f(b))}
[Yλ(f,g).
  (λx.F(f,g,x),λx.G(f,g,x))]

{λg.g({λf.f}[λx.ax²+bx+c],
  u/(u+1),
  v/(v+1))}
[λ(f,p,q).f(p+2q,2p-q)]

{λx.xy(x+y)}
[{λy.a²+a√y}
  [a²+b²]]

{λ(a,b,f).
  {λ(g,h).
    {λk.X}
    [λ(u,v).λx.K]}
  [Yλ(g,h).
    (λx.G,λ(y,z).H)]}
[A,B,λ(x,y).F]

f(b+2c)+f(2b-c)
where f(x) = x(x+a)

f(b+2c)+f(2b-c)
where f(x) = x(x+a)
  and b = u/(u+1)
  and c = v/(v+1)

f(6)
where rec f(n) = (n=0)→1; nf(n-1)

f(g(a))+g(f(b))
where rec f(x) = F(f,g,x)
      and g(x) = G(f,g,x)

g(f where f(x) = ax²+bx+c,
  u/(u+1),
  v/(v+1))
where g(f,p,q) = f(p+2q,2p-q)

xy(x+y)
where x = a²+a√y
      where y = a²+b²

X
where k(u,v)(x) = K
where rec g(x) = G
      and h(y,z) = H
where a = A
  and b = B
  and f(x,y) = F

let f(x) = x(x+a)
f(b+2c)+f(2b-c)

let f(x) = x(x+a)
and b = u/(u+1)
and c = v/(v+1)
f(b+2c)+f(2b-c)

let rec f(n) = (n=0)→1; nf(n-1)
f(6)

let rec f(x) = F(f,g,x)
    and g(x) = G(f,g,x)
f(g(a))+g(f(b))

let g(f,p,q) = f(p+2q,2p-q)
g((let f(x) = ax²+bx+c; f),
  u/(u+1),
  v/(v+1))

let x =
    let y = a²+b²; a²+a√y
xy(x+y)

let a = A
and b = B
and f(x,y) = F
let rec g(x) = G
    and h(y,z) = H
let k(u,v)(x) = K
X

應用表達式為遞歸定義而採用了Y不動點組合子。上述應用表達式範例中，為處置下行函數參數（英語：Funarg problem）而採用的{λf.f}對應於I恆等組合子。在處置ALGOL 60時，採用λ().L表示無參數函數thunk（英語：thunk），此外還用到了K常數組合子，和B複合組合子。

在ISWIM論文中首次出現了用來定義結構的代數數據類型定義，這是通過自然語言的either……or……和……and……描述完成的，但明確的表示出了當代函數式程式設計語言比如Standard ML中的「積（英語：Product type）之和」^[6]：

抽象ISWIM

Standard ML

an  $a e x p r e s s i o n$  ( $a e x p$ ) is
  either  $s i m p l e$ , and has
    a  $b o d y$ , which is an  $i d e n t i f i e r$ 
  or a  $c o m b i n a t i o n$ , in which case it has
    a  $r a t o r$ , which is an  $a e x p$ ,
    and a  $r a n d$ , which is an  $a e x p$ ,
  or a  $c o n d i t i o n a l$ , …… ,
  or  $o n e - a r m e d$ , …… ,
  or a  $l i s t i n g$ , …… ,
  or  $b e e t$ , …… .

datatype aexp
  = SIMPLE of body 
  | COMBINATION of rator * rand
  | CONDITIONAL ……
  | ONE_ARMED ……
  | LISTING ……
  | BEET ……
and body = BODY of identifier
and rator = RATOR of aexp
and rand = RAND of aexp

這裏的特有術語beet是對beta可歸約式（beta redex）的簡稱，它代表了L where x = M或let x = M; L，這裏的L稱為主要子句，x = M稱為支援（support）即輔助定義。ISWIM衍生語言比如PAL和LCF（英語：Logic for Computable Functions） ML，一般採用let表達式（英語：Let expression）：let x = M in L $\equiv$ let x = M; L。

在ISWIM論文中，Landin將頂層的ISWIM構造稱為amessage即單個訊息；並範例了兩個命令：特定的需求例如Print a+2b，和定義例如Def x = a+2b。

規則

ISWIM基本的等價規則包括：

(let)規則：let x = M; L $\equiv$ L where x = M。
(D')規則：x = L and y = M and …… and z = N $\equiv$ (x, y, ……, z) = (L, M, ……, N)，此規則對應於反向的元組同一性規則，和Standard ML中的模式匹配。
(I')規則：f(x) = L ≡ f = (g where g(x) = L)，這裏的(g where g(x) = L)是閉包，此規則對應於Standard ML中的fun f x = L ⇔ val f = fn x => L。
- (I')規則還有更一般性的柯里化形式，形如f(a, b, c)(x, y) = L $\equiv$ f(a, b, c) = (g where g(x, y) = L)。
(I)規則：(f where f(x) = L) M $\equiv$ L where x = M，這裏的(f where f(x) = L)是閉包。
(β)規則：L where x = M $\equiv$ [M/x]L $\equiv$ L[x:=M]，此規則對應於λ演算中的β-歸約，即用M來避免擷取（capture-avoiding）的代換（英語：Substitution (logic)）L中出現的所有適合的x。
(β')規則：(x = L) where y = M $\equiv$ x = (L where y = M)，此規則用於巢狀局部定義。
(Y)規則：rec x = L $\equiv$ x = (L where rec x = L)，這裏的rec對應於λ演算中的Y不動點算子。

ISWIM的等價規則受到Haskell Curry的著作《組合子邏輯》的影響^[7]。通過運用(I')、(β')、(D')和(Y)等價規則，ISWIM確使任何定義都能被標準化，即表達為lhs = rhs的繫結形式，等式的兩側（英語：Sides of an equation）分別為：左手側（lhs）的確切的一個約束變量，右手側（rhs）的它所對應的主體（body）。下面以階乘函數的應用（英語：Function application）為例：

設`C = (n=0)→1; nf(n-1)`、`G = (g where g(n) = C)`並且`F = (G where rec f = G)`
	`f(6) where rec f(n) = (n=0)→1; nf(n-1)`			`let rec f(n) = (n=0)→1; nf(n-1) in f(6)`
$\equiv$	`f(6) where rec f(n) = C`	`(I')`	$\equiv$	`let rec f(n) = C in f(6)`
$\equiv$	`f(6) where rec f = (g where g(n) = C)`		$\equiv$	`let rec f = (let g(n) = C in g) in f(6)`
$\equiv$	`f(6) where rec f = G`	`(Y)`	$\equiv$	`let rec f = G in f(6)`
$\equiv$	`f(6) where f = (G where rec f = G)`		$\equiv$	`let f = (let rec f = G in G) in f(6)`
$\equiv$	`f(6) where f = F`	`(β)`	$\equiv$	`let f = F in f(6)`
$\equiv$	`F(6)`		$\equiv$	`F(6)`
$\equiv$	`(G where rec f = G)(6)`	`(Y)`	$\equiv$	`(let rec f = G in G)(6)`
$\equiv$	`(G where f = (G where rec f = G))(6)`		$\equiv$	`(let f = (let rec f = G in G) in G)(6)`
$\equiv$	`(G where f = F)(6)`		$\equiv$	`(let f = F in G)(6)`
$\equiv$	`((g where g(n) = C) where f = F)(6)`		$\equiv$	`(let f = F in (let g(n) = C in g))(6)`
$\equiv$	`((g where g(n) = (n=0)→1; nf(n-1)) where f = F)(6)`	`(β)`	$\equiv$	`(let f = F in (let g(n) = (n=0)→1; nf(n-1) in g))(6)`
$\equiv$	`(g where g(n) = (n=0)→1; nF(n-1))(6)`	`(I)`	$\equiv$	`(let g(n) = (n=0)→1; nF(n-1) in g)(6)`
$\equiv$	`((n=0)→1; nF(n-1)) where n = 6`	`(β)`	$\equiv$	`let n = 6 in ((n=0)→1; nF(n-1))`
$\equiv$	`(6=0)→1; 6(F(5))`		$\equiv$	`(6=0)→1; 6(F(5))`
$=$	`6(F(5))`		$=$	`6(F(5))`
	⋮			⋮
$=$	`6(5(4(3(2(1(F(0)))))))`		$=$	`6(5(4(3(2(1(F(0)))))))`

通過反向運用等價規則，ISWIM可在這個例子中恢復出等式的左手側為rec f(n)形式的表達式：

	`6(F(5))`			`6(F(5))`
$\equiv$	`6(f(5) where f = F)`	`(β)↑`	$\equiv$	`6(let f = F in f(5))`
$\equiv$	`6(f(5) where f = (G where rec f = G))`		$\equiv$	`6(let f = (let rec f = G in G) in f(5))`
$\equiv$	`6(f(5) where rec f = G)`	`(Y)↑`	$\equiv$	`6(let rec f = G in f(5))`
$\equiv$	`6(f(5) where rec f = (g where g(n) = C))`		$\equiv$	`6(let rec f = (let g(n) = C in g) in f(5))`
$\equiv$	`6(f(5) where rec f(n) = C)`	`(I')↑`	$\equiv$	`6(let rec f(n) = C in f(5))`
$\equiv$	`6(f(5) where rec f(n) = (n=0)→1; nf(n-1))`		$\equiv$	`6(let rec f(n) = (n=0)→1; nf(n-1) in f(5))`

語意

應用表達式（AE）的形式語意對應於Gordon Plotkin（英語：Gordon Plotkin）在1975年定義的λ_v演算的形式語意^[2]^[8]。R. D. Tennent在1976年論文《程式語言的指稱語意》中將不加語法糖的應用表達式用於示範^[9]。

基於應用表達式的如下形式語法：

B ∈ Bas     #基础值 
I ∈ Ide     #标识符
E ∈ Exp     #表达式

E ⩴ B
  | I
  | λI.E    #抽象
  | E₁E₂    #组合
  | (E)     #加圆括号

定義如下指稱語意^[10]：

元循環風格

續體傳遞風格

δ ∈ D           (*可指称值*)

ρ ∈ U = Ide → D (*环境*)

ϕ ∈ F = D → E   (*函数*)

ℬ : B → E
ℰ : Exp → U → E
ℰ⟦(E)⟧ρ = ℰ⟦E⟧ρ
ℰ⟦B⟧ρ = ℬ⟦B⟧
ℰ⟦I⟧ρ = ρ⟦I⟧ in E
ℰ⟦λI.E⟧ρ = ϕ in E
where ϕ(δ) = ℰ⟦E⟧(ρ[δ/I]) (*闭包*)
ℰ⟦E₁E₂⟧ρ = ϕ(δ)
where ϕ = ℰ⟦E₁⟧ρ|F
  and δ = ℰ⟦E₂⟧ρ|D

δ ∈ D               (*可指称值*)
A = B + {error}°    (*答案*)
ρ ∈ U = Ide → D     (*环境*)
κ ∈ K = E → A       (*表达式续体*)
ϕ ∈ F = D → K → A   (*函数*)

ℬ : B → E
ℰ : Exp → U → K → A
ℰ⟦(E)⟧ρκ = ℰ⟦E⟧ρκ
ℰ⟦B⟧ρκ = κ(ℬ⟦B⟧)
ℰ⟦I⟧ρκ = κ(ρ⟦I⟧ in E)
ℰ⟦λI.E⟧ρκ = κ(ϕ in E)
where ϕ(δ){κ} = ℰ⟦E⟧(ρ[δ/I]){κ} (*闭包*)
ℰ⟦E₁E₂⟧ρκ = ℰ⟦E₁⟧ρκ₁
where κ₁(ε₁) = ℰ⟦E₂⟧ρκ₂
      where κ₂(ε₂) = (ε₁|F)(ε₂|D){κ}

在BNF範式中，⩴（U+2A74常寫為::=）表示產生（英語：Production (computer science)），|表示交替（英語：Alternation (formal language theory)）。在指稱語意中，in表示內射而入，而|表示投射而出^[11]，二者由Dana Scott和Christopher Strachey在1971年介入^[12]。

具有let表達式（英語：Let expression）的應用式語言（英語：Applicative programming language）很適合用於形式語意示範。R. D. Tennent在1991年著作《程式語言的語意》中採用了新的指稱語意表示法並將PCF（英語：Programming Computable Functions）用於示範^[13]。Matthew Hennessy（英語：Matthew Hennessy）在1990年著作《程式語言的語意：使用結構性操作語意的初步介紹》中將簡單的函數式語言Fpl用於小步操作語意示範^[14]。Gilles Kahn（英語：Gilles Kahn）在1987年論文《自然語意》中將Mini-ML用於大步操作語意示範^[15]。

執行

SECD機是第一個專門設計用來求值應用表達式（AE）的抽象機，SECD四者分別指示堆疊、環境、控制和轉儲。它最初描述於Peter Landin的1964年論文《表達式的機器求值》中^[16]。常見的執行指令序列的SECD虛擬機器，是Peter Henderson於1980年在LispKit Lisp編譯器中定義並實現的。

應用表達式擴充了的賦值器（assigner） $\Leftarrow$ ，其應用形式為lhs $\Leftarrow$ rhs，則稱為指令式應用表達式（IAE）。為了執行擴充了J算子（英語：J operator）的具有賦值器的指令式應用表達式，所細化的SECD機叫做共用機^[10]。

Matthias Felleisen和Daniel P. Friedman在1986年借鑑John C. Reynolds（英語：John C. Reynolds）於1972年提出的擴充了續體的元循環直譯器^[17]，修訂Peter Landin的SECD機，從而規定了CEK機（英語：CEK Machine）^[18]，CEK三者分別指示控制、環境和續體^[8]。他們在1986年又將CEK機擴充為CESK機，增加的S指示儲存^[19]。Matthias Felleisen於1987年論文《超越續體》中在CEK機上定義了算子 $𝒞$ 和 $ℱ$ 的指稱語意^[20]。

SECD機

對應用表達式進行機器求值的SECD機，將狀態變遷規則定義為狀態變換（英語：Transformation (function)）函數Transform(S,E,C,D)：

S	E	C	D	$\to$	S	E	C	D
s	e	combination(rator,rand)::c	d	$\to$	s	e	rand::rator::ap::c	d

S	E	C	D	$\to$	S	E	C	D
s	e	identifier(x)::c	d	$\to$	locate(position(e,x),e)::s	e	c	d
s	e	λexp(v,L)::c	d	$\to$	closure((e,v),[L])::s	e	c	d

S	E	C	D	$\to$	S	E	C	D
closure((e',v),[L])::x::s	e	ap::c	d	$\to$	[]	(v,x)::e'	[L]	(s,e,c,d)
f::x::s	e	ap::c	d	$\to$	f(x)::s	e	c	d
x::s	e	[]	(s',e',c',d')	$\to$	x::s'	e'	c'	d'

這裏的[]是空列表，它在ISWIM中表示為nullist，在應用表達式中表示為()。這裏的::是列表構造的中綴構造子，x::L $\equiv$ cons(x,L) $\equiv$ prefix(x)(L)。

在Landin的規定中，取得識別碼X有關於環境E所指稱的值的函數為：val(E)(X) = location(E*)(X)(E*)，其中的E*指示與環境E對應的名值對的列表，這裏將這個取值函數表示為locate(position(e,x),e)，即定位在環境e中佔據位置position(e,x)的常數x並取得它的原始值。

在Landin的規定中，設v = bv(X)且L = body(X)，從λ表達式X所在的環境E衍生出在其中求值L的新環境的函數為：derive(assoc(v,x))(E)，這裏假定環境E已經實現為特定LISP共用結構即元素為有序對的可永續性單向鏈結串列，從而將這個衍生函數直接用代數數據類型的元組和遞歸數據類型的列表的特定算子來表示。

J算子（英語：J operator）的應用形式f = J(λX.L)稱為「程式點」，它將函數F = λX.L變換成程式閉包。J算子對應的狀態變換函數為：

S	E	C	D	$\to$	S	E	C	D
F::s	e	J::ap::c	d	$\to$	program-closure(F,d)::s	e	c	d

S	E	C	D	$\to$	S	E	C	D
program-closure(F,(s',e',c',d'))::x::s	e	ap::c	d	$\to$	F::x::s'	e'	ap::c'	d'

程式點在ISWIM中表示為pp f(X) = L。

共用機

共用機建模於指令式編程語言ALGOL 60的過程呼叫機制^[21]，這裏預設傳遞給形式參數的是實際參數（英語：Argument of a function）的名字，在這個過程內定義的形式參數的名字，與在這個過程外定義的實際參數的名字，二者之間具有等價關係。歷經可能的多次傳名呼叫得到這些等價的名字，其狀態內位置屬於同一個等價類故而稱為共用，在直接電腦表示中每個等價類對應一個地址。

這裏採用了Christopher Strachey在1963年提出的左值和右值概念^[22]，共用機預設共用一個變量的左值，這裏的左值表示了它所處在的環境和它在這個環境中的位置，傳名呼叫形式參數的狀態內位置儲存傳遞過來的左值。執行指令式應用表達式的抽象機的狀態變換函數為：

C	E	S	D	$\to$	C	E	S	D
combination(rator,rand)::c	e	s	d	$\to$	rand::rator::ap::c	e	s	d
()::identifier(x)::ap::c	e	s	d	$\to$	parameter(x)::c	e	s	d
assigner(lhs,rhs)::c	e	s	d	$\to$	rhs::lhs::assign::c	e	s	d

C	E	共用	S	D	$\to$	C	E	共用	S	D
identifier(x)::c	e		s	d	$\to$	c	e	l=(position(e,x),e)	locate(l)::s	d
parameter(x)::c	e		s	d	$\to$	c	e	l=locate(position(e,x),e)	locate(l)::s	d
assign::c	e	l	r::x::s	d	$\to$	c	e		reset(l,x)::s	d
λexp(v,L)::c	e		s	d	$\to$	c	e		closure((e,v),[L])::s	d

C	E	共用	S	D	$\to$	C	E	共用	S	D
ap::c	e	l	closure((e',v),[L])::r::s	d	$\to$	[L]	(v,l)::e'		[]	(s,e,c)::d
ap::c	e	l	f::r::s	d	$\to$	c	e	x=f(r)	x::s	d
[]	e	l	r::s	(s',e',c')::d	$\to$	c'	e'	l	r::s'	d

賦值器重設其lhs確定的左值所參照的那個右值，並在堆疊S上留下nullist作為結果。Landin規定在這個過程內以無參數函數呼叫的形式，來訪問傳名呼叫形式參數所參照的系統儲存的那個值本身，即處在賦值器rhs的右值，例如通過x()訪問形式參數x。

separate(x)函數共用一個變量所參照的右值，從而避免了後續的賦值變更這個處在外層的非局部（英語：Non-local variable）值。在處置ALGOL 60時它的用途典型為：聲明已經傳遞來的形式參數為傳值呼叫^[23]，例如let x = separate(x()); L；通過回溯傳名呼叫形式參數傳遞，最終能確定其對應的實際參數，是在某個外層過程中聲明即採用separate函數初始化的局部識別碼，比如let x = separate(0.0)。

separate函數對應的狀態變換函數可以定義為：

C	E	共用	S	D	$\to$	C	E	共用	S	D
separate::ap::c	e		r::s	d	$\to$	c	e	r	r::s	d
separate::ap::c	e	l	r::s	d	$\to$	c	e	r	r::s	d

Landin將在SECD機和共用機上執行的Y不動點算子，實現為指令式應用表達示式：Y(F) ≡ {λz.{λz′.2nd(z⇐z′,z)}[F(z)]}[separate(nullist)]，它對應的ISWIM表示為：

Y(F) $\equiv$ let z = separate(nullist); let z' = F(z); 2nd(z $\Leftarrow$ z',z)

Landin為處置ALGOL 60而規定了賦值且保全命令assignandhold，它採用守衛命令處置原始數據類型：

assignandhold(x)(y)  $\equiv$  let x = (real(y)→float(x); integer(y)→entier(x+0.5); Boolean(y)→(Boolean(x)→x)); 2nd(y $\Leftarrow$ x,x)

。

CEK機

在CEK機（英語：CEK Machine）中，環境ρ ∈ E是從變量到語意值的有限對映。下面是CEK機對應於應用表達式的狀態變遷函數：

C	E	K	$\mapsto$	C	E	K
x	ρ	κ	$\mapsto$	""	{}	(ret ρ(x))::κ
λx.M	ρ	κ	$\mapsto$	""	{}	(ret ⟨λx.M,ρ⟩)::κ
M N	ρ	κ	$\mapsto$	M	ρ	(arg N ρ)::κ
""	{}	(ret V)::(arg N ρ)::κ	$\mapsto$	N	ρ	(fun V)::κ
""	{}	(ret V)::(fun ⟨λx.M,ρ⟩)::κ	$\mapsto$	M	ρ[x:=V]	κ

這裏的""表示空字串，而{}表示空集合。這裏的⟨λx.M,ρ⟩是閉包，它屬於語意值。初始狀態是三元組⟨M, {}, [stop]⟩，終止狀態是三元組⟨"", {}, [(ret V), stop]⟩。

CEK機分別定義了擷取當前續體算子 $𝒞$ 和退出算子 $𝒜$ ^[18]，後續論文中簡化了算子 $𝒞$ 的定義。下面是算子 $𝒞$ 和 $𝒜$ 的定義：

C	E	K	$\mapsto$	C	E	K
$𝒞$ M	ρ	κ	$\mapsto$	Mc	ρ[c:=⟨p,κ⟩]	[stop]
$𝒜$ M	ρ	κ	$\mapsto$	M	ρ	[stop]
""	{}	(ret V)::(fun ⟨p,κ₀⟩)::κ	$\mapsto$	""	{}	(ret V)::κ₀

這裏有着c ∉ Dom(ρ)，其中的Dom(ρ)表示ρ的定義域。這裏的⟨p,κ⟩是叫做「續延點」的標籤結構，它屬於語意值。

算子 $𝒜$ 可定義為語法抽象： $𝒜$ M $\equiv$ $𝒞$ (λd.M)，這裏有着d ∉ FV(M)，其中的FV(M)表示M的自由變量。以當前續體呼叫（英語：call-with-current-continuation）算子可定義為：call/cc $\equiv$ λf. $𝒞$ (λk.k(f k))，注意這裏的k(f k)，如果在f之中應用了傳遞給它的k則(f k)不會返回，否則k會應用於(f k)的返回值。反過來說，算子 $𝒞$ 可以用算子call/cc和 $𝒜$ 定義為： $𝒞$ $\equiv$ λf.(call/cc (λk. $𝒜$ (f k)))。

Matthias Felleisen在1992年為算子 $𝒞$ 修訂完善了小步操作語意中的歸約語意^[24]。

CESK機

在CESK機中，環境ρ ∈ E是從變量到表示位置的自然數的有限對映，而儲存θ ∈ S是從自然數到語意值的有限對映。下面是CESK機沿襲自CEK機的狀態變遷函數：

C	E	S	K	$\mapsto$	C	E	S	K
x	ρ	θ	κ	$\mapsto$	""	{}	θ	(ret θ(ρ(x)))::κ
λx.M	ρ	θ	κ	$\mapsto$	""	{}	θ	(ret ⟨λx.M,ρ⟩)::κ
M N	ρ	θ	κ	$\mapsto$	M	ρ	θ	(arg N ρ)::κ
""	{}	θ	(ret V)::(arg N ρ)::κ	$\mapsto$	N	ρ	θ	(fun V)::κ
""	{}	θ	(ret V)::(fun ⟨λx.M,ρ⟩)::κ	$\mapsto$	M	ρ[x:=n]	θ[n:=V]	κ

這裏的θ[n:=V]有着n ∉ Dom(θ)。

CESK機增加了賦值抽象σx.M^[19]：

C	E	S	K	$\mapsto$	C	E	S	K
σx.M	ρ	θ	κ	$\mapsto$	""	{}	θ	(ret ⟨σx.M,ρ⟩)::κ
""	{}	θ	(ret V)::(fun ⟨σx.M,ρ⟩)::κ	$\mapsto$	M	ρ	θ[ρ(x):=V]	κ

Matthias Felleisen在1987年博士論文《λ_v-CS轉換的演算：指令式高階程式語言中控制與狀態的語法理論》中，為求值理想化 Scheme而捨棄了CEK機中的算子 $𝒞$ 和 $𝒜$ ^[25]，轉而向CESK機介入了有界續體（英語：Delimited continuation）的函數抽象算子 $ℱ$ ^[26]：

C	E	S	K	$\mapsto$	C	E	S	K
$ℱ$ M	ρ	θ	κ	$\mapsto$	Mγ	ρ[γ:=n]	θ[n:=⟨p,κ⟩]	[stop]
""	{}	θ	(ret V)::(fun ⟨p,κ₀⟩)::κ	$\mapsto$	""	{}	θ	(ret V)::κ₀@κ

這裏的θ[n:=V]有着n ∉ Dom(θ)，並且ρ[γ:=n]有着γ ∉ FV(M)。這裏的@是串接輔助函數：

[stop]@κ	=	κ
[(arg N ρ),κ']@κ	=	(arg N ρ)::κ'@κ
[(fun V),k']@κ	=	(fun V)::κ'@κ

下面以求值1+( $ℱ$ (λk.k(k0)))作為範例:

	C	E	S	K
	1+( $ℱ$ (λk.k(k0)))	{}	{}	[stop]
$\mapsto$	1+	{}	{}	[(arg $ℱ$ (λk.k(k0)) {}),stop]
$\mapsto$	""	{}	{}	[(ret 1+),(arg $ℱ$ (λk.k(k0)) {}),stop]
$\mapsto$	$ℱ$ (λk.k(k0))	{}	{}	[(fun 1+),stop]
$\mapsto$	(λk.k(k0))γ	{γ $\mapsto$ 1}	{1 $\mapsto$ cl₀}	[stop]
		where cl₀=⟨p,[(fun 1+),stop]⟩
$\mapsto$	λk.k(k0)	{γ $\mapsto$ 1}	{1 $\mapsto$ cl₀}	[(arg γ {γ $\mapsto$ 1}),stop]
$\mapsto$	""	{}	{1 $\mapsto$ cl₀}	[(ret ⟨λk.k(k0),{γ $\mapsto$ 1}⟩),(arg γ {γ $\mapsto$ 1}),stop]
$\mapsto$	γ	{γ $\mapsto$ 1}	{1 $\mapsto$ cl₀}	[(fun ⟨λk.k(k0),{γ $\mapsto$ 1}⟩),stop]
$\mapsto$	""	{}	{1 $\mapsto$ cl₀}	[(ret cl₀),(fun ⟨λk.k(k0),{γ $\mapsto$ 1}⟩),stop]
$\mapsto$	k(k0)	ρ₀	θ₀	[stop]
		where ρ₀={γ $\mapsto$ 1,k $\mapsto$ 2} θ₀={1 $\mapsto$ cl₀,2 $\mapsto$ cl₀}
$\mapsto$	k	ρ₀	θ₀	[(arg k0 ρ₀),stop]
$\mapsto$	""	{}	θ₀	[(ret cl₀),(arg k0 ρ₀),stop]
$\mapsto$	k0	ρ₀	θ₀	[(fun cl₀),stop]
$\mapsto$	k	ρ₀	θ₀	[(arg 0 ρ₀),(fun cl₀),stop]
$\mapsto$	""	{}	θ₀	[(ret cl₀),(arg 0 ρ₀),(fun cl₀),stop]
$\mapsto$	0	ρ₀	θ₀	[(fun cl₀),(fun cl₀),stop]
$\mapsto$	""	{}	θ₀	[(ret 0),(fun ⟨p,[(fun 1+),stop]⟩),(fun cl₀),stop]
$\mapsto$	""	{}	θ₀	(ret 0)::[(fun 1+),stop]@[(fun cl₀),stop]
$\mapsto$	""	{}	θ₀	[(ret 0),(fun 1+),(fun cl₀),stop]
$\mapsto$	1+0	{}	θ₀	[(fun cl₀),stop]
$\mapsto$	""	{}	θ₀	[(ret 1),(fun ⟨p,[(fun 1+),stop]⟩),stop]
$\mapsto$	""	{}	θ₀	(ret 1)::[(fun 1+),stop]@[stop]
$\mapsto$	""	{}	θ₀	[(ret 1),(fun 1+),stop]
$\mapsto$	1+1	{}	θ₀	[stop]
$\mapsto$	""	{}	θ₀	[(ret 2),stop]

下面以求值1+( $ℱ$ (λd.0))作為範例:

	C	E	S	K
	1+( $ℱ$ (λd.k0))	{}	{}	[stop]
$\overset{+}{\mapsto}$	$ℱ$ (λd.0)	{}	{}	[(fun 1+),stop]
$\mapsto$	(λd.0)γ	{γ $\mapsto$ 1}	{1 $\mapsto$ cl₀}	[stop]
		where cl₀=⟨p,[(fun 1+),stop]⟩
$\overset{+}{\mapsto}$	γ	{γ $\mapsto$ 1}	{1 $\mapsto$ cl₀}	[(fun ⟨λd.0,{γ $\mapsto$ 1}⟩),stop]
$\overset{+}{\mapsto}$	0	ρ₀	θ₀	[stop]
		where ρ₀={γ $\mapsto$ 1,d $\mapsto$ 2} θ₀={1 $\mapsto$ cl₀,2 $\mapsto$ cl₀}
$\mapsto$	""	{}	θ₀	[(ret 0),stop]

在CEK機和CESK機上，算子 $ℱ$ 和算子 $#$ 定義有小步操作語意中的歸約語意^[27]。算子 $𝒜$ 可定義為語法抽象： $𝒜$ M $\equiv$ $ℱ$ (λd.M)，這裏有着d ∉ FV(M)。算子 $𝒞$ 可定義為語法抽象： $𝒞$ M $\equiv$ $ℱ$ (λk.M(λv. $ℱ$ (λd.kv)))。以當前續體呼叫（英語：call-with-current-continuation）算子可定義為：call/cc $\equiv$ λf. $ℱ$ (λk.k(f(λv. $ℱ$ (λd.kv))))。

參照

^ Landin, P. J. The Next 700 Programming Languages (PDF). Communications of the ACM (Association for Computing Machinery). March 1966, 9 (3): 157–165 [2021-08-28]. S2CID 13409665. doi:10.1145/365230.365257. （原始內容 (PDF)存檔於2022-03-23）.
^ ^2.0 ^2.1 Gordon Plotkin（英語：Gordon Plotkin）. Call-by-Name, Call-by Value and the Lambda Calculus (PDF) (報告). 1975 [2020-04-26]. （原始內容存檔 (PDF)於2020-02-01）. As primary example of a λ-calculus based programming language we consider ISWIM [5,7], without the recursion operator or any syntactic sugar. It has an operational semantics which is given by the SECD machine. ……
The notion of value is changed to that induced by the SECD machine, and a normal order reduction sequence theorem is given, which establishes a good correspondence between λ_v and ISWIM. ……
We are going to define ISWIM without letrec, without any syntactic sugar and without any imperative features. Abstract syntax will also ignored. ……
The SECD machine is given by a set, Dumps, of states and and transition function $\Rightarrow$ . ……
Dumps is specified via definition of the sets: Closures, Environments, Controlstrings, and Stacks. ……
The transition function $\Rightarrow$ , in Dumps $\overset{P}{\to}$ Dumps is defined by:
⑴⟨Cl:S,E,nil,⟨S',E',C',D'⟩⟩ $\Rightarrow$ ⟨Cl:S',E',C',D'⟩,
⑵⟨S,E,x:C,D⟩ $\Rightarrow$ ⟨E(x):S,E,C,D⟩,
⑶⟨S,E,a:C,D⟩ $\Rightarrow$ ⟨⟨a,∅⟩:S,E,C,D⟩,
⑷⟨S,E,(λxM):C,D⟩ $\Rightarrow$ ⟨⟨(λxM),E⟩:S,E,C,D⟩,
⑸⟨⟨(λxM),E'⟩:Cl:S,E,ap:C,D⟩ $\Rightarrow$ ⟨nil,E'{Cl/x},M,⟨S,E,C,D⟩⟩,
⑹⟨⟨a,E'⟩:⟨b,E"⟩:S,E,ap:C,D⟩ $\Rightarrow$ ⟨⟨Constapply(a,b),∅⟩:S,E,C,D⟩,
⑺⟨S,E,(MN):C,D⟩ $\Rightarrow$ ⟨S,E,N:M:ap:C,D⟩.
Now Load and Unload are defined by:
  Load(M) = ⟨nil,∅,M,nil⟩
  Unload(⟨Cl,∅,nil,nil⟩) = Real(Cl).
The evaluation function can now be defined by:
  Eval_v(M) = N iff Load(M) $\overset{*}{\Rightarrow}$ D and N = Unload(D) for some dump D.
^ Landin, P.J. A Generalization of Jumps and Labels (PDF). 1965 [2026-03-04]. （原始內容存檔 (PDF)於2025-12-28）.
Thielecke, H. An Introduction to Landin's "A Generalization of Jumps and Labels". Higher-Order and Symbolic Computation. December 1998, 11 (2): 117–123. S2CID 1562780. doi:10.1023/A:1010060315625.
^ Arthur Evans. PAL: a language designed for teaching programming linguistics. Proceedings ACM National Conference. ACM National Conference. Association for Computing Machinery. 1968 [2026-04-07]. （原始內容存檔於2024-10-08）.
^ John C. Reynolds（英語：John C. Reynolds）. GEDANKEN: a simple typeless language which permits functional data structures and co-routines (PDF) (報告). Argonne National Laboratory. September 1969 [2021-09-09]. （原始內容存檔 (PDF)於2021-09-09）.
John C. Reynolds（英語：John C. Reynolds）. GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept. Communications of the ACM, Volume 13, Issue 5, Pages 308 - 319. 01 May 1970. doi:10.1145/362349.362364. 請檢查|date=中的日期值 (幫助)
^ Turner, D. A., Some History of Functional Programming Languages (PDF), Lecture Notes in Computer Science 7829, Berlin, Heidelberg: Springer Berlin Heidelberg: 1–20, 2013 [2024-01-28], ISBN 978-3-642-40446-7, doi:10.1007/978-3-642-40447-4_1, （原始內容存檔 (PDF)於2020-04-15）, The ISWIM paper also has the first appearance of algebraic type definitions used to define structures. This is done in words, but the sum-of-products idea is clearly there.
^ Haskell Curry; Robert Feys（英語：Robert Feys）. Combinatory Logic I. Amsterdam: North Holland. 1958. ISBN 0-7204-2208-6.
^ ^8.0 ^8.1 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 $\overset{β_{v}}{⟶}$ M[x:=N]  (β_v)  provided that N is a value. ……
For the control operations $𝒞$ and $𝒜$ , we need new reduction rules.
Given the expression ( $𝒞$ M)N, we know that M should be applied to a function which simulates the continuation. The expression λf.(fN) almost satisfies the requirement when the application is not nest within other expressions. We need to know the continuation of the entire application in order to sent the result of fN to the rest of the computation. So the reductions are:
  ( $𝒞$ M)N $\overset{𝒞_{L}}{⟶}$ $𝒞$ λκ.M(λf.κ(fN)),  ( $𝒞$ _L)
  M( $𝒞$ N) $\overset{𝒞_{R}}{⟶}$ $𝒞$ λκ.N(λv.κ(Mv))  ( $𝒞$ _R)  provided that M is a value. ……
The $𝒜$ -application must abort all pending computations. …… so we define the following reductions:
  ( $𝒜$ M)N $\overset{𝒜_{L}}{⟶}$ $𝒜$ M,  ( $𝒜$ _L)
  M( $𝒜$ N) $\overset{𝒜_{R}}{⟶}$ $𝒜$ N  ( $𝒜$ _R)  provided that M is a value. ……
Next we have to consider occurrences of $𝒞$ - and $𝒜$ -applications at the root of a term …… but neither of the above rules can evaluate then any further. We need two top-level evaluation rules. ……
The top-level continuation object should, when invoked, stop the evaluation and make its argument the final value of the entire program …… A natural representation for this abort continuation is λx. $𝒜$ x. ……
the top-level relations are needed to reflect the semantics of $𝒞$ and $𝒜$ . …… we define them to be computation rules and indicate this by use $⊳$ in place of $⟶$ :
  ( $𝒞$ M) $⊳_{𝒞}$ M(λx. $𝒜$ x),  ( $𝒞$ _T)
  ( $𝒜$ M) $⊳_{𝒜}$ M.  ( $𝒜$ _T)
Matthias Felleisen, Daniel P. Friedman. Control Operators, the SECD-Machine, and the Lambda-Calculus. Department of Computer Science, Indiana University. 1986. So we expect that the $𝒞$ -reduction rules must be designed according to the position of $𝒞$ M in an sk-context and that they must be similar to $𝒜$ -reductions. For example, the expression ( $𝒞$ M)N must relate to a term $𝒞$ X for some term X. ……
A first approximation of X is hence λκ.M(λf.κ(fN)). ……
This reflects the fact that upon a continuation invocation, the CEK-machine ignores the current continuation. It means for our Λ_c-continuations that the first action must be an abort action to remove the current context, Hence, λf. $𝒜$ (κ(fN)) is the correct continuation for M. The symmetric case where $𝒞$ N is to the right of a value M is treated in a similar way and so we define the two notions of reduction for the $𝒞$ -application by:
  ( $𝒞$ M)N $\overset{𝒞_{L}}{⟶}$ $𝒞$ λκ.M(λf. $𝒜$ (κ(fN)))  ( $𝒞$ _L)
  M( $𝒞$ N) $\overset{𝒞_{R}}{⟶}$ $𝒞$ λκ.N(λv. $𝒜$ (κ(Mv)))  provided that M is a value.  ( $𝒞$ _R)
^ R. D. Tennent. The denotational semantics of programming languages. Communications of the ACM, Volume 19, Issue 8 Pages 437 - 453. 1976. Languages or language subsets having the property of referential transparency are termed applicative; other adjectives that have been used include declarative, denotative, descriptive, and functional. ……
It turns out that identifier-binding constructions may be regarded as being merely more readable representations ("syntactic sugarings") of certain arrangements of abstractions, atomic constituents and operator-operand combinations. ……
These examples have provided evidence for the thesis due to Landin [1964] that applicative languages are "spanned" by the "basis" of atomic constituents, combinations, and abstractions. ……
In words, the meaning of a parenthesization is that of the parenthesized expression; the value of a base is given by applying ℬ to it, independently of the environment, while that of an identifier is obtained by applying the given environment to it; the value of an abstraction is, as before, the function whose result for any argument value is the value of the body relative to an environment that binds the bound variable of the abstraction to the argument value; the value of a combination is obtained by applying the value of the operator part to the value of the operand part.
Note that for the evaluation of an abstraction body, the environment used is the one relative to which the abstraction expression is evaluated (rather than the operator-operand combination that caused the activation); i.e. the scope of identifiers is always statically determined, as in Algol 60. To achieve this form of binding for nonlocal variables in LISP the FUNCTION operator must be used; see Gordon[1973].
^ ^10.0 ^10.1 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].
^ Michael J. C. Gordon（英語：Michael J. C. Gordon）. The denotational description of programming languages - an introduction. Springer-Verlag, Berlin, Heidelberg. 1979. Each member of [D₁ + D₂ + …… + D_n] corresponds to exactly one member of some D_i. …… To make this clear we define
[D₁ + D₂ + …… + D_n] = {(d_i, i)|d_i∈D_i, 0<i<n+1}
so that if d∈D_i and d∈D_j then (d, i) represents d considered as a member of D_i and (d, j) represents d considered as a member of D_j.
If D = [D₁ + D₂ + …… + D_n] and d∈D then isD_i d is true if d corresponds to a member of D_i and false otherwise. If isD_i d = true then outD_i d is the member of D_i corresponding to d. If d_i∈D_i then inD_i d_i is the member of D corresponding to d_i.……
isD_i, outD_i and inD_i can be thought of as functions with types:
isD_i : [D₁ + D₂ + …… + D_n] → Bool
outD_i : [D₁ + D₂ + …… + D_n] → D_i
inD_i : D_i → [D₁ + D₂ + …… + D_n]
^ 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.
^ R. D. Tennent. Semantics Of Programming Languages. Prentice Hall International Series in Computer Science. 1991. The presentation of denotational-semantic methods is unconventional in some other respects. In their pioneering papers, it was convenient for Dana Scott and Christopher Strachey to demonstrate their new techniques on typeless or dynamically-typed languages. Most workers in the field (including this author) went on to use virtually the same techniques on statically-typed languages. But this style of semantics is cumbersome and unrealistic because of the unnecessary type-checking and branching on types that appears in the semantic equations. ……
To give examples, I have chosen to focus attention on a single ALGOL 60-like language and two important fragments of it: the simple imperative language of while programs, and a "sugared" version of the applicative language that Gordon Plotkin termed PCF; i.e., the simply-typed lambda notation augmented by conditionals, recursion, and arithmetic. This approach emphasizes call-by-name, statically-typed, and deterministic languages, but there is also some brief discussion of the semantics of call-by-value, dynamically-typed, and indeterminate languages. Although ALGOL 60-like languages are relatively unfamiliar these days, their semantic elegance, as revealed to us by John Reynolds, is, in my view, compelling.
Tennent, R.D. Denotational semantics. Abramsky, S.; Gabbay, Dov M.; Maibaum, T.S.E. (編). Semantic Structures. Handbook of logic in computer science 3. Oxford University Press. 1994: 169–322. ISBN 978-0-19-853762-5.
^ Matthew Hennessy（英語：Matthew Hennessy）. The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. John Wiley and Sons, New York. 1990. ISBN 0-471-92772-4.
^ Gilles Kahn（英語：Gilles Kahn）. Natural semantics (PDF). 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, FRG. 1987.
^ Landin, P. J. The Mechanical Evaluation of Expressions (PDF). The Computer Journal（英語：The Computer Journal）. January 1964, 6 (4): 308–320 [2022-11-16]. doi:10.1093/comjnl/6.4.308. （原始內容存檔 (PDF)於2022-11-16）.
^ 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 f_old by an f_new such that f_new(a, c) = c(f_old(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.
^ ^18.0 ^18.1 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. ……
The rules (CEK1) through (CEK5) correspond to an evaluator for the λ-value-calculus, e.g., the classical SECD-machine. The rules (CEK6) to (CEK8) define the operations of a $𝒞$ -application: the current continuation is marked, the $𝒞$ -argument is evaluated, and, eventually, the continuation point is passed to the evaluated argument. The last step in this sequence also replaces the current continuation by the initial one. This is where call/cc and $𝒞$ differ: call/cc is equivalent to λf. $𝒞$ λk.k(f k). Rule (CEK9) shows that the invocation of a continuation removes the current continuation, and move the former one in its place. The invocation argument is placed on the stack. According to rule (CEK10), an $𝒜$ -application ignores the continuation and start the evaluation of the $𝒜$ -argument.
^ ^19.0 ^19.1 Matthias Felleisen, Daniel P. Friedman. A Calculus for Assignments in Higher-Order Languages. Indiana University Computer Science Technical Reports; TR202. 1986. In order to avoid this difficulty we have added σ-abstractions to Λ. Their syntax is (σx.M) where x is a variable and M is an expression. A σ-abstraction does not bind the variable, but it abstracts the right to assign a variable a new value. When a σ-abstraction is applied to a value, it assigns x that value and M is evaluated to yield the result of the application. The meaning of the remaining constructs should be adapted accordingly: variables are re-assignable placeholders for values, abstractions correspond to the call-by-value procedures, and applications invoke the result of the function part on the value of the argument part.
^ 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.
^ Heinz Rutishauser（英語：Heinz Rutishauser）. Description of ALGOL 60 (PDF). Springer-Verlag New York Inc. 1967 [2023-07-06]. ISBN 978-3-642-86936-5. doi:10.1007/978-3-642-86934-1. （原始內容存檔 (PDF)於2022-12-22）. A formal parameter of a procedure X does not represent a true quantity as identifiers usually do but is only a designation given to a formal quantity (formal variable, formal array, formal string, formal label, formal switch, formal procedure) which exists only inside the procedure declaration without actually being declared there.
Moreover, a formal parameter has no connection whatsoever with any quantity having the same identifier and existing outside the procedure declaration, and it does not induce any requirements concerning the existence of certain quantities outside the procedure declaration as global parameters do.
The attributive formal has the meaning that such a quantity Q (except if called by value, ……) has no independent existence as a declared quantity has but is only the representative for another quantity A which ultimately will be used as actual operand in place of Q.
^ Barron, D. W.; Buxton, J. N.; Hartley, D. F.; Nixon, E.; Strachey, C. The Main Features of CPL (PDF). The Computer Journal. 1963-08-01, 6 (2): 134–143. ISSN 0010-4620. doi:10.1093/comjnl/6.2.134 （英語）.
Christopher Strachey. Fundamental Concepts in Programming Languages (PDF). Higher-Order and Symbolic Computation 13:11 (2000). August, 1967 [2026-03-28]. （原始內容存檔 (PDF)於2025-06-30）. An L-value represents an area of the store of the computer. We call this a location rather than an address in order to avoid confusion with the normal store-addressing mechanism of the computer. There is no reason why a location should be exactly one machine-word in size — the objects discussed in programming languages may be, like complex or multiple precision numbers, more than one word long, or, like characters, less. Some locations are addressable (in which case their numerical machine address may be a good representation) but some are not. Before we can decide what sort of representation a general, non-addressable location should have, we should consider what properties we require of it.
The two essential features of a location are that it has a content — i.e. an associated R-value — and that it is in general possible to change this content by a suitable updating operation. ……
The characteristic feature of an expression is that it has a value. We have seen that in general in a programming language, an expression may have two values — an L-value and an R-value. 請檢查|date=中的日期值 (幫助)
^ Heinz Rutishauser（英語：Heinz Rutishauser）. Description of ALGOL 60 (PDF). Springer-Verlag New York Inc. 1967 [2023-07-06]. ISBN 978-3-642-86936-5. doi:10.1007/978-3-642-86934-1. （原始內容存檔 (PDF)於2022-12-22）. If a formal operand X is called by value, this has the consequence that it is considered as a true quantity local to the fictitious block as if it were declared there. Then upon a procedure call, not a quantity, but a value (single value or an array of values) is designated as corresponding operand, and this value is assigned to X just prior to the execution ofthe procedure.

^ 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 deﬁnition and future reference to the above rules, we introduce the notion of a singular evaluation context:
$E^{s}$ ⩴ (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). (

C

_T) ……
The disturbing element in the calculus of control abstractions is the rule

C

_T. …… 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 eﬀect. ……
More precisely, when a

𝒞

-application reaches the root of the program after a number of

C

_lift 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,

C

_idem, and

C

_top suffices for simulating a complete evaluation. ……


`fa`	$⟶$	`δ(f,a)`	(δ)
`(λx.e)v`	$⟶$	`e[x←v]`	(βv)
`$E^{s}$ [ $𝒞$ e]`	$⟶$	`$𝒞$ (λk.e(λx. $𝒜$ (k $E^{s}$ [x])))`	( $C$ _lift)
`$𝒞$ e`	$⟶$	`$𝒞$ (λk.e(λx. $𝒜$ (kx)))`	( $C$ _top)
`$𝒞$ (λk.( $𝒞$ e))`	$⟶$	`$𝒞$ (λk.e(λx. $𝒜$ x))`	( $C$ _idem)

Figure 1: The revised syntactic theory of control"

^ Matthias Felleisen. The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (學位論文). Indiana University. 1987 [July 22, 2021]. Originally, the control fragment of the λv-CS-calculus was designed around Scheme's control operation call-with-current-continuation, abbreviated call/cc. As explained in Section 3.2, call/cc applies its argument to the continuation of the entire application. The difference between the continuation and the functional abstraction of the continuation is that the former eliminates the continuation of its invocation. Furthermore, call/cc does not give its argument total control over the continuation since the continuation of the call/cc-application remains the defaults continuation for the evaluation of the call/cc-argument. This leads to rather baroque reductions and computations. Two different sets of relations are required. The first captures the behavior of an abort-application ( $𝒜$ M):
  ( $𝒜$ M) $⊳$ M,
  V( $𝒜$ M) $⟶$ ( $𝒜$ M),
  ( $𝒜$ M)N $⟶$ ( $𝒜$ M);
the second group resembles the $ℱ$ -relations and explains how call/cc provides its argument with an abstraction of its control context:
  (call/cc M) $⊳$ M(λx. $𝒜$ x),
  V(call/cc M) $⟶$ (call/cc λk.V(M(λm. $𝒜$ (k(Vm))))),
  (call/cc M)N $⟶$ (call/cc λk.(M(λm. $𝒜$ (k(mN)))N)).
The $𝒜$ -applications on the right-hand sides are necessary to ensure that all continuation objects immediately eliminate their control contexts upon application.
The second group of reductions contains some regular patterns. The most outstanding is the replication of the call/cc-context, i.e., the term N. If we omit the occurrence that is outside of continuation, we obtain simpler reductions:
  ( $𝒞$ M) $⊳$ M(λx. $𝒜$ x),
  V( $𝒞$ M) $⟶$ ( $𝒞$ λk.(M(λm. $𝒜$ (k(Vm))))),
  ( $𝒞$ M)N $⟶$ ( $𝒞$ λk.(M(λm. $𝒜$ (k(mN))))),
and we can still implement call/cc as a syntactic abstraction:
  (call/cc M) $\equiv$ $𝒞$ (λk.k(Mk)).
Unlike call/cc, $𝒞$ can express $𝒜$ -applications:
  ( $𝒜$ M) $\equiv$ $𝒞$ (λd.M) where d ∉ FV(M).
The inverse relationship is:
  ( $𝒞$ M) $\equiv$ (call/cc (λk. $𝒜$ (Mk))).
Although the introduction of $𝒞$ is an essential improvement for the axiom system, the new reductions and the computation still share a common pattern: the occurrence of the form ( $𝒜$ ……) $\equiv$ $𝒞$ (λd. ……). It is easy to see that an omission of these additional $𝒞$ -applications lead to the $ℱ$ -relations in there current form. Given $ℱ$ 's higher degree of expressiveness and the simplicity of the axioms, $ℱ$ is an improvement for a semantic meta-language like Scheme.
^ Matthias Felleisen. The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (學位論文). Indiana University. 1987 [July 22, 2021]. The term set of Idealized Scheme is Λ_{$ℱ$ σ}, an extension of Λ. …… The language contains two new classes of expressions:
— $ℱ$ -applications: $(ℱ$ M), which are control expressions; M is called the $ℱ$ -argument;
— σ-capabilities: (σx.M), which roughly correspond to assignments; x is the assignable variable, M is the σ-body. ……
The evaluation of an $ℱ$ -application directly corresponds to the informal description of $ℱ$ at outset of the first section. The $ℱ$ -argument is applied to γ, which stands for the current continuation. The current continuation is transferred out of the register into a p-closure and this gives the program total control over its use. In particular the decision about when to use the continuation is left to the program. The operation call/cc in Scheme does not offer the option: it always copies the continuation into a program accessible structure. From the program's perspective this is equivalent to saying that a call/cc-continuation is immediately invoked.
The application of a continuation in Λ_{$ℱ$ σ}-program results in the concatenation of the applied continuation to the current one. This causes the machine to evaluate the applied continuation as if it were a function. If the applied continuation does not affect its continuation during the evaluation, the result is returned to the point of application. In this respect again, CESK-continuations differ from Scheme-continuations. When a program invokes a continuation in Scheme, the interpreter first discards its current continuation and then installs the invoked continuation in the continuation register. Put differently, Scheme-continuation objects have an abortive effect on the continuation of their application point.
Matthias Felleisen, Mitch Wand, Dan Friedman, Bruce Duba. Abstract Continuations: A Mathematical Semantics for Handling Full Functional Jumps. LISP and Functional Programming. 1988. A control-expression transforms the current rest of the computation into a λ-abstraction and binds this abstraction to its variable during the evaluation of the sub-expression:
$C$ [control x M] $\Rightarrow$ M[x:=(λu. $C$ [u])].
Thus, control provides total power over the rest of the computation without introducing another class of objects. If x does not occur free in M, the operation corresponds to an abort; on the other hand, if M immediately invokes x, the default continuation for the rest of M is the current evaluation context. Hence, control is as expressive as abort and escape.
^ 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,
— V $C$ [] 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]) ……
For a reduction simulation of this rule this means that $ℱ$ -applications must encode their context and apply this to their argument. For the top-level computation rule this is rather simple:
   $ℱ$ M $⊳$ _$ℱ$ M(λx.x)
is the required relation. For the other cases, we must consider the two inductive cases of a context definition. Consider the expression ( $ℱ$ M)N and suppose it is embedded in a context $C$ [ ]. Clearly, the function λf.fN is a correct encoding of the immediate context, i.e., $C$ [], can be encoded by another $ℱ$ -application and by building this part of the continuation into the expression λf.fN. Putting these ideas together, the reductions for $ℱ$ -applications should be
  ( $ℱ$ M)N $⟶$ $ℱ$ λk.M(λf.k(fN)),
  U( $ℱ$ M) $⟶$ $ℱ$ λk.M(λv.k(Uv)).
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.

[1] Landin, P. J. The Next 700 Programming Languages (PDF). Communications of the ACM (Association for Computing Machinery). March 1966, 9 (3): 157–165 [2021-08-28]. S2CID 13409665. doi:10.1145/365230.365257. （原始內容 (PDF)存檔於2022-03-23）.

[lambda-v-2] 2.0 ^2.1 Gordon Plotkin（英語：Gordon Plotkin）. Call-by-Name, Call-by Value and the Lambda Calculus (PDF) (報告). 1975 [2020-04-26]. （原始內容存檔 (PDF)於2020-02-01）. As primary example of a λ-calculus based programming language we consider ISWIM [5,7], without the recursion operator or any syntactic sugar. It has an operational semantics which is given by the SECD machine. ……
The notion of value is changed to that induced by the SECD machine, and a normal order reduction sequence theorem is given, which establishes a good correspondence between λ_v and ISWIM. ……
We are going to define ISWIM without letrec, without any syntactic sugar and without any imperative features. Abstract syntax will also ignored. ……
The SECD machine is given by a set, Dumps, of states and and transition function $\Rightarrow$ . ……
Dumps is specified via definition of the sets: Closures, Environments, Controlstrings, and Stacks. ……
The transition function $\Rightarrow$ , in Dumps $\overset{P}{\to}$ Dumps is defined by:
⑴⟨Cl:S,E,nil,⟨S',E',C',D'⟩⟩ $\Rightarrow$ ⟨Cl:S',E',C',D'⟩,
⑵⟨S,E,x:C,D⟩ $\Rightarrow$ ⟨E(x):S,E,C,D⟩,
⑶⟨S,E,a:C,D⟩ $\Rightarrow$ ⟨⟨a,∅⟩:S,E,C,D⟩,
⑷⟨S,E,(λxM):C,D⟩ $\Rightarrow$ ⟨⟨(λxM),E⟩:S,E,C,D⟩,
⑸⟨⟨(λxM),E'⟩:Cl:S,E,ap:C,D⟩ $\Rightarrow$ ⟨nil,E'{Cl/x},M,⟨S,E,C,D⟩⟩,
⑹⟨⟨a,E'⟩:⟨b,E"⟩:S,E,ap:C,D⟩ $\Rightarrow$ ⟨⟨Constapply(a,b),∅⟩:S,E,C,D⟩,
⑺⟨S,E,(MN):C,D⟩ $\Rightarrow$ ⟨S,E,N:M:ap:C,D⟩.
Now Load and Unload are defined by:
Load(M) = ⟨nil,∅,M,nil⟩
Unload(⟨Cl,∅,nil,nil⟩) = Real(Cl).
The evaluation function can now be defined by:
Eval_v(M) = N iff Load(M) $\overset{*}{\Rightarrow}$ D and N = Unload(D) for some dump D.

[3] Landin, P.J. A Generalization of Jumps and Labels (PDF). 1965 [2026-03-04]. （原始內容存檔 (PDF)於2025-12-28）.
Thielecke, H. An Introduction to Landin's "A Generalization of Jumps and Labels". Higher-Order and Symbolic Computation. December 1998, 11 (2): 117–123. S2CID 1562780. doi:10.1023/A:1010060315625.

[4] Arthur Evans. PAL: a language designed for teaching programming linguistics. Proceedings ACM National Conference. ACM National Conference. Association for Computing Machinery. 1968 [2026-04-07]. （原始內容存檔於2024-10-08）.

[5] John C. Reynolds（英語：John C. Reynolds）. GEDANKEN: a simple typeless language which permits functional data structures and co-routines (PDF) (報告). Argonne National Laboratory. September 1969 [2021-09-09]. （原始內容存檔 (PDF)於2021-09-09）.
John C. Reynolds（英語：John C. Reynolds）. GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept. Communications of the ACM, Volume 13, Issue 5, Pages 308 - 319. 01 May 1970. doi:10.1145/362349.362364. 請檢查|date=中的日期值 (幫助)

[6] Turner, D. A., Some History of Functional Programming Languages (PDF), Lecture Notes in Computer Science 7829, Berlin, Heidelberg: Springer Berlin Heidelberg: 1–20, 2013 [2024-01-28], ISBN 978-3-642-40446-7, doi:10.1007/978-3-642-40447-4_1, （原始內容存檔 (PDF)於2020-04-15）, The ISWIM paper also has the first appearance of algebraic type definitions used to define structures. This is done in words, but the sum-of-products idea is clearly there.

[7] Haskell Curry; Robert Feys（英語：Robert Feys）. Combinatory Logic I. Amsterdam: North Holland. 1958. ISBN 0-7204-2208-6.

[cont-sem-8] 8.0 ^8.1 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 $\overset{β_{v}}{⟶}$ M[x:=N] (β_v) provided that N is a value. ……
For the control operations $𝒞$ and $𝒜$ , we need new reduction rules.
Given the expression ( $𝒞$ M)N, we know that M should be applied to a function which simulates the continuation. The expression λf.(fN) almost satisfies the requirement when the application is not nest within other expressions. We need to know the continuation of the entire application in order to sent the result of fN to the rest of the computation. So the reductions are:
( $𝒞$ M)N $\overset{𝒞_{L}}{⟶}$ $𝒞$ λκ.M(λf.κ(fN)), ( $𝒞$ _L)
M( $𝒞$ N) $\overset{𝒞_{R}}{⟶}$ $𝒞$ λκ.N(λv.κ(Mv)) ( $𝒞$ _R) provided that M is a value. ……
The $𝒜$ -application must abort all pending computations. …… so we define the following reductions:
( $𝒜$ M)N $\overset{𝒜_{L}}{⟶}$ $𝒜$ M, ( $𝒜$ _L)
M( $𝒜$ N) $\overset{𝒜_{R}}{⟶}$ $𝒜$ N ( $𝒜$ _R) provided that M is a value. ……
Next we have to consider occurrences of $𝒞$ - and $𝒜$ -applications at the root of a term …… but neither of the above rules can evaluate then any further. We need two top-level evaluation rules. ……
The top-level continuation object should, when invoked, stop the evaluation and make its argument the final value of the entire program …… A natural representation for this abort continuation is λx. $𝒜$ x. ……
the top-level relations are needed to reflect the semantics of $𝒞$ and $𝒜$ . …… we define them to be computation rules and indicate this by use $⊳$ in place of $⟶$ :
( $𝒞$ M) $⊳_{𝒞}$ M(λx. $𝒜$ x), ( $𝒞$ _T)
( $𝒜$ M) $⊳_{𝒜}$ M. ( $𝒜$ _T)
Matthias Felleisen, Daniel P. Friedman. Control Operators, the SECD-Machine, and the Lambda-Calculus. Department of Computer Science, Indiana University. 1986. So we expect that the $𝒞$ -reduction rules must be designed according to the position of $𝒞$ M in an sk-context and that they must be similar to $𝒜$ -reductions. For example, the expression ( $𝒞$ M)N must relate to a term $𝒞$ X for some term X. ……
A first approximation of X is hence λκ.M(λf.κ(fN)). ……
This reflects the fact that upon a continuation invocation, the CEK-machine ignores the current continuation. It means for our Λ_c-continuations that the first action must be an abort action to remove the current context, Hence, λf. $𝒜$ (κ(fN)) is the correct continuation for M. The symmetric case where $𝒞$ N is to the right of a value M is treated in a similar way and so we define the two notions of reduction for the $𝒞$ -application by:
( $𝒞$ M)N $\overset{𝒞_{L}}{⟶}$ $𝒞$ λκ.M(λf. $𝒜$ (κ(fN))) ( $𝒞$ _L)
M( $𝒞$ N) $\overset{𝒞_{R}}{⟶}$ $𝒞$ λκ.N(λv. $𝒜$ (κ(Mv))) provided that M is a value. ( $𝒞$ _R)

[9] R. D. Tennent. The denotational semantics of programming languages. Communications of the ACM, Volume 19, Issue 8 Pages 437 - 453. 1976. Languages or language subsets having the property of referential transparency are termed applicative; other adjectives that have been used include declarative, denotative, descriptive, and functional. ……
It turns out that identifier-binding constructions may be regarded as being merely more readable representations ("syntactic sugarings") of certain arrangements of abstractions, atomic constituents and operator-operand combinations. ……
These examples have provided evidence for the thesis due to Landin [1964] that applicative languages are "spanned" by the "basis" of atomic constituents, combinations, and abstractions. ……
In words, the meaning of a parenthesization is that of the parenthesized expression; the value of a base is given by applying ℬ to it, independently of the environment, while that of an identifier is obtained by applying the given environment to it; the value of an abstraction is, as before, the function whose result for any argument value is the value of the body relative to an environment that binds the bound variable of the abstraction to the argument value; the value of a combination is obtained by applying the value of the operator part to the value of the operand part.
Note that for the evaluation of an abstraction body, the environment used is the one relative to which the abstraction expression is evaluated (rather than the operator-operand combination that caused the activation); i.e. the scope of identifiers is always statically determined, as in Algol 60. To achieve this form of binding for nonlocal variables in LISP the FUNCTION operator must be used; see Gordon[1973].

[Stoy-10] 10.0 ^10.1 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].

[11] Michael J. C. Gordon（英語：Michael J. C. Gordon）. The denotational description of programming languages - an introduction. Springer-Verlag, Berlin, Heidelberg. 1979. Each member of [D₁ + D₂ + …… + D_n] corresponds to exactly one member of some D_i. …… To make this clear we define
[D₁ + D₂ + …… + D_n] = {(d_i, i)|d_i∈D_i, 0<i<n+1}
so that if d∈D_i and d∈D_j then (d, i) represents d considered as a member of D_i and (d, j) represents d considered as a member of D_j.
If D = [D₁ + D₂ + …… + D_n] and d∈D then isD_i d is true if d corresponds to a member of D_i and false otherwise. If isD_i d = true then outD_i d is the member of D_i corresponding to d. If d_i∈D_i then inD_i d_i is the member of D corresponding to d_i.……
isD_i, outD_i and inD_i can be thought of as functions with types:
isD_i : [D₁ + D₂ + …… + D_n] → Bool
outD_i : [D₁ + D₂ + …… + D_n] → D_i
inD_i : D_i → [D₁ + D₂ + …… + D_n]

[12] 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.

[13] R. D. Tennent. Semantics Of Programming Languages. Prentice Hall International Series in Computer Science. 1991. The presentation of denotational-semantic methods is unconventional in some other respects. In their pioneering papers, it was convenient for Dana Scott and Christopher Strachey to demonstrate their new techniques on typeless or dynamically-typed languages. Most workers in the field (including this author) went on to use virtually the same techniques on statically-typed languages. But this style of semantics is cumbersome and unrealistic because of the unnecessary type-checking and branching on types that appears in the semantic equations. ……
To give examples, I have chosen to focus attention on a single ALGOL 60-like language and two important fragments of it: the simple imperative language of while programs, and a "sugared" version of the applicative language that Gordon Plotkin termed PCF; i.e., the simply-typed lambda notation augmented by conditionals, recursion, and arithmetic. This approach emphasizes call-by-name, statically-typed, and deterministic languages, but there is also some brief discussion of the semantics of call-by-value, dynamically-typed, and indeterminate languages. Although ALGOL 60-like languages are relatively unfamiliar these days, their semantic elegance, as revealed to us by John Reynolds, is, in my view, compelling.
Tennent, R.D. Denotational semantics. Abramsky, S.; Gabbay, Dov M.; Maibaum, T.S.E. (編). Semantic Structures. Handbook of logic in computer science 3. Oxford University Press. 1994: 169–322. ISBN 978-0-19-853762-5.

[14] Matthew Hennessy（英語：Matthew Hennessy）. The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. John Wiley and Sons, New York. 1990. ISBN 0-471-92772-4.

[15] Gilles Kahn（英語：Gilles Kahn）. Natural semantics (PDF). 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, FRG. 1987.

[16] Landin, P. J. The Mechanical Evaluation of Expressions (PDF). The Computer Journal（英語：The Computer Journal）. January 1964, 6 (4): 308–320 [2022-11-16]. doi:10.1093/comjnl/6.4.308. （原始內容存檔 (PDF)於2022-11-16）.

[17] 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 f_old by an f_new such that f_new(a, c) = c(f_old(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.

[CEK-18] 18.0 ^18.1 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. ……
The rules (CEK1) through (CEK5) correspond to an evaluator for the λ-value-calculus, e.g., the classical SECD-machine. The rules (CEK6) to (CEK8) define the operations of a $𝒞$ -application: the current continuation is marked, the $𝒞$ -argument is evaluated, and, eventually, the continuation point is passed to the evaluated argument. The last step in this sequence also replaces the current continuation by the initial one. This is where call/cc and $𝒞$ differ: call/cc is equivalent to λf. $𝒞$ λk.k(f k). Rule (CEK9) shows that the invocation of a continuation removes the current continuation, and move the former one in its place. The invocation argument is placed on the stack. According to rule (CEK10), an $𝒜$ -application ignores the continuation and start the evaluation of the $𝒜$ -argument.

[CESK-19] 19.0 ^19.1 Matthias Felleisen, Daniel P. Friedman. A Calculus for Assignments in Higher-Order Languages. Indiana University Computer Science Technical Reports; TR202. 1986. In order to avoid this difficulty we have added σ-abstractions to Λ. Their syntax is (σx.M) where x is a variable and M is an expression. A σ-abstraction does not bind the variable, but it abstracts the right to assign a variable a new value. When a σ-abstraction is applied to a value, it assigns x that value and M is evaluated to yield the result of the application. The meaning of the remaining constructs should be adapted accordingly: variables are re-assignable placeholders for values, abstractions correspond to the call-by-value procedures, and applications invoke the result of the function part on the value of the argument part.

[20] 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.

[21] Heinz Rutishauser（英語：Heinz Rutishauser）. Description of ALGOL 60 (PDF). Springer-Verlag New York Inc. 1967 [2023-07-06]. ISBN 978-3-642-86936-5. doi:10.1007/978-3-642-86934-1. （原始內容存檔 (PDF)於2022-12-22）. A formal parameter of a procedure X does not represent a true quantity as identifiers usually do but is only a designation given to a formal quantity (formal variable, formal array, formal string, formal label, formal switch, formal procedure) which exists only inside the procedure declaration without actually being declared there.
Moreover, a formal parameter has no connection whatsoever with any quantity having the same identifier and existing outside the procedure declaration, and it does not induce any requirements concerning the existence of certain quantities outside the procedure declaration as global parameters do.
The attributive formal has the meaning that such a quantity Q (except if called by value, ……) has no independent existence as a declared quantity has but is only the representative for another quantity A which ultimately will be used as actual operand in place of Q.

[22] Barron, D. W.; Buxton, J. N.; Hartley, D. F.; Nixon, E.; Strachey, C. The Main Features of CPL (PDF). The Computer Journal. 1963-08-01, 6 (2): 134–143. ISSN 0010-4620. doi:10.1093/comjnl/6.2.134 （英語）.
Christopher Strachey. Fundamental Concepts in Programming Languages (PDF). Higher-Order and Symbolic Computation 13:11 (2000). August, 1967 [2026-03-28]. （原始內容存檔 (PDF)於2025-06-30）. An L-value represents an area of the store of the computer. We call this a location rather than an address in order to avoid confusion with the normal store-addressing mechanism of the computer. There is no reason why a location should be exactly one machine-word in size — the objects discussed in programming languages may be, like complex or multiple precision numbers, more than one word long, or, like characters, less. Some locations are addressable (in which case their numerical machine address may be a good representation) but some are not. Before we can decide what sort of representation a general, non-addressable location should have, we should consider what properties we require of it.
The two essential features of a location are that it has a content — i.e. an associated R-value — and that it is in general possible to change this content by a suitable updating operation. ……
The characteristic feature of an expression is that it has a value. We have seen that in general in a programming language, an expression may have two values — an L-value and an R-value. 請檢查|date=中的日期值 (幫助)

[23] Heinz Rutishauser（英語：Heinz Rutishauser）. Description of ALGOL 60 (PDF). Springer-Verlag New York Inc. 1967 [2023-07-06]. ISBN 978-3-642-86936-5. doi:10.1007/978-3-642-86934-1. （原始內容存檔 (PDF)於2022-12-22）. If a formal operand X is called by value, this has the consequence that it is considered as a true quantity local to the fictitious block as if it were declared there. Then upon a procedure call, not a quantity, but a value (single value or an array of values) is designated as corresponding operand, and this value is assigned to X just prior to the execution ofthe procedure.

[24] 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 deﬁnition and future reference to the above rules, we introduce the notion of a singular evaluation context:
$E^{s}$ ⩴ (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). ( $C$ _T) ……
The disturbing element in the calculus of control abstractions is the rule $C$ _T. …… 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 eﬀect. ……
More precisely, when a $𝒞$ -application reaches the root of the program after a number of $C$ _lift 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, $C$ _idem, and $C$ _top suffices for simulating a complete evaluation. ……

fa $⟶$ δ(f,a) (δ)

(λx.e)v $⟶$ e[x←v] (βv)

$E^{s}$ [ $𝒞$ e] $⟶$ $𝒞$ (λk.e(λx. $𝒜$ (k $E^{s}$ [x]))) ( $C$ _lift)

$𝒞$ e $⟶$ $𝒞$ (λk.e(λx. $𝒜$ (kx))) ( $C$ _top)

$𝒞$ (λk.( $𝒞$ e)) $⟶$ $𝒞$ (λk.e(λx. $𝒜$ x)) ( $C$ _idem)

Figure 1: The revised syntactic theory of control"

[25] Matthias Felleisen. The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (學位論文). Indiana University. 1987 [July 22, 2021]. Originally, the control fragment of the λv-CS-calculus was designed around Scheme's control operation call-with-current-continuation, abbreviated call/cc. As explained in Section 3.2, call/cc applies its argument to the continuation of the entire application. The difference between the continuation and the functional abstraction of the continuation is that the former eliminates the continuation of its invocation. Furthermore, call/cc does not give its argument total control over the continuation since the continuation of the call/cc-application remains the defaults continuation for the evaluation of the call/cc-argument. This leads to rather baroque reductions and computations. Two different sets of relations are required. The first captures the behavior of an abort-application ( $𝒜$ M):
( $𝒜$ M) $⊳$ M,
V( $𝒜$ M) $⟶$ ( $𝒜$ M),
( $𝒜$ M)N $⟶$ ( $𝒜$ M);
the second group resembles the $ℱ$ -relations and explains how call/cc provides its argument with an abstraction of its control context:
(call/cc M) $⊳$ M(λx. $𝒜$ x),
V(call/cc M) $⟶$ (call/cc λk.V(M(λm. $𝒜$ (k(Vm))))),
(call/cc M)N $⟶$ (call/cc λk.(M(λm. $𝒜$ (k(mN)))N)).
The $𝒜$ -applications on the right-hand sides are necessary to ensure that all continuation objects immediately eliminate their control contexts upon application.
The second group of reductions contains some regular patterns. The most outstanding is the replication of the call/cc-context, i.e., the term N. If we omit the occurrence that is outside of continuation, we obtain simpler reductions:
( $𝒞$ M) $⊳$ M(λx. $𝒜$ x),
V( $𝒞$ M) $⟶$ ( $𝒞$ λk.(M(λm. $𝒜$ (k(Vm))))),
( $𝒞$ M)N $⟶$ ( $𝒞$ λk.(M(λm. $𝒜$ (k(mN))))),
and we can still implement call/cc as a syntactic abstraction:
(call/cc M) $\equiv$ $𝒞$ (λk.k(Mk)).
Unlike call/cc, $𝒞$ can express $𝒜$ -applications:
( $𝒜$ M) $\equiv$ $𝒞$ (λd.M) where d ∉ FV(M).
The inverse relationship is:
( $𝒞$ M) $\equiv$ (call/cc (λk. $𝒜$ (Mk))).
Although the introduction of $𝒞$ is an essential improvement for the axiom system, the new reductions and the computation still share a common pattern: the occurrence of the form ( $𝒜$ ……) $\equiv$ $𝒞$ (λd. ……). It is easy to see that an omission of these additional $𝒞$ -applications lead to the $ℱ$ -relations in there current form. Given $ℱ$ 's higher degree of expressiveness and the simplicity of the axioms, $ℱ$ is an improvement for a semantic meta-language like Scheme.

[26] Matthias Felleisen. The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (學位論文). Indiana University. 1987 [July 22, 2021]. The term set of Idealized Scheme is Λ_{$ℱ$ σ}, an extension of Λ. …… The language contains two new classes of expressions:
— $ℱ$ -applications: $(ℱ$ M), which are control expressions; M is called the $ℱ$ -argument;
— σ-capabilities: (σx.M), which roughly correspond to assignments; x is the assignable variable, M is the σ-body. ……
The evaluation of an $ℱ$ -application directly corresponds to the informal description of $ℱ$ at outset of the first section. The $ℱ$ -argument is applied to γ, which stands for the current continuation. The current continuation is transferred out of the register into a p-closure and this gives the program total control over its use. In particular the decision about when to use the continuation is left to the program. The operation call/cc in Scheme does not offer the option: it always copies the continuation into a program accessible structure. From the program's perspective this is equivalent to saying that a call/cc-continuation is immediately invoked.
The application of a continuation in Λ_{$ℱ$ σ}-program results in the concatenation of the applied continuation to the current one. This causes the machine to evaluate the applied continuation as if it were a function. If the applied continuation does not affect its continuation during the evaluation, the result is returned to the point of application. In this respect again, CESK-continuations differ from Scheme-continuations. When a program invokes a continuation in Scheme, the interpreter first discards its current continuation and then installs the invoked continuation in the continuation register. Put differently, Scheme-continuation objects have an abortive effect on the continuation of their application point.
Matthias Felleisen, Mitch Wand, Dan Friedman, Bruce Duba. Abstract Continuations: A Mathematical Semantics for Handling Full Functional Jumps. LISP and Functional Programming. 1988. A control-expression transforms the current rest of the computation into a λ-abstraction and binds this abstraction to its variable during the evaluation of the sub-expression:
$C$ [control x M] $\Rightarrow$ M[x:=(λu. $C$ [u])].
Thus, control provides total power over the rest of the computation without introducing another class of objects. If x does not occur free in M, the operation corresponds to an abort; on the other hand, if M immediately invokes x, the default continuation for the rest of M is the current evaluation context. Hence, control is as expressive as abort and escape.

[27] 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,
— V $C$ [] 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]) ……
For a reduction simulation of this rule this means that $ℱ$ -applications must encode their context and apply this to their argument. For the top-level computation rule this is rather simple:
$ℱ$ M $⊳$ _$ℱ$ M(λx.x)
is the required relation. For the other cases, we must consider the two inductive cases of a context definition. Consider the expression ( $ℱ$ M)N and suppose it is embedded in a context $C$ [ ]. Clearly, the function λf.fN is a correct encoding of the immediate context, i.e., $C$ [], can be encoded by another $ℱ$ -application and by building this part of the continuation into the expression λf.fN. Putting these ideas together, the reductions for $ℱ$ -applications should be
( $ℱ$ M)N $⟶$ $ℱ$ λk.M(λf.k(fN)),
U( $ℱ$ M) $⟶$ $ℱ$ λk.M(λv.k(Uv)).
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.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]