SWI-Prolog / swipl-devel

SWI-Prolog Main development repository
http://www.swi-prolog.org
Other
976 stars 176 forks source link

union/3 might go into infinite loop, even for well typed arguments #716

Open ghost opened 3 years ago

ghost commented 3 years ago

Try this:

?- union(X,[],[_|X])
ERROR: Stack limit (1.0Gb) exceeded

My guess, it is a steadfastness problem.

JanWielemaker commented 3 years ago

It is a mode error. See Discourse comments.

ghost commented 3 years ago

This here is also nice:

?- intersection(_, [], [_]).
... hangs ...

You use steadfastness via (=)/2 here, this is from SWI-Prolog source:

intersection([X|T], L, Intersect) :-
    memberchk(X, L),
    !,
    Intersect = [X|R],
    intersection(T, L, R).

Note the extra (=)/2. Oki Doki. Not sure whether I can find an error, where the mode is satisfied, but there is nevertheless an error. But since you use steadfastness rewriting anyway, despite not

having a mode checker. Why not improve type/instantiation checking, despite not having a type checker? Or maybe the rewriting was done for other reasons than steadfastness?

And why is the rewriting not applied everywhere? Sometimes behaviour is “undefined” which can mean loops. And sometimes I assume steadfastness is addressed?

JanWielemaker commented 3 years ago

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/why-steadfastness/3313/4

ghost commented 3 years ago

The aformentioned defects are gone for the new (=>)/2 based list predicates union/3 and intersection/3. Cool!

But they are a little asymmetric:

?- intersection(X, [1,2,3], L).
ERROR: No rule matches lists:intersection(_21734,[1,2,3],_21738)

?- intersection([1,2,3], X, L).
X = [1, 2, 3|_1062],
L = [1, 2, 3]. 

Maybe because they still use memberchk/2 which isn't implemented with (=>)/2.

JanWielemaker commented 3 years ago

memberchk(x, L) is supposed to succeed. I don't want to touch that. So yes, maybe an alternative to memberchk is an option. Fot now out of scope though.