algorithm - 什么是统一算法？

Question

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

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

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

非常感谢你，圣诞快乐。

score 5 · Accepted Answer

如果您有两个带有变量的表达式，则统一算法会尝试匹配这两个表达式并为您分配变量以使两个表达式相同。

例如，如果您在 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# 的函数式语言的实现）。

score 2 · Accepted Answer

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

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

score 1 · Accepted Answer

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

这可能会有所帮助：

3 回答 3