2013-07-28 24 views
6

Agda 2.3.2.1 non può vedere che la seguente funzione termina:Terminazione controllo sulla lista di unire

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 dice che è OK per il controllo di terminazione se gli argomenti su chiamate ricorsive diminuiscono lessicografico. Sulla base di ciò sembra che questa funzione dovrebbe anche passare. Quindi cosa mi manca qui? Inoltre, è forse OK nelle versioni precedenti di Agda? Ho visto un codice simile su Internet e nessuno ha menzionato problemi di terminazione lì.

risposta

6

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!

+0

Grazie, questa è solo la risposta che ho cercato. –

Problemi correlati