Understanding Prolog Lists

In Prolog, you need to think of predicates not as functions as you would normally in other languages. Predicates describe relationships which might include arguments that help define that relationship.

For example, let's take this simple case:

same_term(X, X).

This is a predicate that defines a relationship between two arguments. Through unification it is saying that the first and second arguments are the same if they are unified (and that definition is up to us, the writers of the predicate). Thus, same_term(a, a) will succeed, same_term(a, b) will fail, and same_term(a, X) will succeed with X = a.

You could also write this in a more explicit form:

same_term(X, Y) :-
    X = Y.  % X and Y are the same if they are unified

Now let's look at your example, val_and_remainder/3. First, what does it mean?

val_and_remainder(X, List, Rest)

This means that X is an element of List and Rest is a list consisting of all of the rest of the elements (without X). (NOTE: You didn't explain this meaning right off, but I'm determining this meaning from the implementation your example.)

Now we can write out to describe the rules. First, a simple base case:

val_and_remainder(X,[X|Xs],Xs).

This says that:

Xs is the remainder of list [X|Xs] without X.

This statement should be pretty obvious by the definition of the [X|Xs] syntax for a list in Prolog. You need all of these arguments because the third argument Xs must unify with the tail (rest) of list [X|Xs], which is then also Xs (variables of the same name are, by definition, unified). As before, you could write this out in more detail as:

val_and_remainder(X, [H|T], R) :-
    X = H,
    R = T.

But the short form is actually more clear.

Now the recursive clause says:

val_and_remainder(X, [Y|Ys], [Y|R]) :- 
    val_and_remainder(X, Ys, R).

So this means:

[Y|R] is the remainder of list [Y|Ys] without X if R is the remainder of list Ys without the element X.

You need to think about that rule to convince yourself that it is logically true. The Y is the same in second and third arguments because they are referring to the same element, so they must unify.

So these two predicate clauses form two rules that cover both cases. The first case is the simple case where X is the first element of the list. The second case is a recursive definition for when X is not the first element.

When you make a query, such as val_and_remainder(2, [1,2,3], R). Prolog looks to see if it can unify the term val_and_remainder(2, [1,2,3], R) with a fact or the head of one of your predicate clauses. It fails in its attempt to unify with val_and_remainder(X,[X|Xs],Xs) because it would need to unify X with 2, which means it would need to unify [1,2,3] with [2|Xs] which fails since the first element of [1,2,3] is 1, but the first element of [2|Xs] is 2.

So Prolog moves on and successfully unifies val_and_remainder(2, [1,2,3], R) with val_and_remainder(X,[Y|Ys],[Y|R]) by unifying X with 2, Y with 1, Ys with [2,3], and R with [Y|R] (NOTE, this is important, the R variable in your call is NOT the same as the R variable in the predicate definition, so we should name this R1 to avoid that confusion). We'll name your R as R1 and say that R1 is unified with [Y|R].

When the body of the second clause is executed, it calls val_and_remainder(X,Ys,R). or, in other words, val_and_remainder(2, [2,3], R). This will unify now with the first clause and give you R = [3]. When you unwind all of that, you get, R1 = [Y|[3]], and recalling that Y was bound to 1, the result is R1 = [1,3].

Stepwise reproduction of Prolog's mechanism often leads to more confusion than it helps. You probably have notions like "returning" meaning something very specific—more appropriate to imperative languages.

Here are different approaches you can always use:

Ask the most general query

... and let Prolog explain you what the relation is about.

| ?- val_and_remainder(X, Xs, Ys).
     Xs = [X|Ys]
  ;  Xs = [_A,X|_B],
     Ys = [_A|_B]
  ;  Xs = [_A,_B,X|_C],
     Ys = [_A,_B|_C]
  ;  Xs = [_A,_B,_C,X|_D],
     Ys = [_A,_B,_C|_D]
  ;  Xs = [_A,_B,_C,_D,X|_E],
     Ys = [_A,_B,_C,_D|_E]
  ; ...

So Xs and Ys share a common list prefix, Xs has thereafter an X, followed by a common rest. This query would continue producing further answers. Sometimes, you want to see all answers, then you have to be more specific. But don't be too specific:

| ?- Xs = [_,_,_,_], val_and_remainder(X, Xs, Ys).
     Xs = [X,_A,_B,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,X,_B,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,_B,X,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,_B,_C,X],
     Ys = [_A,_B,_C]
  ;  false.

So here we got all possible answers for a four-element list. All of them.

Stick to ground goals when going through specific inferences

So instead of val_and_remainder(2, [1,2,3], R). (which obviously got your head spinning) rather consider val_and_remainder(2, [1,2,3], [1,3]). and then val_and_remainder(2, [2,3],[3]). From this side it should be obvious.

Read Prolog rules right-to-left

See Prolog rules as production rules. Thus, whenever everything holds on the right-hand side of a rule, you can conclude what is on the left. Thus, the :- is an early 1970s' representation of a ←

Later on, you may want to ponder more complex questions, too. Like

Functional dependencies

Does the first and second argument uniquely determine the last one? Does X, Xs → Ys hold?

Here is a sample query that asks for Ys and Ys2 being different for the same X and Xs.

| ?- val_and_remainder(X, Xs, Ys), val_and_remainder(X, Xs, Ys2), dif(Ys,Ys2).
     Xs = [X,_A,X|_B],
     Ys = [_A,X|_B],
     Ys2 = [X,_A|_B],
     dif([_A,X|_B],[X,_A|_B])
  ;  ...

So apparently, there are different values for Ys for a given X and Xs. Here is a concrete instance:

| ?- val_and_remainder(x, [x,a,x], Ys).
     Ys = [a,x]
  ;  Ys = [x,a]
  ;  false.

There is no classical returning here. It does not return once but twice. It's more of a yield.

Yet, there is in fact a functional dependency between the arguments! Can you find it? And can you Prolog-wise prove it (as much as Prolog can do a proof, indeed).

From comment:

How the result of R is correct, because if you look at my run-though of a program call, the value of Xs isn't [1,3], which is what it eventually outputs; it is instead [3] which unifies to R (clearly I am missing something along the way, but I am unsure what that is).

This is correct:

% Initial call
val_and_remainder(2, [1,2,3], R).

val_and_remainder(2, [1|[2,3]], [1|R]) :- val_and_remainder(2, [2,3], R).

% Hits base case
val_and_remainder(2, [2|[3]], [3]).

however Prolog is not like other programming languages where you enter with input and exit with output at a return statement. In Prolog you move forward through the predicate statements unifying and continuing with predicates that are true, and upon backtracking also unifying the unbound variables. (That is not technically correct but it is easier to understand for some if you think of it that way.)

You did not take into consideration the the unbound variables that are now bound upon backtracking.

When you hit the base case Xs was bound to [3],

but when you backtrack you have look at

val_and_remainder(2, [1|[2,3]], [1|R])

and in particular [1|R] for the third parameter.

Since Xs was unified with R in the call to the base case, i.e.

val_and_remainder(X,[X|Xs],Xs).

R now has [3].

Now the third parameter position in

val_and_remainder(2, [1|[2,3]], [1|R])

is [1|R] which is [1|[3]] which as syntactic sugar is [1,3] and not just [3].

Now when the query

val_and_remainder(2, [1,2,3], R).

was run, the third parameter of the query R was unified with the third parameter of the predicate

val_and_remainder(X,[Y|Ys],[Y|R])

so R was unified with [Y|R] which unpon backtracking is [1,3] and thus the value bound to the query variable R is [1,3]