你有关于相信/假设递归在Scheme中有效的技巧吗？

发布于 2024-12-12 01:49:31 字数 558 浏览 3 评论 0原文

我很难理解 PLT 方案中的递归。

例如，如果您有这段代码（未完成），它会输出多个“*”和多个“-”：

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

这是一个我一直难以理解的概念。

原文

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.

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

季末如歌 2024-12-19 01:49:31

有趣的问题。答案归结为：

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 计算 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 不为零，因此使用第二个 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) 适用于所有情况的假设下检查 (mult3 n) m 小于 n。

为了使用归纳原理，递归函数的参数必须变小，在 mult3 示例中，n 变为 n-1。
在星条旗示例中，a 或 b 在递归调用中变小。

这个解释有道理吗？

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?

回复收藏 0 原文

~没有更多了~