Abstraction elimination

(本文不保证不误人子弟,切勿轻信)

Unlambda指的是lambda计算中去掉lambda操作(does not have lambda(or abstraction) operation of the lambda calculus),那实现消除abstraction是如何做到的呢?

一、基本的abstraction elimination

假设表达式F,我们想用它创建一个函数(function),将这个函数应用到X上,用符号表示变量并写成$x(即^xF,这里用^表示标准的lambda),那么想得到unlambda,需要消除lambda operation。

对F来说,有三种情况:1. F是内建(函数)(或者是非$x的变量);2. F是$x;3. F 是一个应用(函数),即 `GH,其中G和H是比F简单的表达式(就是降低F表达式复杂度),对这三种情况分别讨论:

1. 从^xF中消除lambda,其中F不依赖于$x,故可以将F看作是常函数,这是因为X是输入,F不依赖于输入自然就表示F是常函数,即 `kF

2. 从^x$x中消除lambda,对于输入X,这个函数返回就是$x,即自身,故对应i

3. 从^x`GH中消除lambda,假定我们已经知道如何从^xG和^xH中消除lambda,根据^x`GH意思是有一个输入X,而`GH表示应用G到H上,这表示可以将X传入到^xG 和^xH中,然后将后者结果作为前者的输入,这正是内建s的作用,故^x`GH对应

  ``s^xG^xH

总结如上规律,考虑消除^xF的lambda,注意这里的F可能是一个复杂的表达式,并且可能跟$x相关,对F从左往右看,遇到一个 `(backquote),将其替代为 ``s, 遇到 $x 则替代为 i, 遇到任何内建函数或者非$x的变量,则在这个函数符号或者变量符号前加一个 `k,如果有几个lambda需要消除,从内部往外部消除,具体参见下面的例子b。

例子:

a.函数 ^x`$xk 的去lambda,此处我们用上面1)、2)和3)的规律来转换。

^x`$xk -> (F是`$xk,是复杂表达式,应用上面第三点)-> ``s^x$x^xk -> (分别对^x$x 和 ^xk 去lambda)-> ``si`kk

b.函数 ^x^y`$y$x 的去lambda,此处我们用上面的总结规律来转换(当然也可以根据1、 2、 3点规律老老实实的转换)

^x^y`$y$x -> (根据例子a的结论)-> ^x``si`k$x ->(根据总结规律先转换左部两个 ` )-> ``s``s    si`k$x ->(从第三个s开始转换内建函数s和i,空白格是故意加上去为了区分左部是已经转换的,右部尚未转换)

      -> ``s``s`ks`ki`    `k$x -> ``s``s`ks`ki``s`kki 

如果给出了若干个lambda,那么abstraction eliminate后的表达式将会指数级增长(以3为底的指数)。一个 ` 变为 ``s,然后 ``s 变为 ``s``s`ks,然后又变为 ``s``s`ks``s``s`ks``s`kk`ks,依次类推。 

二、高效的abstraction elimination

 上面分析的第一种情况下,表达式F是内建函数或者是非$x的变量,则可以将lambda ^xF 写成 `kF,事实上,只要F不包含 x 就可以这么转换,因为此时 F 是与 x 无关的,可以将 F 看作是 x 的常量,此时可以不用遍历繁杂的F表达式而可以直接转换写成`kF。可以将这种转换看作 abstraction elimination的快捷方式(shortcut)。

