On a logical reading of `foreach/2` predicate

Nice to know
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)].