Чистый метаинтерпретатор Prolog с одним правилом

#prolog #metaprogramming #logical-purity

#пролог #метапрограммирование #логическая чистота

Вопрос:

Интересно, существует ли чистый метаинтерпретатор Prolog только с одним правилом. Обычный метаинтерпретатор Prolog vanilla имеет два правила. Он выглядит следующим образом:

 solve(true).
solve((A, B)) :- solve(A), solve(B). /* rule 1 */
solve(H) :- program(H, B), solve(B). /* rule 2 */

Этот ванильный метаинтерпретатор Prolog использует два правила /* rule 1 */
и /* rule 2 */ . А остальное — факты. Выполняемая программа
представлена фактами программы. Вот пример программы:

 program(append([], X, X), true).
program(append([X|Y], Z, [X|T]), append(Y, Z, T)).
program(nrev([], []), true).
program(nrev([H|T], R), (nrev(T, S), append(S, [H], R))).

И пример запроса:

 ?- solve(nrev([1,2,3], X)).
X = [3, 2, 1] .

Есть ли способ представить программу по-другому как факты, а
затем закодировать другой метаинтерпретатор, который использовал бы только факты
, за исключением одного правила, вместо двух правил? Что-то, что будет
работать для всех программ pure Prolog, а не только для примера nrev?

1. Каково ваше определение понятия «чистый»? Это ;/2 приемлемо?

2. Мета-интерпретатору нужно только понимать true, (,)/2 и атомарные формулы. (;)/2 можно было бы определить как два факта program((A;_), A). program((_;B),B).

3. Я забыл сказать, что правило предложения Horn не имеет (;)/2 в теле. Таким образом, вы не можете использовать (;)/2 в определении вашего решения. В противном случае проблема слишком проста.

Ответ №1:

Вот одна идея, использование списка для хранения остальной части вычислений:

 solve([]).
solve([X|Xs]) :- program(X, Ys, Xs), solve(Ys).

program(true, Xs, Xs).
program(append([],X,X), Xs, Xs).
program(append([X|Y], Z, [X|T]), [append(Y,Z,T)|Xs], Xs).
program(nrev([],[]), Xs, Xs).
program(nrev([H|T],R), [nrev(T,S),append(S,[H],R)|Xs], Xs).

С тестовым вызовом (где нужно обернуть вызов в список).

 ?- solve([nrev([1,2,3],X)]).
X = [3,2,1] ? ;
no

Возможно, вместо этого можно было бы представить факты program / 3 как DCG для повышения удобства чтения (но тогда это больше не может считаться «фактом»).

1. Блестяще, я думаю, что есть даже статья какого-то J …, в которой обсуждалось это несколько десятилетий назад, и подход назван в его честь. Если у меня будет время, я возьму ссылку.

2. Этот метаинтерпретатор реализует конъюнкцию.

3. … и это суть бинаризации.

4. @false Можете ли вы объяснить, что вы подразумеваете под бинаризацией в этом контексте? Не уверен, что я понимаю этот термин… Спасибо!

5. Бинаризация — это преобразование из Prolog в подмножество, называемое двоичным прологом , которое несколько проще реализовать. Суть в том, что общее соединение конкретизируется (так же, как вы это сделали).

Ответ №2:

Вот еще один подход, известный как бинаризация с продолжением.
Это из статьи Пола Тарау «Логические трансформаторы» (2021).

 solve(true).
solve(X) :- program(X, Y), solve(Y).

program(append([],X,X,C), C).
program(append([X|Y],Z,[X|T],C), append(Y,Z,T,C)).
program(nrev([],[],C), C).
program(nrev([H|T],R,C), nrev(T,S,append(S,[H],R,C))).

Небольшая проверка работоспособности показывает, что это неправильно:

 ?- solve(nrev([1,2,3], X, true)).
X = [3, 2, 1] ;
No

Ответ №3:

Если ;/2 разрешено, то это, похоже, работает:

 solve(true).
solve(H) :- ((X, Y) = H, solve(X), solve(Y)); (program(H :- B), solve(B)).

program(append([], X, X) :- true).
program(append([X|Y], Z, [X|T]) :- append(Y, Z, T)).
program(nrev([], []) :- true).
program(nrev([H|T], R) :- (nrev(T, S), append(S, [H], R))).

Тест:

 ?- solve(nrev([1,2,3], X)).
X = [3, 2, 1] ;
false.