纯序言方案奎因 [英] Pure Prolog Scheme Quine

问题描述

有这篇论文:

威廉 E.伯德、埃里克霍尔克、丹尼尔 P.弗里德曼，2012
迷你看人，直播和无标签
通过关系解释器生成奎因
http://webyrd.net/quines/quines.pdf

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

它使用逻辑编程来查找 Scheme Quine.这此处考虑的方案子集不仅包含 lambda抽象和应用，还有一点列表处理通过以下缩减，已转换为 Prolog:

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

所以唯一的符号是引用、[] 和 cons，除了 lembda forlambda 抽象和绑定变量.我们将使用 PrologScheme 列表的列表.目标是找到一个Scheme通过 Prolog 对 Q 进行编程，从而得到 Q ~~>Q，即对自身求值.

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.

有一个复杂的问题，这使得努力变得不平凡，[lembda,X,Y] 不对其自身进行语法评估，而是应该返回一个环境关闭.所以评估者将是与 Plotkin 评估器此处不同.

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.

周围有任何 Prolog 解决方案吗?圣诞快乐

Any Prolog solutions around? Merry X-Mas

推荐答案

我正在使用 SWI Prolog，并在此处打开了发生检查(但 dif/2 无论如何都会跳过发生检查):

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

测试:

查找 eval 为 (i love you) 的 Scheme 表达式——这个例子在 miniKanren 中有一段历史:

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

换句话说，它找到的前 4 件事是:

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

看起来 Scheme 语义是正确的.它放置的语言律师类型的限制非常整洁.确实，真正的Scheme会拒绝

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.

但会接受

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

那么奎因怎么样?

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

miniKanren 使用 BFS，所以也许这就是它在这里产生结果的原因.使用 DFS，这可以工作(假设没有错误):

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

或

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

但 SWI 不一定用 call_with_depth_limit 限制递归.

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

这篇关于纯序言方案奎因的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！