From Newsgroup: comp.lang.prolog

To solve the communicating variables problem, you can use
shift/1 and reset/3 which are available in SWI-Prolog. They are
from the Delimited continuations addition to SWI-Prolog.
The generic approach to use shift/reset for such purposes is:
run_state(Goal, StateIn, StateOut) :-
reset(Goal, Command, Cont),
( Cont == 0 % no more commands from Goal?
-> StateOut = StateIn
; run_state_(Command, Cont, StateIn, StateOut)
).
You have to define a couple of commands and a state. Lets
say we make a simple prototype, and only model P, the
clause space as a state. Then for embedded implication:
P, A |- B
--------------
P |- A -: B
The state would go from P, to [A|P] and then back to P.
We don’t need undo/1, this is part of shift/reset anyway.
Mostowski Collapse schrieb am Freitag, 12. Februar 2021 um 10:19:25 UTC+1:

So the big gain of formal systems compared to working inside a
domain theory T is that formal systems can more clearly see the
context dependency of queries A. Interestingly for queries B => C, if
the following conditions are met:

- B is a ground fact
- C does not throw an error
- B => C is not used with an outside Prolog cut

Then B => C can be safely realized in Prolog with a Pre-CRUD and
a Post-CRUD. Concerning the number of backtracking, the logical
update view of Prolog might give the best results? Otherwise C
might even unnecessarily loop?

(B => C) :-
(assertz(B); retract(B), fail), /* Pre-CRUD */
C,
(retract(B); assertz(B), fail). /* Post-CRUD */

λProlog extends the cases where (=>)/2 can be deployed. But I wonder
what happens when B is tabled, i.e. when we combine hypothetical
reasoning and tabling. SWI-Prolog has incremental and/or monotonic
tabling? Are there some show cases? Both the Pre-CRUD and the Post-CRUD require that the tabling not only supports assertz/1 but also retract/1. Mostowski Collapse schrieb am Freitag, 12. Februar 2021 um 10:17:40 UTC+1:

Now sombody on SWI-Prolog discourse scriveled:

I was thinking the exact query repeated would not

produce the same result (loss of idempotency).

If the query is issued via DQL, and if the query depends on data.
And if the data is DMLed. It is to expect that the query might give
a different result. This is normal first order predicate logic. In formal semantics proof is usually denoted by “|-”, it depends on domain axioms T. So that a query A is a consequence of some domain
axioms is denoted by:

T |- A

Translated to Prolog, domain axioms T can be Prolog facts and Prolog rules. Now when you are inside a formal system T and A are well formed, but not necessary fixed. Only if your are inside a domain axiom system T, then you have some invariant. But like you change the query A to A’, by issuing another query:

T |- A'

You might also change T to T’, or even both:

T' |- A'
For example if your domain axiom model ships in harbours, and a ship has changed the harbour. The ship example is used in early logic programming, that adds hypothethical reasoning to Prolog, as found in λProlog. λProlog
has (=>)/2 for hypothetical reasoning. The use of (=>)/2 for single sided unification clashes with λProlog.

But lets put aside this clash, λProlog allows this inference:

T, B |- C
------------------ (Hypo)
T |- B => C

Which allows posing hypothetical questions, i.e. what-if questions, like what if a ship is in this and that harbour. The (=>)/2 is found in every classical logic, it is sometimes called the deduction theorem. It blurs the
distinction between DML and DQL. It is also found in DES, the deductive educational system written on top of SWI-Prolog and SICStus Prolog.

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

