regex之人工智能匹配，统一

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

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

我需要写一个函数来判断一个 对应于基本项的常数，例如 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

请您参考如下方法:

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