Как зацикливаться на использовании рекурсии в ACL2?

Question

Мне нужно сделать что -то подобное, но в ACL2:

for (i=1; i<10; i++) {
    print i;
}

Он использует Common LISP, но я не имею никакого представления, как выполнить эту задачу ...

Мы не можем использовать стандартные общие конструкции LISP, такие как Loop, Do. Просто рекурсия.

У меня есть несколько ссылок, но мне очень трудно понять:

• Нежное вступление в программирование ACL2

Answer 1

Раздел «Посещение всех натуральных чисел от N до 0» в Нежное введение в программирование ACL2 объясняет, как это сделать.

В вашем случае вы хотите посетить цифры в порядке возрастания, поэтому ваш код должен выглядеть примерно так:

(defun visit (n max ...)
  (cond ((> n max) ...)             ; N exceeds MAX: nothing to do.
        (t .                        ; N less than or equal to MAX:
            . n                     ; do something with N, and
             .
              (visit (+ n 1) max ...) ; visit the numbers above it.
             .
            .
           .)))

Answer 2

Решение, которое использует рекурсию:

> (defun for-loop (from to fn)
    (if (<= from to)
       (progn
         (funcall fn from)
         (for-loop (+ from 1) to fn))))

;; Test
> (for-loop 1 10 #'(lambda (i) (format t "~a~%" i)))
1
2
3
4
5
6
7
8
9
10
NIL

Answer 3

(Defun foo-loop (n) (cond (zp n) "dode") (t (prog2 $ (cw "~ x0" n) (foo-loop (1-n))))))))))))))))))))))))))))))))))))))))))))))))))))))

(Foo-Loop 10)

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