问题标签 [unification]

有谁知道类型推断问题如何

与打字环境

可以在统一问题中转移吗？

任何帮助将不胜感激！

问题

什么是最有效的 MGU 算法？它的时间复杂度是多少？在堆栈溢出答案中描述是否足够简单？

我一直试图在 Google 上找到答案，但一直在寻找我只能通过 ACM 订阅访问的私人 PDF。

我在 SICP 中找到了一个讨论：这里

解释什么是“最通用的统一算法”：采用两个包含“自由变量”和“常量”的表达式树......例如

然后最通用统一器算法返回使两个表达式等效的最通用绑定集。例如：

“最一般”的意思是您可以改为绑定{x ↦ 1}and{z ↦ 1}并且这也可以使e1和e2等效，但它会更具体。

SICP 文章似乎暗示它相当昂贵。

对于信息，我问的原因是因为我知道类型推断也涉及这种“统一”算法，我想了解它。

我试图弄清楚类型推断是如何实现的。特别是，我不太明白“统一”的繁重工作在哪里/为什么发挥作用。

我将在“伪 C#”中举一个例子来帮助澄清：

天真的方法是这样的：

假设您将程序“解析”成一个表达式树，以便可以使用以下命令执行它：

所以像“乘法”这样的东西可以用：

然后要“实现”类型推断，您可以执行以下操作：

那么“乘法”的类型推断可能就是这样的：

lhs 和 rhs 可能是简单的常量，或者是在环境中查找的“变量”：

但在这方面，我们最终不需要“统一”算法。

所以，很明显，我的例子不够复杂。它需要高阶函数吗？我们需要“参数多态性”吗？

什么是最简单的示例，其中实际上需要“统一”来正确推断表达式的类型。

Scheme 中的一个例子是理想的（即一个非常小的Scheme 程序的例子，你需要统一来正确推断s 表达式的类型）。

我试图理解这里SICP 中描述的统一算法

特别是，在“extend-if-possible”过程中，有一个检查（第一个用星号“*”标记的地方）检查右手“表达式”是否是一个已经绑定到某个变量的变量当前帧：

相关评论指出：

“在第一种情况下，如果我们尝试匹配的变量未绑定，但我们尝试匹配的值本身是一个（不同的）变量，则有必要检查该值是否已绑定，并且“

但是，我想不出实际上有必要这样做的情况。

我认为它在谈论的是您当前可能存在以下框架绑定的地方：

然后被要求“扩展IfPossible”一个从?z 到?y 的绑定。

有了“*”检查，当被要求用“?y”扩展“?z”时，我们看到“?y”已经绑定到4，然后递归地尝试将“?z”和“4”统一起来，这导致我们用“？z = 4”扩展框架。

如果没有检查，我们最终会用“?z = ?y”来扩展框架。但是在这两种情况下，只要 ?z 还没有绑定到其他东西，我就看不到问题所在。

注意，如果 ?z已经绑定到其他东西，那么代码不会到达标记为“*”的部分（我们已经递归到与 ?z 已经匹配的内容统一）。

仔细考虑之后，我意识到生成“最简单”的 MGU（最通用统一器）可能存在某种论据。例如，您可能想要一个具有最少数量的变量引用其他变量的 MGU……也就是说，我们宁愿生成替换 {?x = 4, ?y = 4} 而不是替换 {?x = ?y, ?y = 4}... 但我认为这个算法在任何情况下都不能保证这种行为，因为如果你要求它将 "(?x 4)" 与 "(?y ?y)" 统一起来，那么你会仍然以 {?x = ?y, ?y = 4} 结束。如果无法保证行为，为什么还要增加复杂性？

我的推理在这里都正确吗？如果不是，那么需要“*”检查才能生成正确的MGU 的反例是什么？

我正在阅读我得到的 AI 教科书，我已经来到了我的部分的最后一个作业问题：

“以您选择的任何语言实施第 69 页概述的统一算法。”

在第 69 页，您有以下统一算法的伪代码：

现在，我了解了统一的一般概念，但我完全不知道如何开始用 Java 或 C# 之类的语言来实现它。

我什至不确定方法签名会是什么样子。它需要什么类型的变量？我相当确定我需要返回列表来表示谓词演算结构，但这是一个猜测。

例如，当它说“E1 是一个变量”时，如果我将它传递给 Unify 方法，它怎么可能不是呢？我可以检查 null 但这会与“空列表”不同吗？

谁能帮助我或指出正确的方向以在 C# 或 Java 中实现 Unificaiton 算法？

为什么会这样：

这会产生堆栈溢出异常吗？

我在过去 5 天工作以了解统一算法在 Prolog 中的工作原理。现在，我想用Java实现这样的算法..

我认为也许最好的方法是使用诸如 Stacks 之类的数据结构来操作字符串并分解其部分。

说清楚：

假设用户输入是：a(X,c(d,X)) = a(2,c(d,Y))。

我已经将它作为一个字符串并将其拆分为两个字符串（Expression1 和 2）。现在，我怎么知道下一个字符是变量还是常量等等。我可以通过嵌套 if 来做到这一点，但在我看来这不是一个好的解决方案。我尝试使用继承，但问题仍然存在（如何我可以知道正在读取的字符类型吗？）

为什么这会失败L is [1,2,3,4]，这有效：L = [1,2,3]？

但是L is 1，L = 1两者的工作方式相同。

将 X,Y 与 (1,2), (1,-2), (-1,2), (-1,-2), (2,1), (2,-1) 统一的优雅方法是什么, (-2,1), (-2,-1)?

这样做似乎容易出错且乏味：

而且这种方式似乎太贵了：

统一的（实际）应用是什么？它在现实世界中实际使用在哪里？

我无法理解它的真正含义以及为什么它被视为人工智能的一部分。