handling the cut with a simple meta-interpreter

117 views Asked by At

The following is a simple meta-interpreter, as seen in many guides/textbooks.

prove(true) :- !.
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- clause(H,B), prove(B),
   write(H), write(" <- "), writeln(B).

The following is a simple program to test the meta-interpreter with.

% parent facts
parent(john, jane).
parent(john, james).
parent(sally, jane).
parent(martha, sally).
parent(deirdre, martha).

% ancestor recursive definition
ancestor(X,Y) :- parent(X,Y), !.
ancestor(X,Y) :- parent(X,A), ancestor(A,Y).

The meta-interpreter works for programs that are simple facts. It also works for simple deduction. However it fails when the program uses a cut.

?- prove(ancestor(martha, jane)).

parent(martha,sally) <- true
parent(sally,jane) <- true
No permission to access private_procedure `!/0'
In:
   [6] clause(!,_692)
   [5] prove(!) at  line 20
   [3] prove(ancestor(sally,jane)) at  line 20
   [1] prove(ancestor(martha,jane)) at  line 20

Question: Is there a simple way to handle cuts in the programs that the meta-interpreter is trying to run?

I know how to extend the meta-interpreter to handle additional syntax, eg the following adds the ability handle \+ thanks to the answer here: negation \+ and vanilla meta-interpreter

prove(true) :- !.
prove((A,B)):- !, prove(A), prove(B).
prove(\+ A) :- !, \+ prove(A). %%% handling \+
prove(H) :- clause(H,B), prove(B),
   write(H), write(" <- "), writeln(B).
0

There are 0 answers