ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた
目次
1. 注意
この記事はいま思うとあまりよく分かっていなかったときに書いたものなので参考にしない方がいいです。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張る予定です。
2. はじめに
ACL2 でリストから k 個取り出す全ての組み合わせを求める関数
combinations と、組み合わせの数を求める関数 comb
を定義し、 (equal (len (combinations x n)) (comb (len x) n))
を証明します。
プログラムのライセンスは3条項BSDライセンスとします。
3. きっかけ
acl2-kernel
を使ってブログ記事を書いてみたいというのが本記事の主な動機です。今回良い感じに書けたら、今後も
ACL2 でなんかやってみた記事を acl2-kernel
を使って書いてみようと思います。
4. combinations 関数を定義する
リストから k 個の要素を取り出す全ての組み合せを求める関数 combinations
関数を定義します。
4.1. 補助関数 cons-all を定義する
combinations を作成するためには全てのリストの先頭に要素を一つ追加する
cons-all 関数が必要です。 cons-all の停止性は ACL2
が自動証明してくれました。 cons-all
の第二引数は真リストしか渡らないようにガードを設定していますが、ガードの証明も問題なく自動証明されました。
(defun cons-all (e x)
(declare (xargs :guard (true-listp x)))
(if (endp x)
nil
(cons (cons e (car x))
(cons-all e (cdr x)))))
Summary Form: ( RESET-PREHISTORY NIL ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) :NEW-PREHISTORY-SET The admission of CONS-ALL is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of CONS-ALL is described by the theorem (TRUE-LISTP (CONS-ALL E X)). We used primitive type reasoning. Computing the guard conjecture for CONS-ALL.... The guard conjecture for CONS-ALL is trivial to prove, given primitive type reasoning. CONS-ALL is compliant with Common Lisp. Summary Form: ( DEFUN CONS-ALL ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) CONS-ALL
4.2. combinations 関数
リスト x から k 個を取り出す全ての組み合せのリストを求める関数
combinations を定義します。
再帰によって combinations 関数を定義します。 combinations
関数を作成するにはリストの先頭の要素を含む場合と含まない場合に分けて分離して考えてそれらを連結するのがよいです。
4.2.1. リストの先頭の要素を含む組み合せを求める
リストの先頭の要素を含む場合は、まずリストの先頭の要素を含まない全ての組み合せを
combinations 関数により求めます。その後に cons-all
関数を用いて全ての組み合せのそれぞれに先頭の要素を追加します。
(cons-all (car x)
(combinations (cdr x) (- n 1)))
4.2.2. リストの先頭の要素を含まない組み合せを求める
リストの先頭の要素を含まない場合は簡単で、下記のように combinations
関数を使ってリストの先頭の要素を含めない場合を求めるだけです。
(combinations (cdr x) n)
4.2.3. combinations 関数の基底部を考える
基底部として考えられるケースには与えられた自然数が 0
の場合と与えられたリストが空の場合があります。 リストから 0
個取り出す組み合せはただ一つ存在し、空リストです。よってリストから0個取り出す場合の全ての組み合せは
(list nil) です。
空のリストからは 1
以上取り出す組み合せを求めることは不可能です(空リストから 0
個を取り出す組み合せを求めることは可能で結果は上述した通りです)。不可能なわけですから、空リストから
1 以上取り出す場合の全ての組み合せは nil です。
4.2.4. combinations 関数
上記をまとめると、=combinations= 関数は下記のように実装できます。 停止性とガードは補助定理なしで ACL2 が自動証明してくれました。
(defun combinations (x n)
(declare (xargs :guard (and (true-listp x)
(natp n))))
(cond
((zp n) (list nil))
((endp x) nil)
(t
(append (cons-all (car x)
(combinations (cdr x) (- n 1)))
(combinations (cdr x) n)))))
The admission of COMBINATIONS is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X). We observe that the type of COMBINATIONS is
described by the theorem (TRUE-LISTP (COMBINATIONS X N)). We used
the :type-prescription rules BINARY-APPEND and TRUE-LISTP-APPEND.
Computing the guard conjecture for COMBINATIONS....
The guard conjecture for COMBINATIONS is trivial to prove, given the
:compound-recognizer rules NATP-COMPOUND-RECOGNIZER and
ZP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription
rules COMBINATIONS and CONS-ALL. COMBINATIONS is compliant with Common
Lisp.
Summary
Form: ( DEFUN COMBINATIONS ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
(:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION COMBINATIONS)
(:TYPE-PRESCRIPTION CONS-ALL)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
COMBINATIONS
5. comb 関数を定義する
n 個から k 個を取り出す組み合せの数を求める関数を定義します。
combinations の定義を参照しながら対応するように記述しましょう。
- 0 個を取り出す組み合せは空リストただ一つなので、組み合せの数は 1
- 長さ 0 のリストから 1 個以上取り出すことはできないため、組み合せの数は 0
- 先頭要素を含む組み合せの数は
(comb (- n 1) (- k 1))- cons-all 関数は与えられたリストの長さを変えないことに注意
- 先頭要素を含まない組み合せの数は
(comb (- n 1) k)
(defun comb (n k)
(cond
((zp k) 1)
((zp n) 0)
(t (+ (comb (- n 1) (- k 1))
(comb (- n 1) k)))))
The admission of COMB is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). We observe that the type of COMB is described by the theorem (AND (INTEGERP (COMB N K)) (<= 0 (COMB N K))). We used primitive type reasoning. Summary Form: ( DEFUN COMB ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) COMB
6. len-combinations 定理
(len (combinations x k)) が (comb (len x) k)
と一致することを証明します。 これは ACL2
が補助定理を必要とせずに自動証明してくれました。
(defthm len-combinations
(equal (len (combinations x k))
(comb (len x) k)))
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (COMBINATIONS X K).
This suggestion was produced using the :induction rules COMBINATIONS
and LEN. If we let (:P K X) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ZP K))
(NOT (ENDP X))
(:P (+ -1 K) (CDR X))
(:P K (CDR X)))
(:P K X))
(IMPLIES (AND (NOT (ZP K)) (ENDP X))
(:P K X))
(IMPLIES (ZP K) (:P K X))).
This induction is justified by the same argument used to admit COMBINATIONS.
Note, however, that the unmeasured variable K is being instantiated.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'
Subgoal *1/3'5'
Subgoal *1/3'6'
Subgoal *1/3'7'
Subgoal *1/3'8'
Subgoal *1/3'9'
Subgoal *1/3'10'
([ A key checkpoint while proving *1 (descended from Goal):
Subgoal *1/3''
(IMPLIES (AND (NOT (ZP K))
(CONSP X)
(EQUAL (LEN (COMBINATIONS (CDR X) (+ -1 K)))
(COMB (LEN (CDR X)) (+ -1 K)))
(EQUAL (LEN (COMBINATIONS (CDR X) K))
(COMB (LEN (CDR X)) K)))
(EQUAL (LEN (APPEND (CONS-ALL (CAR X)
(COMBINATIONS (CDR X) (+ -1 K)))
(COMBINATIONS (CDR X) K)))
(+ (COMB (LEN (CDR X)) K)
(COMB (LEN (CDR X)) (+ -1 K)))))
*1.1 (Subgoal *1/3'10') is pushed for proof by induction.
])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
So we now return to *1.1, which is
(IMPLIES (AND (TRUE-LISTP CS0) (TRUE-LISTP CS))
(EQUAL (LEN (APPEND (CONS-ALL X1 CS0) CS))
(+ (LEN CS) (LEN CS0)))).
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/1
Subgoal *1.1/1'
*1.1 and *1 are COMPLETED!
Thus key checkpoints Subgoal *1/3'' and Goal are COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM LEN-COMBINATIONS ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:DEFINITION BINARY-APPEND)
(:DEFINITION COMB)
(:DEFINITION COMBINATIONS)
(:DEFINITION CONS-ALL)
(:DEFINITION ENDP)
(:DEFINITION FIX)
(:DEFINITION LEN)
(:DEFINITION NOT)
(:DEFINITION SYNP)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEN)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COMBINATIONS)
(:INDUCTION CONS-ALL)
(:INDUCTION LEN)
(: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 COMBINATIONS)
(:TYPE-PRESCRIPTION CONS-ALL)
(:TYPE-PRESCRIPTION LEN)
(:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 5105
LEN-COMBINATIONS
7. おわりに
無事に組み合せを求める関数と組み合せの数を求める関数の関係が意図した通りであることを証明できました。 今回は二つの関数の定義がほとんど同じであったため補助定理を考える必要もなく証明できたのですが、通常はもう少し難しいことが多いです。
comb
の定義の方法は他にもあるため、他の定義による組み合せの数と一致するかについての証明を試みても良いかもしれません。