• Reifying backtracking for Haskell programmers

    From Mild Shock@janburse@fastmail.fm to comp.lang.prolog on Mon Feb 26 01:37:50 2024
    From Newsgroup: comp.lang.prolog

    One buzzword that Markus Triska is using is:

    Reifying backtracking
    https://www.metalevel.at/acomip/

    But he is more up to meta interpreters.

    Can we turn the whole thing into something small step?

    Here is a take:

    % step(+Bool, +List, +List, -Bool, -List, -List)
    step(true, [write(Term)|Cont], CPs, true, Cont, CPs) :- !, write(Term). step(true, [nl|Cont], CPs, true, Cont, CPs) :- !, nl.
    step(true, [Goal|Cont], CPs, Flag, Cont2, CPs2) :-
    findall(Goal-Body, rule(Goal, Body), Pairs),
    pick(Pairs, [Goal|Cont], CPs, Flag, Cont2, CPs2).
    step(fail, _, [Pairs-Cont|CPs], Flag, Cont2, CPs2) :-
    pick(Pairs, Cont, CPs, Flag, Cont2, CPs2).

    % pick(+Bool, +List, +List, -Bool, -List, -List)
    pick([], Cont, CPs, fail, Cont, CPs).
    pick([Goal-Body|Pairs], Cont, CPs, true, Cont3, [Pairs-Cont|CPs]) :-
    copy_term(Cont, [Goal|Cont2]),
    append(Body, Cont2, Cont3).

    % run(+Bool, +List, +List)
    run(Flag, Cont, CPs) :-
    step(Flag, Cont, CPs, Flag2, Cont2, CPs2),
    run(Flag2, Cont2, CPs2).

    It only carries around a state consisting of flag for CALL
    or REDO, and the continuations and the choicepoints. The meaning
    of the transformed flag is EXIT or FAIL.
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Mild Shock@janburse@fastmail.fm to comp.lang.prolog on Mon Feb 26 01:38:32 2024
    From Newsgroup: comp.lang.prolog


    Does it work?

    t assumes the rules and facts in a predicate rule/2, here an example:

    % rule(-Term, -List)
    :- dynamic rule/2.
    rule(app([], X, X), []).
    rule(app([X|Y], Z, [X|T]), [app(Y, Z, T)]).

    rule(rev([], []), []).
    rule(rev([X|Y], Z), [rev(Y,T),app(T,[X],Z)]).
    Works fine:

    ?- run(true, [app(X,Y,[1,2,3]),write(('X'=X,'Y'=Y)),nl,fail], []). X=[],Y=[1,2,3]
    X=[1],Y=[2,3]
    X=[1,2],Y=[3]
    X=[1,2,3],Y=[]
    false.

    ?- run(true, [rev([1,2,3],X),write('X'=X),nl,fail], []).
    X=[3,2,1]
    false.

    Mild Shock schrieb:
    One buzzword that Markus Triska is using is:

    Reifying backtracking
    https://www.metalevel.at/acomip/

    But he is more up to meta interpreters.

    Can we turn the whole thing into something small step?

    Here is a take:

    % step(+Bool, +List, +List, -Bool, -List, -List)
    step(true, [write(Term)|Cont], CPs, true, Cont, CPs) :- !, write(Term). step(true, [nl|Cont], CPs, true, Cont, CPs) :- !, nl.
    step(true, [Goal|Cont], CPs, Flag, Cont2, CPs2) :-
       findall(Goal-Body, rule(Goal, Body), Pairs),
       pick(Pairs, [Goal|Cont], CPs, Flag, Cont2, CPs2).
    step(fail, _, [Pairs-Cont|CPs], Flag, Cont2, CPs2) :-
       pick(Pairs, Cont, CPs, Flag, Cont2, CPs2).

    % pick(+Bool, +List, +List, -Bool, -List, -List)
    pick([], Cont, CPs, fail, Cont, CPs).
    pick([Goal-Body|Pairs], Cont, CPs, true, Cont3, [Pairs-Cont|CPs]) :-
       copy_term(Cont, [Goal|Cont2]),
       append(Body, Cont2, Cont3).

    % run(+Bool, +List, +List)
    run(Flag, Cont, CPs) :-
       step(Flag, Cont, CPs, Flag2, Cont2, CPs2),
       run(Flag2, Cont2, CPs2).

    It only carries around a state consisting of flag for CALL
    or REDO, and the continuations and the choicepoints. The meaning
    of the transformed flag is EXIT or FAIL.

    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Mild Shock@janburse@fastmail.fm to comp.lang.prolog on Mon Feb 26 01:39:22 2024
    From Newsgroup: comp.lang.prolog


    But what does it do?

    A step goes through the Byrd Box, just like a Prolog debugger:

    The Byrd Box Model And Ports
    models each predicate in a Prolog program as a
    state machine (“box”) that transitions through
    states (“ports”) as a program is evaluated. https://www.swi-prolog.org/pldoc/man?section=byrd-box-model

    Mild Shock schrieb:

    Does it work?

    t assumes the rules and facts in a predicate rule/2, here an example:

    % rule(-Term, -List)
    :- dynamic rule/2.
    rule(app([], X, X), []).
    rule(app([X|Y], Z, [X|T]), [app(Y, Z, T)]).

    rule(rev([], []), []).
    rule(rev([X|Y], Z), [rev(Y,T),app(T,[X],Z)]).
    Works fine:

    ?- run(true, [app(X,Y,[1,2,3]),write(('X'=X,'Y'=Y)),nl,fail], []). X=[],Y=[1,2,3]
    X=[1],Y=[2,3]
    X=[1,2],Y=[3]
    X=[1,2,3],Y=[]
    false.

    ?- run(true, [rev([1,2,3],X),write('X'=X),nl,fail], []).
    X=[3,2,1]
    false.

    Mild Shock schrieb:
    One buzzword that Markus Triska is using is:

    Reifying backtracking
    https://www.metalevel.at/acomip/

    But he is more up to meta interpreters.

    Can we turn the whole thing into something small step?

    Here is a take:

    % step(+Bool, +List, +List, -Bool, -List, -List)
    step(true, [write(Term)|Cont], CPs, true, Cont, CPs) :- !, write(Term).
    step(true, [nl|Cont], CPs, true, Cont, CPs) :- !, nl.
    step(true, [Goal|Cont], CPs, Flag, Cont2, CPs2) :-
        findall(Goal-Body, rule(Goal, Body), Pairs),
        pick(Pairs, [Goal|Cont], CPs, Flag, Cont2, CPs2).
    step(fail, _, [Pairs-Cont|CPs], Flag, Cont2, CPs2) :-
        pick(Pairs, Cont, CPs, Flag, Cont2, CPs2).

    % pick(+Bool, +List, +List, -Bool, -List, -List)
    pick([], Cont, CPs, fail, Cont, CPs).
    pick([Goal-Body|Pairs], Cont, CPs, true, Cont3, [Pairs-Cont|CPs]) :-
        copy_term(Cont, [Goal|Cont2]),
        append(Body, Cont2, Cont3).

    % run(+Bool, +List, +List)
    run(Flag, Cont, CPs) :-
        step(Flag, Cont, CPs, Flag2, Cont2, CPs2),
        run(Flag2, Cont2, CPs2).

    It only carries around a state consisting of flag for CALL
    or REDO, and the continuations and the choicepoints. The meaning
    of the transformed flag is EXIT or FAIL.


    --- Synchronet 3.20a-Linux NewsLink 1.114