Adrienne
Adrienne

Reputation: 2680

Do you have tips for trusting/assuming that recursion works in Scheme?

I'm having a hard time wrapping my head around recursion in PLT Scheme.

For example, if you have this code (unfinished), that outputs a number of "*"'s and b number of "-"'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))...])))

How can I trust that this part works correctly?

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

This is a conceptual concept I've had trouble grasping.

Upvotes: 1

Views: 269

Answers (1)

soegaard
soegaard

Reputation: 31147

Interesting question. The answer boils down to:

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

That statement deserves an elaboration. Let us consider a simpler recursive function:

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

My claim is that (mult3 n) calculated n times 3 for all natural numbers n. How does one prove a statement ending in " for all n" ? Well, one must use induction.

The base case is n=0. What does (mult3 0) return? Since the n=0, the first cond-clause is used, and the result is 0. And since 3*0=0, we have that mult3 works in the base case.

For the induction step one assumes that the property is true for all numbers less than n, and must prove that implies the property is true for n. In this case we must assume we can assume (mult3 n-1) returns 3*(n-1).

With that assumption we must consider what (mult3 n) returns. Since m is not zero the second cond-clause is used. The value returned is (+ 3 (mult3 (- n 1))) and we have:

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

For this example, your question is "How can I trust the expression (mult3 m-1) works correctly?". The answer, is that you can trust it, due to the induction principle. In short: First check the base case(s), then check (mult3 n) under the assumption that (mult3 m) works for all m less than n.

In order to use the induction principle, it is important that the argument to the recursive function besomes smaller. In the mult3 example to n becomes n-1. In the stars-and-stripe example either a or b becomes smaller in the recursive calls.

Is this explanation making sense?

Upvotes: 2

Related Questions