Advent of Code: Combinatorial Logic

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

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

Here a little foto album of BOOKS for the next beach holiday:

https://esb-dev.github.io/mat/cl-b.pdf

1 Like

Its quite interesting how some combinators might fit a notion
of “computation”, while they might not fit a notion of “derivation”,
as we did for A → A here, this is what is understood by “derivation”:

For example Christopher Strachey and Dana Scott were
quite excited when they discovered function space constructions
that could solve D = [D → D], and thus allowing certain denotational

semantics. You can see their enthusiasm for example here:

image

Toward a Mathematical Semantics for Computer Languages
https://www.cs.ox.ac.uk/files/3228/PRG06.pdf

What they judge as remarkable and particularly useful for “computation”, turns
out a real nightmare for “derivation”. You can try yourself, I am adding the “I”
combinator which we have already shown to be derivable,

and then a new “Y” combinator:

/* I axiom */
typeof(i, (A -> B)) :-
   unify_with_occurs_check(A,B).
/* Y axiom */
typeof(y, ((A -> B) -> C)) :-
   unify_with_occurs_check(A,B),
   unify_with_occurs_check(A,C).

Lets see what happens, can we prove anything?

?- between(1,6,N), search(typeof(X, a), N, 0).
N = 3,
X = y*i .

Yes it collapses trivally, even doesn’t need a complicated Curry Paradox.
So what would be a signature of Y that is compatible with the Curry-Howard
isomorphism and does not make the formula-as-types notion collapse?

And last but not least, try answering this question which might have surprising
answers, why would we even need a Y combinator for derivations?

Source code:

craft2.p.log (2,3 KB)