Ok, a solution would be SKK = I where S = #7 and K = #8:

It does not take much CPU to find it. First the logic definition, we
need to linearize the axiom schemas with unify_with_occurs_check/2:
:- dynamic typeof/2.
/* modus ponens */
typeof((S*T), B) :-
typeof(S, (A -> B)),
typeof(T, A).
/* K axiom */
typeof(k, (A -> _ -> C)) :-
unify_with_occurs_check(A,C).
/* S axiom */
typeof(s, ((A -> B -> C) -> (D -> F) -> (E -> G))) :-
unify_with_occurs_check(A,D),
unify_with_occurs_check(A,E),
unify_with_occurs_check(B,F),
unify_with_occurs_check(C,G).
Now from THE BOOK, the Craft of Prolog piece here, something
similar like iterative depening, iterative counting:
/* vanilla interpreter with typeof/2 counting */
search(true, N, N).
search((A,B), N, M) :-
search(A, N, H),
search(B, H, M).
search(typeof(P, T), N, M) :- N>0, H is N-1,
clause(typeof(P, T), B),
search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :-
unify_with_occurs_check(A,B).
Eh voila the helping hand is finished. And we can use
it as a brain extension, looking for proofs on our behalf:
?- between(1,6,N), search(typeof(X, a->a), N, 0).
N = 5,
X = s*k*k ;
false.
Source code:
craft.p.log (2,1 KB)