# Does Mathematica use first order or second order order unification?

When Mathematica is pattern-matching expressions, does it use first order or second order unification?

Just to clarify the difference between first order and second order unification:
In second order unification, it is possible to replace a pattern variable with a function: When the expression 3+3 or Plus[3,3] is matched with the pattern f, the matching succeeds and f is bound to Plus[#, #]& or Plus[3, #]&.

• Does first order unification include the constrain (** /; **) operator? Apr 28, 2012 at 6:51
• Just to clarify the difference between first order and second order unification. Apr 28, 2012 at 16:17
• In Second order unification, it is possible to replace a pattern variable with a function: Apr 28, 2012 at 16:19

I am not an expert in the field, but ...

According to Roman Maeder (and he is an expert):

The process of unification should be easy to understand for Mathematica users, since a weaker form of it —pattern matching— is the fundamental operating principle of Mathematica’s evaluator.

So, no unification is done in native Mma.

If you need it, Maeder presents in that 2 articles series a package with a modified evaluator that aims to bring second order unification to Mma.

Just for those to whom unification means only a physics Grail, should Mma have unification you could do things like:

f[x_,a] /. f[b,y_]-> {x,y}
(*
-> {b,a}
*)

• Thank you! Could you explain the difference between unification and matching for I think the difference isn't clear in my head. Apr 29, 2012 at 10:55
• @user1176201 I prefer not, because subtle things may be wrong in my explanation (as I said, I am not an expert). I suggest: 1) Read Maeder's articles linked above 2) post a question in cs.SE Apr 29, 2012 at 13:37
• @11Kilobytes In my opinion, the two should operate as follows: (matching) Match[a, b] == c iff b /. c == a (e.g. Match[{1,1}, {x_, x_}] == {Verbatim@x_ -> 1}). (unification) Unify[a, b] == c iff, for all x, MatchQ[x, a] && MatchQ[x, b] iff MatchQ[x, c]. (e.g. Unify[f[x_,a], f[b,y_]] == f[b,a]). Or you might want Unify to output a list of rules/dictionary that translates both a and b into the unified pattern c. Nov 5, 2017 at 14:30