10
$\begingroup$

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

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

1 Answer 1

12
$\begingroup$

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}
*)
$\endgroup$
3
  • $\begingroup$ Thank you! Could you explain the difference between unification and matching for I think the difference isn't clear in my head. $\endgroup$ Apr 29, 2012 at 10:55
  • $\begingroup$ @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 $\endgroup$ Apr 29, 2012 at 13:37
  • $\begingroup$ @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. $\endgroup$
    – masterxilo
    Nov 5, 2017 at 14:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.