2

I wonder whether there is a pure Prolog meta-interpreter with only one rule. The usual Prolog vanilla meta-interpreter has two rules. It reads as follows:

solve(true).
solve((A, B)) :- solve(A), solve(B). /* rule 1 */
solve(H) :- program(H, B), solve(B). /* rule 2 */

This Prolog vanilla meta-interpreter uses two rules /* rule 1 */ and /* rule 2 */. And the rest is facts. The program that is executed is represented by program facts. Here is an example program:

program(append([], X, X), true).
program(append([X|Y], Z, [X|T]), append(Y, Z, T)).
program(nrev([], []), true).
program(nrev([H|T], R), (nrev(T, S), append(S, [H], R))).

And an example query:

?- solve(nrev([1,2,3], X)).
X = [3, 2, 1] .

Is there a way to represent the program differently as facts, and then code a different meta-interpreter, which would use only facts except for a single rule instead of two rules? Something that would work for all pure Prolog programs, not only the nrev example?

false
  • 10,264
  • 13
  • 101
  • 209
  • What's your definition of "pure"? Is `;/2` acceptable? – MWB Dec 23 '20 at 15:29
  • The meta interpreter need only understand true, (,)/2 and atomic formulas. (;)/2 could be defined as two facts program((A;_), A). program((_;B),B). –  Dec 23 '20 at 15:31
  • I forgot to say, that a Horn clause rule doesn't have (;)/2 in the body. So you cannot use (;)/2 in the definition of your solve. Otherwise the problem is too easy. –  Dec 23 '20 at 15:38

3 Answers3

3

Here is one idea, using a list to hold the rest of the computation:

solve([]).
solve([X|Xs]) :- program(X, Ys, Xs), solve(Ys).

program(true, Xs, Xs).
program(append([],X,X), Xs, Xs).
program(append([X|Y], Z, [X|T]), [append(Y,Z,T)|Xs], Xs).
program(nrev([],[]), Xs, Xs).
program(nrev([H|T],R), [nrev(T,S),append(S,[H],R)|Xs], Xs).

With test call (where one needs to wrap the call in a list).

?- solve([nrev([1,2,3],X)]).
X = [3,2,1] ? ;
no

Arguably, one could represent the program/3 facts as a DCG instead, for increased readability (but then it might not be considered a "fact" any more).

jnmonette
  • 1,794
  • 4
  • 7
  • Brilliant, I think there is even a paper by some J... which discussed this some decades ago, and the approach is named after him. If I have time I will pick up the reference. –  Dec 23 '20 at 16:44
  • This meta-interpreter reifies conjunction. – false Dec 23 '20 at 19:33
  • ... and it is the essence of binarization. – false Dec 23 '20 at 19:35
  • @false Can you explain what you mean by binarization in this context? Not sure I understand the term... Thanks! – jnmonette Dec 24 '20 at 06:30
  • 1
    Binarization is a transformation from Prolog towards a subset called [Binary Prolog](https://duckduckgo.com/?q=%22Binary+Prolog%22+Paul+Tarau) which is somewhat simpler to implement. The essence is that general conjunction is reified (just as you did it). – false Dec 24 '20 at 08:32
0

Here is another approach, known as binarization with continuation.
Its from this logic transformers paper here by Paul Tarau (2021).

solve(true).
solve(X) :- program(X, Y), solve(Y).

program(append([],X,X,C), C).
program(append([X|Y],Z,[X|T],C), append(Y,Z,T,C)).
program(nrev([],[],C), C).
program(nrev([H|T],R,C), nrev(T,S,append(S,[H],R,C))).

A little sanity check shows that it wurks:

?- solve(nrev([1,2,3], X, true)).
X = [3, 2, 1] ;
No
-1

If ;/2 is allowed, then this seems to work:

solve(true).
solve(H) :- ((X, Y) = H, solve(X), solve(Y)); (program(H :- B), solve(B)).

program(append([], X, X) :- true).
program(append([X|Y], Z, [X|T]) :- append(Y, Z, T)).
program(nrev([], []) :- true).
program(nrev([H|T], R) :- (nrev(T, S), append(S, [H], R))).

Test:

?- solve(nrev([1,2,3], X)).
X = [3, 2, 1] ;
false.
MWB
  • 11,740
  • 6
  • 46
  • 91
  • (This answer was posted before OP stated `;/2` was not allowed. Most people consider it "pure Prolog") – MWB Dec 23 '20 at 23:01