3

有这篇论文:

William E. Byrd、Eric Holk、Daniel P. Friedman,2012
miniKanren,
通过关系解释器实时和未标记的 Quines 生成
http://webyrd.net/quines/quines.pdf

它使用逻辑编程来查找 Scheme Quine。这里考虑的 Scheme 子集不仅包含 lambda 抽象和应用程序,还包含通过以下归约处理的小列表处理,已翻译为 Prolog:

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

因此,除了用于 lambda 抽象和绑定变量的 lembda 之外,唯一的符号是引号、[] 和 cons。我们将使用 Prolog 列表作为 Scheme 列表。目标是通过 Prolog 找到一个 Scheme 程序 Q,这样我们得到 Q ~~> Q,即对自身求值。

有一个复杂性,这使得努力变得不平凡,[lembda,X,Y] 不会在语法上对其自身进行评估,而是应该返回一个环境闭包。因此,评估器与此处的 Plotkin 评估器不同。

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

4

3 回答 3

1

我正在使用 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, 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 到的 Scheme 表达式(i love you)——这个例子在 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 件事是:

(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, X), m, R).

但 SWI 并不一定限制使用call_with_depth_limit.

于 2020-12-27T15:51:31.730 回答
0

这是一个使用一点阻塞编程风格的解决方案。它不使用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, 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).

最后是使用 DCG 编码的评估器,
用于限制 cons 的总数并应用调用:

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

主谓词逐渐增加允许的
cons 和应用调用的数量:

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

此查询显示 5 个 cons 和 apply 调用足以生成 Quine。在 SICStus Prolog 和 Jekejeke Prolog 中工作。对于 SWI-Prolog 需要使用例如这个unify/2解决方法:

?- 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 

我们可以手动验证它确实是一个非平凡的 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, []]]]]]] 
于 2020-12-30T18:40:47.230 回答
-1

有人可能会问,发生检查标志是否优于显式 unify_with_occurs_check/2。在具有显式 unify_with_occurs_check/2 的解决方案中,我们在 lookup2/3 和 quine/3 中放置了一个这样的调用。如果我们使用发生检查标志,我们不需要手动进行此类调用,并且可以依赖 Prolog 解释器的动态。

我们在 lookup2/3 中删除了显式的 unify_with_occurs_check/2:

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

并且在 quine/3 中,减少了生成和测试,以及更多的约束逻辑。使用相同的变量 Q 两次就像一个被推入执行的约束:

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

以下是新 SWI-Prolog 8.3.17 的一些结果,它修复了 unify_with_occurs_check/2 并修复了 zhe 发生检查标志:

/* 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)

还有即将推出的 Jekejeke Prolog 1.4.7 的预览版,其中还将包含一个发生检查标志:

/* 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)

令人惊讶的是,发生检查标志可以导致两个 Prolog 系统中的 3 倍加速!结果可能表明我们明确放置 unify_with_occurs_check/2 的方式有问题?

顺便说一句:开源:

通过关系解释器
显式生成 unify_with_occurs_check/2
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine-pl

通过关系解释器生成
Quine_check=true
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine2-pl

于 2021-01-10T00:47:42.890 回答