lisp - 在 ACL2 中添加倒数
问题描述
我对 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)
解决方案
ACL2 使用 LISP 语法,这意味着您需要前缀运算符。所以 1/n^2 应该是 (/ 1 (* nn))。
LISP 允许名称中包含许多字符,示例中的 1/n^2 被视为变量的名称,它没有绑定到任何东西(也不是输入)。这就是您收到“自由出现变量”错误的原因。
推荐阅读
- reactjs - 编写用于渲染帖子列表的测试用例
- rstudio - 减小辅助窗口大小
- c++ - c++中的“@”是干什么用的
- node.js - 虽然我删除了数据,但除非我刷新页面,否则我看不到它被删除
- google-cloud-platform - 没有名为 providers.google.cloud.operators.pubsub 的模块:Google Cloud Composer
- postgresql - 选择多行时Postgres慢
- sql - SQL 2014 - 如何为非标识列的每一行添加增量值
- python - 如何对 vaex 中的列进行 json 规范化?
- spring - java.sql.SQLException:不正确的字符串值:'\xCFC\xFB\xC3\xD4U...'
- api - 蒸汽 API 2020