什么是统一算法？
嗯，我知道这可能听起来有点奇怪，但是是的，我的问题是：“什么是统一算法”。 嗯，我正在尝试用 F# 开发一个像 Prolog 一样的应用程序。它应该获取一系列事实并在查询时处理它们。
有人建议我开始实施一个好的统一算法，但对此一无所知。
如果您想更深入地了解，请参阅此问题我想做的事。
非常感谢，圣诞快乐。
Well I know it might sound a bit strange but yes my question is: "What is a unification algorithm".
Well, I am trying to develop an application in F# to act like Prolog. It should take a series of facts and process them when making queries.
I was suggested to get started in implementing a good unification algorithm but did not have a clue about this.
Please refer to this question if you want to get a bit deeper to what I want to do.
Thank you very much and Merry Christmas.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
如果您有两个带有变量的表达式，则统一算法会尝试匹配这两个表达式，并为您分配变量以使这两个表达式相同。
例如，如果您在 F# 中表示表达式：
并且有两个如下所示的表达式：
那么统一算法应该给您一个赋值：
这意味着如果您替换两个表达式中所有出现的“x”变量，则两个替换将是相同的表达式。如果您有调用不同函数的表达式（例如
Call("foo", ...)和Call("bar", ...)），那么算法会告诉您你认为它们是不可统一的。维基百科上还有一些解释，如果你在互联网上搜索，你肯定会发现找到一些有用的描述（甚至可能是某种类似于 F# 的函数式语言的实现）。
If you have two expressions with variables, then unification algorithm tries to match the two expressions and gives you assignment for the variables to make the two expressions the same.
For example, if you represented expressions in F#:
And had two expressions like this:
Then the unification algorithm should give you an assignment:
This means that if you replace all occurrences of the "x" variable in the two expressions, the results of the two replacements will be the same expression. If you had expressions calling different functions (e.g.
Call("foo", ...)andCall("bar", ...)) then the algorithm will tell you that they are not unifiable.There is also some explanation in WikiPedia and if you search the internet, you'll surely find some useful description (and perhaps even an implementation in some functional language similar to F#).
我发现 Baader斯奈德的著作内容最为丰富。特别是，他们描述了几种统一算法（包括 Martelli 和 Montanari 使用并查找的近线性算法），并描述了句法统一和各种语义统一。
一旦统一，还需要回溯。 Kiselyov/Shan/Friedman 的 LogicT 框架 会在这里提供帮助。
I found Baader and Snyder's work to be most informative. In particular, they describe several unification algorithms (including Martelli and Montanari's near-linear algorithm using union-find), and describe both syntactic unification and various kinds of semantic unification.
Once you have unification, you'll also need backtracking. Kiselyov/Shan/Friedman's LogicT framework will help here.
显然，破坏性统一比纯函数统一更有效，但 F 锐度也低得多。如果您追求的是性能，那么您最终可能会以任何方式实现 WAM 的子集：
https: //en.wikipedia.org/wiki/Warren_Abstract_Machine
这可能会有所帮助：Andre Marien、Bart Demoen：WAM 中的统一新方案。
Obviously, destructive unification would be much more efficient than a pure functional one, but much less F-sharpish as well. If it's a performance you're after, probably you will end up implementing a subset of WAM any way:
https://en.wikipedia.org/wiki/Warren_Abstract_Machine
And probably this could help: Andre Marien, Bart Demoen: A new Scheme for Unification in WAM.