Scheme Quine in Pure Prolog

The name “quine” was coined by Douglas Hofstadter, in his popular science book Gödel, Escher, Bach, in honor of philosopher Willard Van Orman Quine (1908–2000), who made an extensive study of indirect self-reference. We try to find a Scheme quine in pure Prolog.

The problem can be formulated in pure Prolog as finding a Scheme program Q such that Q ~~> Q succeeds. The programming will lead us into the realm of the occurs check in logic programming. The occurs check is a part of algorithms for syntactic unification.

Occurs Check

The ISO core standard requires the predicate unify_with_occurs_check/2. This predicate performs syntactic unification with occurs check. We will need that, since we want our Scheme programs to be acyclic terms. The effect of the occurs check is seen by the following query:

?- unify_with_occurs_check(X, f(X)).
No

On the other hand the ISO core standard does not require that the built-in (=)/2 and clause head unification performs an occurs check. The behaviour is left implementation dependent. A few Prolog systems have now started providing a Prolog flag to control the behavior:

?- X = f(X).
X = <cyclic term>

?- set_prolog_flag(occurs_check, true).
Yes

?- X = f(X).
No

The flag is not mandated by the ISO core standard. But we will make a case for such a flag, and show that a flag can be efficiently implemented and is then superior to an explicit call into the unify_with_occurs_check/2 built-in.

Explicit Solution

We will redo the following computer experiment originally executed for miniKanren. We will first realize an evaluator for toy Scheme in pure Prolog using explicit occurs check calls. Link to the full source code is found at the end of the post.

William E. Byrd, Eric Holk, Daniel P. Friedman, 2012
miniKanren, Live and Untagged
Quine Generation via Relational Interpreters
http://webyrd.net/quines/quines.pdf

The code uses blocking programming style. We use freeze/2 to wait for a variable get unified with a non-variable term. This makes the code excution not anymore stricly serial, rather constraints can be check via non-parallel coroutines. We show the lookup predicate with explicit occurs check:

lookup(S, E, R) :- freeze(E, lookup2(S, E, R)).

lookup2(S, [S-T|_], R) :-
   unify_with_occurs_check(T, R).
lookup2(S, [T-_|E], R) :-
   dif(S, T),
   lookup(S, E, R).

As can be seen we also use the dif/2 constraint, our code will not contain any cut making it pure. For iterative deepening we use DCG to count down the a given inference counter. A solution is searched by gradually incrementing the maximum inference count.

Flag Solution

The flag solution is quickly explained. Instead of relying on the explicit unify with occurs check, we rely on ordinary unification. We even did eliminate any (=)/2 calls by for example moving a variable into the head of a clause as can be seen here:

lookup2(S, [S-T|_], T).
lookup2(S, [T-_|E], R) :-
   dif(S, T),
   lookup(S, E, R).

A link of the full Prolog text of the second variant is as well found at the end of this post. Both programs find the same quine. It can be easily verified that they find as first the following quine, which is indeed a quine. The following query will return in P the input Q:

?- Q = [[lambda, symbol(_Q), [cons, symbol(_Q), [cons, [cons, 
[quote, quote], [cons, symbol(_Q), [quote, []]]], [quote, 
[]]]]], [quote, [lambda, symbol(_Q), [cons, symbol(_Q), [cons, 
[cons, [quote, quote], [cons, symbol(_Q), [quote, []]]], 
[quote, []]]]]]], eval(Q, [], P, [5], _).

Performance Results

We might now ask whether there is an advantage of one approach over the other. To get more insight into this question we performed some performance measures using SWI-Prolog and the upcoming release of Jekejeke Prolog. The ca. 33% time reduction for both Prolog systems is seen here:

We attribute this positive result in that an occurs check flag relieves the programmer from the burden of placing unify with occurs check calls. In the explicit scenario, to solve the quine problem we simply called eval(Q,[],P), unify_with_occurs_check(Q,P), which gives a costly generate and test.

On the other hand in the occurs check flag scenario, we could directly call eval(Q,[],Q) making the equality between the first and third argument of the eval/3 predicate a constraint, that is pushed into the generation phase of our eval/3 predicate. Thus pruning the search more earlier.

Quine Generation via Relational Interpreters
explicit unify_with_occurs_check/2
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine-pl

Quine Generation via Relational Interpreters
occurs_check=true
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine2-pl