为什么 catenable 列表的 append 和 uncons 只是摊销 O(1)？

Question

我采用了 Okasaki 的可连接列表实现，并对其进行了一些重构以避免布尔盲目性问题。除此之外，数据结构本身保持不变：

functor CatList (Q : QUEUE) :> CAT_LIST =
struct
  (* private stuff, not exposed by CAT_LIST *)

  structure L = Lazy
  structure O = Option  (* from basis library *)

  datatype 'a cons = ::: of 'a * 'a cons L.lazy Q.queue

  infixr 5 :::

  (* Q.snoc : 'a Q.queue * 'a -> 'a Q.queue *)
  fun link (x ::: xs, ys) = x ::: Q.snoc (xs, ys)

  (* L.delay : ('a -> 'b) -> ('a -> 'b L.lazy)
   * L.force : 'a L.lazy -> 'a
   * Q.uncons : 'a Q.queue -> ('a * 'a Q.queue lazy) option *)
  fun linkAll (xs, ys) =
    let
      val xs = L.force xs
      val ys = L.force ys
    in
      case Q.uncons ys of
          NONE => xs
        | SOME ys => link (xs, L.delay linkAll ys)
    end

  (* public stuff, exposed by CAT_LIST *)

  type 'a list = 'a cons option

  val empty = NONE

  (* L.pure : 'a -> 'a L.lazy *)
  fun append (xs, NONE) = xs
    | append (NONE, xs) = xs
    | append (SOME xs, SOME ys) = SOME (link (xs, L.pure ys))

  (* Q.empty : 'a Q.queue *)
  fun cons (x, xs) = append (SOME (x ::: Q.empty), xs)
  fun snoc (xs, x) = append (xs, SOME (x ::: Q.empty))

  (* O.map : ('a -> 'b) -> ('a option -> 'b option) *)
  fun uncons NONE = NONE
    | uncons (SOME (x ::: xs)) = SOME (x, L.delay (O.map linkAll) (Q.uncons xs))
end

Okasaki 在他的书中声称，给定具有 O(1) 操作（最坏情况或摊销）的队列的实现，append 和 uncons 被摊销 O(1).

为什么他的主张不能加强？给定实时队列的实现（所有操作都是最坏情况 O(1)），append 和 uncons 在我看来是最坏情况 O(1)。 linkAll 中的所有递归调用都由 L.delay 保护，并且 public 操作的 none 曾经强制不止一次暂停。我的推理（或我的代码）有误吗？

Answer 1

不可变（纯函数式）队列只有 O(1) 的构造函数和析构函数。

http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp95queue.pdf

Answer 2

关于您关于可连接列表的问题。您还需要考虑到强制暂停可能会导致一连串的力量。请注意 linkAll 强制其输入列表，这可能是一个尚未评估的暂停 's'。强制 's' 可能会反过来强制另一个暂停，依此类推。如果您对列表执行一系列 uncons 操作，确实会发生这种情况。最终，最多在 'n' uncons 操作之后，数据结构可能会退化为朴素的 Cons 列表 (Cons(x, Cons(y, ...)))，其中'n' 是列表的大小。任何进一步的 uncons 操作都将具有常数时间。因此，数据结构确实有一个分摊常数时间界限，但这不是最坏的情况。

为什么 catenable 列表的 append 和 uncons 只是摊销 O(1)？

Why are append and uncons for catenable lists merely amortized O(1)?

data-structures

sml

ml

purely-functional