Добавление взаимных оценок в ACL2 - PullRequest
Новая
       57

Добавление взаимных оценок в ACL2

0 голосов
/ 22 сентября 2018

Я очень новичок в 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)

1 Ответ

0 голосов
/ 22 сентября 2018

ACL2 использует синтаксис LISP, что означает, что вам нужны префиксные операторы.Так что 1 / n ^ 2 должно быть (/ 1 (* nn)).

LISP позволяет множеству символов находиться в имени, 1 / n ^ 2 в вашем примере рассматривается как имяпеременная, которая ни к чему не привязана (тоже не к входу).Вот почему вы получаете сообщение об «свободном вхождении переменной».

...