在ACL2中添加往复式

Question

我对ACL2非常陌生，所以我理解你们中的一些人可能会觉得这是一个非常简单的解决方案，你们会对我的帮助表示不满。我试图弄清楚如何使我的代码加起来等于N个倒数平方(也就是说，如果是n=4，那么我正在寻找1/1 + 1/4 + 1/9 + 1/16)。

我有一个函数，加起来等于n，它的工作原理如下所示

(defun sum-up-to-n (n)
(if (zp n)
       0
       (+ n (sum-up-to-n (- n 1)))))

与倒数平方，如下所示

(defun sum-up-to-nSqRecip (n)
   (if (zp n)
       0
         (+  (sum-up-to-nSqRecip (- n 1))) 1/n^2) ))

我收到此错误：“求和到NSQRECIP的主体包含变量符号\1/N^2的自由出现。请注意，在条件上下文(NOT (ZP N))的上下文中，从一个IF测试中发生的情况是连1/N^2都会发生。”我不知道如何解决这个错误。

包括的东西

(encapsulate nil
  (set-state-ok t)
  (program)
  (defun check-expect-fn (left right sexpr state)
    (if (equal left right)
      (mv nil (cw "check-expect succeeded: ~x0~%" sexpr) state)
      (er soft nil "check-expect failed: ~x0
      Expected: ~x1
      Actual:   ~x2" sexpr right left)))
  (defmacro check-expect (&whole sexpr left right)
    `(check-expect-fn ,left ,right (quote ,sexpr) state))
  (logic))

(include-book "doublecheck" :uncertified-okp t :dir :teachpacks)
(include-book "arithmetic-5/top" :uncertified-okp t :dir :system)

Answer 1

ACL2使用LISP语法，这意味着您需要前缀操作符。所以1/n^2应该是(/ 1 (* n))。

LISP允许许多字符在名称中，在您的示例中，1/n^2被视为变量的名称，它不绑定到任何东西(也不是输入)。这就是为什么您要接收“自由发生的变量”错误。