PFDS 償却計算量 求め方

償却計算量 求め方

『Purely Functional Data Structures』の5章6章に似た言葉・概念が頻出して混乱してきたのでまとめておきます。
個人用メモに近いので、予備知識のない方がこれを読んで何か有用な知識を得られたりすることはないと思います。

償却解析のテクニック(PFDS 5章)

• ∑[i=1..j]amortized_cost(j) >= ∑[i=1..j]actual_cost(j)
  • どのような j をとっても上記を満たすことができれば、 amortized bounds を証明できる
• accumulated savings = accumulated amortized costs - accumulated actual costs
  • accumulated savings が非負である限り、accumulated amortized costs は accumulated actual costs の上限となる
• 償却解析における個々の操作のコスト
  • expensive: actual cost が amortized cost を上回る(accumulated savings を減少させる)場合
  • cheap : actual cost が amortized cost を下回る(accumulated savings を増加させる)場合
• accumulated savings がそのコストをまかなえるほど蓄積されていない限り expensive な操作が実行されないと示されたい
  • 示すことができれば amortized bounds を証明できる
• 以下に2つの証明テクニックを紹介する

Banker's method

• accumulated savings をデータ構造の個々の location における credits とみなす
• amortized_cost(i) = actual_cost(i) + allocated_credits(i) - spent_credits(i)
  • ∑allocated_credits(i) >= ∑spent_credits(i)
    • すべての credit は消費される前に蓄積されている必要がある
    • 同じ credit が複数回消費されることはない
  • したがって ∑amortized_cost(i) >= ∑actual_cost(i)
• banker's method を用いた証明を行うときは上記を満たすような credit invariant を定義する

Queue implemented by paired lists の場合

• credit invariant
  • rear list (追加する方)の要素を個々の credit とする
• credit を増減させる操作は以下
• snoc if queue is non-empty
  • actual cost は 1
  • credit が1つ増えるので amortized cost = 2 (cheap な操作)
• tail with reverse
  • 長さ m の rear list を reverse するコストを含めて m + 1 の actual cost
  • 一方で rear list が消えるので credit が m 減る
  • amortized cost = m + 1 - m = 1 (expensive な操作)

Physicist's method

• 関数 Φ を、各オブジェクトを potential と呼ばれる実数に変換する関数とする
  • 初期化直後のデータ構造に適用した場合の値は 0 とすることが多い
  • 常に非負
  • potential は accumulated savings の下限となる
• d(i) を i 番目の操作の出力、 i + 1 番目の操作の入力とした場合
  • amortized_cost(i) = actual_cost(i) + Φ(d(i)) - Φ(d(i - 1))
  • ∑[i=1..j]actual_cost(i) = ∑[i=1..j]amortized_cost(i) + Φ(d(0)) - Φ(d(j))
• Φ(d(0)) が 0、Φ(d(j)) が非負となるような Φ を定義すれば amorized bounds を示すことができる

Queue implemented by paired lists の場合

• potential 関数
  • Φ(queue) = queue の rear list の長さ
• potential を増減させる操作は以下
• snoc if queue is non-empty
  • actual cost は 1
  • potential が 1 増加
  • amortized cost は 2 (cheap な操作)
• tail with reverse
  • 長さ m の rear list を reverse するコストを含めて m + 1 の actual cost
  • rear list が消えるので potential は m 減少
  • amortized cost は m + 1 - m = 1 (expensive な操作)

永続版償却解析のテクニック(PFDS 6章)

• 5章で紹介したデータ構造は persistently に使われると計算量が増す
  • 6章では遅延評価を利用して上記の問題を解決したデータ構造が紹介されている
  • 以下はそのようなデータ構造に対する償却解析の方法の話
• 詳しくはこちら

Execution Traces and Logical Time

• execution traces: 更新操作をノードとして表現した有向グラフ
• logical history: 更新操作ノードが依存する操作の集合
• logical future: 更新操作ノードから終点へのパス
• 以下特定のオブジェクトに対するlogical history、logical future という言葉を使う場合がある
  • そのオブジェクトが生成された操作に対する logical history、logical futureという意味

Reconciling Amortization and Persistence

• accumulated savings の代わりに accumulated debt という概念を導入
  • debt = 評価されず遅延されている操作のコスト
  • savings は1度しか消費できないけど debt は複数回清算できる
  • accumulated debt の初期値は 0

遅延データ構造解析フレームワーク

• ある操作に対するコストの定義
  • unshared cost: サスペンションが force 及びメモ化されている場合にかかるコスト
  • shared cost: その操作が生成したサスペンションを実行するのにかかるコスト
  • complete cost = unshared cost + shared cost
  • unshared cost <= actual cost <= complete cost
  • amortized cost = unshared cost + その操作によって清算された accumulated debt
• ある一連の操作に対するコストの定義
  • realized costs: shared costの合計のうち実行された分
  • unrealized costs: shared costの合計のうち実行されなかった分
  • total actual cost = unshared costs + realized costs
