函数式编程的数学基础(六)组合子逻辑
通过对丘奇数的推导,我们已经初步熟悉了lambda演算。
历史上的组合子逻辑受到lambda演算的启发,并且与lambda演算有千丝万缕的联系,但它实际上发展成了一个与lambda演算独立且竞争的理论体系。
从lambda演算出发去定义组合子,我们可以把组合子理解成,我们把一些特定的lambda函数起了名字。
比如,接受一个参数,并且把它直接返回的函数,我们起名为Identifier,简称为I组合子:
我们不难发现,此组合子也就是丘奇数0。当然,lambda函数无穷无尽,我们不可能给每一个函数都起一个名字把它变成组合子。组合子的意义也绝不仅仅是给lambda函数起名。
使得组合子逻辑变得有意义的是,一些数学家发现,仅通过一组特定的组合子,我们就可以无需定义新的lambda函数,达成图灵完备。
ISK系统
我们首先来介绍第一组组合子—ISK组合子系统,在前文介绍的I组合子的基础上,我们再定义两个组合子,首先是K组合子:
从直觉上理解,K组合子的右边部分λy.x\lambda y.xλy.x是一个常函数:即,不论传入什么参数y,都返回一个固定值x,而x则由前一步传入,因此,K组合子可被理解为一个常函数生成器。
这里为了方便后文讨论,我们给(Kx)(K x)(Kx)起名为CxC_xCx,即常函数。
S组合子是非常巧妙的设计,当我们给x和y分别传入I函数或者C函数,就可以得到不同的结构。
数学上,能够证明ISK系统是图灵完备的,即,无需lambda符号,仅仅通过I、S、K函数的调用就可以表达一切lambda演算。
我们考虑lambda演算,任何一个lambda表达式,仅可能是以下两种形式之一:
其中,M和N均表示lambda表达式。MxM_xMx表示可能含有自由变量的lambda表达式。
我们考虑仅用SK是否能够表达这两种形式。这种转换我们定义为T。针对上述两种形式的第二种,即M NM\ NM N,显然有:
接下来,我们需要分情况讨论λx.Mx\lambda x.M_xλx.Mx。MxM_xMx有四种可能性:
其中TxT_xTx定义如下:
上面一组关系也揭示了ISK系统的设计思路。
实际上,若单以数学角度,I组合子也不是必需。我们只需要给S传入两个K,即可得到I。推导过程如下:
所以,ISK系统在有些资料中也被称为SK系统。
BCKW系统
ISK系统是否是唯一的组合子系统呢?当然不是。
接下来我们介绍另一组组合子系统:BCKW系统。
BCKW 系统是 Haskell Curry 的成果。
我们保留常量生成组合子K,在此基础上,我们引入B、C和W三种组合子。
B组合子可以理解为函数的复合运算,与我们在初等数学中的函数复合定义一致。
在一些数学分支的写法中,函数复合会以二元运算的方式书写:
B组合子可以视为函数复合的lambda版本。
C组合子交换二元函数的两个参数。
W组合子把函数传递给自身。
W组合子看上去是半个不动点,我们可以用 W WW\ WW W 来构造一个不动点。
SK系统的与lambda演算的等价性已经可以证明,那么我们只需要构造出K组合子,即可实现图灵完备。
S组合子的构造方法如下:
因此,BCKW系统也实现了图灵完备。
单点组合子系统X
定义XXX为:
不难验证:
因此,单点X组合子系统与SK系统等价,所以它也是图灵完备的。
结语
组合子系统最初从lambda体系定义出来,后期实际上与lambda演算形成了竞争关系。
组合子系统揭示了一些高阶函数更本质的特征,它提供了一种全新的视角去理解lambda。
在带类型的lambda演算提出后,Haskel Curry的成果又将组合子逻辑纳入了数学界主流的希尔伯特公理体系。我们留待后文介绍。
转载自:https://juejin.cn/post/7332331306212900901