邱奇数
维基百科,自由的 encyclopedia
邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式,最常见的形式即邱奇数,它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇,他首先以这种方法把数据编码到lambda演算中。
透过邱奇编码,在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都会被映射到高阶函数。在无型别lambda演算,函数是唯一的原始型别。
邱奇编码本身并非用来实践原始型别,而是透过它来展现我们不须额外原始型别即可表达计算。