热门问题
时间线
聊天
视角
邱奇数
来自维基百科,自由的百科全书
Remove ads
邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式,最常见的形式即邱奇数,它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇,他首先以这种方法把数据编码到lambda演算中。
透过邱奇编码,在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都会被映射到高阶函数。在无型别lambda演算,函数是唯一的原始型别。
邱奇编码本身并非用来实践原始型别,而是透过它来展现我们不须额外原始型别即可表达计算。
用途
直接实现邱奇编码会将某些访问操作的时间复杂度从降低到(其中是数据结构的大小),这使得该编码方式在实际应用中受到限制。[1]研究表明可以通过针对性优化解决这个问题,但大多数函数式编程语言选择扩展其中间表示以包含代数数据类型。[2] 尽管如此,邱奇编码仍常用于理论论证,因为它在部分求值和定理证明中具有自然表示优势。[1]通过使用高阶类型可以对操作进行类型标注,[3]并能便捷地实现原始递归。[1]由于函数被假定为唯一的原始数据类型,这种设定简化了许多证明过程。
邱奇编码具有表示完整性但仅限于表征层面。需要额外函数将这种表示转换为通用数据类型以供人工解读。由于邱奇定理中等价性不可判定,通常无法判断两个函数是否具有外延等价性。转换过程可能需要通过某种方式应用函数来提取其表征值,或者以λ项字面量的形式查找其值。λ演算通常被解释为使用内涵等价性。由于等价性的内涵定义与外延定义存在差异,在结果解释方面可能存在潜在问题。
Remove ads
邱奇数
邱奇数为使用邱奇编码的自然数表示法,而用以表示自然数的高阶函数是个任意函数映射到它自身的n重函数复合之函数,简言之,数的“值”即等价于参数被函数包裹的次数。
不论邱奇数为何,其都是接受两个参数的函数。邱奇数0、1、2、... 在λ演算中的定义如下:
从 0 不应用函数开始, 1 应用函数一次, 2 应用函数两次, 3 应用函数三次,依此类推:
邱奇数3表示对任意给定函数应用三次的操作。当输入函数被提供时,首先应用于初始参数,然后连续应用于自身结果。最终结果并非数字3(除非初始参数恰好为0且函数为后继函数)。邱奇数3的本质是函数的应用次数,而非计算结果本身。其核心意义在于“重复三次”的动作,这正是“三次”概念的直观体现。
就是说,自然数被表示为邱奇数n,它对于任何lambda-项F
和X
有着性质:
- n
F X
=βFn X
。
Remove ads
在 lambda 演算中,数值函数被表示为在邱奇数上的相应函数。这些函数在大多数函数式语言中可以通过 lambda 项的直接变换来实现(服从于类型约束)(请参阅将lambda表达式转换为函数)。
加法函数 利用了恒等式 。
后继函数 β-等价于(plus 1)。
乘法函数 利用了恒等式 。
指数函数 通过邱奇数定义给出:将定义中的和代入可得,因此:
对应的lambda表达式为:
前驱函数 的实现较为复杂:
邱奇数通过n次应用函数来运作。前驱函数需要返回一个应用参数n-1次的函数。这通过构建包含f和x的容器来实现,该容器以省略第一次函数应用的方式初始化(详见前驱函数推导)。
基于前驱函数可定义减法函数:
Remove ads
总结
视角
注意:
Remove ads
邱奇编码中使用的前驱函数定义为:
为了减少一次函数应用次数来构造前驱函数,需采用容器函数封装值。定义新函数 inc 和 init 替代原函数f和参数x,其中容器函数称为value。下表左侧展示了邱奇数n作用于inc和init的情况:
通用递归规则为:
若定义从容器中提取值的函数extract:
则可构造同数函数samenum:
通过将init替换为特殊容器const(该容器首次调用时忽略参数以跳过第一次函数应用),可推导前驱函数:
具体函数定义如下:
最终得到前驱函数的lambda表达式:
值容器值容器将函数作用于其内部值,定义为: 即: Inc函数inc 函数需接收包含v的容器,返回包含f v的新容器: 设g为值容器: 则: 因此: |
提取函数通过应用恒等函数提取值: 利用I可得: 故: Const容器为实现pred函数,需将init替换为不应用f的const容器。该容器需满足: 当满足条件: 对应的lambda表达式为: |
Remove ads
使用组合子符号可简化前驱函数的解释:
通过下列推导可验证其正确性:
通过eta-归约和归纳法可得:
Remove ads
使用序对可定义前驱函数:
此定义虽简洁但展开式较复杂,以为例:
Remove ads
计算需要多次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)))
Remove ads
通过使用包含正负值的邱奇序对,可将邱奇数扩展至有符号数[5]。整数值即两个邱奇数的差值。
自然数转有符号数的定义为:
取反操作通过交换序对元素实现:
当序对中某一元素为零时,整数表示更自然。OneZero函数确保该条件:
使用Y组合子实现递归:
Remove ads
加法数学定义为:
对应lambda表达式:
减法定义为:
对应lambda表达式:
Remove ads
乘法定义为:
对应lambda表达式:
除法需确保序对元素含零(见上文的OneZero),定义辅助函数:
除法表达式:
Remove ads
有理数可表示为有符号数序对,可计算实数可通过极限过程编码[6][7]。复数可自然地表示为实数序对。上述数据类型验证了邱奇-图灵论题:任何数据类型或计算均可编码于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和Pico即为典型示例。
布尔逻辑本质上是选择机制。邱奇布尔值的编码形式为接收两个参数的函数:
- 真(true)选择第一个参数
- 假(false)选择第二个参数
其标准定义为:
这种编码允许谓词函数(返回逻辑值的函数)直接作为条件语句使用。当布尔函数作用于两个参数时,将根据真值返回其中一个参数:
若predicate-x为真则返回then-clause,否则返回else-clause。
由于真值与假值的选择特性,它们可组合出各类逻辑运算符。需注意逻辑非not存在多种实现方式:
注:
- 1 求值策略使用应用次序时,这个方法才正确。
- 2 求值策略使用正常次序时,这个方法才正确。
运算示例解析:
谓词
谓词是返回布尔值的函数。最基础的谓词是,当其参数为邱奇数时返回,否则返回:
下列谓词检测第一个参数是否小于等于第二个参数:
基于恒等关系:
相等性检测可定义为:
邱奇序对
邱奇序对是二元组的邱奇编码实现。序对被表示为接收函数的函数,当传入参数时会将该参数作用于序对的两个分量。其lambda演算定义为:
示例推导:
列表编码
以下给出四种不同的列表表示法:
- 使用双序对构造列表节点(支持空列表)
- 使用单序对构造列表节点
- 基于右折叠函数的列表表示
- 采用Scott编码的模式匹配参数化表示
非空列表可用邱奇序对表示:
- First 存储首元素
- Second 存储尾部
为支持空列表,需额外包裹序对形成三层结构:
- First - 空列表标识符
- Second.First 存储首元素
- Second.Second 存储尾部
基于此的核心操作定义如下:[8]
注意:当列表为空时,head和tail函数不应被调用。
另一种定义方式[9]:
通用处理模板定义为:
其他扩展操作:
作为邱奇序对编码的替代方案,列表可通过其右折叠函数进行编码。例如,包含三个元素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编码,这种方式能生成更简洁的代码[10](参见摩根森-斯科特编码)。
该编码的核心思想是利用模式匹配的特性。以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
作为类型参数。
参见
外部链接
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads