什么是统一算法？

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#的函数语言中实现).