3
votes

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, use copy_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.

1
In SICStus Prolog, which has much more experience in this area (dif and coroutining from the very beginning 1980s and attributed variables as the first platform since the 1990s), copy_term/2, setof/3 &ct never copy constraints — not without reason.false
What about '?- sorted(Xs).`repeat
@repeat There are two problems with ?- sorted(Xs). First, in order to ensure that ∀x(p(X)⇒q(X) Prolog will try to satisfy q for all solutions of p. This is impossible when p has infinite number of solutions. In the particular case of sorted(Xs), when the value of Xs 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. Zinoviev
The second problem is semantic. According to the specification of forany I've given above, "Condition is not permitted to modify in any way the variables listed in Context, otherwise forany won't work correctly." But the definition of sorted is such that with ?- sorted(Xs) Prolog will unify Xs first with the empty list, then with a non-empty list and these are not allowed.A. Zinoviev
Ad #2: why not check for sufficient instantiation upfront and raise a proper exception in cases of insufficiency?repeat

1 Answers

0
votes

Great news! I was surprised that bagof is written in Prolog. By looking at its code I learned that some things I thought are impossible are in fact possible. And just as the manual of SWI-Prolog suggested, copy_term/3 or rather the similar predicate copy_term_nat/2 helped.

So with great joy I am able to present a fully working (as far as I can tell) universal quantifier for SWI-Prolog:

forany(V, {Vars}, Condition, Body) :-
    findall(V-Vars, Condition, Solutions),
    % For SWI-Prolog.  Can be replaced by Solutions=Clean_solutions in other systems
    copy_term_nat(Solutions, Clean_solutions),
    forany_execute_goals(Clean_solutions, Vars, V, Body).

forany_execute_goals([], _, _, _).
forany_execute_goals([Sol-NewVars|Solutions], Vars, V, Body) :-
    % The following test can be removed
    assertion(subsumes_term(NewVars, Vars)),
    % or replaced by the following more standard use of throw/1:
%   (  subsumes_term(NewVars, Vars)
%   -> true
%   ;  throw('Forbidden instantiation of context variables by the antecedent of forany')  ),
    NewVars = Vars,
    call({Vars}/[V]>>Body, Sol),
    forany_execute_goals(Solutions, Vars, V, Body).