Advent of Logic 2024: Solution Weekend 2 (Was: Advent of Logic 2024: Specification and Deadline)

As a warmup I started with a subintuitionistic logic:
https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-minimal-p
With these test cases:
/* 4 positive test cases */
% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = s*k .
% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 13,
% X = s*(k*(s*(s*k*k)))*k .
% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .
% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = s*s*(s*k) .
And then I made the required substructural logic:
https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p
With these test cases:
/* 2 positive test cases */
% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 1,
% X = i .
% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 3,
% X = c*i .
/* 2 negative test cases */
% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% false.
% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.
Mild Shock schrieb:

Its quite intersting that Affine Logic can
be measured by the realization of this output:
  > - Output = Variable         % Repetition
 Its seems to me that in Affine Logic a variable
is only allowed to occur in a Repetition at most
once, it seems also to me that each variable
 must be also repeated at least once. So that
variables are repreated exactly once.
 Here is a counter example with too many repetitions,
this would not be a valid output for weekend 3,
since it cannot be converted into the output of weekend 2:
 λx:A->A.λy:A.(x (x y))   :  ((A -> A) -> (A -> A))
 And her is a counter example with too few repetitions,
equally well it cannot be converted to a BCI expression.
 λx:A.λy:B.x : (A -> (B -> A))
 I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.
 Mild Shock schrieb:

Specification:
>
>
Weekend 2:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication
>
- Output = B               % B Axiom Schema
          | C               % C Axiom Schema
          | I               % I Axiom Schema
          | (Output Output) % Modus Ponens
>
Weekend 3:
-----------
- Input = Atom            % Propositional variable
         | Input -> Input  % Implication
>
- Output = Variable         % Repetition
          | λVariable.Output % Assumption & Detachment
          | (Output Output)  % Modus Ponens
>
>
Deadline:
>
24. December 2024
>