ISWIM 📖 Wikipedia

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

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

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

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

ISWIM程序基于了一个单一表达式，它由where或let子句、条件表达式和函数定义所限定。ISWIM在表示法上的特色，是与CPL一起，最早使用了局部定义子句L where x = M${\displaystyle \ \equiv \ }$ let x = M; L，尤其是let子句适合表达ALGOL 60的嵌套（英语：Nested function）的块结构而为后继者语言所承袭：

{λ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

λ演算中的应用（英语：Function application）项(M N)及其关联的抽象项M := λx.L，在应用表达式中要一起表示为：{λM.(M N)}[λx.L]，它对应的ISWIM表示为：M(N) where M(x) = L或let M(x) = L; M(N)。

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

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

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

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论文中，Landin将顶层的ISWIM构造称为amessage即消息，并示例了两个命令，特定的需求例如Print a+2b，和定义例如Def x = a+2b。

ISWIM基本的等价规则包括：

• (D')规则：x = L and y = M and …… and z = N${\displaystyle \ \equiv \ }$ (x, y, ……, z) = (L, M, ……, N)，它对应于Standard ML中的模式匹配。
• (I')规则：f(x) = L${\displaystyle \ \equiv \ }$ f = (g where g(x) = L)，它对应于Standard ML中的fun f x = L${\displaystyle \ \Leftrightarrow \ }$ val f = fn x => L。
  • (I')规则还有更一般性的柯里化形式，形如f(a, b, c)(x, y) = L${\displaystyle \ \equiv \ }$ f(a, b, c) = (g where g(x, y) = L)。
• (I)规则：(f where f(x) = L) M${\displaystyle \ \equiv \ }$ L where x = M，这里的f where f(x) = L对应于Standard ML中此前将fn x => L绑定到变量时所生成的闭包。
• (β')规则：(x = L) where y = M${\displaystyle \ \equiv \ }$ x = (L where y = M)。
• (β)规则：L where x = M${\displaystyle \ \equiv \ }$ Subst${\displaystyle \,{\begin{smallmatrix}{\mathsf {M}}\\{\mathsf {x}}\end{smallmatrix}}\,}$ L，它对应于λ演算中的β-归约，即用M代换（英语：Substitution (logic)）L中出现的所有适合的x。
• (Y)规则：rec x = L${\displaystyle \ \equiv \ }$ x = (L where rec x = L)，这里的rec对应于λ演算中的Y不动点算子。

下面以阶乘函数的应用（英语：Function application）为例，它用到了(I')、(Y)、(β)和(I)等价规则：

通过运用(I')、(β')、(D')和(Y)等价规则，ISWIM确使任何定义都能被标准化，即表达为lhs = rhs的绑定形式，等式的两侧（英语：Sides of an equation）分别为：左手侧（lhs）的确切的一个约束变量，右手侧（rhs）的它所对应的主体（body）。通过反向运用等价规则，ISWIM可在这个例子中恢复出等式的左手侧为rec f(n)形式的表达式：

对应用表达式（AE）进行机器求值的SECD抽象机将状态（英语：State (computer science)）变迁规则定义为状态变换（英语：Transformation (function)）函数Transform(S,E,C,D)：

这里的[]是空列表，它在ISWIM中表示为nullist，在应用表达式中表示为()。这里的::是列表构造的中缀构造子，x::L${\displaystyle \,\equiv \,}$ cons(x,L)${\displaystyle \,\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算子对应的状态变换函数为：

程序点在ISWIM中表示为pp f(X) = L。

应用表达式扩展了的赋值器（assigner）${\displaystyle \,\Leftarrow \,}$ ，其应用形式为lhs${\displaystyle \,\Leftarrow \,}$ rhs，则称为指令式应用表达式（IAE）。ALGOL 60中传名调用所关联起来的形式参数和实际参数（英语：Argument of a function），具有等价关系，它们的状态内位置属于同一个等价类故而称为共享，在直接计算机表示中每个等价类对应一个地址。赋值器重置lhs确定的状态内位置以及同它共享的所有的状态内位置，并在堆栈S上留下nullist作为结果。执行指令式应用表达式的抽象机的状态变换函数为：

这里的l表示左值，传递左值的所有的状态内位置position(e,p)共享同一个地址(position(e,x),e)。为了执行扩展了J算子（英语：J operator）的具有赋值器的指令式应用表达式，所细化的SECD抽象机叫做共享机器。

Landin将Y不动点算子表示为指令式应用表达示式：Y(F) ≡ {λz.{λz′.2nd(z⇐z′,z)}[F(z)]}[separate(nullist)]，它对应的ISWIM表示为：

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

separate(x)函数同I恒等组合子一样取用右值x，从而避免了后续的赋值变更这个处在外层的非局部（英语：Non-local variable）值。它的用途典型的对应于ALGOL 60中声明形式参数为传值调用，例如let x = separate(x()); L，形式参数对应的实际参数是在某个外层中声明的局部标识符，它采用separate函数初始化比如let x = separate(0.0)。separate函数对应的状态变换函数为：

Landin规定了赋值且保全命令assignandhold，它采用守卫命令处置指令式编程语言如ALGOL 60的原始数据类型：

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

本條目部分或全部内容出自以GFDL授權發佈的《自由線上電腦詞典》（FOLDOC）。