$\lambda$演算: 其句法和语义

本书关于纯粹的无类型$\lambda$演算, 而不是$\lambda$演算和类型论, 也不是$\lambda$演算在其他各个领域的应用. 可以说, 我还不具备阅读这本书所需要的maturity, 甚至也没有读这本书的必要, 但我就是想读一读而已.

第1章 引论

第1.1节 lambda演算的各个方面

lambda演算是一种将函数当作规则而不是图的无类型理论. "将函数当作规则"是一种曾经流行的函数概念, 其指的是从参数到值的过程, 这个过程往往是由定义编码的. 将函数视为图 (即参数和值的序对的集合) 的想法通常归功于Dirichlet, 是一项重要的数学贡献. 然而, $\lambda$演算重新将函数视为规则以强调其计算性的方面.

将函数视为规则以全然的一般性考虑问题. 例如, 我们可以考虑由通常的自然语言定义的函数应用于同样由自然语言表述的参数. 或者, 更确切地, 考虑由供机器运行的程序给定的函数应用于其他这样的程序. 在这两种情况下我们都拥有一个无类型的结构, 其中研究的对象同时为函数和参数. 这是无类型$\lambda$演算的起点. 特别地, 一个函数可以被应用于自身. 对于数学中 (或者说Zermelo-Fraenkel集合论中) 的通常函数概念而言, 这是不可能的 (因为基础公理). (也见练习18.5.30)

$\lambda$演算存在三个方面:

1. 数学基础.
2. 计算.
3. 纯lambda演算.

I. 基础和lambda演算

$\lambda$演算和与其相关的组合子逻辑理论的建立者心中拥有两个目的:

• 建立一般的函数理论 (例如, 可以处理公式操作).
• 用逻辑概念扩展理论以提供逻辑和(部分)数学的基础.

不幸的是, 所有这些为数学提供基础的尝试都失败了.