lambda演算

先了解下相关的知识点(以下都只用先了解简单的概念,建议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)))

时间: 2024-12-12 19:11:55

lambda演算的相关文章

Lambda演算 - 简述Y组合子的作用

Y组合子:\f.(\x.f(xx))(\x.f(xx)),接受一个函数,返回一个高阶函数 Y组合子用于生成匿名递归函数. 什么叫匿名递归函数,考虑以下C语言递归函数 int sum(int n) { return n == 0 ? 0 : n + sum(n-1); } 这个函数在内部递归调用了自身,调用自身需要函数本体的名字,这个函数叫sum,sum内部用名字sum,递归调用了自己 在lambda演算中,可以写成类似的表达式sum = \x. x == 0 ? 0 : sum x 但是对于一个

Lambda演算 Lambda Calculus 的简单理解

Lambda演算 在λ演算中,每个表达式都代表一个函数,这个函数有一个参数,并且返回一个值.不论是参数和返回值,也都是一个单参的函数.可以这么说,λ演算中,只有一种"类型",那就是这种单参函数. 函数是通过λ表达式匿名地定义的,这个表达式说明了此函数将对其参数进行什么操作.例如,"加2"函数f(x)= x + 2可以用lambda演算表示为λx.x + 2 (或者λy.y + 2,参数的取名无关紧要)而f(3)的值可以写作(λx.x + 2) 3.函数的应用(app

图灵机与lambda演算的关系

莱布尼兹曾经有两个梦想: 1. 创建一种"普遍语言"(universal language)使得任何问题都可以用这种语言表述: 2. 找到一种"判定方法"(decision method)以解决所有可以在"普遍语言"中所表述的问题. 这两个问题是上百年来数理逻辑.数学哲学和数学基础问题的核心.实质.对前一个问题的回答就是自弗雷格.罗素开始,经公理集合论运动的最终结果:以一阶谓词逻辑为语言所形式化阐述的集合论,现在已经成为数学的普遍语言,现代逻辑学

lambda演算感想之规则

在lambda演算中,丘奇创建了丘奇数,在理解丘奇数的过程中,逐渐颠覆了一些以前的认知,丘奇数用自己的方式重新定义了数字,即: 0是 lambda s z . z  1是 lambda s z . s z 2是 lambda s z . s (s z) 在理解丘奇数的过程中,我一直在纠结于为何丘奇就可以创建一个数字代表0 1 2,然后还在其中加入了运算规则,因为在我之前的认知中,数字是神圣的,他就像客观事物中的一草一木一样,是不可以被替代的,所以我们不可能在创建一个丘奇数来代替数字,因为数字是唯

lambda 演算

本文是来自 g9yuayon, 算是一篇读书笔记. :-) 详细内容还是看原作者的. 自由变量 在 (lambda (x) (x y…)) 中, x 是绑定的变量, y 是自由变量 在 (lambda (x) (lambda (y) (x y …))) 中, 要分情况 在第一个 lambda 中, x, y 都是绑定的, 在 第二个 lambda中, x是自由变量 alpha 规则, (转换规则) (lambda (x) (if (= x 0) 1 0)) ;; 等价于 (lambda (y)

Lambda演算(二)归约!归约!归约!

(一) 这里先不列出λ项的正式定义,只记住λ表达式语义上的构造方式为: x 一个单独的变量名是一个λ项表达式: (λx.M) 该λ表示一个函数.其中 M 是这个函数的函数体,M 本身也是一个 λ项. 除了 x 之外,M 中可能还有其他变量名,λ 这个符号用于指示函数体 M 的参数为 x. 了便于理解,可以将 M 看作函数体,x 看作形参,即变量名. 例如:λx.x+3 即表示一个函数 f(x) = x+3,该函数会返回x与3相加的结果 要注意的是,我这里的写法并不规范,在λ表达式中,二元运算符是

从lambda到函数式编程

1 Object.send(:remove_const,'TRUE') 2 Object.send(:remove_const,'FALSE') 3 4 def to_integer(pro) 5 pro[-> n { n + 1 }][0] 6 end 7 8 def to_boolean(pro) 9 pro[true][false] 10 end 11 12 def to_array(l, count = nil) 13 array = [] 14 until to_boolean(IS_

Java Lambda简明教程(一)

Lambda表达式背景 许多热门的编程语言如今都有一个叫做lambda或者闭包的语言特性,包括比较经典的函数式编程语言Lisp,Scheme,也有稍微年轻的语言比如JavaScript,Python,Ruby,Groovy,Scale,C#,甚至C++也有Lambda表达式.一些语言是运行在java虚拟机上,作为虚拟机最具代表的语言java当然也不想落后. 究竟什么是Lambda表达式? Lambda表达式的概念来自于Lambda演算,下面是一个java lambda的简单例子, (int x)

C++14尝鲜:Generic Lambdas(泛型lambda)

所谓泛型lambda.就是在形參声明中使用auto类型指示说明符的lambda. 比方 auto lambda = [](auto x, auto y) {return x + y;}; 依据C++14标准,这一lambda与下面代码作用同样. struct unnamed_lambda { template<typename T, typename U> auto operator()(T x, U y) const {return x + y;} }; auto lambda = unna