问题标签 [unification]

我正在使用Franz Baader 和 Tobias Nipkow 的“Term Rewriting and All That”（WoldCat ）在 F# 中编写一个统一算法，用于AST转换。对于第 4.6 节“通过变换统一”，示例中包含了太多的数学理论，并且没有我希望的那么清晰。

有人可以给出或指出使用转换的更简单的例子吗：

删除、分解、定向、消除。

我正在按照Mark Jones和Oleg Kiselyov的教程实现 Hindley-Milner 类型推理算法。这两个都有一个“应用绑定”操作，其类型大致为

它将tyvar -> ty绑定应用于TyEnv给定的Type. 我发现在我的代码中忘记调用是一个常见错误applyBindings，而且我没有从 Haskell 的类型系统中得到任何帮助，因为ty它与applyBindings tyenv ty. 我正在寻找一种在类型系统中强制执行以下不变量的方法：

在进行类型推断时，必须在返回“最终”结果之前应用绑定

在为单态对象语言进行类型推断时，有一种自然的方式来强制执行这一点，正如在 wren ng thornton 的unification-fd 包中实现的那样：我们为 s 定义了两种数据类型Type：

并给出applyBindings类型

（这个函数实际上freeze . applyBindings在unification-fd中）。这强制了我们的不变量——如果我们忘记了applyBindings，那么我们将得到一个类型错误。

这是我正在寻找的解决方案，但对于具有多态性的对象语言。就目前而言，上述方法并不适用，因为我们的对象语言类型可能具有类型变量——事实上，如果在应用绑定后有自由变量，我们不想 return Nothing，但我们想概括一下这些变量。

有没有按照我描述的思路的解决方案，即提供applyBindings不同类型的解决方案const id？真正的编译器是否使用与 Mark 和 Oleg 的教程相同的双关语（在统一变量和对象语言类型变量之间）？

我正在努力完成本页底部的练习，但我发现自己对第 3 点完全感到困惑。

我们得到以下旅游信息知识库：

很容易确定是否可以在两个城市之间旅行。我只是这样做了：

但是，当我必须用变量实际统一路径时，我完全糊涂了！

我写了这个：

并叫travel(valmont, losAngeles,X).

除了最后的匿名变量之外，在跟踪过程中有一个点会显示正确的路径：

travel(valmont, metz, connected(metz, paris, connected(paris, losAngeles, _17)))

但我实际上不知道如何将它与变量统一起来X！

我实在是想不通这个。谁能给我一个提示只是为了把我推向正确的方向？我只是缺少一个终止条件还是什么？

编辑：

我现在有：

但它会像这样卡住：

我玩过它，但我无法让它来构建整个go(a,b,go(b,c))等等......

我想做的是，测试某个表达式是否与 Oz 中的另一个表达式统一。

例如，我想做这样的事情：

that can return truewhen Acan be unity to Band false else.

我想用它来进行特定的模式匹配（即按特定模式过滤列表）。

谢谢您的回答。

我正在尝试实现“自下而上”类型推理算法，该算法可在Generalizing Hindley-Milner Type Inference Algorithms中找到

第 6 页解释了隐式约束是如何产生的

t1应该是类型方案的一个实例，它是通过t2关于单态类型变量集的类型泛化获得的M

然而，在第 9 页，在解释如何对隐式约束应用替换时，有人告诉我对这组单态类型变量应用替换。问题是，如果我有替换[t1 := t2 -> t3]，则M不再是一组类型变量。

我在这里有什么误解？

谁能告诉我如何访问序言中列表的特定成员？例如，我需要访问传递给规则的列表的第三个或第四个元素？

我需要一个统一算法来处理以下情况。

我的表达式树中的每个节点都有一个列表（关联）或一组（关联和交换）子级。我想获得与特定模式的所有可能匹配。

这是一个例子。假设我们正在处理矩阵，因此 + 是可交换的， * 是不可交换的

表达：A + B*C*D + E

或者：Add(A, Mul(B, C, D), E)

图案：X + Y*Z

我看到两场比赛

问题：是否有任何标准算法可以处理这个问题？

可能重复：
Prolog- 将英语翻译成 C

我们基本上有一个作业，我们得到一个表示英语符号的列表，例如 [add,3,to,5]，我们需要接受它并让它在 C 中输出相应的符号。

我们的数量是有限的。我们也可以将两个这样的列表组合成一个更长的列表

但是这些较长的列表总是由较短的列表组成，其中有一定数量的。这就是我卡住的地方。我希望能够使用模式匹配，但我不完全确定 prolog 中的语法如何

所以会有一种情况用于加法，一种用于减法，一种用于乘法等。基本上我想在列表中搜索短语“将 I 加到 J”并将该短语与 (I + J) 统一。或者在列表中搜索“除以 J 后取 I 的余数”并将其与 (I '%' J) 统一。但是所有的短语都是不同的长度，即使我知道我想做什么以及如何去做，我似乎无法在序言中得到它。

有点更新，但我忘了提及我现在拥有的文件中所有基本规则的列表，就像这样

等等等等。问题是组合列表。例如，我们拥有的列表可能是 [add,I,to,J,',',then,subtract,H]，它必须是 I+JH。定义了各个基本规则（I+J 和 XH），但我必须能够匹配更长列表中的每个部分。

在 Haskell 中，我Subst a用一个构造函数定义了一个多态数据类型，S :: [(String, a)] -> Subst a如下所示：

我想定义一个函数get::String -> Subst a -> Maybe a，它接受一个变量名和一个替换，并返回该变量必须被替换的值。如果未在变量上定义替换，则函数应返回 Nothing。

我尝试了以下方法：

但是我遇到了错误。任何想法为什么？

我写了一个 Haskell 函数，如下所示：

像这样的数据类型data Subst a = S [(String,a)]

我已经声明subst了 assubst :: Subst a -> a -> a和varsas vars :: a -> [String]。当我运行它时，我得到一个类型错误。任何想法为什么？