implementing findall in Prolog

[Mark Tarver]

Can findall be implemented in Prolog itself - not using asserta or assertz but only a declarative Prolog with at most cuts and negation-as-failure?

Mark

[Julio Di Egidio]

On Sunday, 21 July 2019 09:35:40 UTC+2, Mark Tarver wrote:
> Can findall be implemented in Prolog itself - not using asserta or assertz
> but only a declarative Prolog with at most cuts and negation-as-failure?

Hi, try this:

--------------------------------------------------
%! fison_f(+N:integer, -L:list) is semidet.
fison_f(N, L) :-
N >= 1,
findall(I, between(1, N, I), L).

%! fison_p(+N:integer, -L:list) is semidet.
fison_p(N, L) :-
N >= 1,
fison_p_(1, N, L).

fison_p_(N, N, [N]) :- !.
fison_p_(I, N, [I| L]) :-
succ(I, I1),
fison_p_(I1, N, L).
--------------------------------------------------

HTH,

Julio

[Julio Di Egidio]

Sorry, I had misunderstood your question.

Actually no, implementing findall requires at least some meta-programming.

It's a bit of a FAQ: <https://duckduckgo.com/?q=prolog+implementing+findall>

Julio

[j4n bur53]

Hi,

A declarative builder/3 could be defined as follows:

builder(X,G,L) :-
forall(member(X,L),G),
forall(G,member(X,L)).

But I guess this is not very helpful.
But you could use it to verify that a findall
result is correct, modulo duplicates and

reordering. For example you can do:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.1.10)

p(a).
p(b).
p(c).

?- builder(X,p(X),[a,b,c]).
true
?- builder(X,p(X),[a,b]).
false
?- builder(X,p(X),[a,b,c,d]).
false

Bye

P.S.: forall/3 is defined as follows and preloaded
standard in SWI-Prolog.

forall(C,A) :- \+ (C, \+ A).

P.P.S.: The builder shows that it as both positive
and negative polarity. Means inserts in the goal G
change the result, and deletes in the goal G change
the result.

Ha Ha

P.P.S.: More ideas:
https://stackoverflow.com/questions/7647758/prolog-findall-implementation

Mark Tarver schrieb:
> Can findall be implemented in Prologitself - not using asserta or assertzbut only a declarative Prolog with at

[j4n bur53]

The declarative builder/3 is just an adoption
of the set theory comprehension axiom:

https://en.wikipedia.org/wiki/Axiom_schema_of_specification#Statement

Explanation: The navie comprehension axiom without
a domain A basically says the following. This
is also known as class builder:

forall x(x e L <=> G)

You can split up the bi-implicatioon P<=>Q
into P=>Q and Q=>P. And move the conjunction
out so that you get:

forall x(x e L => G) &
forall x(G => x e L)

So its two times a bounded quantifier, assuming
that G can also bound the variable. So that in
Prolog we get this approximation:

forall(member(X,L),G),
forall(G,member(X,L)).

But a warning, its an approximation, since forall/2
is implemented via negation as failure. Not sure
whether we can show Russell set this way, most

likely something from classical logic is missing.
Maybe the Curry Paradox works this way, it requires
less than classical logic...

Have Fun!

j4n bur53 schrieb:

[j4n bur53]

Here is an example, where this approximation
doesn't give good results. Take:

q(0-_).
q(_-1).

The usual findall gives:

?- findall(X,q(X),L).
L = [0-_6732, _6718-1].

But the builder verifies:

?- builder(X,q(X),[0-_,_-2]).
true.

So it kind of only works for ground lists.
This is a problem how negation of failure
sometimes creates additional existential

quantifiers and gets more premissive than
one would think. So this here:

C, \+A

Cannot be translated to logically:

C & ~A

Its rather dynamically translated to:

C & ~exists x1,..,xn A

Where x1,..,xn are the variables occuring in A
and not occuring C, at runtime.