Think Stitch
PRINCIPIA  最近の更新


有界な自然数からなるリストの自然数へのエンコーディング 3

有界な自然数からなるリストの自然数へのエンコーディングの3回目です.前2回はこちらです:

前2回では,リストを自然数にエンコードする関数 enc とデコードする関数 dec を定義して,互いに逆関数であることを証明しました. 今回はエンコードとデコードをする命令型のプログラムを書いて,正当性を証明したいと思います.

関数 enc と dec の定義を再掲しておきます.今回はこれらが仕様になります.

fun enc :: "nat => nat list => nat" where
  "enc M [] = 0" |
  "enc M (c#cs) = 1 + c + M * (enc M cs)"
fun dec :: "nat => nat => nat list" where
  "dec M 0 = []" |
  "dec M (Suc x) = (x mod M) # (dec M (x div M))"

エンコードプログラムの部分正当性証明

エンコードする命令型のプログラムを書きます. 入力は自然数を格納したリスト v とします.エンコード結果は変数 x に入れるものとします. そうすると事後条件は

x = enc M v

と表すことができます.

ループ変数 k は配列のインデックスの大きい方から 0 に向って変化させることにします. 配列の後ろの方が M のより大きな指数に対応するので,こうした方がシンプルになります.

ループ不変条件は典型的な累積型のループ不変条件です.

k <= length v & x = enc M (drop k v)

関数 drop k v はリスト v の先頭から k 個の要素を取り除いた残りのリストを表します. 初期状態では k = length v なので drop k v = [] です. enc M [] = 0 ですから x の初期値 0 と一致してループ不変条件が成り立ちます.

ループを実行するにしたがって徐々に k が減っていくとエンコードされた範囲が広がっていって,k = 0 で事後条件 x = enc M v と一致します.

lemma
  "VARS x k
  {True}
  x := 0;
  k := length v;
  WHILE k > 0
  INV {k <= length v & x = enc M (drop k v)}
  DO
    k := k - 1;
    x := 1 + x * M + v!k
  OD
  {x = enc M v}"

では証明します.vcg コマンドで命題に変換してからちょっと整理すると次のようになります.

apply(vcg)
apply(auto)
apply(case_tac k)
apply(auto)
apply(rename_tac n)
------------------------------
goal (1 subgoal):
 1. !!n. Suc n <= length v
         ==> Suc (enc M (drop (Suc n) v) * M + v ! n) =
             enc M (drop n v)

残ったゴールを対象レベルに変換して補題 enc_0 を作ります. リスト v に対して数学的帰納法を適用します.

lemma enc_0 [rule_format]:
  "ALL n. n < length v -->
   Suc (enc M (drop (Suc n) v) * M + v ! n) = enc M (drop n v)"
apply(induct_tac v)
apply(auto)
apply(case_tac n)
apply(auto)
done

できた補題を適用すれば証明は完成です.dec_enc 同様,こちらは簡単でした.

lemma
  "VARS x k
  {True}
  x := 0;
  k := length v;
  WHILE k > 0
  INV {k <= length v & x = enc M (drop k v)}
  DO
    k := k - 1;
    x := 1 + x * M + v!k
  OD
  {x = enc M v}"

apply(vcg)
apply(auto)
apply(case_tac k)
apply(auto)
apply(rename_tac n)
apply(rule enc_0)
apply(auto)
done

デコードプログラムの部分正当性証明

つづいてデコードの命令型プログラムを書きます. 入力はコード化された値 C とします. 出力は自然数のリストで,変数 v に格納することにします. 事後条件は

v = dec M C

となります. リストは逆順に生成されるので,最後で逆転することにします.

デコードプログラムのループ不変条件はエネルギー保存型のループ不変条件としました.

(rev v) @ (dec M x) = dec M C

右辺の dec M C は定数で,かつ求めるリストを表しています. 左辺は2項 rev v と dec M x からなります. 初期状態では v = [], x = C です. ループが進むにしたがい徐々に v が伸びて,dec M x が短くなっていき,最後は dec M x = [] となって事後条件(で v を逆転したもの)と一致します.

lemma
  "M > 0 ==>
  VARS x v
  {True}
  x := C;
  v := [];
  WHILE x > 0
  INV {(rev v) @ (dec M x) = dec M C}
  DO
    x := x - 1;
    v := (x mod M) # v;
    x := x div M
  OD;
  v := rev v
  {v = dec M C}"

では証明します.まず vcg コマンドで命題に変換して auto で整理します.

