Абстракция скобок в Prolog

#lambda #prolog

#лямбда #пролог

Вопрос:

Алгоритм «A», согласно Антони Диллеру, выглядит довольно просто:

введите описание изображения здесь

http://www.cantab.net/users/antoni.diller/brackets/intro.html

Можем ли мы сделать это в Prolog?

Комментарии:

1. Спасибо. Теперь мне есть что почитать.

2. В моем ответе также есть ссылка на прекрасную статью.

Ответ №1:

 % associate formulas to left
associate_left(F, A, B) :-
    append(A, [B], F).

% apply algorithm
reduce(b(_, []), []).
reduce(b(A, B), 'K'(B)) :- atom(B), dif(A, B).
reduce(b(A, A), 'I').
reduce(b(A, [F]), R) :- reduce(b(A, F), R). % uncessary paranthesis case
reduce(b(A, F), 'S'(Pr, Qr)) :-
    associate_left(F, P, Q),
    reduce(b(A, P), Pr),
    reduce(b(A, Q), Qr).
 

Я предполагаю, что связанные формулы b(x, F) — это то, где x связано в F.

 ?- reduce(b(x, [x]), A).
A = 'I' 

?- reduce(b(x, [y]), A).
A = 'K'(y) 

?- reduce(b(x, [u, v]), A).
A = 'S'('K'(u), 'K'(v)) 
 

Пример из вашей ссылки

 ?- reduce(b(x, [u, v, [w, z, x], [x, z, y], [z, x, [y, x]]]), A).
A = 'S'('S'('S'('S'('K'(u), 'K'(v)), 'S'('S'('K'(w), 'K'(z)), 'I')), 'S'('S'('I', 'K'(z)), 'K'(y))), 'S'('S'('K'(z), 'I'), 'S'('K'(y), 'I'))) 
 

Я тоже пробовал алгоритм B. Это немного сложно, но это так.

Комментарии:

1. Круто! Ваша система Prolog также может иметь last/3 . Но с вашим кодированием приложения я ожидал результатов [‘K’, y] и [‘S’, [‘K’, u], [‘K’, v]], это позволило бы полностью разархивировать, т. Е., Например, преобразовать b(y, b(x, [y])).

2. Сначала я закодировал его как [const, y], [genapp, [const, u], [const, v]] . Позже я изменил его на текущую составную форму для более традиционной читаемости.

Ответ №2:

Используется немного другое кодирование для приложения
с оператором Prolog, который уже остается ассоциативным:

 ?- X = ((a*b)*c).
X = a*b*c
 

И добавлен предикат unlambda/2:

 unlambda(b(X,Y), Z) :- !,
   unlambda(Y, H),
   reduce(H, X, Z).
unlambda(P*Q, W) :- !,
   unlambda(P, R),
   unlambda(Q, S),
   W = R*S.
unlambda(X, X).

reduce(X, X, W) :- !,
   W = 'I'.
reduce(P*Q, Z, W) :- !,
   reduce(P, Z, R),
   reduce(Q, Z, S),
   W = 'S'*R*S.
reduce(X, _, 'K'*X).
 

Но мы видим, что есть проблема,
результаты могут быть довольно длинными:

 ?- unlambda(b(x,b(y,x)), X).
X = 'S'*('K'*'K')*'I'
?- unlambda(b(x,b(y,b(z,(x*z)*(y*z)))), X).
X = 'S'*('S'*('K'*'S')*('S'*('S'*('K'*'S')*('S'*('K'*'K')*('K'*'S')))*
('S'*('S'*('K'*'S')*('S'*('S'*('K'*'S')*('S'*('K'*'K')*('K'*'S')))*
('S'*('S'*('K'*'S')*('S'*('K'*'K')*('K'*'K')))*('S'*('K'*'K')*'I'))))*
('S'*('K'*'K')*('K'*'I')))))*('S'*('S'*('K'*'S')*('S'*('S'*('K'*'S')*
('S'*('K'*'K')*('K'*'S')))*('S'*('S'*('K'*'S')*('S'*('K'*'K')*
('K'*'K')))*('K'*'I'))))*('S'*('K'*'K')*('K'*'I')))
 

Мы можем использовать два идентификатора, уже задокументированные Curien(*),
которые имеют эффект [x]E = 'K'E и [x]Ex = E :

 reduce(P*Q, Z, W) :- !,
   reduce(P, Z, R),
   reduce(Q, Z, S),
   (S = 'I', R = 'K'*L ->
       W = L;
    S = 'K'*M, R = 'K'*L ->
       W = 'K'*(L*M);
       W = 'S'*R*S).
 

Результат теперь намного лучше:

 ?- unlambda(b(x,b(y,x)), X).
X = 'K'
?- unlambda(b(x,b(y,b(z,(x*z)*(y*z)))), X).
X = 'S'
 

(*) См. стр. 215 правило (abs) и правило (eta):
Категориальные комбинаторы
П.-Л. Кюриен — 1986
https://core.ac.uk/download/pdf/82017242.pdf