2011-04-27 103 views
3


這個函數是否是尾遞歸的?我的rec函數尾遞歸嗎?

let rec rec_algo1 step J = 
    if step = dSs then J 
    else 
     let a = Array.init (Array2D.length1 M) (fun i -> minby1J i M J) 
     let argmin = a|> Array.minBy snd |> fst 
     rec_algo1 (step+1) (argmin::J) 

一般情況下,是有辦法正式檢查呢?

謝謝。

+0

你可以有條不紊地檢查編譯器是否認識到它(畢竟,這是最重要的),但不是不向編譯器詢問相應分析過程的結果(或者實施一些你自己並希望它們不是更聰明比編譯器)。 – delnan 2011-04-27 19:49:04

+0

這可能會也可能不會回答你的第二個問題,但是,如果你的函數在遞歸調用後沒有做任何事情,那麼它是尾遞歸的。一個跡象表明它不是尾遞歸的:你正在做遞歸調用的返回值,除了返回它。 – Daniel 2011-04-27 21:04:28

+0

參見http://stackoverflow.com/questions/806712/how-do-i-know-if-a-function-is-tail-recursive-in-f – Brian 2011-04-27 22:16:33

回答

4

這個函數是尾遞歸的;我可以通過目測來判斷。

通常情況下並不總是很容易分辨。也許最可靠/實用的方法就是在大量輸入中檢查它(並確保在「釋放」模式下進行編譯,因爲「調試」模式會關閉尾部調用以進行更好的調試)。

+0

謝謝布萊恩。您對編譯模式的評論也很有幫助。 – jliettehk 2011-04-27 20:00:29

+1

@布萊恩 - 你能通過檢查相應的IL來判斷函數嗎?另外,雖然普通的正式支票可能很難(不可能?),但是您能否舉例說明僅僅通過目測難以分辨的地方?我已經看到它多次說過,這並不總是很容易說出來,但我從來沒有見過一個複雜的尾遞歸函數,它不容易分辨。 – 2011-04-27 20:11:18

+1

某處我看到F#團隊正在考慮一個未來的關鍵字,它會讓你告訴編譯器你想要一個函數是尾遞歸的,這樣編譯器可以警告你它是否真的不是。我認爲這真的很方便。 – 2011-04-27 20:29:45

4

是的,你可以正式證明函數是尾遞歸的。每個表達式都有一個尾部位置,如果所有的遞歸都在尾部位置,那麼函數是尾遞歸的。函數在一個地方可能是尾遞歸的,但在另一個地方是不可能的。

在表達式let pat = exprA in exprB中,只有exprB處於尾部位置。也就是說,儘管您可以評估exprA,但您仍然必須回頭評估exprBexprA。對於語言中的每個表達式,都有一個減少規則,告訴你尾部位置在哪裏。在ExprA; ExprB它再次ExprB。在if ExprA then ExprB else ExprC這是ExprBExprC等等。

編譯器當然知道這一點。然而,F#中可用的許多表達式以及編譯器進行的許多內部優化,例如,在模式匹配編譯期間,計算表達式如seq{}async{}可以使得知道哪些表達式處於尾部位置不明顯。

實際上,通過一些實踐,小功能很容易通過查看嵌套表達式並檢查不在尾部位置的槽來進行函數調用來確定尾部調用。 (請記住,尾巴呼叫可能是另一個功能!)

4

你問我們如何正式檢查這個,所以我會刺傷。我們首先必須定義函數是尾遞歸的意思。形式

let rec f x_1 ... x_n = e 

的遞歸函數的定義是尾遞歸如果fe所有呼叫都尾調用 - 即。發生在尾部情況下。甲尾上下文C感應定義爲術語具有孔[]

C ::= [] 
    | e 
    | let p = e in C 
    | e; C 
    | match e with p_1 -> C | ... | p_n -> C 
    | if e then C else C 

其中e是F#表達,x是可變的,並且是p的圖案。我們應該把它擴展到相互遞歸的函數定義,但我會把它作爲一個練習。

現在讓我們將這個應用到您的示例中。在函數體內rec_algo1唯一的呼叫在這方面:

if step = dSs then J 
else 
    let a = Array.init (Array2D.length1 M) (fun i -> minby1J i M J) 
    let argmin = a|> Array.minBy snd |> fst 
    [] 

而且因爲這是一個尾背景下,功能是尾遞歸。這就是函數程序員如何看待它 - 掃描遞歸調用定義的主體,然後驗證每個調用是否發生在尾部上下文中。一個更直觀的尾部呼叫定義是除了返回呼叫之外沒有其他任何操作的結果。