Substructural Logics in Prolog

General
1

Weekend 1:

  • Draw a Colored ASCII Christmas tree with Prolog.

Weekend 2:

  • Create a proof search in Combinatory Logic,
    that finds a Combinator Expression as proof
    for a given formula in propositional logic.

    The propositional logic can do with
    implication only, and it should be Linear Logic.
    French logician Jean-Yves Girard is credited

    with Linear Logic, and since we have implication
    logic only, the Logic will be also affine, i.e.
    it will have no contraction, which makes

    it special towards certain paradoxes.

Weekend 2:

  • Create a proof search in Simple Types,
    that finds Lambda Expressions as proof,
    for a given formula in propositional logic.

    The logic is the same as in Weekend 2.

Have Fun!

2

Now that Christmas is over, are you excited for the new year?

Here is the task for Weekend 4:

  • Do the same as for Weekend 2 and Weekend 3
    for a relevant logic.

This would complete the picture, since we would have:

Logic Weakening Contraction
Minimal Yes Yes
Relevant No Yes
Affine Yes No
Linear No No

Edit 17.01.2025:
Programming languages such as Vault, Rust, etc… have recently
popularized substructural logics. Their type systems share various
forms of resource awareness.

Part of the problem was already answered in this post:

Combinatory Logic in Prolog
https://swi-prolog.discourse.group/t/combinatory-logic-in-prolog/7536

Lets use these combinators:

   I:A->A                           /* (I x)     = x */
   K:A->(B->A)                      /* ((K x) y) = x */
   W:(A->(A->B))->(A->B)            /* ((W x) y) = ((x y) y) */
   S:(A->(B->C))->((A->B)->(A->C))  /* (((S x) y) z) = ((x z) (y z)) */
   B:(B->C)->((A->B)->(A->C))       /* (((B x) y) z) = ( x    (y z)) */
   C:(A->(B->C))->(B->(A->C))       /* (((C x) y) z) = ((x z)  y   ) */

In above we have put in comments the original definitions
found in Moses Schönfinkels paper from 1918. What has
changed since then are the mnemonics of the combinators,
whereas the paper used I, C, T, Z, S we nowadays use I, K, C, B, S.

We can determine type equalities:

   I ~ ((S K) K) ~ ((C K) K)
   B ~ (S (K S) K)
   C ~ ((S (S (K (S (K S) K)) S) (K K))
   W ~ ((S S) (S K)) ~ ((C S) I)

And this gives already Affine ⊂ Minimal, Relevant ⊂ Minimal,
Linear ⊂ Affine and Linear ⊂ Relevant. Plus half of the answer:

Logic Weakening K Contraction W
Minimal SK Yes Yes
Relevant SBCI Yes
Affine BCK Yes
Linear BCI
3

What is missing is a proper separation of the logics. Instead
of solving algebra problems we can use McCunes counter
model finder to solve logic problems. The approach is to see
logical connectives through the lense of algebra,

considering (->)/2 a binary operation on truth values:

    |- A -> B     |- A
   -------------------- (Modus Ponens)
          |- B

   -------- (Axiom Schema i)
    |- A_i

We erase the combinatory expression s from the judgment
|- s : A and consider judgment |- A. We do not ask for a congruence
relation, only a consequence relation. We can now show that
Affine Logic (BCK) does not generally admit contraction:

problem(2, (
   (![X]:![Y]:t((X -> (Y -> X))) &
    ![X]:![Y]:(t((X -> Y)) & t(X) => t(Y)) &
    ![X]:![Y]:![Z]:t(((Y -> Z) -> ((X -> Y) -> (X -> Z)))) &
    ![X]:![Y]:![Z]:t(((X -> (Y -> Z)) -> (Y -> (X -> Z)))))
    => t(((a->(a->b))->(a->b))))).

The first found counter model is a three-valued logic,
not from some text book:

?- between(1,3,N), problem(2, F), solve(F, N, R), !,
   show(R), fail.
a = 1 b = 2 
t(0) = 1 t(1) = 0 t(2) = 0 
(0 -> 0) = 0 (0 -> 1) = 1 (0 -> 2) = 2 
(1 -> 0) = 0 (1 -> 1) = 0 (1 -> 2) = 1 
(2 -> 0) = 0 (2 -> 1) = 0 (2 -> 2) = 0 
fail.

In summary it turns out that an according t/1 predicate for singled
out truth values leads to relative short counter models that separate
the investigated logics. We didn’t need to go beyond three valued logics:

Logic Weakening K Contraction W
Minimal SK
Relevant SBCI No
Affine BCK No
Linear BCI No No

Source code:

quine.p.log (5,8 KB)
mccune.p.log (5,8 KB)
truthy.p.log (3,4 KB)

Disclaimer: The file mccune.p contains a very simple Prolog mace4
implementation, it can be speed up by various methods.