The essence of the append infinite loop thread

Ok. I had no memory of this behavior of Prolog whatsoever from learning Prolog long ago.

?- length(Ls, N).

literally generates all solutions Ls = , N = 0; Ls = [_], N = 1 forever.
This is to my understanding because it stands for all possible lists that might exist in
the universe.

Thats really cool, and completely unexpected and a bit magical.
Now that append infinite unification makes much more sense.
I suppose Prolog’s depth first search keeps going down some infinite branch
of the tree of possible values.

Yes, and this is why it is so easy to let it run away. As in this example of a class of mistakes I have done many times:

?- length(L, N), N =< 3.


written with the intent of “I want lists up to three elements long”.

Do you have any insight into why this works ( obvious list length )

list_length([], 0).
list_length([_ | Tail], Length) :-
list_length(Tail, TailLength),
Length is TailLength + 1.


But the following runs into a loop of some sort? I was trying to do this to get Tau Prolog to draw that nice tree visualization of list length…

leng([], 0, K) :- K < 4.
leng([_|T], N, J) :- JJ is J + 1, leng(T, M, JJ), N is M + 1.

list_length([], 0).
list_length([_ | Tail], Length) :-
list_length(Tail, TailLength),
Length is TailLength + 1.


So the recursive call doesn’t need to be necessarily the last. It’s enough to make sure that recursion finds an appropriate termination condition at some point? I always stuck to that rule, but it’s not mandatory then…

I was trying to put an upper bound to give Tau Prolog a termination condition.

But I think I figured out the issue. Both the recursions need a guard, since the
first clause is not the only one that can match.
We need the second J < 4 which I did not have earlier

leng([], 0, K) :- K < 4.
leng([_|T], N, J) :- J < 4, JJ is J + 1, leng(T, M, JJ), N is M + 1.


Ok. Thanks @asanay . Very kind of you Congrats for your progress

This is of course possible but not sure if it is necessary. The easy way to get lists up to 3 long is to write instead:

?- between(0, 3, N), length(L, N).


Depending on your purposes, it might be helpful to consider predicates like between/3 and length/2 as primitives that don’t need a pure Prolog implementation.

There can be a big performance difference:

list_length_upto(Lst, MaxLen) :-
(   is_list(Lst)
->  length(Lst, Len),
Len =< MaxLen
;   between(0, MaxLen, Len),
length(Lst, Len)
).

list_length_between_upto(Lst, Max) :-
between(0, Max, Len),
length(Lst, Len).

?- numlist(1, 50_000, Lst), time(list_length_upto(Lst, 50_000)).
% 4 inferences, 0.001 CPU in 0.001 seconds (97% CPU, 5411 Lips)

?- numlist(1, 50_000, Lst), time(list_length_between_upto(Lst, 50_000)).
% 150,002 inferences, 6.070 CPU in 6.099 seconds (100% CPU, 24714 Lips)


What exactly are we comparing here? The two predicates do different things? I am not even sure what is the commonality

No, they do the same thing - checking or setting the length of a list, as per this thread.

If the list is already instantiated, list_length_upto is very much faster than list_length_between_upto.

OK, I totally missed the point then. I mistakenly believed that length/2 on its own “checks or sets the length” and we are discussing how that can nevertheless cause non-termination.

You might also ask what causes termination. A simple “modes” based rule is:

• If a “+” argument is smaller in the recursive call, the predicate terminates.
(in a simple “mode” DSL where “+” means input, and “-” means output)

Thats why this here:

app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).


Terminates for this call:

?- app(X, Y, [1,2,3]).


Just look at the mode (-, -, +). On the other hand if such a wellfoundedness
criteria its missing, it is very difficult to judge whether something terminates
or not, typical example beeing the Collatz sequence:

Collatz sequence
Collatz conjecture - Wikipedia

What does not cause non-termination in the Collatz sequence?

The conjecture has been shown to hold for all positive integers up to 2.95 \times 10^{20}

I was not only trying to create a fixed list – I wanted to see how Prolog is unifying as it goes through the leng clauses.
The idea was to get Tau Prolog to show me how unifications are happening
when you run the query

-?  leng(L, N, 1).


I needed the upper bound since otherwise Tau Prolog hung – it is not robust yet like Swish or Ciao, and besides, the bound makes for a understandable visualization in the Tree Visualization Tau provides.

The limit field is a little buggy in Tau Prolog, there is a discrepancy
between ordinary queries and tree view. But we have this non-
termination criteria, simple sketch of it:

• If a variant term is called, it does not terminate.
(a variant results from a term by a bijective variable mapping)

You can edit the limit field. It has initially the value 10000. If you edit
the value to 5. I get this here for len/2:

Ordinary query execution with limit=5:

And with tree display and limit=1, you see the variants
len(X, N), len(_62, _64), len(_66, _68), etc…

Tree view execution with limit=1:

In SWI-Prolog you can test variants with (=@=)/2. Such criterias are
used in SWI-Prolog tabling, to make it terminate nevertheless
sometimes. Not applicable to len/2 though.