Explanation of a Prolog algorithm to append two lists together

This is an algorithm to append together two lists:

Domains
list= integer*

Predicates
nondeterm append(list, list, list)

Clauses
append([], List, List) :- !.
append([H|L1], List2, [H|L3]) :- append(L1, List2, L3).

Goal
append([9,2,3,4], [-10,-5,6,7,8], Ot).

The result is a list [9,2,3,4,-10,-5,6,7,8], and it's saved in "Ot".

My question is, how does this work?

What I understand is that in every recursive call, in the first list, you get only the tail as a list ( thus reducing its size by 1 until it's [] ), the second argument "List2" does not change at all, and the 3rd argument ... at first it's [], and after each recursive call you get its tail, but since it's [], it stays [].

So how come, suddenly, in 3rd argument ("Ot") we have the appended list ? Can someone explain this algorithm step by step ?

First, let's translate the clauses into something more understandable:

append([], List, List) :- !.

can be written

append([], List2, Result) :-
    Result = List2,
    !.

and

append([H|L1], List2, [H|L3]) :- append(L1, List2, L3).

can be written

append(List1, List2, Result) :-
    List1  = [Head1 | Tail1],
    Result = [HeadR | TailR],
    Head1  =  HeadR,
    append(Tail1, List2, TailR).

I hope this will already be clearer for you.

Then, step by step, the number indicates the clause used each time, and the resulting call is shown:

append([9, 2, 3, 4], [-10, -5, 6, 7, 8], Ot).
|
2
|
` append([2, 3, 4], [-10, -5, 6, 7, 8], Ot'). % and Ot = [9|Ot']
  |
  2
  |
  ` append([3, 4], [-10, -5, 6, 7, 8], Ot''). % and Ot' = [2|Ot'']
    |
    2
    |
    ` append([4], [-10, -5, 6, 7, 8], Ot'''). % and Ot'' = [3|Ot''']
      |
      2
      |
      ` append([], [-10, -5, 6, 7, 8], Ot''''). % and Ot''' = [4|Ot'''']
        |
        1
        |
        ` Ot'''' = [-10, -5, 6, 7, 8]

At this step all the values we're interested in are already defined. Notice how the head of the result is set before its tail is filled up by a subsequent (tail recursive) call to append, building the resulting list in the characteristic for Prolog top-down fashion (also known as "tail recursion modulo cons").

Let's follow the definitions to see what Ot is, at the final step:

Ot = [9|Ot']
        Ot' = [2|Ot'']
                 Ot'' = [3|Ot''']
                           Ot''' = [4|Ot'''']
                                      Ot'''' = [-10, -5, 6, 7, 8]
                           Ot''' = [4,          -10, -5, 6, 7, 8]
                 Ot'' = [3,         4,          -10, -5, 6, 7, 8]
        Ot' = [2,        3,         4,          -10, -5, 6, 7, 8]
Ot = [9,       2,        3,         4,          -10, -5, 6, 7, 8]

I hope you'll get something out of it.