たらいまわし関数の停止性証明 by ACL2

まずmeasureを定義。関数定義はlispと同様でdefun。アイデアとしては、まずa<=bとなるような組が最初、次に(a>b and b<=c)となるようなやつが、その次にそれ以外が来るように。二番目と三番目のクラスはa-bでさらに順序付けられています。

ACL2 !>(defun m (a b c)
  (if (and (integerp a)
	   (integerp b)
	   (integerp c))
      (if (<= a b)
	  0
	(if (<= b c)
	    (cons (cons 1 1) (- a b))
	  (cons (cons 1 2) (- a b))))
    0))

こんなのが返ってきて定義されたことを伝えてくれます。

Since M is non-recursive, its admission is trivial.  We observe that
the type of M is described by the theorem 
(OR (EQUAL (M A B C) 0)
    (AND (CONSP (M A B C))
         (NOT (TRUE-LISTP (M A B C))))).
We used primitive type reasoning.

Summary
Form:  ( DEFUN M ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  2.50 seconds (prove: 0.00, print: 0.24, other: 2.26)
 M

たらいまわし関数を定義。再帰を一回手動展開しています。このおかげで三番目の引数をあんまり気にしなくて良くなるので楽です。変なことが起こった場合にはnilを返すようにしています。例えばmeasureがちゃんと動いていないとか。ACL2は停止が確認されなければ関数が定義されないので、未定義を付け加えちゃうわけですな。そうすると、関数はとりあえず定義できた上で、全ての入力に関して整数が返ってくるならば停止性が証明されたことになります。declareとかxargsとかはよくわかりませんが、とりあえずこう書くとmeasureとして(m a b c)を使ってくれます。
最初はACL2からの出力もこぴぺしてたんですが、長すぎるので割愛。

(defun tak (a b c)
  (declare (xargs :measure (m a b c)))
  (if (and (integerp a)
	   (integerp b)
	   (integerp c))
      (if (<= a b)
	  b
	(let ((a1 (tak (1- a) b c))
	      (b1 (tak (1- b) c a)))
	  (if (<= a1 b1)
	      b1
	    (if (o< (m (1- c) a b) (m a b c))
		(let ((c1 (tak (1- c) a b)))
		  (if (o< (m a1 b1 c1) (m a b c))
		      (tak a1 b1 c1)
		    nil))
	      nil))))
    nil))

defthmと書いてから証明したいことを書くと、それを証明しようと頑張ってくれます。長々と途中経過も説明しつつ。証明できればそれが定理として保存されて、そうでない場合には文句を言われます。a<=bの場合はいくらなんでも明らか。

ACL2 !>(defthm lemma1
  (implies (and (integerp a)
		(integerp b)
		(integerp c)
		(<= a b))
	   (equal (tak a b c)
		  b)))


But simplification reduces this to T, using the :definition TAK and
primitive type reasoning.

Q.E.D.

Summary
Form:  ( DEFTHM LEMMA1 ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION TAK)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.15 seconds (prove: 0.02, print: 0.01, other: 0.12)
 LEMMA1

ずいぶん苦労しますが、a>bかつb<=cの場合もなんとか自動的に証明してもらえます。この後は長すぎるので命令とsummaryのみこぴぺします。

(defthm lemma2
    (implies (and (integerp a)
		(integerp b)
		(integerp c)
		(> a b)
		(<= b c))
	     (equal (tak a b c) c)))

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION M)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-FIRST-COEFF)
        (:DEFINITION O-FIRST-EXPT)
        (:DEFINITION O-RST)
        (:DEFINITION O<)
        (:DEFINITION TAK)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART O-FINP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION TAK)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DEFAULT-<-1)
        (:REWRITE DEFAULT-<-2)
        (:REWRITE LEMMA1)
        (:TYPE-PRESCRIPTION TAK))
Warnings:  None
Time:  45.86 seconds (prove: 27.92, print: 17.94, other: 0.00)
 LEMMA2

所要時間45.86秒ですか。お疲れ様。あ、私の環境は貧弱なのでほとんどのところではもっとすばやく終わるでしょう。

問題はa>b>cのとき。この場合には、bとcを固定してaに関する帰納法でやっつけるんですが、それを理解してもらうのが一苦労。ちょっと複雑な帰納法をやるには、それと同じ参照構造を持っている帰納的に定義された関数を定義して、それをhintとして渡します。渡し方の文法は適当にサンプルからこぴぺ。

このケースでは自動証明が十分賢くなくて、b-1==cの場合とb-1>cの場合に分けないとやってくれません。というわけで、b-1==cのときは(a-1, b, c)を参照、b-1>cのときは(a, b, b-1)を参照しておきます。

