Feng.Li's Java See

          抓緊時間,大步向前。
          隨筆 - 95, 文章 - 4, 評論 - 58, 引用 - 0
          數(shù)據(jù)加載中……

          精解遞歸程序設計

           

           

          理解遞歸,以編寫可維護的、一致的、保證正確的代碼

          Jonathan Bartlett
          技術主管, New Media Worx
          2005 年 7 月 11 日

          命令式語言開發(fā)人員并不經(jīng)常使用遞歸這一工具,因為他們認為這樣會較慢而且浪費空間,不過,作者通過示例表明,可以使用一些技術來盡減少或者避免這些問題。他介紹了遞歸以及遞歸程序設計模式的概念,研究了如何使用它們來編寫保證正確的程序。示例是使用 Scheme 和 C 編寫的。

          計算機科學的新學生通常難以理解遞歸程序設計的概念。遞歸思想之所以困難,原因在于它非常像是循環(huán)推理(circular reasoning)。它也不是一個直觀的過程;當我們指揮別人做事的時候,我們極少會遞歸地指揮他們。

          對剛開始接觸計算機編程的人而言,這里有遞歸的一個簡單定義:當函數(shù)直接或者間接調(diào)用自己時,則發(fā)生了遞歸。

          遞歸的經(jīng)典示例
          計算階乘是遞歸程序設計的一個經(jīng)典示例。計算某個數(shù)的階乘就是用那個數(shù)去乘包括 1 在內(nèi)的所有比它小的數(shù)。例如,factorial(5) 等價于 5*4*3*2*1,而 factorial(3) 等價于 3*2*1。

          階乘的一個有趣特性是,某個數(shù)的階乘等于起始數(shù)(starting number)乘以比它小一的數(shù)的階乘。例如,factorial(5) 與 5 * factorial(4) 相同。您很可能會像這樣編寫階乘函數(shù):

          清單 1. 階乘函數(shù)的第一次嘗試

                      int factorial(int n)

                      {

                      return n * factorial(n - 1);

                      }

                     

          不過,這個函數(shù)的問題是,它會永遠運行下去,因為它沒有終止的地方。函數(shù)會連續(xù)不斷地調(diào)用 factorial。當計算到零時,沒有條件來停止它,所以它會繼續(xù)調(diào)用零和負數(shù)的階乘。因此,我們的函數(shù)需要一個條件,告訴它何時停止。

          由于小于 1 的數(shù)的階乘沒有任何意義,所以我們在計算到數(shù)字 1 的時候停止,并返回 1 的階乘(即 1)。因此,真正的遞歸函數(shù)類似于:

          清單 2. 實際的遞歸函數(shù)

                      int factorial(int n)

                      {

                      if(n == 1)

                      {

                      return 1;

                      }

                      else

                      {

                      return n * factorial(n - 1);

                      }

                      }

                     

          可見,只要初始值大于零,這個函數(shù)就能夠終止。停止的位置稱為 基線條件(base case)。基線條件是遞歸程序的最底層位置,在此位置時沒有必要再進行操作,可以直接返回一個結果。所有遞歸程序都必須至少擁有一個基線條件,而且必須確保它們最終會達到某個基線條件;否則,程序?qū)⒂肋h運行下去,直到程序缺少內(nèi)存或者棧空間。

          遞歸程序的基本步驟
          每一個遞歸程序都遵循相同的基本步驟:

          1. 初始化算法。遞歸程序通常需要一個開始時使用的種子值(seed value)。要完成此任務,可以向函數(shù)傳遞參數(shù),或者提供一個入口函數(shù),這個函數(shù)是非遞歸的,但可以為遞歸計算設置種子值。
          2. 檢查要處理的當前值是否已經(jīng)與基線條件相匹配。如果匹配,則進行處理并返回值。
          3. 使用更小的或更簡單的子問題(或多個子問題)來重新定義答案。
          4. 對子問題運行算法。
          5. 將結果合并入答案的表達式。
          6. 返回結果。

          使用歸納定義
          有時候,編寫遞歸程序時難以獲得更簡單的子問題。不過,使用 歸納定義的(inductively-defined)數(shù)據(jù)集 可以令子問題的獲得更為簡單。歸納定義的數(shù)據(jù)集是根據(jù)自身定義的數(shù)據(jù)結構 —— 這叫做 歸納定義(inductive definition)

          例如,鏈表就是根據(jù)其本身定義出來的。鏈表所包含的節(jié)點結構體由兩部分構成:它所持有的數(shù)據(jù),以及指向另一個節(jié)點結構體(或者是 NULL,結束鏈表)的指針。由于節(jié)點結構體內(nèi)部包含有一個指向節(jié)點結構體的指針,所以稱之為是歸納定義的。

          使用歸納數(shù)據(jù)編寫遞歸過程非常簡單。注意,與我們的遞歸程序非常類似,鏈表的定義也包括一個基線條件 —— 在這里是 NULL 指針。由于 NULL 指針會結束一個鏈表,所以我們也可以使用 NULL 指針條件作為基于鏈表的很多遞歸程序的基線條件。

          鏈表示例
          讓我們來看一些基于鏈表的遞歸函數(shù)示例。假定我們有一個數(shù)字列表,并且要將它們加起來。履行遞歸過程序列的每一個步驟,以確定它如何應用于我們的求和函數(shù):

          1. 初始化算法。這個算法的種子值是要處理的第一個節(jié)點,將它作為參數(shù)傳遞給函數(shù)。
          2. 檢查基線條件。程序需要檢查確認當前節(jié)點是否為 NULL 列表。如果是,則返回零,因為一個空列表的所有成員的和為零。
          3. 使用更簡單的子問題重新定義答案。我們可以將答案定義為當前節(jié)點的內(nèi)容加上列表中其余部分的和。為了確定列表其余部分的和,我們針對下一個節(jié)點來調(diào)用這個函數(shù)。
          4. 合并結果。遞歸調(diào)用之后,我們將當前節(jié)點的值加到遞歸調(diào)用的結果上。

          下面是這個函數(shù)的偽代碼和實際代碼:

          清單 3. sum_list 程序的偽代碼

                       function sum_list(list l)

                      is l null?

                      yes - the sum of an empty list is 0 - return that

                      data = head of list l

                      rest_of_list = rest of list l

                      the sum of the list is:

                      data + sum_list(rest_of_list)

                     

          這個程序的偽代碼幾乎與其 Scheme 實現(xiàn)完全相同。

          清單 4. sum_list 程序的 Scheme 代碼

                       (define sum-list (lambda (l)

                      (if (null? l)

                      0

                      (let (

                      (data (car l))

                      (rest-of-list (cdr l)))

                      (+ data (sum-list rest-of-list))))))

                      

          對于這個簡單的示例而言,C 版本同樣簡單。

          清單 5. sum_list 程序的 C 代碼

                      int sum_list(struct list_node *l)

                      {

                      if(l == NULL)

                      return 0;

                      return l.data + sum_list(l.next);

                      }

                     

          您可能會認為自己知道如何不使用遞歸編寫這個程序,使其執(zhí)行更快或者更好。稍后我們會討論遞歸的速度和空間問題。在此,我們繼續(xù)討論歸納數(shù)據(jù)集的遞歸。

          假定我們擁有一個字符串列表,并且想要知道某個特定的字符串是否包含在那個列表中。將此問題劃分為更簡單的問題的方法是,再次到單個的節(jié)點中去查找。

          子問題是這樣:“搜索字符串是否與 這個節(jié)點 中的字符串相同?”如果是,則您就已經(jīng)有了答案;如果不是,則更接近了一步。基線條件是什么?有兩個:

          • 如果當前節(jié)點擁有那個字符串,則那就是基線條件(返回“true”)。
          • 如果列表為空,則那也是基線條件(返回“false”)。

          這個程序不是總能達到第一個基線條件,因為不是總會擁有正在搜索的字符串。不過,我們可以斷言,如果程序不能達到第一個基線條件,那么當它到達列表末尾時至少能達到第二個基線條件。

          清單 6. 確定給定的列表中是否包含給定字符串的 Scheme 代碼

                      (define is-in-list

                      (lambda   (the-list the-string)

                      ;;Check for base case of "list empty"

                      (if (null? the-list)

                      #f

                      ;;Check for base case of "found item"

                      (if (equal? the-string (car the-list))

                      #t

                      ;;Run the algorithm on a smaller problem

                      (is-in-list (cdr the-list) the-string)))))

                     

          這個遞歸函數(shù)能很好地工作,不過它有一個主要的缺點 —— 遞歸的每一次迭代都要為 the-string 傳遞 相同的值。傳遞額外的參數(shù)會增加函數(shù)調(diào)用的開銷。

          不過,我們可以在函數(shù)的起始處設置一個閉包(closure),以使得不再必須為每一個調(diào)用都傳遞那個字符串:

          清單 7. 使用閉包的搜索字符串的 Scheme 程序

                       (define is-in-list2

                      (lambda (the-list the-string)

                      (letrec

                      (

                      (recurse (lambda (internal-list)

                      (if (null? internal-list)

                      #f

                      (if (equal? the-string (car internal-list))

                      #t

                      (recurse (cdr internal-list)))))))

                      (recurse the-list))))

                     

          這個版本的程序稍微難以理解。它定義了一個名為 recurse 的閉包,能夠只使用一個參數(shù)來調(diào)用它,而不是兩個。(要獲得關于閉包的更多資料,請參閱 參考資料。)我們不必將 the-string 傳遞給 recurse,因為它已經(jīng)在父環(huán)境(parent environment)中,而且從一個調(diào)用到另一個調(diào)用時不會改變。由于 recurse 是在 is-in-list2 的 內(nèi)部 定義的,所以它可以訪問所有當前定義的變量,因而不必重新傳遞它們。這就避免了在每一次迭代時都要傳遞一個變量。

          在這個微不足道的示例中,使用閉包來代替參數(shù)傳遞并沒有太多區(qū)別,不過,在更為復雜的函數(shù)中,這樣可以減少很多鍵盤輸入、很多錯誤以及傳遞參數(shù)中引入的很多開銷。

          這個示例中所使用的生成遞歸閉包的方法有些冗長。在遞歸程序設計中,要一次又一次地以相同的模式使用 letrec 創(chuàng)建遞歸閉包,并使用一個初始種子值來調(diào)用它。

          為了讓編寫遞歸模式更為簡單,Scheme 使用一個名為 命名 let(named let) 的快捷方法。這種快捷方法看起來非常像是一個 let,只是整個程序塊會被給定一個名稱,這樣可以將它作為一個遞歸閉包去調(diào)用。使用命名 let 所構建的函數(shù)的參數(shù)定義與普通的 let 中的變量類似;初始種子值的設置方式也與普通的 let 中初始變量值的設置方式相同。從那里開始,每一次后續(xù)的遞歸調(diào)用都使用那些參數(shù)作為新的值。

          命名 let 的內(nèi)容討論起來相當費解,所以來看下面的代碼,并將其與清單 7 中的代碼相比較。

          清單 8. 命名 let 示例

                      (define is-in-list2

                      (lambda (the-list the-string)

                      ;;Named Let

                      ;;This let block defines a function called "recurse" that is the

                      ;;body of this let. The function's parameters are the same as

                      ;;the variables listed in the let.

                      (let recurse

                      ;;internal-list is the first and only parameter. The

                      ;;first time through the block it will be primed with

                      ;;"the-list" and subsequent calls to "recurse" will

                      ;;give it whatever value is passed to "recurse"

                      ( (internal-list the-list) )

                      ;;Body of function/named let block

                      (if (null? internal-list)

                      #f

                      (if (equal? the-string (car internal-list))

                      #t

                      ;;Call recursive function with the

                      ;;rest of the list

                      (recurse (cdr internal-list)))))))

                     

          在編寫遞歸函數(shù)時,命名 let 能夠相當程度地減少鍵盤輸入以及出現(xiàn)錯誤的數(shù)量。如果您理解命名 let 的概念仍有困難,那么我建議您對上面的兩個程序中的每一行進行全面的比較(另外參閱本文 參考資料 部分中的一些文檔)。

          我們的下一個基于列表的遞歸函數(shù)示例要稍微復雜一些。它將檢查列表是否以升序排序。如果列表是以升序排序,則函數(shù)返回 #t;否則,它將返回 #f。這個程序稍有不同,因為除了必須要考查當前的值以外,我們還必須記住處理過的最后一個值。

          對列表中第一項的處理必須與其他項不同,因為沒有在它之前的任何項。對于其余的項,我們需要將先前考查的值傳遞到函數(shù)調(diào)用中。函數(shù)類似如下:

          清單 9. 確定列表是否以升序排序的 Scheme 程序

                      (define is-ascending

                      (lambda (the-list)

                      ;;First, Initialize the algorithm. To do this we

                      ;;need to get the first value, if it exists, and

                      ;;use it as a seed to the recursive function

                      (if (null? the-list)

                      #t

                      (let is-ascending-recurse

                      (

                      (previous-item (car the-list))

                      (remaining-items (cdr the-list))

                      )

                      ;;Base case #1 - end of list

                      (if (null? remaining-items)

                      #t

                      (if (< previous-item (car remaining-items))

                      ;;Recursive case, check the rest of the list

                      (is-ascending-recurse (car remaining-items) (cdr remaining-items))

                      ;;Base case #2 - not in ascending order

                      #f))))))

                     

          這個程序首先檢查邊界條件 —— 列表是否為空。空列表被認為是升序的。然后程序以列表中的第一項及其余部分列表為種子開始遞歸函數(shù)。

          然后檢查基線條件。能到達列表末尾的惟一情形是此前所有項都按順序排列,所以,如果某個列表為空,則列表為升序。否則,我們?nèi)z查當前項。

          如果當前項是升序的,那么我們接下來只需要解決問題的一個子集 —— 列表的其余部分是否為升序。所以我們遞歸處理列表其余部分,并再次嘗試。

          注意在函數(shù)中我們是如何通過向前傳遞程序來保持函數(shù)調(diào)用過程中的狀態(tài)的。以前我們每次只是傳遞了列表的剩余部分。不過,在這個函數(shù)中,我們需要了解關于計算狀態(tài)的稍多些內(nèi)容。當前計算的結果依賴于之前的部分結果,所以,在每次后續(xù)遞歸調(diào)用中,我們向前傳遞那些結果。對更復雜的遞歸過程來說這是一個通用的模式。

          編寫保證正確的程序
          bug
          是每位程序員日常生活的一部分,因為就算是最小的循環(huán)和最簡單的函數(shù)調(diào)用之中也會有 bug。盡管大部分程序員能夠檢查代碼并測試代碼的 bug,但他們并不知道如何證明他們的程序?qū)此麄兯O想的那樣去執(zhí)行。出于此方面的考慮,我們接下來研究 bug 的一些常見來源,然后闡述如何編寫正確的程序以及如何證明其正確性。

          bug 來源:狀態(tài)改變
          變量狀態(tài)改變是產(chǎn)生 bug 的一個主要來源。您可能會認為,程序能敏銳地確切知道變量何時如何改變狀態(tài)。有時在簡單的循環(huán)中的確如此,不過在復雜的循環(huán)中通常不是這樣。通常在循環(huán)中給定的變量能夠以多種方式改變狀態(tài)。

          例如,如果您擁有一個復雜的 if 語句,有些分支可能會修改某個變量,而其他分支可能會修改其他變量。此外,順序通常很重要,但是難以絕對保證在所有情形下編碼的次序都是正確的。通常,由于這些順序問題,為某一情形修改某個 bug 會為其他情形引入 bug。

          為了預防此類錯誤,開發(fā)人員需要能夠:

          • 預先斷定每個變量如何獲得其當前值。
          • 確保變量都沒有雙重用途。(很多程序員經(jīng)常使用同一變量來存儲兩個相關但稍有不同的值。)
          • 當循環(huán)重新開始時,確保所有的變量都處于它們應該處于的狀態(tài)。(在極少使用和測試的不重要情形中疏忽了為循環(huán)變量設置新值,這是常見的程序設計錯誤。)

          為了達成這些目標,我們只需要在程序設計中制定一個規(guī)則:一個變量只賦值一次,而且永遠不再修改它!

          什么?(您說得不可信!)這個規(guī)則對很多人來說不可接受,他們所熟知的是命令式、過程式和面向?qū)ο蟪绦蛟O計 —— 變量賦值與修改是這些程序設計技術的基礎!盡管如此,對命令式語言程序員來說,狀態(tài)的改變依然是程序設計錯誤的主要原因。

          那么,編程時如何才能不修改變量?讓我們來研究一些經(jīng)常要修改變量的情形,并研究我們是否能夠不修改變量而完成任務:

          • 重新使用某個變量。
          • 變量的條件修改(conditional modification)。
          • 循環(huán)變量。

          我們先來研究第一種情形,重新使用某個變量。通常會出于不同的(但是類似的)目的而重新使用某個變量。例如,有時候,循環(huán)的某個部分中,在循環(huán)的前半部分需要一個指向當前位置的索引,而循環(huán)的其余部分需要一個恰在此索引之前或之后的索引,很多程序員為這兩種情況使用同一變量,而只是根據(jù)情況對其進行增量處理。當前程序被修改時,這無疑會令程序員難以理解這兩種用途。為了預防這一問題,最好的解決方案是創(chuàng)建兩個單獨的變量,并以同樣的方法根據(jù)第一個變量得出第二個變量,就像是寫入同一變量那樣。

          第二種情形,即變量的條件修改,是重新使用的問題的一個子集,只是有時我們會保持現(xiàn)有的值,有時需要使用一個新值。同樣,最好創(chuàng)建一個新的變量。在大部分語言中,我們可以使用三元運算符 ? : 來設置新變量的值。例如,如果我們需要為新變量賦一個新值,條件是它不大于 some_value,我們可以這樣寫 int new_variable = old_variable > some_value ? old variable : new_value;。

          (我們將在本文中稍后討論循環(huán)變量。)

          當我們解決了所有變量狀態(tài)改變的問題后,就可以確信,當我們第一次定義變量時,變量的定義在函數(shù)整個生存期間都會保持。這使得操作的順序簡單了很多,尤其是當修改已有代碼時。您不必關心變量被修改的順序,也不必關心在每一個時刻關于其狀態(tài)要做什么假定。

          當變量的狀態(tài)不能改變時,在聲明它的時刻和地方就給出了其起源的完全定義。您再也不用搜索全部代碼去找出不正確的或者混亂的狀態(tài)。

          什么是循環(huán)變量?
          現(xiàn)在,問題是如何不通過賦值來進行循環(huán)?答案是 遞歸函數(shù)。在表 1 中了解循環(huán)的特性,看它們可以如何與遞歸函數(shù)的特性相對比。

          表 1. 對比循環(huán)與遞歸函數(shù)

          特性

          循環(huán)

          遞歸函數(shù)

          重復

          為了獲得結果,反復執(zhí)行同一代碼塊;以完成代碼塊或者執(zhí)行 continue 命令信號而實現(xiàn)重復執(zhí)行。

          為了獲得結果,反復執(zhí)行同一代碼塊;以反復調(diào)用自己為信號而實現(xiàn)重復執(zhí)行。

          終止條件

          為了確保能夠終止,循環(huán)必須要有一個或多個能夠使其終止的條件,而且必須保證它能在某種情況下滿足這些條件的其中之一。

          為了確保能夠終止,遞歸函數(shù)需要有一個基線條件,令函數(shù)停止遞歸。

          狀態(tài)

          循環(huán)進行時更新當前狀態(tài)。

          當前狀態(tài)作為參數(shù)傳遞。

          可見,遞歸函數(shù)與循環(huán)有很多類似之處。實際上,可以認為循環(huán)和遞歸函數(shù)是能夠相互轉換的。區(qū)別在于,使用遞歸函數(shù)極少被迫修改任何一個變量 —— 只需要將新值作為參數(shù)傳遞給下一次函數(shù)調(diào)用。這就使得您可以獲得避免使用可更新變量的所有益處,同時能夠進行重復的、有狀態(tài)的行為。

          將一個常見的循環(huán)轉化為遞歸函數(shù)
          讓我們來研究一個打印報表的常見循環(huán),了解如何將它轉化為一個遞歸函數(shù)。

          • 這個循環(huán)將在每一個分頁處打印出頁編號和頁眉。
          • 假定報告的行依照某個數(shù)字標準分組,并假定有用來了解這些組的一個總數(shù)。
          • 在每一組的最后,打印出組的總數(shù)。

          出于演示目的,我們略去了所有次要的函數(shù),假定它們存在而且按預期執(zhí)行。下面是我們的報告打印程序的代碼:

          清單 10. 用普通循環(huán)實現(xiàn)的報告打印程序

                      void print_report(struct report_line *report_lines, int num_lines)

                      {

                      int num_lines_this_page = 0;

                      int page_number = 1;

                      int current_line; /* iterates through the lines */

                      int current_group = 0; /* tells which grouping we are in */

                      int previous_group = 0; /* tells which grouping was here on the last loop */

                      int group_total = 0; /* saves totals for printout at the end of the grouping */

                      print_headings(page_number);

                      for(current_line = 0; current_line < num_lines; current_line++)

                      {

                      num_lines_this_page++;

                      if(num_lines_this_page == LINES_PER_PAGE)

                      {

                      page_number++;

                      page_break();

                      print_headings(page_number);

                      }

                      current_group = get_group(report_lines[current_line]);

                      if(current_group != previous_group)

                      {

                      print_totals_for_group(group_total);

                      group_total = 0;

                      }

                      print_line(report_lines[current_line]);

                      group_total += get_line_amount(report_lines[current_line]);

                      }

                      }

                     

          程序中故意留了一些 bug。看您是否能夠找出它們。

          由于我們要不斷地修改狀態(tài)變量,所以難以預見在任意特定時刻它們是否正確。下面是遞歸實現(xiàn)的同一程序:

          清單 11. 使用遞歸實現(xiàn)的報告打印程序

                      void print_report(struct report_line *report_lines, int num_lines)

                      {

                      int num_lines_this_page = 0;

                      int page_number = 1;

                      int current_line; /* iterates through the lines */

                      int current_group = 0; /* tells which grouping we are in */

                      int previous_group = 0; /* tells which grouping was here on the last loop */

                      int group_total = 0; /* saves totals for printout at the end of the grouping */

                      /* initialize */

                      print_headings(page_number);

                      /* Seed the values */

                      print_report_i(report_lines, 0, 1, 1, 0, 0, num_lines);

                      }

                      void print_report_i(struct report_line *report_lines, /* our structure */

                      int current_line, /* current index into structure */

                      int num_lines_this_page, /* number of lines we've filled this page */

                      int page_number,

                      int previous_group, /* used to know when to print totals */

                      int group_total, /* current aggregated total */

                      int num_lines) /* the total number of lines in the structure */

                      {

                      if(current_line == num_lines)

                      {

                      return;

                      }

                      else

                      {

                      if(num_lines_this_page == LINES_PER_PAGE)

                      {

                      page_break();

                      print_headings(page_number + 1);

                     print_report_i(

                      report_lines,

                      current_line,

                      1,

                      page_number + 1,

                      previous_group,

                      group_total,

                      num_lines);

                      }

                      else

                      {

                      int current_group = get_group(report_lines[current_line]);

                      if(current_group != previous_group && previous_group != 0)

                      {

                      print_totals_for_group(group_total);

                      print_report_i(

                      report_lines,

                      current_line,

                      num_lines_this_page + 1,

                      page_number,

                      current_group,

                      0,

                      num_lines);

                      }

                      else

                      {

                      print_line(report_lines[current_line]);

                      print_report_i(

                      report_lines,

                      current_line + 1,

                      num_lines_this_page + 1,

                      page_number,

                      current_group,

                      group_total + get_line_amount(report_lines[current_line]),

                      num_lines);

                      }

                      }

                      }

                      }

                     

          注意,我們所使用的所有數(shù)字都是始終一致的。幾乎在任何情形下,只要修改多個狀態(tài),在狀態(tài)改變過程中就會有一些代碼行中將不能擁有始終一致的數(shù)字。如果以后向程序中此類改變狀態(tài)的代碼中添加一行,而對變量狀態(tài)的判斷與實際情況不相匹配,那么將會遇到很大的困難。這樣修改幾次以后,可能會因為順序和狀態(tài)問題而引入難以捉摸的 bug。在這個程序中,所有狀態(tài)改變都是通過使用完全前后一致的數(shù)據(jù)重新運行遞歸程序而實現(xiàn)的。

          遞歸的報告打印程序的證明
          由于從來沒有改變變量的狀態(tài),所以證明您的程序非常簡單。讓我們來研究關于清單 11 中報告打印程序的一些特性證明。

          提示那些大學畢業(yè)后沒有進行過程序證明的人(或者可能從來沒有進行過),進行程序證明,基本上就是尋找程序的某個特性(通常指定為 P),并證明那個特性適用。要完成此任務需要使用:

          • 公理(axioms),假定的真理。
          • 定理(theorems) 由公理推論得到的關于程序的陳述。

          目標是將公理與定理聯(lián)合起來證明特性 P 為真。如果程序有不只一個特性,則通常分別去證明每一個。由于這個程序有若干個特性,我們將為其中一些給出簡短的證明。

          由于我們在進行不正式的證明,所以我不會為所使用的公理命名,也不會嘗試去證明那些用來令證明有效的中間定理。但愿它們足夠明顯,以致不必對它們進行證明。

          在證明過程中,我將把程序的三個遞歸點分別稱為 R1、R2 和 R3。所有程序都有一個隱式的假設:report_lines 為合法的指針,且 num_lines 準確地反映 report_lines 所顯示的行數(shù)。

          在示例中,我將嘗試去證明:

          • 任意給定的一組行,程序都能終止。
          • 在 LINES_PER_PAGE 行之后會發(fā)生分頁。
          • 每一個報告項都嚴格只打印一次。

          證明程序會終止
          此證明將確認對于任意給定的一組行,程序都會終止。這個證明將使用一種在遞歸程序中常見的證明技術,名為 歸納證明(inductive proof)

          歸納證明由兩個步驟構成。首先,需要證明特性 P 對于給定的一組參數(shù)是適用的。然后去證明一個歸納,表明如果 P 對于 X 的值適用,那么它對于 X + 1(或者 X - 1,或者任意類型的步進處理)的值也必須適用。通過這種方法您就可以證明特性 P 適用于從已經(jīng)證明的那個數(shù)開始依次連續(xù)的所有數(shù)。

          在這個程序中,我們將證明 print_report_i 會在 current_line == num_lines 的條件下終止,然后證明如果 print_report_i 會在給定的 current_line 條件下終止,那么它也可以在 current_line - 1 條件下終止,假定 current_line > 0。

          證明 1. 證明對于任意給定的一組行,程序都能終止

          假定
          我們假定 num_lines >= current_line 且 LINES_PER_PAGE > 1。

          基線條件證明
          通過觀察,我們可以知道,當 current_line == num_lines 時,程序會立即終止。

          歸納步驟證明
          在程序的每一次迭代中,current_line 或者增 1(R3),或者保持不變(R2 和 R3)。

          只有當 current_line 的當前值與 current_line 的先前值不同時,R2 才會發(fā)生,因為 current_group 和 previous_group 直接由它派生而來。

          只有 num_lines_this_page 中的變化會令 R1 發(fā)生,而這種變化只能由 R2 和 R3 產(chǎn)生。

          由于只有以 R3 為基礎才能發(fā)生 R2,且只有以 R2 和 R3 為基礎才能發(fā)生 R1,我們可以斷定,current_line 必須是增加的,而且只能是單調(diào)遞增。

          因此,如果 current_line 的某一值可以終止,那么 current_line 之前的所有值都可以終止。

          我們現(xiàn)在已經(jīng)證明,在我們的假設前提下,print_report_i 將可以終止。

          證明在 LINES_PER_PAGE 行之后會發(fā)生分頁
          這個程序會保持在何處分頁的追蹤,因此,有必要證明分頁機制有效。如前所述,證明以公理和定理做為其論據(jù)。在此,我將提出兩個定理來完成證明。如果定理的條件被證明為真,則我們可以使用此定理來確定我們的程序的定理結果的正確性。

          證明 2. 在 LINES_PER_PAGE 行之后發(fā)生分頁

          假定
          當前頁的第一行已經(jīng)打印了一個頁眉。

          定理 1
          如果 num_lines_this_page 設置為正確起始值(條件 1),每打印一行 num_lines_per_page 增 1(條件 2),并且在分頁之后重新設置 num_lines_per_page(條件 3),那么 num_lines_per_page 則精確地表示此頁上已經(jīng)打印的行數(shù)。

          定理 2
          如果 num_lines_this_page 精確地表示已經(jīng)打印的行數(shù)(條件 1),并且每當 num_lines_this_page == LINES_PER_PAGE 時執(zhí)行一次分頁,那么我們就確信我們的程序在打印 LINES_PER_PAGE 行之后會進行一次分頁。

          證明
          設想定理 1 的條件 1。如果我們假定通過 print_report 調(diào)用 print_report_i,那么觀察可知,這無論如何都是顯然的。

          通過確認每一個打印一行的過程都相應使 num_lines_this_page 增 1,條件 2 能得到確定。在以下三種情況下完成行打印:

          1. 打印組的總數(shù)。
          2. 打印單個的報告行。
          3. 打印頁眉。

          觀察可見,行打印條件 1 和 2 將 num_lines_this_page 增 1,行打印條件 3 在一個 分頁/頁眉 組合打印之后將 num_lines_this_page 重新設置為適當?shù)闹担ǔR?guī)的條件 3)。定理 1 的要求得到了滿足,所以我們就已經(jīng)證明了程序會在打印 LINES_PER_PAGE 行之后進行一次分頁。

          證明每一個報告項都嚴格只打印一次
          我們需要確保程序總是打印報告的每一行,從不遺漏。我們可以使用一個歸納證明來證明,如果 print_report_i 根據(jù) current_line == X 準確地打印一行,那么它也將或者準確地打印一行,或者因 current_line == X + 1 而終止。另外,由于我們既有起始條件也有終止條件,所以我們必須證明兩者都是正確的,因此我們必須證明那個基線條件,即當 current_line == 0 時 print_report_i 有效,而當 current_line == num_lines 時它 只是 會終止。

          不過,在本例中,我們可以進行相當程度的簡化,只是通過補充我們的第一個證明來給出一個直接證明。我們的第一個證明表明,在起始時使用一個給定的數(shù)字,將在適當?shù)臅r候終止程序。通過觀察可知,算法繼續(xù)進行,證明已經(jīng)完成了一半。

          證明 3. 每一個報告項的行都嚴格只打印一次

          假定
          由于我們要使用證明 1,所以這個證明依賴于證明 1 的假定。另外我們假定 print_report_i 的第一次調(diào)用來自于 print_report,這表示 current_line 從 0 開始。

          定理 1
          如果 current_line 只有在一次 print_line(條件 1)調(diào)用之后才會增加,而且只有在 current_line 增加之前才會調(diào)用 print_line,那么 current_line 每經(jīng)歷一個數(shù)字將會打印出單獨的一行。

          定理 2
          如果定理 1 為真(條件 1),同時 current_line 經(jīng)歷從 0 到 num_lines - 1 的每一個數(shù)字(條件 2),而且當 current_line == num_lines 時終止(條件 3),那么每一個報告項的行都嚴格只打印一次。

          證明
          觀察可知,定理 1 的條件 1 和條件 2 為真。R3 是惟一一處 current_line 會增加的地方,而且這個增加在 print_line 的調(diào)用之后隨即就會發(fā)生。因此,定理 1 可證,同樣定理 2 的條件 1 可證。

          通過歸納可以證明條件 2 和 3,并且,實際上這只是第一個終止證明的重復。我們可以使用終止的證明來最終證明條件 3。基于那個證明,以及 current_line 從 0 開始的假定,條件 2 為真。因此,我們已經(jīng)證明報告的每一行都嚴格只打印一次。

          證明和遞歸程序設計
          這些只是我們能為程序所做的一些證明。它們還可以更為嚴格,不過我們大部分人選擇的是程序設計而非數(shù)學,因為我們不能忍受數(shù)學的單調(diào),也不能忍受它的符號。

          使用遞歸可以極度簡化程序的核查。并不是不能為命令式程序進行那種程序證明,而是狀態(tài)改變發(fā)生的次數(shù)之多使得那些證明不具意義。使用遞歸程序,用遞歸取代修改狀態(tài),狀態(tài)改變發(fā)生的次數(shù)很少,并且,通過一次設置所有遞歸變量,程序變更能保持前后一致。這不能完全避免邏輯錯誤,但它確實可以消除其中很多種類的錯誤。這種只使用遞歸來完成狀態(tài)改變和重復的程序設計方法通常被稱作 函數(shù)式程序設計(functional programming)

          尾部遞歸(Tail-recursive)函數(shù)
          這樣,我已經(jīng)向您展示了循環(huán)與遞歸函數(shù)有何種關聯(lián),以及如何將循環(huán)轉化為遞歸的、非狀態(tài)改變的函數(shù),以獲得比先前的程序設計可維護性更高而且能夠保證正確的成果。

          不過,對于遞歸函數(shù)的使用,人們所關心的一個問題是棧空間的增長。確實,隨著被調(diào)用次數(shù)的增加,某些種類的遞歸函數(shù)會線性地增加棧空間的使用 —— 不過,有一類函數(shù),即 尾部遞歸 函數(shù),不管遞歸有多深,棧的大小都保持不變。

          尾部遞歸
          當我們將循環(huán)轉化為遞歸函數(shù)時,遞歸調(diào)用是函數(shù)所做的最后一件事情。如果仔細觀察 print_report_i,您會發(fā)現(xiàn)在函數(shù)中遞歸調(diào)用之后沒有再進一步發(fā)生任何事情。

          這表現(xiàn)為類似循環(huán)的行為。當循環(huán)到達循環(huán)的末尾,或者它執(zhí)行 continue 時,那是它在代碼塊中要做的最后一件事情。同樣地,當 print_report_i 再次被調(diào)用時,在遞歸點之后不再做任何事情。

          函數(shù)所做的最后一件事情是一個函數(shù)調(diào)用(遞歸的或者非遞歸的),這被稱為 尾部調(diào)用(tail-call)。使用尾部調(diào)用的遞歸稱為 尾部遞歸。讓我們來看一些函數(shù)調(diào)用示例,以了解尾部調(diào)用的含義到底是什么:

          清單 12. 尾部調(diào)用和非尾部調(diào)用

                      int test1()

                      {

                      int a = 3;

                      test1(); /* recursive, but not a tail call. We continue */

                      /* processing in the function after it returns. */

                      a = a + 4;

                      return a;

                      }

                      int test2()

                      {

                      int q = 4;

                      q = q + 5;

                      return q + test1(); /* test1() is not in tail position.

                      * There is still more work to be

                      * done after test1() returns (like

                      * adding q to the result

                      */

                      }

                      int test3()

                      {

                      int b = 5;

                      b = b + 2;

                      return test1(); /* This is a tail-call. The return value

                      * of test1() is used as the return value

                      * for this function.

                      */

                      }

                      int test4()

                      {

                      test3(); /* not in tail position */

                      test3(); /* not in tail position */

                      return test3(); /* in tail position */

                      }

                      

          可見,要使調(diào)用成為真正的尾部調(diào)用,在尾部調(diào)用函數(shù)返回之前,對其結果 不能執(zhí)行任何其他操作

          注意,由于在函數(shù)中不再做任何事情,那個函數(shù)的實際的棧結構也就不需要了。惟一的問題是,很多程序設計語言和編譯器不知道如何除去沒有用的棧結構。如果我們能找到一個除去這些不需要的棧結構的方法,那么我們的尾部遞歸函數(shù)就可以在固定大小的棧中運行。

          尾部調(diào)用優(yōu)化
          在尾部調(diào)用之后除去棧結構的方法稱為 尾部調(diào)用優(yōu)化

          那么這種優(yōu)化是什么?我們可以通過詢問其他問題來回答那個問題:

          • 函數(shù)在尾部被調(diào)用之后,還需要使用哪個本地變量?哪個也不需要。
          • 會對返回的值進行什么處理?什么處理也沒有。
          • 傳遞到函數(shù)的哪個參數(shù)將會被使用?哪個都沒有。

          好像一旦控制權傳遞給了尾部調(diào)用的函數(shù),棧中就再也沒有有用的內(nèi)容了。雖然還占據(jù)著空間,但函數(shù)的棧結構此時實際上已經(jīng)沒有用了,因此,尾部調(diào)用優(yōu)化就是要在尾部進行函數(shù)調(diào)用時使用下一個棧結構 覆蓋 當前的棧結構,同時保持原來的返回地址。

          我們所做的本質(zhì)上是對棧進行處理。再也不需要活動記錄(activation record),所以我們將刪掉它,并將尾部調(diào)用的函數(shù)重定向返回到調(diào)用我們的函數(shù)。這意味著我們必須手工重新編寫棧來仿造一個返回地址,以使得尾部調(diào)用的函數(shù)能直接返回到調(diào)用它的函數(shù)。

          這里是為那些真正熱衷底層編程的人準備的一個優(yōu)化尾部調(diào)用的匯編語言模板:

          清單 13. 尾部調(diào)用的匯編語言模板

                      ;;Unoptimized tail-call

                      my_function:

                      ...

                      ...

                      ;PUSH ARGUMENTS FOR the_function HERE

                      call the_function

                      ;results are already in %eax so we can just return

                      movl %ebp, %esp

                      popl %ebp

                      ret

                      ;;Optimized tail-call optimized_function:

                      ...

                      ...

                      ;save the old return address

                      movl 4(%ebp), %eax

                      ;save old %ebp

                      movl (%ebp), %ecx

                      ;Clear stack activation record (assuming no unknowns like

                      ;variable-size argument lists)

                      addl $(SIZE_OF_PARAMETERS + 8), %ebp ;(8 is old %ebp + return address))

                      ;restore the stack to where it was before the function call

                      movl %ebp, %esp

                      ;Push arguments onto the stack here

                      ;push return address

                      pushl %eax

                      ;set ebp to old ebp

                      movl %ecx, %ebp

                      ;Execute the function

                      jmp the_function

                     

          可見,尾部調(diào)用使用了更多一些指令,但是它們可以節(jié)省相當多內(nèi)存。使用它們有一些限制:

          • 當函數(shù)返回到進行調(diào)用的函數(shù)時,后者一定不能依賴于仍在棧中的參數(shù)列表。
          • 調(diào)用的函數(shù)一定不能顧慮棧指針當前所指的位置。(當然,可以假定它超出了其本地變量的范圍。)這意味著您不能使用 -fomit-frame-pointer 進行編譯,所有寄存器向棧中保存都要參照 %ebp 而不是 %esp。
          • 不能有任何變長的參數(shù)列表。

          當函數(shù)在尾部調(diào)用中調(diào)用自己時,方法更為簡單。我們只需要將參數(shù)的新值移到舊值之上,然后在本地變量保存到棧上之后立即進行一個到函數(shù)中位置的跳轉。由于我們只是跳轉到同一個函數(shù),所以返回地址和舊的 %ebp 是相同的,棧的大小也不會改變。因此,在跳轉之前我們要做的惟一一件事情就是使用新的參數(shù)取代舊的參數(shù)。

          從而,在只是付出了一些指令的代價后,您的程序會擁有函數(shù)式程序的可證明性和命令式程序的速度和內(nèi)存特性。惟一的問題在于,現(xiàn)在只有非常少的編譯器實現(xiàn)了尾部調(diào)用優(yōu)化。Scheme 實現(xiàn)必需要實現(xiàn)這種優(yōu)化,很多其他函數(shù)式語言實現(xiàn)也必須要實現(xiàn)。不過,要注意,由于有時函數(shù)式語言使用棧的方式與命令式語言區(qū)別很大(或者根本不使用棧),所以實現(xiàn)尾部調(diào)用優(yōu)化的方法可能會有相當大的區(qū)別。

          最新版本的 GCC 也包含了一些在受限環(huán)境下的尾部遞歸優(yōu)化。例如,前面描述的 print_report_i 函數(shù)在 GCC 3.4 中使用 -O2 進行尾部調(diào)用優(yōu)化編譯,因此運行時使用的棧的大小是固定的,而不是線性增長的。

          結束語
          遞歸是一門偉大的藝術,使得程序的正確性更容易確認,而不需要犧牲性能,但這需要程序員以一種新的眼光來研究程序設計。對新程序員來說,命令式程序設計通常是一個更為自然和直觀的起點,這就是為什么大部分程序設計說明都集中關注命令式語言和方法的原因。不過,隨著程序越來越復雜,遞歸程序設計能夠讓程序員以可維護且邏輯一致的方式更好地組織代碼。

          posted on 2008-04-22 01:15 小鋒 閱讀(544) 評論(0)  編輯  收藏 所屬分類: algorithm

          主站蜘蛛池模板: 东丽区| 泰州市| 通海县| 北流市| 溧水县| 九江县| 礼泉县| 小金县| 三台县| 北流市| 南京市| 延庆县| 盐源县| 临澧县| 太和县| 车险| 余干县| 乐亭县| 株洲县| 合作市| 博客| 长葛市| 吉木萨尔县| 泊头市| 广元市| 柞水县| 张北县| 平陆县| 黄山市| 石门县| 和平县| 平武县| 六盘水市| 安多县| 金沙县| 凤冈县| 定远县| 东城区| 奇台县| 固原市| 枝江市|