同学们啊，Covid20已经到达扭腰。是纽约州长鸠毛说他凭直觉知道的。虽然吧。先暂时将越脏越臭越有人爱搞的穿补和女人的屄忘记一下。假设明天有一个飞碟落在你的窗台上，从里边走出几个拇指大小的外星人。或者黑白无常，牛头马面带着锁链来找你。你怎样与牠们交谈？用什么语言？

摘抄自《维基百科》“λ演算”

λ演算（英语：lambda calculus，λ calculus）是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。

在最简单的lambda演算中，只使用以下的规则来建构lambda项：
语法       名称      描述
============================================================
a             变量        表示参数或数学/逻辑值的字符或字符串。
(λx.M)    抽象化    函数定义（M是一个lambda项）。变量x在表达式中已被绑定。
(M N)     应用        将函数应用于参数。M和N是lambda项。

在λ演算中，每个表达式都代表一个函数，这个函数有一个参数，并且会返回一个值。不论是参数和返回值，也都是一个单参的函数。可以这么说，λ演算中只有一种“类型”，那就是这种单参函数。函数是通过λ表达式匿名地定义的，这个表达式说明了此函数将对其参数进行什么操作。

lambda演算的语法将一些表达式定义为有效的lambda演算式，而某一些表达式无效。

有效的lambda演算式称为“lambda项”。

以下三个规则给出了语法上有效的lambda项，如何建构的归纳定义：

1)变量x本身就是一个有效的lambda项；
2)如果t是一个lambda项，而x是一个变量，则(λx.t)是一个lambda项（称为lambda抽象）；
3)如果t和s是lambda项，那么(ts)是一个lambda项（称为应用）。

其它的都不是lambda项。

在lambda演算中，函数被认为是第一类对象，因此函数可以当作输入，或作为其它函数的输出返回。

形式化定义

形式化地，我们从一个标识符（identifier）的可数无穷集合开始，比如{a,b,c,...,x,y,z,x1,x2,...}，则所有的lambda表达式可以通过下述以BNF范式表达的上下文无关文法描述：

1. <表达式> ::= <标识符>
2. <表达式> ::= (λ<标识符>.<表达式>)
3. <表达式> ::= (<表达式> <表达式>)

头两条规则用来生成函数，而第三条描述了函数是如何作用在参数上的。

（下面的部分我还没读懂，呵呵。想妆屄吓唬我一下的清华北大牛叉人物可要抓紧时间。晚了就错过机会了。）

lambda演算中的算术在lambda演算中有许多方式都可以定义自然数，但最常见的还是邱奇数，下面是它们的定义：

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))

以此类推。

逻辑与谓词

习惯上，下述两个定义（称为邱奇布尔值）被用作TRUE和FALSE这样的布尔值：

TRUE := λx.λy.x
FALSE := λx.λy.y
(注意FALSE等价于前面定义邱奇数零)

通过这两个λ-项，我们可以定义一些逻辑运算：
AND := λp q.p q FALSE
OR := λp q.p TRUE q
NOT := λp.p FALSE TRUE
IFTHENELSE := λp x y.p x y

“谓词”是指返回布尔值的函数。最基本的一个谓词是ISZERO，当且仅当其参数为零时返回真，否则返回假：

ISZERO := λn.n (λx.FALSE) TRUE

运用谓词与上述TRUE和FALSE的定义，使得"if-then-else"这类语句很容易用lambda演算写出。