ISWIM

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

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

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

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

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

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

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

λ演算中的项(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表示无参数函数。示例中处置的{λf.f}对应于I恒等组合子，此外还可能用到K常量组合子，和B复合组合子。

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

这里的特有术语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\ \equiv\ (x, y, ……, z) = (L, M, ……, N)，此规则对应于Standard ML中的模式匹配。
*(I')规则：f(x) = L\ \equiv\ f = (g where g(x) = L)，这里的(g where g(x) = L)是闭包，此规则对应于Standard ML中的fun f x = L\ \Leftrightarrow\ 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)是闭包。
*(β')规则：(x = L) where y = M\ \equiv\ x = (L where y = M)。
*(β)规则：L where x = M\ \equiv\ Subst\,\begin{smallmatrix} \mathsf{M} \\ \mathsf{x} \end{smallmatrix}\,L，此规则对应于λ演算中的β-归约，即用ML中出现的所有适合的x。
*(Y)规则：rec x = L\ \equiv\ x = (L where rec x = L)，这里的rec对应于λ演算中的Y不动点算子。

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

通过反向运用等价规则，ISWIM可在这个例子中恢复出等式的左手侧为形式的表达式：

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

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

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

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

定义如下指称语义：

δ ∈ 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年介入。

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

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

应用表达式扩展了的赋值器（assigner）\,\Leftarrow\,，其应用形式为lhs\,\Leftarrow\,rhs，则称为指令式应用表达式（IAE）。为了执行扩展了的具有赋值器的指令式应用表达式，所细化的SECD机叫做共享机，修订Peter Landin的SECD机，从而规定了，CEK三者分别指示控制、环境和续体。

SECD机
对应用表达式进行机器求值的SECD机，将变迁规则定义为状态函数Transform(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共享结构即元素为有序对的可持久性单向链表，从而将这个派生函数直接用代数数据类型的元组和递归数据类型的列表的特定算子来表示。

的应用形式f = J(λX.L)称为“程序点”，它将函数F = λX.L变换成程序闭包。J算子对应的状态变换函数为：

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

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

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

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

separate(x)函数共享一个变量所引用的右值，从而避免了后续的赋值变更这个处在外层的值。在处置ALGOL 60时它的用途典型为：声明已经传递来的形式参数为传值调用，例如let x = separate(x()); L；通过回溯传名调用形式参数传递，最终能确定其对应的实际参数，是在某个外层过程中声明即采用separate函数初始化的局部标识符，比如let x = separate(0.0)。

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

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机
在中定义了捕获当前续体算子\,\mathcal{C}\,和算子call/cc ≡ λf.\mathcal{C}λk.(f k)。下面是CEK机的变迁函数：

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

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

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

引用