как понять эту рекурсию в SML?

Question

почему hd даты становятся самыми старыми? Я просто не могу понять процесс

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

На мой взгляд, это гораздо проще понять с помощью небольшой вспомогательной функции и анализа случаев путем сопоставления с образцом.
(Мой совет - освоиться с шаблонами и анализом случаев, избегая условных выражений и функций выбора. Это гораздо проще рассуждать об одной вещи за раз, чем помнить целую цепочку логик c и деструктуризации.)

Переписав свой код таким образом, можно получить следующее:

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. Если список содержит элемент, мы go перейдем в ветку else, let ting d будет NONE, потому что tl списка с одним элементом возвращает пустой список. isSome d будет ложным, поэтому мы вернем SOME(hd dates) - единственный элемент, который по определению является самым старым.

3. Предполагая, что функция работает для случая списка из n-1 элементов, давайте посмотрим, что произойдет, если в списке будет n элементов: go перейдем в ветку else и назначим d самый старый элемент из хвост списка (который работает, потому что он содержит n-1 элементов). Теперь есть два возможных сценария ios:

   a. d старше первого элемента списка. В этом случае будет возвращено d, поскольку оба значения isSome d и is_older(valOf d, hd dates) будут истинными.

   b. d не старше первого элемента списка. Поэтому мы вернем SOME(hd dates) - первый элемент списка.

4. Мы показали, что он работает для n элементов, если он работает для n -1 , и мы показали, что это работает для n = 0 и n = 1 (технически мы могли бы пропустить шаг 2). Поэтому он будет работать для списка любого размера.