diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2022-08-17 15:41:36 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-08-17 15:41:36 +0900 |
commit | c46988581916a3324b72933b7df2d41b5cfb4b0f (patch) | |
tree | 968239d4428c8db2944f7723264d7aa716d9dea5 | |
parent | 7e66be39b29b1e80ccb56dc0b6a429355f02d95d (diff) |
factorial: 階乗を求めるプログラムを追加
-rw-r--r-- | factorial.lisp | 38 |
1 files changed, 38 insertions, 0 deletions
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))) + + |