问题标签 [successor-arithmetics]

我正在开发（在 Java 中），为了好玩，一个使用统一算法的应用程序。

我选择我的统一算法返回所有可能的统一。例如，如果我尝试解决

添加（X，Y）=成功（成功（0））

它返回

{X = succ(succ(0)), Y = 0}, {X = succ(0), Y = succ(0)}, {X = 0, Y = succ(succ(0))}

然而，在某些情况下，可能存在无限多的统一（例如 X > Y = true）。

有人知道算法允许确定是否可能遇到无限数量的统一吗？

提前致谢

我试图了解公理解析在 prolog 中是如何工作的。

假设我定义了自然数的两个基本运算：

• s(term)（代表继任者）和

• 添加（术语，另一个术语）。

add 的语义由下式给出

• 添加 (0, x1) -> x1

• 添加 (x1, 0) -> x1

• 添加（s（x1），y1）-> s（添加（x1，y1））

然后，我想解方程

添加（x，添加（y，z））= s（0）

我想一种策略可能是

• 测试等式的右手边 (RHS) 是否等于其左手边 (LHS)

• if not 看看是否可以通过寻找最通用的统一器找到解决方案

• 如果不是，那么尝试找到一个可以在这个方程中使用的公理。完成这项工作的策略可能是（对于每个公理）：尝试求解方程的 RHS 等于公理的 RHS。如果有解，则尝试求解方程的 LHS 等于公理的 LHS。如果它成功了，那么我们就找到了正确的公理。

• 最终，如果没有解，并且方程的 LHS 和 RHS 是相同的操作（即相同的签名但不同的操作数），则将算法应用于每个操作数，如果为每个操作数找到解，则找到解。

我认为这个（简单的）算法可能有效。但是，我想知道是否有人有解决此类问题的经验？有谁知道我在哪里可以找到一些关于更好算法的文档？

提前致谢

编辑：解决。我不知道在源文件中启用语言扩展名并没有在 GHCi 中启用语言扩展名。解决方案是:set FlexibleContexts在 GHCi 中。

我最近发现 Haskell 中的类和实例中的类型声明是 Horn 子句。所以我将 Prolog 的艺术第 3 章中的算术运算编码到 Haskell 中。例如：

在 Prolog 中，为证明中的（逻辑）变量实例化值。但是，我不明白如何在 Haskell 中实例化类型变量。也就是说，我不明白 Prolog 查询的 Haskell 等价物是什么

是。我假设

会导致 Haskell 实例化xi，但这会产生Non type-variable argument in the constraint错误，即使FlexibleContexts启用。

我有下一个自然数的程序是 SWI-prolog：

现在我想做一个递归调用，当我们到达 0 时停止。

我的自然数由 -s(0)=0, s(s(0))=1, s(s(s(0)))=2, etc

所以我定义：

并打电话给：3,5,s(0). 但它给了我错误：out of local stack。

问题是什么？谢谢你。

这是我不明白的加号代码

同时给出：

我不明白这个递归。如果我有我plus(s(0),s(s(s(0))),Z)怎么能得到答案1+3=4？

我需要对第一个代码进行一些解释。我尝试这样做plus(0,X,X)会停止递归，但我认为我做错了。

我有下一个规则

查询是：ackermann (M,N,s(s(0)))。

现在，据我了解，在第三次计算中，我们得到了无限搜索（失败分支）。我检查了一下，我得到了一个有限搜索（失败分支）。

我将解释：首先，我们得到了 M=0, N=s(0) 的替换（规则 1 - 成功！）。在第二个中，我们得到了 M=s(0),N=0 的替换（规则 2 - 成功！）。但是现在呢？我尝试匹配 M=s(s(0)) N=0，但它有一个有限搜索 - 失败分支。为什么编译器不写我“失败”。

谢谢你。

我正在尝试使用余数定理和良序原则来定义序言中的除法。

到目前为止，我已经：

但是 的定义在div某种程度上是错误的。有人可以给我一个提示吗？

PS：我不应该使用eq，但我无法获得is或=工作。

我有这个非常简单的代码作为数字的表示。问题是当我使用 add2 函数时。

示例：正确add2(s(0)+s(s(0)), s(s(0)), Z).返回s(s(s(s(s(0)))))。然而add2(0, s(0)+s(s(0)), Z).总是returns s(0)+s(s(0))。谁能明白为什么会这样？

我一直在尝试学习 Prolog，并且完全不知道谓词 s() 的作用。我看到它经常使用，互联网上关于 Prolog 的资源很少，我找不到答案。

前任。

我在教程中遇到了逻辑数的自然数评估，这让我有些头疼：

该规则大致说明：如果N它0是自然的，如果不是，我们尝试将s/1返回的内容递归地发送到规则，直到内容为0，那么它是一个自然数，如果不是那么它不是。

所以我测试了上面的逻辑实现，心想，如果我想表示s(0)as1和s(s(0))as ，这很有效2，但我希望能够转换s(0)为1。

我想到了基本规则：

所以这是我的问题：如何将 s(0) 转换为 1 并将 s(s(0)) 转换为 2？

已回复

编辑：我修改了实现中的基本规则，我接受的答案指向我：

所以我现在可以随心所欲地使用它了，谢谢大家！