Проверка завершения при слиянии списка

Agda 2.3.2.1 не видит, что следующая функция завершается:

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _     = y ∷ merge (x ∷ xs) ys 
merge xs ys = xs ++ ys

Agda wiki говорит, что для проверки завершения нормально, если аргументы рекурсивных вызовов уменьшаются лексикографически. Исходя из этого, кажется, что эта функция также должна пройти. Так чего мне здесь не хватает? Кроме того, это может быть хорошо в предыдущих версиях Agda? Я видел подобный код в Интернете, и никто не упомянул о проблемах завершения.

1 ответ

Решение

Я не могу дать вам причину, почему именно это происходит, но я могу показать вам, как вылечить симптомы. Прежде чем начать: Это известная проблема с проверкой завершения. Если вы хорошо разбираетесь в Haskell, вы можете взглянуть на источник.


Одним из возможных решений является разделение функции на две части: первая для случая, когда первый аргумент становится меньше, а вторая для второго:

mutual
  merge : List ℕ → List ℕ → List ℕ
  merge (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ merge xs (y ∷ ys)
  ... | no  _ = y ∷ merge′ x xs ys
  merge xs ys = xs ++ ys

  merge′ : ℕ → List ℕ → List ℕ → List ℕ
  merge′ x xs (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ merge xs (y ∷ ys)
  ... | no  _ = y ∷ merge′ x xs ys
  merge′ x xs [] = x ∷ xs

Итак, первая функция вырубает xs и как только мы должны срубить ysпереключаемся на вторую функцию и наоборот.


Другой (возможно, удивительный) вариант, который также упоминается в отчете о проблеме, состоит в том, чтобы представить результат рекурсии через with:

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y | merge xs (y ∷ ys) | merge (x ∷ xs) ys
... | yes _ | r | _ = x ∷ r
... | no  _ | _ | r = y ∷ r
merge xs ys = xs ++ ys

И, наконец, мы можем выполнить рекурсию на Vecтуловища, а затем преобразовать обратно в List:

open import Data.Vec as V
  using (Vec; []; _∷_)

merge : List ℕ → List ℕ → List ℕ
merge xs ys = V.toList (go (V.fromList xs) (V.fromList ys))
  where
  go : ∀ {n m} → Vec ℕ n → Vec ℕ m → Vec ℕ (n + m)
  go {suc n} {suc m} (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _                 = x ∷ go xs (y ∷ ys)
  ... | no  _ rewrite lem n m = y ∷ go (x ∷ xs) ys
  go xs ys = xs V.++ ys

Однако здесь нам понадобится простая лемма:

open import Relation.Binary.PropositionalEquality

lem : ∀ n m → n + suc m ≡ suc (n + m)
lem zero    m                 = refl
lem (suc n) m rewrite lem n m = refl

Мы могли бы также иметь go вернуть List прямо и избегать леммы в целом:

merge : List ℕ → List ℕ → List ℕ
merge xs ys = go (V.fromList xs) (V.fromList ys)
  where
  go : ∀ {n m} → Vec ℕ n → Vec ℕ m → List ℕ
  go (x ∷ xs) (y ∷ ys) with x ≤? y
  ... | yes _ = x ∷ go xs (y ∷ ys)
  ... | no  _ = y ∷ go (x ∷ xs) ys
  go xs ys = V.toList xs ++ V.toList ys

Первый трюк (т.е. разделение функции на несколько взаимно рекурсивных) на самом деле очень хорошо запомнить. Поскольку средство проверки завершения не заглядывает в определения других используемых вами функций, оно отвергает множество совершенно прекрасных программ, рассмотрим:

data Rose {a} (A : Set a) : Set a where
  []   :                     Rose A
  node : A → List (Rose A) → Rose A

И теперь мы хотели бы реализовать mapRose:

mapRose : ∀ {a b} {A : Set a} {B : Set b} →
          (A → B) → Rose A → Rose B
mapRose f []          = []
mapRose f (node t ts) = node (f t) (map (mapRose f) ts)

Проверка завершения, однако, не заглядывает внутрь map чтобы убедиться, что он не делает ничего прикольного с элементами и просто отвергает это определение. Мы должны включить определение map и напишите пару взаимно рекурсивных функций:

mutual
  mapRose : ∀ {a b} {A : Set a} {B : Set b} →
            (A → B) → Rose A → Rose B
  mapRose f []          = []
  mapRose f (node t ts) = node (f t) (mapRose′ f ts)

  mapRose′ : ∀ {a b} {A : Set a} {B : Set b} →
             (A → B) → List (Rose A) → List (Rose B)
  mapRose′ f []       = []
  mapRose′ f (t ∷ ts) = mapRose f t ∷ mapRose′ f ts

Как правило, вы можете скрыть большую часть беспорядка в where объявление:

mapRose : ∀ {a b} {A : Set a} {B : Set b} →
          (A → B) → Rose A → Rose B
mapRose {A = A} {B = B} f = go
  where
  go      :       Rose A  →       Rose B
  go-list : List (Rose A) → List (Rose B)

  go []          = []
  go (node t ts) = node (f t) (go-list ts)

  go-list []       = []
  go-list (t ∷ ts) = go t ∷ go-list ts

Примечание. Объявление сигнатур обеих функций до их определения можно использовать вместо mutual в более новых версиях Agda.


Обновление: версия разработки Agda получила обновление для проверки завершения, я позволю сообщению о фиксации и примечаниям к выпуску говорить сами за себя:

  • Пересмотр завершения графа вызовов, который может иметь дело с произвольной глубиной завершения. Этот алгоритм некоторое время сидел в MiniAgda, ожидая его великого дня. Это сейчас здесь! Опция --termination-глубина теперь может быть удалена.

И из примечаний к выпуску:

  • Проверка завершения функций, определенных 'with' была улучшена.

    Случаи, которые ранее требовали --termination-глубина (теперь устарели!), Чтобы пройти проверку завершения (из-за использования 'с') больше не
    нужен флаг. Например

    merge : List A → List A → List A
    merge [] ys = ys
    merge xs [] = xs
    merge (x ∷ xs) (y ∷ ys) with x ≤ y
    merge (x ∷ xs) (y ∷ ys)    | false = y ∷ merge (x ∷ xs) ys
    merge (x ∷ xs) (y ∷ ys)    | true  = x ∷ merge xs (y ∷ ys)
    

    Это не удалось завершить проверку ранее, так как "с" расширяется до вспомогательной функции merge-aux:

    merge-aux x y xs ys false = y ∷ merge (x ∷ xs) ys
    merge-aux x y xs ys true  = x ∷ merge xs (y ∷ ys)
    

    Эта функция вызывает слияние, при котором размер одного из аргументов увеличивается. Чтобы сделать это, проверка завершения завершает теперь определение merge-aux перед проверкой, таким образом, фактически проверяя завершение исходной программы.

    В результате этого преобразования "переменная" над переменной больше не сохраняет завершение. Например, это не проверка завершения:

    bad : Nat → Nat
    bad n with n
    ... | zero  = zero
    ... | suc m = bad m
    

И действительно, ваша оригинальная функция теперь проходит проверку завершения!

Другие вопросы по тегам