Think Stitch
PRINCIPIA  最近の更新


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

あらかじめ定めた自然数 \(M > 0\) に対して, \(0 \le k < M\) の範囲にある自然数からなるリストを1つの自然数で表す次のような方法について考えます.

リスト cs の長さが L のとき,これを M 進数の表現と見なせば,次の自然数で表すことができます. \[ x = G(cs) = c_0 + c_1 M + c_2 M^2 + \ldots + c_{L-1} M^{L-1} = \sum_{0 \le i < L} c_i M^i \] ここで ci はリストの要素です.x の値の範囲は \[ 0 \le x < M^L \] となります.これを L = 0 から順番に,重ならないようにずらしながら並べれば,任意の長さのリストを自然数に変換できたことになります.

L値の範囲
0x = 0
11 <= x < 1 + M
21 + M <= x < 1 + M + M2
31 + M + M2 <= x < 1 + M + M2 + M3
......

各 L に対応する値の範囲の下限を F(L) で表すことにします. \[ F(L) = 1 + M + M^2 + \ldots + M^{L-1} = \sum_{0 \le i < L} M^i \] これを使うと値の範囲の上限は F(L + 1) になることがわかります. すると表は次のように少し見やすい形になります.

L値の範囲
0F(0) <= x < F(1)
1F(1) <= x < F(2)
2F(2) <= x < F(3)
3F(3) <= x < F(4)
......
LF(L) <= x < F(L + 1)
......

エンコード関数 enc

リストを自然数にエンコードする関数 enc を定義します.[] は空リスト,# はリストの cons です.

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

この定義はそれほど自明ではないように思われます.そこで,上の定義との関係を調べてみます.(もしかしたらエンコードをこの関数で「定義」していると考える方が分かりやすいという人もいるかもしれません.:P )

