'$skip_max_list/4' wrong behavior on unbounded or big `Max` skip with cyclic term tail

[bakaq]

?- [user]. sml(Skip,Max,Ls0,Ls) :- '$skip_max_list'(Skip,Max,Ls0,Ls).

?- Ls0 = [1,2|Ls0], sml(S,1,Ls0,Ls).
   Ls0 = [1,2|Ls0], S = 1, Ls = [2,1|Ls].
?- Ls0 = [1,2|Ls0], sml(S,2,Ls0,Ls).
   Ls0 = [1,2|Ls0], S = 2, Ls = [1,2|Ls0].
?- Ls0 = [1,2|Ls0], sml(S,3,Ls0,Ls).
   Ls0 = [1,2|Ls0], S = 2, Ls = [2,1|Ls], unexpected.
   Ls0 = [1,2|Ls0], S = 2, Ls = [1,2|Ls0]. % Expected, but not found
?- Ls0 = [1,2|Ls0], sml(S,_,Ls0,Ls).
   Ls0 = [1,2|Ls0], S = 2, Ls = [2,1|Ls], unexpected.
   Ls0 = [1,2|Ls0], S = 2, Ls = [1,2|Ls0]. % Expected, but not found

[UWN]

Why is it wrong? It detects at least the loop. But where I do agree with you is when I look into:

?- Ls0 = [A,B|Ls0], A=a,B=b,sml(S,_,Ls0,Ls).
   Ls0 = [a,b|Ls0], A = a, B = b, S = 2, Ls = [b,a|Ls].
?- Ls0 = [a,b|Ls0], sml(S,_,Ls0,Ls).
   Ls0 = [a,b|Ls0], S = 2, Ls = [a,b|Ls0].

There should not be a different result. That's for sure. And Trealla agrees with you.

((It depends a bit whether or not there is a second phase for Brent. Originally, that second phase is not needed, but if there is such a second phase, then it should produce the result you indicated.))

[bakaq]

I though '$skip_max_list'(S,_,Ls0,Ls) would always guarantee that length(S, Skipped), append(Skipped, Ls, Ls0), is that not the case?

?- Ls0 = [1,2|Ls0], sml(S,2,Ls0,Ls), length(Skipped, S), append(Skipped, Ls, Ls0).
   Ls0 = [1,2|Ls0], S = 2, Ls = [1,2|Ls0], Skipped = [1,2].
?- Ls0 = [1,2|Ls0], sml(S,3,Ls0,Ls), length(Skipped, S), append(Skipped, Ls, Ls0).
   false. % Intentional??

[UWN]

is that not the case?

You are talking here about cases of infinite lists only. That is, not terms but trees. The best case to test against currently, is probably nth0/3. Maybe there are problems due to this.

[bakaq]

Yep, the implementation of nth0/3 assumes that '$skip_max_list'/4 has this property. Look at this for example:

?- Ls0 = [1,2|Ls0], between(0, 5, N), nth0(N, Ls0, L).
   Ls0 = [1,2|Ls0], N = 0, L = 1
;  Ls0 = [1,2|Ls0], N = 1, L = 2
;  Ls0 = [1,2|Ls0], N = 2, L = 1
;  Ls0 = [1,2|Ls0], N = 3, L = 1, unexpected % L should be 2!
;  Ls0 = [1,2|Ls0], N = 4, L = 2, unexpected
;  Ls0 = [1,2|Ls0], N = 5, L = 1, unexpected.
?- Ls0 = [1,2|Ls0], Ls0 = [1,2,1,1,2,1|_].
   false.
?- Ls0 = [1,2|Ls0], Ls0 = [1,2,1,2,1,2|_].
   Ls0 = [1,2|Ls0].

[bakaq]

The Ls argument of '$skip_max_list'(S,Max,Ls0,Ls) being undefined in the case that Ls0 is an infinite list makes it pretty useless as a building block for predicates that need to deal with rational trees. I think that guaranteeing length(Skipped, S), append(Skipped, Ls, Ls0) is a reasonable property to enforce, because it's what I would expect and what most of the code out there already seems to assume. Is there anything problematic about this?

[UWN]

(The original implementation for SWI did stop just when the algorithm found that we are in a loop. But then, it was never used for nth0/3.)

[UWN]

The Ls argument of '$skip_max_list'(S,Max,Ls0,Ls) being undefined in the case that Ls0 is an infinite list makes it pretty useless as a building block for predicates that need to deal with rational trees. I think that guaranteeing length(Skipped, S), append(Skipped, Ls, Ls0) is a reasonable property to enforce, because it's what I would expect and what most of the code out there already seems to assume. Is there anything problematic about this?

Probably. But consider ambiguous cases like L = [a,b,a,b|L]. So this guaranteeing length(Skipped, S), append(Skipped, Ls, Ls0) is a bit unstable here, since we do not have a declarative semantics. But, say, maybe you can state that for ground trees.

[bakaq]

But consider ambiguous cases like L = [a,b,a,b|L].

It is ambiguous, but it's guaranteeable isn't it? In the sense that '$skip_max_list/4' can always return something that fits the property right? In this case I think either S = 0, Ls = Ls0 or S = 4, Ls = [a,b,a,b|Ls0] make sense, and both guarantee the property.

S = 4, Ls = [a,b,a,b|Ls0] is the current behavior, probably because we don't do the cycle check in Ls0 at the start. This behavior may be desirable since then you can "iterate" an infinite list by repeatedly calling '$skip_max_list'/4. I'm not sure how to guarantee this semantic though. Maybe guarantee that S > 0 if Ls = [_|_]? I think S = 0, Ls = Ls0 is cleaner though.