码迷,mamicode.com
首页 > 其他好文 > 详细

lambda演算

时间:2014-09-15 14:06:39      阅读:350      评论:0      收藏:0      [点我收藏+]

标签:blog   http   java   ar   问题   sp   log   on   c   

先了解下相关的知识点(以下都只用先了解简单的概念,建议wiki):

BNF范式,上下文无关文法,函数柯里化。

 

lambda读书笔记演算:

http://www.blogjava.net/wxb_nudt/archive/2005/05/15/4311.aspx

lambda演算实例

 

关于lambda演算的定义和解释的确有点让人迷糊,主要不是因为lambda演算有多复杂,而是一些基本概念没有归入正确位置的原因。

这里先写一点草稿,在实践中学习和领悟lambda演算到底是个什么东西。

一:自然数运算:

在lambda演算中的邱奇数定义
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))

SUCC = λn.λf.λx.f(n f x)

SUCC是一个有三个自由变量的函数

计算
SUCC 0
=λn.λf.λx.f (n f x) 0 //将0代入n
=λf.λx.f (0 f x) //0=λf.λx.x
=λf.λx.f (λf.λx.x f x) //λf.λx.x f x是将两个参数的函数λf.λx.x应用于(f x)这两个值的结果,结果等于x
=λf.λx.f x //正好等于1的邱奇数定义

SUCC 1
=λn.λf.λx.f (n f x) 1 //将1代入n
=λf.λx.f (1 f x) //0=λf.λx.x
=λf.λx.f (λf.λx.(f x) f x) //λf.λx.(f x) f x是将两个参数的函数λf.λx.(f x)应用于(f x)这两个值的结果,结果等于(f x)
=λf.λx.f (f x) //正好等于2的邱奇数定义

小节:
不妨把lambda演算看做一个自动机,你输入一个式子(一个λ项),它就给你输出一个演算结果,至于输入和输出有什么意义,是我们自己赋予的。

比如为了计算0的后继,我们只是输入(λn.λf.λx.f(n f x) λf.λx.x)给这个机器,这个机器就会给我们输出λf.λx.f x。在解释这个输入输出关系时,我们会说,SUCC 0 = 1,这样就赋予这个运算一个意义。这个自动机知道自己在做加1操作吗?其实它什么也不知道。

为什么邱奇数这样定义?其实不妨把它们看做是被偶然发现的一些λ项,这些λ项的组合项的演算结果恰好能对应于自然数的运算而已。定义自然数还有别的定义方式,邱奇数及对应的运算符只是其中的一种而已。

比如我们又发现一个λ项PLUS
PLUS = λm.λn.λf.λx.m f (n f x)
先不要管什么意义,试试下面这个组合起来的λ项

PLUS 2 3
= λm.λn.λf.λx.m f (n f x) 2 3 //将3和2应用于m,n这两个自由变量上
=λf.λx.3 f (2 f x) //(2 f x) = (λf.λx.(f (f x)) f x) = f (f x)
=λf.λx.3 f (f (f x)) //3=λf.λx.f (f (f x))
=λf.λx.(λf.λx.f (f (f x)))) f (f (f x)) //将f 和 (f (f x)) 应用于f和x这两个自由变量上
=λf.λx.f (f (f (f (f x)))) //我们发现正好等于5的邱奇数定义

很奇妙的性质,我们用PLUS(λm.λn.λf.λx.m f (n f x) )这样的λ项作用于代表2和3的邱奇数时,得到的演算结果恰恰是代表5的邱奇数。

此外,还可以构造出乘法和除法等各种运算符。



二、逻辑运算:

TRUE := λx y.x
FALSE := λx y.y
AND := λp q.p q FALSE
OR := λp q.p TRUE q
NOT := λp.p FALSE TRUE
IFTHENELSE := λp x y.p x y

需要重复加以强调的是,这些λ项都是一些构造,我们构造它们的原因是,这些项的组合所得到的演算结果恰恰符合我们对逻辑运算的认识,所以我们才赋予它们以逻辑运算符的意义,也正因为这些构造,我们才可以让那个演算自动机代替我们去做各种逻辑运算。

计算:

