I recently have been looking to make a Prolog meta-interpreter with a certain set of features, but I am starting to see that I don't have the theoretical knowledge to work on it.
The features are as follows :
Obviously, (3) and (4) are the ones I am having problems with. I am not sure if those 2 features are compatible. I am not even sure if there is a way to define complexity such that (4) makes logical sense.
In my researches, I have come across the concept of "unavoidable pattern", which, I believe, provides a way to ensure feature (3), as long as feature (4) has a well-formed definition.
I specifically want to know if this kind of interpreter has been proven impossible, and, if not, if theoretical or concrete work on similar interpreters has been done in the past.
Provided the above features are possible to implement, I have extra features I want to add, and would be grateful if you could enlighten me on the feasibility of such features as well :
Here is a simple predicate that obviously results in infinite recursion in a normal Prolog interpreter in all but the simplest of cases. This interpreter should be able to evaluate it in at most PSPACE (and, I believe, at most P if (6) is possible to implement), while still giving relevant results.
eq(E, E).
eq(E, F):- eq(E,F0), eq(F0,F).
eq(A + B, AR + BR):- eq(A, AR), eq(B, BR).
eq(A + B, B + A).
eq(A * B, B * A).
eq((A * B) / B, A).
eq(E, R):- eq(R, E).
Example of results expected :
?- eq((a + c) + b, b + (c + a)).
true.
?- eq(a, (a * b) / C).
C = b.
The fact that this kind of interpreter might prove useful by the provided example hints me towards the fact that such an interpreter is probably impossible, but, if it is, I would like to be able to understand what makes it impossible (for example, does (3) + (4) reduce to the halting problem? is (6) NP?).
If you want to guarantee termination you can conservatively assume any input goal is nonterminating until proven otherwise, using a decidable proof procedure. Basically, define some small class of goals which you know halt, and expand it over time with clever ideas.
Here are three examples, which guarantee or force three different kinds of termination respectively (also see the Power of Prolog chapter on termination):
In the following, halts(Goal) is assumed to correctly test a goal for existential-existential termination.
This uses halts/1 to prove existential termination of a modest class of goals. The current evaluator eval/1 just falls back to the underlying engine:
halts(halts(_)).
eval(Input) :- Input.
:- \+ \+ halts(halts(eval(_))).
safe_eval(Input) :-
halts(eval(Input)),
eval(Input).
?- eval((repeat, false)).
C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- safe_eval((repeat, false)).
false.
The optional but highly recommended goal directive \+ \+ halts(halts(eval(_))) ensures that halts will always halt when run on eval applied to anything.
The advantage of splitting the problem into a termination checker and an evaluator is that the two are decoupled: you can use any evaluation strategy you want. halts can be gradually augmented with more advanced methods to expand the class of allowed goals, which frees up eval to do the same, e.g. clause reordering based on static/runtime mode analysis, propagating failure, etc. eval can itself expand the class of allowed goals by improving termination properties which are understood by halts.
One caveat - inputs which use meta-logical predicates like var/1 could subvert the goal directive. Maybe just disallow such predicates at first, and again relax the restriction over time as you discover safe patterns of use.
This example uses a meta-interpreter, adapted from the Power of Prolog chapter on meta-interpreters, to prune off branches which can't be proven to existentially terminate:
eval(true).
eval((A,B)) :- eval(A), eval(B).
eval((A;_)) :- halts(eval(A)), eval(A).
eval((_;B)) :- halts(eval(B)), eval(B).
eval(g(Head)) :-
clause(Head, Body),
halts(eval(Body)),
eval(Body).
So here we're destroying branches, rather than refusing to evaluate the goal.
For improved efficiency, you could start by naively evaluating the input goal and building up per-branch sets of visited clause bodies (using e.g. clause/3), and only invoke halts when you are about to revisit a clause in the same branch.
The above meta-interpreter rules out at least all the diverging branches, but may still have an infinite number of individually terminating branches. If we want to ensure universal termination we can again do everything before entering eval, as in the existential-existential variation:
...
:- \+ \+ halts(halts(\+ \+ eval(_))).
...
safe_eval(Input) :-
halts(\+ \+ eval(Input)),
eval(Input).
So we're just adding in universal quantification.
One interesting thing you could try is running halts itself using eval. This could yield speedups, better termination properties, or qualitatively new capabilities, but would of course require the goal directive and halts to be written according to eval's semantics. E.g. if you remove double negations then \+ \+ would not universally quantify, and if you propagate false or otherwise don't conform to the default left-to-right strategy then the (goal, false) test for universal termination (PoP chapter on termination) also would not work.