Substructural Logics in Prolog

General
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