Завершение проверки при объединении списков

Я не могу назвать вам причину, почему именно это происходит, но я могу показать вам, как вылечить симптомы. Прежде чем начать: это известная проблема со средством проверки завершения. . Если вы хорошо разбираетесь в 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

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

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-depth теперь может быть удалена.

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

• Улучшена проверка завершения функций, определенных с помощью 'with'.

  Случаи, которые ранее требовали --termination-depth (теперь устарело!) Для прохождения проверки завершения (из-за использования 'with'), больше не нуждаются в этом флаге. Например

  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)
  

  Ранее это не удавалось выполнить проверку завершения, так как 'with' расширяется до вспомогательной функции 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
  

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