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.

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.

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.

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