1

我对 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) ))

我收到此错误“SUM-UP-TO-NSQRECIP 的主体包含自由出现的变量符号 |1/N^2|。请注意 |1/N^2| 出现在条件上下文中（NOT (ZP N)) 来自周围的 IF 测试。” 我不知道如何解决这个错误。

包括的东西

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

1 回答 1

5

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

LISP 允许名称中包含许多字符，示例中的 1/n^2 被视为变量的名称，它没有绑定到任何东西（也不是输入）。这就是您收到“自由出现变量”错误的原因。

于 2018-09-21T23:26:45.173 回答