无类型lambda演算编程入门

### 无类型 lambda 演算编程入门 在编程的世界里，lambda 演算虽然定义简洁，但其蕴含的强大能力却超乎想象。本文将深入探讨 lambda 演算中的编程示例，包括多参数函数、布尔值、数字表示、递归等内容。 #### 1. 评估策略与 lambda 演算 在讨论类型系统时，评估策略的选择影响不大。各种类型特性背后的问题及解决方法，在不同策略下大致相同。这里采用按值调用策略，因为它在多数知名语言中被使用，且易于添加异常和引用等特性。 #### 2. lambda 演算编程示例 ##### 2.1 多参数函数 lambda 演算本身没有内置对多参数函数的支持，但可借助高阶函数实现相同效果，这种转换称为柯里化（Currying）。 假设我们有一个包含自由变量 `x` 和 `y` 的项 `s`，要定义一个函数 `f`，对于参数对 `(v, w)`，能将 `v` 替换 `x`，`w` 替换 `y` 得到结果。在 lambda 演算中，我们这样定义 `f`： ``` f = λx.λy.s ``` 调用时，依次传入参数，如 `f v w`，它会逐步规约为最终结果。 ##### 2.2 布尔值与条件判断 在 lambda 演算中，布尔值和条件判断也能轻松编码。定义布尔值 `tru` 和 `fls` 如下： ``` tru = λt. λf. t; fls = λt. λf. f; ``` 可以使用 `test` 组合子来测试布尔值的真假： ``` test = λl. λm. λn. l m n; ``` `test b v w` 当 `b` 为 `tru` 时规约为 `v`，为 `fls` 时规约为 `w`。 逻辑与运算符 `and` 可定义为： ``` and = λb. λc. b c fls; ``` **练习 2.2.1**：定义逻辑或和非函数。 ##### 2.3 配对 利用布尔值，可将值对编码为项： ``` pair = λf.λs.λb. b f s; fst = λp. p tru; snd = λp. p fls; ``` `pair v w` 是一个函数，当应用于布尔值 `b` 时，会根据 `b` 的值返回 `v` 或 `w`。 ##### 2.4 丘奇数 丘奇数是用 lambda 项表示数字的一种方式： ``` c0 = λs. λz. z; c1 = λs. λz. s z; c2 = λs. λz. s (s z); c3 = λs. λz. s (s (s z)); ``` 每个数字 `n` 由组合子 `cn` 表示，它接受两个参数 `s` 和 `z`，将 `s` 应用 `n` 次到 `z` 上。 后继函数 `scc` 定义如下： ``` scc = λn. λs. λz. s (n s z); ``` 加法函数 `plus`： ``` plus = λm. λn. λs. λz. m s (n s z); ``` 乘法函数 `times`： ``` times = λm. λn. m (plus n) c0; ``` 判断丘奇数是否为零的函数 `iszro`： ``` iszro = λm. m (λx. fls) tru; ``` 减法相对复杂，使用“前驱函数” `prd`： ``` zz = pair c0 c0; ss = λp. pair (snd p) (plus c1 (snd p)); prd = λm. fst ```