SWI-Prolog-compatible DCG-ification of Power of Prolog's 'mi_list3' (www.metalevel.at/acomip/)

mi_dcg.pl

% The following is a 3-line meta-interpreter for pure Prolog (no
% cuts/negation). It reifies conjunction and dispatch, leaving
% unification and backtracking implicit. It is written for brevity,
% leveraging DCG notation and using lists to denote conjunctions of
% goals. It implements the semantics of a program (in the sense of a
% set of rules or "immediate consequence operator") as the program's
% least fixed point, obtained by "reflexive transitive closure" /
% exponential / "Kleene iteration".

%%%%%

% Kleene star
star(_) --> {}.
star(P) --> call(P), star(P).

% Meta-interpreter
prove(Goals) :- star(dcg_clause, Goals, []).

% 'Goals' is a conjunction (represented as a list) of goals. The
% empty list [] represents Prolog's 'true'. 'star(dcg_clause, Goals,
% [])' succeeds iff zero or more applications of 'dcg_clause' can
% reduce 'Goals' to []. In other words, 'Goals' must be finitely
% reachable from []. This is the meaning of least fixed point or
% minimal model semantics.

% The definition of 'star' uses '-->' instead of the traditional ':-'
% connective. This is called DCG notation. Basically, '-->' means
% that two extra arguments (thought of as input and output,
% respectively) are implicitly appended to the head and all
% conjuncts. This eliminates unnecessary verbosity. It is analogous to
% Haskell's State monad.

% You can use 'listing' to see how DCG clauses are expanded into
% regular Prolog clauses:
% ?- listing(star).
% star(_, A, A).
% star(P, A, B) :-
%     call(P, A, C),
%     star(P, C, B).

%%%%%

% Here is an example program defining addition and multiplication of
% natural numbers:
dcg_clause, []       --> [nat(0)].
dcg_clause, [nat(N)] --> [nat(s(N))].

dcg_clause, [nat(N)]          --> [add(0, N, N)].
dcg_clause, [add(A, s(B), C)] --> [add(s(A), B, C)].

dcg_clause, [nat(N)]                       --> [mul(0, N, 0)].
dcg_clause, [mul(A, B, C0), add(B, C0, C)] --> [mul(s(A), B, C)].

% The above uses some more features of DCG notation. Intuitively,
% 'dcg_clause, [mul(A, B, C0), add(B, C0, C)] --> [mul(s(A), B, C)]'
% can be read as "if we can derive mul(A, B, C0) and add(B, C0, C)
% then we can derive mul(s(A), B, C)". Operationally, it works
% backwards: it means "if [mul(s(A),B,C)] is a prefix of the current
% list of goals, replace it with [mul(A, B, C0), add(B, C0, C)]",
% which is what we would expect the analogous Prolog clause to do.

% This is the expanded form, which makes the operation obvious (first
% arg is the before state, second arg is the after state):
% ?- listing(dcg_clause).
% dcg_clause([nat(0)|A],          B) :- B=A. % Impl detail: 'dcg_clause --> [nat(0)]' would expand to the simpler 'dcg_clause([nat(0)|A], A)'.
% dcg_clause([nat(s(A))|B],       [nat(A)|B]).
% dcg_clause([add(0, A, A)|B],    [nat(A)|B]).
% dcg_clause([add(s(A), B, C)|D], [add(A, s(B), C)|D]).
% dcg_clause([mul(0, A, 0)|B],    [nat(A)|B]).
% dcg_clause([mul(s(A), B, C)|D], [mul(A, B, E), add(B, E, C)|D]).

%%%%%

demo :-
    Goal = mul(A, s(A), B),
    prove([Goal]),
    writeln(A * s(A) = B).

%% ?- demo.
%% 0*s(0)=0
%% true ;
%% s(0)*s(s(0))=s(s(0))
%% true ;
%% s(s(0))*s(s(s(0)))=s(s(s(s(s(s(0))))))
%% true ;
%% s(s(s(0)))*s(s(s(s(0))))=s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))
%% true