Come ciclo utilizzando la ricorsione in ACL2?

Question

ho bisogno di fare qualcosa di simile, ma in ACL2:

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

Si utilizza Common Lisp, ma non hanno alcuna idea di come fare questa operazione ...

Non possiamo utilizzare costruzioni standard Common Lisp, come LOOP, DO. Basta ricorsione.

Ho alcuni link, ma lo trovo molto difficile da capire:

• Gentle Introduzione alla programmazione ACL2

Answer 1

La sezione "Visitare tutti i numeri naturali da N a 0" in a Gentle Introduction to ACL2 programmazione spiega come farlo.

Nel tuo caso si desidera i numeri visita in ordine crescente, in modo che il codice dovrebbe essere qualcosa di simile:

(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

Una soluzione che utilizzi la ricorsione:

> (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) "done") (T (PROG2 $ (CW "~ x0" n) (Foo-loop (1- n)))))

(foo-loop 10)

È possibile rifare la condizione di terminazione e la ricorsione per imitare che va da 1 a 10.