问题标签 [non-termination]

我正在尝试在 Prolog中实现Levenshtein 距离。

实现非常简单：

但是，此代码失败并出现此错误：

我SWIPL在Mac OS X Sierra.

在Isabelle/HOL的优秀编程和证明中它说

[...] 与递归函数相比，归纳定义没有终止要求。（pdf 第 40 页）

1. 这是否意味着存在可以拥有无​​限深推导树的归纳定义？
2. 这种非终止派生的例子是什么（最好是无限高的派生）？你如何“构建”这些？
3. 关于这些的规则归纳原则如何仍然有效？

在这个关于如何getLine在 Agda 中做的问题中，主要答案建议使用偏性 monad 来处理可能不终止使用生成的 Costring 的情况。

另一方面，在 2.5.3 版本中，Coinduction的手册页建议不要使用 ∞，称它可以用来证明荒谬。但是 ∞ 用于IO.IO 和 IO.run的定义以及偏性monad。

问题：

1. 是否可以使用没有 ∞ 的标准库来进行偏心和非终止 IO？如果没有，有什么替代方案？
2. 标准库/文档是否过时？
3. ∞ 的问题是由于与大小类型的交互吗？

谢谢！

假设我想断言三个列表的长度相同。我可以做这样的事情：

First当实例化或Second实例化时，这会做正确的事情。当所有三个参数都被实例化时，它也可以工作！然而，调用 likelength(Third, 3), same_length(First, Second, Third)会导致它返回带有选择点的正确答案（所有三个列表的长度均为 3），然后永远循环生成永远不会匹配的解决方案。

我写了一个我相信在任何情况下都能做正确事情的版本：

我一直听说应该尽可能避免切割，这里可以避免吗？

作为一个额外的问题，我认为这些是绿色削减，因为最终谓词是完全相关的，这是真的吗？

我目前正在研究 Learn Prolog Now 示例，对于一个练习，如果我对一条规则进行微小更改，我的 KB 会用完本地堆栈。这是知识库：

和相关规则：

这是有问题的查询，它用完了堆栈：

但是，如果我将规则更改为

然后它工作。

如果我跟踪查询，我会很快陷入这样的困境：

但我不明白为什么。难道它不应该只了解 raglan 是一个终端站，因此它必须再回溯一个级别吗？

谢谢！

编辑：我使用 SWI Prolog

编辑：我一步步解决后发现了问题。在插肩的情况下，任何地方都没有规则。因此，在尝试之后byPlane, byTrain, byCar，它travel(raglan, X)再次尝试（最后一条规则的第一个目标），从而循环。但我看不出另一条规则有什么更好的地方。

我想知道为什么在这些情况下程序会无限递归：

和

这是代码：

我写了一个基本的java服务器类。当它处理“关闭”请求时，它会调用 server.stop(0) 并且旋转到位。为什么会这样？

我从这个 StackOverflow 帖子中复制了大部分代码。对这段代码的唯一重要修改是我添加了 server.stop(0)。

其他事实：我正在使用 java 8 运行它，我正在通过 IntelliJ 运行它。

目前，服务器向客户端返回响应消息（我使用邮递员测试过），然后将“Stopping Server”打印到控制台。在那之后，服务器对象似乎被关闭了，因为当我向它发送更多请求时，它没有响应它们，但是，运行服务器的线程继续旋转。

最低限度，我希望服务器能够到达这行代码

但它永远不会。

更重要的是，我希望服务器线程终止，但它只是旋转。

为什么会这样？（我在某处的代码中有死锁吗？）是否有更好的方法来处理服务器关闭（使用 httpserver 库）？

我正在尝试在 agda 中定义二进制数，但 agda 看不到它⟦_⇑⟧正在终止。我真的不想打破可访问性关系。如何向 agda 显示 n 变小？

错误：

在关于不终止的问题中，带有模糊终止的条款的答案建议求助于<-wellFounded.

我查看了<-wellFounded之前的定义，让我印象深刻的是--safe在OPTIONS. 没有这个选项就可以工作吗？也就是说，是在使用--safe一些优化，还是在解决一些基本问题？所以在这种情况下，我们只是将终止问题委托给标记为“安全”的函数？

在研究有根据的时候，我想看看不同的设计是如何表现的。例如，对于一个类型：

有根据很容易证明。但是如果类似的类型定义不同：

很明显，在这两种情况下，下降链都不是无限的，但在第二种情况下，有根据并不容易证明：(y -> y < x -> Acc y)对于给定的 证明存在并不容易x。

是否有一些原则可以帮助选择第一个设计而不是第二个设计？

证明第二个定义的有根据并不难，它只需要额外的定理。在这里，依靠_==_for的可判定性，我们可以为 caseNat构造新的，并且可以重写目标类型以使用已知尺寸减小问题的解决方案作为 for 的解决方案。_<_(suc y) != xsuc y