Проверка завершения при слиянии списка
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
И действительно, ваша оригинальная функция теперь проходит проверку завершения!