How to implement SKI combinators in Prolog?

I want to implement SKI combinators in Prolog.

There are just 3 simple rules:

(I x) = x
((K x) y) = x
(S x y z) = (x z (y z))

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).

Solution

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)"