原始遞迴函數及模擬執行的優化
版權申明：本文為博主窗戶(Colin Cai)原創，歡迎轉帖。如要轉貼，必須註明原文網址 http://www.cnblogs.com/Colin-Cai/p/13499260.html 作者：窗戶 QQ/微信：6679072 E-mail：[email protected]
看到網上一個題目，證明x開y次方是原始遞迴函數(primitive recursive function)。這個問題並不難，只要把x開y次方實現出來即可。於是，正好把《遞迴論》相關內容補一補。
【原始遞迴函數】
首先，我們明確，《遞迴論》裡研究的都是自然數裡的函數。
所謂自然數，在這裡的意思是指非負整數，我們可以用Peano五公理定義。
那麼原題的x開y次方，x和y當然都是自然數，而且應該都是正整數，自然數下x開y次方的結果為實數下x開y次方得到的結果向下取整。當然，為了方便，x取0或者y取0的函數值可以隨便定義。
在講原始遞迴函數之前，我們先要定義幾個基本函數，我們一般稱之為本原函數：
零函數$z$，對於任何自然數，返回0。
後繼函數$s$，對於任何自然數，返回它的後繼數，也就是傳入n返回n+1。
投影函數$p_k^i$，
$p_k^i(a_1,...a_n)=a_i$
以上，零函數和後繼函數都是帶一個元的函數，投影函數可以帶任意多個元(當然，投影函數其實是一堆函數，而不是一個)。
但我們知道，我們平常遇到的自然數下的函數遠遠不止上面這麼點，這就需要不斷的用規則來合成新的函數，用於合成原始遞迴函數的規則有兩個：
複合規則：
一個n元函數$f$和n個m元函數$g_0,...g_n$可以通過以下規則得到一個m元函數
$h(a_0,...a_m)=f(g_0(a_0,...a_m),...g_n(a_0,...a_m))$
遞迴規則:
一個n元函數$f$和一個n+2元函數$g$可以通過以下規則得到一個n+1元函數
$h(a_0,...a_n,0)=f(a_0,...a_n)$
$h(a_0,...a_n,t+1)=g(a_0,...a_n,t,h(a_0,...a_n,t))$
從本原函數開始出發，有限次通過上述規則所得到的函數，就叫原始遞迴函數了。當然，本原函數自己也是原始遞迴函數。
這個原始遞迴函數基本上覆蓋了我們常見的幾乎所有的自然數下的函數了。當然，既然有原始遞迴函數，就有一般遞迴函數了，函數產生規則多了個μ運算元，不過這是本文敘述範圍之外的事情。不過既然提到，說一下，一般認為，一般遞迴函數是可計算的，也就是圖靈機可以解決的(可停機)。我們平常見到的絕大多數自然數下的函數都是原始遞迴函數。
【原始遞迴函數的可計算性】
原始遞迴函數的可計算性很容易證明。
首先，本原函數是可計算的。
然後，我們來看複合規則，如果$f$和$g_0,...g_n$都是可計算的，那麼對於
$h(a_0,...a_m)=f(g_0(a_0,...a_m),...g_n(a_0,...a_m))$
$g_0(a_0,...a_m),...g_n(a_0,...a_m)$都是可計算的，
從而$f(g_0(a_0,...a_m),...g_n(a_0,...a_m))$是可計算的，
從而複合得到的函數$h$是可計算的。
最後，我們來看遞迴規則，如果$f$和$g$是可計算的，
那麼
$h(a_0,...a_n,0)=f(a_0,...a_n)$是可計算的，
$h(a_0,...a_n,1)=g(a_0,...a_n,0,h(a_0,...a_n,0))$是可計算的
...
$h(a_0,...a_n,t+1)=g(a_0,...a_n,t,h(a_0,...a_n,t))$是可計算的
$h(a_0,...a_n,t+2)=g(a_0,...a_n,t+1,h(a_0,...a_n,t+1))$是可計算的
...
【實現】
我們就用Scheme來描述。
零函數z、後繼函數s都很容易實現，
(define (z n) 0) (define (s n) (+ n 1))
而投影函數p則是一堆函數，於是使用p函數來產生投影函數
(define (p k i) (lambda s (list-ref s (- i 1)))))
兩種函數產生規則可以看成是兩個高階函數，寫起來並不複雜，畢竟這只是環境的基礎，複雜的在後面
(define (comb g . h) (lambda s (apply g (map (lambda (f) (apply f s)) h)))) (define (primitive-rec g h) (lambda s (let ((rs (reverse s))) (let ((s2 (reverse (cdr s))) (n (car rs))) (if (zero? n) (apply g s2) (apply h (append s2 (list (- n 1) (apply (primitive-rec g h) (append s2 (list (- n 1))))))))))))
既然目的是為了寫出開方，大致能想的出依次需要造出哪些函數，主方向上大致可以想到比如加法、比較、減法、乘法、乘方以及一些過程中的別的函數。
加法的定義可以這樣：
$a+0=a$
$a+(n+1)=s(a+n)$
顯然，這已經很像用遞迴規則可以寫出的樣子。
改一下上面的遞推式，用符號$\oplus$來表示加法函數，
$add(a,0)=p_1^1(a)$
$add(a,n+1)=s(p_3^3(a,n,add(a,n)))$
為了區別+，我們在Scheme中用+~來表示加法，於是，很容易就寫出程式碼
(define +~ (primitive-rec (p 1 1) (comb s (p 3 3))))
之後，我們Scheme裡構造的函數都加上~來區別。
為了構造減法，我們想先構造一個後繼函數的「相反」函數，前趨函數pre。
定義這個函數用在其他自然數上都是返回傳入值減1，而對於0則返回0.
則定義如下：
$pre(0)=0$
$pre(n+1)=n$
這也很像用一次遞迴規則就可以完成的事，只可惜，無法構造出不帶引數的函數，所以需要一個技巧，先構造一個帶兩元的函數。
$pre2(a,0)=0$
$pre2(a,n+1)=n$
那麼也就是
$pre2(a,0)=z(a)$
$pre2(a,n+1)=p_3^2(a,n,pre2(a,n))$
再用pre2來通過複合規則構造pre函數。
(define pre~ (comb (primitive-rec z (p 3 2)) z (p 1 1)))
有了前趨函數，就可以構造減法。遞迴論的減法有一點不一樣，在於a-b在a<b時等於0。
$sub(a,0)=a$
$sub(a,n+1)=pre(sub(a,n))$
於是
$sub(a,0)=p_1^1(a)$
$sub(a,n+1)=pre(p_3^3(a,n,sub(a,n)))$
寫成程式碼如下：
(define -~ (primitive-rec (p 1 1) (comb pre~ (p 3 3))))
各種謂詞肯定是需要的。
遞迴論裡，我們一般用0、非0來代表假、真。
實現邏輯非和實現之前的pre函數的手法類似，我們先用遞迴規則做一個二元函數，然後再用複合規則。
(define not~ (comb (primitive-rec s (comb z (p 3 1))) z (p 1 1)))
我們可以很聰明的未必要用1來表示真，那麼一切就很得心應手了。
與
$and(a,0)=0$
$and(a,n+1)=a$
或
$or(a,0)=a$
$or(a,n+1)=s(a)$ s是後繼函數
互斥或
$xor(a,0)=a$
$xor(a,n+1)=not(a)$
以上都很容易看出我故意寫成了遞迴規則這樣，於是很容易寫出程式碼
(define and~ (primitive-rec z (p 3 1))) (define or~ (primitive-rec (p 1 1) (comb s (p 3 1)))) (define xor~ (primitive-rec (p 1 1) (comb not~ (p 3 1))))
再寫各種比較謂詞，
大於等於
$ge(a,0)=s(a)$
$ge(a,n+1)=a-n$
大於
$gt(a,0)=a$
$gt(a,n+1)=a-s(n)$
小於
$lt(a,0)=0$
$lt(a,n+1)=s(n)-a$
以上依然用遞迴規則編寫
(define >=~ (primitive-rec s (comb -~ (p 3 1) (p 3 2)))) (define >~ (primitive-rec (p 1 1) (comb -~ (p 3 1) (comb s (p 3 2))))) (define <~ (primitive-rec z (comb -~ (comb s (p 3 2)) (p 3 1))))
而小於等於可以用大於等於通過複合規則構造
$le(a,b)=gt(b,a)$
$=>$
$le(a,b)=gt(p_2^2(a,b),p_2^1(a,b))$
(define <=~ (comb >=~ (p 2 2) (p 2 1)))
也可以構造等於和不等於
$ne(a,b)=or(a-b,b-a)$
等於通過非和不等於兩個謂詞複合得到
$eq(a,b)=not(ne(a,b))$
(define !=~ (comb or~ -~ (comb -~ (p 2 2) (p 2 1)))) (define =~ (comb not~ !=~))
以上這些謂詞對於我們最終的開方來說，大多是不需要的。
乘法是很容易用遞迴規則實現的
$mul(a,0)=0$
$mul(a,n+1)=add(a,mul(a,n))$
(define *~ (primitive-rec z (comb + (p 3 1) (p 3 3))))
有了乘法，乘方也一樣(我們不考慮0為底)
$pow(a,0)=1$
$pow(a,n+1)=mul(a,pow(a,n))$
(define pow (primitive-rec (comb s z) (comb * (p 3 1) (p 3 3))))
最後，我們就可以構造開方了。想到的構造開方的方式有很多種，以下選擇一種，
我們取$root(0,n)=0$
根據
$root(m+1,n)\le root(m,n)+1$
將$root$函數的兩個引數交換為$rootv$
可以用遞迴規則來構造$rootv$，
$rootv(a,0)=0$
$rootv(a,n+1)=if\ {(rootv(a,n)+1)}^{a} \le n+1\ then\ rootv(a,n)+1\ else\ rootv(a,n)$
我們給if-else做個函數，叫condch
$condch(a,b,0)=b$
$condch(a,b,n+1)=a$ 此時第三個引數為非0
(define condch~ (primitive-rec (p 2 2) (p 4 1)))
於是，重新整理$rootv$
$rootv(a,0)=z(a)$
$rootv(a,n+1)=condch(s(rootv(a,n)),rootv(a,n),le(expt(s(rootv(a,n))),s(n)))$
再交換一下兩個引數，當然用的是複合規則，得到$root$函數
寫成程式碼
(define root~ (comb (primitive-rec z (comb condch~ (comb s (p 3 3)) (p 3 3) (comb <=~ (comb pow~ (comb s (p 3 3)) (p 3 1)) (comb s (p 3 2))))) (p 2 2) (p 2 1)))
到這裡為止，我們已經用原始遞迴函數的構造方式實現了開方，當然證明了開方運算是原始遞迴函數。
再拿程式測試了幾下，數比較小的時候，結果都是對的，數稍微大一點計算量很大就算了。
【優化】
以上的運算效率很慢，一個原因在於運算方式。
比如投影函數，雖然是從幾個數中選擇一個，明明對於純函數來說，不選擇的幾個數去計算是多餘的，但基於Lisp的運算規則限制，這是必須要先算的。
遞迴規則中，也會帶來相同的問題。
以上問題導致了絕大部分的無意義計算，從而使得運算速度非常緩慢。
一種思路是運算的時候再加個call函數，按之前，z、s、p、comb、primitive-rec都為產生函數的實現下，call函數應該如下:
(define (call f . s) (apply f s))
而此處，加了一個call就給了優化無限的可能。我們可以換一條思路來實現上面的z、s、p、comb、primitive-rec，引入優化，比如z、s、p、comb、primitive-rec拼成資料結構來代表計算。
(define z 'z) (define s 's) (define p (lambda (k i) `(p ,k ,i))) (define (comb . fs) `(comb ,@fs)) (define (primitive-rec g h) `(rec ,g ,h)
比如之前的(define +~ (primitive-rec (p 1 1) (comb s (p 3 3))))
+~就是list結構，(rec (p 1 1) (comb s (p 3 3)))
然後call函數再來對這樣的list來進行優化，產生較高效的計算方式。
我這裡是再call函數裡先將上述的list轉換成lambda表示式，然後再對lambda表示式進行優化。
(define (call f . s) (apply (eval (func->lambda f)) s))
這裡的func->lambda則是包含了轉換為lambda表示式以及對lambda表示式的優化。優化一般以pass的方式，依次進行，每個pass只做一件事情。迴圈進行，到無法改變程式碼的時候結束。
(define (optimize s)
(let ((passes (list
;...all optimization passes
)))
(do
((r s (fold-left
(lambda (r pass)
(pass r))
r
passes))
(r-old '() r))
((equal? r-old r)
r))))
本想寫出Knuth's up arrow的表示的(雖然計算就不指望了)，帶三個引數，
用 k(a, b, c)來代表
a ↑...↑ b
箭頭個數為c
但感覺寫不出，懷疑它不是原始遞迴函數，可惜不會證明，哪位大佬看到給個證明吧。
原始碼放在github裡，點選下面圖片
