ISWIM

ISWIM（“If you See What I Mean”的首字母缩写），是一种抽象的计算机编程语言或编程语言家族，它由彼得·兰丁设计，并描述在他1966年于ACM通讯发表的文章《接下来的700种编程语言》之中。

尽管没有实现，它被证明为在编程语言开发中非常有影响力的语言，特别是对于函数式编程语言，比如SASL、ML、NPL、Haskell和它们的后继者，还有数据流程编程语言如Lucid。

## 概述

ISWIM是具有函数式核心的指令式编程语言，它构成自加了语法糖的叫做“应用式编程语言表达式 (计算机科学)”（AE）的扩展λ演算，并增加了强力控制机制即对应J算子的程序点算子`pp`。ISWIM的操作语义，可以使用Landin的SECD机来定义，并且使用了传值调用，从而具有及早求值的求值策略。

ISWIM基于了λ演算，从而具有高阶函数和词法作用域变量。ISWIM的目标之一，就是要看起来更像数学表示，所以在定义结构之时，放弃了ALGOL的语句括号`begin……end`，转而采用了越位规则和基于缩进的作用域。

没有进行过直接实现ISWIM的尝试，但是Arthur Evans的PAL，和John C. Reynolds的Gedanken，获取了Landin的多数概念，包括强力的控制转移运算，这两者都是动态类型语言。Robin Milner的ML，可以被认为等价于没有J算子，而有类型推论的ISWIM。

从ISWIM衍生出的另一条路线，是去掉指令式特征如J算子并加以单赋值限制，从而成为纯函数式语言并进一步切换为惰性求值。这条路线导致了SASL、Hope、KRC、Miranda、Haskell、Clean。

## 语法

ISWIM程序基于了一个单一表达式，它由`where`或`let`子句、条件表达式和函数定义所限定。ISWIM在表示法上的特色，是与CPL一起，最早使用了局部定义子句

```sml
L where x = M
```

$$\ \equiv\ $$

```sml
let x = M; L
```

尤其是`let`子句适合表达ALGOL 60的嵌套函数的块结构而为后继者语言所承袭：

AE｜逻辑ISWIM

```bash
{λ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]
```

```sml
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
```

```sml
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
```

λ演算中的函数应用项`(M N)`及其关联的抽象项`M := λx.L`，在应用表达式中要一起表示为：

```bash
{λM.(M N)}[λx.L]
```

它对应的ISWIM表示为：

```sml
M(N) where M(x) = L
```

或

```sml
let M(x) = L; M(N)
```

ISWIM所基于的应用表达式，采用花括号包围算子，采用方括号包围运算元或运算元列表，它为了“同时”或“平行”定义而在`λ`和`.`之间扩展了标识符列表，列表用圆括号包围并在其中用逗号分隔元素。应用表达式为递归定义而采用了Y不动点组合子，采用`λ().L`表示无参数函数thunk。示例中处置函数参数问题的`{λf.f}`对应于I恒等组合子，此外还可能用到K常量组合子，和B复合组合子。

在ISWIM论文中首次出现了用来定义结构的代数数据类型定义，这是通过自然语言的`either……or……`和`……and……`描述完成的，但明确的表示出了当代函数式编程语言比如Standard ML中的“积类型之和”：

抽象ISWIM｜Standard ML

an $\mathrm{aexpression}$ ($\mathrm{aexp}$) is either $simple$, and has a $body$, which is an $\mathrm{identifier}$ or a $combination$, in which case it has a $rator$, which is an $\mathrm{aexp}$, and a $rand$, which is an $\mathrm{aexp}$, or a $conditional$, …… , or $one\text{-}armed$, …… , or a $listing$, …… , or $beet$, …… .

