接續前一篇 《可持久化雙向隊列 Persistent Deque 序》，同樣的概念，Okasaki 用了他那精妙的公式描述了前一篇採用的策略只不過是常數 $c = 3$ 的情況，實際上可以根據需求去改變常數 $c$，先決條件 $c \ge 2$。
預先評估雙向隊列 (Pre-Evaluation)
- SIMPLE AND EFFICIENT PURELY FUNCTIONAL QUEUES AND DEQUES, Chris Okasaki, 1995
同樣地，雙向隊列為兩個堆疊表示，並限制其中一個大小不能大於另一個的 $c$ 倍，如果發生了用另一種方式表示部分翻轉的結果。
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}$$放眼望去共計 15 條式子，而一半都是對稱操作。唯獨在式 12 到 式 15 較為特別，相當於前一篇的反轉操作，只是我們透過額外的定義來描述它，實作時相當多一個類別。不管是記憶體分析、還是時間複雜度分析，原則上與前一篇是相同的。
公式裡描述了一堆的 $\hat{L}, \; \hat{R}$，我們卻沒有在任何的條件式中使用，只作為我們去理解操作的含意。因此，實作時只在 $makedq$ 區域變數中作用，並不會成為一個必要紀錄的值。
特別注意到建構子中，令 $R' = \textit{rot1}(n, R, L)$，這個操作可能直接成為 $\textit{rot2}(L, \textit{drop}(n, R), \left [ \; \right ])$，思維必須往前看一步去轉化所有實際的類別，否則很容易在相關操作退化。因為 $L, \; R$ 都是作為 rot1 或者是 rot2 後的產物，盡可能地使之成為最簡單的表達式。