ハフマン符号化して復号すると元に戻ることをACL2で証明した
目次
投稿日: 2022-07-14 木
1. 注意
この記事はいま思うと ACL2 との付き合い方がよく分かっていなかったときに、 書いたものなので参考にしない方がいいです。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張る予定です。
2. はじめに
ハフマン符号を ACL2 で実装し、符号化したデータを正しく元の情報に復号できることを証明します。 今回は符号化した情報を復号すると元に戻るというところまでしか証明しないため、 ハフマン符号化木の生成が正しくできているかという点については触れません。 ハフマン符号化木の生成が適切であることの証明は今後の課題として残しておこうと思います。
本記事は ACL2 によるハフマン符号の実装について文書として残すことが最大の目的であるため ACL2 の解説はしません。 ACL2 について学ぶには ACL2-tutorial を参照するのがおすすめです。 ハフマン符号の仕組みについても深く説明しないため、 ハフマン符号 - Wikipedia や 計算機プログラムの構造と解釈 第二版 2.3.4 例: Huffman 符号化木 などを参考にしてください。
本記事のハフマン符号化の実装は 計算機プログラムの構造と解釈 第二版 2.3.4 例: Huffman 符号化木 のものとだいたい同じなのですが、 実装時に参照しなかったため関数名や細かい部分は異なっています。 いくつか書籍の問題の答えに相当する関数も提示するので、 自分で問題を解きたい方は先に計算機プログラムの構造と解釈を読むことをおすすめします。
ソースコードは huffman-encode.lisp から参照できます。 上記のコードの LICENSE と同様に、本記事中のプログラムのライセンスも3条項BSDライセンスとします。
ACL2 の実行環境がある場合はこの記事の先頭から順に実行していけば問題なく動作するはずです(ACL2 Version 8.4 で確認済み)。 本記事から ACL2 の出力を全て貼るのはやめて Summary の部分のみ掲載するようにしました。 出力を全部残したところで長くて邪魔な割に不要な情報であるためです。
3. ハフマン木の定義
3.1. ハフマン木の述語
まずハフマン木の節であることを確認する述語を定義します。
ハフマン木には節と葉の二つがありそのうちの節である場合に真を返します。
ハフマン木の全体の構造については後述する huffman-treep 関数で紹介します。
(defun nodep (x) (declare (xargs :guard t)) (and (consp x) (eq (car x) 'node)))
Summary を確認する
Summary Form: ( DEFUN NODEP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) NODEP
ハフマン木かどうかを調べる述語は次のように定義します。
(defun huffman-treep (x) (declare (xargs :guard t)) (flet ((symbol-list (x) (if (nodep x) (second x) (list (second x))))) (if (nodep x) (and (true-listp x) (equal (len x) 5) (true-listp (second x)) (rationalp (third x)) (huffman-treep (fourth x)) (huffman-treep (fifth x)) (equal (second x) (append (symbol-list (fourth x)) (symbol-list (fifth x)))) (equal (third x) (+ (third (fourth x)) (third (fifth x))))) (and (true-listp x) (equal (len x) 3) (equal (first x) 'leaf) (rationalp (third x))))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN HUFFMAN-TREEP ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION FIX)
(:DEFINITION HUFFMAN-TREEP)
(:DEFINITION INTEGER-ABS)
(:DEFINITION LEN)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION SYNP)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART RATIONALP)
(:EXECUTABLE-COUNTERPART SYMBOLP)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-2-OF-+)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE DEFAULT-CAR)
(:REWRITE FOLD-CONSTS-IN-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION ACL2-COUNT)
(:DEFINITION INTEGER-ABS)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION O<)
(:DEFINITION TRUE-LISTP))
Time: 0.10 seconds (prove: 0.09, print: 0.01, other: 0.01)
Prover steps counted: 37530
HUFFMAN-TREEP
huffman-treep が真であることの意味について説明します。
まず (nodep x) が偽の場合、
すなわち x が葉の場合は次のようなリストであることを要求します。
(leaf <シンボル> <重み>)
ここで、 <シンボル> とは符号化する対象の記号のことです。
ACL2 の symbolp で真になるオブジェクトとは別ものとして考えてください。
huffman-treep の定義でも <シンボル> の部分が symbolp であることを要求していません。
<重み> は <シンボル> の出現頻度を表現する値で有理数によって表現します。
<重み> が大きければ出現頻度が高いことを意味し、 <シンボル> を符号化したときのビット列は短かくなります。
次に (nodep x) が真の場合、すなわち x が節の場合について説明します。
節は次のようなリスト構造をしています。
(node <シンボルのリスト> <重み> <左のハフマン木> <右のハフマン木>)
<シンボルのリスト> は節から辿れる全ての葉のシンボルを集めたリストです。
<シンボルのリスト> の中に含まれているシンボルは必ず、
<左のハフマン木> か <右のハフマン木> にも含まれています。
このことは定義のうちの下記の部分によって保証されています。
(equal (second x)
(append (symbol-list (fourth x))
(symbol-list (fifth x))))
<重み> は節から辿れる全ての葉の重みの総和です。
そうなっていることは下記の部分によって保証されています。
(equal (third x)
(+ (third (fourth x))
(third (fifth x))))
どのような構造であるかを定義するだけなら上記二つは不要ですが、
huffman-treep が真になるようなハフマン木で符号化した後、
元の情報に復号できることを証明するのには必要です。
3.2. コンストラクタとアクセサ
ハフマン木を作成する関数とハフマン木の要素にアクセスするための関数を定義していきます。
3.2.1. 木に関する定義
節と葉に共通するアクセサとしてシンボルのリストを取り出す symbol-list
と重みを取り出す weight を定義します。
(defun symbol-list (x) (declare (xargs :guard (huffman-treep x))) (if (nodep x) (second x) (list (second x))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN SYMBOL-LIST ...)
Rules: ((:DEFINITION HUFFMAN-TREEP)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 129
SYMBOL-LIST
(defun weight (x) (declare (xargs :guard (huffman-treep x))) (third x))
証明成功: Summary を確認する
Summary
Form: ( DEFUN WEIGHT ...)
Rules: ((:DEFINITION HUFFMAN-TREEP)
(:DEFINITION LEN)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART RATIONALP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE DEFAULT-CAR))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 320
WEIGHT
3.2.2. 葉に関する定義
ハフマン木の葉を作成する huffman-leaf と、
ハフマン木の葉から <シンボル> を取り出す関数
leaf-symbol を定義します。
(defun huffman-leaf (s w) (declare (xargs :guard (rationalp w))) (list 'leaf s w))
Summary を確認する
Summary Form: ( DEFUN HUFFMAN-LEAF ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) HUFFMAN-LEAF
(defun leaf-symbol (x) (declare (xargs :guard (and (huffman-treep x) (not (nodep x))))) (second x))
証明成功: Summary を確認する
Summary
Form: ( DEFUN LEAF-SYMBOL ...)
Rules: ((:DEFINITION HUFFMAN-TREEP)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 151
LEAF-SYMBOL
3.2.3. 節に関する定義
ハフマン木の節を作成する huffman-node と
左の木を返す left と右の木を返す right を定義します。
木を作成するときに左右の木のシンボルのリストの連結と重みの和を求めています。
(defun huffman-node (l r) (declare (xargs :guard (and (huffman-treep l) (huffman-treep r)))) (list 'node (append (symbol-list l) (symbol-list r)) (+ (weight l) (weight r)) l r))
証明成功: Summary を確認する
Summary
Form: ( DEFUN HUFFMAN-NODE ...)
Rules: ((:DEFINITION HUFFMAN-TREEP)
(:DEFINITION LEN)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION SYMBOL-LIST)
(:DEFINITION TRUE-LISTP)
(:DEFINITION WEIGHT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION NODEP)
(:DEFINITION SYMBOL-LIST))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 2053
HUFFMAN-NODE
(defun left (x) (declare (xargs :guard (and (huffman-treep x) (nodep x)))) (fourth x))
証明成功: Summary を確認する
Summary
Form: ( DEFUN LEFT ...)
Rules: ((:DEFINITION HUFFMAN-TREEP)
(:DEFINITION LEN)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREEP)
(:EXECUTABLE-COUNTERPART LEN)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE DEFAULT-CAR))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 543
LEFT
(defun right (x) (declare (xargs :guard (and (huffman-treep x) (nodep x)))) (fifth x))
証明成功: Summary を確認する
Summary
Form: ( DEFUN RIGHT ...)
Rules: ((:DEFINITION HUFFMAN-TREEP)
(:DEFINITION LEN)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREEP)
(:EXECUTABLE-COUNTERPART LEN)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE DEFAULT-CAR))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 871
RIGHT
3.3. ハフマン木がリスト構造であることを忘れさせる
ハフマン木をリストとして定義しましたが、 リスト構造のままこのハフマン木を使って、 ハフマン木の生成する関数を書いたり定理の証明に進むのには困難を伴います。
ハフマン木に関する複雑な定理を証明しようとするときにリスト構造が見えていると
ACL2 はリスト構造を誤った方向に簡約することがあって不便だし、
ACL2 が変形した式に (CAR (CDDDDR X))
みたいのがでてくると訳が分からなくてつらいという問題があります。
これを解消するために関数の展開を無効にして与えた定理のみを使用するように ACL2 に指示します。
そのための定理や関数を書いていきます。 なお、 ここで書いている定理や関数は後のハフマン木の生成や符号化のプログラムを書いている際に必要になったものであり、 本当に必要なものが網羅されているとはいえない可能性があることに注意してください。
3.3.1. デストラクタを除去するルール
elim ルールクラスはデストラクタを除去して一般的な変数に置き換えるルールです。
コンスセルにおけるデストラクタとは car や cdr に相当し、
ACL2 がデストラクタを使用した項、例えば (car x) などを発見すると
x を (cons x1 x2) のような形に書き換えてくれます。
こうすることによって (car x) であった部分は x1 とシンプルな形に置き換えられます。
詳細は ACL2 - Elim を参照してください。
同じことを leaf-symbol, weight と left, right に対してもできるようにします。
leaf-symbol-weight-elim
leaf-symbol,weightをデストラクタとして、 これらが見つかった時点で(huffman-leaf s w)の形に置き換えられるようにします。(defthm leaf-symbol-weight-elim (implies (and (not (nodep x)) (huffman-treep x)) (equal (huffman-leaf (leaf-symbol x) (weight x)) x)) :rule-classes :elim)証明成功: Summary を確認する
Summary Form: ( DEFTHM LEAF-SYMBOL-WEIGHT-ELIM ...) Rules: ((:DEFINITION HUFFMAN-LEAF) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEAF-SYMBOL) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION NOT) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:DEFINITION WEIGHT) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART HUFFMAN-TREEP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART SYMBOLP) (:EXECUTABLE-COUNTERPART TAU-SYSTEM) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION HUFFMAN-TREEP) (:INDUCTION LEN) (:INDUCTION TRUE-LISTP) (:REWRITE CDR-CONS) (:REWRITE CONS-EQUAL) (:REWRITE FOLD-CONSTS-IN-+)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 4034 LEAF-SYMBOL-WEIGHT-ELIMleft-right-elim
left,rightをデストラクタとして、 これらが見つかった時点で(huffman-node l r)の形に置き換えられるようにします。この定理を証明するのに
(equal (len x) 5)をconspとnullを使用した版に置き換える補助定理len=5が必要になりました。(defthm len=5 (implies (true-listp x) (equal (equal (len x) 5) (and (consp x) (consp (cdr x)) (consp (cddr x)) (consp (cdddr x)) (consp (cddddr x)) (null (cdr (cddddr x)))))))証明成功: Summary を確認する
Summary Form: ( DEFTHM LEN=5 ...) Rules: ((:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION NULL) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART LEN) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION LEN) (:INDUCTION TRUE-LISTP) (:REWRITE DEFAULT-CDR) (:REWRITE FOLD-CONSTS-IN-+) (:TYPE-PRESCRIPTION LEN)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 4640 LEN=5(defthm left-right-elim (implies (and (nodep x) (huffman-treep x)) (equal (huffman-node (left x) (right x)) x)) :hints (("Goal" :use len=5 :in-theory (disable len=5))) :rule-classes :elim)証明成功: Summary を確認する
Summary Form: ( DEFTHM LEFT-RIGHT-ELIM ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION FIX) (:DEFINITION HUFFMAN-NODE) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEFT) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION NOT) (:DEFINITION NULL) (:DEFINITION RIGHT) (:DEFINITION SYMBOL-LIST) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:DEFINITION WEIGHT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART BINARY-APPEND) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART HUFFMAN-TREEP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART RATIONALP) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-+-1) (:REWRITE DEFAULT-+-2) (:REWRITE DEFAULT-CAR) (:REWRITE DEFAULT-CDR) (:REWRITE FOLD-CONSTS-IN-+) (:TYPE-PRESCRIPTION LEN)) Hint-events: ((:USE LEN=5)) Splitter rules (see :DOC splitter): if-intro: ((:DEFINITION FIX) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION TRUE-LISTP)) Time: 0.04 seconds (prove: 0.04, print: 0.00, other: 0.00) Prover steps counted: 18872 LEFT-RIGHT-ELIM
3.3.2. コンストラクタとアクセサに関する定理
- huffman-node によって作られたものはハフマン木である
(defthm huffman-treep-huffman-node (implies (and (huffman-treep l) (huffman-treep r)) (huffman-treep (huffman-node l r))))証明成功: Summary を確認する
Summary Form: ( DEFTHM HUFFMAN-TREEP-HUFFMAN-NODE ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION FIX) (:DEFINITION HUFFMAN-NODE) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION NOT) (:DEFINITION NULL) (:DEFINITION SYMBOL-LIST) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:DEFINITION WEIGHT) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART BINARY-APPEND) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART HUFFMAN-TREEP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART RATIONALP) (:EXECUTABLE-COUNTERPART SYMBOLP) (:EXECUTABLE-COUNTERPART TAU-SYSTEM) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION HUFFMAN-TREEP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DEFAULT-+-1) (:REWRITE DEFAULT-+-2) (:REWRITE DEFAULT-CAR) (:REWRITE DEFAULT-CDR) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE LEN=5) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION BINARY-APPEND) (:TYPE-PRESCRIPTION HUFFMAN-TREEP) (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND)) Splitter rules (see :DOC splitter): if-intro: ((:DEFINITION BINARY-APPEND) (:DEFINITION FIX) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION NODEP) (:DEFINITION SYMBOL-LIST) (:DEFINITION TRUE-LISTP)) Warnings: Non-rec Time: 0.46 seconds (prove: 0.45, print: 0.01, other: 0.00) Prover steps counted: 148287 HUFFMAN-TREEP-HUFFMAN-NODE - huffman-node によって作られたものは節である
(defthm nodep-huffman-node (implies (and (huffman-treep l) (huffman-treep r)) (nodep (huffman-node l r))))証明成功: Summary を確認する
Summary Form: ( DEFTHM NODEP-HUFFMAN-NODE ...) Rules: ((:DEFINITION HUFFMAN-NODE) (:DEFINITION NODEP) (:DEFINITION SYMBOL-LIST) (:DEFINITION WEIGHT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:TYPE-PRESCRIPTION NODEP)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 731 NODEP-HUFFMAN-NODE - 節の場合
symbol-listは左右の木のsymobl-listを連結したものである
(defthm symbol-list-left-right (implies (and (nodep x) (huffman-treep x)) (equal (symbol-list x) (append (symbol-list (left x)) (symbol-list (right x))))))証明成功: Summary を確認する
Summary Form: ( DEFTHM SYMBOL-LIST-LEFT-RIGHT ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEFT) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION RIGHT) (:DEFINITION SYMBOL-LIST) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART BINARY-APPEND) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART RATIONALP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-CDR) (:REWRITE FOLD-CONSTS-IN-+)) Splitter rules (see :DOC splitter): if-intro: ((:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION TRUE-LISTP)) Warnings: Non-rec Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) Prover steps counted: 6991 SYMBOL-LIST-LEFT-RIGHT - 節の場合
weightは左右の木のweightを足したものである
(defthm weight-left-right (implies (and (nodep x) (huffman-treep x)) (equal (weight x) (+ (weight (left x)) (weight (right x))))))証明成功: Summary を確認する
Summary Form: ( DEFTHM WEIGHT-LEFT-RIGHT ...) Rules: ((:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEFT) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION RIGHT) (:DEFINITION TRUE-LISTP) (:DEFINITION WEIGHT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 525 WEIGHT-LEFT-RIGHT - 節の場合、左の木はハフマン木である
(defthm huffman-treep-left (implies (and (nodep x) (huffman-treep x)) (huffman-treep (left x))))証明成功: Summary を確認する
Summary Form: ( DEFTHM HUFFMAN-TREEP-LEFT ...) Rules: ((:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEFT) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION HUFFMAN-TREEP)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 266 HUFFMAN-TREEP-LEFT - 節の場合、右の木はハフマン木である
(defthm huffman-treep-right (implies (and (nodep x) (huffman-treep x)) (huffman-treep (right x))))証明成功: Summary を確認する
Summary Form: ( DEFTHM HUFFMAN-TREEP-RIGHT ...) Rules: ((:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION RIGHT) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION HUFFMAN-TREEP)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 337 HUFFMAN-TREEP-RIGHT symbol-listは真リストである
(defthm true-listp-symbol-list (implies (huffman-treep x) (true-listp (symbol-list x))))証明成功: Summary を確認する
Summary Form: ( DEFTHM TRUE-LISTP-SYMBOL-LIST ...) Rules: ((:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION NOT) (:DEFINITION SYMBOL-LIST) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART TAU-SYSTEM) (:TYPE-PRESCRIPTION TRUE-LISTP)) Splitter rules (see :DOC splitter): if-intro: ((:DEFINITION NODEP) (:DEFINITION SYMBOL-LIST)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 506 TRUE-LISTP-SYMBOL-LIST- 葉に対する
symbol-listをleaf-symbolを使った式に置き換える
(defthm symbol-list-leaf-symbol (implies (and (huffman-treep x) (not (nodep x))) (equal (symbol-list x) (list (leaf-symbol x)))))証明成功: Summary を確認する
Summary Form: ( DEFTHM SYMBOL-LIST-LEAF-SYMBOL ...) Rules: ((:DEFINITION LEAF-SYMBOL) (:DEFINITION NODEP) (:DEFINITION NOT) (:DEFINITION SYMBOL-LIST) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DEFAULT-CDR)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 483 SYMBOL-LIST-LEAF-SYMBOL weightは有理数である
(defthm rationalp-weight (implies (huffman-treep x) (rationalp (weight x))))証明成功: Summary を確認する
Summary Form: ( DEFTHM RATIONALP-WEIGHT ...) Rules: ((:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:DEFINITION TRUE-LISTP) (:DEFINITION WEIGHT) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 288 RATIONALP-WEIGHT- 葉について
weightは有理数である
後の
orderp関数のガードの検証で必要です。(defthm rationalp-weight/leaf (implies (huffman-treep (huffman-leaf s w)) (rationalp w)))証明成功: Summary を確認する
Summary Form: ( DEFTHM RATIONALP-WEIGHT/LEAF ...) Rules: ((:DEFINITION HUFFMAN-LEAF) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART LEN) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: Non-rec and Free Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 124 RATIONALP-WEIGHT/LEAF huffman-leafはハフマン木である
(defthm huffman-treep-huffman-leaf (implies (rationalp w) (huffman-treep (huffman-leaf s w))))証明成功: Summary を確認する
Summary Form: ( DEFTHM HUFFMAN-TREEP-HUFFMAN-LEAF ...) Rules: ((:DEFINITION HUFFMAN-LEAF) (:DEFINITION HUFFMAN-TREEP) (:DEFINITION LEN) (:DEFINITION NODEP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART LEN) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION HUFFMAN-TREEP)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 120 HUFFMAN-TREEP-HUFFMAN-LEAF
3.3.3. 節の数を求める関数
ハフマン木に再帰的にアクセスする関数を書くときに停止性の証明が必要になる。
しかしハフマン木の構造がリスト構造であることを伏せるため、
ACL2 がデフォルトで使用する尺度である acl2-count は使えない。
そのため、節の数を求める関数 node-count を提供することで対応する。
(defun node-count (x) (declare (xargs :guard (huffman-treep x))) (if (nodep x) (+ 1 (node-count (left x)) (node-count (right x))) 0))
証明成功: Summary を確認する
Summary
Form: ( DEFUN NODE-COUNT ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION FIX)
(:DEFINITION HUFFMAN-TREEP)
(:DEFINITION LEFT)
(:DEFINITION LEN)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION RIGHT)
(:DEFINITION SYNP)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART SYMBOLP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-2-OF-+)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE DEFAULT-CAR)
(:REWRITE DEFAULT-CDR)
(:REWRITE FOLD-CONSTS-IN-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT)
(:TYPE-PRESCRIPTION NODE-COUNT))
Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 7263
NODE-COUNT
また停止性を証明できるように left と right の node-count は
元のハフマン木の node-count よりも小さいことを証明する。
(defthm node-count-left
(implies (nodep x)
(< (node-count (left x))
(node-count x)))
:rule-classes :linear)
証明成功: Summary を確認する
Summary
Form: ( DEFTHM NODE-COUNT-LEFT ...)
Rules: ((:DEFINITION LEFT)
(:DEFINITION NODE-COUNT)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION RIGHT)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NODE-COUNT)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART SYMBOLP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE DEFAULT-CAR)
(:REWRITE DEFAULT-CDR)
(:TYPE-PRESCRIPTION NODE-COUNT))
Warnings: Non-rec
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 1492
NODE-COUNT-LEFT
(defthm node-count-right
(implies (nodep x)
(< (node-count (right x))
(node-count x)))
:rule-classes :linear)
証明成功: Summary を確認する
Summary
Form: ( DEFTHM NODE-COUNT-RIGHT ...)
Rules: ((:DEFINITION FIX)
(:DEFINITION LEFT)
(:DEFINITION NODE-COUNT)
(:DEFINITION NODEP)
(:DEFINITION NOT)
(:DEFINITION RIGHT)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NODE-COUNT)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART SYMBOLP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE DEFAULT-CAR)
(:REWRITE DEFAULT-CDR)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION NODE-COUNT))
Warnings: Non-rec
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 2004
NODE-COUNT-RIGHT
3.4. 関数を展開しないようにする
ACL2 による自動証明時にここまで定義した全ての関数が展開されないようにします。 これでいままでに与えた定理による式の変形のみが行なわれるようになります。
(in-theory (disable nodep huffman-treep
leaf-symbol
huffman-leaf huffman-node
symbol-list weight left right
node-count))
Summary を確認する
Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) (:NUMBER-OF-ENABLED-RUNES 4372)
4. ハフマン木を生成する
はじめにの節で言及していますが、 今回はハフマン木の生成アルゴリズムが正しいかどうかという点については触れません。 こちらは余裕があったらいずれ挑戦しようと思います。 しかし、 生成した結果がこれまでに定義したハフマン木の節であるという最低限の必要な性質については証明します。
ハフマン木を生成するアプローチについて紹介します。 下記のようなシンボルと重みのペアからなるリストを用意します(重みの設定は雑にしました)。
(assign pairs '((a 5) (this 7) (is 9) (pen 6)))
出力:
((A 5) (THIS 7) (IS 9) (PEN 6))
このリストを重みで昇順に並んだハフマン木の葉のリストに変換します。
ハフマン木のリストについて、まずハフマン木のリストのうち最も重みが小さい二つのハフマン木同士でハフマン木の節を構成します。 構成したハフマン木と残りのハフマン木をあわせて再度最も小さい二つのハフマン木同士で節を作る工程を繰り返すことで、 最終的には一つのハフマン木になります。 ハフマン木の葉を重みで昇順に並べたのは、最小の二つのハフマン木を求めるためです。
4.1. ハフマン木を生成するための関数を定義する
シンボルト重みのペアのリストの述語を定義します。
(defun symbol-weight-pair-listp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (consp (car x)) (consp (cdar x)) (rationalp (cadar x)) (null (cddar x)) (symbol-weight-pair-listp (cdr x)))))
Summary を確認する
Summary Form: ( DEFUN SYMBOL-WEIGHT-PAIR-LISTP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) SYMBOL-WEIGHT-PAIR-LISTP
変換先であるハフマン木のリストの述語を定義します。
(defun huffman-tree-listp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (huffman-treep (car x)) (huffman-tree-listp (cdr x)))))
Summary を確認する
Summary Form: ( DEFUN HUFFMAN-TREE-LISTP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) HUFFMAN-TREE-LISTP
ハフマン木のリストが昇順に並んでいることを確認する述語を定義します。
(defun orderdp (x) (declare (xargs :guard (huffman-tree-listp x))) (cond ((atom x) t) ((<= (weight (car x)) (weight (car x))) (orderdp (cdr x))) (t nil)))
証明成功: Summary を確認する
Summary
Form: ( DEFUN ORDERDP ...)
Rules: ((:DEFINITION ATOM)
(:DEFINITION HUFFMAN-TREE-LISTP)
(:DEFINITION NOT)
(:ELIM CAR-CDR-ELIM)
(:ELIM LEAF-SYMBOL-WEIGHT-ELIM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREEP-LEFT)
(:REWRITE HUFFMAN-TREEP-RIGHT)
(:REWRITE RATIONALP-+)
(:REWRITE RATIONALP-WEIGHT)
(:REWRITE RATIONALP-WEIGHT/LEAF)
(:REWRITE WEIGHT-LEFT-RIGHT)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 544
ORDERDP
昇順に並んだハフマン木のリストに要素を追加する関数を定義します。
(defun insert (e x) (declare (xargs :guard (and (huffman-treep e) (huffman-tree-listp x)))) (cond ((endp x) (list e)) ((<= (weight e) (weight (car x))) (cons e x)) (t (cons (car x) (insert e (cdr x))))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN INSERT ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION EQ)
(:DEFINITION HUFFMAN-TREE-LISTP)
(:DEFINITION NOT)
(:ELIM CAR-CDR-ELIM)
(:ELIM LEAF-SYMBOL-WEIGHT-ELIM)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREEP-LEFT)
(:REWRITE HUFFMAN-TREEP-RIGHT)
(:REWRITE RATIONALP-+)
(:REWRITE RATIONALP-WEIGHT)
(:REWRITE RATIONALP-WEIGHT/LEAF)
(:REWRITE WEIGHT-LEFT-RIGHT)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 771
INSERT
ペアのリストを重みで昇順に並んだハフマン木の葉のリストに変換する関数を定義します。
(defun pairs-to-leaves (x) (declare (xargs :guard (symbol-weight-pair-listp x))) (if (endp x) nil (insert (huffman-leaf (caar x) (cadar x)) (pairs-to-leaves (cdr x)))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN PAIRS-TO-LEAVES ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION EQ)
(:DEFINITION HUFFMAN-TREE-LISTP)
(:DEFINITION INSERT)
(:DEFINITION NOT)
(:DEFINITION PAIRS-TO-LEAVES)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREE-LISTP)
(:EXECUTABLE-COUNTERPART PAIRS-TO-LEAVES)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION HUFFMAN-TREE-LISTP)
(:INDUCTION INSERT)
(:INDUCTION PAIRS-TO-LEAVES)
(:INDUCTION SYMBOL-WEIGHT-PAIR-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-LEAF)
(:TYPE-PRESCRIPTION HUFFMAN-TREE-LISTP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION INSERT))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 4712
PAIRS-TO-LEAVES
昇順に並んだハフマン木の葉のリストからハフマン木を生成する関数を定義します。
a には重みが最小のハフマン木を、 x には最小を除いた残りのハフマン木を渡します。
この関数はもっとシンプルにできると思われるかもしれませんが、
(insert a (cdr x)) の形で再帰すると x の長さが変わらなくなるために、
停止性の証明が難しくなるので (insert a (cddr x)) の形で再帰するようにしています。
試してはいませんが、
停止性の証明が難しくなるだけであって証明できないというわけではでないと思っています。
(defun generate (x a) (declare (xargs :measure (len x) :guard (and (huffman-tree-listp x) (orderdp x) (huffman-treep a)))) (cond ((endp x) a) ((<= (weight a) (weight (car x))) (generate (cdr x) (huffman-node a (car x)))) ((endp (cdr x)) (huffman-node (car x) a)) ((<= (weight a) (weight (cadr x))) (generate (cdr x) (huffman-node (car x) a))) (t (generate (insert a (cddr x)) (huffman-node (car x) (cadr x))))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN GENERATE ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
(:DEFINITION ENDP)
(:DEFINITION EQ)
(:DEFINITION HUFFMAN-TREE-LISTP)
(:DEFINITION INSERT)
(:DEFINITION LEN)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O-P)
(:DEFINITION O<)
(:DEFINITION ORDERDP)
(:DEFINITION SYNP)
(:ELIM CAR-CDR-ELIM)
(:ELIM LEAF-SYMBOL-WEIGHT-ELIM)
(:ELIM LEFT-RIGHT-ELIM)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREE-LISTP)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART ORDERDP)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION HUFFMAN-TREE-LISTP)
(:INDUCTION INSERT)
(:INDUCTION LEN)
(:INDUCTION ORDERDP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE FOLD-CONSTS-IN-+)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-LEAF)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-NODE)
(:REWRITE HUFFMAN-TREEP-LEFT)
(:REWRITE HUFFMAN-TREEP-RIGHT)
(:REWRITE NODEP-HUFFMAN-NODE)
(:REWRITE RATIONALP-+)
(:REWRITE RATIONALP-WEIGHT)
(:REWRITE RATIONALP-WEIGHT/LEAF)
(:REWRITE WEIGHT-LEFT-RIGHT)
(:TYPE-PRESCRIPTION HUFFMAN-NODE)
(:TYPE-PRESCRIPTION HUFFMAN-TREE-LISTP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION NODEP)
(:TYPE-PRESCRIPTION ORDERDP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION INSERT))
Time: 0.69 seconds (prove: 0.62, print: 0.07, other: 0.00)
Prover steps counted: 226247
GENERATE
pairs-to-leaves と generate を組み合せてペアのリストからハフマン木を生成する関数を定義します。
ただ、この時点だとガード検証には失敗するためガード検証は後に回します(そのため :verify-guards nil と指定している)。
(defun generate-huffman-tree (x) (declare (xargs :guard (and (symbol-weight-pair-listp x) (< 1 (len x))) :verify-guards nil)) (let ((leaves (pairs-to-leaves x))) (generate (cdr leaves) (car leaves))))
Summary を確認する
Summary Form: ( DEFUN GENERATE-HUFFMAN-TREE ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) GENERATE-HUFFMAN-TREE
ここで先程用意したシンボルと重みのペアのリストをハフマン木に変換してみましょう。
(assign tree (generate-huffman-tree (@ pairs)))
出力:
(NODE (A PEN THIS IS)
27
(NODE (A PEN)
11 (LEAF A 5)
(LEAF PEN 6))
(NODE (THIS IS)
16 (LEAF THIS 7)
(LEAF IS 9)))
それぞれの節について最小の要素同士で節が構成されているように見えますね。 問題なさそうに見えます。
4.2. generate-huffman-tree で生成された木がハフマン木であることの証明
最小の要素同士で節を構成して作られた木が生成されることの検証は今後の課題として、
generate-huffman-tree で生成された木がハフマン木であることの証明をします。
まず、 insert 関数の性質から確かめていきます。
insert した結果はハフマン木のリストである。
(defthm huffman-tree-listp-insert
(implies (and (huffman-tree-listp x)
(huffman-treep e))
(huffman-tree-listp (insert e x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM HUFFMAN-TREE-LISTP-INSERT ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION HUFFMAN-TREE-LISTP)
(:DEFINITION INSERT)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION HUFFMAN-TREE-LISTP)
(:INDUCTION INSERT)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION HUFFMAN-TREE-LISTP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 870
HUFFMAN-TREE-LISTP-INSERT
insert した結果は昇順に並んでいる。
(defthm orderdp-insert
(implies (orderdp x)
(orderdp (insert e x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM ORDERDP-INSERT ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION INSERT)
(:DEFINITION NOT)
(:DEFINITION ORDERDP)
(:EXECUTABLE-COUNTERPART ORDERDP)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION INSERT)
(:INDUCTION ORDERDP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION ORDERDP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 1008
ORDERDP-INSERT
pairs-to-leaves の結果はハフマン木のリストである。
(defthm huffman-tree-listp-pairs-to-leaves
(implies (symbol-weight-pair-listp x)
(huffman-tree-listp (pairs-to-leaves x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM HUFFMAN-TREE-LISTP-PAIRS-TO-LEAVES ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION PAIRS-TO-LEAVES)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREE-LISTP)
(:EXECUTABLE-COUNTERPART PAIRS-TO-LEAVES)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION PAIRS-TO-LEAVES)
(:INDUCTION SYMBOL-WEIGHT-PAIR-LISTP)
(:REWRITE HUFFMAN-TREE-LISTP-INSERT)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-LEAF)
(:TYPE-PRESCRIPTION HUFFMAN-TREE-LISTP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 600
HUFFMAN-TREE-LISTP-PAIRS-TO-LEAVES
generate はハフマン木である。
(defthm huffman-treep-generate
(implies (and (huffman-treep a)
(huffman-tree-listp x)
(consp x))
(huffman-treep (generate x a))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM HUFFMAN-TREEP-GENERATE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION GENERATE)
(:DEFINITION HUFFMAN-TREE-LISTP)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION GENERATE)
(:INDUCTION HUFFMAN-TREE-LISTP)
(:REWRITE HUFFMAN-TREE-LISTP-INSERT)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-NODE)
(:TYPE-PRESCRIPTION HUFFMAN-TREE-LISTP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION INSERT))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 4927
HUFFMAN-TREEP-GENERATE
generate は節である。
(defthm nodep-generate
(implies (and (huffman-treep a)
(huffman-tree-listp x)
(consp x))
(nodep (generate x a))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM NODEP-GENERATE ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION GENERATE)
(:DEFINITION HUFFMAN-TREE-LISTP)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION GENERATE)
(:INDUCTION HUFFMAN-TREE-LISTP)
(:REWRITE HUFFMAN-TREE-LISTP-INSERT)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-NODE)
(:REWRITE NODEP-HUFFMAN-NODE)
(:TYPE-PRESCRIPTION HUFFMAN-TREE-LISTP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION INSERT)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 4927
NODEP-GENERATE
ハフマン木のリストを cdr してもハフマン木のリストである。
(defthm huffman-tree-listp-cdr
(implies (huffman-tree-listp x)
(huffman-tree-listp (cdr x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM HUFFMAN-TREE-LISTP-CDR ...)
Rules: ((:DEFINITION HUFFMAN-TREE-LISTP)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION HUFFMAN-TREE-LISTP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 39
HUFFMAN-TREE-LISTP-CDR
ハフマン木のリストをの car はハフマン木である。
(defthm huffman-treep-car
(implies (and (consp x) (huffman-tree-listp x))
(huffman-treep (car x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM HUFFMAN-TREEP-CAR ...)
Rules: ((:DEFINITION HUFFMAN-TREE-LISTP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 49
HUFFMAN-TREEP-CAR
(< 1 (len x)) は consp で置き換えられる。
(defthm len>1-consp
(equal (< 1 (len x))
(and (consp x)
(consp (cdr x)))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM LEN>1-CONSP ...)
Rules: ((:DEFINITION LEN)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:TYPE-PRESCRIPTION LEN))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 652
LEN>1-CONSP
generate-huffman-tree が返す値は節(nodep)である。
(defthm nodep-generate-huffman-tree
(implies (and (symbol-weight-pair-listp x)
(< 1 (len x)))
(nodep (generate-huffman-tree x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM NODEP-GENERATE-HUFFMAN-TREE ...)
Rules: ((:DEFINITION GENERATE)
(:DEFINITION GENERATE-HUFFMAN-TREE)
(:DEFINITION INSERT)
(:DEFINITION NOT)
(:DEFINITION PAIRS-TO-LEAVES)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART GENERATE)
(:EXECUTABLE-COUNTERPART NODEP)
(:EXECUTABLE-COUNTERPART PAIRS-TO-LEAVES)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION SYMBOL-WEIGHT-PAIR-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREE-LISTP-CDR)
(:REWRITE HUFFMAN-TREE-LISTP-INSERT)
(:REWRITE HUFFMAN-TREE-LISTP-PAIRS-TO-LEAVES)
(:REWRITE HUFFMAN-TREEP-CAR)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-LEAF)
(:REWRITE LEN>1-CONSP)
(:REWRITE NODEP-GENERATE)
(:REWRITE NODEP-HUFFMAN-NODE)
(:TYPE-PRESCRIPTION INSERT)
(:TYPE-PRESCRIPTION NODEP)
(:TYPE-PRESCRIPTION PAIRS-TO-LEAVES)
(:TYPE-PRESCRIPTION SYMBOL-WEIGHT-PAIR-LISTP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION GENERATE)
(:DEFINITION INSERT)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP))
Warnings: Non-rec
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted: 13636
NODEP-GENERATE-HUFFMAN-TREE
generate-huffman-tree が返す値はハフマン木(huffman-treep)である。
(defthm huffman-treep-generate-huffman-tree
(implies (and (symbol-weight-pair-listp x)
(< 1 (len x)))
(huffman-treep (generate-huffman-tree x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM HUFFMAN-TREEP-GENERATE-HUFFMAN-TREE ...)
Rules: ((:DEFINITION GENERATE)
(:DEFINITION GENERATE-HUFFMAN-TREE)
(:DEFINITION INSERT)
(:DEFINITION NOT)
(:DEFINITION PAIRS-TO-LEAVES)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART GENERATE)
(:EXECUTABLE-COUNTERPART HUFFMAN-TREEP)
(:EXECUTABLE-COUNTERPART PAIRS-TO-LEAVES)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION SYMBOL-WEIGHT-PAIR-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREE-LISTP-CDR)
(:REWRITE HUFFMAN-TREE-LISTP-INSERT)
(:REWRITE HUFFMAN-TREE-LISTP-PAIRS-TO-LEAVES)
(:REWRITE HUFFMAN-TREEP-CAR)
(:REWRITE HUFFMAN-TREEP-GENERATE)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-LEAF)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-NODE)
(:REWRITE LEN>1-CONSP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION INSERT)
(:TYPE-PRESCRIPTION PAIRS-TO-LEAVES)
(:TYPE-PRESCRIPTION SYMBOL-WEIGHT-PAIR-LISTP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION GENERATE)
(:DEFINITION INSERT)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP))
Warnings: Non-rec
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted: 13636
HUFFMAN-TREEP-GENERATE-HUFFMAN-TREE
4.3. generate-huffman-tree のガードの検証をする
ここまでに ACL2 に与えたルールが揃っていれば、
generate-huffman-tree のガード検証にも成功します。
(verify-guards generate-huffman-tree)
証明成功: Summary を確認する
Summary
Form: ( VERIFY-GUARDS GENERATE-HUFFMAN-TREE)
Rules: ((:DEFINITION ENDP)
(:DEFINITION INSERT)
(:DEFINITION NOT)
(:DEFINITION ORDERDP)
(:DEFINITION PAIRS-TO-LEAVES)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART ORDERDP)
(:EXECUTABLE-COUNTERPART PAIRS-TO-LEAVES)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEN)
(:INDUCTION PAIRS-TO-LEAVES)
(:INDUCTION SYMBOL-WEIGHT-PAIR-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREE-LISTP-CDR)
(:REWRITE HUFFMAN-TREE-LISTP-INSERT)
(:REWRITE HUFFMAN-TREE-LISTP-PAIRS-TO-LEAVES)
(:REWRITE HUFFMAN-TREEP-CAR)
(:REWRITE HUFFMAN-TREEP-HUFFMAN-LEAF)
(:REWRITE LEN>1-CONSP)
(:REWRITE ORDERDP-INSERT)
(:TYPE-PRESCRIPTION INSERT)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION ORDERDP)
(:TYPE-PRESCRIPTION PAIRS-TO-LEAVES)
(:TYPE-PRESCRIPTION SYMBOL-WEIGHT-PAIR-LISTP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION INSERT)
(:DEFINITION NOT)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP))
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted: 8614
GENERATE-HUFFMAN-TREE
4.4. 記号列からハフマン木を生成する
ハフマン木を生成する関数が定義できたので、 実際のシチュエーションを想定し記号列からハフマン木を構築してみましょう。
そのためには記号列を記号と重みのペアを作成する関数が必要です。
補助関数として count-and-remove を定義します。
これはリストから特定のシンボルの要素の数とシンボルを除いたリストの二つを返す関数です。
(defun count-and-remove (e x) (declare (xargs :guard (true-listp x))) (cond ((endp x) (mv 0 nil)) ((equal e (car x)) (mv-let (c rest) (count-and-remove e (cdr x)) (mv (+ 1 c) rest))) (t (mv-let (c rest) (count-and-remove e (cdr x)) (mv c (cons (car x) rest))))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN COUNT-AND-REMOVE ...)
Rules: ((:DEFINITION COUNT-AND-REMOVE)
(:DEFINITION ENDP)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART ACL2-NUMBERP)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COUNT-AND-REMOVE)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:TYPE-PRESCRIPTION COUNT-AND-REMOVE))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 1514
COUNT-AND-REMOVE
count-and-remove を使用して、記号と重みのペアを作成する関数を定義します。
(defun message-to-pairs (x) (declare (xargs :guard (true-listp x))) (if (endp x) nil (mv-let (c rest) (count-and-remove (car x) x) (cons (list (car x) c) (message-to-pairs rest)))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN MESSAGE-TO-PAIRS ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION COUNT-AND-REMOVE)
(:DEFINITION ENDP)
(:DEFINITION FIX)
(:DEFINITION INTEGER-ABS)
(:DEFINITION LENGTH)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION SYNP)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART MV-NTH)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ACL2-COUNT)
(:INDUCTION COUNT-AND-REMOVE)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-2-OF-+)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE FOLD-CONSTS-IN-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT)
(:TYPE-PRESCRIPTION COUNT-AND-REMOVE))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION ACL2-COUNT)
(:DEFINITION COUNT-AND-REMOVE)
(:DEFINITION INTEGER-ABS))
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted: 8034
MESSAGE-TO-PAIRS
ハムレットの To be, or not to be という詩を与えてみます。
(assign to-be-or-not-to-be
(coerce
"To be, or not to be: that is the question:
Whether 'tis nobler in the mind to suffer
The slings and arrows of outrageous fortune,
Or to take arms against a sea of troubles,
And by opposing end them? To die: to sleep;
No more; and by a sleep to say we end
The heart-ache and the thousand natural shocks
That flesh is heir to, 'tis a consummation
Devoutly to be wish'd. To die, to sleep;
To sleep: perchance to dream: ay, there's the rub;
For in that sleep of death what dreams may come
When we have shuffled off this mortal coil,
Must give us pause: there's the respect
That makes calamity of so long life;
For who would bear the whips and scorns of time,
The oppressor's wrong, the proud man's contumely,
The pangs of despised love, the law's delay,
The insolence of office and the spurns
That patient merit of the unworthy takes,
When he himself might his quietus make
With a bare bodkin? who would fardels bear,
To grunt and sweat under a weary life,
But that the dread of something after death,
The undiscover'd country from whose bourn
No traveller returns, puzzles the will
And makes us rather bear those ills we have
Than fly to others that we know not of?
Thus conscience does make cowards of us all;
And thus the native hue of resolution
Is sicklied o'er with the pale cast of thought,
And enterprises of great pith and moment
With this regard their currents turn awry,
And lose the name of action.--Soft you now!
The fair Ophelia! Nymph, in thy orisons
Be all my sins remember'd!"
'list))
出力:
(#\T #\o #\Space #\b #\e #\, #\Space
#\o #\r #\Space #\n #\o #\t #\Space #\t
#\o #\Space #\b #\e #\: #\Space #\t #\h
#\a #\t #\Space #\i #\s #\Space #\t #\h
#\e #\Space #\q #\u #\e #\s #\t #\i #\o
#\n #\: #\Newline #\W #\h #\e #\t #\h
#\e #\r #\Space #\' #\t #\i #\s #\Space
#\n #\o #\b #\l #\e #\r #\Space #\i
#\n #\Space #\t #\h #\e #\Space #\m #\i
#\n #\d #\Space #\t #\o #\Space #\s #\u
#\f #\f #\e #\r #\Newline #\T #\h #\e
#\Space #\s #\l #\i #\n #\g #\s #\Space
#\a #\n #\d #\Space #\a #\r #\r #\o #\w
#\s #\Space #\o #\f #\Space #\o #\u #\t
#\r #\a #\g #\e #\o #\u #\s #\Space #\f
#\o #\r #\t #\u #\n #\e #\, #\Newline
#\O #\r #\Space #\t #\o #\Space #\t #\a
#\k #\e #\Space #\a #\r #\m #\s #\Space
#\a #\g #\a #\i #\n #\s #\t #\Space
#\a #\Space #\s #\e #\a #\Space #\o
#\f #\Space #\t #\r #\o #\u #\b #\l #\e
#\s #\, #\Newline #\A #\n #\d #\Space
#\b #\y #\Space #\o #\p #\p #\o #\s #\i
#\n #\g #\Space #\e #\n #\d #\Space #\t
#\h #\e #\m #\? #\Space #\T #\o #\Space
#\d #\i #\e #\: #\Space #\t #\o #\Space
#\s #\l #\e #\e #\p #\; #\Newline #\N
#\o #\Space #\m #\o #\r #\e #\; #\Space
#\a #\n #\d #\Space #\b #\y #\Space
#\a #\Space #\s #\l #\e #\e #\p #\Space
#\t #\o #\Space #\s #\a #\y #\Space
#\w #\e #\Space #\e #\n #\d #\Newline
#\T #\h #\e #\Space #\h #\e #\a #\r
#\t #\- #\a #\c #\h #\e #\Space #\a #\n
#\d #\Space #\t #\h #\e #\Space #\t #\h
#\o #\u #\s #\a #\n #\d #\Space #\n #\a
#\t #\u #\r #\a #\l #\Space #\s #\h #\o
#\c #\k #\s #\Newline #\T #\h #\a #\t
#\Space #\f #\l #\e #\s #\h #\Space #\i
#\s #\Space #\h #\e #\i #\r #\Space #\t
#\o #\, #\Space #\' #\t #\i #\s #\Space
#\a #\Space #\c #\o #\n #\s #\u #\m
#\m #\a #\t #\i #\o #\n #\Newline #\D
#\e #\v #\o #\u #\t #\l #\y #\Space #\t
#\o #\Space #\b #\e #\Space #\w #\i #\s
#\h #\' #\d #\. #\Space #\T #\o #\Space
#\d #\i #\e #\, #\Space #\t #\o #\Space
#\s #\l #\e #\e #\p #\; #\Newline
#\T #\o #\Space #\s #\l #\e #\e #\p #\:
#\Space #\p #\e #\r #\c #\h #\a #\n #\c
#\e #\Space #\t #\o #\Space #\d #\r #\e
#\a #\m #\: #\Space #\a #\y #\, #\Space
#\t #\h #\e #\r #\e #\' #\s #\Space
#\t #\h #\e #\Space #\r #\u #\b #\;
#\Newline #\F #\o #\r #\Space #\i #\n
#\Space #\t #\h #\a #\t #\Space #\s #\l
#\e #\e #\p #\Space #\o #\f #\Space #\d
#\e #\a #\t #\h #\Space #\w #\h #\a #\t
#\Space #\d #\r #\e #\a #\m #\s #\Space
#\m #\a #\y #\Space #\c #\o #\m #\e
#\Newline #\W #\h #\e #\n #\Space #\w
#\e #\Space #\h #\a #\v #\e #\Space #\s
#\h #\u #\f #\f #\l #\e #\d #\Space #\o
#\f #\f #\Space #\t #\h #\i #\s #\Space
#\m #\o #\r #\t #\a #\l #\Space #\c #\o
#\i #\l #\, #\Newline #\M #\u #\s #\t
#\Space #\g #\i #\v #\e #\Space #\u #\s
#\Space #\p #\a #\u #\s #\e #\: #\Space
#\t #\h #\e #\r #\e #\' #\s #\Space #\t
#\h #\e #\Space #\r #\e #\s #\p #\e #\c
#\t #\Newline #\T #\h #\a #\t #\Space
#\m #\a #\k #\e #\s #\Space #\c #\a
#\l #\a #\m #\i #\t #\y #\Space #\o #\f
#\Space #\s #\o #\Space #\l #\o #\n #\g
#\Space #\l #\i #\f #\e #\; #\Newline
#\F #\o #\r #\Space #\w #\h #\o #\Space
#\w #\o #\u #\l #\d #\Space #\b #\e #\a
#\r #\Space #\t #\h #\e #\Space #\w #\h
#\i #\p #\s #\Space #\a #\n #\d #\Space
#\s #\c #\o #\r #\n #\s #\Space #\o #\f
#\Space #\t #\i #\m #\e #\, #\Newline
#\T #\h #\e #\Space #\o #\p #\p
#\r #\e #\s #\s #\o #\r #\' #\s #\Space
#\w #\r #\o #\n #\g #\, #\Space #\t #\h
#\e #\Space #\p #\r #\o #\u #\d #\Space
#\m #\a #\n #\' #\s #\Space #\c #\o #\n
#\t #\u #\m #\e #\l #\y #\, #\Newline
#\T #\h #\e #\Space #\p #\a #\n
#\g #\s #\Space #\o #\f #\Space #\d #\e
#\s #\p #\i #\s #\e #\d #\Space #\l #\o
#\v #\e #\, #\Space #\t #\h #\e #\Space
#\l #\a #\w #\' #\s #\Space #\d #\e
#\l #\a #\y #\, #\Newline #\T #\h #\e
#\Space #\i #\n #\s #\o #\l #\e #\n #\c
#\e #\Space #\o #\f #\Space #\o #\f #\f
#\i #\c #\e #\Space #\a #\n #\d #\Space
#\t #\h #\e #\Space #\s #\p #\u #\r #\n
#\s #\Newline #\T #\h #\a #\t #\Space
#\p #\a #\t #\i #\e #\n #\t #\Space
#\m #\e #\r #\i #\t #\Space #\o #\f
#\Space #\t #\h #\e #\Space #\u #\n #\w
#\o #\r #\t #\h #\y #\Space #\t #\a #\k
#\e #\s #\, #\Newline #\W #\h #\e #\n
#\Space #\h #\e #\Space #\h #\i #\m #\s
#\e #\l #\f #\Space #\m #\i #\g #\h #\t
#\Space #\h #\i #\s #\Space #\q #\u #\i
#\e #\t #\u #\s #\Space #\m #\a #\k #\e
#\Newline #\W #\i #\t #\h #\Space #\a
#\Space #\b #\a #\r #\e #\Space #\b #\o
#\d #\k #\i #\n #\? #\Space #\w #\h #\o
#\Space #\w #\o #\u #\l #\d #\Space #\f
#\a #\r #\d #\e #\l #\s #\Space #\b #\e
#\a #\r #\, #\Newline #\T #\o #\Space
#\g #\r #\u #\n #\t #\Space #\a #\n #\d
#\Space #\s #\w #\e #\a #\t #\Space #\u
#\n #\d #\e #\r #\Space #\a #\Space #\w
#\e #\a #\r #\y #\Space #\l #\i #\f #\e
#\, #\Newline #\B #\u #\t #\Space #\t
#\h #\a #\t #\Space #\t #\h #\e #\Space
#\d #\r #\e #\a #\d #\Space #\o #\f
#\Space #\s #\o #\m #\e #\t #\h #\i #\n
#\g #\Space #\a #\f #\t #\e #\r #\Space
#\d #\e #\a #\t #\h #\, #\Newline #\T
#\h #\e #\Space #\u #\n #\d #\i #\s #\c
#\o #\v #\e #\r #\' #\d #\Space #\c #\o
#\u #\n #\t #\r #\y #\Space #\f #\r #\o
#\m #\Space #\w #\h #\o #\s #\e #\Space
#\b #\o #\u #\r #\n #\Newline #\N #\o
#\Space #\t #\r #\a #\v #\e #\l #\l #\e
#\r #\Space #\r #\e #\t #\u #\r #\n #\s
#\, #\Space #\p #\u #\z #\z #\l #\e #\s
#\Space #\t #\h #\e #\Space #\w #\i #\l
#\l #\Newline #\A #\n #\d #\Space #\m
#\a #\k #\e #\s #\Space #\u #\s #\Space
#\r #\a #\t #\h #\e #\r #\Space #\b
#\e #\a #\r #\Space #\t #\h #\o #\s #\e
#\Space #\i #\l #\l #\s #\Space #\w #\e
#\Space #\h #\a #\v #\e #\Newline #\T
#\h #\a #\n #\Space #\f #\l #\y #\Space
#\t #\o #\Space #\o #\t #\h #\e #\r #\s
#\Space #\t #\h #\a #\t #\Space #\w #\e
#\Space #\k #\n #\o #\w #\Space #\n #\o
#\t #\Space #\o #\f #\? #\Newline #\T
#\h #\u #\s #\Space #\c #\o #\n #\s #\c
#\i #\e #\n #\c #\e #\Space #\d #\o #\e
#\s #\Space #\m #\a #\k #\e #\Space #\c
#\o #\w #\a #\r #\d #\s #\Space #\o #\f
#\Space #\u #\s #\Space #\a #\l #\l #\;
#\Newline #\A #\n #\d #\Space #\t #\h
#\u #\s #\Space #\t #\h #\e #\Space #\n
#\a #\t #\i #\v #\e #\Space #\h #\u #\e
#\Space #\o #\f #\Space #\r #\e #\s #\o
#\l #\u #\t #\i #\o #\n #\Newline #\I
#\s #\Space #\s #\i #\c #\k #\l #\i #\e
#\d #\Space #\o #\' #\e #\r #\Space #\w
#\i #\t #\h #\Space #\t #\h #\e #\Space
#\p #\a #\l #\e #\Space #\c #\a #\s #\t
#\Space #\o #\f #\Space #\t #\h #\o #\u
#\g #\h #\t #\, #\Newline #\A #\n #\d
#\Space #\e #\n #\t #\e #\r #\p #\r #\i
#\s #\e #\s #\Space #\o #\f #\Space #\g
#\r #\e #\a #\t #\Space #\p #\i #\t #\h
#\Space #\a #\n #\d #\Space #\m #\o #\m
#\e #\n #\t #\Newline #\W #\i #\t #\h
#\Space #\t #\h #\i #\s #\Space #\r #\e
#\g #\a #\r #\d #\Space #\t #\h #\e #\i
#\r #\Space #\c #\u #\r #\r #\e #\n #\t
#\s #\Space #\t #\u #\r #\n #\Space #\a
#\w #\r #\y #\, #\Newline #\A #\n #\d
#\Space #\l #\o #\s #\e #\Space #\t #\h
#\e #\Space #\n #\a #\m #\e #\Space #\o
#\f #\Space #\a #\c #\t #\i #\o #\n #\.
#\- #\- #\S #\o #\f #\t #\Space #\y #\o
#\u #\Space #\n #\o #\w #\! #\Newline
#\T #\h #\e #\Space #\f #\a #\i #\r
#\Space #\O #\p #\h #\e #\l #\i #\a #\!
#\Space #\N #\y #\m #\p #\h #\, #\Space
#\i #\n #\Space #\t #\h #\y #\Space
#\o #\r #\i #\s #\o #\n #\s #\Newline
#\B #\e #\Space #\a #\l #\l #\Space #\m
#\y #\Space #\s #\i #\n #\s #\Space #\r
#\e #\m #\e #\m #\b #\e #\r #\' #\d #\!)
(message-to-pairs (@ to-be-or-not-to-be))
出力を確認する
((#\T 17) (#\o 97) (#\Space 240) (#\b 15) (#\e 146) (#\, 20) (#\r 71) (#\n 67) (#\t 103) (#\: 6) (#\h 79) (#\a 82) (#\i 56) (#\s 87) (#\q 2) (#\u 41) (#\Newline 34) (#\W 5) (#\' 11) (#\l 44) (#\m 31) (#\d 42) (#\f 34) (#\g 14) (#\w 24) (#\O 2) (#\k 10) (#\A 5) (#\y 18) (#\p 24) (#\? 3) (#\; 6) (#\N 3) (#\- 3) (#\c 23) (#\D 1) (#\v 8) (#\. 2) (#\F 2) (#\M 1) (#\B 2) (#\z 2) (#\I 1) (#\S 1) (#\! 3))
シンボルと重みのリストができました。 これからハフマン木を生成してみましょう。
(assign tree (generate-huffman-tree (message-to-pairs (@ to-be-or-not-to-be))))
出力を確認する
(NODE
(#\f #\v #\W #\A #\y #\r #\e #\h #\,
#\k #\' #\u #\a #\d #\l #\s #\c #\: #\;
#\- #\! #\? #\N #\w #\p #\o #\t #\Space
#\i #\g #\b #\m #\q #\O #\I #\S #\D
#\M #\B #\z #\. #\F #\T #\Newline #\n)
1488
(NODE (#\f #\v #\W #\A #\y
#\r #\e #\h #\, #\k #\' #\u #\a #\d #\l)
616
(NODE (#\f #\v #\W #\A #\y #\r #\e)
287
(NODE (#\f #\v #\W #\A #\y #\r)
141
(NODE (#\f #\v #\W #\A #\y)
70 (LEAF #\f 34)
(NODE (#\v #\W #\A #\y)
36
(NODE (#\v #\W #\A)
18 (LEAF #\v 8)
(NODE (#\W #\A)
10 (LEAF #\W 5)
(LEAF #\A 5)))
(LEAF #\y 18)))
(LEAF #\r 71))
(LEAF #\e 146))
(NODE (#\h #\, #\k #\' #\u #\a #\d #\l)
329
(NODE (#\h #\, #\k #\' #\u)
161 (LEAF #\h 79)
(NODE (#\, #\k #\' #\u)
82
(NODE (#\, #\k #\')
41 (LEAF #\, 20)
(NODE (#\k #\')
21 (LEAF #\k 10)
(LEAF #\' 11)))
(LEAF #\u 41)))
(NODE (#\a #\d #\l)
168 (LEAF #\a 82)
(NODE (#\d #\l)
86 (LEAF #\d 42)
(LEAF #\l 44)))))
(NODE
(#\s #\c #\: #\;
#\- #\! #\? #\N #\w #\p #\o #\t #\Space
#\i #\g #\b #\m #\q #\O #\I #\S #\D
#\M #\B #\z #\. #\F #\T #\Newline #\n)
872
(NODE (#\s #\c
#\: #\; #\- #\! #\? #\N #\w #\p #\o #\t)
382
(NODE (#\s #\c #\: #\; #\- #\! #\? #\N #\w #\p)
182 (LEAF #\s 87)
(NODE (#\c #\: #\; #\- #\! #\? #\N #\w #\p)
95
(NODE (#\c #\: #\; #\- #\! #\? #\N)
47 (LEAF #\c 23)
(NODE (#\: #\; #\- #\! #\? #\N)
24
(NODE (#\: #\;)
12 (LEAF #\: 6)
(LEAF #\; 6))
(NODE (#\- #\! #\? #\N)
12
(NODE (#\- #\!)
6 (LEAF #\- 3)
(LEAF #\! 3))
(NODE (#\? #\N)
6 (LEAF #\? 3)
(LEAF #\N 3)))))
(NODE (#\w #\p)
48 (LEAF #\w 24)
(LEAF #\p 24))))
(NODE (#\o #\t)
200 (LEAF #\o 97)
(LEAF #\t 103)))
(NODE
(#\Space #\i #\g #\b #\m #\q #\O #\I #\S #\D
#\M #\B #\z #\. #\F #\T #\Newline #\n)
490 (LEAF #\Space 240)
(NODE (#\i #\g #\b #\m #\q #\O #\I #\S #\D
#\M #\B #\z #\. #\F #\T #\Newline #\n)
250
(NODE (#\i #\g #\b #\m)
116 (LEAF #\i 56)
(NODE (#\g #\b #\m)
60
(NODE (#\g #\b)
29 (LEAF #\g 14)
(LEAF #\b 15))
(LEAF #\m 31)))
(NODE (#\q #\O #\I #\S #\D
#\M #\B #\z #\. #\F #\T #\Newline #\n)
134
(NODE (#\q #\O #\I #\S
#\D #\M #\B #\z #\. #\F #\T #\Newline)
67
(NODE (#\q #\O #\I #\S #\D #\M #\B #\z #\. #\F #\T)
33
(NODE (#\q #\O #\I #\S #\D #\M #\B #\z #\. #\F)
16
(NODE (#\q #\O #\I #\S #\D #\M)
8
(NODE (#\q #\O)
4 (LEAF #\q 2)
(LEAF #\O 2))
(NODE (#\I #\S #\D #\M)
4
(NODE (#\I #\S)
2 (LEAF #\I 1)
(LEAF #\S 1))
(NODE (#\D #\M)
2 (LEAF #\D 1)
(LEAF #\M 1))))
(NODE (#\B #\z #\. #\F)
8
(NODE (#\B #\z)
4 (LEAF #\B 2)
(LEAF #\z 2))
(NODE (#\. #\F)
4 (LEAF #\. 2)
(LEAF #\F 2))))
(LEAF #\T 17))
(LEAF #\Newline 34))
(LEAF #\n 67))))))
ハフマン木ができていますね(確認するには「出力を確認する」をクリックしてください)。
message-to-pairs の結果が symbol-weight-pair-listp であることを証明します。
(defthm rationalp-0-count-and-remove (rationalp (car (count-and-remove e x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM RATIONALP-0-COUNT-AND-REMOVE ...)
Rules: ((:DEFINITION COUNT-AND-REMOVE)
(:DEFINITION ENDP)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART RATIONALP)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COUNT-AND-REMOVE)
(:REWRITE CAR-CONS)
(:TYPE-PRESCRIPTION COUNT-AND-REMOVE))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 855
RATIONALP-0-COUNT-AND-REMOVE
(defthm symbol-weight-pair-listp-message-to-pairs (symbol-weight-pair-listp (message-to-pairs x)))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM SYMBOL-WEIGHT-PAIR-LISTP-MESSAGE-TO-PAIRS ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION MESSAGE-TO-PAIRS)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:DEFINITION SYMBOL-WEIGHT-PAIR-LISTP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART SYMBOL-WEIGHT-PAIR-LISTP)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MESSAGE-TO-PAIRS)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE RATIONALP-0-COUNT-AND-REMOVE)
(:TYPE-PRESCRIPTION COUNT-AND-REMOVE)
(:TYPE-PRESCRIPTION MESSAGE-TO-PAIRS)
(:TYPE-PRESCRIPTION SYMBOL-WEIGHT-PAIR-LISTP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 564
SYMBOL-WEIGHT-PAIR-LISTP-MESSAGE-TO-PAIRS
5. ハフマン符号化を実装する
本題のハフマン符号化の実装に入ります。
まず一つのシンボルのみビット列に符号化する関数 encode-1 を定義します。
(defun encode-1 (x tree) (declare (xargs :guard (huffman-treep tree) :measure (node-count tree))) (if (nodep tree) (cond ((member-equal x (symbol-list (left tree))) (cons 0 (encode-1 x (left tree)))) (t (cons 1 (encode-1 x (right tree))))) nil))
証明成功: Summary を確認する
Summary
Form: ( DEFUN ENCODE-1 ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O-P)
(:DEFINITION O<)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:LINEAR NODE-COUNT-LEFT)
(:LINEAR NODE-COUNT-RIGHT)
(:TYPE-PRESCRIPTION NODE-COUNT)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 378
ENCODE-1
encode-1 を使用してシンボル列をビット列に変換する encode を定義します。
(defun encode (x tree) (declare (xargs :guard (and (true-listp x) (nodep tree) (huffman-treep tree)))) (if (endp x) nil (append (encode-1 (car x) tree) (encode (cdr x) tree))))
Summary を確認する
Summary
Form: ( DEFUN ENCODE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION ENCODE-1)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ENCODE
先程用意した To be, or not to be を encode に与えてみます。
(assign bits (encode (@ to-be-or-not-to-be) (@ tree)))
出力を確認する
(1 1 1 1 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 1 0 0 1 0 1 0 1 0 0 1 1 0 1 0 1 0 0 0 0 1 1 1 0 1 1 1 1 1 1 0 1 0 1 0 1 1 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 1 1 0 1 0 1 0 0 1 1 0 0 1 0 1 0 0 1 1 0 1 0 1 1 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 1 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 1 1 1 0 0 0 0 0 0 0 1 0 1 1 0 0 1 1 0 0 0 1 0 1 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 1 0 0 1 0 1 0 0 1 1 1 1 0 1 0 0 0 0 1 0 1 0 0 1 0 0 0 0 1 1 0 1 1 0 1 0 0 0 0 1 0 0 0 1 1 1 0 0 1 0 1 0 1 1 1 0 1 1 1 1 1 0 0 1 0 0 0 1 1 0 1 1 1 1 1 1 0 1 0 1 1 1 0 1 0 1 0 1 1 1 1 0 0 1 0 0 0 1 1 1 0 1 1 1 0 0 1 1 1 1 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 1 1 0 1 1 1 1 1 0 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 0 1 1 1 0 1 0 0 0 0 1 1 1 1 1 1 1 0 0 1 1 1 1 1 1 1 1 0 1 0 0 1 0 0 0 1 1 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 0 1 1 0 0 0 0 1 0 0 0 1 1 0 1 0 1 0 0 1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 1 0 0 1 0 1 1 1 0 1 1 0 0 0 1 0 1 1 0 1 1 1 0 1 0 0 0 0 1 1 0 1 0 0 1 0 1 1 1 0 0 0 1 1 0 0 0 0 0 0 1 0 1 0 0 0 0 1 1 0 1 1 0 1 0 1 1 1 1 1 1 1 0 0 1 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 0 0 0 1 0 0 0 1 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 1 1 1 0 0 0 1 1 0 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 0 1 1 1 1 0 0 1 1 0 1 1 0 1 0 0 0 0 0 1 0 1 1 0 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 1 1 0 0 0 1 1 0 1 0 0 1 0 1 1 1 1 1 0 1 0 1 0 1 1 1 1 0 0 1 1 0 0 0 0 1 0 1 0 0 1 1 1 1 0 1 0 0 0 0 1 0 1 1 1 1 1 1 1 0 1 1 1 0 1 1 0 1 1 1 0 1 0 1 0 0 0 0 1 1 1 1 0 1 0 1 0 1 0 0 1 1 1 1 0 0 1 1 1 1 0 1 0 1 0 0 0 1 1 1 0 0 1 1 1 1 1 1 1 1 0 1 0 0 1 1 0 0 0 1 1 1 1 1 1 0 1 1 1 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 1 0 1 1 1 0 0 1 0 1 1 1 0 1 1 0 1 1 1 1 0 0 1 1 0 1 0 1 1 0 0 1 1 1 0 1 1 1 0 0 0 0 1 1 0 0 1 0 1 0 0 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 1 0 0 1 0 0 1 1 0 0 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 1 0 0 1 0 1 1 1 1 1 0 1 0 1 1 0 1 1 1 0 1 1 1 0 1 0 0 0 0 1 0 0 1 1 0 0 1 0 1 0 1 1 1 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 1 1 0 1 0 1 0 0 0 0 1 1 1 1 0 0 1 1 0 1 1 0 1 0 0 0 0 1 1 1 1 0 0 1 0 0 1 1 0 0 1 1 1 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 0 0 0 0 0 1 1 1 1 0 1 0 0 1 1 0 0 0 1 1 1 0 0 0 1 1 1 1 1 1 0 1 1 1 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 0 1 1 1 0 0 1 0 0 0 0 1 0 1 1 0 0 0 0 1 1 0 1 1 1 0 0 1 0 1 1 0 0 0 1 1 0 1 0 0 1 0 0 0 1 0 0 0 0 1 1 1 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 0 1 1 0 1 0 0 1 0 1 0 0 1 0 1 1 1 0 0 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 1 1 1 1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 0 1 0 1 1 0 0 1 1 1 1 1 1 0 1 0 0 0 0 1 0 0 1 0 1 0 1 0 0 1 0 0 0 1 0 1 0 1 0 1 0 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 0 0 0 0 0 0 1 1 1 1 0 0 1 1 0 0 0 0 1 0 0 1 1 0 1 1 1 0 0 1 0 0 0 1 1 0 0 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 1 1 0 1 0 1 1 1 0 1 0 0 1 0 1 0 0 1 1 0 0 1 0 1 0 1 1 1 0 1 1 1 1 1 0 0 1 0 0 0 1 1 0 0 1 1 0 1 1 0 1 0 0 1 0 0 1 0 1 0 1 1 1 1 1 1 0 0 0 0 1 0 1 1 1 1 1 0 1 1 1 1 1 0 1 1 0 1 1 0 1 0 1 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 1 1 1 1 0 0 0 0 1 1 0 0 0 1 0 0 0 0 1 0 0 1 0 1 0 0 1 0 1 1 1 0 1 1 0 1 1 1 1 0 0 0 0 1 1 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 1 1 0 1 0 1 0 0 1 1 1 0 1 0 0 1 1 0 1 1 1 0 0 1 0 0 0 0 1 0 0 0 1 0 1 0 1 1 0 1 1 1 0 1 1 1 1 0 0 0 1 1 0 1 1 0 1 1 1 1 0 0 1 1 0 1 0 1 1 0 0 1 1 1 0 1 1 1 0 0 0 0 1 0 1 0 1 0 0 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 1 0 0 1 0 0 1 1 0 0 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 1 1 1 1 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 1 0 0 1 0 0 1 1 0 0 1 1 1 1 0 0 1 0 1 0 0 1 1 0 1 0 0 1 1 1 0 0 1 0 0 0 1 1 0 0 1 0 0 0 1 0 0 0 1 1 0 1 1 1 1 1 1 0 0 1 0 0 0 0 1 1 1 0 1 0 1 1 1 0 1 0 1 1 0 0 1 1 1 0 0 0 0 1 0 0 1 0 1 1 0 1 1 1 0 1 1 1 0 0 1 0 1 0 0 1 1 0 0 1 1 0 0 0 0 0 1 1 0 1 0 1 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 0 0 0 1 0 0 1 0 1 0 1 0 1 1 1 0 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 0 0 0 1 0 1 0 1 1 1 1 1 0 1 0 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 1 1 1 1 0 0 0 1 1 1 1 0 1 0 0 0 0 1 1 1 0 1 1 1 0 0 1 1 1 1 1 1 1 0 1 0 1 1 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 1 0 0 0 0 1 1 1 1 0 0 1 0 0 1 1 0 0 1 1 1 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 0 1 1 1 0 0 0 1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 1 0 0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 0 1 1 1 0 0 0 0 1 0 0 1 0 1 1 0 1 1 1 0 1 1 1 0 0 0 1 1 0 1 1 1 0 1 1 0 1 1 0 0 0 0 0 1 1 1 1 0 1 0 0 1 0 0 1 0 1 0 1 1 1 0 1 1 0 0 1 1 1 1 1 0 1 0 0 0 0 1 0 1 0 0 1 0 0 0 0 1 1 1 1 1 1 1 1 0 1 0 0 1 1 0 0 0 1 1 1 0 0 1 0 0 0 1 1 0 0 0 0 0 1 0 0 0 0 1 1 1 0 1 0 0 0 0 1 0 0 0 1 0 1 1 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 0 0 1 0 1 1 1 0 1 1 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 1 1 0 1 0 1 1 0 1 0 0 1 1 1 0 0 1 0 0 0 1 1 0 1 1 1 0 1 1 1 0 1 0 0 0 0 1 1 0 1 1 0 1 1 0 0 1 1 1 1 1 1 0 1 0 0 1 0 0 1 0 1 0 1 1 1 0 0 0 1 1 1 1 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 0 0 1 1 1 0 1 0 1 1 1 0 0 0 1 0 1 1 1 1 0 1 1 1 0 1 0 0 1 1 1 0 0 0 0 0 0 1 0 0 0 0 1 1 1 0 0 1 0 1 1 1 0 0 0 1 1 0 1 0 0 1 1 1 0 1 1 0 0 1 0 1 1 1 0 0 0 0 0 1 1 0 0 1 0 1 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 0 0 0 1 0 0 1 0 1 0 1 0 1 1 1 0 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 0 0 0 1 0 0 1 1 0 0 0 1 0 0 1 1 1 0 0 1 1 0 0 1 0 0 1 0 1 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 1 1 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 0 0 0 1 1 0 1 0 0 1 0 0 0 1 1 0 0 1 1 1 1 0 1 1 0 1 1 1 0 1 1 1 1 1 0 0 1 0 1 1 0 0 0 0 1 1 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 0 0 1 0 1 0 1 1 0 0 1 1 1 1 1 0 1 0 1 1 1 1 1 1 1 1 0 1 0 0 1 1 0 0 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 1 1 1 1 0 0 0 1 1 1 1 0 1 0 0 0 0 1 1 1 0 1 0 0 1 1 0 0 1 0 0 1 0 1 0 1 1 0 1 0 0 1 1 0 1 0 1 0 0 1 0 1 1 0 1 1 1 1 0 1 1 1 0 1 1 0 1 1 1 0 1 0 1 0 0 1 0 1 1 0 0 0 0 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 0 0 1 1 0 0 1 0 0 1 1 1 0 0 1 0 0 1 1 1 1 0 0 0 1 1 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 0 0 0 1 0 0 1 0 0 1 0 1 0 0 0 0 1 1 1 1 1 1 1 0 0 0 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 1 1 1 1 1 0 0 1 1 1 0 1 1 0 0 1 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 0 1 1 1 0 1 0 1 0 1 0 0 1 1 1 1 0 0 1 1 1 0 0 0 1 0 0 1 1 0 0 0 1 0 0 0 1 0 1 0 0 0 0 1 0 1 0 1 0 1 1 1 0 0 0 1 1 0 1 0 0 1 1 0 0 0 0 1 1 0 1 0 1 1 1 1 1 1 1 1 0 1 0 0 0 1 0 1 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 0 0 1 1 1 0 0 0 1 1 0 1 0 0 1 0 1 1 0 1 1 1 0 1 1 0 1 1 1 0 1 1 0 1 1 0 1 1 1 1 1 0 1 0 1 0 1 1 1 0 0 0 1 1 0 1 0 0 1 0 0 1 0 1 0 1 1 1 1 1 1 0 1 1 0 1 0 1 1 1 1 1 0 1 1 0 0 1 0 1 1 1 1 0 0 0 0 1 1 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 0 1 1 1 0 1 0 0 1 1 1 0 1 1 0 1 1 1 1 1 1 1 1 0 1 0 0 1 0 0 0 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 0 1 1 1 0 0 0 1 1 0 0 0 1 0 0 1 1 1 1 1 1 0 0 1 0 0 0 0 0 1 0 1 1 1 0 1 1 0 0 1 1 1 1 1 0 1 0 0 0 0 0 1 0 0 0 0 1 0 1 0 1 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 0 1 1 1 1 0 1 1 0 1 0 0 1 1 0 0 1 0 1 0 1 1 1 0 0 0 1 1 0 0 1 1 1 0 0 0 1 0 1 1 1 1 0 1 1 0 0 0 0 0 1 1 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 0 1 1 1 0 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 0 1 0 0 1 1 1 1 0 0 1 1 1 1 1 1 1 0 0 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 1 0 0 1 0 0 0 0 1 1 1 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 0 0 0 1 0 0 1 1 1 0 1 0 1 1 0 0 0 1 1 1 1 1 1 1 0 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 1 0 0 1 1 1 0 1 1 0 1 0 1 1 1 1 1 0 0 0 0 1 1 1 1 1 1 1 0 1 1 1 1 0 1 1 1 0 1 1 0 0 1 0 0 0 1 1 1 1 0 0 1 0 1 1 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 0 1 0 1 1 1 1 1 1 1 1 0 0 1 1 0 1 0 1 0 0 0 0 1 1 0 1 1 0 1 0 0 0 0 0 0 1 1 1 1 0 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 0 0 0 0 1 0 1 0 0 1 1 1 1 0 1 0 0 0 0 1 0 1 0 0 1 0 0 0 0 1 1 1 1 1 1 1 1 0 0 1 0 0 0 0 1 1 1 0 0 1 0 0 1 1 1 0 0 1 1 1 0 1 1 1 0 0 0 0 0 1 0 1 1 1 1 0 0 0 0 0 1 1 0 1 1 1 0 1 1 1 1 1 0 0 1 1 1 0 1 0 0 0 1 0 0 1 0 1 1 1 1 0 0 1 0 0 1 1 1 0 0 1 0 0 0 1 1 0 1 1 1 1 0 0 0 0 0 0 0 1 0 1 1 1 1 1 0 0 0 0 1 1 0 1 1 0 1 0 1 1 1 0 0 0 1 1 0 1 1 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 1 1 1 0 1 0 0 0 0 1 0 1 0 1 1 1 0 0 1 0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1 1 1 0 1 0 1 0 1 1 0 0 0 0 1 0 0 1 1 1 0 1 1 1 0 1 0 1 1 0 1 0 0 1 1 1 0 0 1 0 1 0 1 0 1 1 1 0 0 1 1 1 1 1 1 0 0 1 0 1 1 1 0 1 1 0 1 0 0 1 1 0 0 1 0 0 1 0 1 0 1 1 0 1 0 0 1 1 0 1 0 1 0 0 1 0 1 1 0 1 1 1 1 0 1 1 1 0 1 1 0 0 0 0 0 0 0 1 1 0 0 0 0 1 0 1 1 1 0 0 0 1 0 1 1 1 1 1 0 0 0 1 1 0 1 1 1 0 1 0 1 0 0 1 0 1 1 0 0 0 0 1 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 0 1 0 1 1 1 1 1 1 1 1 0 1 1 1 1 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 0 0 0 1 0 0 1 1 0 0 0 1 0 1 1 0 1 0 1 1 1 1 0 0 1 0 1 1 1 1 1 1 1 0 1 1 1 0 0 0 1 0 0 0 1 1 1 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 0 1 0 1 1 0 0 0 0 1 0 0 0 0 1 1 1 1 0 0 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 1 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 0 1 0 0 0 1 0 1 1 1 0 1 1 1 1 0 1 0 1 1 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 0 1 1 1 0 0 0 0 1 0 0 1 0 1 1 0 0 1 1 1 0 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 0 0 1 0 1 0 1 1 1 0 1 1 0 0 1 1 0 1 1 0 1 0 0 1 1 1 0 0 1 1 1 1 1 1 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 0 0 0 1 0 1 1 0 0 1 0 0 0 1 1 1 0 0 1 1 1 0 0 0 1 0 1 1 0 1 0 1 1 0 1 0 0 0 1 0 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 0 1 1 1 0 0 1 0 1 1 1 1 1 1 1 0 1 1 1 0 1 1 1 0 0 1 0 0 0 1 0 0 1 0 0 1 0 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 1 0 1 0 1 0 1 1 0 1 1 1 0 1 1 0 1 0 0 1 0 0 1 0 1 0 0 1 0 1 1 1 1 1 1 1 1 0 1 1 0 0 0 1 0 0 0 0 1 1 1 1 0 0 0 0 0 0 0 0 0 1 1 0 1 0 1 1 1 0 1 1 1 1 0 1 0 0 1 1 0 0 1 0 0 1 0 1 0 1 0 0 0 0 0 1 1 1 0 1 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 0 0 1 1 1 1 1 1 1 1 1 1 0 1 1 0 0 1 0 1 1 1 1 1 0 1 0 1 1 0 1 0 1 1 0 0 0 1 0 1 1 0 0 0 0 0 1 0 0 0 0 1 0 1 1 1 1 0 1 1 1 1 0 0 1 0 0 0 1 1 1 0 0 0 0 1 0 0 1 1 0 1 1 0 1 0 1 1 0 0 0 1 1 1 1 1 1 1 0 0 0 0 1 0 1 0 0 1 1 0 1 0 0 1 1 1 0 1 0 1 1 1 1 1 1 0 0 0 1 0 1 1 1 1 1 0 0 0 1 0 1 0 1 1 1 1 0 0 1 1 0 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 0 0 1 1 0 1 1 1 0 0 0 1 1 1 1 0 1 1 1 1 1 1 1 1 0 1 0 0 0 0 1 0 1 1 1 1 1 1 1 0 1 1 1 0 1 1 0 1 1 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 0 0 0 1 1 0 0 1 0 1 1 1 0 0 0 1 1 0 0 0 0 1 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 0 0 0 1 1 1 0 1 1 1 0 1 0 1 0 0 1 0 1 1 0 0 0 0 1 1 1 0 1 0 1 1 0 1 0 0 1 0 1 0 1 0 0 0 0 0 1 1 1 0 1 1 1 0 0 0 1 1 1 1 0 1 1 1 1 1 0 0 0 1 1 0 1 0 0 1 1 0 0 0 1 1 1 0 0 1 0 0 0 1 1 0 0 0 0 0 1 0 0 0 0 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 1 1 0 1 1 1 1 1 1 1 0 0 0 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 0 1 0 1 1 1 0 1 0 1 1 0 1 0 1 0 1 0 1 1 0 1 0 0 0 0 1 0 0 0 1 1 0 0 0 1 1 0 1 0 1 1 0 1 0 0 0 1 1 0 1 0 1 1 1 1 0 1 0 0 1 1 0 0 0 1 1 1 0 0 1 0 1 0 1 0 1 1 1 1 1 1 0 1 0 1 0 0 1 1 0 1 1 0 1 1 1 1 1 1 0 1 0 1 0 1 1 1 1 0 1 0 1 0 0 0 0 0 0 1 0 0 1 0 1 1 1 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 1 0 1 1 1 0 0 0 1 1 0 1 0 0 1 0 0 1 0 1 0 1 1 1 1 1 1 0 0 0 1 0 0 1 0 0 1 1 1 0 0 0 0 1 1 1 1 1 1 1 0 0 1 0 0 0 0 1 1 1 0 0 1 1 1 0 1 0 1 0 0 0 1 1 0 0 0 1 1 0 1 1 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 1 0 1 0 0 1 0 0 1 0 1 0 1 0 0 1 1 0 0 1 1 0 0 0 0 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 0 1 0 1 1 1 0 0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 0 0 0 0 1 0 1 1 1 1 1 1 1 0 1 1 1 0 1 1 0 1 0 1 1 0 1 0 0 0 1 0 1 1 1 0 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 1 1 1 1 0 1 1 0 1 0 1 1 1 1 1 0 0 0 0 0 0 1 0 0 0 0 1 1 1 0 0 1 0 0 0 1 0 1 1 0 0 1 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 0 0 0 1 0 0 1 1 0 0 0 1 0 1 0 0 1 1 1 1 0 1 0 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 1 1 1 1 0 0 0 0 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1 1 0 0 1 0 0 1 0 0 0 1 0 1 0 1 0 0 1 1 1 1 1 1 1 0 0 0 0 1 0 1 1 1 0 1 1 0 1 0 1 0 0 1 0 1 0 1 1 0 0 1 0 0 0 1 1 1 0 1 0 0 1 1 0 1 1 1 0 0 1 0 1 1 0 1 0 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 0 0 1 1 1 0 1 1 0 0 1 1 1 1 0 0 1 1 1 0 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 0 1 1 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 0 0 1 0 1 1 1 1 1 0 1 0 0 0 1 0 0 1 0 1 1 0 1 0 1 0 0 1 1 1 1 0 1 0 0 0 0 1 0 1 1 1 1 1 1 1 0 1 1 1 0 1 1 0 0 0 1 1 1 1 1 1 1 0 1 1 0 0 1 0 0 0 1 1 0 0 1 1 1 0 0 0 1 1 1 1 0 0 1 0 0 0 0 0 1 1 0 0 0 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 0 0 1 0 1 1 0 1 0 1 1 1 1 0 1 0 0 1 1 1 1 1 1 0 0 1 0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 1 1 1 0 1 1 1 0 1 1 0 1 1 1 0 1 1 1 0 1 0 1 1 1 0 1 1 0 0 1 1 1 1 1 1 1 0 1 1 1 1 1 1 0 1 0 0 0 0 1 0 1 0 1 1 1 0 0 1 0 1 1 0 1 0 0 1 1 0 1 0 1 1 0 1 0 0 1 1 1 0 0 1 0 0 0 1 1 0 0 0 0 1 0 0 1 1 1 1 0 1 0 0 0 1 1 0 0 0 0 1 0 1 1 1 0 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 1 1 0 1 0 0 1 0 0 0 1 0 1 1 0 0 0 1 0 0 0 1 0 0 1 1 1 1 1 1 1 0 1 1 1 0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 0 1 1 1 1 1 1 1 1 0 0 1 1 0 1 0 0 1 1 0 0 0 0 1 0 0 0 0 1 1 0 1 0 1 0 0 1 1 1 1 0 1 0 0 0 0 1 0 1 1 1 1 1 1 1 0 1 1 1 0 1 1 0 0 1 1 1 1 1 0 1 0 1 0 0 0 0 0 1 1 1 0 1 0 1 1 0 1 0 0 0 0 1 1 1 0 1 1 1 1 1 0 1 1 0 1 1 1 0 1 1 0 0 1 1 1 0 1 0 1 0 0 0 0 0 0 1 1 0 0 1 1 0 1 0 0 1 0 0 1 0 1 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 1 1 1 1 0 0 0 1 1 0 1 0 0 1 0 1 1 0 0 1 0 0 1 0 1 1 0 0 1 1 1 1 0 0 0 0 1 0 1 1 0 1 0 0 0 0 0 0 1 0 1 1 1 1 0 0 0 0 0 1 1 1 0 1 0 0 1 0 1 1 1 1 0 1 1 1 1 1 1 0 1 0 1 0 0 1 1 0 1 0 0 1 0 1 1 0 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 0 0 0 0 1 1 1 0 0 0 0 0 0 0 1 1 0 1 1 1 0 0 0 0 0 1 1 1 0 1 1 1 1 0 0 0 0 0 1 1 0 0 1 1 1 0 1 0 0 0 0 1 0 1 1 1 1 1 1 1 0 0 0 1 1 0 1 0 0 1 0 1 1 0 1 1 1 0 1 0 0 1 0 1 1 1 1 0 0 0 0 1 1 1 1 1 0 1 1 1 0 0 1 1 1 0 1 0 0 0 1 0 1 0 0 1 1 0 1 1 1 0 0 1 1 1 1 1 1 1 0 1 0 1 1 0 1 0 0 0 0 0 0 1 1 1 1 0 1 0 1 0 0 0 0 1 1 1 1 0 0 1 0 0 0 1 0 1 0 1 1 1 1 1 1 0 0 0 1 1 1 1 0 1 1 1 1 1 0 0 0 1 0 0 0 0 1 1 1 0 0 1 1 0 0 1 1 1 1 0 1 1 1 1 1 1 0 1 1 1 0 1 1 0 0 0 0 1 1 1 1 0 1 0 0 0 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 1 0 0 0 0 1 0 0 1 1 1 1 0 1 1 0 0 1 1 1 1 0 1 1 1 1 1 0 1 0 1 0 0 1 0 0 0 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0 1 0 1 1 0 1)
ビット列になっていますね。
出現頻度の高い e と出現頻度の低い z を比較して、
出現頻度に応じてビット列の長さが調節されていることを確認します。
(encode '(#\e) (@ tree))
出力:
(0 0 1)
(encode '(#\z) (@ tree))
出力:
(1 1 1 1 0 0 0 1 0 1)
たしかにシンボルの出現頻度に応じて長さが調節されています。
6. ビット列から元の情報を復号する関数を定義する
ビット列を元の記号列に戻す関数 decode を定義します。
まず、 decode-1 関数のガードに bit のリストであるという条件を設定するために
述語 bit-listp を定義します。
(defun bit-listp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (bitp (car x)) (bit-listp (cdr x)))))
Summary を確認する
Summary Form: ( DEFUN BIT-LISTP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) BIT-LISTP
一つの記号だけ復号する関数 decode-1 を定義します。
一つの記号を復号できるまでビット列を読んで、
記号と残りのビット列の二つを返す関数です。
(defun decode-1 (x tree) (declare (xargs :guard (and (bit-listp x) (huffman-treep tree)) :measure (node-count tree))) (cond ((and (consp x) (nodep tree)) (if (equal (car x) 0) (decode-1 (cdr x) (left tree)) (decode-1 (cdr x) (right tree)))) ((nodep tree) (mv nil nil)) (t (mv (leaf-symbol tree) x))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN DECODE-1 ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
(:DEFINITION BIT-LISTP)
(:DEFINITION BITP)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O-P)
(:DEFINITION O<)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:LINEAR NODE-COUNT-LEFT)
(:LINEAR NODE-COUNT-RIGHT)
(:TYPE-PRESCRIPTION NODE-COUNT)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 519
DECODE-1
decode-1 を使ってビット列を元の記号列に復号する関数 decode を定義します。
(defun decode (x tree) (declare (xargs :measure (len x) :guard (and (bit-listp x) (nodep tree) (huffman-treep tree)))) (if (or (endp x) (not (nodep tree))) nil (mv-let (symbol rest) (decode-1 x tree) (cons symbol (decode rest tree)))))
証明成功: Summary を確認する
Summary
Form: ( DEFUN DECODE ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
(:DEFINITION BIT-LISTP)
(:DEFINITION BITP)
(:DEFINITION DECODE-1)
(:DEFINITION ENDP)
(:DEFINITION EQ)
(:DEFINITION LEN)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O-P)
(:DEFINITION O<)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART BIT-LISTP)
(:EXECUTABLE-COUNTERPART BITP)
(:EXECUTABLE-COUNTERPART CONS)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BIT-LISTP)
(:INDUCTION DECODE-1)
(:INDUCTION LEN)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION BIT-LISTP)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION NODEP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION DECODE-1))
Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 5788
DECODE
decode を使って encode でビット列に変換した To be, or not to be
を元の文字列に戻してみましょう。
(coerce (decode (@ bits) (@ tree)) 'string)
出力を確認する
"To be, or not to be: that is the question: Whether 'tis nobler in the mind to suffer The slings and arrows of outrageous fortune, Or to take arms against a sea of troubles, And by opposing end them? To die: to sleep; No more; and by a sleep to say we end The heart-ache and the thousand natural shocks That flesh is heir to, 'tis a consummation Devoutly to be wish'd. To die, to sleep; To sleep: perchance to dream: ay, there's the rub; For in that sleep of death what dreams may come When we have shuffled off this mortal coil, Must give us pause: there's the respect That makes calamity of so long life; For who would bear the whips and scorns of time, The oppressor's wrong, the proud man's contumely, The pangs of despised love, the law's delay, The insolence of office and the spurns That patient merit of the unworthy takes, When he himself might his quietus make With a bare bodkin? who would fardels bear, To grunt and sweat under a weary life, But that the dread of something after death, The undiscover'd country from whose bourn No traveller returns, puzzles the will And makes us rather bear those ills we have Than fly to others that we know not of? Thus conscience does make cowards of us all; And thus the native hue of resolution Is sicklied o'er with the pale cast of thought, And enterprises of great pith and moment With this regard their currents turn awry, And lose the name of action.--Soft you now! The fair Ophelia! Nymph, in thy orisons Be all my sins remember'd!"
元の文字列に戻っています。
7. ハフマン符号化してから復号すると元に戻ることを証明する
下記を証明します。
(defthm decode-encode
(implies (and (true-listp x)
(huffman-treep tree)
(nodep tree)
(subsetp x (symbol-list tree)))
(equal (decode (encode x tree)
tree)
x)))
仮説に (subsetp x (symbol-list tree)) とあるのでこれだけ説明します。
(subsetp x y) は本来リスト x がリスト y の部分集合であることを意味する述語なのですが、
これは x の要素が全て y にも含まれていることを確認する関数です。
よって (subsetp x (symbol-list tree)) は、 x に含まれる全ての要素が、
(symbol-list tree) にも含まれているという意味です。
この decode-encode が真であると証明できれば、
適切なハフマン木を用意すればハフマン符号化をしてその結果を復号したら元の記号列に戻るということを証明できたといえます。
7.1. decode-encode の補助定理を証明する
7.1.1. (encode-1 x tree) はビット列である
(defthm bit-listp-encode-1 (bit-listp (encode-1 x tree)))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM BIT-LISTP-ENCODE-1 ...)
Rules: ((:DEFINITION BIT-LISTP)
(:DEFINITION ENCODE-1)
(:EXECUTABLE-COUNTERPART BIT-LISTP)
(:EXECUTABLE-COUNTERPART BITP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ENCODE-1)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION BIT-LISTP)
(:TYPE-PRESCRIPTION ENCODE-1)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 443
BIT-LISTP-ENCODE-1
7.1.2. (encode x tree) はビット列である
(defthm bit-listp-encode (bit-listp (encode x tree)))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM BIT-LISTP-ENCODE ...)
Rules: ((:COMPOUND-RECOGNIZER BITP-COMPOUND-RECOGNIZER)
(:DEFINITION ATOM)
(:DEFINITION BINARY-APPEND)
(:DEFINITION BIT-LISTP)
(:DEFINITION BITP)
(:DEFINITION ENCODE)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART BIT-LISTP)
(:EXECUTABLE-COUNTERPART BITP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION BIT-LISTP)
(:INDUCTION ENCODE)
(:INDUCTION TRUE-LISTP)
(:REWRITE APPEND-TO-NIL)
(:REWRITE BIT-LISTP-ENCODE-1)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION BIT-LISTP)
(:TYPE-PRESCRIPTION ENCODE)
(:TYPE-PRESCRIPTION ENCODE-1)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION BITP))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 6615
BIT-LISTP-ENCODE
7.1.3. (consp (append x y)) は x か y が consp という意味である
(defthm consp-append
(equal (consp (append x y))
(or (consp x)
(consp y))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM CONSP-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 300
CONSP-APPEND
7.1.4. encode-1 で符号化したら必ず要素が一つ以上のリストが返る
ただし、 tree が nodep である場合に限る。
(defthm consp-encode-1
(implies (and (huffman-treep tree)
(nodep tree))
(consp (encode-1 x tree))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM CONSP-ENCODE-1 ...)
Rules: ((:DEFINITION ENCODE-1)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ENCODE-1)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREEP-LEFT)
(:REWRITE SYMBOL-LIST-LEAF-SYMBOL)
(:TYPE-PRESCRIPTION ENCODE-1)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 721
CONSP-ENCODE-1
7.1.5. encode で符号化したら必ず要素が一つ以上のリストが返る
ただし x は要素が一つ以上のリストであるとし、
tree は nodep とする。
(defthm consp-encode
(implies (and (consp x)
(true-listp x)
(huffman-treep tree)
(nodep tree))
(consp (encode x tree))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM CONSP-ENCODE ...)
Rules: ((:DEFINITION ENCODE)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ENCODE)
(:INDUCTION TRUE-LISTP)
(:REWRITE CONSP-APPEND)
(:REWRITE CONSP-ENCODE-1)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION ENCODE)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION NODEP)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 702
CONSP-ENCODE
7.1.6. decode-1 が返す残りのリストは元のリストより短い
(defthm len-decode-1
(implies (and (consp x)
(nodep tree))
(< (len (mv-nth 1 (decode-1 x tree)))
(len x))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM LEN-DECODE-1 ...)
Rules: ((:DEFINITION DECODE-1)
(:DEFINITION LEN)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION DECODE-1)
(:INDUCTION LEN)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION NODEP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION DECODE-1))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 2317
LEN-DECODE-1
7.1.7. (member e (append x y)) の真偽は (or (member e x) (member e y)) と一致する
(defthm member-append
(iff (member-equal e (append x y))
(or (member-equal e x)
(member-equal e y))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM MEMBER-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION IFF)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION BINARY-APPEND)
(:INDUCTION MEMBER-EQUAL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MEMBER-EQUAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 1331
MEMBER-APPEND
7.1.8. (decode-1 (encode-1 x tree) tree) は x になる
(defthm decode-1-encode-1
(implies (and (huffman-treep tree)
(member-equal x (symbol-list tree)))
(and (equal (mv-nth 0 (decode-1 (encode-1 x tree) tree))
x)
(equal (mv-nth 1 (decode-1 (encode-1 x tree) tree))
nil))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM DECODE-1-ENCODE-1 ...)
Rules: ((:DEFINITION DECODE-1)
(:DEFINITION ENCODE-1)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONS)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART MV-NTH)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION DECODE-1)
(:INDUCTION ENCODE-1)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE HUFFMAN-TREEP-LEFT)
(:REWRITE HUFFMAN-TREEP-RIGHT)
(:REWRITE MEMBER-APPEND)
(:REWRITE SYMBOL-LIST-LEAF-SYMBOL)
(:REWRITE SYMBOL-LIST-LEFT-RIGHT)
(:TYPE-PRESCRIPTION DECODE-1)
(:TYPE-PRESCRIPTION ENCODE-1)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NODEP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION ENCODE-1))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 3970
DECODE-1-ENCODE-1
7.1.9. (decode-1 (append (encode-1 x tree) y)) から append を除去する
(defthm decode1-append-encode-1
(implies (and (huffman-treep tree)
(member-equal x (symbol-list tree)))
(and (equal (mv-nth 0 (decode-1 (append (encode-1 x tree)
y)
tree))
x)
(equal (mv-nth 1 (decode-1 (append (encode-1 x tree)
y)
tree))
y))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM DECODE1-APPEND-ENCODE-1 ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION DECODE-1)
(:DEFINITION ENCODE-1)
(:DEFINITION MEMBER-EQUAL)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION DECODE-1)
(:INDUCTION ENCODE-1)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONSP-APPEND)
(:REWRITE HUFFMAN-TREEP-LEFT)
(:REWRITE HUFFMAN-TREEP-RIGHT)
(:REWRITE MEMBER-APPEND)
(:REWRITE SYMBOL-LIST-LEAF-SYMBOL)
(:REWRITE SYMBOL-LIST-LEFT-RIGHT)
(:TYPE-PRESCRIPTION DECODE-1)
(:TYPE-PRESCRIPTION ENCODE-1)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NODEP))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION ENCODE-1))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 6152
DECODE1-APPEND-ENCODE-1
7.1.10. decode-encode を decode1-encode1 で簡約できる形に変換する
(defthm decode-encode-to-decode1-encode1
(implies (and (huffman-treep tree)
(nodep tree)
(member-equal x (symbol-list tree))
(subsetp y (symbol-list tree)))
(equal (decode (append (encode-1 x tree)
(encode y tree))
tree)
(cons (mv-nth 0 (decode-1 (encode-1 x tree) tree))
(decode (encode y tree)
tree))))
:hints (("Goal" :induct (decode x tree))))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM DECODE-ENCODE-TO-DECODE1-ENCODE1 ...)
Rules: ((:DEFINITION DECODE)
(:DEFINITION ENDP)
(:DEFINITION MV-NTH)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION DECODE)
(:REWRITE CONSP-APPEND)
(:REWRITE CONSP-ENCODE-1)
(:REWRITE DECODE-1-ENCODE-1)
(:REWRITE DECODE1-APPEND-ENCODE-1)
(:REWRITE MEMBER-APPEND)
(:REWRITE SYMBOL-LIST-LEFT-RIGHT)
(:TYPE-PRESCRIPTION DECODE-1)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NODEP))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 9239
DECODE-ENCODE-TO-DECODE1-ENCODE1
7.2. decode-encode を証明する
これで decode-encode を decode1-encode1 が使える形に変換できるようになったため、
decode-encode を証明することができます。
追記: よく Summary を見たら encode1-decode1 や
decode-encode-to-decode1-encode1 は使われていなくて、
decode-encode-to-decode1-encode1 の補助定理である decode1-append-encode-1 で証明されていました。
(defthm decode-encode
(implies (and (true-listp x)
(huffman-treep tree)
(nodep tree)
(subsetp x (symbol-list tree)))
(equal (decode (encode x tree)
tree)
x)))
証明成功: Summary を確認する
Summary
Form: ( DEFTHM DECODE-ENCODE ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION DECODE)
(:DEFINITION DECODE-1)
(:DEFINITION ENCODE)
(:DEFINITION ENCODE-1)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION SUBSETP-EQUAL)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ENCODE)
(:INDUCTION SUBSETP-EQUAL)
(:INDUCTION TRUE-LISTP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-CAR-CDR)
(:REWRITE DECODE1-APPEND-ENCODE-1)
(:REWRITE HUFFMAN-TREEP-LEFT)
(:REWRITE HUFFMAN-TREEP-RIGHT)
(:REWRITE MEMBER-APPEND)
(:REWRITE SYMBOL-LIST-LEFT-RIGHT)
(:TYPE-PRESCRIPTION ENCODE)
(:TYPE-PRESCRIPTION ENCODE-1)
(:TYPE-PRESCRIPTION HUFFMAN-TREEP)
(:TYPE-PRESCRIPTION MEMBER-EQUAL)
(:TYPE-PRESCRIPTION NODEP)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION ENCODE-1)
(:DEFINITION SUBSETP-EQUAL)
(:REWRITE MEMBER-APPEND))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 8150
DECODE-ENCODE
8. おわりに
ハフマン符号化をしてから復号すると元に戻ることを証明できました。 この問題の発展として、ハフマン木の生成が正しくできているかや、 ハフマン符号化によって情報をどれくらい圧縮できるかなどについても ACL2 に検証させてもよいかもしれません。
ハフマン木の符号化と復号が正常にできることを証明できるのであれば、 他にも色々な性質を証明できそうだとワクワクする例になっているかと思います。 これからも ACL2 の用途を色々考えて試してみようと思います。
面白そうだなと思ったら、 是非 ACL2 の環境を手元に構築して試してみてください。