# 可持久化堆疊 操作 Persistent Stack Operators

## 串接 Append

\begin{aligned} \left [ \; \right ]_{\textit{append}} &= \left \langle \left [ \; \right ], \left [ \; \right ] \right \rangle \\ \\ |\left \langle T, \; B \right \rangle | &= |T| + |B| \\ \\ \textit{push} \; (\textit{e}, \left \langle T, \; B \right \rangle) &= \left \langle e : T, \; B \right \rangle \\ \\ \textit{pop} \; (\left \langle T, \; B \right \rangle) &= \left \langle \text{hd} \; T, \left \langle \text{tl} \; T, \; B \right \rangle \right \rangle & \{ |T| > 0 \} \\ &= \left \langle \text{hd} \; B, \text{tl} \; B \right \rangle & \{ |T| = 0 \} \end{aligned}

## 提取 Take

\begin{aligned} \left [ \; \right ]_{\textit{take}} &= \left \langle 0, X \right \rangle \\ \\ |\left \langle n, X \right \rangle | &= n \\ \\ \textit{push} \; (\textit{e}, \left \langle n, X \right \rangle) &= \text{Append}(e,\; \left \langle n, X \right \rangle) \\ \\ \textit{pop} \; (\left \langle n, X \right \rangle) &= \left [ \; \right ] & \{ n = 1 \} \\ &= \left \langle \text{hd} \; X, \left \langle n-1, \text{tl} \; X \right \rangle \right \rangle & \{ n > 1 \} \end{aligned}

## 移除 Drop

\begin{aligned} \text{Drop} \; (n, X) &= X & \{ n = 0 \} \\ &= \text{Drop} \; (n-1, X) & \{ n > 1\} \end{aligned}

## 反轉 Rev

\begin{aligned} \text{Rev} \; (X) &= \text{Rev}'(X, \left [ \; \right ]) & \\ \\ \text{Rev}'(X, A) &= A & \{ |X| = 0\} \\ &= \text{Rev}' \; (\text{tl} \; X, \text{hd} \; X : A) & \{ |X| > 0\} \end{aligned}

## 參考資料

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

## 來點題目 《記憶中的堆疊》

### 題目描述

• 0 v: 退回版本 v
• 1 x: 在當前堆疊，push x 到堆頂
• 2: 印出當前堆疊狀態