Declarative interpretation of this program that says if an element belongs to a list

Question

From what I have understood the declarative paradigm indicate what is important to reach the solution and not how reach it but, being accustomed to think procedurally, I often make confusion...

So the solution is this one:

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

This is my declarative interpretation of this simple program:

1) X belong to the list if it is TRUE that X is the Head of this list (if the head element of the list unifies with the X element that I would know if is in the list)

2) If the first fact is not true (X don't unifies with the first list element) the program try to execute the second rule (and maybe here I have some interpretation problem). This rule say that: the head is true if the body of the rule is true)

The head of rule say that: X belongs to the TAIL of the list (I use an anonymous variable using the _ character to say that don't care of the first element of the list)

So this rule say that: It is TRUE that the X element belong to list without its head if it is TRUE that the X element belong to the tail of the list

Is it a correct declarative and logic interpretation of this program or I am missing something?

Answer 1

You're reading them as exclusive-or, but they're actually inclusive-or. Both 1) and 2) are correct, minus the connective "if the first fact is not true". It's not necessary for 1) to be false for 2) to hold. In other words, it can be true that X is both the head of the list and present in the tail of the list (for instance mymember(a, [a, b, a]).

Edit: responding to your comment.

There's a language barrier issue here, so let me try answering your question with yes and no.

Yes, that using ; produces another answer is evidence that Prolog was able to compute alternative answers. In one sense, ; triggers backtracking manually, but in another sense it is Prolog asking you if this is the answer you wanted, and then you're able to say "yes" or "no." When you say ; you're telling Prolog, in essence, "this isn't the right answer." But this is not the only way to trigger backtracking; in fact, most of the time you won't trigger it manually at all.

For instance, let's look at this:

even_member(X, L) :- member(X, L), 0 is X mod 2.

?- even_member(X, [1,5,17,23,4,19]).
X = 4 ;
false.

So here I defined a predicate that says, declaratively, X is an even_member of L if X is a member of L and X mod 2 = 0. When I used the predicate, we got the answer X = 4. We then pressed ; to say, this isn't the right answer, and Prolog said there are no more answers. But internally, member(X, L) backtracked 5 times before it found an element that satisfied the second part of the predicate--in other words, the statement 0 is X mod 2 tells Prolog that 1, 5, 17 and 23 are "wrong" the same way we do by pressing ; interactively. When we said we wanted another answer, we engaged the same machinery, so Prolog went back to member(X, L), found 19, and then found that 19 is not divisible by two and gave up.

Prolog backtracked six times, five of those times just to get the one answer. We only asked it to backtrack once, and it happened that it was the last possibility so it didn't backtrack again.

Answer 2

Let me try:

mymember(X, [X|_]).

X is a member of the list if it's the first element of the list

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

X is a member of the list if it's a member of the rest of the list.

Suppose I give you a stack of (paper) programmer resumes and say "see if there is a programmer who knows Prolog among these"

What do you do? You look at the top resume. If that programmer knows Prolog, you're done.

If not, then the only way there can be such a resume is if it's in the rest of the stack.

Answer 3

point 2) doesn't hold: Prolog will try each rule searching for a solution.

But it will follow a strictly specified order searching in your database, resulting in a depth first search of the solution space.

I would read

X is a member of a list if it is the first element (i.e. unify the head, clause 1), or is a member of the tail (clause 2).