I want to implement SKI combinators in Prolog.
There are just 3 simple rules:
I came up with the following code by using epilog:
term(s)
term(k)
term(i)
term(app(X,Y)) :- term(X) & term(Y)
proc(s, s)
proc(k, k)
proc(i, i)
proc(app(i,Y), Y1) :- proc(Y,Y1)
proc(app(app(k,Y),Z), Y1) :- proc(Y,Y1)
proc(app(app(app(s,P1),P2),P3), Y1) :- proc(app( app(P1,P3), app(P2, P3) ), Y1)
proc(app(X, Y), app(X1, Y1)) :- proc(X, X1) & proc(Y, Y1)
proc(X,X)
It works for some cases but has 2 issues:
It takes too much time to execute simple queries:
term(X) & proc(app(app(k, X), s), app(s,k))
100004 unification(s)
It requires multiple queries to process some terms. For example:
((((S(K(SI)))K)S)K) -> (KS)
requires 2 runs:
proc(app(app(app(app(s,app(k,app(s,i))),k),s),k), X) ==>
proc(app(app(app(app(s,app(k,app(s,i))),k),s),k), app(app(app(s,i),app(k,s)),k))
proc(app(app(app(s,i),app(k,s)),k), X) ==>
proc(app(app(app(s,i),app(k,s)),k), app(k,s))
Can you please suggest how to optimize my implementation and make it work on complex combinators?
edit: The goal is to reduce combinators. I want to enumerate them (without duplicates) where the last one is in normal form (if it exists of course).
It can be implemented with iterative deepening like this:
term(s) --> "S".
term(k) --> "K".
term(i) --> "I".
term(a(E0,E)) --> "(", term(E0), term(E), ")".
reduce_(s, s).
reduce_(k, k).
reduce_(i, i).
% Level 1.
reduce_(a(s,A0), a(s,A)) :-
reduce_(A0, A).
reduce_(a(k,A0), a(k,A)) :-
reduce_(A0, A).
reduce_(a(i,A), A).
% level 2.
reduce_(a(a(s,E0),A0), a(a(s,E),A)) :-
reduce_(E0, E),
if_(E0 = E, reduce_(A0, A), A0 = A).
% reduce_(A0, A). % Without `reif`.
reduce_(a(a(k,E),_), E).
reduce_(a(a(i,E),A), a(E,A)).
% level 3.
reduce_(a(a(a(s,E),F),A), a(a(E,A),a(F,A))).
reduce_(a(a(a(k,E),_),A), a(E,A)).
reduce_(a(a(a(i,E),F),A), a(a(E,F),A)).
% Recursion.
reduce_(a(a(a(a(E0,E1),E2),E3),A0), a(E,A)) :-
reduce_(a(a(a(E0,E1),E2),E3), E),
if_(a(a(a(E0,E1),E2),E3) = E, reduce_(A0, A), A0 = A).
% reduce_(A0, A). % Without `reif`.
step(E, E0, E) :-
reduce_(E0, E).
reduce_(N, E0, E, [E0|Es]) :-
length(Es, N),
foldl(step, Es, E0, E).
reduce(N, E0, E) :-
reduce_(N, E0, E, _),
reduce_(E, E), % Fix point.
!. % Commit.
The term can be inputted and outputted as a list of characters with term//1
. The grammar rule term//1
can also generate unique terms.
?- length(Cs, M), M mod 3 =:= 1, phrase(term(E0), Cs).
The goal is to be as lazy as possible when reducing a term thus dif/2
and the library reif is used in reduce_/2
. The predicate reduce_/2
does a single reduction. If any of the argument of reduce_/2
is ground then termination is guarantee (checked with cTI).
To reduce a term, reduce_/4
can be used. The first argument specifies the depth, the last argument holds the list of terms. The predicate reduce_/4
is pure and does not terminate.
?- Cs = "(((SK)K)S)", phrase(term(E0), Cs), reduce_(N, E0, E, Es).
The predicate reduce/3
succeeds if there is a normal form. It is recommended to provide a maximum depth (e.g. Cs = "(((SI)I)((SI)(SI)))"
):
?- length(Cs, M), M mod 3 =:= 1, phrase(term(E0), Cs), \+ reduce(16, E0, _).
Test with ((((S(K(SI)))K)S)K)
:
?- Cs0 = "((((S(K(SI)))K)S)K)", phrase(term(E0), Cs0),
reduce(N, E0, E), phrase(term(E), Cs).
Cs0="((((S(K(SI)))K)S)K)", E0=a(a(a(a(s,a(k,a(s,i))),k),s),k), N=5, E=a(k,s), Cs="(KS)"