如何递归地思考`msort`函数

Question

这些问题在一般情况下要多做一些关于如何递归思考的问题，但我会举一个具体的例子来说明。

Graham Hutton 在视频中解释了函数mSort：

https://youtu.be/I9S61BYM9_4?t=2089

因此，在我在视频中链接的特定点上，教授说：

在这里，我有两个排序列表：

msort :: [Int] -> [Int] 
msort []  = [] 
msort [x] = [x] 
msort xs  =      (msort ys) (msort zs)
    where
        (ys, zs) = halve xs

并突出显示表达式(msort ys) 和(msort zs)。然后，他在这些表达式前面添加了单词merge。

msort :: [Int] -> [Int] 
msort []  = msort [] 
msort [x] = msort [x] 
msort xs  = merge (msort ys) (msort zs)
    where
        (ys, zs) = halve xs

对我来说，似乎有一些假设，类似于逻辑中的假设，例如“如果这个假设场景是真的，那么（推导出一些陈述）”。这些对于考虑递归很有用，但与递归函数的评估无关。所以，我的问题是：

• 当msort 尚未完全定义时，他怎么能谈论msort ys？
• 当然，那里写的所有东西都没有任何神奇的意义。但是选择的词是否仅有助于推理功能？我在问，因为他谈到 msort ys 是一个“排序列表”。他使用过去时。
• 这是否假设halve 将以合理的方式定义？同样，halve 只是一个名称。

如果这些真的是基本问题，我深表歉意。这是我最近才开始疑惑的事情。

Answer 1

这些问题是“基本的”，但从某种意义上说，它们是理解函数式语言和递归程序概念的基础，而不是因为它们很容易或显而易见。

与逻辑假设的相似性并非完全巧合。 Hutton 给出的msort 的定义与数理逻辑中的归纳证明有关。在通常的数学归纳证明中，我们证明某些东西适用于一个小的“基本情况”（例如，适用于n=0），然后我们证明如果适用于任意大小的情况（例如，任何特定的n），它适用于“稍大”的情况（例如，对于n+1）。由此，我们可以得出结论，它适用于所有情况（例如，对于n>=0 的所有值）。

在这里，我们证明了几个小案例的属性（例如，很容易对空列表进行排序，并且很容易对单元素列表进行排序），然后我们证明如果我们可以对两个大致长度为n/2（例如msort ys和msort zs）的列表进行排序，然后我们可以对长度为n (msort xs) 的列表进行排序，我们通过归纳得出结论，可以对任何大小的列表进行排序。这里有很多细节要填写，比如用一个奇数长度列表的一半长度来得到两个“大约”一半长度的列表意味着什么，等等，但这是一般的想法。

可能值得指出的是，即使部分数学证明采用“如果我们假设大小为 15 的列表可以排序，那么我们可以对大小为 30 的列表进行排序”的形式，我们也没有必要假设大小 15 可以排序以使用此证明。证明有效，因为前提“可以对大小为 1 的列表进行排序”和“假设可以对大小为 n 的列表进行排序，那么可以对大小为 n*2 的列表进行排序”允许我们得出结论，所有大小相等的列表可以对 2 的幂进行排序（并且对这个证明进行一些小的修改，我们可以证明任何大小的列表也可以排序）。 “假设”是有效证明的形式结构的一部分，而不是我们需要为证明有效而做出的假设。

在某种程度上，递归函数msort 也是如此。现代函数式语言的魔力在于msort能够在“完全定义”之前在msort 中使用。这是因为我们不需要证明我们可以为大小为 15 的列表定义 msort。我们只需要证明我们可以为大小为 30 的列表定义 msort在条款msort 的大小为 15 的列表，只要我们添加几个不依赖于 msort 的基本情况（例如，大小为 0 或 1 的列表直接排序），@987654338 的定义@——就像归纳的数学证明——工作得很好。

当 Sutton 谈到 msort ys 以过去时排序时，他遇到了将英语时态与递归函数的含义相匹配的困难。在编译时，msort ys 只是对正在定义过程中的函数的引用，但这就是递归函数的魔力——定义它们的过程的一部分涉及调用正在定义中的函数.在运行时，时态是准确的。当您运行msort [4,3,2,1] 时，它将调用msort [4,3]，它将列表排序为[3,4] 和msort [2,1]，这会将列表排序为[1,2]，这些排序（过去时）值将可用merged 转化为最终结果 [1,2,3,4]。

我不确定我是否理解您为什么不确定您是否理解halve——是的，这是假设halve 将以与其名称匹配的某种合理方式定义。但是，由于halve 不依赖于msort 或halve，它不会提出与msort 相同的哲学问题。如果有帮助，请假装 halve 定义为：

halve xs = (take n xs, drop n xs) where n = length xs `div` 2