Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

 MostGeneralUnifier

Source Notebook

Unify expressions containing pattern variables

Contributed by: Nikolay Murzin

ResourceFunction["MostGeneralUnifier"][t1,t2,…]

returns an association representing a most general unifier of terms t1,t2,….

Details

ResourceFunction["MostGeneralUnifier"] finds a set of assignments of expressions to pattern variables (expressions with Pattern head), under substitution of which, provided terms become equal.
ResourceFunction["MostGeneralUnifier"] outputs an association with pattern variables as keys.
ResourceFunction["MostGeneralUnifier"] uses J. A. Robinson’s 1965 unification algorithm.

Examples

Basic Examples (1) 

Find the most general unifier for terms:

In[1]:=
ResourceFunction["MostGeneralUnifier"][f[x_], f[a]]
Out[1]=
In[2]:=
ResourceFunction["MostGeneralUnifier"][f[x_, y_], f[z_, g[x_]]]
Out[2]=

Scope (5) 

Unifying already equal terms returns an empty unifier:

In[3]:=
ResourceFunction["MostGeneralUnifier"][x, x, x]
Out[3]=

Trying to unify non-unifiable terms returns a Failure:

In[4]:=
ResourceFunction["MostGeneralUnifier"][x, y]
Out[4]=

Only a single unifier is found, but in general it's not unique (e.g. <|y_⧴x_|>is also valid here):

In[5]:=
ResourceFunction["MostGeneralUnifier"][x_, y_]
Out[5]=

MostGeneralUnifier holds its arguments:

In[6]:=
ResourceFunction["MostGeneralUnifier"][x_ + y_, 1 + Echo[2]]
Out[6]=

Unify heads:

In[7]:=
ResourceFunction["MostGeneralUnifier"][ f_[a_, a_][x_, y_], (1 + 1)[a, b]]
Out[7]=

Applications (1) 

Given multiple expressions, unifier makes them equal by substitution using ReplaceAll:

In[8]:=
ResourceFunction["MostGeneralUnifier"][f[x_, y_], f[z_, g[x_]], f[a, g[a]]]
Out[8]=
In[9]:=
HoldForm[f[x_, y_] === f[z_, g[x_]] === f[a, g[a]]] /. %
Out[9]=

Possible Issues (2) 

Different pattern variables with the same name are still considered distinct:

In[10]:=
ResourceFunction["MostGeneralUnifier"][f[x_, x_Integer], f[1, 2]]
Out[10]=
In[11]:=
ResourceFunction["MostGeneralUnifier"][f[x_, x__], f[1, 2]]
Out[11]=

PatternTest and Condition are treated verbatim:

In[12]:=
ResourceFunction["MostGeneralUnifier"][f[x_, x_?OddQ], f[1, 1]]
Out[12]=
In[13]:=
ResourceFunction["MostGeneralUnifier"][f[x_, x_?OddQ], f[1, 1?OddQ]]
Out[13]=
In[14]:=
ResourceFunction["MostGeneralUnifier"][f[x_, y_ /; OddQ[y]], f[1, 1]]
Out[14]=
In[15]:=
ResourceFunction["MostGeneralUnifier"][f[x_, y_ /; OddQ[y]], f[1, 2 /; OddQ[y]]]
Out[15]=

Version History

  • 1.0.0 – 22 April 2022

Source Metadata

  • Citation:
    • J.A. Robinson (Jan 1965). “A Machine-Oriented Logic Based on the Resolution Principle”. Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32

License Information