邱奇编码是把
数据和
运算符嵌入到lambda演算内的一种方式，最常见的形式是邱奇数，它是使用
lambda符号的自然数的表示法。这种方法得名于
阿隆佐·邱奇，他首先以这种方法把数据编码到lambda演算中。
程序简介
邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式，最常见的形式是邱奇数，它是使用lambda符号的自然数的表示法。这种方法得名于阿隆佐·邱奇，他首先以这种方法把数据编码到lambda演算中。
在其他符号系统中通常被认定为基本的项（比如整数、布尔值、有序对、列表和tagged unions）都被映射到使用 邱奇编码的高阶函数；根据邱奇-图灵论题我们知道任何可计算的运算符（和它的运算数）都可以用邱奇编码表示。
很多学数学的学生熟悉可计算函数集合的哥德尔编号；邱奇编码是定义在lambda抽象而不是自然数上的等价运算。
Church数
Church数是在Church编码下的
自然数的表示法。表示自然数n的高阶函数是把任何其他函数f映射到它的n重函数复合的函数。
定义
Church数0, 1, 2, ...在lambda演算中被定义如下：
0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x
...
n F X =β Fn X。
使用Church数的计算
在lambda演算中，数值函数被表示为在Church数上的相应函数。这些函数在大多数函数式语言中可以通过lambda项的直接变换来实现（服从于类型约束）。
加法函数 plus(m,n)=m+n 利用了恒等式 f^{{(m+n)}}(x)=f^{m}(f^{n}(x))。
plus ≡ λm.λn.λf.λx. m f (n f x)
后继函数succ(n)=n+1 β-等价于（plus 1）。
succ ≡ λn.λf.λx. f (n f x)
乘法函数times(m,n)=m*n利用了恒等式 f^{{(m*n)}}=(f^{m})^{n}。
mult ≡ λm.λn.λf. n (m f)
指数函数 exp(m,n)=m^{n}由Church数定义直接给出。
exp ≡ λm.λn. n m
前驱函数 通过生成每次都应用它们的参数g于f的n重函数复合来工作；基础情况丢弃它的f复本并返回x。
pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)
Church布尔值
Church布尔值是布尔值真和假的Church编码。布尔值被表示为两个参数的
函数，它得到这两个参数中的一个。
lambda演算中的形式定义：
true ≡ λa.λb. a
false ≡ λa.λb. b
从Church布尔值推导来的布尔算术的函数：
and ≡ λm.λn.λa.λb. m (n a b) b
or ≡ λm.λn.λa.λb. m a (n a b)
not ≡ λm.λa.λb. m b a