Я пытаюсь доказать эту функцию в ACL2s/Lisp, но она возвращает ошибку переполнения стека, хотя я не вижу недостатка в коде.Какие входные данные могут привести к тому, что эта функция не завершится?
(defunc foo (x y)
:input-contract (and (natp x) (natp y))
:output-contract (natp (foo x y))
(cond ((equal 0 x) (+ y 1))
((equal 0 y) (foo (- x 1) 1))
(t (foo (- x 1) (foo x (+ y 1))))))
не любое положительное x и y причиной этого переполнения? Давайте посмотрим на (foo 1 1).
Ни x, ни y равен нулю, поэтому он попадает в t ветви конд, и называет:
(foo 0
(foo 1 2))
Хорошо, давайте оценивать внутренний foo вызов:
(foo 1 2)
Точно так же, он попадает в ветвь t, и звонки:
(foo 0
(foo 1 3))
Оценим внутреннюю foo:
(foo 1 3)
Вы можете увидеть, где это происходит. Пояснения к t:
(foo 0
(foo 1 4))
И так далее. Это произойдет в любое время, когда оба x и y отличны от нуля. Откуда у вас этот код? Что вы пытаетесь с этим сделать? Запуск - это также хорошая идея, чтобы увидеть, что происходит. В этом случае вы получите переполнение стека почти с каждым возможным вызовом.
Какие значения вы используете для переполнения стека? – DavidC
Я не. ACL2s имеет автоматический теоретический прорыв, который пропускает входы в него, но я не вижу, что это такое, но один из них вызывает переполнение стека, поэтому он отвергает эту функцию. – b33k3rz