调用函数 n 次 acl2

Question

我不知道如何调用一个函数 n 次以在另一个函数中使用

我有一个功能

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

我需要编写另一个需要移动 '(l) n 次的函数

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

我什至不确定我是否正确启动了该函数，并且我不知道如何调用它 n 次。

Answer 1

您应该提供更多有关问题的背景信息。如果你想按位移动数据，我想有更有效的方法。

对于家庭作业式的解决方案，我会从这样的事情开始：

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

但我不是一个非常有经验的 Lisper。

Answer 2

ACL2 是用 Common Lisp 实现的定理证明器，其语言类似于 Common Lisp，但有一些差异。它的定理适用于可数论域，该论域遗传地由符号、整数、有理数（但不是浮点数）、复数有理数、字符串和 cons 单元构建而成。

ACL2 的论域也排除了函数，因此无法表达高阶函数。

因此，这是所有 ACL2 函数运行的域，但还有一个额外的要求，满足完整性检查器。

基本上，ACL2 内核必须确信您的函数将始终终止，而证明这一点的主要方法是在结构上引入您的参数之一（例如调用较小的数字或在每个代码路径中调用子列表）。我对 ACL2 不太有经验，对完整性检查器也不太了解。如果 ACL2 不接受我的定义之一，我通常只是重写它或将其分解为更小的函数。通过这种方式，您可以取得合理的进步。

综上所述，有两种方法可以在 ACL2 中模拟高阶函数。

一种方法是定义自己的递归函数来调用另一个函数，就像Martin Buchmann对此问题的回答中所做的那样。如果您愿意的话，可以将其隐藏在宏后面。

另一种方法是使用宏构建一个大型表达式，然后将其馈送到内部的完整性检查器（当在函数体内时）或仅进行评估。

这是一个名为

repeat

的宏的样子，它会重复调用某些内容。

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