【问题标题】:Pure Prolog Scheme Quine纯 Prolog 方案 Quine
【发布时间】:2020-12-25 08:48:41
【问题描述】:

有这篇论文:

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

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

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

所以除了 lembda for 之外,唯一的符号是引号、[] 和 cons lambda 抽象和绑定变量。我们会使用 Prolog 方案列表的列表。目标是找到一个方案 通过 Prolog 对 Q 进行编程,因此我们得到 Q ~~> Q,即对自身求值。

有一个复杂因素,使努力变得不平凡, [lembda,X,Y] 不会对自身进行语法评估,而是 应该返回一个环境闭包。所以评估者将是 不像 Plotkin 评估器here

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

【问题讨论】:

  • > 有任何 Prolog 解决方案吗?是的,在comp.lang.prolog mailing list 上有一些关于这个问题和解决方案的讨论。
  • 这里的两个解决方案不使用 sto/1 约束。而是在一个变体中 unify_with_occurs_check/2 和在另一个变体中发生_check = true。后一种变体在速度上优于前一种变体。

标签: prolog logical-purity lambda-prolog occurs-check


【解决方案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 为 (i love you) 的 Scheme 表达式——这个例子在 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 的递归。

【讨论】:

  • 如果你在某个节点有无限分支,bfs 理论上也应该有问题。相反,需要采用某种对角化。
  • @MostowskiCollapse 我不这么认为。我在.swiplrc 中将OC 设置为true。 BFS Prolog 引擎就是这里所需要的。 evil(X,Y)“创建所有可能的输入/输出对”——这在非常短的程序之外是不可行的。
  • @MaxB 这个方案没有cons。是否有不需要cons 的(小型)Scheme quines?如果没有,那么再多的调整搜索也不会让您有任何收获。
  • @IsabelleNewbie 谢谢!添加了cons。如果call_with_depth_limit(evil(X, X), 6, R). 找到任何东西,我会进行编辑——它仍在运行。
  • 我的版本不能处理(lambda x,只能处理(lambda (x)。我不知道这是允许的。但((lambda x (cons x (cons (cons (quote quote) (cons x (quote ()))) (quote ())))) (quote (lambda x (cons x (cons (cons (quote quote) (cons x (quote ()))) (quote ())))))) 实际上也不是 quine。它评估为(((lambda ... -- 三个括号。
【解决方案2】:

这是一个使用一点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, 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 编码的评估器,
限制缺点的总数并应用调用:

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

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

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, []]]]]]] 

【讨论】:

  • 这个 quine 看起来并不真实:((lambda x (cons x (cons (cons (quote quote) (cons x (quote ()))) (quote ())))) (quote (lambda x (cons x (cons (cons (quote quote) (cons x (quote ()))) (quote ())))))) -- 它相当于 ((( -- 注意括号的数量。
  • (lambda (x) ...(lambda x 不同,事实证明,两者在 Scheme 中都是允许的。
【解决方案3】:

有人可能会问,发生检查标志是否优于 一个明确的 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, [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 固定在一起 哲发生检查标志固定:

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

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

【讨论】:

  • 这些要点现在不再可用。你能更新他们的新位置吗?
猜你喜欢
  • 2021-05-16
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 2021-04-02
  • 1970-01-01
  • 2014-07-28
相关资源
最近更新 更多