梦的开始
Lambda (/ˈlæmdə/，大写形式 Λ, 小写形式 λ) 是希腊字母表中第十一个字母 [1]。
说起 Calculus，大家更多地会想到微积分。但其实微积分的全称是 “the differential calculus and the integral calculus”，而 calculus 的本意是一个推理的系统 [2]，中国人发明了一个高妙的词来概括它——演算。 其实“演算”和“calculus”都是属于无法直接推出含义的描述，并且也和计算（calculate）看似相关，对于不了解相关领域的同学来说仍然是一头雾水。索性，之后就直接以 λ-Calculus 来称呼它吧。
演算究竟是什么，就不深究了吧。就好像 λ-Calculus 的历史故事虽然很有趣，但作为引入的话总是有一种喧宾夺主的感觉。不过不能不提它的创造者，数学家阿隆佐·邱奇 (Alonzo Church)。
称 λ-Calculus 道生万物，因为它拥有最简洁的符号定义，却足以构建起一个可靠的逻辑系统，似一门晦涩难懂的语言。可若说它只能被相关专业领域的人所理解，那也有失偏颇。我希望在阅读本文的过程中，每位读者都能够感受到 λ-Calculus 的优美和浪漫。但愿以我匮乏的文字表述，能够勉强揭开它潜藏的奥妙。
声明
本站对 λ-Calculus 的叙述主要面向对相关领域（高阶函数、函数式编程、形式验证与自动证明、代数类型系统）不了解的同学，因此很多地方的叙述不够严谨，希望大家多多海涵。也欢迎大家对不妥的部分提出修改意见！