什么是统一算法？答案

【问题标题】：What is a unification algorithm?什么是统一算法？
【发布时间】：2011-05-27 12:41:47
【问题描述】：

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

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

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

非常感谢，圣诞快乐。

【问题讨论】：

【解决方案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", ...)），那么算法会告诉你它们是不可统一的。

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

【讨论】：

看来你是我的 f# 大师 Petricek 先生...再次感谢 :) 啊，圣诞快乐。
托马斯给出了很好的解释。正如他所指出的，可以在互联网上找到好的资源。较老的人工智能来自 Prolog 鼎盛时期 c.1986-1992 的书籍有时也有很好的解释和可以适应 F# 的 LISP 代码。

【解决方案2】：

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

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

【讨论】：

【解决方案3】：

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

这可能会有所帮助：

【讨论】：