Combinatory Logic in Prolog

General
1

Now I was reading a paper where somebody used
modus ponens and these two axioms:

image

He then claimed that this here is derivable, whereby
later in the paper he presented a derivation:

image

He also said its not easy to find such a proof
and that he was helped! Can Prolog help?

Maybe using something from here can help:

Meta-interpreter collection for Prolog
https://github.com/Joelbyte/verdi-neruda

6

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

image

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)

1 Like