标签：

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

Abstraction elimination

标签：

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