On a logical reading of `foreach/2` predicate

Nice to know
1

It was surprising for me when I leaned the meaning of forach goal e.g. foreach(between(1, 3, X), dif(X, Y)), which is expanded at runtime to the goal

  `( dif(1, Y), dif(2, Y),  dif(3, Y) ).`

However, after a while, I understood that this is natural from logics. Suppose D is a finite domain, e.g, D=\{1,2,3\}. Then quantifiers can be eliminated into propositional conjunction or disjunction by following rules.

  1. \forall x\, p(x) \equiv p(1) \land p(2) \land p(3)
  2. \exists x\, p(x) \equiv p(1) \lor p(2) \lor p(3)

That is, in a finite domain, a first-order formula is a disguised form of a proposition. With this observation in mind, the meaning foreach(p(x), q(x, y)) is clear if it is written

\exists y \forall x ( p(x)\to q(x,y) )

which reads there exists y such that q(x,y) holds for each x satisfying p(x). Also it is read: find y such that q(x,y) holds for all x satisying p(x). I am posting a trivial observation, and I am afraid I am missing such quantifier scope aware description of foreach.

Similary \forall x \exists y ( p(x)\to q(x,y) ) is close to a logical reading for forall(p(x), q(x, y)).

BTW. as English phrases, it is not clear for me the difference between “for all” and “for each”.

EDIT 2022.2.13.
Based on the observation above, I wrote a model finder for FOL closed formulae with finite domain. Though this is a toy codes it might be useful for instructive purpose on quantifiers of logics. I used my ZDD library for simplicity and my familiarity. Sample
is taken: “Every one likes some one.”

% ?- nnf_model([a,b,c], some(y, all(x, like(x, y)))).
%@ [like(a,c),like(b,c),like(c,c)]
%@ [like(a,b),like(b,b),like(c,b)]
%@ [like(a,a),like(b,a),like(c,a)]
%@ true.

% ?- nnf_model([a,b,c], -some(y, all(x, like(x, y)))).
%@ [-like(c,a),-like(c,b),-like(c,c)]
%@ [-like(c,a),-like(c,b),-like(b,c)]
% ...

% ?- nnf_model([a,b,c], all(x, some(y, like(x, y)))).
%@ [like(a,c),like(b,c),like(c,c)]
%@ [like(a,c),like(b,c),like(c,b)]
% ...
 ....
2 Likes
4

I’m coming from functional programming community. For me that the foreach usually means something like monadic code (e.g. List comprehension). I didn’t realize before that the foreach could have logical reading. Your post gave me a new perspective.

Thanks.

5

Also, it makes sense to me that, you said:

foreach(p(x), q(x, y)) is read as ∃y∀x(p(x)→q(x,y))

forall(p(x), q(x, y)) is read as ∀x∃y(p(x)→q(x,y))

Merely exchanging ∀ and ∃ leads to difference meaning.

Is it possible to find an example in Prolog that can represent the difference between these two by foreach and forall (especially for finite domain)?

2 Likes
6

How about this ?

% ?- forall(between(1, 3, X),  X = Y).
%@ true.
% ?- foreach(between(1, 3, X),  X = Y).
%@ false.
1 Like
7

I seemly found an example:

?-foreach(between(1, 3, X), (between(1, 3, Y), X=<Y)).
Y = 3.

?- forall(between(1, 3, X), (between(1, 3, Y), X=<Y)).
true.

For the 1st query, we found the unique Y = 3 which satisfies ∃Y.∀X.(between(1, 3, X) → (between(1, 3, Y) ∧ X≤Y)).

For the 2nd query, there is no unique Y, because for each X \in \{1,2,3\}, we can have different Y.

Correct me if I am wrong.

Thanks.

8

Good example, I think, though other readers must have better query samples than me.

1 Like
9

You are doing something fun.

Also for fun, I extends all and some quantifiers for forall and foreach so that negation normal form are obtained like the standard syntax. Block quantifiers are allowed. compound ground terms allowed as variables, which finally becomes prolog variables. I have no idea of application of this extension for now, but just for fun. It seems a natural and useful extension of the standard FOL syntax, and everybody already uses it as folklore.

% ?- nnf(some(y, all(x, between(1,3,x), member(x, y))), R), numbervars(R).
%@ R = all(A, between(1, 3, A), member(A, sk4)).
% ?- nnf(-some(y, all(x, -between(1,3,x), -member(x, y))), R), numbervars(R).
%@ R = all(A,  (-between(1, 3, sk5(A)), member(sk5(A), A))).
12

