Wie werden die Elemente einer Liste nach `Fin`s in linearer Zeit aufgelistet?
Wir können die Elemente einer Liste wie folgt auflisten:
-- enumerate-ℕ = zip [0..]
enumerate-ℕ : ∀ {α} {A : Set α} -> List A -> List (ℕ × A)
enumerate-ℕ = go 0 where
go : ∀ {α} {A : Set α} -> ℕ -> List A -> List (ℕ × A)
go n [] = []
go n (x ∷ xs) = (n , x) ∷ go (ℕ.suc n) xs
Z.B.enumerate-ℕ (1 ∷ 3 ∷ 2 ∷ 5 ∷ [])
entspricht(0 , 1) ∷ (1 , 3) ∷ (2 , 2) ∷ (3 , 5) ∷ []
. Unter der Annahme, dass es in Agda eine gemeinsame Nutzung gibt, ist die Funktion linear.
Wenn wir jedoch versuchen, die Elemente einer Liste nach @ aufzulistFin
s anstattℕ
s, die Funktion wird quadratisch:
enumerate-Fin : ∀ {α} {A : Set α} -> (xs : List A) -> List (Fin (length xs) × A)
enumerate-Fin [] = []
enumerate-Fin (x ∷ xs) = (zero , x) ∷ map (pmap suc id) (enumerate-Fin xs)
Ist es möglich, durch @ aufzuzählFin
s in linearer Zeit?