How is it that a clause that requires a ground term works, but that term isn't ground outside of the clause?

Question

I'd like to test whether a term has only one solution. (Understanding that this might be done in different ways) I've done the following and would like to understand why it doesn't work, if it can be made to work, and if not, what the appropriate implementation would be.

First, I have an "implies" operator (that has seemed to work elsewhere):

:- op(1050,xfy,'==>').
'==>'(A,B) :-·forall(call(A), call(B)).

next I have my singleSolution predicate:

singleSolution(G) :- copy_term(G,G2), (call(G), call(G2)) ==> (G = G2).

Here I'm trying to say: take a term G and make a copy of it, so I can solve them independently. Now if solving both independently implies they are equal, then there must be only one solution.

This works in some simple cases.

BUT.
I have a predicate foo(X,Y,Z) (too large to share) which solves things properly, and for which singleSolution can answer correctly. However, X,Y,Z are not fully ground after singleSolution(foo(X,Y,Z)) is called, even though they would be after directly calling foo(X,Y,Z).

I don't understand that. (As a sanity test: I've verified that I get the same results under swi-prolog and gprolog.)

EDIT: Here is an example of where this fails.

increasing([]).
increasing([_]).
increasing([X,Y|T]) :- X < Y, increasing([Y|T]).

increasingSublist(LL,L) :-·
  sublist(L,LL),
  length(L, Len),
  Len > 1,
  increasing(L).

then

| ?- findall(L, singleSolution(increasingSublist([1,2],L)),R).
R = [_]
yes

But we don't know what L is.

What does sublist/2 (I can imagine...) do? Can you share its code? — damianodamiano, Feb 14 '23 at 15:48
Sorry, just saw this is gprolog specific. "sublist(List1, List2) succeeds if all elements of List1 appear in List2 in the same order. This predicate is re-executable on backtracking." This is just for an example to use with `singleSolution`. — Mark Bolusmjak, Feb 14 '23 at 15:50
BTW, I think you can use findall/3 to retrieve all the answers for a goal and then if the list containing these has lenght greater than 1 it means that the goal has multiple solutions, otherwise it has only one. — damianodamiano, Feb 14 '23 at 15:53
@damianodamiano yes, but this is problematic if there are often too many solutions (which there are in the cases I'm looking at). Seems even if I constrain the length of solutions, this doesn't prevent findall from exhausting all memory: `length(Ans,1), findall(L, member(L,Y), Ans).` — Mark Bolusmjak, Feb 14 '23 at 16:02
@MarkBolusmjak `forall/2` does not bind variables from the calling goal. In your example `L` is a free variable and the goal `G=G2` from `==>/2` does not bind it. Check the definition of `forall/2` — gusbro, Feb 14 '23 at 22:17
@MarkBolusmjak: To help you more you need first to state what you want. `forall/2` and `findall/3` are all constructs that do not readily express your intention, — false, Feb 15 '23 at 06:08

guregu · Answer 1 · 2023-02-15T11:03:38.633

1

This seems to work, but I'm not sure if it's logically sound :)

It uses call_nth/2, a nonstandard but common predicate. It abuses throw to short-circuit the computation. Using bagof/3 instead of findall/3 lets us keep the Goal argument bound (and it will fail where findall/3 would succeed if it finds 0 solutions).

only_once(Goal) :-
    catch(bagof(_, only_once_(Goal), _), too_many, fail).
only_once_(Goal) :-
    call_nth(Goal, N),
    (  N > 1
    -> throw(too_many)
    ;  true
    ).

Testing it (on SWI):

?- only_once(member(X, [1])).
X = 1.

?- only_once(member(a, [a, b])).
true.

?- only_once(member(X, [a, b])).
false.

?- only_once(between(1,inf,X)).
false.

Unfortunately, I don't think call_nth/2 is supported in GNU Prolog.

edited Feb 15 '23 at 11:03

answered Feb 15 '23 at 10:44

guregu

176
5

Thanks. You are right that `call_nth` isn't part of GNU Prolog. I've posted a generic solution that I think should work with any ISO Prolog. – Mark Bolusmjak Feb 15 '23 at 14:53
[`call_nth/2`](http://www.complang.tuwien.ac.at/ulrich/iso-prolog/call_nth) is going into the Prolog prologue. So GNU Prolog should provide [some implementation](https://stackoverflow.com/a/12942551/772868). – false Feb 22 '23 at 06:13
Using `bagof/3` makes your code brittle for constraints. Instead, just consider [`call_semidet/1`](https://stackoverflow.com/a/12942551/772868) which calls the goal twice but preserves all constraints. – false Feb 22 '23 at 06:16

score 1 · Answer 2 · answered Feb 15 '23 at 22:23

Another possible solution:

single_solution(G) :-
    copy_term(G, H),
    call(G),
    !,
    (   ground(H)
    ->  true
    ;   \+ ( call(H), G \= H )  % There is no H different from G
    ).

p(a).
p(a).

q(b).
q(c).

Examples:

?- single_solution( p(X) ).
X = a.

?- single_solution( q(X) ).
false.

?- single_solution( member(X, [a,a,a]) ).
X = a.

?- single_solution( member(X, [a,b,c]) ).
false.

?- single_solution( repeat ).
true.

?- single_solution( between(1,inf,X) ).
false.

?- single_solution( between(1,inf,5) ).
true.

score 0 · Answer 3 · answered Feb 15 '23 at 14:52

0

Here is an another approach I came up with after @gusbro commented that forall/2 doesn't bind variables from the calling goal.

single_solution(G) :-·
  % duplicate the goal so we can solve independently
  copy_term(G,G2), 

  % solve the first goal at least / at most once.
  G, !,           
 
  % can we solve the duplicate differently?
  % if so, cut & fail. Otherwise, succeed.
  (G2, G2 \= G, !, fail; true).

answered Feb 15 '23 at 14:52

Mark Bolusmjak

23,606
10
74
129

What if you have more than one of the same solution? For example, `single_solution(repeat).` will never terminate. `assertz(a), assertz(a), single_solution(a).` would succeed, etc. – guregu Feb 15 '23 at 16:07
I'm looking for a single unique solution. Perhaps I should have been more clear, but I'd say it's typically accepted that when someone says "multiple solutions" they mean multiple unique solutions, and not the same identical solution considered multiple times. And given infinite time, and finite memory, this will correctly show that `repeat` has a unique single solution. – Mark Bolusmjak Feb 15 '23 at 21:38
1

Ah, thanks for the clarification. You might want to look into `dif/2` if you can use SWI, Scryer, etc. It would let you write this in a slightly easier way. – guregu Feb 16 '23 at 05:56

How is it that a clause that requires a ground term works, but that term isn't ground outside of the clause?

3 Answers3