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]