丘奇编码

定义

丘奇编码(Church Encoding)是 Alonzo Church 提出的一种技术,用纯 λ 演算中的函数来表示数据:自然数、布尔值、序对、列表等都被编码为高阶函数,从而证明纯函数系统足以表达一切数据结构。

原理

丘奇数把自然数 n 表示为"把函数 f 应用 n 次"的高阶函数:0 = λf.λx.x,1 = λf.λx.f x,2 = λf.λx.f (f x)。加法、乘法等运算随之定义为对这些函数的组合。布尔值则编码为二选一的选择函数:true = λa.λb.a,false = λa.λb.b,if 语句即函数应用。

意义

丘奇编码表明"数据"与"操作数据的方式"可以统一为函数,是可计算性理论的重要构造,也启发了面向对象消息传递与访问者模式等设计。

相关

后续发展出 Scott 编码等变体,在归约效率与模式匹配表达上各有取舍;在 System F 中丘奇编码还与多态类型精确对应。