How to loop using recursion in ACL2?

Question

I need to make something like this but in ACL2:

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

It uses COMMON LISP, but I haven't any idea how to do this task...

We can't use standard Common Lisp constructions such as LOOP, DO. Just recursion.

I have some links, but I find it very difficult to understand:

• Gentle Intro to ACL2 Programming

Answer 1

The section "Visiting all the natural numbers from n to 0" in A Gentle Introduction to ACL2 Programming explains how to do it.

In your case you want to visit numbers in ascending order, so your code should look something like this:

(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

A solution that uses recursion:

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

You can redo the termination condition and the recursion to mimic going from 1 to 10.