什么是合一算法？

Question

好吧，我知道这听起来可能有点奇怪，但是是的，我的问题是：“什么是统一算法”。好吧，我正在尝试用 F# 开发一个应用程序，使其像 Prolog 一样运行。它应该在查询时获取一系列事实并处理它们。

有人建议我开始实施一个好的统一算法，但对此一无所知。

如果你想更深入地了解我想做的事情，请参考这个问题。

非常感谢你，圣诞快乐。

Answer 1

如果你有两个带有变量的表达式，那么统一算法会尝试匹配这两个表达式并为你赋值变量以使两个表达式相同。

例如，如果您在 F# 中表示表达式：

type Expr = 
  | Var of string              // Represents a variable
  | Call of string * Expr list // Call named function with arguments

还有两个这样的表情：

Call("foo", [ Var("x"),                 Call("bar", []) ])
Call("foo", [ Call("woo", [ Var("z") ], Call("bar", []) ])

那么统一算法应该给你一个作业：

"x" -> Call("woo", [ Var("z") ]

这意味着如果您替换两个表达式中所有出现的“x”变量，则两个替换的结果将是相同的表达式。如果你有调用不同函数的表达式（例如

Call("foo", ...)

和

Call("bar", ...)

）那么算法会告诉你它们是不可统一的。

WikiPedia 中也有一些解释，如果您在互联网上搜索，您肯定会找到一些有用的描述（甚至可能是类似于 F# 的某种函数式语言的实现）。

Answer 2

我发现 Baader 和 Snyder 的作品信息量最大。特别是，他们描述了几种统一算法（包括 Martelli 和 Montanari 的使用 union-find 的近线性算法），并描述了句法统一和各种语义统一。

统一后，还需要回溯。 Kiselyov/Shan/Friedman 的 LogicT 框架将在这里提供帮助。

Answer 3

显然，破坏性统一比纯功能统一更有效，但 F-sharpish 也少得多。如果这是您追求的性能，您可能最终会以任何方式实现 WAM 的一个子集：