See also
No solutions for Goal lead to failure, instead of an empty bag.
"Failure" is the logically correct way of saying "there are no solutions".
?- bagof(X,member(X,[a,b,c]),Bag). Bag = [a, b, c]. ?- bagof(X,member(X,[]),Bag). false.
findall/3 is laxer in that regard and yields the empty bag if there is no solution. (see also: Notes about findall/3 ... how to use it etc.)
This means binding the Bag to [] must always fail, because an empty Bag is never generated
?- bagof(X,true,[]). false.
Note that the true
goal generates a one-element bag with whatever can be found in the first argument position of bagof/3, here an unbound variable:
?- bagof(X,true,L). L = [_65320].
You can use the if-then-else ->/2 (which is non-logical) to emulate the behaviour of findall/3:
?- (bagof(X,member(X,[a,b,c]),Bag) -> true ; Bag=[]). Bag = [a, b, c].
?- (bagof(X,member(X,[]),Bag) -> true ; Bag=[]). Bag = [].
Bag needs to fit exactly
The "bag" needs to exactly fit the number of results; there is no "early breakoff if the bag is too small" or "leave remaining elements in bag non-unified if the bag is too large".
From a logical standpoint, this makes sense.
If the bag is an unbound variable, it is bound to (the head of) a newly constructed list (with length > 0, fitting the number of results obtained).
Example:
The bag is too small:
?- bagof(B,between(1,3,B),[X]). false.
The bag is still too small:
?- bagof(B,between(1,3,B),[X,Y]). false.
The bag is an exact fit:
?- bagof(B,between(1,3,B),[X,Y,Z]). X = 1, Y = 2, Z = 3.
You can just request that bagof/3 build a new list for you, so no worries about list size (the most common case):
?- bagof(B,between(1,3,B),Bag). Bag = [1, 2, 3].
Another way: this bag requires a prefix of 3 elements, but any surplus goes into the suffix Rest:
?- bagof(B,between(1,3,B),[A,B,C|Rest]). B = 2, A = 1, C = 3, Rest = [4, 5, 6, 7, 8, 9, 10].
The above also applies to setof/3:
bagof/3 leaves duplicate elements (as decided by ==/2) in the bag:
?- bagof(B,(between(1,3,B);between(1,2,B)),Bag). Bag = [1, 2, 3, 1, 2].
setof/3 does not retain duplicate elements:
?- setof(S,(between(1,3,S);between(1,2,S)),Bag). Bag = [1, 2, 3]. ?- setof(S,(between(1,3,S);between(1,2,S)),[X,Y,Z]). X = 1, Y = 2, Z = 3.
But the resulting list (now a "set") still must fit exactly:
?- setof(S,(between(1,3,S);between(1,2,S)),[X,Y]). false.
Non-termination for infinitely many solutions even if the Bag is of limited size
Edge case: If the Goal generates solutions forever, the goal won't terminate even if the Bag is of limited size :
?- bagof(X,between(0,5,X),[A1,A2,A3,A4,A5]). false. ?- bagof(X,between(0,inf,X),[A1,A2,A3,A4,A5]). ... NON TERMINATION
One could have a bagof/3 that gives up when it detects that it will have to unify with a shorter list than the one it already has collected solutions with.
This is not currently foreseen to be added: Issue #700
Making sure the goal is dropped if it goes over a fixed number of solutions
Using library(solution_sequences)
?- Bag=[A1,A2,A3,A4,A5], length(Bag,BagLen), succ(BagLen,Over), bagof(X,limit(Over,between(0,3,X)),Bag). false. ?- Bag=[A1,A2,A3,A4,A5], length(Bag,BagLen), succ(BagLen,Over), bagof(X,limit(Over,between(0,4,X)),Bag). Bag = [0, 1, 2, 3, 4], A1 = 0, A2 = 1, A3 = 2, A4 = 3, A5 = 4, BagLen = 5, Over = 6. ?- Bag=[A1,A2,A3,A4,A5], length(Bag,BagLen), succ(BagLen,Over), bagof(X,limit(Over,between(0,5,X)),Bag). false. ?- Bag=[A1,A2,A3,A4,A5], length(Bag,BagLen), succ(BagLen,Over), bagof(X,limit(Over,between(0,inf,X)),Bag). false.
Notes on the ^ ("caret") mark of setof / 3 and bagof / 3
More text and test cases at this page: Behaviour of the caret ^ in setof/3 and bagof/3 goal expressions
Clause-wide variable | | +------------------------+------------------------+ | | | Clause-wide variables | | that are collected via the | | template at arg-position 1 by | | setof/3 (NOT local to setof/3) | | thus can be constrained elsewhere | | in the clause (possibly accidentally) | | | | | | | | +-+--------+----------+-+ | | | | | | | | | | | | | get_closed_set(Set,K) :- setof( [X,Y] , P^R^search(P,R,X,Y,K) , Set). | | | | | | | <-------------------> Goal expression | | | | | | | | | | | | +---------------------------------------+-----+ | | | | | | | | | | +-+----+---+-+ Clause-wide variable. | Backtracking over this | is done by the caller | of get_closed_set/2. | Variables marked as "free for backtracking if fresh". This is NEARLY the same as "being local to the goal expression" or "being existentially quantified." Backtracking over these is done by setof/3. If these appear elsewhere in the clause, they be constrained (possibly accidentally)!
TL;DR It doesn't always work as expected.
You may want to write a dedicated predicate to "hide" the caret-adorned variables from the context of the clause calling bagof/3:
So transform
bag_them(Bag) :- bagof( [X,Y] , P^R^search(P,R,X,Y) , Bag).
into
bag_them(Bag) :- bagof( [X,Y] , indirect_search(X,Y) , Bag). indirect_search(X,Y) :- search(_P,_R,X,Y).
See also the "free variable" bracy notation {X}
used in the lambda expressions of library(yall)
. It does the contrary of the caret notation of bagof/3
- The caret notation of bagof/3 hides variables of the goal from the context of the surrounding clause.
- The bracy notation of library(yall) connects variables of the lambda expression to the context of the surrounding clause.