您是否有提示信任/假設遞歸在Scheme中有效？

Question

我很難在PLT計劃中遞歸。

舉例來說，如果你有這樣的代碼（未完成），輸出一批「*」'S和B號‘ - ’的：

(define (stars-and-stripes a b) 
(local ((define repeat (lambda(w n) (cond [(= n 0) ""] [(> n 0) (string-append w (repeat w (− n 1)))])))) 
(cond 
[(= 0 a) (cons (repeat "-" b) empty)] 
[(= 0 b) (cons (repeat "∗" a) empty)] 
[ (and (> a 0) (> b 0)) ... (stars-and-stripes (− a 1) b) ... (stars-and-stripes a (− b 1))...]))) 

我怎麼能相信，這部分工作正常嗎？

(stars-and-stripes (− a 1) b) ... (stars-and-stripes a (− b 1)) 

這是一個概念性的概念，我有麻煩抓住。

Answer 1

有趣的問題。答案歸結爲：

You can trust it due to the principle of induction for natural numbers. 

該聲明值得詳細闡述。讓我們考慮一個簡單的遞歸函數：

(define (mult3 n) 
    (cond 
    [(= n 0) 0] 
    [else (+ 3 (mult3 (- n 1)))])) 

我的要求是所有自然數n表示(mult3 n)計算n次3。 如何證明以「for all n」結尾的陳述？那麼，我們必須使用誘導。

基本情況是n = 0。 (mult3 0)返回什麼？由於n = 0，所以使用第一個cond-clause，結果爲0.由於3 * 0 = 0，所以我們有mult3在基本情況下工作。

對於歸納步​​驟1，假定對於所有小於n的數字，屬性爲真，並且必須證明暗示屬性對於n是真實的。 在這種情況下，我們必須假設我們可以假設(mult3 n-1)返回3 *（n-1）。

有了這個假設，我們必須考慮(mult3 n)返回什麼。由於m不爲零，因此使用第二個cond-clause。返回的值是 和(+ 3 (mult3 (- n 1)))我們：

(mult3 n) = (+ 3 (mult3 (- n 1))) 
      = (+ 3 3*(n-1))   ; by induction hypothesis 
      = 3*n 

在這個例子中，你的問題是「我怎麼能相信 工作正常表達（mult3 M-1）？」。答案是，由於歸納原理，您可以信任它。簡而言之：首先檢查基本情況，然後檢查（mult3 n），假設（mult3 m）適用於所有小於n的m。

爲了使用歸納原理，重要的是遞歸函數的參數要小些。在mult3的例子中，n變成n-1。 在星條旗的例子中，a或b在遞歸調用中變小。

這個解釋有意義嗎？