リスト cs の長さを L とし,x = enc M (c#cs) とします.リスト c#cs の長さは L + 1 です. x はリスト c#cs を M 進数表現と見なしたときの値 G(c#cs) を F(L + 1) だけオフセットしたものですから \[ x = F(L + 1) + G(c\#cs) \] となります.G(c#cs) は G(cs) を一桁ずらして c を加えたものですから次のようになります. \[ G(c\#cs) = c + M G(cs) \] F(L + 1) は定義から次のようになることがわかるでしょう. \[ F(L+1) = M F(L) + 1 \] 以上2つの式を最初の式に代入すると \[ \begin{split} x &= (M F(L) + 1) + (c + M G(cs)) \\ &= 1 + c + M(F(L) + G(cs)) \\ &= 1 + c + M(\mathtt{enc}\ M\ cs) \end{split} \] これで enc の定義が最初の定義と一致していることが分かりました.

デコード関数 dec

自然数をリストに戻すデコード関数 dec を定義します.

fun dec :: "nat => nat => nat list" where
  "dec M 0 = []" |
  "dec M (Suc x) = (x mod M) # (dec M (x div M))"

こちらについても先ほどと同じように,半形式的な議論をして定義の正しさを確認することができると思います. しかしここではちょっと違うことをしましょう. 関数 dec が関数 enc の逆関数であること,つまり要素が M 未満の自然数であるという条件を満たす任意の cs について \[ \mathtt{dec}\, M\, (\mathtt{enc}\, M\, cs) = cs \] であることを証明してみることにします.

dec M (enc M cs) = cs の証明

定理証明支援系 Isabelle にかけると瞬殺です :P

(set cs はリスト cs の要素からなる集合を表します.言い換えれば,リストから集合への変換関数です.)

lemma dec_enc: "M > 0 ==>
   (ALL x:set cs. x < M) --> dec M (enc M cs) = cs"
apply(induct_tac cs)
apply(auto)
done

これでは性質が見えないので,証明を細かく分けてみることにします. まず数学的帰納法 induct_tac を適用すると,基底ケースと帰納ケースの2つのゴールが出ます.

goal (2 subgoals):
 1. 0 < M ==> (ALL x:set []. x < M) --> dec M (enc M []) = []
 2. !!a list.
       [| 0 < M; (ALL x:set list. x < M) --> dec M (enc M list) = list |]
       ==> (ALL x:set (a # list). x < M) -->
           dec M (enc M (a # list)) = a # list

まず基底ケースを考えます.enc M [] は定義から 0 で,dec M 0 は [] ですから基底ケースは [] = [] となり成り立ちます.

apply(subst enc.simps)
apply(subst dec.simps)
------------------------------
 1. 0 < M ==> (ALL x:set []. x < M) --> [] = []

次は帰納ケースです.定義を使って整理すると次のようになります.

 1. !!a list.
       [| 0 < M; (ALL x:set list. x < M) --> dec M (enc M list) = list;
          ALL x:set (a # list). x < M |]
       ==> dec M (1 + a + M * enc M list) = a # list

dec の中の 1 + ... を Suc (...) にすれば dec の定義が使えます. そこで次のようにして置き換えます.

apply(subgoal_tac "Suc(a + M * enc M list) = 1 + a + M * enc M list")
apply(rotate_tac -1)
apply(erule_tac t="1 + a + M * enc M list" in subst)
------------------------------
 1. !!a list.
       [| 0 < M; (ALL x:set list. x < M) --> dec M (enc M list) = list;
          ALL x:set (a # list). x < M |]
       ==> dec M (Suc (a + M * enc M list)) = a # list

dec の定義を使うと次のようになります.

 1. !!a list.
       [| 0 < M; (ALL x:set list. x < M) --> dec M (enc M list) = list;
          ALL x:set (a # list). x < M |]
       ==> (a + M * enc M list) mod M # dec M ((a + M * enc M list) div M) =
           a # list

次は先頭の (a + M * enc M list) mod M を攻撃しましょう.0 <= a < M で2項目は M の倍数ですからこれは a に等しいはずです.

apply(subgoal_tac "a = (a + M * enc M list) mod M")
apply(rotate_tac -1)
apply(erule_tac t="(a + M * enc M list) mod M" in subst)
------------------------------
 1. !!a list.
       [| 0 < M; (ALL x:set list. x < M) --> dec M (enc M list) = list;
          ALL x:set (a # list). x < M |]
       ==> a # dec M ((a + M * enc M list) div M) = a # list

同様に (a + M * enc M list) div M は enc M list になるでしょう.

apply(subgoal_tac "enc M list = (a + M * enc M list) div M")
apply(rotate_tac -1)
apply(erule_tac t="(a + M * enc M list) div M" in subst)
------------------------------
 1. !!a list.
       [| 0 < M;
          (ALL x:set list. x < M) -->
          dec M (enc M list) = list;
          ALL x:set (a # list). x < M |]
       ==> a # dec M (enc M list) = a # list

ここで帰納法の仮定が使えます.結果は list になり,証明完了です.

apply(drule mp)
apply(clarsimp)
apply(erule ssubst)
------------------------------
 1. !!a list.
       [| 0 < M; ALL x:set (a # list). x < M |]
       ==> a # list = a # list

スクリプト全体を示しておきます.

theory NatListEncDec imports "~~/src/HOL/Hoare/Hoare_Logic"
begin

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

value "enc 10 []"
value "enc 10 [1]"
value "enc 10 [1,2]"
value "enc 10 [1,2,3]"
value "enc 10 [1,2,3,4]"

fun dec :: "nat => nat => nat list" where
  "dec M 0 = []" |
  "dec M (Suc x) = (x mod M) # (dec M (x div M))"

value "dec 10 3"
value "dec 10 43"
value "dec 10 432"
value "dec 10 5432"

lemma dec_enc: "M > 0 ==>
 (ALL c:set cs. c < M) --> dec M (enc M cs) = cs"
apply(induct_tac cs)
apply(auto)
done

lemma "M > 0 ==>
 (ALL x:set cs. x < M) --> dec M (enc M cs) = cs"
(* base *)
apply(induct_tac cs)
apply(subst enc.simps)
apply(subst dec.simps)
apply(simp)
(* ind *)
apply(rule impI)
apply(subst enc.simps)

apply(subgoal_tac "Suc(a + M * enc M list) = 1 + a + M * enc M list")
apply(rotate_tac -1)
apply(erule_tac t="1 + a + M * enc M list" in subst)

apply(subst dec.simps)

apply(subgoal_tac "a = (a + M * enc M list) mod M")
apply(rotate_tac -1)
apply(erule_tac t="(a + M * enc M list) mod M" in subst)

apply(subgoal_tac "enc M list = (a + M * enc M list) div M")
apply(rotate_tac -1)
apply(erule_tac t="(a + M * enc M list) div M" in subst)

apply(drule mp)
apply(clarsimp)
apply(erule ssubst)

apply(simp)
apply(simp)
apply(simp)
apply(simp)
done

コメント

次は当然 enc M (dec M x) = x の証明ということになります.これは読者の宿題とします(すみません,言ってみたかっただけです)

つづく

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