λ演算是一套用于研究函数定义、函数应用和递归的形式系统。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世纪三十
年代引入,Church 运用 lambda 演算在 1936 年给出 判定性问题 (Entscheidungsproblem) 的一个否定的答案。这种演算可以
用来清晰地定义什么是一个可计算函数。关于两个 lambda 演算表达式是否等价的命题无法通过一个通用的算法来解决,这是
不可判定性能够证明的头一个问题,甚至还在停机问题之先。Lambda 演算对函数式编程有巨大的影响,特别是Lisp 语言。
Lambda 演算可以被称为最小的通用程序设计语言。它包括一条变换规则 (变量替换) 和一条函数定义方式,Lambda 演算之通
用在于,任何一个可计算函数都能用这种形式来表达和求值。因而,它是等价于图灵机的。
尽管如此,Lambda 演算强调的是变换规则的运用,而非实现它们的具体机器。可以认为这是一种更接近软件而非硬件的方
式。
有界vs自由
python 代码
lambda表达式中的x,y与外部x,y显然是不同的,为了区别两者,引入了有界和自由的概念。lambda只能处理有界的标识
符。
当一个标识符出现在了lambda的参数里面,并包含在了这个lambda表达式中,那么就称其有界限,反之无界。
python 代码
x,y被包含在了lambda表达式中,所以其有界,而z没有那么他就是自由标识符,虽然y在lambda的参数中,但并没有在表达式中
出现。那么他就是自由的
有界和自由是一个相对的概念
python 代码
- (lambda x:(lambda y,z:y+2))
相对于内嵌的lambda,z是自由的,因为在内嵌的表达式中并没有z出现,然后相对于整个lambda表达式,它又是有界的。
“free(x)”代表表达式x所有的自由变量集合
判定lambda表达式完全合法的标准是它的所有变量都是有界的。
上例中
(lambda x,y:x+2)虽然可以在程序中正常执行,但其实是一个不完全合法的lambda表达式
lambda算子计算规则
alpha,beta,eta
alpha(conversion)(转换规则):
简单来说就是重命名规则(但被绑定的变量能否由另一个变量替换有一系列的限制):
lambda x,y:x+y与
lambda m,n:m+n是等价的
beta(reduction)(归约)
将lambda表达式中的有界变量替换为应用中对应得实际值
(lambda x,y:x+y)(2,3)等价于
2+3
Beta的严格定义:
lambda x . B e = B[x := e] if free(e) \subset free(B[x := e]
考虑这样一种情况
python 代码
- (lambda x:(lambda y:x+y)(x+3)
其等价的表达式现在是
x+x+3
这里的问题是lambda中得有界变量与(x+3)中得自由变量有冲突,两则是不同的,需要区别
alpha[x/z]:(lambda x:(lambda y:x+y)(x+3)=(lambda z:(lambda y:z+y)(x+3)
现在展开后就是
z+x+3,正确结果
eta(变换)
Eta表达的是外延性的概念,在这里外延性指的是,两个函数对于所有的参数得到的结果都一致,当且仅当它们是同一个函数。
(python中的lambda不等价与该处所指的lambda)
www.wikilib.com/wiki
分享到:
相关推荐
The Lambda Calculus (Stanford Encyclopedia of Philosophy)
Lambda Calculus for computer science; Although it is an introduction, it is an abstract for lambda calculus
A short introduction to the Lambda CalculusA short introduction to the Lambda CalculusA short introduction to the Lambda Calculus
Lambda Calculus its Syntax and Semantics.djvu 俄文版
An Introduction to Functional Programming Through Lambda Calculus 英文版 200页
这是一本讲述了Lambda Calculus的书,而且其内容讲的十分透彻,只是很厚,希望大家努力
λ演算,λ(Lambda(大写Λ,小写λ)读音:lan b(m) da(兰亩达)['læ;mdə])演算是一套用于研究函数定义、函数应用和递归的形式系统。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世纪三十年代引入,...
Lambda学习,不错的资料参考 The λ-calculus was begun at Princeton, and the purpose of this report is to show how it has been recycled every decade after the 1930s in new and useful ways.
lambda的书
函数式编程的理论论文
introduction to lambda calculus.Henk Barendregt Erik Barendsen.pdf
Functional programming is rooted in lambda calculus, which constitutes the world's smallest programming language. This well-respected text offers an accessible introduction to functional programming ...
Graphic lambda calculus
很好的书,要看的人也不用我安利,某宝上35大洋买的...希望大家也上传一些自己的私藏~~~~~
The λ-calculus and combinatory logic are two systems of logic which can also serve as abstract programming languages. They both aim to describe some very general properties of programs that can ...
It is surprising that despite the simplicity of its syntax, the λ-calculus hosts a large body of notation, abbreviations, naming conventions, etc. Our aim, as far as the notation throughout this work...
The Impact of the Lambda Calculus in Logic and Computer Science (1997)-计算机科学
λ演算(lambda calculus)是一套用于研究函数定义、函数应用和递归的形式系统。它由阿隆佐·邱奇和他的学生斯蒂芬·科尔·克莱尼在20世纪30年代发明的。 λ演算可以被称为最小的通用程序设计语言。它包括一条变换...
those without this familiarity may find it heavy going., The first part describes how to translate a high-level functional language into an intermediate language, called the lambda calculus, ...