Prolog中的括号抽象答案

【问题标题】：Bracket Abstraction in PrologProlog中的括号抽象
【发布时间】：2020-11-30 21:20:17
【问题描述】：

根据 Antoni Diller 的算法“A”看起来相当简单：

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

我们可以在 Prolog 中做到这一点吗？

【问题讨论】：

谢谢。现在我要阅读更多内容。
我的答案还有一篇精美论文的链接。

【解决方案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。有点毛茸茸，但here 确实如此。

【讨论】：

酷！你的 Prolog 系统也可能有 last/3。但是通过您对应用程序的编码，我期望结果 ['K', y] 和 ['S',['K',u],['K',v]]，这将允许一个完整的 unlambda，例如转换 b(y, b(x, [y]))。
一开始我将它编码为 [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)：
分类组合器
P.-L.居里安 - 1986
https://core.ac.uk/download/pdf/82017242.pdf

【讨论】：