Schemeで再帰が動作することを信頼する/仮定するためのヒントはありますか？

Question

私はPLTスキームで再帰を回避するのに苦労しています。例えば

、あなたが「*」の数のとのBナンバー 『 - 』 'を出力する。このコード（未完）、持っている場合はSを：

私はこの部分ことを信頼することができますどのように

(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節が使用され、結果は0になります.3 * 0 = 0であるため、その基数でmult3が機能します。

誘導ステップでは、nより小さいすべての数に対してプロパティが真であると仮定し、nに対してプロパティが真であることを示す必要があります。 この場合、(mult3 n-1)が3 *（n-1）を返すと仮定できると仮定しなければなりません。

その前提では、(mult3 n)が返すものを考慮する必要があります。 mがゼロでないため、2番目のcond節が使用されます。値が が(+ 3 (mult3 (- n 1)))であり、我々は持って返さ：

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

この例では、あなたの質問は、「どうすれば正常に動作する 式（mult3 M-1）を信頼することができますか？」です。答えは、誘導の原則のために、あなたがそれを信じることができるということです。要するに：まず、基底ケースをチェックし、（mult3 m）がnより小さい全てのmに対して働くという仮定の下で（mult3 n）をチェックする。

誘導原理を使用するには、再帰関数の引数が小さくなることが重要です。 mult3の例では、nはn-1になります。 stars-and-stripeの例では、aまたはbは再帰呼び出しで小さくなります。

この説明は意味がありますか？