```SML
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）的简称，它代表了

```sml
L where x = M
```

或

```sml
let x = M; L
```

这里的`L`称为主要子句，`x = M`称为支持（support）即辅助定义。

在ISWIM论文中，Landin将顶层的ISWIM构造称为`amessage`即消息，并示例了两个命令，特定的需求例如`<span style="color:green;">'''Print'''</span> a+2b`，和定义例如`<span style="color:green;">'''Def'''</span> x = a+2b`。

## 规则

ISWIM基本的等价规则包括：

```sml
x = L and y = M and …… and z = N
```

$$\ \equiv\ $$

```sml
(x, y, ……, z) = (L, M, ……, N)
```

此规则对应于Standard ML中的模式匹配。

```sml
f(x) = L
```

$$\ \equiv\ $$

```sml
f = (g where g(x) = L)
```

这里的

```sml
(g where g(x) = L)
```

是闭包，此规则对应于Standard ML中的

```sml
fun f x = L
```

$$\ \Leftrightarrow\ $$

```sml
val f = fn x => L
```

- (I')规则还有更一般性的柯里化形式，形如

```sml
f(a, b, c)(x, y) = L
```

$$\ \equiv\ $$

```sml
f(a, b, c) = (g where g(x, y) = L)
```

```sml
(f where f(x) = L) M
```

$$\ \equiv\ $$

```sml
L where x = M
```

这里的

```sml
(f where f(x) = L)
```

是闭包。

```sml
(x = L) where y = M
```

$$\ \equiv\ $$

```sml
x = (L where y = M)
```

```sml
L where x = M
```

$\ \equiv\ $`Subst<big><math>\,\begin{smallmatrix} \mathsf{M} \\ \mathsf{x} \end{smallmatrix}\,</math></big>L`，此规则对应于λ演算中的β-归约，即用`M`代换 (逻辑)`L`中出现的所有适合的`x`。

```sml
rec x = L
```

$$\ \equiv\ $$

```sml
x = (L where rec x = L)
```

这里的

```sml
rec
```

对应于λ演算中的Y不动点算子。

通过运用(I')、(β')、(D')和(Y)等价规则，ISWIM确使任何定义都能被标准化，即表达为`lhs = rhs`的绑定形式，等式的等式的两侧分别为：左手侧（lhs）的确切的一个约束变量，右手侧（rhs）的它所对应的主体（body）。下面以阶乘函数的函数应用为例，这里采用了ISWIM派生语言比如PAL和可计算函数逻辑 ML之中的let表达式：

```sml
let x = M in L
```

$$\ \equiv\ $$

```sml
let x = M; L
```

设 `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可在这个例子中恢复出等式的左手侧为形式的表达式：

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

## 语义

R. D. Tennent在1976年论文《编程语言的指称语义》中将应用表达式（AE）用于示范。

基于应用表达式的如下形式语法：

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

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

定义如下指称语义：

```sml
δ ∈ 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
```

在BNF范式中，`⩴`（U+2A74常写为`::=`）表示产生式，`|`表示交替 (形式语言)。在指称语义中，`in`表示内射而入，而`|`表示投射而出，二者由Dana Scott和Christopher Strachey在1971年介入。

具有let表达式的应用式编程语言很适合用于形式语义示范。R. D. Tennent在1991年著作《编程语言的语义》中采用了新的指称语义表示法并将编程可计算函数用于示范。Matthew Hennessy在1990年著作《编程语言的语义：使用结构性操作语义的初步介绍》中将简单的函数式语言用于小步操作语义示范。Gilles Kahn在1987年论文《自然语义》中将Mini-ML用于大步操作语义示范。

## 执行

SECD机是第一个专门设计用来求值应用表达式（AE）的抽象机，SECD四者分别指示堆栈、环境、控制和转储。它最初描述于Peter Landin的1964年论文《表达式的机器求值》中。常见的处理指令序列的SECD虚拟机，是Peter Henderson于1980年在LispKit Lisp编译器中定义并实现的。

应用表达式扩展了的赋值器（assigner）$\,\Leftarrow\,$，其应用形式为`lhs<math>\,\Leftarrow\,</math>rhs`，则称为指令式应用表达式（IAE）。为了执行扩展了J算子的具有赋值器的指令式应用表达式，所细化的SECD机叫做共享机。

Matthias Felleisen和Daniel P. Friedman在1986年借鉴John C. Reynolds于1972年提出的扩展了续体的元循环解释器，修订Peter Landin的SECD机，从而规定了CEK机

$\mathcal{C}$

$\mathcal{A}$

$\mathcal{A}$

$\mathcal{C}$

$\mathcal{C}$

$\mathcal{C}$

$\mathcal{C}$

$\mathcal{A}$

$\mathcal{A}$

CEK三者分别指示控制、环境和续体。

### SECD机

对应用表达式进行机器求值的SECD机，将状态 (计算机科学)变迁规则定义为状态变换 (函数)函数`Transform(S,E,C,D)`：

S｜E｜C｜D｜ $\rightarrow$ ｜S｜E｜C｜D

s｜e｜combination(rator,rand)::c｜d｜ $\rightarrow$ ｜s｜e｜rand::rator::ap::c｜d

S｜E｜C｜D｜ $\rightarrow$ ｜S｜E｜C｜D

s｜e｜identifier(x)::c｜d｜ $\rightarrow$ ｜locate(position(e,x),e)::s｜e｜c｜d

s｜e｜λexp(v,L)::c｜d｜ $\rightarrow$ ｜closure((e,v),L)::s｜e｜c｜d

S｜E｜C｜D｜ $\rightarrow$ ｜S｜E｜C｜D

