Does Mathematica use first order or second order order unification?

Question

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, #]&.

Answer 1

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}
*)