邱奇数

邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式，最常见的形式即邱奇数，它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇，他首先以这种方法把数据编码到lambda演算中。

透過邱奇編碼，在其他符号系统中通常被认定为基本的项（比如整数、布尔值、有序对、列表和tagged unions）都會被映射到高阶函数。在無型別lambda演算，函數是唯一的原始型別。

邱奇編碼本身並非用來實踐原始型別，而是透過它來展現我們不須額外原始型別即可表達計算。

很多学数学的学生熟悉可计算函数集合的哥德尔编号；邱奇编码是定义在lambda抽象而不是自然数上的等价运算。

 用途 

直接实现邱奇编码会将某些访问操作的时间复杂度从降低到（其中是数据结构的大小），这使得该编码方式在实际应用中受到限制。研究表明可以通过针对性优化解决这个问题，但大多数函数式编程语言选择扩展其中间表示以包含代数数据类型。
尽管如此，邱奇编码仍常用于理论论证，因为它在部分求值和定理证明中具有自然表示优势。通过使用高阶类型可以对操作进行类型标注，并能便捷地实现原始递归。由于函数被假定为唯一的原始数据类型，这种设定简化了许多证明过程。

邱奇编码具有表示完整性但仅限于表征层面。需要额外函数将这种表示转换为通用数据类型以供人工解读。由于邱奇定理中等价性不可判定，通常无法判断两个函数是否具有外延等价性。转换过程可能需要通过某种方式应用函数来提取其表征值，或者以λ项字面量的形式查找其值。λ演算通常被解释为使用内涵等价性。由于等价性的内涵定义与外延定义存在差异，在结果解释方面可能存在潜在问题。

邱奇数

邱奇数為使用邱奇编码的自然数表示法，而用以表示自然数的高阶函数是個任意函数映射到它自身的n重函数复合之函数，簡言之，數的「值」即等價於參數被函數包裹的次數。

不論邱奇數為何，其都是接受兩個參數的函數。邱奇数0、1、2、... 在λ演算中的定義如下：

從 0 不應用函數開始， 1 應用函數一次， 2 應用函數兩次， 3 應用函數三次，依此類推：

邱奇数3表示對任意給定函數應用三次的操作。當輸入函數被提供時，首先應用於初始參數，然後連續應用於自身結果。最終結果並非數字3（除非初始參數恰好為0且函數為後繼函數）。邱奇数3的本質是函數的應用次數，而非計算結果本身。其核心意義在於「重複三次」的動作，這正是「三次」概念的直觀體現。

就是说，自然数被表示为邱奇数n，它对于任何lambda-项F和X有着性质：

 n F X =β Fn X。

使用邱奇数的计算

在 lambda 演算中，数值函数被表示为在邱奇数上的相应函数。这些函数在大多数函数式语言中可以通过 lambda 项的直接变换来实现（服从于类型约束）（请参阅将lambda表达式转换为函数）。

加法函数  利用了恒等式 。



后继函数  β-等价于（plus 1）。



乘法函数  利用了恒等式 。



指数函数  通过邱奇数定义给出：将定义中的和代入可得，因此：


对应的lambda表达式为：


前驱函数  的实现较为复杂：



邱奇数通过n次应用函数来运作。前驱函数需要返回一个应用参数n-1次的函数。这通过构建包含f和x的容器来实现，该容器以省略第一次函数应用的方式初始化（详见前驱函数推导）。

基于前驱函数可定义减法函数：


 邱奇數函數一表 

 函數  代數  等同  函數定義 Lambda 表達式 後繼           ... 加法           乘法          指數          前驅        減法        ...  

注意：

 前驱函数推导 

邱奇编码中使用的前驱函数定义为：

为了减少一次函数应用次数来构造前驱函数，需采用容器函数封装值。定义新函数  和  替代原函数和参数，其中容器函数称为。下表左侧展示了邱奇数作用于和的情况：

通用递归规则为：

若定义从容器中提取值的函数：

则可构造同数函数：


通过将替换为特殊容器（该容器首次调用时忽略参数以跳过第一次函数应用），可推导前驱函数：


具体函数定义如下：

最终得到前驱函数的lambda表达式：


 值容器 

值容器将函数作用于其内部值，定义为：

即：

 Inc函数 

 函数需接收包含的容器，返回包含的新容器：

设为值容器：

则：

因此： 提取函数 

通过应用恒等函数提取值：

利用可得：

故：

 Const容器 

为实现函数，需将替换为不应用的容器。该容器需满足：

当满足条件：

对应的lambda表达式为：

 前驱函数的另一种解释 
使用组合子符号可简化前驱函数的解释：





通过下列推导可验证其正确性：




通过eta-归约和归纳法可得：




 前驱函数的另一种定义 
使用序对可定义前驱函数：

此定义虽简洁但展开式较复杂，以为例：

 除法函式 

自然数除法可通过以下方式实现：



计算需要多次beta归约。除非手动进行归约，否则这并不重要，但最好避免重复计算。最简单的数值检测谓词是IsZero，故考虑条件：

此条件等价于而非。若采用该条件，则上述数学定义可转化为邱奇数函数：


此定义仅调用一次，但结果为此公式给出的是的值。

通过给n加1后调用divide可修正该问题，定义式为：


divide1为递归定义，需用Y组合子实现递归。通过以下步骤创建新函数div：
 左側替换：
 右側替换：
得到：


完整定义式为：

其中：




最终展开式：


以文本格式表示（用\代替λ）：
divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))

例如，9/3可表示为：
divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))

使用lambda演算计算器，按正規順序归约后结果为3：
\f.\x.f (f (f (x)))

 有符号数 

