Calling a function n times acl2

Question

I cannot figure out how to call a function n times to be used in another function

I have a function

(defun right-shift (l)
   (append l '(0))) 

And I need to write another function that needs to shift '(l) n times

(defun right-shift-n-times (l n)
   (natp n)
       ...)

I am not even sure I started that function right and I cannot figure out how to call it n times.

Answer 1

ACL2 is a theorem prover implemented in Common Lisp whose language resembles Common Lisp but has a few differences. Its theorems apply to a countable domain of discourse, which is hereditarily built up from symbols, integers, rationals (but not floats), complex rationals, strings, and cons cells.

ACL2's domain of discourse also excludes functions, so higher order functions cannot be expressed.

So, this is the domain that all ACL2 functions operate on, but there is an additional requirement, satisfying the totality checker.

Basically, the ACL2 kernel has to be convinced that your function will always terminate, and the main way to prove that is to structurally induct on one of your parameters (like calling a smaller number or calling a sublist in every code path). I'm not very experienced with ACL2 and don't know much about the totality checker. If ACL2 doesn't accept one of my definitions, I generally just rewrite it or break it into smaller functions. You can make a reasonable amount of progress this way.

All that being said, there are two ways of emulating higher-order functions in ACL2.

One way is to define your own recursive function that calls another function, as is done in Martin Buchmann's answer to this question. This can be hidden behind a macro if you are so inclined.

Another way is to use a macro to build a large expression, which will then be fed to the totality checker internally (when inside a function body) or just evaluated.

Here's how that might look like for a macro called repeat which calls something repeatedly.

;; BEGIN_HEADER                                                                                                                                                                              
;; (defpkg "ACL2-REPEAT"                                                                                                                                                                     
;;  (union-eq *common-lisp-symbols-from-main-lisp-package*                                                                                                                                   
;;   *acl2-exports*))                                                                                                                                                                        
;; END_HEADER                                                                                                                                                                                
                                                                                                                                                                                             
(in-package "ACL2-REPEAT")                                                                                                                                                                   
                                                                                                                                                                                             
(defun right-shift (l)                                                                                                                                                                       
  (append l '(0)))                                                                                                                                                                           
                                                                                                                                                                                             
                                                                                                                                                                                             
(defun repeat-implementation (n f arg others)                                                                                                                                                
  (cond                                                                                                                                                                                      
    ((= (nfix n) 0) arg)                                                                                                                                                                     
    ((= (nfix n) 1) `(,f ,arg ,@others))                                                                                                                                                     
    (t `(,f ,(repeat-implementation (1- (nfix n))                                                                                                                                            
                                    f                                                                                                                                                        
                                    arg                                                                                                                                                      
                                    others)                                                                                                                                                  
            ,@others))))                                                                                                                                                                     
                                                                                                                                                                                             
                                                                                                                                                                                             
(defthm repeat-implementation-0                                                                                                                                                              
        (equal (repeat-implementation 0 'a 'a 'a) 'a))                                                                                                                                       
                                                                                                                                                                                             
(defthm repeat-implementation-1                                                                                                                                                              
        (equal (repeat-implementation 1 '1+ 1 nil)                                                                                                                                           
               '(1+ 1)))                                                                                                                                                                     
                                                                                                                                                                                             
(defthm repeat-implementation-2                                                                                                                                                              
        (equal (repeat-implementation 2 '1+ 1 nil)                                                                                                                                           
               '(1+ (1+ 1))))                                                                                                                                                                
                                                                                                                                                                                             
(defmacro repeat (n f &rest args)                                                                                                                                                            
  (repeat-implementation n f (car args) (cdr args)))  

Answer 2

You should given some more background of your problem. If you want to shift bit-wise data there are way more efficient ways, I guess.

For a homework-style solution, I would start with something like this:

 (defun right-shift-n-times (l n)
       (if (zerop n)
           l
           (right-shift-n-times (right-shift l) (1- n))))

but I am not a very experienced lisper.