问题标签 [unification]

我想仔细看看OCaml中类型推断的实现，我的OCaml似乎安装在/usr/local/lib/ocaml，但.ml里面似乎没有包含类型推断的代码......

有人可以帮忙吗？

我在 PROLOG 中编写了我的第一个简单代码：

它旨在找出 is_beginning 的第一个参数是否等于第二个开始。好吧，恕我直言，它可以很好地回答问题，但现在我想知道是否有可能获得定义的第二个参数的所有可能答案。例如。为了

我希望得到 [], [a], [a,b], [a,b,c] 作为答案统一，但我只得到 [] （最简单的答案）。

有没有可能得到我想要的？也许我的定义有问题？我已经尝试使用 findall 和 forall，但对我来说效果不佳:(

感谢所有的答案。

在 Prolog 中：

B 显示为 [_G1091] 表明它是一个未实例化的变量。但是，如果我稍微改变...

突然之间，它对向我展示 B 未实例化但仍然是一个准备好与任何东西统一的变量不感兴趣.. 怎么会？（有时我喜欢关注奇怪的细节：）

这是过去考试中关于 Prolog 统一的问题。我们应该说它们是否统一，然后是实例化。

这统一了 a = X, g(b,a) = g(Y,X) 并且非常简单

我不认为这是因为 g(Y) =/ X 而统一，尽管 h(c,d) 确实与 h(W,d) 统一。虽然有可能 X = g(Y) 因为大写 X 一直查找直到找到解决方案？

我想实现一个解析算法，它在解析候选子句时尝试获取空集。

我希望算法以广度优先顺序解决候选父子句。但是，我有一点困惑：

令 S 为知识库中所有子句的合取和目标子句的否定

当我们尝试用 S 中的候选子句解析 S 中的候选子句时，我们得到 S'

作为算法的第二步，我们应该尝试用 S' 本身来解决 S 和 S' 还是 S'？它应该如何进行？

例如;

假设知识库+否定。目标集由一组子句组成，例如

p(a,b) ^ q(z),~p(z,b) ^ ~q(y) ((我们称这个集合为 S)

当我们在集合 S 上运行解析算法时，我们得到如下子句：

q(a) ^ ~p(z,b)（我们称这个集合为 S'）

现在，如果我们必须采用 BFS 策略，我们是否应该首先找到其第一个父级在 S 中，第二个在 S' 中的解析器？或尝试检查其父母都来自S'的解析器？

在某些示例中，当您第一次使用 S' 和 S' 检查解析剂时，您会得到解决方案。但是，当您继续检查一对集合 (S, S') (S, (S, S')) 时，您会得到另一种导致空子句的方法。那么，BFS 对应的是哪个顺序呢？

提前致谢

给定 Haskell 函数：

现在的问题是如何手动“手动”查找类型。如果我让 Haskell 告诉我我得到的类型：

但我想了解它是如何工作的，仅使用定义如下的已使用函数的签名：

编辑：这么多很好的解释......选择最好的并不容易！

我正在使用 prolog 脚本来执行所有查询，代码如下：

问题是，queryAll当我想看到统一结果时，只会打印“是”或“否”：

如何在序言中做到这一点？提前致谢。

我正在尝试研究在无类型语言上使用自定义类型推理语言的项目的可行性。（语言本身并不重要，但它恰好是 PHP）。我的第一个想法是对此运行类型统一。我在 Haskell 中编写了一些程序，所以我知道从最终用户的角度来看类型统一是如何工作的，但我从未深入研究过算法的细节。

此时，我可以解析一个 PHP 代码文件，构建一组相应的规则，并希望开始针对这些规则运行统一算法。与其重新发明轮子，我想我会使用现有的统一算法，而 AFIAK，Prolog 是目前最强大的统一算法之一。

我现在已经到了这样的程度，如果我传入一个可验证的正确输入，Prolog 就会返回“true”。如果我传入不正确的内容，它会返回“错误”。现在我在那种情况下真正想要的是得到一条错误消息，指出为什么类型没有统一。如果我在 SWI-Prolog 中打开“跟踪”模式，我或多或少会得到我想要的东西，逐步解释为什么类型没有统一。我的核心问题是，是否可以通过编程方式获取这些信息？如果需要的话，我愿意编写一个 C 扩展并直接链接到 Prolog 编译器。此外，我与 SWI-Prolog 没有任何联系，它只是我在 google 上找到的第一个。

另外，作为一个完整的问题，有没有人知道序言中的任何好的教程，无论是网络格式还是作为一本真正的书？

我有一个学校项目，我必须与 Prolog 一起工作。这对我来说都是新的，所以我遇到了一些问题。

我有一个这样的列表：

我应该通过我必须创建的几个谓词从每个成员的输入信息中接收。

其中之一是以下类型：

它说 M1 是 M2 或 M3，但不是两者兼而有之。例如，

表示带有“a”的成员在第一个字段中有 2 或 3。

我整晚都在尝试，但无法提出解决方案。我相信我必须使用统一，但不知道该怎么做。

我试过这个：

这可能看起来很荒谬，但正如我所说，Prolog 对我来说是全新的，我不能完全掌握它的功能。

任何提示表示赞赏。谢谢！

编辑：

例子：

所以现在我有一个 3 人的列表，爱因斯坦排在第一位。

以上是应用谓词后的 2 个可接受的列表。

这应该是一个简单的问题，但我无法弄清楚。

谢谢！

我有一组形式的定义pair/2和一个谓词propagate/3：

如果我有List = [pair(1, 2), pair(2, 3), pair(3, 4), pair(4, 5)]而且我有

我得到了想要的输出，Result = [1, 3]; 即与 形成对的所有数字的列表2。

但是，如果我有List = [pair(N1, N2), pair(N2, N3), pair(N3, N4), pair(N4, N5)]并且如果我有

那么输出是

Result = [N1, N3]相反，我希望输出为。我怎样才能做到这一点？