Prolog and limitations of backtracking

Question

This is probably the most trivial implementation of a function that returns the length of a list in Prolog

count([], 0).
count([_|B], T) :- count(B, U), T is U + 1.

one thing about Prolog that I still cannot wrap my head around is the flexibility of using variables as parameters.

So for example I can run count([a, b, c], 3). and get true. I can also run count([a, b], X). and get an answer X = 2.. Oddly (at least for me) is that I can also run count(X, 3). and get at least one result, which looks something like X = [_G4337877, _G4337880, _G4337883] ; before the interpreter disappears into an infinite loop. I can even run something truly "flexible" like count(X, A). and get X = [], A = 0 ; X = [_G4369400], A = 1., which is obviously incomplete but somehow really nice.

Therefore my multifaceted question. Can I somehow explain to Prolog not to look beyond first result when executing count(X, 3).? Can I somehow make Prolog generate any number of solutions for count(X, A).? Is there a limitation of what kind of solutions I can generate? What is it about this specific predicate, that prevents me from generating all solutions for all possible kinds of queries?

Answer 1

This is probably the most trivial implementation

Depends from viewpoint: consider

count(L,C) :- length(L,C).

Shorter and functional. And this one also works for your use case.

edit

library CLP(FD) allows for

:- use_module(library(clpfd)).

count([], 0).
count([_|B], T) :- U #>= 0, T #= U + 1, count(B, U).

?- count(X,3).
X = [_G2327, _G2498, _G2669] ;
false.

(further) answering to comments

It was clearly sarcasm

No, sorry for giving this impression. It was an attempt to give you a synthetic answer to your question. Every details of the implementation of length/2 - indeed much longer than your code - have been carefully weighted to give us a general and efficient building block.

There must be some general concept

I would call (full) Prolog such general concept. From the very start, Prolog requires us to solve computational tasks describing relations among predicate arguments. Once we have described our relations, we can query our 'knowledge database', and Prolog attempts to enumerate all answers, in a specific order.

High level concepts like unification and depth first search (backtracking) are keys in this model.

Now, I think you're looking for second order constructs like var/1, that allow us to reason about our predicates. Such constructs cannot be written in (pure) Prolog, and a growing school of thinking requires to avoid them, because are rather difficult to use. So I posted an alternative using CLP(FD), that effectively shields us in some situation. In this question specific context, it actually give us a simple and elegant solution.

I am not trying to re-implement length

Well, I'm aware of this, but since count/2 aliases length/2, why not study the reference model ? ( see source on SWI-Prolog site )

Answer 2

The answer you get for the query count(X,3) is actually not odd at all. You are asking which lists have a length of 3. And you get a list with 3 elements. The infinite loop appears because the variables B and U in the first goal of your recursive rule are unbound. You don't have anything before that goal that could fail. So it is always possible to follow the recursion. In the version of CapelliC you have 2 goals in the second rule before the recursion that fail if the second argument is smaller than 1. Maybe it becomes clearer if you consider this slightly altered version:

:- use_module(library(clpfd)).

count([], 0).
count([_|B], T) :-
    T #> 0,
    U #= T - 1,
    count(B, U).

Your query

?- count(X,3).

will not match the first rule but the second one and continue recursively until the second argument is 0. At that point the first rule will match and yield the result:

X = [_A,_B,_C] ?

The head of the second rule will also match but its first goal will fail because T=0:

X = [_A,_B,_C] ? ;
no

In your above version however Prolog will try the recursive goal of the second rule because of the unbound variables B and U and hence loop infinitely.