问题描述
有这篇论文：
威廉 E.伯德、埃里克霍尔克、丹尼尔 P.弗里德曼，2012
迷你看人，直播和无标签
通过关系解释器生成奎因
http://webyrd.net/quines/quines.pdf
它使用逻辑编程来查找 Scheme Quine。这 此处考虑的方案子集不仅包含 lambda 抽象和应用，还有一点列表处理 通过以下缩减，已翻译为 Prolog：
[quote,X] ~~> X
[] ~~> []
[cons,X,Y] ~~> [A|B],for X ~~> A and Y ~~> B
所以唯一的符号是引用、[] 和 cons，除了 lembda for lambda 抽象和绑定变量。我们将使用 Prolog Scheme 列表的列表。目标是找到一个Scheme 通过 Prolog 编程 Q，这样我们得到 Q ~~> Q，即对自身求值。
有一个复杂的问题，这使得努力变得不平凡， [lembda,Y] 不对其自身进行语法评估，而是 应该返回一个环境关闭。所以评估者将是 与 Plotkin 评估器 here 不同。
周围有任何 Prolog 解决方案吗？圣诞快乐
解决方法
我正在使用 SWI Prolog 并在此处打开发生检查（但 dif/2 无论如何都会跳过发生检查）：
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,Val).
evil([quote,X],X) :-
lookup(quote,unbound(quote)),symbols(X).
evil(Expr,Val) :-
symbol(Expr),lookup(Expr,Val),dif(Val,unbound(quote)).
evil([lambda,[X],Body],closure(X,Body,Env)).
evil([list|Tail],Val) :-
evil_list(Tail,Val).
evil([E1,E2],Val) :-
evil(E1,Env1_Old)),evil(E2,Arg),evil(Body,[X-Arg|Env1_Old],Val).
evil([cons,E1,Val) :-
evil(E1,E1E),E2E),Val = [E1E | E2E].
evil_list([],_,[]).
evil_list([H|T],[H2|T2]) :-
evil(H,H2),evil_list(T,T2).
% evaluate in the empty environment
evil(Expr,Val) :-
evil(Expr,[quote-unbound(quote)],Val).
测试：
查找 eval 为 (i love you) 的 Scheme 表达式——这个例子在 miniKanren 中有一段历史：
?- evil(X,[i,love,you]),print(X).
[quote,you]]
X = [quote,you]] ;
[list,[quote,i],love],you]]
X = [list,[[lambda,[_3302],you]],_3198]]]
X = [list,[_3722],[quote|...]],_3758]]],dif(_3722,quote),freeze(_3758,atom(_3758)) ;
[list,[_3234],_3234],you]]]
X = [list,[_3572],_3572],you]]],freeze(_3572,atom(_3572)) ;
换句话说，它找到的前 4 件事是：
(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
看起来 Scheme 语义是正确的。它放置的语言律师类型的限制非常整洁。确实，真正的Scheme会拒绝
> (list (quote i) (quote love) ((lambda (quote) (quote you)) (quote _B)))
Exception: variable you is not bound
Type (debug) to enter the debugger.
但会接受
> (list (quote i) (quote love) ((lambda (quote) quote) (quote you)))
(i love you)
那么奎因怎么样？
?- evil(X,X).
<loops>
miniKanren 使用 BFS，所以也许这就是它在这里产生结果的原因。使用 DFS，这可以工作（假设没有错误）：
?- call_with_depth_limit(evil(X,X),n,R).
或
?- call_with_inference_limit(evil(X,m,R).
但 SWI 不一定用 call_with_depth_limit 限制递归。
这是一个使用一点blocking programming style的解决方案。它不使用 when/2，而只使用 freeze/2。有一个谓词 expr/2 用于检查某事物是否是一个没有任何闭包的正确表达式：
expr(X) :- freeze(X,expr2(X)).
expr2([X|Y]) :-
expr(X),expr(Y).
expr2(quote).
expr2([]).
expr2(cons).
expr2(lambda).
expr2(symbol(_)).
然后再次使用freeze/2进行查找谓词，
等待环境列表。
lookup(S,E,R) :- freeze(E,lookup2(S,R)).
lookup2(S,[S-T|_],R) :-
unify_with_occurs_check(T,R).
lookup2(S,[T-_|E],R) :-
dif(S,T),lookup(S,R).
最后是使用 DCG 编码的评估器，
限制 cons 的总数并应用调用：
eval([quote,X) --> [].
eval([],[]) --> [].
eval([cons,X,Y],[A|B]) -->
step,eval(X,A),eval(Y,B).
eval([lambda,symbol(X),B],B,E)) --> [].
eval([X,R) -->
step,closure(Z,F)),eval(B,[Z-A|F],R).
eval(symbol(S),R) -->
{lookup(S,R)}.
step,[C] --> [D],{D > 0,C is D-1}.
主谓词逐渐增加允许的数量
缺点和应用调用：
quine(Q,M,N) :-
expr(Q),between(0,N),eval(Q,[],P,[N],_),unify_with_occurs_check(Q,P).
此查询显示 5 个 cons 和应用调用足以生成一个 Quine。在 SICStus Prolog 和 Jekejeke Prolog 中工作。例如，对于 SWI-Prolog 需要使用此 unify/2 解决方法：
?- dif(Q,[]),quine(Q,6,N).
Q = [[lambda,symbol(_Q),[cons,quote],[]]]],[]]]]],[lambda,[]]]]]]],N = 5
我们可以手动验证它确实是一个非平凡的 Quine：
?- Q = [[lambda,[5],_).
Q = [[lambda,P = [[lambda,[]]]]]]]
有人可能会问一个发生的检查标志是否优于 一个显式的 unify_with_occurs_check/2。在 solution 与 明确的 unify_with_occurs_check/2 我们已经在 lookup2/3 和 quine/3 中放置了一个这样的调用。如果我们使用发生 检查标志，我们不需要手动拨打这样的电话和 可以依赖 Prolog 解释器的动态。
我们在 lookup2/3 中删除了显式的 unify_with_occurs_check/2：
lookup2(S,T).
lookup2(S,R).
还有在 quine/3 中，减少生成和测试，以及 更多约束逻辑之类的。两次使用相同的变量 Q 就像一个被推入执行的约束：
quine(Q,Q,_).
以下是新的 SWI-Prolog 8.3.17 的一些结果，其中 将其 unify_with_occurs_check/2 固定为与 zhe发生检查标志固定：
/* explicit unify_with_occurs_check/2 */
?- time((dif(Q,N))).
% 208,612,270 inferences,11.344 CPU in 11.332 seconds (100% CPU,18390062 Lips)
/* occurs_check=true */
?- time((dif(Q,N))).
% 48,502,916 inferences,2.859 CPU in 2.859 seconds (100% CPU,16962768 Lips)
还有即将发布的 Jekejeke Prolog 1.4.7 的预览版， 它还具有发生检查标志：
/* explicit unify_with_occurs_check/2 */
?- time((dif(Q,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,N))).
% Up 13,367 ms,GC 99 ms,Threads 13,235 ms (Current 01/10/21 01:35:24)
令人惊讶的是，发生检查标志可以导致两个 Prolog 系统中的 3 倍加速！结果可能表明我们明确放置 unify_with_occurs_check/2 的方式有问题？
顺便说一句：开源：
通过关系解释器生成Quine
显式 unify_with_occurs_check/2
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine-pl
通过关系解释器生成Quine
发生_检查=真
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine2-pl