语言特征与模式- λ演算

时间 2019-12-05

标签语言特征模式演算繁體版

原文原文链接

语言特征与模式- λ演算

λ演算

wiki定义javascript

Lambda演算能够被称为最小的通用程序设计语言。它包括一条变换规则（变量替换）和一条函数定义方式，Lambda演算之通用在于，任何一个可计算函数都能用这种形式来表达和求值。于是，它是等价于图灵机的。尽管如此，Lambda演算强调的是变换规则的运用，而非实现它们的具体机器。能够认为这是一种更接近软件而非硬件的方式。java

λ 表达式通俗定义

$λ$表达式所属空间$Λ$描述为：算法

$变量 a ∈ Λ$编程
$对于任何 M ∈ Λ，若变量a ∈ Λ，则λa . M ∈ Λ$函数式编程
$对于 F，M ∈ Λ，有 (FM) ∈ Λ$函数

规则一中说明了$a$是一个标识符，表明了一个元素。工具

规则二中说明了能够从$ λ$ 表达式中构造出一个函数$f(a)$，这个函数以参数$a$为自变量，以$λ$表达式描述映射关系，构造出的函数$f$也同属于$λ $表达式.net

规则三中说明了$M$能够做用在$F$上，也即以$M$做为函数$F$的实参数进行计算，返回的值也属于$λ$表达式翻译

三条规则说明了定义了从$Λ$空间到$Λ$空间的映射关系的函数做为$λ $表达式，其全部表达式的集合构成了$Λ$空间。设计

λ 表达式描述了这样的集合$E$，对于函数$y = f(x)$, 其输入$x$，映射关系$f$，输出$y$均属于集合$E$

在函数式编程思想中，说明了这么一个理念，变量和函数等同，能够做为变量参与运算，运算结果也但是函数。这就是高阶函数的定义。

咱们须要以lambda演算为基础构建出可用的基本编程语句模式：包括简单的天然数及其运算、布尔运算、条件语句和循环（递归）语句，由此体现出lambda演算的图灵完备性。lambda演算的图灵完备性须要更为严谨的证实，故此做“体现”两字。

α-变换和 β-规约

对应于程序函数中的入参声明和实参替入概念，不冲突的状况下，入参名称的改变不影响函数的描述，而应用函数时将实参代入形参进行计算。

单位元

类比实数集合中的$1$，对任意$a∈R$，均有 $ 1 * a= a$
λ 表达式的单位元为
$$
e = λx.x
$$
有 $e a = ( λx.x) a = a$,特别的，有$ e e = ( λx.x)( λx.x) = ( λx.x) = e$

η-变换

$$
f = λx.(f x)
$$
这个等价变换有个好处，若$f = g y$，则能够延迟到须要调用函数$f$的时候再计算$g(y)$

柯里化

纯粹的λ 表达式不支持多个参数的函数表达式，能够经过逐步经过返回接受一个参数的函数间接表达多参数函数。如：

function add(a, b) { return a + b; };
var $add = function (a) { return function (b) {return a + b;};};

这样，经过这种转换（翻译），从原理上λ 表达式能够支持多参数函数表达式，咱们可使用多参数函数表达式简化表达。

做用：

描述λ 表达式支持多参数函数表达式的机制。
能够解耦函数中的各个参数，在调用时没必要一次性所有将各个参数值给出，能够将未给出所有实参的“不彻底”表达式看成变量使用。
封装和信息隐藏，将一些参数进行隐藏，仅给出须要传参的参数，而内部已经绑定的实参对于调用者说不可见。
组装，经过各个算子的组合构建出更高层次的函数，提升函数的复用性。

布尔类型构建

布尔变量

布尔全集仅有 true 和 false 两个，考虑设计一个二元组描述整个全集，并将第一个设为false，第二个设为true

(define true  (lambda (x y) x))
(define false (lambda (x y) y))

布尔运算-或

注意到true和false有选择功能，对于OR(x, y), 当x为真时选择x，不然选择y，故能够这样定义OR

(define OR (lambda (x y) (x true y)))

布尔运算-与

对于AND(x, y), 当x为真时选择y，不然选择false

(define AND (lambda (x y) (x y false)))

布尔运算-非

当x为真时选择false，不然选择true

(define NOT (lambda (x) (x false true)))

天然数类型构建

零

考虑这一函数，其表明的数字和参数f被应用的次数相同

(define ZERO  (lambda (f x) x))

则有

(define ONE  (lambda (f x) (f x)))
(define TWO  (lambda (f x) (f (f x))))
(define N    (lambda (f x) (f (f (....  (f x))))))

递增算子

