问题标签 [acl2]

我不知道如何调用一个函数 n 次以在另一个函数中使用

我有一个功能

而且我需要编写另一个需要移动'（l）n次的函数

我什至不确定我是否正确启动了该功能，我无法弄清楚如何调用它 n 次。

我是 ACL2 定理证明器的新手。我想根据三个变量的 XOR 结果更新变量的值。我认为“setq”会为我做到这一点。

但是，我收到此错误：

TOP-LEVEL 中的 ACL2 错误：符号 SETQ（在包“COMMON-LISP”中）在 ACL2 中既没有函数也没有宏定义。此外，这个符号在 Lisp 主包中；因此，您不能在 ACL2 中定义它。请参阅：DOC 未遂事件。注意：这个错误发生在上下文（SETQ OUT (XOR (XOR AB) C)）中。

我们不能在 ACL2 中使用主要的 Lisp 函数吗？是否有另一种方法来更新 ACL2 中的变量值？我已经尝试过“分配”，但我不希望我的变量成为全局变量。

我对 ACL2 非常陌生，所以我知道你们中的一些人可能会觉得这是一个如此简单的解决方案，以至于您会不赞成我的外展寻求帮助。我试图弄清楚如何让我的代码加起来为第 N 个倒数平方（如果 n = 4，那么我正在寻找 1/1 + 1/4 + 1/9 + 1/16）

我有一个函数可以加起来 n 并且它可以工作并且看起来像这样

倒数平方看起来像这样

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

包括的东西

试图弄清楚如何遍历 ACL2 中的列表，我知道它可以在 lisp 中完成，但我不能使用这些函数。任何提示将非常感谢。

所以我对 acl2 和 lisp 还比较陌生，我不知道在 lisp 中这样做的方法。我怎样才能实现我的评论？（缺点...）我一直在思考迭代器，但有人告诉我 ACL2 只使用递归

对于这个问题，我被分配实现一个函数，该函数在给定数据的情况下决定决策树的输出。逻辑：如果是符号，那么就是输出的值，否则，在内存中查找varname的值，如果小于等于阈值，则在left-tree中查找该值，如果大于超过阈值，在右树中查找值

决策树是： 一个符号，例如 'versicolor 或 [ varname threshold left-tree right-tree ]

这是我已经完成的，

这是一个单元测试：

这是使用的常量的定义

当函数到达递归调用时，我不断收到错误。它说“（DEFUN DECISION ...）中的ACL2错误：否：MEASURE提供了DECISION的定义。”

我测试了每个 if 语句以查看它们是否有效，并多次在我的脑海中运行代码的逻辑，似乎我可能遇到的唯一问题可能是语法错误，但一切似乎都是正确的。

这应该是一个函数的定义，如果输入的值是偶数自然数，则返回t，如果输入的值是奇数自然数，则返回nil：

当我输入一个偶数时，它会正确返回t并且它应该为其他任何东西返回nil但它没有！其实我猜它不会停止，我不明白为什么。当我输入像 -1 这样显然不是偶数自然数的数字时，我希望这段代码首先通过“if”，因为 (zp -1) 等于t，并且由于 -1 不等于 0，因此 (zerop - 1) 应该是nil，这意味着输出应该是nil并且程序应该终止。

事实上，我知道如何以实际工作的方式更好地实现这个功能，我只需要知道为什么这段代码不起作用，以便更好地理解这种语言，因为我刚刚开始学习 ACL2！...

谢谢您的考虑。

我在 ACL2 中定义一个（is-related）函数时有点挣扎。有人告诉我它可以在一行中完成，但我不确定如何做到这一点。目标是定义函数（is-related xy R）。请记住，关系是对的列表，因此例如 R 可能如下所示：

((a 1) (a 2) (b 1) (b 3) )

在这种情况下，

(is-related 'a 1 R) = T

(is-related 'a 3 R) = NIL

提示：这应该很容易编码，只需一行代码即可。

我曾尝试将该函数definec contains 与 a 一起使用，if-then-else statment但它肯定比一行代码长。我对如何做到这一点进行了一些研究，并且不断收到使用建议，defthm 但我认为这不是问题所要求的。任何帮助，将不胜感激！

目标是将“或”标识应用于第一个表达式的某些部分。我对如何做到这一点有点困惑。我知道我需要使用命题表达式(OR expr1 expr2)，但我不确定如何去做。任何帮助，将不胜感激。

1. 请记住，我们可以在表达式的深处使用命题公理，而不仅仅是在表达式本身的顶部。编写一个函数(from-or-identity expr1 expr2) ，当 expr2 是对 `expr1. 例如

我正在尝试用 d 交换数字列表的第 n 位。我找到了一种用 1 替换第 n 位数字的方法，但我不知道如何概括它，以便我可以使用definec通用字母替换第 n 位数字。

1. 我们有兴趣检测错误，例如无效的票号。我们想要展示的是，如果一个票号写错了，例如，有一个常见的错误（改变一个数字或调换两个相邻的数字），那么生成的票将是无效的。

   首先，我们需要编写执行这两种错误的函数。即，编写一个函数，该函数(change-nth-digit-to ticket n d)返回一个与旧票相等的新票，只是第 n 个数字是 d。另外，编写一个名为的函数，该函数(transpose-nth-digit ticket n)返回一张票，其中第 n 个数字与下一个数字交换。

   重要提示：我们稍后将使用这些函数，所以不要将它们编写为仅用于机票。编写它们，以便它们适用于任意数字列表。

   注意：如果票证中有数字，n 应介于 0 和 -1 之间（对于 change-nth-digit-to）和介于 0 和 -2 之间（对于 transpose-nth-digit）。