问题标签 [successor-arithmetics]

我正在阅读“序言的艺术”一书，我发现了一个练习，上面写着“如果 Sum 是 ListOfIntegers 的总和，则定义关系 sum(ListOfIntegers,Sum)，而不使用任何辅助谓词”。我想出了这个解决方案：

这并不像我想要的那样工作。

我期待 X 是

我认为问题在于我必须在第一次“迭代”中将 Sum 初始化为 0，但这将是非常程序化的，不幸的是我不太适合在 prolog 中完成这项工作。有什么想法或建议吗？

我需要使用自然数为 2 的幂创建一个 Prolog 谓词。自然数是：0、s(0)、s(s(0)) 等等。

例如：

这是我的代码：

它与第一个示例完美配合，但在第二个示例中进入无限循环。
我该如何解决这个问题？

不断收到Arguments are not sufficiently instantiated我写的乘法乘法规则的错误，如下所示。

我是 Prolog 的新手，即使是这样简单的问题也很挣扎。

任何关于书籍或在线教程的建议都会很棒。

我在 Ubuntu Linux 上的 SWI-Prolog 上运行它。

我开始学习 Prolog 并首先了解了后继符号。

这就是我发现在 Prolog 中编写 Peano 公理的地方。

请参阅PDF的第 12 页：

我将乘法规则放入 Prolog。然后我进行查询：

这意味着基本上找到了 6 的因数。

这是结果。

这个结果有两个问题：

1. 并未显示所有结果，请注意结果 X=6,Y=1 缺失。
2. 它不会停止，除非我 Ctrl+C 然后选择中止。

所以......我的问题是：

1. 这是为什么？我尝试切换“prod”和“sum”。结果代码给了我所有的结果。再说一次，为什么会这样？虽然它仍然是死循环。
2. 如何解决？

我读了关于无限循环的另一个答案。但我很感激有人根据这种情况回答。它对我有很大帮助。

有人可以向我解释为什么这个序言查询会这样工作。定义是：

鉴于这种：

这是查询的跟踪：

那个教程最让我困惑的部分是，在第一个参数中，成功被剥离了，并且它递归了。虽然在递归时，R 获得了成功......如何？！另外，第一个出口 (9) 处的零是从哪里来的？我是序言的新手，我正在努力理解家庭作业的语言。非常感谢任何帮助。

注意：对于任何感兴趣的人，本教程的链接是http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse9

我是 Prolog 的新手，我正在尝试解决这个问题：

定义一个谓词，该谓词greater_than/2采用我们在本讲座中介绍的符号（即 , ...）中的两个数字0作为succ(0)参数succ(succ(0))，并确定第一个数字是否大于第二个数字。例如：

到目前为止，这是我的回答：

但当然不能正常工作，所以我正在向任何人寻求帮助。谢谢。

我正在尝试实现类型安全的二项式堆。为此，我有两种数据类型，它们的元素类型由它们的类型编码索引参数化：

Vec使用递减的数字参数对值进行编码，其中最后一个元素始终由 参数化Zero。RVec使用增加的数字参数对值进行编码，没有其他限制（这就是为什么RNil可以产生RVec任何数字的原因）。

这允许我（例如）拥有一个高度增加/减少的树木列表，由类型系统检查。在实现了我的大部分项目之后，我意识到我需要一个看似简单的函数，但我无法实现：

它应该简单地颠倒给定列表的顺序。有任何想法吗？提前致谢。

我在 Prolog 中做一个非常简单的练习，跟踪中有一些我不明白的东西。>该程序是对表示为后继的整数的“大于”( )：

我的问题：我不明白为什么请求会在以下跟踪中greater_than(succ(succ(succ(0))),succ(0))生成：redo

为什么redo这里有？我怎样才能避免它（当然没有削减）？

顺便说一句，在你问之前：不，这不是某种家庭作业......

编写一个谓词less/2，如果 t1 代表 n1，t2 代表 n2，则 less(t1, t2)当 n1 < n2 时成功。例如，less(s(z), s(s(s(z))))应该成功，less(s(z), s(z))应该失败。如果 t1 是未实例化的逻辑变量，而 t2 是自然数 n2 的正确表示，则谓词应枚举小于 n2 的所有数。例如，查询

应该成功X = z并且X = s(z)（不一定按此顺序）。

让我们考虑以下 Prolog 程序（来自“Prolog 的艺术”）：

和查询：

SICStus 和 SWI 都会产生预期的Z = s(s(s(s(0))))答案，但会向用户查询下一个答案（正确no/false答案）。但是，我无法理解为什么在找到唯一目标之后 SLD 树中有一个开放的分支。我尝试在 SICStus 和 SWI 下进行调试，但我还不能真正解释结果。我只能说，据我所知，两者都回溯到plus(s(s(s(0))), 0, _Z2). 有人可以帮助我理解这种行为吗？