0

我正在尝试在 ACL2 中以一元符号 ( O, (S O), (S (S O)), ...) 对自然数进行建模，并证明加法的交换性。这是我的尝试：

; a NATURAL is 'O or a list ('S n') where n' is a NATURAL
(defun naturalp (n)
  (cond ((equal n 'O) t)
        (t (and (true-listp n)
                (equal (length n) 2)
                (equal (first n) 'S)
                (naturalp (second n))))))

(defun pred (n)
  (cond ((equal n 'O) 'O)
        ((naturalp n) (second n))))

(defun succ (n)
  (list 'S n))

(defun plus (n m)
  (cond ((equal n 'O) m)
        ((naturalp n) (succ (plus (pred n) m)))))

; FIXME: cannot prove this because rewriting loops...
(defthm plus_comm                                 
  (implies (and (naturalp n) (naturalp m))
           (iff (equal (plus n m) (plus m n)) t)))

这可能不是最 LISPy 的方式，我习惯于使用模式匹配的语言。

我的问题正如评论所建议的那样：证明者循环，试图证明同一事物的越来越深的嵌套版本。我该如何阻止这个？该手册确实简要提到了循环重写规则，但没有说明如何处理它们。

我的期望是这个证明会失败，给我提示需要哪些辅助引理来完成它。我可以使用循环证明的输出来找出可能停止循环的引理吗？

4

1 回答 1

2

ACL2 最终可能会进入不同类型的循环。一种常见的类型是重写器循环，通常非常明显。例如，以下内容：

(defun f (x) x)
(defun g (x) x)
(defthm f-is-g (implies (consp x) (equal (f x) (g x))))
(defthm g-is-f (implies (consp x) (equal (g x) (f x))))
(in-theory (disable f g))
(defthm loop (equal (f (cons a b)) (cons a b)))

引发重写循环，并提供信息丰富的调试消息：

HARD ACL2 ERROR in REWRITE:  The call depth limit of 1000 has been
exceeded in the ACL2 rewriter.  To see why the limit was exceeded,
first execute
  :brr t
and then try the proof again, and then execute the form (cw-gstack)
or, for less verbose output, instead try (cw-gstack :frames 30).  You
will then probably notice a loop caused by some set of enabled rules,
some of which you can then disable; see :DOC disable.  Also see :DOC
rewrite-stack-limit.

不幸的是，您的示例正在进入另一种循环。特别是，看起来 ACL2 正在进入一个循环，其中

  • 它引入，但随后达到了无法通过重写来证明的子目标，所以
  • 它引入，但随后达到了无法通过重写来证明的子目标，所以
  • ...

很难看出这就是正在发生的事情。我所做的只是(set-gag-mode nil)在提交定理之前运行，然后检查中断证明者后打印的输出。

避免这种情况的一种方法是给出提示，特别是您可以告诉 ACL2 不要像这样进行感应：

(defthm plus_comm
  (implies (and (naturalp n) (naturalp m))
           (iff (equal (plus n m) (plus m n)) t))
  :hints(("Goal" :do-not-induct t)))

但如果你这样做，它就会立即卡住，因为你可能真的想通过归纳来证明这个定理。所以你真正想告诉它的是：“感应一次，但不要感应更多。” 语法有点傻：

(defthm plus_comm
  (implies (and (naturalp n) (naturalp m))
           (iff (equal (plus n m) (plus m n)) t))
  :hints(("Goal"
          :induct t          ;; Induct once.
          :do-not-induct t   ;; But don't induct more than once.
      )))

这应该会给您留下一个合理的检查点，然后您可以尝试通过添加重写规则或提供进一步的提示来进行调试。

祝你好运！

于 2016-02-05T22:13:49.187 回答