That extension is a syntax sugar to be expanded to the standard FOL, which is too simple to cause problem.

15

Recently I revisited your logical reading of forall/2 and foreach/2 and found some interesting conclusions.

  1. The derivation of the forall/2

    The SWI-Prolog manual said that

    The predicate forall/2 is implemented as \+ ( Cond, \+ Action)

    but it doesn’t provide a derivation.

    In fact, this double negation implementation could be derived from logical equivalence:

        forall(p(x), q(x,y))
<=> ∀x.∃y.(p(x) → q(x,y))
<=> ∀x.∃y.(¬ p(x) ∨ q(x,y))
<=> ∀x.(¬ p(x) ∨ ∃y.q(x,y)) % reverse rule of prenex normal form. 
<=> ¬ ¬ ∀x.(¬ p(x) ∨ ∃y.q(x,y))
<=> ¬ ∃x.¬ (¬ p(x) ∨ ∃y.q(x,y))
<=> ¬ ∃x.(p(x) ∧ ¬ ∃y.q(x,y))

    Indeed this result formula ¬ ∃x.(p(x) ∧ ¬ ∃y.q(x,y)) can be implemented by \+ (p(X), \+ q(X,Y)) in Prolog directly, no matter X and Y are fresh variables or not.

    For example (I assume X is alway a fresh variable, just consider Y),

    When Y is a fresh variable,

    ?- \+ (p(X), \+ q(X,Y))

    OK, it follows the FOL definition ¬ ∃x.(p(x) ∧ ¬ ∃y.q(x,y)), no problem,

    When Y is a gound value,

    ?- Y=1, \+ (p(X), \+ q(X,Y))

    The query follows the FOL definition ¬ ∃x.(p(x) ∧ ¬ q(x,1)), so the double negation form still works.

  2. The derivation of the foreach/2

        foreach(p(x), q(x, y))
<=> ∃y.∀x.(p(x) → q(x,y)) 
<=> ∃y.¬ ¬∀x.(p(x) → q(x,y)) 
<=> ∃y.¬ ∃x.¬ (p(x) → q(x,y)) 
<=> ∃y.¬ ∃x.(p(x) ∧ ¬ q(x,y))

    Note that this result formula ∃y.¬ ∃x.(p(x) ∧ ¬ q(x,y)) can not be implemented by \+ (p(X), \+ q(X,Y)) in general, because someone might pass a fresh variable Y.

    For example,

    suppose foreach/2 was also implemented by \+ (p(X), \+ q(X,Y)) , the following query would be problematic:

    ?- \+ (p(X), \+ q(X,Y))

    Here Y is a fresh variable.

    It means ¬ ∃x.(p(x) ∧ ¬ ∃y.q(x,y)) instead of ∃y.¬ ∃x.(p(x) ∧ ¬ q(x,y)) .

  3. forall/2 and foreach/2 are interchangeable when Y is a ground value.

    The forall/2 version:

    ?- between(1,3,Y), forall(p(X), q(X,Y)).

    The FOL semantics of the query is

    ∃y.between(1,3,y) ∧ ¬ ∃x.(p(x) ∧ ¬ q(x,y))

    This is due to the fact that variables are sharing in Prolog (not shadowing).

    The foreach/2 version:

    ?- between(1,3,Y), foreach(p(X), q(X,Y)).

    The FOL semantics of the query is

    ∃y.between(1,3,y) ∧ ¬ ∃x.(p(x) ∧ ¬ q(x,y))

    which is the same as the forall/2 version.

  4. forall/2 is more efficient than foreach/2 when they are interchangeable.

    For example,

    repeat(N, Goal) :-
  forall(between(1,N,_), Goal).

q(2,y).
q(3,y).

?- time(repeat(100000, (Y=y, forall(between(1,3,X), q(X,Y))))).
% 12 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
false.

?- time(repeat(100000, (Y=y, foreach(between(1,3,X), q(X,Y))))).
% 70,214 inferences, 0.016 CPU in 0.027 seconds (58% CPU, 4500869 Lips)
false.

    This is due to that

    forall/2 will short-circuit once q(1,y) fail, i.e. it doesn’t try q(2,y) and q(3,y), whereas

    foreach/2 must generate all the X Y pairs.

    ?- Y=y, findall(q(X,Y), between(1,3,X), Goals).
Y = y,
Goals = [q(1,y),q(2,y),q(3,y)].