Search code examples
prologunificationprolog-anonymous-variable

Prolog and List Unification


I'm trying to further my understanding of Prolog, and how it handles unification. In this case, how it handles unification with lists.

This is my knowledgebase;

member(X, [X|_]).
member(X, [_|T]):- member(X, T).

If I'm understanding the process correctly. If member(X, [X|_]) is not true, then it moves into the recursive rule, and if X is in list T, then [_|T] is unified with T.

So what happens to the anonymous variable in my recursive predicate? Does it get discarded? I'm having difficulty understanding the exact unification process with lists, as [_|T] is two variables, rather than one. I'm just trying to figure out how the unification process works precisely with lists.


Solution

  • Assume that _ is Y

    member(X, [Y|T]):- member(X, T).
    

    Then this is True regardless Y. Now you are "returning" member(X, T). In other words, you are discarding Y and "returning" member(X, T).

    _ means, whatever it is, ignore that variable.

    The _ is just like any other variable, except that each one you see is treated as a different variable and Prolog won't show you what it unifies with. There's no special behavior there; if it confuses you about the behavior, just invent a completely new variable and put it in there to see what it does.

    In your case, your function check if a given element exists on a list, so, you take first element of the list, check if is equal, if not, you discard that element and moves on.