Re: Linear Logic as Natural Deduction (Was: Advent of Logic 2024: Friendly Reminder)

The source code is here:
https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-linear-p
And some testing is here:
/* 2 positive test cases */
% ?- between(1,13,N), search(typeof(X, [], [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .
% ?- between(1,13,N), search(typeof(X, [], [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .
/* 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:

I skipped doing an affine logic. But one can derive
it from the linear logic. So I made a linear logic.
It is derived from the minimal logic but typeof
 as a different signatur:
 /* Minimal Logic */
G |- M : t              /* typeof(M, G, t) */
 /* Linear Logic
G |- M : t | G'         /* typeof(M, G, G', t) */
 The updated context G' does a tracking and sees to it
that every assumption is only use once. An assumption
has initially the flag 0 and when it was used it has
 the flag 1. There are two places in the code where
this is used:
 /* Implication Intro */
typeof(lam(A, Y), L, R, (A -> B)) :-
    typeof(Y, [A-0|L], [A-1|R], B).
/* Axiom */
typeof(K, L, R, B) :-
    nth0(K, L, A-0, H),
    unify_with_occurs_check(A, B),
    nth0(K, R, A-1, H).
 Its not yet extremly tested. And its not widely known,
since most presentations are Sequent Calculus and not
Natural Deduction. I only found one paper:
 Introduction to linear logic - Emmanuel Beffara
Table 6: Intuitionistic linear logic as natural deduction
https://hal.science/cel-01144229
 Mild Shock schrieb:

Ok, I made a solution for Weekend 3,
first I made minimal logic. I opted for
Lambda Expressions with de Brujin indexes:
>
/* 4 positive test cases */
>
% ?- between(1,13,N), search(typeof(X, [], ((a->a)->(a->a))), N, 0).
% N = 2,
% X = lam((a->a), 0) .
>
% ?- between(1,13,N), search(typeof(X, [], (a->((a->b)->b))), N, 0).
% N = 5,
% X = lam(a, lam((a->b), 0*1)) .
>
% ?- between(1,13,N), search(typeof(X, [], (a->(b->a))), N, 0).
% N = 3,
% X = lam(a, lam(b, 1)) .
>
% ?- between(1,13,N), search(typeof(X, [], ((a->(a->b))->(a->b))), N, 0).
% N = 7,
% X = lam((a->a->b), lam(a, 1*0*0)) .
>
For example the 2nd solution with de Brujin indexs
can be read without de Brujin indexes as follows:
>
λx:a.λy:(a->b).(y x)    :    (a->((a->b)->b))
>
https://gist.github.com/Jean-Luc-Picard-2021/db6f71f66781838c98ee8b828eb5b9c2#file-minimal-p >
>
Mild Shock schrieb:

Hi,
>
Friendly Reminder that the Deadline 24. December 2024
is approaching. Please be aware that Weekend 3 asks for
Natural Deduction, where (E⊃) and Modus Ponens are synonymous:
>
/* Scope of Weekend 3 */
>
   C, X  ⊢  Y
-------------- (I⊃)
   C ⊢ X ⊃ Y
>
   C ⊢ X    C ⊢ X ⊃ Y
--------------------- (E⊃) /* Also known as Modus Ponens */
        C ⊢ Y
>
>
Simply Types and its Curry Howard is primarily defined
for Natural Deduction. Extracting Lambda Experessions
from Non-Natural Deduction is a little bit more complicated.
>
So Weekend 3 is NOT for Sequent Calculus:
>
/* Not Scope of Weekend 3 */
>
   C, X  ⊢  Y
-------------- (R⊃)
   C ⊢ X ⊃ Y
>
   C ⊢ X    C, Y ⊢ Z
--------------------- (L⊃)
     C, X ⊃ Y ⊢ Z
>
Bye
>
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
>

>

>