lambda演算学习笔记

《lambda演算学习笔记》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、前言blog好久没有更新了，上次更新还是4月28号。这段时间实在是很忙，4月的最后一周为了赶一篇论文，累死累活，最后在tom的帮助下总算在4月30号截稿之前完成了。4月29号的晚上一直改到了第二天凌晨3点才睡。4月30号下午回家，可是没有料到长沙的八一路修路，路上堵车。打的从学校到火车站花了40分钟，平时只要15分钟的。于是在最后10分钟一路狂奔，终于在开车前1分钟上车了。五一长假的第一天去了双峰山，云雾缭绕之中真的颇有几分气势，可惜数码照片全部都拍得很模糊，早知道我就自己动手好了。五一归来马上开始整理软件工程相关资料，一共花了3天时间，还剩软

2、件标准化的部分没有整理完毕。接下来的三天，一直在学习lambda演算的相关内容，由于资料不全，学习的过程很是痛苦。国内的大学好像基本上不开设FunctionalProgramming课程，因此FP的基础知识lambda演算也讲得很少。不过好歹在网上找到了一些资料，加上数理逻辑中的少量介绍，明白了一个大致。相关资料网址会列在最后。Lamda演算简介Wikipedia（维基百科全书）中关于lambda演算的解释如下：Thelambdacalculusisaformalsystemdesignedtoinvestigatefunctiondefini

3、tion,functionapplication,andrecursion.ItwasintroducedbyAlonzoChurchandStephenColeKleeneinthe1930s;Churchusedthelambdacalculusin1936togiveanegativeanswertotheEntscheidungsproblem.Thecalculuscanbeusedtocleanlydefinewhatacomputablefunctionis.Thequestionofwhethertwolambdacalculu

4、sexpressionsareequivalentcannotbesolvedbyageneralalgorithm,andthiswasthefirstquestion,evenbeforethehaltingproblem,forwhichundecidabilitycouldbeproved.Lambdacalculushasgreatlyinfluencedfunctionalprogramminglanguages,especiallyLisp.Lambda演算是一个形式系统，它被设计出来用来研究函数定义，函数应用和递归。它是在二十世

5、纪三十年代由AlonzoChurch和StephenColeKleene发明的。Church在1936年使用lambda演算来证明了判定问题是没有答案的。Lambda演算可以用来清晰的定义什么是一个可计算的函数。两个lambda演算表达式是否相等的问题不能够被一个通用的算法解决，这是第一个问题，它甚至排在停机问题之前。为了证明停机问题是没有答案的，不可判定性能够被证明。Lambda演算对于函数式编程语言（例如lisp）有重大的影响。同时，数理逻辑中对于lambda演算的介绍就简单得多：λ-演算可以说是最简单、最小的一个形式系统。它是在二十世纪三

6、十年代由AlonzoChurch和StephenColeKleene发明的。至今，在欧洲得到了广泛的发展。可以说，欧洲的计算机科学是从λ-演算开始的，而现在仍然是欧洲计算机科学的基础，首先它是函数式程序理论的基础，而后，在λ-演算的基础上，发展起来的π-演算、χ-演算，成为近年来的并发程序的理论工具之一，许多经典的并发程序模型就是以π-演算为框架的。这里不由得想起一位我尊敬的老师的博士毕业论文就是关于π-演算的，可惜这位老师已经去别的学校了。Lambda演算表达了两个计算机计算中最基本的概念“代入”和“置换”。“代入”我们一般理解为函数调用，或

7、者是用实参代替函数中的形参；“置换”我们一般理解为变量换名规则。后面会讲到，“代入”就是用lambda演算中的β-归约概念。而“替换”就是lambda演算中的α-变换。Lambda演算系统的形式化定义维基百科全书上面的对于lambda演算的定义不是很正规，但是说明性的文字较多。而数理逻辑中的定义很严密，不过没有说明不容易理解。我尽可能把所有资料结合起来说明lambda演算系统的定义。字母表lambda演算系统中合法的字符如下：1.        x1，x2，x3，…变元（变元的数量是无穷的，不能在有限步骤内穷举，这个很重要，后面有定理是根据这一

8、点证明的）2.        à归约3.        ＝等价4.        λ，（，） （辅助工具符号，一共有三个，λ和左括号右括号）所有能够在