スタック

スタックとは、次の操作をもつ抽象データ型である。値の型を $X$、スタックの全体を $\mathcal{S}$ と書く。

• $\mathrm{empty} \in \mathcal{S}$（空のスタック）
• $\mathrm{push} : \mathcal{S} \times X \to \mathcal{S}$（積む）
• $\mathrm{pop} : \mathcal{S} \to \mathcal{S}$（頂上を取り除く）
• $\mathrm{top} : \mathcal{S} \to X$（頂上を読む）
• $\mathrm{isEmpty} : \mathcal{S} \to \{\mathrm{true}, \mathrm{false}\}$

これらは任意の $S \in \mathcal{S}$、$x \in X$ について次の公理を満たす。

$\mathrm{top}(\mathrm{empty})$ と $\mathrm{pop}(\mathrm{empty})$ は定義されない（実装ではエラーとする）。