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

Question

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

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

Уильям Э. Берд, Эрик Холк, Дэниел П. Фридман, 2012
miniKanren,
Генерация Quine в реальном времени и без тегов с помощью реляционных интерпретаторов
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] не оценивает синтаксически для себя, а скорее должен возвращать закрытие среды. Таким образом, оценщик будет в отличии от Плоткина оценщика здесь .

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

4

prolog logical-purity occurs-check lambda-prolog

Источник

user502187 25 дек '20 в 11:48

3 ответа

Другие вопросы по тегам prolog logical-purity occurs-check lambda-prolog

user1937197 27 дек '20 в 18:51 2020-12-27 18:51 · Answer 1 · 2020-12-27 18:51

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

или же

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

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

user502187 30 дек '20 в 21:40 2020-12-30 21:40 · Answer 2 · 2020-12-30 21:40

Вот решение, в котором используется небольшой стиль программирования с блокировкой . Он не использует 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, []]]]]]]

user502187 10 янв '21 в 03:47 2021-01-10 03:47 · Answer 3 · 2021-01-10 03:47

Можно спросить, превосходит ли флаг проверки «происходит» над явным 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 с помощью реляционных интерпретаторов
происходит_check = true
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine2-pl