How to implement SKI combinators in Prolog?

Question

I want to implement SKI combinators in Prolog.

There are just 3 simple rules:

1. (I x) = x
2. ((K x) y) = x
3. (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:

1. It takes too much time to execute simple queries:
   

   term(X) & proc(app(app(k, X), s), app(s,k)) 
   

   100004 unification(s)

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

Answer 1

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

Answer 2

Based on Will Ness answer here is my solution:

term(s).
term(k).
term(i).
term(app(X,Y)) :- term(X), term(Y).

eq(s,s).
eq(k,k).
eq(i,i).
eq(app(X,Y),app(X,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), Z) :- proc(X, X1), proc(Y, Y1), eq(X, X1), eq(X, X1), eq(app(X, Y), Z).
proc(app(X, Y), Z) :- proc(X, X1), proc(Y, Y1), not(eq(X, X1)), proc(app(X1, Y1), Z).
proc(app(X, Y), Z) :- proc(X, X1), proc(Y, Y1), not(eq(Y, Y1)), proc(app(X1, Y1), Z).

1. Move code to swish prolog. It works much faster

time((term(X), proc(app(app(k, X), s), app(s,k)))). 
% 356 inferences, 0.000 CPU in 0.000 seconds (94% CPU, 3768472 Lips)
X = app(s,k)

2. Implemented complete reduction procedure:

proc(app(app(app(app(s,app(k,app(s,i))),k),s),k), X) 
answer contains: X = app(k,s)

There are still issues that I can not resolve

1. time((term(X), proc(app(app(X, k), s), app(s,k)))). runs forever
2. Answers are not ordered by reductions.

Answer 3

Translating your code trivially to Prolog, using the built-in left-associating infix operator - for app, to improve readability,

term(s).
term(k).
term(i).
term( X-Y ) :- term(X) , term(Y).

/* proc(s, s).      %%% not really needed.
proc(k, k).
proc(i, i). */

proc( i-Y, Y1) :- proc( Y,Y1).
proc( k-Y-Z, Y1) :- proc( Y,Y1).
proc( s-X-Y-Z, Y1) :- proc( X-Z-(Y-Z), Y1).

proc( X-Y, X1-Y1 ) :- proc( X, X1) , proc( Y, Y1).
proc( X, X).

executing in SWI Prolog,

26 ?- time( (term(X), proc( k-X-s, s-k)) ).
% 20 inferences, 0.000 CPU in 0.001 seconds (0% CPU, Infinite Lips)
X = s-k ;
% 1 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = s-k ;
Action (h for help) ? abort
% 952,783 inferences, 88.359 CPU in 90.112 seconds (98% CPU, 10783 Lips)
% Execution Aborted
27 ?- 

the first result is produced in 20 inferences.

---

Furthermore, indeed

32 ?- time( proc( s-(k-(s-i))-k-s-k, X) ).
% 10 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = s-i- (k-s)-k ;
% 2 inferences, 0.000 CPU in 0.001 seconds (0% CPU, Infinite Lips)
X = s-i- (k-s)-k ;
% 5 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = s-i- (k-s)-k ;
% 2 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = s-i- (k-s)-k ;
% 11 inferences, 0.000 CPU in 0.001 seconds (0% CPU, Infinite Lips)
X = k- (s-i)-s- (k-s)-k ;
% 2 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = k- (s-i)-s- (k-s)-k . % stopped manually

and then

33 ?- time( proc( s-i- (k-s)-k, X) ).
% 5 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = k-s ;
% 5 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = k- (k-s-k) ;
% 2 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = k- (k-s-k) ;
% 1 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = k- (k-s-k) ;
% 5 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = i-k-s ;
% 5 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = i-k- (k-s-k) ;
% 2 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = i-k- (k-s-k) ;
% 1 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = i-k- (k-s-k) ;
% 3 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = i-k-s ;
% 5 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
X = i-k- (k-s-k) . % stopped manually

but probably the result you wanted will still get generated directly, just after some more time.