Declarative interpretation of list inversion in Prolog

Question

I have some problem to join declarative reasoning...so I am here to ask you if my reasoning is correct or if there is something wrong or if I am missing something...

I have the following problem: Write a Prolog program that invert the element of a list

for example if I call something like:

myreverse([a,b,c,d,e],X). I have to obtain that X=[e,d,c,b,a]

I have the following solution:

naiverev([],[]).  
naiverev([H|T],R):- naiverev(T,RevT),
                    append(RevT,[H],R).

This is my interpretation:

I have a fact that say that the inverse of an empty list is an empty list.

If the first list it is not empty, the fact it is not true and the fact it is not match so move on to the next rule.

The rule say that: the program that prove that the list R is the inverse of the list [H|T]

I can read the logic implication from right to left in the following way:

IF it is TRUE that naivrev(T, RevT) AND append(RevT, [H], R) ---> naivrev([H|T],R) it is TRUE

So (in the body of the rule) I am assuming that the "function" naivrev(T,RevT) respond TRUE if RevT is the inverse of T, FALSE otherwise.

At the same time I am assuming* that **append(RevT,[H],R) respond TRUE if R is [H|RevT], FALSE otherwise.

Then, if both the parts of the rule body are TRUE, the program can infer that the HEAD is TRUE (in this case that R is the inverse of [H|T])

Is this reasoning good or I am missing something?

Answer 1

Like the last two times, you have again intermixed Prolog's engine of computation with the purely declarative reading. Whenever you say, procedurally "the rule is not matched so move on" or anything like that, you're invoking Prolog's algorithm to explain what's going on, not logic. But you're getting better, because the rest of your stuff is much closer than before.

Rule 1: the reverse of the empty list is the empty list. (Same as you have.)

Rule 2: the reverse of [H|T] is the reverse of T, called RevT, appended to the list [H].

What makes this work, of course, is that Prolog will try rule 1, when it doesn't match, it will try rule 2, and recursively build up the result (in a tremendously inefficient way, as you probably realize). But this "making it go" of checking rules and choosing between them and how that process is performed, is what Prolog adds to a declarative or logical statement.

Your reading of the logical implication is correct: If naiverev(T, RevT) is true and append(RevT, [H], R) is true, then naiverev([H|T], R) is true. This is just as @false explained in your previous question, so I would say you're definitely starting to get it. Your remarks about the body being true leading to the head being true are spot on.

So good job, it looks like you're getting it. :)