Pure Prolog Scheme Quine

Question

There is this paper:

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

Which uses logic programming to find a Scheme Quine. The Scheme subset that is consider here does not only contain lambda abstraction and application, but also a little list processing by the following reduction, already translated to Prolog:

[quote,X] ~~> X
[] ~~> []                                      
[cons,X,Y] ~~> [A|B], for X ~~> A and Y ~~> B

So the only symbols are quote, [] and cons, besides lembda for lambda abstraction and bound variables. And we would use Prolog lists for the Scheme lists. The goal is to find a Scheme programm Q via Prolog, so that we get Q ~~> Q, i.e. evaluates to itself.

There is one complication, which makes the endeavour non-trival, [lembda,X,Y] doesn't evaluate syntactically to itself, but is rather supposed to return an environment closure. So the evaluator would be unlike the Plotkin evaluator here.

Any Prolog solutions around? Merry X-Mas

Answer 1

I'm using SWI Prolog with the occurs check turned on here (but dif/2 skips the occurs check anyway):

symbol(X) :- freeze(X, atom(X)).

symbols(X) :- symbol(X).

symbols([]).

symbols([H|T]) :-
    symbols(H),
    symbols(T).

% lookup(X, Env, Val).
%
% [quote-unbound(quote)] will be the empty environment
% when unbound(quote) is returned, this means that
% `quote` is unbound

lookup(X, [X-Val|_], Val).

lookup(X, [Y-_|Tail], Val) :- 
    dif(X, Y),
    lookup(X, Tail, Val).

% to avoid name clashing with `eval`
%
% evil(Expr, Env, Val).

evil([quote, X], Env, X) :-
    lookup(quote, Env, unbound(quote)),
    symbols(X).

evil(Expr, Env, Val) :-
    symbol(Expr),
    lookup(Expr, Env, Val),
    dif(Val, unbound(quote)).

evil([lambda, [X], Body], Env, closure(X, Body, Env)).

evil([list|Tail], Env, Val) :-
    evil_list(Tail, Env, Val).

evil([E1, E2], Env, Val) :- 
    evil(E1, Env, closure(X, Body, Env1_Old)),
    evil(E2, Env, Arg), 
    evil(Body, [X-Arg|Env1_Old], Val).

evil([cons, E1, E2], Env, Val) :-
    evil(E1, Env, E1E),
    evil(E2, Env, E2E),
    Val = [E1E | E2E].

evil_list([], _, []).
evil_list([H|T], Env, [H2|T2]) :-
    evil(H, Env, H2), evil_list(T, Env, T2).

% evaluate in the empty environment

evil(Expr, Val) :-
    evil(Expr, [quote-unbound(quote)], Val).

Tests:

Find Scheme expressions that eval to (i love you) -- this example has a history in miniKanren:

?- evil(X, [i, love, you]), print(X).
[quote,[i,love,you]]
X = [quote, [i, love, you]] ;
[list,[quote,i],[quote,love],[quote,you]]
X = [list, [quote, i], [quote, love], [quote, you]] ;
[list,[quote,i],[quote,love],[[lambda,[_3302],[quote,you]],[quote,_3198]]]
X = [list, [quote, i], [quote, love], [[lambda, [_3722], [quote|...]], [quote, _3758]]],
dif(_3722, quote),
freeze(_3758, atom(_3758)) ;
[list,[quote,i],[quote,love],[[lambda,[_3234],_3234],[quote,you]]]
X = [list, [quote, i], [quote, love], [[lambda, [_3572], _3572], [quote, you]]],
freeze(_3572, atom(_3572)) ;

In other words, the first 4 things it finds are:

(quote (i love you))

(list (quote i) (quote love) (quote you))

(list (quote i) (quote love) ((lambda (_A) (quote you)) (quote _B)))
; as long as _A != quote

(list (quote i) (quote love) ((lambda (_A) _A) (quote you))) 
; as long as _A is a symbol

It looks like the Scheme semantics are correct. The language-lawyer type of constraints it places are pretty neat. Indeed, real Scheme will refuse

> (list (quote i) (quote love) ((lambda (quote) (quote you)) (quote _B)))
Exception: variable you is not bound
Type (debug) to enter the debugger.

but will accept

