What is the approach for dealing with "residual goals" in Prolog?

Question

Consider this program as an example. It uses a delayed goal

room(green).
room(blue).
room(red).
room(white).

location(jimmy,red).
location(ricky,blue).
location(cindy,green).

% "Is a certain room unoccupied?"
   
not_occupied(Room) :-
   nonvar(Room),
   assertion(room(Room)),
   \+ location(_Person,Room).

% If no specific "Room" has been given, the negated goal is
% delayed until the "Room" has been instantiated.

not_occupied(Room) :-
   var(Room),
   !,
   when(
      ground(Room),
      (\+ location(_Person,Room))
   ).

If I now ask

?- not_occupied(R).

then Prolog succeeds and outputs a residual goal

?- not_occupied(R).
when(ground(R),\+location(_7676,R)).

In effect, it doesn't really succeed. It succeeds optimistically (because in order to not stop the computation, succeed it must) but the actual logical success is dependent on actual success of the residual goal.

How do I find out programmatically whether a subgoal succeeded with a residual goal? (And what do I do then?) What is the approach?

P.S.

Having a secondary Prolog truth value might be a nice Prolog extension, in that a true+ would indicate "success under condition that the residual goals succeed". This actually seems to be of some necessity:

In SWI-Prolog, take this inherently ambiguous goal:

do :- not_occupied(_).

Calling it does not even print out any residual goal at all:

?- do.
true.

Did the goal succeed? Not really, it's still in logical limbo, but the toplevel doesn't even tell me. On the other hand there is no way to feed more information into the program to resolve residual goals. But defaulting to "success" because the computation ran to its end feels wrong.

Answer 1

A query that cannot resolve its residual goals is called a floundering query. Computations can flounder when they are intended to succeed or finitely fail. Residual goals introduce a third state that is neither success nor finitely failed.

Constraint logic programs can fail to invoke certain constraint solvers because variables are insufficiently instantiated or constrained. To avoid floundering in constraint solvers, they often offer labeling as a last resort.

The third state is seen in the top level, when residual goals are listed. And it is implementation dependent how residual goals can be queried. Typical predicates are:

• call_residue_vars(G, L):
  The predicate succeeds whenever the goal G succeeds and unifies L with the newly introduced attributed variables.
• call_residue(G, L):
  The predicate succeeds whenever the goal G succeeds and unifies L with the constraints of the newly introduced attributed variables.

That SWI-Prolog doesn't print the residue variables in the toplevel, is a service by SWI-Prolog, to only show the projected variables. But you can neverthless query the residue:

/* SWI-Prolog */
?- do.
true.

?- call_residue_vars(do, X).
X = [_5968],
when(ground(_5968), \+location(_6000, _5968)).

Pitty that SWI-Prolog doesn't support call_residue/2. copy_term/3 is not really a substitute. In my Prolog system I have stopped computing a projection in the top-level and display everthing. Also I do support call_residue/2:

/* Jekejeke Prolog */
?- do.
when(ground([_A]), \+ location(_B, _A))

?- call_residue_vars(do, X).
X = [_A],
when(ground([_A]), \+ location(_B, _A))

?- call_residue(do, X).
X = [when(ground([_A]), \+ location(_B, _A))],
when(ground([_A]), \+ location(_B, _A))

call_residue/2 is also found in ECLiPSe Prolog and SICStus Prolog. In SICStus Prolog it returns a pair list, also showing principal variables. ECLiPSe Prolog on the other hand only returns dummy variables. And then there are compatibilty issues for call_residue_vars/2 like here.

Answer 2

First some terminological issues. What we get back from the top level is an answer. Say:

?- length(Xs, 0).
   Xs = [].

Here, the answer is in the form of an answer substitution which describes a single solution.

?- length(Xs, 1).
   Xs = [_A].

Again, this is an answer substitution, but this time it describes infinitely many solutions.

Often the notion of answer and solution are used interchangeably, but once we use delayed goals or constraints, we need a clear distinction. What is now new is that answers may contain an arbitrary number of solutions including none at all.

?- freeze(X, false).
   freeze(X,false).   % no solution

?- freeze(X, ( X = 1 ; X = 2 ) ).
   freeze(X,(X=1;X=2)).  % two solutions

Some implementations provide frozen(Var, Goal) to get just the goals related to Var. In this context, the built-in call_residue(Goal_0, Residuum) was conceived. Originally, in SICStus 0.7 it was defined for delayed goals were the residuum is quite well defined. However, once we extend our language to clpfd, things are much less clear. Here is SICStus 3.12.5:

| ?- X in 1..3, call_residue(X in 2..4, Residuum).
Residuum = [[X]-(X in 2..3),
X in 1..3 ?

Should the residuum now be X in 2..3 or X in \{1}? Things can get quite complex (read: buggy). Also, undoing the bindings is quite an effort; or implementations first create a copy of the entire goal and then retain the constraints.

SICStus 4 replaced call_residue/2 by two new built-ins. call_residue_vars(Goal_0, Vars) unifies Vars with the variables that are related to the delayed goals or constraints created in Goal_0. Note that this notion is not that precise, when some constrained variables exist prior to Goal_0 and occur in Goal_0. But the main point is that this built-in is relatively cheap to implement. It does not copy Goal_0 or any subterm thereof.

The other is copy_term(Term, Copy, G_0s) which can be used to reconstruct the attached constraints by calling maplist(call, G_0s) (in SWI, Scryer) or call(G_0) (in SICStus). In the implementations of SWI (clpfd) and Scryer (clpz), some redundant constraints of the form V in inf..sup are omitted by the projection. But projection is really for another issue.