Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Differences between pattern matching and unification?

I thought I understand how pattern matching like found in Scala and Haskell is different from unification found in Prolog but my misunderstands of Prolog is great. What is some simple problems solvable by one that cannot be solved by the other? Thank you

like image 406
Eli Schneider Avatar asked Dec 14 '10 17:12

Eli Schneider


2 Answers

Simple statement: pattern matching is one-way, unification is two-way. That is, in Prolog the right-hand side (the one being matched against) can include unbound variables. E.g., if you have two unbound variables X and Y, this will work fine:

X = Y, X = 5, %% Y = 5 now as well 

In Erlang (which uses pattern-matching with syntax close to Prolog), the line X = Y will produce an error: variable 'Y' is unbound. Note that X being unbound is fine: it is supposed to be pattern-matched.

This can be useful when you want to deal with partially-defined values. A very good example is difference lists.

This is also what allows use of Prolog predicate in multiple modes. E.g. in Scala/Haskell/Erlang, if you want to 1) find A ++ B, 2) solve the equation A ++ X == B, or 3) solve the equation X ++ A == B for given lists A and B, you need to write 3 separate functions; in Prolog, all these jobs (and more!) are done by one predicate.

like image 116
Alexey Romanov Avatar answered Nov 23 '22 16:11

Alexey Romanov


I think it is useful to formalize the concepts, instead of looking into a specific language. Matching and unification are fundamental concepts that are used in more contexts than pattern matching and prolog.

  • A term s matches t, iff there is a substitution phi such that phi(s) = t
  • A term s unifies with a term t, iff there is a substitution such that phi(s) = phi(t)

To give an example we inspect the terms s = f(Y,a) and t = f(a,X) where X,Y are variables and a is a constant. s does not match t, because we cannot universally quantify the constant a. However, there is a unifier for s and t: phi = {X\a, Y\a}

like image 41
hexhex Avatar answered Nov 23 '22 16:11

hexhex