Can someone please help explain this copy function works?

Question

copyList([], []).           % base case
copyList([H|T], [H|R]) :- 
    copyList(T, R).

I "sort of" understand how recursion works, but when I analysed this function, I got really confused. Can someone please explain, step-by-step what happens in this function and how it reaches the end using the example below:

?- copyList([1,2,3],L).

Can you give a query with no solution but which - unfortunately - does not terminate? — false, May 08 '15 at 14:14
Promise: 100-bounty to answer this question, here along. (You can answer your question, too!) — false, May 08 '15 at 14:47

score 2 · Accepted Answer · edited May 23 '17 at 12:04

To understand what happens, you must see Prolog as a theorem solver: when you give Prolog the query ?- copyList([1, 2, 3], L)., you're essentially asking Prolog to prove that copyList([1, 2, 3], L) is true.

Prolog will therefore try to prove it. At its disposal, it has two clauses:

```
copyList([], []).
```

copyList([H|T], [H|R]):- 
copyList(T, R).

As it is the first that it encounters, Prolog wil try to prove that copyList([1, 2, 3], L) is true by using the clause copyList([], []).

To do so, and since the clause has no body (nothing after :-), it would just have to unify the arguments of your query with the arguments of the clause (unify [1, 2, 3] with [] and L with []). While it is easy to unify L5 with [] (with the unification L5 = []), it is impossible to unify [1, 2, 3] with []. Therefore Prolog has failed to prove your query by using the first clause at its disposal. It must then try to use the second.

Once again it will unify the query arguments with the clause arguments to see if the clause is applicable: here it can do so, with the unifications H = 1, T = [2, 3], L = [H|R]. Now it has to see if the conditions listed after :- are respected, so it has to prove copyList(T, R). The exact same thing goes on twice, until it finds itself trying to prove copyList([], R). There, the first clause is applicable, and its job is over.

You can sum up the execution with a drawing as follows:

copyList([1, 2, 3], L).
|
| try to use clause number 1, doesn't unify with arguments.
| use clause number 2 and L = [1|R]
|
` copyList([2, 3], R).
 |
 | try to use clause number 1, doesn't unify with arguments.
 | use clause number 2 and R = [2|R2]
 |
 ` copyList([3], R2).
  |
  | try to use clause number 1, doesn't unify with arguments.
  | use clause number 2 and R2 = [3|R3]
  |
  ` copyList([], R3).
   |
   | use clause number 1 and R3 = []. One solution found
   | try to use clause number 2, doesn't unify with arguments.
   | No more possibilities to explore, execution over.

Now that the execution is over, we can see what the original L is by following the chain of unifications:

L = [1|R]
       R = [2|R2]
              R2 = [3|R3]
                      R3 = []
              R2 = [3]
       R = [2, 3]
L = [1, 2, 3]

Thanks to Will Ness for his original idea on how to explain the final value of a variable.

Thank you so much for your answer, but I have a quick question. From your diagrams above, I understand that L unifies to R. But at each stage, R becomes R2 and R2 becomes R3? Are the variable names for demonstration purposes or do the variable names change behind the scenes in Prolog? Do you get what I mean? — jellybean_232, May 08 '15 at 16:34
Also another question, regarding the last diagram, does L become the final copied list when it reaches to the point where R3 = []? If so, where are the values of the list stored? — jellybean_232, May 08 '15 at 16:41
Only the tail of `L` unifies with `R`. The name `R2` and `R3` are arbitrary: variables in Prolog are scoped to predicates, which means that during recursion it's each time "a new `R`" that is used. To denote that I used `R2` and `R3`. — m09, May 08 '15 at 16:41
Regarding your second question, consider that `L` is a list of `1` and a pointer to `R`. Then when `R` changes from a completely free variable to a list made of `2` and a pointer to `R2`, it's reflected on `L` without any additional work, because it was a pointer to `R` that `L` stored, not a copy. Was it clear? — m09, May 08 '15 at 16:43

score 1 · Answer 2 · answered May 12 '15 at 00:20

1

While your specific question was already answered, few remarks.

First, you could just as well call ?- copyList(L,[1,2,3]). or ?- copyList([1,2,3],[1,2|Z]). etc. What's important is that both lists can be of equal length, and their elements at the corresponding positions can be equal (be unified), because the meaning of the predicate is that its two argument lists are the same - i.e. of the same length, and having the same elements.

For example, the first condition can be violated with the call

?- copyList(X, [A|X]).

because it says that the 2nd argument is one element longer than the first. Of course such solution can not be, but the query will never terminate, because the first clause won't ever match and the second always will.

answered May 12 '15 at 00:20

Will Ness

70,110
9
98
181

Note that in many implementations, non-termination is preserved, even when adding the redundant goal `X = Y`: Thus `..., X = Y, copyList(X, Y).` is just as bad or good (although maybe a bit more efficient) than `..., copyList(X,Y).` alone. – false May 12 '15 at 17:04
Only `unify_with_occurs_check(X, Y), copyList(X, Y)` will help to fail — or a system with built-in occurs check. – false May 12 '15 at 17:30
... and some loop checking, indeed. At least it is trivial to prove universal and existential non-termination. – false May 12 '15 at 20:40
if the loop was detected, that would signal the non-termination in advance; I see. although it seems unusual anybody would make a call like that, intentionally. maybe the simple and practical, "non-theoretical" way to ensure a system's responsiveness is just with preemptive multitasking - putting timeouts here and there and letting a user to decide whether to continue - if it's so hard to do right. i.e. https://www.cpp.edu/~jrfisher/www/prolog_tutorial/3_3.html says general loop detection is impossible... – Will Ness May 12 '15 at 22:05
1

Of course detecting all loops is impossible, but - as you indicate you can start with timeouts + some provers. It's not perfect, but much faster than no checking at all. – false May 12 '15 at 22:09
There are more bounties! – false May 13 '15 at 00:11

Can someone please help explain this copy function works?

2 Answers2