regex - 人工智能匹配，统一

Question

尝试实现一种有限形式的匹配统一。

尝试匹配两个公式匹配如果我们能找到替代出现在公式中的变量使得两者在句法上是等价。

我需要写一个函数来判断一个对应于基本项的常数，例如 Brother(George) 和 a对应于量化公式的模式，例如 Brother(x) 匹配。如果他们确实匹配函数返回一组称为绑定(bind)的替换将变量映射到术语。如果一个常量匹配另一个常量是平等的。未绑定(bind)变量(当前没有绑定(bind))匹配任何公式。如果常量和变量绑定(bind)的值是相等的。

例子:

match( Loves(Dog(Fred), Fred)

Loves(x,y))

is true with x = Dog(Fred) and y = Fred

另一个

match( Loves(Dog(Fred), Fred)

Loves(x,x)

fails

Answer 1

MGU 的概念，即 Most General Unifiers 似乎在这里很有用。解决方法如下图所示。
让我们有一个名为 mgu 的初始空集和另一个空集 E。

mgu = {}
G = match(Loves(Dog(Fred),Fred),Loves(x,y))
E = {Loves(Dog(Fred),Fred),Loves(x,y)}


mgu = {Fred|y}             // Replace Fred by y, variables to be replaced first.
G = match(Loves(Dog(y),y),Loves(x,y))
E = {Loves(Dog(y),y),Loves(x,y)}


mgu = {Fred|y,Dog(y)|x}    // Replace Dog(y) by x
G = match(Loves(x,y),Loves(x,y))  
E = {Loves(x,y)}           // E becomes a singleton set here, we stop here.
                           // No more substitutions are possible at this stage.

ma​​tch() 返回 True 如果 E 成为单例集且没有更多的替换是可能的，否则返回 False>。 mgu 可以作为所需的替换集返回。

G = True
mgu = {Fred|y,Dog(y)|x}

另一个例子可以说明如下。

mgu = {}
G = match(Loves(Dog(Fred),Fred),Loves(x,x))
E = {Loves(Dog(Fred),Fred),Loves(x,x)}


mgu = {Fred|x}             // Replace Fred by x.
G = match(Loves(Dog(x),x),Loves(x,x))
E = {Loves(Dog(x),x),Loves(x,x)}


mgu = {Fred|x,Dog(x)|y}       // Replace Dog(x) by y
G = match(Loves(y,x),Loves(x,x))  
E = {Loves(y,x),Loves(x,x)}   // E does not becomes a singleton set here.
                              // But no more substitutions are 
                              // possible at this stage.

因此，

G = False