问题标签 [non-termination]

我有这个代码

当我投射类似的东西np(X). vp(X).或pp(X)得到一个可能的解析然后出现堆栈错误时。当我投射时，s(X).我什至没有得到解析。我知道这是因为有一些无限循环正在运行，但我无法指出它在哪一点被循环。我认为这可能会发生，因为我的所有变量都使用相同的名称，但后来我将它们更改为单独的，它没有改变任何东西。

有人有提示吗？

提前致谢！

我尝试做一些练习 - 以“s 表示”表示数字，这意味着“0”为零，s(0) 为 1，s(s(0)) 为 2，依此类推。我尝试编写谓词来添加“s numbers”：谓词 s2int 将“s number”转换为 int。

当我查询添加时，它会写入正确的答案，但提示不会回来。有什么问题？

The third chapter of CPDT briefly discusses why negative inductive types are forbidden in Coq. If we had

then we could easily define a function

so that the term uhoh (Abs uhoh) would be non-terminating, with which "we would be able to prove every theorem".

I understand the non-termination part, but I don't get how we can prove anything with it. How would one prove False using term as defined above?

TL;DR：这个问题是关于评估候选故障片的一个特定方面。

以下代码ancestor_of/2表示 的传递闭包child_of/2：

如果我们定义child_of/2并包含几个循环......

...ancestor_of(X, Y)不会普遍终止：

使用 SWI-Prolog，我们可以限制在执行查询中投入的工作量：

好吧，但 它可能会更好！

• 首先，我们或许能够明确地证明目标循环。
• 其次，我们也许可以用更少的努力做到这一点。

让我们添加一个额外的参数来ancestor_of/2传输调用堆栈信息！

示例查询：

是这个吗？！那太容易了。这是否涵盖一般情况？

我觉得我错过了一些重要的东西，但我不能完全指出它。请帮忙！

我们正在实施诊断工具，用于解释纯单调 Prolog 程序中意外的普遍不终止——基于故障切片的概念。

正如论文“本地化和解释带有故障片的非终止逻辑程序的原因”中所介绍的那样，在许多程序点添加目标false/0以减少解释候选的程序片段大小（同时仍然保留非终止）。

到目前为止，一切都很好......所以我的问题¹来了：

为什么有 N 个目标的子句中有 N+1 个程序点？

或者，更准确地说：

为什么N分不够？我们是否需要第 (N+1) 个程序点？

难道我们不能把它转移false到关注谓词的每次使用上吗？

此外，我们知道程序片段仅用于查询，例如?- G, false.

_{脚注 1：我们假设每个事实foo(bar,baz).都被视为规则。foo(bar,baz) :- true.}

我是 Prolog 的新手，需要在不使用内置谓词的情况下对自然数实现一些基本的算术运算。

我用一元表示法表示自然数 Term，这意味着我有常数 0 和递归后继仿函数s [即 4 = s(s(s(s(0))))]。关于上述符号，我实现了算术运算。

规则集是：

现在，当我查询时：

我一切正常：

RES = s(s(s(s(s(s(0))))))。

当我查询时：（想问6/3=？）

我陷入了无限循环并得到了如此

即使我更改了 mult 谓词中递归调用的顺序，它也无济于事：

我在 linux 机器上运行 swi-prolog。

将感谢您的建议！

我正在阅读Thinking as Computation一书，并将代码编写为第 9.4 章：

但我发现程序永远不会停止......打印堆栈信息后，我发现goal_state生成了无限长的列表。我试图限制列表的长度has_banana

它N指的是Lin的长度plan(L)（例如Nquery 时为 4 plan([M1, M2, M3, M4])）但它不起作用。

有什么解决办法吗？

我正在尝试解决这个问题，并且我已经阅读了这个答案，但我的问题是无限循环，即使我使用了访问过的节点列表。

让我们看看我的两次尝试：

这给了我类似的答案，即：

然后 Swi-Prolog IDE 冻结。

• 我应该将什么定义为基本情况？
• 如果是这种情况，为什么第二个实现会循环，即使我使用访问的节点列表和 dif() 来确保避免统一来回走动？我打错了函数名。

我想摆脱 length/2 的使用。谢谢。

编辑：

所以，我发现这应该是更干净的方法，即使我想要更类似于第二种实现的东西，这在最短路径问题求解器中更容易转换，因为它只是一个 min{ pathLengths }从第一次调用 path3/4 开始。

这是第二个实现路径2的更正版本：

所以

工作和终止和

也可以工作并终止。但不知何故

不终止。可能的原因是什么？

到目前为止，我在 Prolog 程序中始终坚持的意思是：

如果对于 query Q，有一个 subterm S，这样有一个T使?- S=T, Q. success虽然?- Q, S=T. failed的术语，那么调用的谓词之一Q不是坚定的。

直觉上，我因此将坚定性理解为我们不能使用实例化来“欺骗”谓词来给出解决方案，否则这些解决方案不仅从未给出，而且被拒绝。注意非终止程序的区别！

特别是，至少对我来说，逻辑上的纯粹总是意味着坚定不移。

例子。为了更好地理解稳定的概念，考虑一个几乎经典的反例，在向高级学生介绍 Prolog 的操作方面时经常引用该属性，使用了两个整数与其最大值之间关系的错误定义：

一个明显的错误——我们是否应该说“摇摆不定”——定义当然是以下查询错误地成功：

而交换目标会产生正确的答案：

这个问题的一个很好的解决方案是依靠纯方法来描述关系，例如：

这在两种情况下都可以正常工作，甚至可以在更多情况下使用：

现在 Covington 等人的论文Coding Guidelines for Prolog由该概念的发明者Richard O'Keefe 合着，包含以下部分：

5.1 谓词必须坚定。

任何体面的谓词都必须是“坚定不移的”，即，如果它的输出变量恰好被实例化为输出值，则必须正确工作（O'Keefe 1990）。

那是，

和

必须在完全相同的条件下成功并且具有相同的副作用。只有辅助谓词的调用模式受到主谓词的强烈约束，否则只能容忍这种情况。

因此，引用论文中给出的定义比我上面所说的要严格得多。

例如，考虑纯Prolog 程序：

现在我们处于以下情况：

这显然违反了在完全相同的条件下成功的属性，因为其中一个查询根本不再成功。

因此我的问题是：我们是否应该称上述程序不坚定？请解释坚定性背后的意图及其在现有文献中的定义、其与逻辑纯度的关系以及相关的终止概念，以证明您的回答是正确的。