有一点需要注意,这样的转换在 “纯的隐式类型的lambda计算” 领域可以很好的工作,或者在我们不用过多担心计算非终止(如死循环,或无限大列表)的情况下也是可以很好的工作。因为没有边界作用(side effect),当然目前我们所看到的函数确实不产生边界作用。可是,当我们写 ^xF的时候,我们可能是考虑到有边界作用的或者计算不能结束(因为是lambda),这个边界作用使得某些计算被延迟直到函数被应用到某个变量上(即,直到 $x 接收到一个值,哪怕那个值其实是被忽略的),所以如果我们使用shortcut并写成 `kF,那么一旦遇到这个表达式,F 就会被计算,即使这个函数没有被应用到某个参数变量,这跟原来的 ^xF的延迟性不吻合。

于是使用shortcut将 ^xF写成 `kF 的前提条件是 a)F 不包含 $x;b)计算 F 能计算出来并且没有边界作用。一个确保条件b)能满足的方法是检查F的应用形式为:内建函数 K 应用到一个参数上, 或者内建函数 S 应用到一个或两个参数上,或者内建函数 D 应用到任何表达式上。(这样保证F是无法立即被计算出来)

如果F不包含 x 但是包含一些可能导致边界作用或者无法计算完成(比如死循环)的计算,此时虽然不能使用 shortcut 转换,但仍然有另一种方法较高效地实现 abstraction elimination,即使用内建函数 D,转换成 `d`kF 。(可能,对于一个纯函数论者,他是不会在程序中使用 D 的。)

abstraction elimination的另一个快捷方法是将形如 ^x`F$x 转换为 F,当然这需要确保 F 中没有变量 $x。这在F不是内建函数 D 并且非 $x的情况下,转换非常快捷。然而如果 F 可能会产生边界作用时,跟其他shortcut一样,这种转换带有危险(也可以写成 `dF从而绕开这种危险)。

三、更多的unlambda内建函数

1. v 函数

v 函数好比一个黑洞,v需要一个输入参数,并忽略这个参数然后返回v自己,故 v 可以用来吞噬 N个参数。

v函数可以由 s,k 和 i 来实现(即,也可以使用 s 和 k 来实现)。

2.   .x 函数

.x 函数需要一个参数,并将这个参数打印到标准输出。 r 函数 是 .x 函数的一个实例,即x参数是一个换行符, 因此, `ri 的作用是打印一个新行, `rv 或者 `rr 或者 `r(anything) 都是打印一个新行,当然, r 函数本身不会做任何事情,因为 r 函数没有被应用到一个参数中。

3. d 函数

 d 函数是一个特例。当unlambda准备计算 `FG,并且 F 计算出来为 d (比如 F 就是 d),那么 G 将不会被计算, 结果为 `dG, `dG允诺会计算G(a promise to evaluate G),只有在 `dG被应用到表达式H上(在此之前,G是保持未计算状态),这时,G 最终被计算出来(在 H 被计算出来之后),然后 再应用到 H 上。

例如, `d`ri 不会做任何事情(保持未计算状态), ``d`rii 打印一个新行,因为 `d`ri 被应用到 i 上,于是 `ri(作为G)被计算出来为i(其副作用是打印新行),然后在应用到 i 上, 还是为 i 本身。另一个例子是 ``dd`ri ,打印一个空白行,事实上, `dd 首先被计算,根据 d 函数的特性,计算结果为允诺计算d(a promise to evaluate d),即可以看作第二个 d 被第一个 d 暂时封住了,所以不会阻止 `ri 打印新行,然后再 计算 d(第二个d),此时新行已经被打印。另一方面, ``id`ri 不会打印新行,因为 `id会被先计算出来为 d,阻止了后面的 `ri, 类似地, ```s`kdri 首先转为 ```kdi`ri (将`kd 看作 X,`r 看作 Y, i 看作 Z),然后 ``kdi 被计算为 d, 然后阻止了后面的 `ri, 故这个函数不会打印新行。

`d`kF 是另一个 promise 的形式(与 `dG 比较):当这个函数 应用到 参数 Y 上, Y 被忽略,然后返回 F 。这在上文 abstraction elimination 中有关 shortcut 的讨论中提到(大概因为 d 函数的 promise 特性与边界作用类似吧)。

原文地址:https://www.cnblogs.com/sjjsxl/p/5628349.html