Ich kann Ihnen nicht den Grund geben, warum genau das passiert, aber ich kann Ihnen zeigen, wie man die Symptome kuriert. Bevor ich beginne: Dies ist eine known problem mit der Terminierungsprüfung. Wenn Sie sich in Haskell auskennen, können Sie sich die source ansehen.
Eine mögliche Lösung ist die Funktion in zwei aufgeteilt: erste für den Fall, dass das erste Argument kleiner und die zweite für die zweite bekommt:
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
Also, die erste Funktion Koteletts nach unten xs und sobald wir ys hacken müssen, wechseln wir zur zweiten Funktion und umgekehrt.
Weitere (vielleicht überraschend) Option, die auch in der Frage Bericht erwähnt wird, ist das Ergebnis der Rekursion über with vorstellen:
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
Und schließlich können wir die führen Rekursion auf Vec toren und dann konvertieren zurück zu 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
jedoch hier brauchen wir eine einfache Lemma:
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
Wir auch go Rückkehr List direkt haben könnte und vermeiden das Lemma zusammen:
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
Der erste Trick (d Teilen Sie die Funktion in einige gegenseitig rekursive) ist eigentlich ziemlich gut zu erinnern. Da die Abschlussprüfung innerhalb der Definitionen von anderen Funktionen verwenden Sie sieht nicht aus, es lehnt viel völlig in Ordnung Programme betrachten:
data Rose {a} (A : Set a) : Set a where
[] : Rose A
node : A → List (Rose A) → Rose A
Und jetzt möchten wir umsetzen möchten 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)
Der Terminierungsprüfer sieht jedoch nicht innerhalb der map, um zu sehen, ob es nichts mit den Elementen funky macht und nur diese Definition zurückweist.Wir müssen die Definition von map Inline- und ein Paar einander rekursiven Funktionen schreiben:
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
Normalerweise Sie die meisten der Unordnung in einem where Erklärung verstecken kann:
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
Hinweis: Deklarieren von Unterschriften beider Funktionen, bevor sie definiert sind, können anstelle von mutual in neueren Versionen von Agda verwendet werden.
Update: Die Entwickler-Version von Agda bekam ein Update auf die Beendigung checker, werde ich die Meldung verpflichten lassen und Release Notes sprechen für sich:
- Eine Revision des Aufrufgraphen Abschluss das kann mit beliebiger Abbruchtiefe umgehen. Dieser Algorithmus sitzt seit einiger Zeit in MiniAgda, wartet auf seinen großen Tag. Es ist jetzt hier! Option - Die Abschlusstiefe kann jetzt zurückgezogen werden.
Und aus der Release Notes:
Termination Überprüfung der Funktionen, die durch definiert 'durch' wurde verbessert.
Fälle, die zuvor --termination eingehende erforderlich (jetzt veraltet!) die Beendigung checker (aufgrund der Verwendung von ‚mit‘) nicht länger
müssen die Fahne zu übergeben. Zum Beispiel
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)
Dies scheiterte bisher an Abschlusswiderstandsprüftyps, da die ‚mit‘ erweitert auf eine Hilfsfunktion 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)
dieser Funktion wird ein Anruf, in dem fusionieren macht die Größe Eines der Argumente steigt. Um dies zu bestehen, inliniert der Terminierungsprüfer nun die Definition von merge-aux vor der Überprüfung, also effektiv Kündigung das ursprüngliche Quellprogramm zu überprüfen.
Als Ergebnis dieser Umwandlung macht 'doing' mit einer Variablen Nr. länger die Beendigung. Zum Beispiel, tut dies nicht Abschlussprüfung:
bad : Nat → Nat
bad n with n
... | zero = zero
... | suc m = bad m
Und in der Tat, Ihre ursprüngliche Funktion übergibt nun die Abschlussprüfung!
Danke, das ist nur die Antwort, die ich suchte. –