From c46988581916a3324b72933b7df2d41b5cfb4b0f Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Wed, 17 Aug 2022 15:41:36 +0900 Subject: factorial: 階乗を求めるプログラムを追加 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- factorial.lisp | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 factorial.lisp diff --git a/factorial.lisp b/factorial.lisp new file mode 100644 index 0000000..d51157a --- /dev/null +++ b/factorial.lisp @@ -0,0 +1,38 @@ +;; factorial.lisp -- 階乗を求める + +(in-package "ACL2") + +(defun factorial (n) + (if (zp n) + 1 + (* n (factorial (- n 1))))) + +;; factorial は常に正の整数 +(defthm posp-factorial + (posp (factorial n))) + + +;; 末尾再帰版の階乗関数 +(defun factorial-tail (n a) + (if (zp n) + a + (factorial-tail (- n 1) + (* n a)))) + +;; 積の交換の定理が必要なので +;; arithmetic books を使う +(local (include-book "arithmetic/top-with-meta" :dir :system)) + +;; 末尾再帰版と通常版の値は一致する +;; ただし、a は1以外の値も取れるとする +(defthm factorial-tail-factorial-generic + (implies (integerp a) + (equal (factorial-tail n a) + (* a (factorial n))))) + +;; 末尾再帰版と通常版の値は一致する +(defthm factorial-tail-factorial + (equal (factorial-tail n 1) + (factorial n))) + + -- cgit v1.2.3