小编b33*_*3rz的帖子

我想知道如何仅使用cons,first,rest,empty等基本操作来反转列表.

不允许辅助函数或累加器,该函数只接受一个输入 - 列表.

我被告知这是可能的,虽然我无法绕过它.

这就是我到目前为止所概念化的内容.我不知道如何为列表的其余部分形成递归.

(defunc rev-list (x)
  (if (or (equal (len x) 0) (equal (len x) 1))
      x
      (cons (first (rev-list (rest x)))
            ???)))

显然,可以使用交换列表的第一个和最后一个的函数来执行类似的操作,但我也不完全理解它.这是它的代码:

(define swap-ends (x)
  (if (or (equal (len x) 0) (equal (len x) 1))
      x
      (cons (first (swap-ends (rest x))) 
            (swap-ends (cons (first x) 
                             (rest (swap-ends (rest x))))))))

我试图在ACL2s/Lisp中证明这个函数,但它返回一个堆栈溢出错误,虽然我看不到代码中的缺陷.

(defunc foo (x y)
 :input-contract (and (natp x) (natp y))
 :output-contract (natp (foo x y))
 (cond ((equal 0 x) (+ y 1))
       ((equal 0 y) (foo (- x 1) 1))
       (t (foo (- x 1) (foo x (+ y 1))))))