> (list (quote i) (quote love) ((lambda (quote) quote) (quote you)))
(i love you)

So how about quines?

?- evil(X, X).
<loops>

miniKanren uses BFS, so maybe that's why it produces results here. With DFS, this could work (assuming there are no bugs):

?- call_with_depth_limit(evil(X, X), n, R).

or

?- call_with_inference_limit(evil(X, X), m, R).

but SWI doesn't necessarily limit the recursion with call_with_depth_limit.

Answer 2

Here is a solution that uses a little blocking programming style. Its not using when/2, rather only freeze/2. There is one predicate expr/2 which checks whether something is a proper expression without any closure in it:

expr(X) :- freeze(X, expr2(X)).

expr2([X|Y]) :-
   expr(X),
   expr(Y).
expr2(quote).
expr2([]).
expr2(cons).
expr2(lambda).
expr2(symbol(_)).

And then there is a lookup predicate again using freeze/2,
to wait for an environment list.

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).

And finally the evaluator, which is coded using DCG,
to limit the total number of cons and apply invokations:

eval([quote,X], _, X) --> [].
eval([], _, []) --> [].
eval([cons,X,Y], E, [A|B]) -->
   step,
   eval(X, E, A),
   eval(Y, E, B).
eval([lambda,symbol(X),B], E, closure(X,B,E)) --> [].
eval([X,Y], E, R) -->
   step,
   eval(X, E, closure(Z,B,F)),
   eval(Y, E, A),
   eval(B, [Z-A|F], R).
eval(symbol(S), E, R) -->
   {lookup(S, E, R)}.

step, [C] --> [D], {D > 0, C is D-1}.

The main predicate gradually increases the number of allowed
cons and apply invokations:

quine(Q, M, N) :-
   expr(Q),
   between(0, M, N),
   eval(Q, [], P, [N], _),
   unify_with_occurs_check(Q, P).

This query shows that 5 cons and apply invokations are enough to produce a Quine. Works in SICStus Prolog and Jekejeke Prolog. For SWI-Prolog need to use for example this unify/2 workaround:

?- dif(Q, []), quine(Q, 6, N).
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, []]]]]]],
N = 5 

We can manually verify that it is indeed a non-trivial Quine:

?- 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], _).
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, []]]]]]],
P = [[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, []]]]]]] 

Answer 3

One might ask whether an occurs check flag is superior to an explicit unify_with_occurs_check/2. In the solution with explicit unify_with_occurs_check/2 we have placed one such call in lookup2/3 and in quine/3. If we use an occurs check flag, we do not need to manually place such calls and can rely on the dynamics of the Prolog interpreter.

We removed the explicit unify_with_occurs_check/2 in lookup2/3:

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

And also in quine/3, making it less generate and test, and more constraint logic like. Using the same variable Q twice acts like a constraint that is pushed into the execution:

quine(Q, M, N) :-
   expr(Q),
   between(0, M, N),
   eval(Q, [], Q, [N], _).

Here are some results for the new SWI-Prolog 8.3.17, which got its unify_with_occurs_check/2 fixed to gether with zhe occurs check flag fixed:

/* explicit unify_with_occurs_check/2 */
?- time((dif(Q, []), quine(Q, 6, N))).
% 208,612,270 inferences, 11.344 CPU in 11.332 seconds (100% CPU, 18390062 Lips)

/* occurs_check=true */
?- time((dif(Q, []), quine(Q, 6, N))).
% 48,502,916 inferences, 2.859 CPU in 2.859 seconds (100% CPU, 16962768 Lips)

And also a preview for the upcoming Jekejeke Prolog 1.4.7, which will also feature an occurs check flag:

/* explicit unify_with_occurs_check/2 */
?- time((dif(Q, []), quine(Q, 6, N))).
% Up 37,988 ms, GC 334 ms, Threads 37,625 ms (Current 01/10/21 01:29:35)

/* occurs_check=true */
?- time((dif(Q, []), quine(Q, 6, N))).
% Up 13,367 ms, GC 99 ms, Threads 13,235 ms (Current 01/10/21 01:35:24)

Quite amazing that the occurs check flag can lead to a 3-fold spead-up in both Prolog systems! The result is possibly indicative the way we explicitly placed unify_with_occurs_check/2 was faulty?

BTW: Open source:

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