# 可持久化雙向隊列 Persistent Deque 續

## 預先評估雙向隊列 (Pre-Evaluation)

• SIMPLE AND EFFICIENT PURELY FUNCTIONAL QUEUES AND DEQUES, Chris Okasaki, 1995

### Invariants

\begin{aligned} & |L| \le c |R| + 1 \; \wedge \; |R| \le c |L| + 1\\ & |\hat{L}| \le \max(2j+2-k, 0) \; \wedge \; |\hat{R}| \le \max(2j+2-k, 0) &\\ & \text{where} \; j = \min(|L|, |R|) \; \wedge \; k = \max(|L|, |R|) \end{aligned}

### Functional Definition

\begin{align} \left [ \; \right ]_{d} &= \left \langle \left [ \; \right ], \left [ \; \right ], \left [ \; \right ], \left [ \; \right ] \right \rangle \\ |\left \langle L, R, \hat{L}, \hat{R}\right \rangle| &= |L| + |R| \\ \textit{insert}L(e, \left \langle L, R, \hat{L}, \hat{R}\right \rangle) &= \textit{makedq}\left \langle e:L, R, \textit{tl}\; \hat{L}, \textit{tl}\; \hat{R}\right \rangle \\ \textit{insert}R(e, \left \langle L, R, \hat{L}, \hat{R}\right \rangle) &= \textit{makedq}\left \langle L, e:R, \textit{tl}\; \hat{L}, \textit{tl}\; \hat{R}\right \rangle \\ \textit{remove}L\left \langle L, R, \hat{L}, \hat{R}\right \rangle &= \left \langle \textit{hd}\; R, \left [ \; \right ]_d \right \rangle & \left \{ |L| = 0 \right \}\\ &= \left \langle \textit{hd}\; L, \textit{makedq} \left \langle \textit{tl} \; L, R, \textit{tl} \; (\textit{tl} \hat{L}), \textit{tl} \; (\textit{tl} \hat{R}) \right \rangle \right \rangle & \left \{ |L|> 0 \right \}\\ \textit{remove}R\left \langle L, R, \hat{L}, \hat{R}\right \rangle &= \left \langle \textit{hd}\; L, \left [ \; \right ]_d \right \rangle & \left \{ |R| = 0 \right \}\\ &= \left \langle \textit{hd}\; R, \textit{makedq} \left \langle L, \textit{tl} \; R, \textit{tl} \; (\textit{tl} \hat{L}), \textit{tl} \; (\textit{tl} \hat{R}) \right \rangle \right \rangle & \left \{ |R|> 0 \right \}\\ \textit{makedq}\left \langle L, R, \hat{L}, \hat{R}\right \rangle &= \left \langle \hat{L}, \hat{R}, \hat{L}, \hat{R} \right \rangle, \; \begin{aligned} \text{let} \; n &= \left \lfloor (|L| + |R|)/2 \right \rfloor \\ L' &= \textit{take}(n, L) \\ R' &= \textit{rot1}(n, R, L) \end{aligned} & \left \{ |L| > c |R| + 1 \right \} \\ &= \left \langle \hat{L}, \hat{R}, \hat{L}, \hat{R} \right \rangle, \; \begin{aligned} \text{let} \; n &= \left \lfloor (|L| + |R|)/2 \right \rfloor \\ L' &= \textit{rot1}(n, L, R) \\ R' &= \textit{take}(n, R) \end{aligned} & \left \{ |R| > c |L| + 1 \right \} \\ &= \left \langle L, R, \hat{L}, \hat{R} \right \rangle & \left \{ \text{otherwise} \right \} \\ \textit{rot1}(n, L, R) &= \textit{hd} \; L : \; \textit{rot1}(n-c, \textit{tl}\; L, \textit{drop}(c, R)) & \left \{ n \ge c \right \} \\ &= \textit{rot2}(L, \textit{drop}(n, R), \left [ \; \right ]) & \left \{ n < c \right \} \\ \textit{rot2}(L, R, A) &= \textit{hd}\; L : \; \textit{rot2}(\textit{tl}\; L, \textit{drop}(c, R), \textit{rev}(\textit{take}(c, R)) + A) & \left \{ |L| > 0 \wedge |R| \ge c \right \} \\ &= L + \textit{rev}R + A & \left \{ |L| = 0 \vee |R| < c \right \} \end{align}