如何理解 SML 中的这种递归？

Question

为什么高清日期成为最旧的日期？我就是搞不懂流程

fun oldest(dates : (int * int * int) list) = 
    if null dates
    then NONE
    else
        let
            val d = oldest(tl dates)
        in
            if isSome d andalso is_older(valOf d, hd dates) 
            then d
            else SOME(hd dates) 
        end

Answer 1

在我看来，通过一个小的辅助函数和模式匹配的案例分析，这更容易理解。
（我的建议是熟悉模式和案例分析，避免使用条件和选择器函数。一次推理一件事比记住整个逻辑链和解构要容易得多。）

以这种方式重写你的代码可能会得到这样的结果：

fun oldest_of (d, d') = if is_older (d, d') then d else d'

fun oldest [] = NONE
  | oldest (d::ds) = case oldest ds of
                        NONE => SOME d
                      | SOME d' => SOME (oldest_of (d, d'))

也就是说，

• 如果列表为空，则没有最早的日期
• 否则，在输入的尾部查找最旧的日期；
  • 如果没有，则输入的第一个元素必须是最旧的
  • 否则，选择最旧的元素和输入的第一个元素

现在（希望）很明显，递归中的 NONE 情况只有在尾部 ds 为空时才会发生 - 也就是说，如果输入只有一个元素。
让我们把它放到自己的案例中：

fun oldest [] = NONE
  | oldest [d] = SOME d
  | oldest (d::ds) =  SOME (oldest_of (d, valOf (oldest ds)))

这读起来很像最早日期的定义：

• 如果没有日期，则没有最旧的日期
• 如果只有一个日期，那就是最旧的日期
• 如果至少有两个日期，则为第一个日期中最早的日期，其余日期中最旧的日期

这不需要太多的归纳思考。

Answer 2

你可以通过归纳来证明：

1. 在空列表的情况下，oldest 将返回NONE。

2. 如果列表包含一个元素，我们将进入else 分支，letting d 是NONE，因为带有一个元素的列表的tl 返回一个空列表. isSome d 将为 false，这就是为什么我们将返回 SOME(hd dates) — 唯一的元素，根据定义，它是最旧的。

3. 假设函数适用于 n-1 个项目的列表，让我们看看当列表有 n 个项目时会发生什么：我们将进入 @ 987654330@ 分支并分配给d 列表尾部最旧的元素（有效，因为它包含 n-1 个项目）。现在有两种可能的情况：

   一个。 d 早于列表的第一个元素。在这种情况下，d 将被返回，因为 isSome d 和 is_older(valOf d, hd dates) 都为真。

   b. d 不早于列表的第一个元素。因此，我们将返回 SOME(hd dates) — 列表的第一个元素。

4. 如果它适用于 n-1，我们已经证明它适用于 n 元素，并且我们已经证明它适用于 n=0 和 n =1（从技术上讲，我们可以跳过第 2 步）。因此，它适用于任何大小的列表。