Схема чистого пролога Quine

Вот эта бумага:

Уильям Э. Берд, Эрик Холк, Дэниел П. Фридман, 2012
miniKanren, Прямая трансляция и без тегов
Генерация Куайна с помощью реляционных интерпретаторов
http://webyrd.net/quines/quines.pdf

Которая использует логическое программирование, чтобы найти схему Quine. Рассматриваемое здесь подмножество Scheme не только содержит лямбда-абстракцию и приложение, но и небольшую обработку списка с помощью следующего сокращения, уже переведенного на Prolog:

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

Таким образом, единственными символами являются кавычки, [] и cons, помимо lembda для лямбда-абстракции и связанных переменных. И мы будем использовать списки Пролога для списков схем. Цель состоит в том, чтобы найти программу Q на схеме Q через Prolog, чтобы мы получили Q ~~ ›Q, т.е. вычислили для себя.

Есть одна сложность, которая делает попытку нетривиальной, [lembda, X, Y] не оценивает синтаксически для себя, а скорее должен возвращать закрытие среды. Таким образом, оценщик будет отличаться от оценщика Plotkin, который здесь.

Какие-нибудь решения Prolog? С Рождеством


person Mostowski Collapse    schedule 25.12.2020    source источник
comment
›Есть какие-нибудь решения Prolog? Да, эта проблема и решения обсуждались на сайте comp Список рассылки .lang.prolog.   -  person Jason Hemann    schedule 20.06.2021
comment
Два решения здесь не используют ограничение sto / 1. Но точнее в одном варианте unify_with_occurs_check / 2, а в другом варианте встречается_check = true. Более поздний вариант превосходит предыдущий по скорости.   -  person Mostowski Collapse    schedule 20.06.2021


Ответы (3)


Я использую 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).

Тесты:

Найдите выражения схемы, которые оцениваются до (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

Похоже, семантика схемы верна. Ограничения типа «язык-юрист» довольно изящны. Действительно, настоящая Схема откажется

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

or

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

но SWI не обязательно ограничивает рекурсию с помощью call_with_depth_limit.

person bobcat    schedule 27.12.2020
comment
Теоретически у bfs также должны быть проблемы, если у вас есть бесконечное ветвление на каком-то узле. вместо этого нужно использовать какую-то диагонализацию. - person Will Ness; 27.12.2020
comment
@MostowskiCollapse Я так не думаю. У меня OC установлено на true в .swiplrc. Здесь нужен движок BFS Prolog. evil(X,Y) говорит: создавать ВСЕ возможные пары ввода / вывода - это невозможно, кроме очень коротких программ. - person bobcat; 30.12.2020
comment
@MaxB в этой схеме нет cons. Существуют ли (мелкие) лохмотья схемы, которым не нужны cons? Если их нет, то никакие настройки поиска ни к чему не приведут. - person Isabelle Newbie; 31.12.2020
comment
@IsabelleNewbie Спасибо! Добавлен cons. Я отредактирую, если call_with_depth_limit(evil(X, X), 6, R). что-нибудь найдет - все еще работает. - person bobcat; 31.12.2020
comment
Я попытался перевести квайн, найденный другим ответом, в представление зла и оценить его, но, похоже, он не оценивает это выражение самому себе. - person Isabelle Newbie; 01.01.2021
comment
Моя версия не обрабатывает (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 ())))))) на самом деле не квин. Это равняется (((lambda ... - трем скобкам. - person bobcat; 02.01.2021
comment
Вы также можете найти quine для другого языка. Это может быть другая лоза. - person Mostowski Collapse; 02.01.2021

Вот решение, в котором используется небольшой стиль программирования с блокировкой. Он не использует when / 2, а только замораживает / 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 минусов и вызовов применения достаточно для создания 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 

Мы можем вручную убедиться, что это действительно нетривиальный Куайн:

?- 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, []]]]]]] 
person Mostowski Collapse    schedule 30.12.2020
comment
Этот 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 ())))))) - он равен ((( - обратите внимание на количество скобок. - person bobcat; 02.01.2021
comment
(lambda (x) ... отличается от (lambda x Оказывается, в схеме разрешены оба варианта. - person bobcat; 02.01.2021

Можно спросить, превосходит ли флаг проверки «происходит» над явным unify_with_occurs_check / 2. В решении с явным unify_with_occurs_check / 2 мы разместили один такой вызов в lookup2 / 3 и quine / 3. Если мы используем флаг проверки «происходит», нам не нужно вручную размещать такие вызовы и мы можем полагаться на динамику интерпретатора Пролога.

Мы удалили явный unify_with_occurs_check / 2 в lookup2 / 3:

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! Результат, возможно, указывает на то, что способ, которым мы явно поместили unify_with_occurs_check / 2, был ошибочным?

Кстати: с открытым исходным кодом:

Создание Quine с помощью реляционных интерпретаторов
явное unify_with_occurs_check / 2
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine-pl

Создание Quine с помощью реляционных интерпретаторов
plays_check = true
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine2-pl

person Mostowski Collapse    schedule 10.01.2021