通过使用包含正负值的邱奇序对，可将邱奇数扩展至有符号数。整数值即两个邱奇数的差值。

自然数转有符号数的定义为：

取反操作通过交换序对元素实现：

当序对中某一元素为零时，整数表示更自然。OneZero函数确保该条件：

使用Y组合子实现递归：

 加减运算 

加法数学定义为：

对应lambda表达式：

减法定义为：

对应lambda表达式：

 乘除运算 

乘法定义为：

对应lambda表达式：

除法需确保序对元素含零（见上文的OneZero），定义辅助函数：

除法表达式：

 有理数与实数 

有理数可表示为有符号数序对，可计算实数可通过极限过程编码。复数可自然地表示为实数序对。上述数据类型验证了邱奇-图灵论题：任何数据类型或计算均可编码于lambda演算中。

換成其它表達法
大部分真實世界的程式語言都提供原生於機器的整數，church 與 unchurch 函式會在整數及與之對應的邱奇數間轉換。這裡使用Haskell撰寫函式， \ 等同於lambda演算的 λ。 用其它語言表達也會很類似。

type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0

邱奇布尔值

邱奇布尔值是布尔值真和假的邱奇编码形式。某些程式語言使用這個方式來實踐布爾算術的模型，Smalltalk和即為典型示例。

布爾邏輯本質上是選擇機制。邱奇布尔值的编码形式为接收两个参数的函数：
 真（true）選擇第一個參數
 假（false）選擇第二個參數

其标准定义为：


这种编码允许谓词函数（返回逻辑值的函数）直接作为条件语句使用。当布尔函数作用于两个参数时，将根据真值返回其中一个参数：

若predicate-x为真则返回then-clause，否则返回else-clause。

由于真值与假值的选择特性，它们可组合出各类逻辑运算符。需注意逻辑非not存在多种实现方式：


註：
1 求值策略使用應用次序時，這個方法才正確。
2 求值策略使用正常次序時，這個方法才正確。

运算示例解析：



 谓词 

谓词是返回布尔值的函数。最基础的谓词是，当其参数为邱奇数时返回，否则返回：


下列谓词检测第一个参数是否小于等于第二个参数：


基于恒等关系：

相等性检测可定义为：


 邱奇序对 

邱奇序对是二元组的邱奇编码实现。序对被表示为接收函数的函数，当传入参数时会将该参数作用于序对的两个分量。其lambda演算定义为：



示例推导：


 列表编码 

不可变的列表由列表节点构成，其基本操作包括：

 函数  描述 nil  构造空列表 isnil  检测列表是否为空 cons  在列表头部添加元素 head  获取列表首元素 tail  获取列表尾部

以下给出四种不同的列表表示法：
 使用双序对构造列表节点（支持空列表）
 使用单序对构造列表节点
 基于右折叠函数的列表表示
 采用Scott编码的模式匹配参数化表示

 双序对列表节点 

非空列表可用邱奇序对表示：
 First 存储首元素
 Second 存储尾部

为支持空列表，需额外包裹序对形成三层结构：
 First - 空列表标识符
 Second.First 存储首元素
 Second.Second 存储尾部

基于此的核心操作定义如下：

 表达式  描述  序对首元素为true表示空列表  提取空列表标识符  构造非空列表节点 通过second.first获取首元素  通过second.second获取尾部

注意：当列表为空时，head和tail函数不应被调用。

 单序对列表节点 

另一种定义方式PDF版本：：


通用处理模板定义为：


其他扩展操作：








 右折叠列表表示 

作为邱奇序对编码的替代方案，列表可通过其右折叠函数进行编码。例如，包含三个元素x、y、z的列表可编码为高阶函数，当该函数应用组合子c和初始值n时，返回c x (c y (c z n))。这等价于部分应用函数组合链的调用：(c x ∘ c y ∘ c z) n。



此列表表示可在系统F类型系统中定义。

与邱奇数的对应关系并非巧合，邱奇数本质上是单元值列表（如[() () ()]）的一进制编码，列表长度即表示自然数值。对此类列表进行右折叠时，组合函数忽略元素值，其本质与邱奇数中的函数组合链（即(c () ∘ c () ∘ c ()) n = (f ∘ f ∘ f) n）具有等价性。

 Scott编码列表表示 

另一种实现方式是采用了续体的Scott编码，这种方式能生成更简洁的代码（参见）。

该编码的核心思想是利用模式匹配的特性。以Scala语法为例，假设list表示包含空列表Nil和构造器Cons(h, t)的列表类型，可通过模式匹配进行计算：
list match {
  case Nil        => nilCode
  case Cons(h, t) => consCode(h,t)
}
列表的行为由其模式匹配决定，因此可将列表定义为接收nilCode和consCode参数的函数：


设n对应空列表处理参数，c对应非空列表处理参数，则：
空列表定义为：

非空列表（含首元素h和尾部t）定义为：


更一般地，包含种构造器的代数数据类型将被编码为具有个参数的函数。当第个构造器包含个参数时，对应编码参数也接收个参数。

该编码可在无类型λ演算中使用，但带类型版本需支持递归和类型多态的系统。以元素类型E、计算结果类型C的列表为例，其递归类型定义为（"=>"表示函数类型）：
type List =
  C =>                    // 空列表分支
  (E => List => C) =>     // 非空列表分支
  C                       // 模式匹配结果
支持任意计算类型的列表需量化类型C，而泛型列表还需将元素类型E作为类型参数。

参见
Lambda演算
系统F，在有类型lambda演算中的邱奇数

引用

外部链接
Some interactive examples of Church numerals 

Category:Lambda演算
Category:递归论