# 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[3], the matching succeeds and f is bound to Plus[#, #]& or Plus[3, #]&.

-
Does first order unification include the constrain (** /; **) operator? –  belisarius Apr 28 '12 at 6:51
Just to clarify the difference between first order and second order unification. –  user1176201 Apr 28 '12 at 16:17
In Second order unification, it is possible to replace a pattern variable with a function: –  user1176201 Apr 28 '12 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. –  user1176201 Apr 29 '12 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 –  belisarius Apr 29 '12 at 13:37