Non riesco a darvi il motivo per cui esattamente questo accade, ma posso mostrarvi come curare i sintomi. Prima di iniziare: Questo è un known problem con il correttore di terminazione. Se sei esperto in Haskell, puoi dare un'occhiata allo source.
Una possibile soluzione è quella di dividere la funzione in due: primo, per il caso in cui il primo argomento diventa più piccolo e secondo per il secondo:
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
Quindi, le prime costolette funzione giù xs
e una volta che dobbiamo abbattere lo ys
, passiamo alla seconda funzione e viceversa.
Un altro (forse sorprendente) opzione, che viene citato anche nella relazione problema, è quello di introdurre il risultato di ricorsione via 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
E, infine, siamo in grado di effettuare il ricorsione su Vec
tori e poi riconvertire 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
Tuttavia, qui è necessario uno 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
Potremmo anche avere go
ritorno List
direttamente ed evitare il lemma tutto:
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
Il primo trucco (cioè dividere la funzione in poche reciprocamente ricorsive) è abbastanza buono da ricordare. Dal momento che il correttore di terminazione non guarda dentro le definizioni di altre funzioni che si utilizzano, respinge una grande quantità di programmi perfettamente bene, prendere in considerazione:
data Rose {a} (A : Set a) : Set a where
[] : Rose A
node : A → List (Rose A) → Rose A
Ed ora, vorremmo implementare 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)
Il controllo di terminazione, tuttavia, non guarda all'interno dello map
per vedere se non fa nulla di strano con gli elementi e rifiuta semplicemente questa definizione.Dobbiamo inline la definizione di map
e scrivere un paio di funzioni mutuamente ricorsive:
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
Di solito, è possibile nascondere la maggior parte del caos in una dichiarazione 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
Nota: Dichiarare le firme di entrambi le funzioni prima che siano definite possono essere utilizzate al posto di mutual
nelle versioni più recenti di Agda.
Aggiornamento: La versione di sviluppo di Agda ottenuto un aggiornamento per il correttore di terminazione, vi svelo il messaggio di commit e le note di rilascio parlano da soli:
- Una revisione di completamento grafico delle chiamate che può gestire profondità di terminazione arbitrarie. Questo algoritmo è stato in giro per MiniAgda per un po 'di tempo, in attesa del suo grande giorno. Ora è qui! Opzione L'opzione --termination-depth può ora essere ritirata.
E dalle note di rilascio: controllo
Cessazione delle funzioni definite da 'con' è stata migliorata.
casi che in precedenza richiedevano --termination-profondità (ormai obsoleta!) per passare il controllo di terminazione (grazie all'uso di 'con') non è più
bisogno di bandiera. Ad esempio
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)
Questo non ha controllo terminazione in precedenza, poiché il 'con' espande ad una funzione ausiliaria di unione-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)
Questa funzione effettua una chiamata a fondersi in cui la dimensione di uno degli argomenti è in aumento. Per fare questo passare il correttore di terminazione ora inline la definizione di merge-aux prima di controllare, quindi terminazione in modo efficace controllando il programma di origine originale.
Come risultato di questa trasformazione facendo 'con' su una variabile no si conserva più la terminazione. Per esempio, questo non controllo non terminazione:
bad : Nat → Nat
bad n with n
... | zero = zero
... | suc m = bad m
E in effetti, la funzione originale ora passa il controllo di terminazione!
Grazie, questa è solo la risposta che ho cercato. –