Как исправить петлю в перезаписи доказательства

Question

Я пытаюсь моделировать натуральные числа в унарной записи (O, (S O), (S (S O)),...) в ACL2 и докажем коммутативность сложения. Вот моя попытка:

; 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 способ сделать это, я привык к языкам с сопоставлением с образцом.

Моя проблема состоит в том, что было предложено в комментарии: проверяющий зацикливается, пытаясь доказать все более и более глубоко вложенные версии одной и той же вещи. Как мне это остановить? В руководстве кратко упоминаются правила циклического переписывания, но ничего не говорится о том, что с ними делать.

Я ожидал, что это доказательство потерпит неудачу, дав мне подсказки о том, какие вспомогательные леммы необходимы для его завершения. Могу ли я использовать выходные данные из доказательства зацикливания, чтобы выяснить лемму, которая может остановить зацикливание?

Answer 1

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.
      )))

Это должно дать вам разумную контрольную точку, которую вы можете затем попытаться отладить, добавив правила перезаписи или дав дополнительные подсказки.

Удачи!