closure((e',v),L)::x::s｜e｜ap::c｜d｜ $\rightarrow$ ｜(v,x)::e'｜L｜(s,e,c,d)

f::x::s｜e｜ap::c｜d｜ $\rightarrow$ ｜f(x)::s｜e｜c｜d

x::s｜e｜(s',e',c',d')｜ $\rightarrow$ ｜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算子的应用形式`f = '''J'''(λX.L)`称为“程序点”，它将函数`F = λX.L`变换成程序闭包。J算子对应的状态变换函数为：

S｜E｜C｜D｜ $\rightarrow$ ｜S｜E｜C｜D

F::s｜e｜J::ap::c｜d｜ $\rightarrow$ ｜program-closure(F,d)::s｜e｜c｜d

S｜E｜C｜D｜ $\rightarrow$ ｜S｜E｜C｜D

program-closure(F,(s',e',c',d'))::x::s｜e｜ap::c｜d｜ $\rightarrow$ ｜F::x::s'｜e'｜ap::c'｜d'

程序点在ISWIM中表示为`<span style="color:green;">'''pp'''</span> f(X) = L`。

### 共享机

共享机建模于指令式编程语言ALGOL 60的过程调用机制，这里默认传递给形式参数的是函数的变元的名字，在这个过程内定义的形式参数的名字，与在这个过程外定义的实际参数的名字，二者之间具有等价关系。历经可能的多次传名调用得到这些等价的名字，其状态内位置属于同一个等价类故而称为共享，在直接计算机表示中每个等价类对应一个地址。

这里采用了Christopher Strachey在1963年提出的左值和右值概念，共享机默认共享一个变量的左值，这里的左值表示了它所处在的环境和它在这个环境中的位置，传名调用形式参数的状态内位置保存传递过来的左值。执行指令式应用表达式的抽象机的状态变换函数为：

C｜E｜共享｜S｜D｜ $\rightarrow$ ｜C｜E｜共享｜S｜D

combination(rator,rand)::c｜e｜s｜d｜ $\rightarrow$ ｜rand::rator::ap::c｜e｜s｜d

::identifier(x)::ap::c｜e｜s｜d｜ $\rightarrow$ ｜parameter(x)::c｜e｜s｜d

assigner(lhs,rhs)::c｜e｜s｜d｜ $\rightarrow$ ｜rhs::lhs::assign::c｜e｜s｜d

C｜E｜共享｜S｜D｜ $\rightarrow$ ｜C｜E｜共享｜S｜D

identifier(x)::c｜e｜s｜d｜ $\rightarrow$ ｜c｜e｜l=(position(e,x),e)｜locate(l)::s｜d

parameter(x)::c｜e｜s｜d｜ $\rightarrow$ ｜c｜e｜l=locate(position(e,x),e)｜locate(l)::s｜d

assign::c｜e｜l｜r::x::s｜d｜ $\rightarrow$ ｜c｜e｜reset(l,x)::s｜d

λexp(v,L)::c｜e｜s｜d｜ $\rightarrow$ ｜c｜e｜closure((e,v),L)::s｜d

C｜E｜共享｜S｜D｜ $\rightarrow$ ｜C｜E｜共享｜S｜D

ap::c｜e｜l｜closure((e',v),L)::r::s｜d｜ $\rightarrow$ ｜L｜(v,l)::e'｜(s,e,c)::d

ap::c｜e｜l｜f::r::s｜d｜ $\rightarrow$ ｜c｜e｜x::s｜d

e｜l｜r::s｜(s',e',c')::d｜ $\rightarrow$ ｜c'｜e'｜l｜r::s'｜d

Landin规定在这个过程内以无参数函数调用的形式，来访问传名调用形式参数所引用的系统存储的那个值本身，即处在赋值器`rhs`的右值，例如通过`x()`访问形式参数`x`。赋值器重置其`lhs`确定的左值所引用的那个右值，并在堆栈`S`上留下`nullist`作为结果。

`separate(x)`函数共享一个变量所引用的右值，从而避免了后续的赋值变更这个处在外层的非局部变量值。在处置ALGOL 60时它的用途典型为：声明已经传递来的形式参数为传值调用，例如

```SML
let x = separate(x()); L
```

通过回溯传名调用形式参数传递，最终能确定其对应的实际参数，是在某个外层过程中声明即采用`separate`函数初始化的局部标识符，比如

```SML
let x = separate(0.0)
```

`separate`函数对应的状态变换函数可以定义为：

C｜E｜共享｜S｜D｜ $\rightarrow$ ｜C｜E｜共享｜S｜D

separate::ap::c｜e｜r::s｜d｜ $\rightarrow$ ｜c｜e｜r｜r::s｜d

separate::ap::c｜e｜l｜r::s｜d｜ $\rightarrow$ ｜c｜e｜r｜r::s｜d

Landin将在SECD机和共享机上执行的Y不动点算子，实现为指令式应用表达示式：

```bash
Y(F) ≡ {λz.{λz′.2nd(z⇐z′,z)}[F(z)]}[separate(nullist)]
```

它对应的ISWIM表示为：

`<span style="color:green;">'''Y'''</span>(F) <math>\equiv</math> <span style="color:green;">'''let'''</span> z = <span style="color:green;">separate</span>(<span style="color:green;">nullist</span>); <span style="color:green;">'''let'''</span> z' = F(z); 2nd(z<math>\,\Leftarrow\,</math>z',z)`

Landin为处置ALGOL 60而规定了赋值且保全命令`assignandhold`，它采用守卫命令处置原始数据类型：

`assignandhold(x)(y) <math>\equiv</math> <span style="color:green;">'''let'''</span> x = (<span style="color:green;">real</span>(y)→float(x); <span style="color:green;">integer</span>(y)→entier(x+0.5); <span style="color:green;">Boolean</span>(y)→(<span style="color:green;">Boolean</span>(x)→x)); 2nd(y<math>\,\Leftarrow\,</math>x,x)`。

### CEK机

在CEK机中定义了捕获当前续体算子$\,\mathcal{C}\,$和以当前续体调用算子`call/cc ≡ λf.<math>\mathcal{C}</math>λk.(f k)`。下面是CEK机的状态 (计算机科学)变迁函数：

C｜E｜K｜ $\mapsto$ ｜C｜E｜K

λx.L｜ρ｜κ｜ $\mapsto$ ｜""｜{}｜(ret (λx.L,ρ))::κ

M N｜ρ｜κ｜ $\mapsto$ ｜M｜ρ｜(arg N ρ)::κ

""｜{}｜(ret V)::(fun (λx.L,ρ))::κ｜ $\mapsto$ ｜L｜ρx:=V｜κ

C｜E｜K｜ $\mapsto$ ｜C｜E｜K

$\mathcal{C}\,$L｜ρ｜κ｜ $\mapsto$ ｜L｜ρ｜cont::κ

""｜{}｜(ret (λk.L,ρ))::cont::κ｜ $\mapsto$ ｜L｜ρk:=(p,κ)｜stop

""｜{}｜(ret (p,κ'))::cont::κ｜ $\mapsto$ ｜""｜{}｜(ret (p,κ))::κ'

""｜{}｜(ret V)::(fun (p,κ'))::κ｜ $\mapsto$ ｜""｜{}｜(ret V)::κ'

$\mathcal{A}\,$L｜ρ｜κ｜ $\mapsto$ ｜L｜ρ｜stop

这里的`""`表示空字符串，而`{}`表示空集合。这里的环境`ρ`是从变量到语义值的有限映射。这里的`(λx.L,ρ)`是闭包，而`('''p''',κ)`是叫做“续延点”的标签结构，二者都属于语义值。初始状态是三元组`⟨L, {}, ['''stop''']⟩`，终止状态是三元组`⟨"", {}, [('''ret''' V), '''stop''']⟩`。

Matthias Felleisen和Daniel P. Friedman在1986年又将CEK机扩展为CESK机，CESK四者分别指示控制、环境、存储和续体，在其中增加了赋值抽象`σx.L`。下面是CESK机的状态变迁函数：

C｜E｜S｜K｜ $\mapsto$ ｜C｜E｜S｜K

λx.L｜ρ｜θ｜κ｜ $\mapsto$ ｜""｜{}｜θ｜(ret (λx.L,ρ))::κ

M N｜ρ｜θ｜κ｜ $\mapsto$ ｜M｜ρ｜θ｜(arg N ρ)::κ

""｜{}｜θ｜(ret V)::(fun (λx.L,ρ))::κ｜ $\mapsto$ ｜L｜ρx:=n｜θn:=V｜κ

这里的环境`ρ`是从变量到表示位置的自然数的有限映射，而存储`θ`是从自然数到语义值即λ-闭包或σ-闭包的有限映射。这里的`θ[n:=V]`有着`n ∉ Dom(θ)`。

C｜E｜S｜K｜ $\mapsto$ ｜C｜E｜S｜K

σx.L｜ρ｜θ｜κ｜ $\mapsto$ ｜""｜{}｜θ｜(ret (σx.L,ρ))::κ

""｜{}｜θ｜(ret V)::(fun (σx.L,ρ))::κ｜ $\mapsto$ ｜L｜ρ｜θρ(x):=V｜κ

## 引用

本条目部分或全部内容出自以GFDL授权发布的《自由线上电脑词典》（FOLDOC）

## 基本资料

- 编程范型：函数式, 指令式
- 发行时间：1966年
- 设计者：彼得·兰丁
- 作用域：词法
- 受影响于：ALGOL 60、Lisp
- 施影响于：PAL、SASL、ML、NPL、Lucid、Haskell