prologfailure-slicenon-termination

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


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?


Solution

  • 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.