本文介绍了如何在线性时间内通过`Fin`s枚举列表的元素?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

限时删除!!

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

We can enumerate the elements of a list like this:

-- 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 中有共享,则函数是线性的.

E.g. enumerate-ℕ (1 ∷ 3 ∷ 2 ∷ 5 ∷ []) is equal to (0 , 1) ∷ (1 , 3) ∷ (2 , 2) ∷ (3 , 5) ∷ []. Assuming there is sharing in Agda, the function is linear.

然而,如果我们尝试通过 Fins 而不是 s 来枚举列表的元素,函数就会变成二次的:

However if we try to enumerate the elements of a list by Fins rather than s, the function becomes quadratic:

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进行枚举?

Is it possible to enumerate by Fins in linear time?

推荐答案

将此视为第一次尝试:

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 在每次递归调用时都会增长,但存在不匹配:

i grows at each recursive call as it should, but there is a mismatch:

目标类型为List(Fin(.m + suc(length xs)) × .A)

孔内的表达式类型为List (Fin (suc (.m + length xs)) × .A)

证明两种类型相等很容易,但也很脏.这是一个常见的问题:一个参数变大而另一个变小,所以我们需要定义可交换的 _+_ 来处理这两种情况,但没有办法定义它.解决方案是使用 CPS:

It's easy to prove that two types are equal, but it's also dirty. This is a common problem: one argument grows and the other lowers, so we need definitionally commutative _+_ to handle both the cases, but there is no way to define it. The solution is to use 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))),在当前上下文中是无人居住的,所以介绍一些居民:

(k ∘ suc) (length xs) is the same thing as k (length (x ∷ xs)), hence the mismatch is fixed, but what is i now? The type of the hole is Fin (k (suc (length xs))) and it's uninhabited in the current context, so let's introduce some inhabitant:

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 必须在每次递归调用时增长.但是 suck 不通勤,所以 suc iFin (suc (k (suc (_n_65 kix xs))))).所以我们在k下添加了suc的另一个参数,最终定义为

The type of the new hole is {n : ℕ} → Fin (k (suc (suc n))). We can fill it with i, but i must grow at each recursive call. However suc and k doesn't commute, so suc i is Fin (suc (k (suc (_n_65 k i x xs)))). So we add another argument that sucs under k, and the final definition is

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 (kn) → Fin (k (suc n)) 可以被视为 {n : ℕ} → Fin (k (suc n)) → Fin (k (suc (suc n))).

which works, because s : {n : ℕ} → Fin (k n) → Fin (k (suc n)) can be treated as {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:


Now note that in enumerate-Fin k always follows Fin in the types. Hence we can abstract Fin ∘ k and get a generic version of the function that works with both and 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`s枚举列表的元素?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!

1403页,肝出来的..

09-09 00:58