Simplification and binarization of Prolog clauses

binary-simple.prolog

% Simplification and binarization of Prolog clauses.
%
% This code was my note paper while reading
% "The BinProlog Experience: Architecture and
% Implementation Choices for Continuation Passing
% Prolog and First-Class Logic Engines" by Paul Tarau.
%
% I find it especially pleasing that binary logic programs
% require only about half as many WAM instructions as
% traditional Prolog.  This should make it easy to build
% an "open WAM instruction set" and have small implementations
% in JavaScript, Go, Prolog, etc.  That would let people run
% the same Prolog code in multiple environments.

append_arg(T0, Arg, T) :-
    T0 =.. L0,
    append(L0,[Arg],L),
    T =.. L.

binarize((Head0:-Body0),(Head:-Body)) :-
    !,
    append_arg(Head0,Cont,Head),
    simplify(Body0,Body1),
    binarize(Body1,Cont,Body).
binarize(Fact,(Fact:-true)).

binarize((A0,B0),Cont,A) :-
    !,
    append_arg(A0,B,A),
    binarize(B0,Cont,B).
binarize((A0;B0),Cont,T) :-
    !,
    binarize(or(A0,B0),Cont,T).
binarize(A0,Cont,A) :-
    append_arg(A0,Cont,A).


simplify(G0,G) :-
    ( simplify_(G0,G1), G0\==G1 -> simplify(G1,G); G=G0 ).

simplify_(G0,G) :-
    pure(G0),
    is_semidet(G0),
    ( call(G0) -> G=true; G=fail ).
simplify_((fail,_),fail).
simplify_((A0,B0),(A,B)) :-
    simplify(A0,A),
    simplify(B0,B).
simplify_((true,G),G).
simplify_((G,true),G).
simplify_((If->Then),(If->Then;fail)).
simplify_((true->Then;_),Then).
simplify_((fail->_;Else),Else).
simplify_((If->true;fail),once(If)).
simplify_((If->Then;_),(once(If),Then)) :-
    will_succeed(If).
simplify_((If0->Then0;Else0),(If->Then;Else)) :-
    simplify(If0,If),
    simplify(Then0,Then),
    simplify(Else0,Else).
simplify_((fail;G),G).
simplify_((G;fail),G).
simplify_((A0;B0),(A;B)) :-
    simplify(A0,A),
    simplify(B0,B).
simplify_(once(G),G) :-
    cardinality(G,_,High),
    High \= many.


pure(_=_).
pure(memberchk(_,_)).
pure(once(G)) :-
    pure(G).
pure(true).
pure(fail).


is_fail(G) :-
    cardinality(G,zero,zero).

is_semidet(G) :-
    cardinality(G,zero,one).

is_nondet(G) :-
    cardinality(G,zero,many).

is_det(G) :-
    cardinality(G,one,one).

is_multi(G) :-
    cardinality(G,one,many).

can_fail(G) :-
    cardinality(G,zero,_).

will_succeed(G) :-
    cardinality(G,Low,_),
    Low \= zero.


cardinality(_=_,zero,one).
cardinality((If->Then),Low,High) :-
    cardinality(If,LowI,_),
    cardinality(Then,LowT,High),
    ( LowI=zero -> Low=zero; Low=LowT ).
cardinality((_->Then;Else),Low,High) :-
    cardinality(Then,LowT,HighT),
    cardinality(Else,LowE,HighE),
    minimum_cardinality(LowT,LowE,Low),
    maximum_cardinality(HighT,HighE,High).
cardinality(fail,zero,zero).
cardinality(memberchk(X,Xs),zero,one) :-
    nonvar(X),
    is_list(Xs).
cardinality(memberchk(X,Xs),one,one) :-
    var(X),
    var(Xs).
cardinality(once(G),Low,Upper) :-
    cardinality(G,L,U),
    ( L=many -> Low=one; Low=L ),
    ( U=many -> Upper=one; Upper=U ).
cardinality(true,one,one).
cardinality(writeln(_),one,one).


minimum_cardinality(L1,L2,L) :-
    once(minc_(L1,L2,L)).
minc_(_,zero,zero).
minc_(zero,_,zero).
minc_(one,_,one).
minc_(_,one,one).
minc_(_,_,many).


maximum_cardinality(L1,L2,L) :-
    once(maxc_(L1,L2,L)).
maxc_(_,many,many).
maxc_(many,_,many).
maxc_(_,one,one).
maxc_(one,_,one).
maxc_(_,_,zero).


or(A,_) :- call(A).
or(_,B) :- call(B).