λ演算（LambdaCalculus）⼊门基础（⼀）：定义与归约
此系列⽂章是我学习lambda演算过程的总结与复习，着重于探讨“为什么(Why)”与“怎么做(How)”，也希望能对看到它的⼈学习了解这个形式系统有些微帮助。由于之前看了不少wiki、tutorial、introduction之流，绝⼤多数读过之后仅知其然⽽不知其所以然，我不知道为什么它们都不解释为什么要这么做，为什么要有这些东西，这些东西是怎么得来的，但这个事实让我⾮常苦恼，因此才有了这个系列。我试图将⾃⼰的浅薄理解稍作阐释梳理，知之尚浅，如有错漏不妥之处请不吝指出，欢迎交流讨论批评建议。
部分参考：
Wikipedia
SEP(Stanford Encyclopedia of Philosophy)
Brilliant
Cornell Recitation Course
⼀个有翻译的tutorial：[翻译][原⽂]
⼀个完全how to的introduction
NOTE: 在lambda演算中，函数是⼀等公民。即对函数做⼀般的基本操作都是合法的，⽐如把函数作为参数传⼊或返回，赋给⼀个变量等等。
lambda | λ 定义
要描述⼀个形式系统，我们⾸先需要约定⽤到的基本符号，对于本系列所介绍的lambda演算，其符号集包括λ.()和变量名(x, y, z, etc.)。1. λ 表达式/项
在lambda演算中只有三种合法表达式（也可以称之为项：λ-expression or λ-term）存在：
变量(Variable)
形式：x
变量名可能是⼀个字符或字符串，它表⽰⼀个参数（形参）或者⼀个值（实参）。
< z var
抽象(Abstraction)
形式：λx.M
它表⽰获取⼀个参数x并返回M的lambda函数，M是⼀个合法lambda表达式，且符号λ和.表⽰绑定变量x于该函数抽象的函数体M。简单来说就是表⽰⼀个形参为x的函数M。
< λx.yλx.(λy.xy)
前者表⽰⼀个常量函数(constant function)，输出恒为y与输⼊⽆关；后者的输出是⼀个函数抽象λy.xy，输⼊可以是任意的lambda表达式。
注意：⼀个lambda函数的输⼊和输出也可以是函数。
应⽤(Application)
形式：M N
它表⽰将函数M应⽤于参数N，其中M、N均为合法lambda表达式。简单来说就是给函数M输⼊实参N。
variable used in lambda
< (λx.x) y, (λx.x) (λx.x)
前者表⽰将函数λx.x应⽤于变量y，得到y；后者表⽰将函数λx.x应⽤于λx.x，得到λx.x。函数λx.x是⼀个恒等函数(identity function)，即输⼊恒等于输出，它可以⽤ I 来表⽰。
这时候可能就有⼈纳闷⼉了，(λx.x) y意义很明确，但λy.xy为什么代表函数抽象⽽不是将函数λy.x应⽤于y的函数应⽤呢？为了消除类似的表达

版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。