So lets try this:
run_state_(push(A), Cont, StateIn, StateOut) :- !,
run_state(Cont, [A|StateIn], StateOut).
run_state_(pop, Cont, [_|StateIn], StateOut) :- !,
run_state(Cont, StateIn, StateOut).
run_state_(in(A), Cont, StateIn, StateOut) :- !,
member(A, StateIn),
run_state(Cont, StateIn, StateOut).
And then we can define embedded implication (:-)/2 as
follows. And I am also adopting (+)/1 from @philzock:
:- op(1200, xfy, -:).
(A -: B) :- shift(push(A)), B, shift(pop).
(+ A) :- shift(in(A)).
Lets see whether it works:
/* First Test Case, Communicating Variables, Ok! */
?- run_state((p(X) -: +p(Y)),[],S).
X = Y,
S = [].
/* Second Test Case, Backtracking, Ok! */
?- run_state((p(1) -: p(2) -: +p(X)),[],S).
X = 2,
S = [] ;
X = 1,
S = [].
Works fine! Maybe try the problematic Example 6 and Example 7
from the Bousi~Prolog paper as well.
Mostowski Collapse schrieb am Mittwoch, 19. April 2023 um 00:56:01 UTC+2:

To solve the communicating variables problem, you can use
shift/1 and reset/3 which are available in SWI-Prolog. They are
from the Delimited continuations addition to SWI-Prolog.

The generic approach to use shift/reset for such purposes is:

run_state(Goal, StateIn, StateOut) :-
reset(Goal, Command, Cont),
( Cont == 0 % no more commands from Goal?

StateOut = StateIn

; run_state_(Command, Cont, StateIn, StateOut)
).
You have to define a couple of commands and a state. Lets
say we make a simple prototype, and only model P, the
clause space as a state. Then for embedded implication:

P, A |- B
--------------
P |- A -: B

The state would go from P, to [A|P] and then back to P.
We don’t need undo/1, this is part of shift/reset anyway.
Mostowski Collapse schrieb am Freitag, 12. Februar 2021 um 10:19:25 UTC+1:

So the big gain of formal systems compared to working inside a
domain theory T is that formal systems can more clearly see the
context dependency of queries A. Interestingly for queries B => C, if
the following conditions are met:

- B is a ground fact
- C does not throw an error
- B => C is not used with an outside Prolog cut

Then B => C can be safely realized in Prolog with a Pre-CRUD and
a Post-CRUD. Concerning the number of backtracking, the logical
update view of Prolog might give the best results? Otherwise C
might even unnecessarily loop?

(B => C) :-
(assertz(B); retract(B), fail), /* Pre-CRUD */
C,
(retract(B); assertz(B), fail). /* Post-CRUD */

λProlog extends the cases where (=>)/2 can be deployed. But I wonder
what happens when B is tabled, i.e. when we combine hypothetical
reasoning and tabling. SWI-Prolog has incremental and/or monotonic tabling? Are there some show cases? Both the Pre-CRUD and the Post-CRUD require that the tabling not only supports assertz/1 but also retract/1. Mostowski Collapse schrieb am Freitag, 12. Februar 2021 um 10:17:40 UTC+1:

Now sombody on SWI-Prolog discourse scriveled:

I was thinking the exact query repeated would not

produce the same result (loss of idempotency).

If the query is issued via DQL, and if the query depends on data.
And if the data is DMLed. It is to expect that the query might give
a different result. This is normal first order predicate logic. In formal
semantics proof is usually denoted by “|-”, it depends on domain axioms T. So that a query A is a consequence of some domain
axioms is denoted by:

T |- A

Translated to Prolog, domain axioms T can be Prolog facts and Prolog rules. Now when you are inside a formal system T and A are well formed, but not necessary fixed. Only if your are inside a domain axiom system T,
then you have some invariant. But like you change the query A to A’, by
issuing another query:

T |- A'

You might also change T to T’, or even both:

T' |- A'
For example if your domain axiom model ships in harbours, and a ship has changed the harbour. The ship example is used in early logic programming,
that adds hypothethical reasoning to Prolog, as found in λProlog. λProlog
has (=>)/2 for hypothetical reasoning. The use of (=>)/2 for single sided
unification clashes with λProlog.

But lets put aside this clash, λProlog allows this inference:

T, B |- C
------------------ (Hypo)
T |- B => C