• サスペンションが属する debt が完全に清算されるまで、そのサスペンションは force できない
  • ↑の場合、debt の総量が realized shared cost の上限となる
  • したがって、amortized cost の合計が actual cost の合計の上限となる

Banker's method for accumulated debt

• accumulated savings バージョンから accumulated debt バージョンへのアップデート
• credits を debits に置き換えて考える
  • debits はサスペンドされたタスクのコスト
• 計算がサスペンドされた場合、その shared costs と同等の debits を作成する
  • そのうちの各 debit をデータ構造のどこかの location に対応させる
    • モノリシックな計算であればすべての debits がその計算結果のルートに割り当てられる
    • インクリメンタルな計算であれば個々の計算結果のルートに分散されて割り当てられる
• amortized cost = unshared cost + 支払われた debits
  • 作成された debits は amortized cost に含まれない
• amortized bounds を証明するには
  • ある location にアクセスする(サスペンションを実行する)とき、それに関する debits が完済されていることを示せばよい
  • debits はすぐにアクセスされるであろうノードに割り当てられてるものから支払っていく
  • そうすると清算済み debits の合計が realized shared costs の上限となるので OK
  • 未清算 debits は unrealized shared costs に対応

Queue implemented by paired streams の場合

• d(i) = i番目のノードの front stream の debits
• D(i) = ∑[j=0..i]d(j)
• debit invariant
  • D(i) <= min(2i, |f| - |r|)
  • 2i は front stream の最初のノードの debits が清算済みであることを保証する
  • |f| - |r| はすべての debits がローテーションされる直前のタイミングで清算済みとなることを保証する
• debits を増減させる操作は以下
• snoc without rotation
  • |r| が 1 増えるので |f| - |r| が 1 減少
  • D(i) が |f| - |r| だった場合に debit invariant に違反するので、
    • キューの最初の debit を清算することで debit invariant を維持する
• tail without rotation
  • |f| が 1 減るので |f| - |r| が 1 減少
  • 残りノードの i(index) がそれぞれ 1 減るので、 2i が 2減る
  • したがってキューの debits を2つ清算することで、 debit invariant を維持する
• snoc or tail with rotation
  • ローテーション直前にすべての debits が清算済みであることは debit invariant が保証している
  • したがってローテーション後の未清算 debits はローテーションにかかるコスト
    • |f| = m, |r| = m + 1 とすると
    • append のために m, reverse のために m + 1 の debits が加算される
    • append はインクリメンタルな操作なので、最初の m ノードに分散して割り当てる
    • reverse はモノリシックな操作なので、インデックス m のノードに m + 1 すべてを割り当てる
  • したがって debits の分配は
    • d(i) = 1 if i < m
    • d(i) = m + 1 if i = m
    • d(i) = 0 if i > m
  • したがって
    • D(i) = i + 1 if i < m
    • D(i) = 2m + 1 if i >= m
  • 0 と m の場合 debit invariant が壊れるが、ノード 0 の debit を清算することで治る

Physicist's method for accumulated debt

• Φ の代わりに Ψ を導入
  • accumulated debt の上限に変換するポテンシャル関数
  • accumulated debt の変化はすべてこの関数に反映される
• amortized cost = complete cost - ポテンシャルの変化
  • = unshared cost + shared cost - ポテンシャルの変化
  • 一切の shared costs が清算されない場合、ポテンシャルは shared cost 分増える
    • amoritzed cost = unshared cost + shared cost - shared cost = unshared cost
    • accumulated debt は shared cost 分増加
  • shared costs を精算する場合、ポテンシャルの変化 <= shared cost の範囲でポテンシャルが変化
    • amortized cost = unshared cost + shared cost - ポテンシャルの変化 > unshared cost
• banker's method と違い、 physicist's method は accmulated debt 全体を支払うまでサスペンションを force できない

Queue implemented by paired lists の場合

• potential 関数
  • Ψ(q) = min(2|w|, |f| - |r|)
    • suspended list を force するタイミングで0となる
      • working copy が 空の場合
      • front list < rear list となる場合
• ポテンシャルが変化する操作は以下
• snoc without rotation
  • |r| が 1 増えるのでポテンシャル(|f| - |r|)が 1 減少
  • amortized cost = 1 + 0 - (-1) = 2
• snoc with rotation
  • |f| = m, |r| = m + 1
  • shared costs は「f ++ reverse r」にかかる 2m + 1
  • 操作前のポテンシャルは 0、操作後のポテンシャルは 2|w| = 2m
  • amortized cost = 1 + (2m + 1) - 2m = 2
• tail without rotation
  • |w| と |f| - |r| が 1 減少
    • ポテンシャルは 2 減少
  • suspended list を遅延 tail するので shared cost は1
  • amortized cost = 1 + 1 - (-2) = 4
• tail with rotation
  • |f| = m, |r| = m + 1
  • unshared costs は 2
    • working copy への tail
    • front list への tail(rotation 時に force される)
  • shared costs は「f ++ reverse r」にかかる 2m + 1
  • 操作前のポテンシャルは 0、操作後のポテンシャルは 2|2| = 2m
  • amortized cost = 2 + (2m + 1) - 2m = 3