图灵机的逻辑等价形式——lambda演算简介
译者述
才疏学浅，非数学专业，翻译尽量尊重原文，如有纰漏，海涵。
论文摘要
这篇论文是一篇简短易懂的lambda演算介绍。λ-calculus（lambda演算）是Alonzo Church开创，最初是作为研究数学函数的可计算性的相关属性的工具，随着它的流行，其逐渐成为函数编程语言家族强有力的理论基础。这篇简介展示了利用lambda演算如何构建算数和逻辑的数学计算，以及如何定义递归函数（尽管lambda演算子中的函数是匿名的，因此它们不能被显示引用，我们仍然可以定义递归函数）。
1 定义Definition
lambda演算子可以说是世界上最小的通用编程语言。lambda演算子由一个单一转换规则(变量替换，通常被叫做β-conversion，β变换)和一个单一函数定义系统构成。它在1930年代被Alonzo Church作为一个方法引入有效计算能力的概念的形式化中。lambda演算子是通用的，是因为任意可计算函数可以使用此形式表达和求值。因此它等价于图灵机（这也是为什么我费劲翻译原文的原因）。尽管如此，lambda演算子强调的是符号变换规则的使用，却并不关心实际机器是如何实现这些规则的。这是一个更接近软件而不是硬件的方法。
lambda演算子的核心概念是“表达式”（“expression”）。一个“名字”，也被叫做“变量”，是一个标示符，它可以是任意字母a, b, c… 一个表达式可能只是一个名字或者可能是一个函数（function）。函数使用希腊字母λ来来表示函数变量的名字。函数体（body）指定变量名如何排列。身份函数（The identity function），例如：字符串(λx.x）可以代表一个身份函数，字符串中的“λx”告诉我们函数的变量是“x”，“x”是被函数体不做任何改变的返回了。
函数可以被其他的函数使用。比如，函数A被用在了函数B中，可以写为“AB”的形式。注意在本文中，大写的字母被专门用来表示函数。实际上，Lambda演算中任何元素都可是函数，就连数字或者逻辑值都使用可以相互作用的函数来表示，它们是通过符号的字符串转换成另一种符号的字符串达到目的的。所以Lambda演算中没有类型一说，任何函数可以作用于其他函数。开发者的责任是保证计算指令的合理性。
表达式被第归的定义如下：
1 | < expression > := < name >|< function >|< application > |
表达式可以使用括号来包裹以达到清晰表示的目的，比如“E”为一个表达式，”(E)“是等效的（译者加了引号）。另外，这门语言中仅有的两个关键字是”λ “和”.”。为了避免将带括号的表达式混淆，我们约定：函数应用从左边开始关联（左结合），也就是下方的组合表达式：
E 1E 2E 3 . . . E n 可以被下面连续表达式所表示： (…((E 1E 2)E 3) . . . E n)
从 λ表达式的定义可见，一种优雅的函数表现形式是之前出现过的的字符串，带括号或者不带括号：
λx.x ≡ (λx.x)
