Есть ли у вас советы, как доверять / предполагать, что рекурсия работает в Схеме?

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)))]))

Я утверждаю, что (mult3 n) рассчитано n раз 3 для всех натуральных чисел n. Как доказать утверждение, оканчивающееся на «для всех n»? Ну, нужно использовать индукцию.

Базовый случай n = 0. Что возвращает (mult3 0)? Поскольку n = 0, используется первое условие cond, а результат равен 0. И так как 3 * 0 = 0, мы имеем, что mult3 работает в базовом случае.

Для шага индукции предполагается, что свойство истинно для всех чисел, меньших n, и должно быть доказано, что свойство истинно для n. В этом случае мы должны предположить, что мы можем предположить, что (mult3 n-1) возвращает 3 * (n-1).

С этим допущением мы должны рассмотреть, что возвращает (mult3 n). Поскольку m не равно нулю, используется второе условие-условие. Возвращаемое значение это (+ 3 (mult3 (- n 1))) и у нас есть:

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

В этом примере ваш вопрос звучит так: «Как я могу доверять выражению (мульт3 м-1) работает правильно? ". Ответ, это то, что вы можете доверять ему, из-за принципа индукции. Вкратце: сначала проверьте базовый вариант (ы), а затем проверьте (mult3 n) в предположении, что (mult3 m) работает для всех м меньше чем п.

Чтобы использовать принцип индукции, важно, чтобы аргумент рекурсивной функции был меньше. В примере с mult3 n становится n-1. В примере со звездами и полосами или a, или b становится меньше в рекурсивных вызовах.

Имеет ли это объяснение смысл?