清单 8. 命名 let 示例
(define is-in-list2
(lambda (the-list the-string)
;;Named Let
;;This let block defines a function called "recurse" that is the
;;body of this let. The function's parameters are the same as
;;the variables listed in the let.
(let recurse
;;internal-list is the first and only parameter. The
;;first time through the block it will be primed with
;;"the-list" and subsequent calls to "recurse" will
;;give it whatever value is passed to "recurse"
( (internal-list the-list) )
;;Body of function/named let block
(if (null? internal-list)
#f
(if (equal? the-string (car internal-list))
#t
;;Call recursive function with the
;;rest of the list
(recurse (cdr internal-list)))))))
|
在编写递归函数时，命名 let 能够相当程度地减少键盘输入以及出现错误的数量。如果您理解命名 let 的概念仍有困难，那么我建议您对上面的两个程序中的每一行进行全面的比较（另外参阅本文 参考资料 部分中的一些文档）。
我们的下一个基于列表的递归函数示例要稍微复杂一些。它将检查列表是否以升序排序。如果列表是以升序排序，则函数返回 #t；否则，它将返回 #f。这个程序稍有不同，因为除了必须要考查当前的值以外，我们还必须记住处理过的最后一个值。
对列表中第一项的处理必须与其他项不同，因为没有在它之前的任何项。对于其余的项，我们需要将先前考查的值传递到函数调用中。函数类似如下：
清单 9. 确定列表是否以升序排序的 Scheme 程序
(define is-ascending
(lambda (the-list)
;;First, Initialize the algorithm. To do this we
;;need to get the first value, if it exists, and
;;use it as a seed to the recursive function
(if (null? the-list)
#t
(let is-ascending-recurse
(
(previous-item (car the-list))
(remaining-items (cdr the-list))
)
;;Base case #1 - end of list
(if (null? remaining-items)
#t
(if (< previous-item (car remaining-items))
;;Recursive case, check the rest of the list
(is-ascending-recurse (car remaining-items) (cdr remaining-items))
;;Base case #2 - not in ascending order
#f))))))
|
这个程序首先检查边界条件 —— 列表是否为空。空列表被认为是升序的。然后程序以列表中的第一项及其余部分列表为种子开始递归函数。
然后检查基线条件。能到达列表末尾的惟一情形是此前所有项都按顺序排列，所以，如果某个列表为空，则列表为升序。否则，我们去检查当前项。
如果当前项是升序的，那么我们接下来只需要解决问题的一个子集 —— 列表的其余部分是否为升序。所以我们递归处理列表其余部分，并再次尝试。
注意在函数中我们是如何通过向前传递程序来保持函数调用过程中的状态的。以前我们每次只是传递了列表的剩余部分。不过，在这个函数中，我们需要了解关于计算状态的稍多些内容。当前计算的结果依赖于之前的部分结果，所以，在每次后续递归调用中，我们向前传递那些结果。对更复杂的递归过程来说这是一个通用的模式。
编写保证正确的程序
bug 是每位程序员日常生活的一部分，因为就算是最小的循环和最简单的函数调用之中也会有 bug。尽管大部分程序员能够检查代码并测试代码的 bug，但他们并不知道如何证明他们的程序将会按他们所设想的那样去执行。出于此方面的考虑，我们接下来研究 bug 的一些常见来源，然后阐述如何编写正确的程序以及如何证明其正确性。
bug 来源：状态改变
变量状态改变是产生 bug 的一个主要来源。您可能会认为，程序能敏锐地确切知道变量何时如何改变状态。有时在简单的循环中的确如此，不过在复杂的循环中通常不是这样。通常在循环中给定的变量能够以多种方式改变状态。
例如，如果您拥有一个复杂的 if 语句，有些分支可能会修改某个变量，而其他分支可能会修改其他变量。此外，顺序通常很重要，但是难以绝对保证在所有情形下编码的次序都是正确的。通常，由于这些顺序问题，为某一情形修改某个 bug 会为其他情形引入 bug。
为了预防此类错误，开发人员需要能够：
- 预先断定每个变量如何获得其当前值。
- 确保变量都没有双重用途。（很多程序员经常使用同一变量来存储两个相关但稍有不同的值。）
- 当循环重新开始时，确保所有的变量都处于它们应该处于的状态。（在极少使用和测试的不重要情形中疏忽了为循环变量设置新值，这是常见的程序设计错误。）
为了达成这些目标，我们只需要在程序设计中制定一个规则：一个变量只赋值一次，而且永远不再修改它！
什么？（您说得不可信！）这个规则对很多人来说不可接受，他们所熟知的是命令式、过程式和面向对象程序设计 —— 变量赋值与修改是这些程序设计技术的基础!尽管如此，对命令式语言程序员来说，状态的改变依然是程序设计错误的主要原因。
那么，编程时如何才能不修改变量？让我们来研究一些经常要修改变量的情形，并研究我们是否能够不修改变量而完成任务：
- 重新使用某个变量。
- 变量的条件修改（conditional modification）。
- 循环变量。
我们先来研究第一种情形，重新使用某个变量。通常会出于不同的（但是类似的）目的而重新使用某个变量。例如，有时候，循环的某个部分中，在循环的前半部分需要一个指向当前位置的索引，而循环的其余部分需要一个恰在此索引之前或之后的索引，很多程序员为这两种情况使用同一变量，而只是根据情况对其进行增量处理。当前程序被修改时，这无疑会令程序员难以理解这两种用途。为了预防这一问题，最好的解决方案是创建两个单独的变量，并以同样的方法根据第一个变量得出第二个变量，就像是写入同一变量那样。
第二种情形，即变量的条件修改，是重新使用的问题的一个子集，只是有时我们会保持现有的值，有时需要使用一个新值。同样，最好创建一个新的变量。在大部分语言中，我们可以使用三元运算符 ? : 来设置新变量的值。例如，如果我们需要为新变量赋一个新值，条件是它不大于 some_value，我们可以这样写 int new_variable = old_variable > some_value ? old variable : new_value;。
（我们将在本文中稍后讨论循环变量。）
当我们解决了所有变量状态改变的问题后，就可以确信，当我们第一次定义变量时，变量的定义在函数整个生存期间都会保持。这使得操作的顺序简单了很多，尤其是当修改已有代码时。您不必关心变量被修改的顺序，也不必关心在每一个时刻关于其状态要做什么假定。
当变量的状态不能改变时，在声明它的时刻和地方就给出了其起源的完全定义。您再也不用搜索全部代码去找出不正确的或者混乱的状态。
什么是循环变量？
现在，问题是如何不通过赋值来进行循环？答案是 递归函数。在表 1 中了解循环的特性，看它们可以如何与递归函数的特性相对比。
表 1. 对比循环与递归函数
| 特性 |
循环 |
递归函数 |
| 重复 |
为了获得结果，反复执行同一代码块；以完成代码块或者执行 continue 命令信号而实现重复执行。 |
为了获得结果，反复执行同一代码块；以反复调用自己为信号而实现重复执行。 |
| 终止条件 |
为了确保能够终止，循环必须要有一个或多个能够使其终止的条件，而且必须保证它能在某种情况下满足这些条件的其中之一。 |
为了确保能够终止，递归函数需要有一个基线条件，令函数停止递归。 |
| 状态 |
循环进行时更新当前状态。 |
当前状态作为参数传递。 |
可见，递归函数与循环有很多类似之处。实际上，可以认为循环和递归函数是能够相互转换的。区别在于，使用递归函数极少被迫修改任何一个变量 —— 只需要将新值作为参数传递给下一次函数调用。这就使得您可以获得避免使用可更新变量的所有益处，同时能够进行重复的、有状态的行为。
将一个常见的循环转化为递归函数
让我们来研究一个打印报表的常见循环，了解如何将它转化为一个递归函数。
- 这个循环将在每一个分页处打印出页编号和页眉。
- 假定报告的行依照某个数字标准分组，并假定有用来了解这些组的一个总数。
- 在每一组的最后，打印出组的总数。
出于演示目的，我们略去了所有次要的函数，假定它们存在而且按预期执行。下面是我们的报告打印程序的代码：
清单 10. 用普通循环实现的报告打印程序
void print_report(struct report_line *report_lines, int num_lines)
{
int num_lines_this_page = 0;
int page_number = 1;
int current_line; /* iterates through the lines */
int current_group = 0; /* tells which grouping we are in */
int previous_group = 0; /* tells which grouping was here on the last loop */
int group_total = 0; /* saves totals for printout at the end of the grouping */
print_headings(page_number);
for(current_line = 0; current_line < num_lines; current_line++)
{
num_lines_this_page++;
if(num_lines_this_page == LINES_PER_PAGE)
{
page_number++;
page_break();
print_headings(page_number);
}
current_group = get_group(report_lines[current_line]);
if(current_group != previous_group)
{
print_totals_for_group(group_total);
group_total = 0;
}
print_line(report_lines[current_line]);
group_total += get_line_amount(report_lines[current_line]);
}
}
|
程序中故意留了一些 bug。看您是否能够找出它们。
由于我们要不断地修改状态变量，所以难以预见在任意特定时刻它们是否正确。下面是递归实现的同一程序：
清单 11. 使用递归实现的报告打印程序
void print_report(struct report_line *report_lines, int num_lines)
{
int num_lines_this_page = 0;
int page_number = 1;
int current_line; /* iterates through the lines */
int current_group = 0; /* tells which grouping we are in */
int previous_group = 0; /* tells which grouping was here on the last loop */
int group_total = 0; /* saves totals for printout at the end of the grouping */
/* initialize */
print_headings(page_number);
/* Seed the values */
print_report_i(report_lines, 0, 1, 1, 0, 0, num_lines);
}
void print_report_i(struct report_line *report_lines, /* our structure */
int current_line, /* current index into structure */
int num_lines_this_page, /* number of lines we've filled this page */
int page_number,
int previous_group, /* used to know when to print totals */
int group_total, /* current aggregated total */
int num_lines) /* the total number of lines in the structure */
{
if(current_line == num_lines)
{
return;
}
else
{
if(num_lines_this_page == LINES_PER_PAGE)
{
page_break();
print_headings(page_number + 1);
print_report_i(
report_lines,
current_line,
1,
page_number + 1,
previous_group,
group_total,
num_lines);
}
else
{
int current_group = get_group(report_lines[current_line]);
if(current_group != previous_group && previous_group != 0)
{
print_totals_for_group(group_total);
print_report_i(
report_lines,
current_line,
num_lines_this_page + 1,
page_number,
current_group,
0,
num_lines);
}
else
{
print_line(report_lines[current_line]);
print_report_i(
report_lines,
current_line + 1,
num_lines_this_page + 1,
page_number,
current_group,
group_total + get_line_amount(report_lines[current_line]),
num_lines);
}
}
}
}
|
注意，我们所使用的所有数字都是始终一致的。几乎在任何情形下，只要修改多个状态，在状态改变过程中就会有一些代码行中将不能拥有始终一致的数字。如果以后向程序中此类改变状态的代码中添加一行，而对变量状态的判断与实际情况不相匹配，那么将会遇到很大的困难。这样修改几次以后，可能会因为顺序和状态问题而引入难以捉摸的 bug。在这个程序中，所有状态改变都是通过使用完全前后一致的数据重新运行递归程序而实现的。
递归的报告打印程序的证明
由于从来没有改变变量的状态，所以证明您的程序非常简单。让我们来研究关于清单 11 中报告打印程序的一些特性证明。
提示那些大学毕业后没有进行过程序证明的人（或者可能从来没有进行过），进行程序证明，基本上就是寻找程序的某个特性（通常指定为 P），并证明那个特性适用。要完成此任务需要使用：
- 公理（axioms），假定的真理。
- 定理（theorems） 由公理推论得到的关于程序的陈述。
目标是将公理与定理联合起来证明特性 P 为真。如果程序有不只一个特性，则通常分别去证明每一个。由于这个程序有若干个特性，我们将为其中一些给出简短的证明。
由于我们在进行不正式的证明，所以我不会为所使用的公理命名，也不会尝试去证明那些用来令证明有效的中间定理。但愿它们足够明显，以致不必对它们进行证明。
在证明过程中，我将把程序的三个递归点分别称为 R1、R2 和 R3。所有程序都有一个隐式的假设：report_lines 为合法的指针，且 num_lines 准确地反映 report_lines 所显示的行数。
在示例中，我将尝试去证明：
- 任意给定的一组行，程序都能终止。
- 在 LINES_PER_PAGE 行之后会发生分页。
- 每一个报告项都严格只打印一次。
证明程序会终止
此证明将确认对于任意给定的一组行，程序都会终止。这个证明将使用一种在递归程序中常见的证明技术，名为 归纳证明（inductive proof）。
归纳证明由两个步骤构成。首先，需要证明特性 P 对于给定的一组参数是适用的。然后去证明一个归纳，表明如果 P 对于 X 的值适用，那么它对于 X + 1（或者 X - 1，或者任意类型的步进处理）的值也必须适用。通过这种方法您就可以证明特性 P 适用于从已经证明的那个数开始依次连续的所有数。
在这个程序中，我们将证明 print_report_i 会在 current_line == num_lines 的条件下终止，然后证明如果 print_report_i 会在给定的 current_line 条件下终止，那么它也可以在 current_line - 1 条件下终止，假定 current_line > 0。
