How to implement list concatenation in Prolog?

Question

I have the following compact example that take 3 parameter L1, L2, L3 and append L1 and L2 in L3 (verify that L3 is the concatenation of L1 and L2)

I have this code (that work well):

myappend([], L, L).
myappend([X|L1], L2, [X|L]) :- myappend(L1,L2,L).

The fact is the base case and say that when the first list is a void list, the concatenation of the first list with second list is just the second list.

Ok, this is clear...the rule is pretty clear for me (but not at all) I can think this rule as the predicate that testing whether the 1st, 2nd and 3rd argument has the relation of 1st and 2nd concatenates is the 3rd argument

Ok, I'm trying to express the previous code in an extended form in which I have the body of this rule that represents all the predicates that must be satisfied (have to be TRUE) before so that the head of the rule is itself satisfied.

I have some problem to implement this code in SWI Prolog, this is my code:

concatena([],L,L).

/* REGOLA */

concatena(L1,L2,L3) :- L1 = [_|T],          /* Always true: anonymous variable: "_" unifies everything */
               concatena(T,L2,L3).     /* Recursively call on the tail of L1 */
           [X|L1],
           [X|L3].

The fact is the base case (as the previous working example)

In my experiment the rule is different.

So that the head of the rule is verified, all the predicates in it's body have to be true...

I think that my idea is good until reaching the base case, in fact doing:

L1 = [_|T],         /* It is always true */
concatena(T,L2,L3)  /* Call recursively on a subproblem of the original problem, this problem have one less element

OK, so in this way, the base case is reached and so L3 is correctly unified with L2

In fact in the trace I have:

[trace] 3 ?- concatena([a,b],[c,d],L3).
   Call: (6) concatena([a, b], [c, d], _G1514) ? creep
   Call: (7) [a, b]=[_G1592|_G1593] ? creep
   Exit: (7) [a, b]=[a, b] ? creep
   Call: (7) concatena([b], [c, d], _G1514) ? creep
   Call: (8) [b]=[_G1595|_G1596] ? creep
   Exit: (8) [b]=[b] ? creep
   Call: (8) concatena([], [c, d], _G1514) ? creep
   Exit: (8) concatena([], [c, d], [c, d]) ? 

(This is the same thing that happens when I look to the trace of the original working example...so until here should be corrected)

The problem is when the program do backtracking, don't work !!!

In the trace in fact I have this (this is how end the previous incomplete trace):

Exit: (7) concatena([b], [c, d], [c, d]) ? creep
   Exit: (6) concatena([a, b], [c, d], [c, d]) ? creep
L3 = [c, d] 

Answer 1

I am not completely clear what you are trying to do here: rewrite the second part of the myappend rule so that all the arguments are simple variable terms? In that case, you can just rewrite the arguments of the original myappend with the = operator:

concatena(L1,L2,L3) :- L1=[X|T], L3=[X|L4], concatena(T,L2,L4).

The second part of your rule, as you've written it here,

[X|L1],
[X|L3].

isn't being counted as part of the rule since it follows the ., so there is no backtracking and nothing is happening as the recursion is unwinding.