A good language for logic programming should allow the programmer to use a language close to the language used by the mathematicians. Therefore, I have always considered the lack of proper universal quantifier in Prolog an important shortcoming.
Today an idea came to me how to define something much better than forall
and foreach
.
forany(Var, {Context}, Condition, Body)
This predicate tries to prove Body
for all instantiations Var
gets successively on backtracking over Condition
. All variables in Condition
and Body
are considered local unless listed in Var
or Context
. Condition
is not permitted to modify in any way the variables listed in Context
, otherwise forany
won't work correctly.
Here is the implementation (based on yall):
forany(V, {Vars}, Goal1, Goal2) :-
( bagof(V, {V,Vars}/Goal1, Solutions)
-> maplist({Vars}/[V]>>Goal2, Solutions)
; true ).
My first question is about the second argument of forany
. I'd like to eliminate it.
Now some examples
Construct a list of the first 8 squares:
?- length(X,8), forany(N, {X}, between(1,8,N),
(Q is N*N, nth1(N, X, Q))).
X = [1, 4, 9, 16, 25, 36, 49, 64].
Reverse a list:
?- X=[1,2,3,4,5], length(X,N), length(Y,N),
forany(I, {X,Y,N}, between(1,N,I),
(J is N-I+1, nth1(I,X,A), nth1(J,Y,A))).
X = [1, 2, 3, 4, 5],
N = 5,
Y = [5, 4, 3, 2, 1].
Subset:
subset(X, Y) :- forany(A, {X,Y}, member(A,X), member(A, Y)).
A funny way to generate all permutations of a list without duplicates:
permutation(X, Y) :-
length(X, N), length(Y, N), subset(X, Y).
?- permutation([1,2,3],X).
X = [1, 2, 3] ;
X = [1, 3, 2] ;
X = [2, 1, 3] ;
X = [2, 3, 1] ;
X = [3, 1, 2] ;
X = [3, 2, 1] ;
false.
A funny way to sort a list of different integers. Notice that constraints are used to make the list sorted so most permutations won't be generated:
sorted(X) :- forany(A-B, {X}, append(_, [A,B|_], X),
A#<B).
?- X=[7,3,8,2,6,4,9,5,1], length(X, N), length(Y, N),
sorted(Y), subset(X,Y).
X = [7, 3, 8, 2, 6, 4, 9, 5, 1],
N = 9,
Y = [1, 2, 3, 4, 5, 6, 7, 8, 9] .
The problem
It seems that this forany
works brilliantly when constraints are not used. Also, it can be used to generate constraints, but at least on SWI-Prolog there are problems when constraints already have been generated. The reason for this is that forany
uses bagof
and according to the manual of SWI-Prolog:
Term-copying operations (
assertz/1
,retract/1
,findall/3
,copy_term/2
, etc.) generally also copy constraints. The effect varies from ok, silent copying of huge constraint networks to violations of the internal consistency of constraint networks. As a rule of thumb, copying terms holding attributes must be deprecated. If you need to reason about a term that is involved in constraints, usecopy_term/3
to obtain the constraints as Prolog goals, and use these goals for further processing.
Here is a demonstration of the problem bagof
creates with constraints:
?- X=[A,B,C], dif(C,D), bagof(_, K^member(K,X), _).
X = [A, B, C],
dif(C, _5306),
dif(C, _5318),
dif(C, _5330),
dif(C, D).
As you can see, three unnecessary constraints are created.
My second question is if this is a problem only of SWI-Prolog.
And the third question: is there a way to fix this in SWI-Prolog. The above quote from the manual suggests that copy_term/3
should be used. Unfortunately, I don't understand this suggestion and I don't know if it is useful for forany
.
?- sorted(Xs).
First, in order to ensure that∀x(p(X)⇒q(X)
Prolog will try to satisfyq
for all solutions ofp
. This is impossible whenp
has infinite number of solutions. In the particular case ofsorted(Xs)
, when the value ofXs
is still unknown, potentially this can be an arbitrarily long list. In result, Prolog will try enthusiastically to reach the infinity and it will be us who will have to say it, "Please, stop". – A. Zinovievforany
I've given above, "Condition
is not permitted to modify in any way the variables listed inContext
, otherwiseforany
won't work correctly." But the definition ofsorted
is such that with?- sorted(Xs)
Prolog will unifyXs
first with the empty list, then with a non-empty list and these are not allowed. – A. Zinoviev