# Advent of Code: Combinatorial Logic

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

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

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:

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:

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)