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