咱们须要一个从$N$递推到$N+1$的函数$ INC$，有

INC N = N + 1

咱们须要解出INC算子，尝试经过递推解决

每次都是经过一个lambda表达式来表达一种类型，由于lambda表达式是函数，故一个类型的特征一般表如今调用该lambda表达式描述的函数后所体现的行为，那么要了解天然数$N$的特征，则看看调用N的函数所表现出的行为：

(TWO f x) = (f (f x))
(N   f x) = (f (f (....  (f x))))

注意到$N$应用到$ (f x)$后是将参数$x$应用到函数$f N$次, 故$N+ 1 $应该是在$N$的基础上多调用$f$一次，固有

((INC N) f x) =  (f (N f x))

利用η-变换解出INC算子，须要将参数$f$、$x$ 柯里化，隐藏到内部lambda的参数列表中，由于$f$、$x$ 是N的参数，不该是INC的参数

((INC N) f x) = (f (N f x))
(lambda (N f x) ((INC N) f x)) = (lambda (N f x)(f (N f x)))
INC = (lambda (N f x)(f (N f x)))
INC = (lambda N (lambda (f x)(f (N f x))))
INC = (lambda N (lambda f (lambda x (f ((N f) x)))))

加法算子

如今定义两个整数的加法ADD，明显有

(define ADD (lambda (N M) (lambda (f x) (N f (M f x)))))

乘法算子

显然，有

(define MUL (lambda (N M) (lambda (f x) (N (M f) x))))

递减算子

相似于求链表中一个节点的前置节点，在单链表的状况下，能够经过设置两个指针p，q，每次走时p紧跟q后面，当q到达某节点时，p即指向该节点的前置节点。故咱们须要定义二元组存放这样的两个指针，同时预留一个参数f以即可以编写关于PAIR实例操做的方法。

(define (PAIR a b)(lambda f (f a b)))

以及访问第一个元素和第二个元素的方法

(define L (lambda (a b) (a)))
(define R (lambda (a b) (b)))

还有一个后驱算法Trans使得
$$(lastNumber,currentNumber)⇒(currentNumber,SuccNumber)$$
有

(define TRANS (lambda (p) (PAIR (p R) (INC (p R)))))

故递减算子PRED为

(define PRED (lambda (N) ((N TRANS (PAIR 0 0)) L)))

减法算子

因而减法就很简单了，将PRED调用M次应用在N上获得N - M
$$Subt:=λnm.m Pred n$$

谓语和条件语句

在条件语句中，if (condition) then {...} else {...},condition称为谓语，谓语是一个依据其变量的值来断定真或假的方法。

从判断一个数是不是零的谓语开始，利用天然数的性质，当函数f被应用时（即数大于等于1）当即返回false，x为初始值true，有

(define (isZero N) (N (lambda (x) false) true))

等于、不等于、大于、小于也能从isZero 和以前的布尔运算构建出，再也不叙述。

而条件语句其实就是单位元e。

(define (IF condition then else) (condition then else))

递归（循环）语句和Y组合子

在数学上，若对于一个函数$f(x)$,存在一个$x = x0$,使得$f(x) = x$,则称$x = x0$为函数$f$的一个不动点。

而在lambda函数上，对于任意一个函数$f$，咱们均能找到一个由$f$推导出来的一个不动点$x =Y(f)$，使得$f(Y(f))=Y(f)$，这个$Y$被称做$Y$组合子，咱们试求出这样的函数$Y$，使得对于任意一个函数都能经过$Y$获得$f$的不动点。

Y组合子用于实现函数的可递归特性。举例，为了完成以下的函数的定义：

(define (fac n) (if (= n 1)
                    1
                    (+ n (fac (- n 1)))))

按照lambda表达式的语法来讲，函数体里的fac是未定义的，没有出如今参数列表中，也不支持对函数命名，咱们想借助一个以下的环境为函数提供可递归的定义：

$$ g:=λf x.M(f, x)$$

$f$为本身定义的可递归函数，在函数体$M$内对$f$的调用如同递归调用自身，而$x$则是本来定义递归函数$f$的参数，因为$f$出如今参数列表中，故能够在函数体内使用函数$f$。咱们根据这样的规则定义了函数$g$用来实现递归语义，则还须要一个工具把具体的$f$算出来以便代入到$g$的参数中实现递归的功能，而这样的一个工具即是组合子$Y$，它知足$Y g = f$。

关于Y的定义以下:
$$Y = λ f. (λ x. f (x x)) (λ x. f (x x))$$

* Y组合子的推导

以斐波那契数列项推导公式为例，目标是消除名字fac

(define (fac n) (if (= n 1)
                1
                (+ n (fac (- n 1)))))

