著作權申明：本文為博主窗戶(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))$是可計算的
...
根據數學歸納法， $h$是可計算的， 于是，我們根據復合規則和遞回規則得到的總是可計算函式，從而所有的原始遞回函式都是可計算的，【實作】
我們就用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里，點擊下面圖片
轉載請註明出處，本文鏈接：https://www.uj5u.com/qita/510956.html
標籤：其他
上一篇：分布式存盤系統之Ceph集群狀態獲取及ceph組態檔說明
下一篇：leetcode 889. Construct Binary Tree from Preorder and Postorder Traversal 根據前序和后