next up previous
Next: Foldl Up: Generalising Both Approaches Previous: Polymorphic Types and Higher

Flexible Modes

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.

next up previous
Next: Foldl Up: Generalising Both Approaches Previous: Polymorphic Types and Higher
Lee Naish