将函数fac放入参数以完成递归调用

(define (fac f n) (if (= n 1)
                  1
                  (+ n (f f (- n 1)))))

柯里化，解耦函数f和参数n

(define (fac f) (lambda (n) (if (= n 1)
                        1
                        (+ n ((f f) (- n 1))))))
;; 调用
((fac fac) 5) ;;15

将w = (f f)抽象出来有

(define (w x) (x x))
(define (fac f) (lambda (n) (if (= n 1)
                       1
                       (+ n ((w f) (- n 1))))))
;; 调用
((w fac) 5) ;;15

将g = (w f) 提取为参数，并根据η-变换处理g延迟g的计算

(define (w x) (x x))
(define (fac f) ((lambda (g) (lambda (n) (if (= n 1)
                         1
                         (+ n (g (- n 1))))))
             (lambda (x) ((w f) x))))
;; 调用
((w fac) 5) ;;15

提取自定义的匿名递归函数表达式做为参数，参数名为h，重构后的函数名为Y0，同时命名斐波那契的匿名递归函数表达式为fac，fac实现了在函数体内不调用fac自身。
```
(define (w x) (x x))
(define fac (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1)))))))
(define Y0 (lambda (h) (lambda (f) (h (lambda (x) ((w f) x))))))
;; 调用
((w (Y0 fac)) 5) ;;15
```

对于调用表达式，将fac从函数w中提出做为参数f

(define (w x) (x x))
(define fac (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1)))))))
(define Y0 (lambda (h) (lambda (f) (h (lambda (x) ((w f) x))))))
;; 调用
(((lambda (f) (w (Y0 f))) fac) 5) ;;15

记Y = (lambda (f) (w (Y0 f)))

(define (w x) (x x))
(define fac (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1)))))))
(define Y0 (lambda (h) (lambda (f) (h (lambda (x) ((w f) x))))))
(define Y  (lambda (f) (w (Y0 f))))
;; 调用
((Y fac) 5) ;;15

至此，只要将fac的定义代入调用式中便可消除名字fac，对于Y，将Y0 展开，把Y0 中的变量f替换为g以避免与函数Y中的f产生歧义(α-变换)，有

(define (w x) (x x))
(define Y  (lambda (f) (w ((lambda (h) (lambda (g) (h (lambda (x) ((w g) x))))) f))))
;; 调用
((Y (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1))))))) 5) ;;15

对于Y，展开最里面的w，并将实参f代入到参数h，有

(define (w x) (x x))
(define Y  (lambda (f) (w (lambda (g) (f (lambda (x) ((g g) x)))))))

展开余下的w，即为最后的结果

(define Y  (lambda (f) ((lambda (g) (f (lambda (x) ((g g) x))))
                    (lambda (g) (f (lambda (x) ((g g) x)))))))
;; 调用
((Y (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1))))))) 5) ;;15

另外，在第6步中，能够将参数h放在f的后面（而不是前面）做为参数，调用时优先与w结合，有

(define (w x) (x x))
(define (fac f) (lambda (h)
                        (h (lambda (x) (((w f) h) x)))))
(((w fac) (lambda (g) (lambda (n) (if (= n 1) 1 (+ n (g (- n 1))))))) 5)

将fac直接代入到调用式中，得出

(define Θ (w (lambda (f) (lambda (h) (h (lambda (x) (((f f) h) x)))))))

这实际上 Θ与以前推导出的Y算子等价，说明不一样的变换和规约顺序能够得出不一样的结果。

拓展

更深刻的主题：

负数、有理数的构造。（思路：和前驱算子同样，设计一个二元组，如 -5 == 0 - 5，0.5 = 1 / 2）
实数的构造，涉及到实数理论。

参考

λ演算，https://zh.wikipedia.org/wiki...
神奇的λ演算，http://www.jianshu.com/p/e7db...
A Tutorial Introduction to the Lambda Calculu，http://www.inf.fu-berlin.de/i...
Fixed-point combinators in JavaScript: Memoizing recursive functions，http://matt.might.net/article...
Lambda Calculus: Subtraction is hard, http://gettingsharper.de/2012...

语言特征与模式- λ演算

语言特征与模式- λ演算

λ演算

λ 表达式通俗定义

α-变换 和 β-规约

单位元

η-变换

柯里化

布尔类型构建

布尔变量

布尔运算-或

布尔运算-与

布尔运算-非

天然数类型构建

零

递增算子

加法算子

乘法算子

递减算子

减法算子

谓语和条件语句

递归（循环）语句和Y组合子

* Y组合子的推导

拓展

参考

α-变换和 β-规约