(defun m_scheme (a b c)
  (if (and (integerp a)
	   (integerp b)
	   (integerp c))
      (if (> a b)
	  (if (equal (1- b) c)
	      (- a b)
	    (cons (cons 1 1) (- a b)))
	0)
    0))

(defun scheme (a b c)
  (declare (xargs :measure (m_scheme a b c)))
  (if (and (integerp a)
	   (integerp b)
	   (integerp c))
      (if (> a b)
	  (if (equal (1- b) c)
	      (scheme (1- a) b c)
	    (scheme a b (1- b)))
	t)
    t))

まずb-1==cのとき。この場合には、tak(a, b, c)=tak(tak(a-1, b, c), tak(b-1, c, a), tak(c-1, a, b))=tak(tak(a-1, b, c), tak(c, c, a), tak(c-1, a, b))=tak(tak(a-1, b, c), c, a)になるんで帰納法+既に片付けたケースで大丈夫。

(defthm lemma3
  (implies (and (integerp a)
		(integerp b)
		(integerp c)
		(>= a b)
		(> b c)
		(equal (1- b) c))
	   (equal (tak a b c)
		  a))
  :hints (("Goal"
	   :induct (scheme a b c))))

Summary
Form:  ( DEFTHM LEMMA3 ...)
Rules: ((:DEFINITION M)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-FIRST-COEFF)
        (:DEFINITION O-FIRST-EXPT)
        (:DEFINITION O<)
        (:DEFINITION TAK)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SCHEME)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE CAR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE LEMMA1)
        (:REWRITE LEMMA2))
Warnings:  None
Time:  0.16 seconds (prove: 0.04, print: 0.07, other: 0.05)
 LEMMA3

続いてb-1>cのとき。この場合は、tak(a, b, c)=tak(tak(a-1, b, c), tak(b-1, c, a), tak(c-1, a, b))=tak(tak(a-1, b, c), a, a)となって、やっぱり帰納法と既に片付けたケースで回せます。

(defthm lemma4
  (implies (and (integerp a)
		(integerp b)
		(integerp c)
		(>= a b)
		(> b c)
		(not (equal (1- b) c)))
	   (equal (tak a b c)
		  a))
  :hints (("Goal"
	   :induct (scheme a b c))))

Summary
Form:  ( DEFTHM LEMMA4 ...)
Rules: ((:DEFINITION M)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-FIRST-COEFF)
        (:DEFINITION O-FIRST-EXPT)
        (:DEFINITION O-RST)
        (:DEFINITION O<)
        (:DEFINITION TAK)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART O-FINP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SCHEME)
        (:INDUCTION TAK)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DEFAULT-<-1)
        (:REWRITE INVERSE-OF-+)
        (:REWRITE LEMMA1)
        (:REWRITE LEMMA2)
        (:REWRITE LEMMA3)
        (:TYPE-PRESCRIPTION TAK))
Warnings:  None
Time:  15.81 seconds (prove: 6.82, print: 8.98, other: 0.01)
 LEMMA4

というわけで、a>b>cのときはいずれにしても問題なし。なんでか知りませんが、ここでもヒントをあげないとぽしゃります。

(defthm lemma5
  (implies (and (integerp a)
		(integerp b)
		(integerp c)
		(>= a b)
		(> b c))
	   (equal (tak a b c)
		  a))
  :hints (("Goal"
	   :induct (scheme a b c))))

Summary
Form:  ( DEFTHM LEMMA5 ...)
Rules: ((:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SCHEME)
        (:REWRITE LEMMA1)
        (:REWRITE LEMMA3)
        (:REWRITE LEMMA4))
Warnings:  Subsume
Time:  0.06 seconds (prove: 0.02, print: 0.04, other: 0.00)
 LEMMA5

ここまで教え込んでやれば、ちゃんと停止性を証明してくれます。

ACL2 !>(defthm mainthm
  (implies (and (integerp a)
		(integerp b)
		(integerp c))
	   (integerp (tak a b c))))

Summary
Form:  ( DEFTHM MAINTHM ...)
Rules: ((:DEFINITION M)
        (:DEFINITION NOT)
        (:DEFINITION TAK)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION TAK)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE LEMMA1)
        (:REWRITE LEMMA2)
        (:REWRITE LEMMA5)
        (:TYPE-PRESCRIPTION TAK))
Warnings:  None
Time:  0.37 seconds (prove: 0.22, print: 0.14, other: 0.01)
 MAINTHM

なんか、ここまでお膳立てしたのにずいぶん長い出力があるんですが、いったい何をやっているんでしょうか？

できたにはできたけれども、どうにもschemeがきもいです。なんでdefunみたいにmeasureでやらせてもらえないんでしょうか？帰納法で使う組が指定されていると楽だなというのはわかるにしても。