Prolog termination domain: How can I know which questions will return a finite number of answers?

Question

Let's say I have a prolog program to concatenate lists like this:

concat([],X,X).
concat([Head|Tail],X,[Head|R]) :- concat(Tail,X,R).

How can I know which questions will return a finite number of answers? For example, asking

concat(X,Y,[1,2,3,4]).

Will return the finite solution set:

X = [],
Y = [1, 2, 3, 4] ;
X = [1],
Y = [2, 3, 4] ;
X = [1, 2],
Y = [3, 4] ;
X = [1, 2, 3],
Y = [4] ;
X = [1, 2, 3, 4],
Y = [] ;
false.

while making the question

concat(X,[2,3],Z).

will return an infinite set of solutions:

X = [],
Z = [1, 2, 3] ;
X = [_G24],
Z = [_G24, 1, 2, 3] ;
X = [_G24, _G30],
Z = [_G24, _G30, 1, 2, 3] ;
X = [_G24, _G30, _G36],
Z = [_G24, _G30, _G36, 1, 2, 3] ;
X = [_G24, _G30, _G36, _G42],
Z = [_G24, _G30, _G36, _G42, 1, 2, 3] ;
X = [_G24, _G30, _G36, _G42, _G48],
Z = [_G24, _G30, _G36, _G42, _G48, 1, 2, 3] ;
X = [_G24, _G30, _G36, _G42, _G48, _G54],
Z = [_G24, _G30, _G36, _G42, _G48, _G54, 1, 2, 3]

and so on (basically, every possible list ending with [1,2,3].

so how can I reason which questions will end or not on a logic program?

Answer 1

You are asking how to determine the termination and non-termination properties of a logic program — here meaning a pure, monotonic Prolog program. There is good news: Yes, there are a lot of techniques how to find out those properties accompanied with a lot of useful notions.

But before going into any detail, just keep in mind that your question cannot be answered for all queries. That is, there are some queries where we cannot confirm termination any better than by actually executing the query. But don't let you be intimidated by fearsome words like undecidability and the like. They are here to shy away the angstful. Just like old sea-maps display horrifying monsters like the red sea-snake. There are problems at sea no doubt: weather, malnutrition, navigation, mutiny, piracy, pestilences, dead water, ice bergs, mines ... you name it. The risk of encountering sea-monsters is manageable, though.

Nowadays, we have our own sea-monsters that have shied away many clever minds from attacking interesting problems. Undecidability of termination used to be one such for many decades. Things have become much better in the last two decades. So: fear not!

The first to consider is the actual relation your logic program is intended to describe. You don't even need a concrete program to answer this question. Just imagine the relation. First, ask how many solutions there are. If there are finitely many, you are done for this part, as there is no inherent reason your program cannot terminate. (In your example, the general relation contains infinitely many solutions: It suffices to see that there are infinitely many lengths of the lists in the 3rd argument.)

In case there are infinitely many, try to find subsets of the query that are finite. (In your example, if the 3rd argument is ground, there are only finitely many solutions. Idem, if the 1st argument and the 2nd are ground. However, note that this is not the case, if only the 1st is ground!)

Another orthogonal direction is to consider the way how solutions are represented as answers in Prolog. Some infinite sets of solutions can be represented compactly with finitely many answers. In the context of constraints, this becomes particularly interesting. (In your example, consider concatenating [] and [X]. Here, there are infinitely many solutions for the 3rd argument, but they are all represented by a single answer substitution A3 = [X].)

With above considerations we have a rough estimate of what we can expect of a logic program: If the set of solutions for a query can only be represented by an infinite set of answers, the program must not terminate. If, however, the solutions can be represented by finitely many answers, the concrete program might terminate. Alas, to guarantee that a program actually does terminate, we need to dig further and look at the actual program.

If you now look at your program, you might find some differences to the intended relation. In your example the query concat([],[],[]) fails, while it should succeed. But also concat([],nonlist,L) succeeds. The former is definitely a typo, the latter is a generalization which is often considered as acceptable.

To understand the termination property of a concrete query, consider the goal Query, false. In this manner you can concentrate on the relevant property, id est, termination and ignore irrelevant properties like the concrete solutions found.

You might now consult a concrete program to determine the termination properties of your program. Consider cTI, which does infer both the termination and non-termination property of your program. In this manner it is possible to determine whether or not the inferred properties are optimal.

Another way is to use failure-slices to determine non-terminating fragments of your program. For more, see answers like this one.

Answer 2

I usually use these rules:

1. Each fresh predicate must be tested with different parameters directions/types. In your case the directions are (+, +, -), (+, -, +), (-, +, +), (-, -, +), (-, +, -), (+, -, -), (-, -, -). "-" means unbound variable, + - a variable with some members already bound. The case of '+' will always work if the case with '-' in the same place works. So, actually you can perform only 4 tests. I don't think any predicate will work in (-, -, ...) mode. Just make a testing from an interpreter command line, you do not need write a unit test yet.

2. If some results you find inappropriate redesign your predicate. For example

   con_fin([],X,X).
   con_fin(A,X,[Head|R]) :- nonvar(A), A=[Head|Tail], con_fin(Tail,X,R).
   

   will always return a finite set of answers. If you can't write a perfect 2-lines predicate at one stroke yet (the perfect predicate is that predicate which effectively works with all possible directions) write several lines for different modes/types, let type checking like var, nonvar, X = [_|_], is_set/1 etc. be your friends.

3. After that testing make a clear comment. You should always mention possible types and directions of arguments and define a predicate as det, semidet or nondet for some modes. I think your problem is not infinite solution for the "(-, +, -) nondet" case but that a user is not warned about possible infinite recursion.

   B=[1, 2], con(A, B, C), A=[0].
   

   just compare with the following case

   B=[1,2], con(A, B, C), proper_length(C, 4), !.
   

   Not effective but correct and deterministic.

4. Add mode and type checking. Throw exception for improper usage. ISO standard have predefined exceptions for some cases (http://www.deransart.fr/prolog/exceptions.html), good design should follow its recommendations.

5. Write a unit test which covers all possible usage (it usually doesn't take more than 15 minutes but you will save much more in the future).

6. Enjoy your life

7. If you found better solution (Eureka!) just rewrite the predicate, the unit test now is your best friend.

Usually, Prolog allows write very compact and smart code but demands more work compare to other languages. It is possible improve one small line during years like a haiku. But actual nature of the language is try->test->use->redesign principle, because it is very easy make experiments in Prolog.

Answer 3

Your program concat is not entirely correct it should be:

concat([],X,X).
concat([Head|Tail],X,[Head|R]) :- concat(Tail,X,R).

Note the | in [Head|R] of the second line. You can not analyze whether it would stop as @DanielLyons said. The thing you can do is trim the solutions tree using "!".