邱奇编码 是把数据和运算符嵌入到lambda演算 内的一种方式,最常见的形式即邱奇数,它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇 ,他首先以这种方法把数据编码到lambda演算中。
透過邱奇編碼,在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都會被映射到高阶函数 。在無型別lambda演算 ,函數是唯一的原始型別 。
邱奇編碼本身並非用來實踐原始型別,而是透過它來展現我們不須額外原始型別即可表達計算。
很多学数学的学生熟悉可计算函数 集合的哥德尔编号 ;邱奇编码是定义在lambda抽象 而不是自然数上的等价运算。
邱奇数 编辑
邱奇数 為使用邱奇编码的自然数 表示法,而用以表示自然数 n {\displaystyle n} 的高阶函数 是個任意函数 f {\displaystyle f} 映射到它自身的n 重函数复合 之函数,簡言之,數的「值」即等價於參數被函數包裹的次數。
f ∘ n = f ∘ f ∘ ⋯ ∘ f ⏟ n 次 . {\displaystyle f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ 次}}}.\,} 不論邱奇數為何,其都是接受兩個參數的函數。
自 然 數 函 數 定 義 lambda 表 達 式 0 0 f x = x 0 = λ f . λ x . x 1 1 f x = f x 1 = λ f . λ x . f x 2 2 f x = f ( f x ) 2 = λ f . λ x . f ( f x ) 3 3 f x = f ( f ( f x ) ) 3 = λ f . λ x . f ( f ( f x ) ) ⋮ ⋮ ⋮ n n f x = f n x n = λ f . λ x . f ∘ n x {\displaystyle {\begin{array}{r|l|l}{\text{ 自 然 數}}&{\text{函 數 定 義}}&{\text{lambda 表 達 式}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}} 就是说,自然数 n {\displaystyle n} 被表示为邱奇数n ,它对于任何lambda-项F
和X
有着性质:
n F X
=β Fn X
。使用邱奇数的计算 编辑 在 lambda 演算中,数值函数被表示为在邱奇数上的相应函数。这些函数在大多数函数式语言中可以通过 lambda 项的直接变换来实现(服从于类型约束)。
加法函数 plus ( m , n ) = m + n {\displaystyle {\text{plus}}(m,n)=m+n} 利用了恒等式 f ( m + n ) ( x ) = f m ( f n ( x ) ) {\displaystyle f^{(m+n)}(x)=f^{m}(f^{n}(x))} 。
plus ≡ λm.λn.λf.λx. m f (n f x)
后继函数 succ ( n ) = n + 1 {\displaystyle {\text{succ}}(n)=n+1} β-等价于(plus 1 )。
succ ≡ λn.λf.λx. f (n f x)
乘法函数 times ( m , n ) = m × n {\displaystyle {\text{times}}(m,n)=m\times n} 利用了恒等式 f ( m × n ) = ( f m ) n {\displaystyle f^{(m\times n)}=(f^{m})^{n}} 。
mult ≡ λm.λn.λf. n (m f)
指数函数 exp ( m , n ) = m n {\displaystyle \exp(m,n)=m^{n}} 由邱奇数定义直接给出。
exp ≡ λm.λn. n m
前驱函数 pred ( n ) = { 0 if n = 0 , n − 1 otherwise {\displaystyle {\text{pred}}(n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}} 通过生成每次都应用它们的参数 g
于 f
的 n {\displaystyle n} 重函数复合来工作;基础情况丢弃它的 f
复本并返回 x
。
pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)
邱奇數函數一表 编辑 * 注意在邱奇編碼中,
pred ( 0 ) = 0 {\displaystyle \operatorname {pred} (0)=0} m < n → m − n = 0 {\displaystyle m<n\to m-n=0}
除法函式 编辑 以下列定義可實作自然數的除法
n / m = if n ≥ m then 1 + ( n − m ) / m else 0 {\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0} 計算 n {\displaystyle n} 除以 m {\displaystyle m} 的遞迴相減時,將會計算很多次的beta歸約。除非以紙筆手工來做,那麼多步驟倒無關緊要, 但我們不想一直重複瑣碎的歸約;而判別數字是否為零的函式是 IsZero,所以考慮下列條件:
IsZero ( minus n m ) {\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)} 這個判別式相當於 n {\displaystyle n} 小於等於 m {\displaystyle m} 而非 n {\displaystyle n} 小於 m {\displaystyle m} 。如果使用這式子,那麼要將上面給出的除法定義, 轉化為邱奇編碼的自然數函數如下,
divide1 n m f x = ( λ d . IsZero d ( 0 f x ) ( f ( divide1 d m f x ) ) ) ( minus n m ) {\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)} 這樣的定義只呼叫了一次 n {\displaystyle n} 減去 m {\displaystyle m} ,正如我們所想的。然而問題是這式子計算成錯誤的結果, 是 (n-1)/m 除法的商。要更正則需在呼叫 divide 之前把 n {\displaystyle n} 再加回 1。 因此除法的正確定義是,
divide n = divide1 ( succ n ) {\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)} divide1 是一個內含遞迴的定義式,要以 Y 組合子來發生遞迴作用。 所以要再宣告一個名為 div 的新函數;
等號左側為 divide1 → div c 等號右側為 divide1 → c 要獲得
div = λ c . λ n . λ m . λ f . λ x . ( λ d . IsZero d ( 0 f x ) ( f ( c d m f x ) ) ) ( minus n m ) {\displaystyle \operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)} 那麼
divide = λ n . divide1 ( succ n ) {\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)} 而式中所用的其它函式定義如下列:
divide1 = Y div succ = λ n . λ f . λ x . f ( n f x ) Y = λ f . ( λ x . f ( x x ) ) ( λ x . f ( x x ) ) 0 = λ f . λ x . x IsZero = λ n . n ( λ x . false ) true {\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}} true ≡ λ a . λ b . a false ≡ λ a . λ b . b {\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}} minus = λ m . λ n . n pred m pred = λ n . λ f . λ x . n ( λ g . λ h . h ( g f ) ) ( λ u . x ) ( λ u . u ) {\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}} 使用倒斜線 \ 代替 λ 符號,完整的除法函式則如下列,
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))
換成其它表達法 编辑 大部分真實世界的程式語言都提供原生於機器的整數,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 即為一例。
布爾邏輯可以想成二選一,而布尔值則表示为有两个参数的函数,它得到两个参数中的一个:
邱奇布爾值在lambda演算 中的形式定义如下:
true ≡ λ a . λ b . a false ≡ λ a . λ b . b {\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}} 由於真 、假 可以選擇第一個或第二個參數,所以其能夠由組合來產生邏輯運算子。注意到 not 版本因不同求值策略 而有兩個。下列為从邱奇布尔值推导来的布尔算术的函数:
and = λ p . λ q . p q p or = λ p . λ q . p p q not 1 = λ p . λ a . λ b . p b a *1 not 2 = λ p . p ( λ a . λ b . b ) ( λ a . λ b . a ) = λ p . p false true *2 xor = λ a . λ b . a ( not b ) b if = λ p . λ a . λ b . p a b {\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\ ^{\scriptstyle {\text{*1}}}\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \ ^{\scriptstyle {\text{*2}}}\\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}} 註:
1 求值策略使用應用次序時,這個方法才正確。2 求值策略使用正常次序時,這個方法才正確。 下頭為一些範例:
and true false = ( λ p . λ q . p q p ) true false = true false true = ( λ a . λ b . a ) false true = false or true false = ( λ p . λ q . p p q ) ( λ a . λ b . a ) ( λ a . λ b . b ) = ( λ a . λ b . a ) ( λ a . λ b . a ) ( λ a . λ b . b ) = ( λ a . λ b . a ) = true not 1 true = ( λ p . λ a . λ b . p b a ) ( λ a . λ b . a ) = λ a . λ b . ( λ a . λ b . a ) b a = λ a . λ b . ( λ c . b ) a = λ a . λ b . b = false not 2 true = ( λ p . p ( λ a . λ b . b ) ( λ a . λ b . a ) ) ( λ a . λ b . a ) = ( λ a . λ b . a ) ( λ a . λ b . b ) ( λ a . λ b . a ) = ( λ b . ( λ a . λ b . b ) ) ( λ a . λ b . a ) = λ a . λ b . b = false {\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}} 参见 编辑 外部链接 编辑
^ This formula is the definition of a Church numeral n with f -> m, x -> f.