time-complexity - 如何在线性时间内通过 `Fin` 秒枚举列表的元素？

Question

我们可以像这样枚举列表的元素:

-- 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

例如。 enumerate-ℕ (1 ∷ 3 ∷ 2 ∷ 5 ∷ [])等于 (0 , 1) ∷ (1 , 3) ∷ (2 , 2) ∷ (3 , 5) ∷ [] .假设 Agda 中有共享，则函数是线性的。

但是，如果我们尝试通过 Fin 枚举列表的元素s 而不是 ℕ s，函数变成二次的:

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)

是否可以通过 Fin枚举s 在线性时间内？

Answer 1

将此视为第一次尝试:

go : ∀ {m α} {A : Set α} -> Fin m -> (xs : List A) -> List (Fin (m + length xs) × A)
go i  []      = []
go i (x ∷ xs) = (inject+ _ i , x) ∷ {!go (suc i) xs!}

i每次递归调用都会增长，但存在不匹配:

目标类型为 List (Fin (.m + suc (length xs)) × .A)
孔内的表达式类型为 List (Fin (suc (.m + length xs)) × .A)
很容易证明两种类型是相等的，但它也很脏。这是一个常见的问题:一个参数增大而另一个参数减小，因此我们需要定义交换 _+_处理这两种情况，但没有办法定义它。解决方案是使用CPS:

go : ∀ {α} {A : Set α} -> (k : ℕ -> ℕ) -> (xs : List A) -> List (Fin (k (length xs)) × A)
go k  []      = []
go k (x ∷ xs) = ({!!} , x) ∷ go (k ∘ suc) xs

(k ∘ suc) (length xs)和 k (length (x ∷ xs)) 是一样的，因此不匹配是固定的，但什么是 i现在？孔的类型是 Fin (k (suc (length xs)))并且在目前的语境下是无人居住的，所以我们来介绍一些居民:

go : ∀ {α} {A : Set α}
   -> (k : ℕ -> ℕ)
   -> (∀ {n} -> Fin (k (suc n)))
   -> (xs : List A)
   -> List (Fin (k (length xs)) × A)
go k i  []      = []
go k i (x ∷ xs) = (i , x) ∷ go (k ∘ suc) {!!} xs

新孔类型为 {n : ℕ} → Fin (k (suc (suc n))) .我们可以填写 i ，但是 i必须在每次递归调用时增长。然而 suc和 k不通勤，所以 suc i是 Fin (suc (k (suc (_n_65 k i x xs)))) .所以我们添加另一个参数 suc下 k ，最终的定义是

enumerate-Fin : ∀ {α} {A : Set α} -> (xs : List A) -> List (Fin (length xs) × A)
enumerate-Fin = go id suc zero where
  go : ∀ {α} {A : Set α}
     -> (k : ℕ -> ℕ)
     -> (∀ {n} -> Fin (k n) -> Fin (k (suc n)))
     -> (∀ {n} -> Fin (k (suc n)))
     -> (xs : List A)
     -> List (Fin (k (length xs)) × A)
  go k s i  []      = []
  go k s i (x ∷ xs) = (i , x) ∷ go (k ∘ suc) s (s i) xs

哪个有效，因为 s : {n : ℕ} → Fin (k n) → Fin (k (suc n))可以视为 {n : ℕ} → Fin (k (suc n)) → Fin (k (suc (suc n))) .

一个测试: C-c C-n enumerate-Fin (1 ∷ 3 ∷ 2 ∷ 5 ∷ [])给

(zero , 1) ∷
(suc zero , 3) ∷
(suc (suc zero) , 2) ∷ (suc (suc (suc zero)) , 5) ∷ []

现在请注意，在 enumerate-Fin k始终关注 Fin在类型中。因此我们可以抽象 Fin ∘ k并获得适用于 ℕ 的函数的通用版本和 Fin :

genumerate : ∀ {α β} {A : Set α}
           -> (B : ℕ -> Set β)
           -> (∀ {n} -> B n -> B (suc n))
           -> (∀ {n} -> B (suc n))
           -> (xs : List A)
           -> List (B (length xs) × A)
genumerate B s i  []      = []
genumerate B s i (x ∷ xs) = (i , x) ∷ genumerate (B ∘ suc) s (s i) xs

enumerate-ℕ : ∀ {α} {A : Set α} -> List A -> List (ℕ × A)
enumerate-ℕ = genumerate _ suc 0

enumerate-Fin : ∀ {α} {A : Set α} -> (xs : List A) -> List (Fin (length xs) × A)
enumerate-Fin = genumerate Fin suc zero