スタックの話：仕様と実装とテスト - 檜山正幸のキマイラ飼育記 (はてなBlog)

【注意】2022年3月より、MathJaxまたは「はてなブログ」の仕様変更またはバグにより、MathJax/XyJaxを使った数式・図が表示できなくなりました。そのため、一部の数式・図は表示できなくなっています（ソースコードが見えます）。新しいタブまたはウィンドウに、この記事のURLを貼り付けて開くと見えることがあります（ダメなときもあります）。もし、表示できていれば、この注意書きは無視してください。

$\newcommand{mrm}[1]{ \mathrm{#1} }$ 小ネタ。雑感。

内容：

無法則スタックと有法則スタック
法則とテストコード
問題点

無法則スタックと有法則スタック

「有法則代数と無法則代数」に書いたように、「無法則〈lawless〉／有法則〈lawful〉」という言葉は便利です。

無法則なスタックの指標を書いてみると：

signature LawlessStack {
  sort S // state
  sort V // value
  operation pop:S → S×V
  operation push:S×V → S
}

オブジェクト指向言語（typescript）のインターフェイスとして書いてみましょう。状態 S の値はオブジェクトの this で参照するので、暗黙化〈隠蔽〉されます。スタックに積む値の型 V は型パラメータにします。

interface LawlessStack<V> {
    // 自分の状態の型 S は暗黙化される。
    pop():V;
    push(v:V):void;
}

無法則なので、メソッド名さえあっていればどんな実装をしてもかまいません。例えば：

class MyNumStack implements LawlessStack<number> {
    pop():number {
        return 7;
    }
    push(v:number) {
        ;
    }
}

ウーム、これじゃスタックらしくないですね。“スタックらしさ”を表現する法則を入れてみましょう。

signature LawfulStack {
  sort S // state
  sort V // value
  operation pop:S → S×V
  operation push:S×V → S

  equation push_pop :: phsh;pop = id_(S×V)
  equation pop_push :: pop;push = id_S
}

等式的法則を集合圏内の可換図式で書くなら：

$\xymatrix{ {S\times V} \ar[r]^-{\mrm{push}} \ar@{=}[dr]_{\mrm{id}_{S\times V}} & {S} \ar[d]^{\mrm{pop}} \\ {} & {S\times V} }\\ \text{commutative in }{\bf Set}\\ \:\\ \xymatrix{ {S} \ar[r]^-{\mrm{pop}} \ar@{=}[dr]_{\mrm{id}_{S}} & {S\times V} \ar[d]^{\mrm{push}} \\ {} & {S} }\\ \text{commutative in }{\bf Set}$

これらの法則は形が簡単でいいのですが、スタックが空のときの挙動をうまく表現できません。今は、理想化して無限に深いスタックを考えましょう。いくらポップしても空にはならないとします。そういう理想的状況では、push_pop法則とpop_push法則がスタックが満たすべき等式的法則だと言っていいでしょう。

法則とテストコード

さてところで、ほとんどのプログラミング言語では、インターフェイスに法則を書くことができません。どうしましょう？法則の代わりにテスト用メソッドを入れておくことにしますか。

まず、要素に言及せずに（ポイントフリーに）書かれた法則を、変数を使った論理式に書き換えます。 $\pi^1, \, \pi^2$ は第一射影、第二射影です。

$\text{push_pop law} :\\ \quad \forall (s, v)\in S\times V.\, \mrm{pop}(\mrm{push}(s, v)) = (s, v)\\ \text{pop_push law} :\\ \quad \forall s\in S.\, \mrm{push}(\pi^1_{S, V}(\mrm{pop}(s)), \pi^2_{S, V}(\mrm{pop}(s)) ) = s$

論理式の $\forall$ （すべての～）を確認するのは無理*1なので、有限個の状態・値で確認してね、ってことになります。

有限のケースで確認はしょうがないのですが、「状態が変わってない」をどうやって確認しましょうか？ある時点の状態をデータとして取り出せて、それを保存できて、なおかつ状態データの等値比較（イコールの判定）ができれば、「状態が変わってない／変わった」を確認できます。

しかし一般には、状態を等値比較可能なデータとして取り出すのはなかなか難しいです。‥‥‥ 諦めましょ。状態は変えずにスタックトップの値にアクセスするメソッド peek() を準備してもらう前提で、状態全体は調べないでスタックトップだけテストするメソッドを書きます。

abstract class LawfulStack<V> implements LawlessStack<V> {
    abstract pop():V;
    abstract push(v:V):void;
    abstract peek():V;

    push_pop_valueTest(v:V):boolean {
        this.push(v);
        let w:V = this.pop();
        return v == w;
    }
    pop_push_valueTest():boolean {
        let w:V = this.pop();
        this.push(w);
        return w == this.peek();
    }
}

問題点

スタックは、誰でも知っている簡単なデータ構造です。しかし、スタックがスタックとして正しく振る舞うことを記述したり確認することは意外に大変です。

「いくらポップしても空にはならない」と仮定しましたが、そんなスタックはありません。状態は変えずに空かどうかを調べるメソッド isEmpty() を追加して、スタックが空のときの挙動も（ある程度は）記述する必要があります。

状態が変わってないことの確認は諦めました。が、諦めちゃダメなこともあるでしょう。それに、peek() や isEmpty() の仕様として「状態は変えずに‥‥」を要求しましたが、状態を変えないことを誰がどうやって保証するのでしょう？

解決策を提示せずに無責任なことを言って今日は終わります：法則を記述する、法則を守らせる、法則を守っていることを確認する、法則を守っていることを保証するって難しいですね。

*1:コンピュータ内に作れる状態は有限ですが、あまりに数が多いので事実上無限だとみなします。