#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