apply(vcg)
apply(auto)
------------------------------
goal (1 subgoal):
 1. !!x v.
       [| 0 < M; rev v @ dec M x = dec M C; 0 < x |]
       ==> rev v @
           (x - Suc 0) mod M # dec M ((x - Suc 0) div M) =
           dec M C

前2回の関数型プログラムについての証明で補題を作ってあるので,ここから先はほぼ機械的にできます. 証明の構造は enc_dec と同じになります. まず二重帰納法が適用できる形に変換します. あとはゴールを対象レベルに変換した補題を作り,n, k に対して順番に帰納法を適用していきます.

上のゴールを対象レベルに変換して補題 dec_0 とします. 二重帰納法が適用できる形に変換する規則 F_ind を適用します.

lemma dec_0 [rule_format]:
  "0 < M ==>
   x > 0 -->
    (x - Suc 0) mod M # dec M ((x - Suc 0) div M) = dec M x"
apply(rule_tac x="x" in F_ind)
apply(assumption)
apply(rule impI)
------------------------------
goal (1 subgoal):
 1. !!n k.
       [| 0 < M; k < M ^ n; 0 < F M n + k |]
       ==> (F M n + k - Suc 0) mod M #
           dec M ((F M n + k - Suc 0) div M) =
           dec M (F M n + k)

対象レベルに変換して補題 dec_1 とします. n に対して数学的帰納法を適用します.

lemma dec_1 [rule_format]:
  "0 < M ==>
  ALL k. k < M ^ n & 0 < F M n + k -->
    (F M n + k - Suc 0) mod M # dec M ((F M n + k - Suc 0) div M)
  = dec M (F M n + k)"
apply(induct_tac n)
apply(auto)
------------------------------
goal (1 subgoal):
 1. !!n k.
       [| 0 < M;
          ALL k.
             k < M ^ n & (0 < F M n | 0 < k) -->
             (F M n + k - Suc 0) mod M #
             dec M ((F M n + k - Suc 0) div M) =
             dec M (F M n + k);
          k < M * M ^ n |]
       ==> (F M n + M ^ n + k - Suc 0) mod M #
           dec M ((F M n + M ^ n + k - Suc 0) div M) =
           dec M (F M n + M ^ n + k)

再び対象レベルに変換して補題 dec_2 とします. こんどは k に対して数学的帰納法を適用します.

lemma dec_2  [rule_format]:
  "0 < M ==>
    (ALL k.
     k < M ^ n & (0 < F M n | 0 < k) -->
     (F M n + k - Suc 0) mod M # dec M ((F M n + k - Suc 0) div M) =
     dec M (F M n + k)) -->
     k < M * M ^ n 
    --> (F M n + M ^ n + k - Suc 0) mod M #
     dec M ((F M n + M ^ n + k - Suc 0) div M) =
     dec M (F M n + M ^ n + k)"
apply(induct_tac k)
apply(auto)
apply(unfold F_div)
apply(unfold F_mod_0)
apply(subgoal_tac "Suc (F M n + M^n - Suc 0) = F M n + M^n")
apply(rotate_tac -1)
apply(erule_tac t="F M n + M^n" in subst)
apply(subst dec.simps)
apply(unfold F_div)
apply(unfold F_mod_0)
apply(auto)
done

補題 dec_1 に戻って dec_2 を適用します.

lemma dec_1 [rule_format]:
  "0 < M ==>
  ALL k. k < M ^ n & 0 < F M n + k -->
   (F M n + k - Suc 0) mod M # dec M ((F M n + k - Suc 0) div M)
 = dec M (F M n + k)"
apply(induct_tac n)
apply(auto)
apply(rule dec_2)
apply(auto)
done

補題 dec_0 に戻って dec_1 を適用します.

lemma dec_0 [rule_format]:
  "0 < M ==>
   x > 0 -->
    (x - Suc 0) mod M # dec M ((x - Suc 0) div M) = dec M x"
apply(rule_tac x="x" in F_ind)
apply(assumption)
apply(rule impI)
apply(rule dec_1)
apply(auto)
done

補題 dec_0 を適用して証明完了です.

lemma
  "M > 0 ==>
  VARS x v
  {True}
  x := C;
  v := [];
  WHILE x > 0
  INV {(rev v) @ (dec M x) = dec M C}
  DO
    x := x - 1;
    v := (x mod M) # v;
    x := x div M
  OD;
  v := rev v
  {v = dec M C}"

apply(vcg)
apply(auto)
apply(subst dec_0)
apply(auto)
done

コメント

エンコードする命令型プログラムの正当性証明では,「リストの要素はすべて M 未満である」という事前条件が必要な気がしませんか? :P

2015/01/31
© 2013,2014,2015 PRINCIPIA Limited