As well as allowing flexibility with types and nondeterminism, logic programs allow flexibility with modes. Rather than having fixed inputs and one output, as in functional programs, logic programs can potentially be run backwards -- computing what would normally be considered the input from a given output. This flexibility can extend to higher order predicates, including those generated automatically from skeletons.
As an example, we will construct a meta interpreter for Prolog by using
foldrrt/4 backwards. A Prolog proof tree can be represented by
an rtree, where each node contains (the representation of) a
Prolog atom which succeeded. The foldrrt/4 procedure can be used
to check that an rtree of atoms is a valid proof tree for a particular
program and goal. A proof tree is valid if the atom in the root is the
goal and for each node in the tree containing atom A and
children B1,B2,..., there is a program clause instance
A:-B1,B2,.... The proof_of/2 procedure in Program
13 represents
clauses as a head plus a list of body atoms (procedure lclause/2)
and can check that an rtree is a valid proof tree and return the atom
which has been proved.
% Checks Proof is a valid proof tree and returns proved Atom;
% run backwards its a meta interpreter returning a proof tree
proof_of(Proof, Atom) :-
foldrrt(lclause2, cons, [], Proof, Atom).
% checks H :- B is a clause instance; returns H
lclause2(H, B, H) :- lclause(H, B).
% clause/2 where clause bodies are lists lclause(append([],A,A), []). lclause(append([A|B],C,[A|D]), [append(B,C,D)]). lclause(append3(A,B,C,D), [append(A,B,E),append(E,C,D)]). ... cons(H, T, [H|T]).Program 13: Interpreter constructed using rtree
With a suitable evaluation order, the code can also be run backwards.
Given an atom, foldrrt/4 acts as a meta interpreter,
(nondeterministically) returning a proof tree for (a computed instance of)
the atom. This is an example of constructing a program based on the type of
its output, as discussed earlier. By utilising the natural association
between a type and foldr and the flexible modes of logic
programming, much of the process can be automated.