如何在线性时间内通过 `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 中有共享，函数是线性的。

然而，如果我们尝试用 Fins 而不是 ℕ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)

是否可以在线性时间内枚举 Fins？

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))))。所以我们在k下再添加一个参数sucs，最终定义为

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

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

How to enumerate the elements of a list by `Fin`s in linear time?

time-complexity

agda

dependent-type

idris