Which allows posing hypothetical questions, i.e. what-if questions, like what if a ship is in this and that harbour. The (=>)/2 is found in every classical logic, it is sometimes called the deduction theorem. It blurs the
distinction between DML and DQL. It is also found in DES, the deductive educational system written on top of SWI-Prolog and SICStus Prolog.

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

To get rid of the (+)/1 operator we can
introduce a directive hypo/1:
:- op(1150, fx, hypo).
term_expansion((:- hypo(F/N)), [(:- dynamic(F/N)),
(H :- shift(in(H)))]) :-
functor(H, F, N).
Now we can run Programming with Higher-Order
Logic, Figure 3.4, as follows:
:- hypo rev/2.
rev([X|Y], Z) :- rev(Y,[X|Z]).
reverse(X,Y) :- (rev([],Y) -: rev(X,[])).
?- run_state(reverse([1,2,3],X),[],_).
X = [3, 2, 1].
Works fine!
Mostowski Collapse schrieb am Mittwoch, 19. April 2023 um 00:57:16 UTC+2:

So lets try this:

run_state_(push(A), Cont, StateIn, StateOut) :- !,
run_state(Cont, [A|StateIn], StateOut).
run_state_(pop, Cont, [_|StateIn], StateOut) :- !,
run_state(Cont, StateIn, StateOut).
run_state_(in(A), Cont, StateIn, StateOut) :- !,
member(A, StateIn),
run_state(Cont, StateIn, StateOut).

And then we can define embedded implication (:-)/2 as
follows. And I am also adopting (+)/1 from @philzock:

:- op(1200, xfy, -:).

(A -: B) :- shift(push(A)), B, shift(pop).

(+ A) :- shift(in(A)).
Lets see whether it works:

/* First Test Case, Communicating Variables, Ok! */
?- run_state((p(X) -: +p(Y)),[],S).
X = Y,
S = [].

/* Second Test Case, Backtracking, Ok! */
?- run_state((p(1) -: p(2) -: +p(X)),[],S).
X = 2,
S = [] ;
X = 1,
S = [].

Works fine! Maybe try the problematic Example 6 and Example 7
from the Bousi~Prolog paper as well.
Mostowski Collapse schrieb am Mittwoch, 19. April 2023 um 00:56:01 UTC+2:

To solve the communicating variables problem, you can use
shift/1 and reset/3 which are available in SWI-Prolog. They are
from the Delimited continuations addition to SWI-Prolog.

The generic approach to use shift/reset for such purposes is:

run_state(Goal, StateIn, StateOut) :-
reset(Goal, Command, Cont),
( Cont == 0 % no more commands from Goal?

StateOut = StateIn

; run_state_(Command, Cont, StateIn, StateOut)
).
You have to define a couple of commands and a state. Lets
say we make a simple prototype, and only model P, the
clause space as a state. Then for embedded implication:

P, A |- B
--------------
P |- A -: B

The state would go from P, to [A|P] and then back to P.
We don’t need undo/1, this is part of shift/reset anyway.

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

Trying the comp.pl from Bousi~Prolog paper, it translates me
the reverse/2 predicate, from Programming with Higher-Order
Logic, Figure 3.4, into:
rev([A|B], C, [], 0, [], D) :-
rev(B, [A|C], _, _, _, D).
rev([], A, [A], 1, [_|_], B) :-
reg(1, [A], C),
chk(C, B).
reverse(A, B, [], 2, [], C) :-
=>([1-[B]], rev(A, [], _, _, _, [D|C]), D, C).
reverse(A, B) :-
reverse(A, B, [], _, _, []).
But it cannot do the query, X doesn’t get instantiated to the result:
?- reverse([1,2,3],X).
true.
So I guess there is still a hick-up with communicating variables after
their 6-th iteration. Maybe there is somewhere a 7-th iteration?
I am refering to this paper:
Planning for an Efficient Implementation of Hypothetical Bousi~Prolog
Pascual Julián-Iranzo - Fernando Sáenz-Pérez
Submitted on 8 Aug 2021
https://arxiv.org/abs/2108.03602
--- Synchronet 3.20a-Linux NewsLink 1.114