Path: ...!news.roellig-ltd.de!open-news-network.org!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Linear Logic as Natural Deduction (Was: Advent of Logic 2024:
 Friendly Reminder)
Date: Tue, 24 Dec 2024 00:22:49 +0100
Message-ID: <vkcrc9$19c05$1@solani.org>
References: <vjks2t$sghb$1@solani.org> <vk2i2c$1gvoe$1@solani.org>
 <vk6kfv$15r1k$1@solani.org> <vkcqk5$19bn1$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 23 Dec 2024 23:22:49 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1355781"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:wDhUZEVwbxkjkx10UidEm1g0/6U=
In-Reply-To: <vkcqk5$19bn1$1@solani.org>
X-User-ID: eJwNyUkBACAIBMBKuNxxBLR/BP3OKNuydjE10asX2SjhoeHxDMKmyuv95ajmIkvwgcjAEDKE3xUM7orx/QA3zxTM
Bytes: 4992
Lines: 133

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
>>>
>>
>