AND TRUE TRUE
=λp q.p q FALSE (TRUE TRUE)//用TRUE和FALSE替换自由变量p和q
=TRUE TRUE FALSE //TRUE = λx y.x
=λx y.x (TRUE FALSE) //用TRUE和FALSE替换自由变量x和y
=TRUE //y没有在函数体中出现,所以等于TRUE

三、有序对
CONS := λx y.λp.IF p x y
CAR := λx.x TRUE
CDR := λx.x FALSE

这里很有趣的一点是,和lisp的实现对照,我们发现car和cdr是在lisp的基本运算符中的,但实际上,它们仍然可以用λ项来表示。

我们先构造一个有序对
CONS m1 m2
=λx y.λp.IF p x y (m1 m2) //很简单,用m1和m2替换x和y就行了
=λp.IF p m1 m2


然后计算这个有序对的CAR
CAR (IF p m1 m2)
=λx.(x TRUE) (λp.IF p m1 m2) //x用(λp.IF p m1 m2)替换
=(λp.IF p m1 m2) TRUE //p用TRUE替换
=IF TRUE m1 m2 //根据IF的含义我们知道结果就是m1
=m1

CDR (IF p m1 m2)
= λx.x FALSE (λp.IF p m1 m2)
=(λp.IF p m1 m2) FALSE
=IF FALSE m1 m2
=m2

四、Y不动点

考虑一下这台λ演算自动机,它再简单不过了,只是按照非常简单的规则应用函数,将值绑定到自由变量,然后继续演算,直到最终结果。

在开始计算时,我们输入的都是长长的λ项,甚至连SUCC,CDR这些简写都没有,比如要做一个2+3的加法,我们会输入 λm.λn.λf.λx.m f (n f x) (λf.λx.f (f x)) (λf.λx.f (f (f x))),然后这台演算自动机会给我们输出λf.λx.f (f (f (f (f x))))这个结果。

这样问题就来了,如果函数要递归调用自己,那该怎么办呢?在lambda演算中,无法定义包含自身的函数(虽然在lisp中可以)。
构造出这样一个Y
Y = λf.(λx.f(x x)) (λx.f(x x))
Y g
= (λf.(λx.f(x x))(λx.f(x x))) g //用g替换f
= λx.g(x x) (λx.g(x x)) //用λx.g(x x)替换x这个自由变量
= g (λx.g (x x) λx.g (x x)) //我们发现λx.g (x x) λx.g (x x)恰好等于Y g
= g (Y g)
继续
= g (λx.g (x x) λx.g (x x))
= g (g (λx.g (x x) λx.g (x x)))
= g (g (g (λx.g (x x) λx.g (x x))))
= ... ...

这里我们能看出来了,如果给这个演算自动机输入Y g,也就是实际上输入了这样一个λ项(λf.(λx.f(x x)) (λx.f(x x)) g)之后,演算自动机将不会停机,永远递归下去,直到耗尽所有内存。

从这里可以看出来,虽然lambda演算表面上不能自己调用自己,因为无法给自己起一个名字,但实际上可以构造出这样一个λ项,可以让计算递归下去。

接下来,看如何利用这一特殊的λ项的性质,来完成一些有用的计算:

计算阶乘的数学公式如下:
fact(n) = if n=0 then 1 else n * fact(n-1)

构造如下的λ项,计算5的阶乘,其中Y=λf.(λx.f(x x)) (λx.f(x x)),而g=λf n.(ISZERO n 1 MULT n·f(n-1)),都是λ项的形式。

(λn.(ISZERO n 1 (MULT n ((Y g)(n-1)))) 5
=
(按照维基百科上的计算过程,改写为容易懂的if then else形式)

if 5 = 0 then 1 else 5·(g(Y g,5-1))
5·(g(Y g)4)
5·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 4)
5·(if 4 = 0 then 1 else 4·(g(Y g,4-1)))
5·(4·(g(Y g)3))
5·(4·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 3))
5·(4·(if 3 = 0 then 1 else 3·(g(Y g,3-1))))
5·(4·(3·(g(Y g)2)))

lambda演算

标签:blog   http   java   ar   问题   sp   log   on   c   

原文地址:http://www.cnblogs.com/foohack/p/3972607.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!