Path: ...!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: Re: Linear Logic as Natural Deduction (Was: Advent of Logic 2024:
 Friendly Reminder)
Date: Tue, 24 Dec 2024 00:24:15 +0100
Message-ID: <vkcreu$19c05$2@solani.org>
References: <vjks2t$sghb$1@solani.org> <vk2i2c$1gvoe$1@solani.org>
 <vk6kfv$15r1k$1@solani.org> <vkcqk5$19bn1$1@solani.org>
 <vkcrc9$19c05$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:24:14 -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:R44JNH64Fjyf9BuWAmrENFv/Kx8=
X-User-ID: eJwFwQkBwDAIA0BLZeWVQ0PwL2F3dl0coW6utrbgrIyVVPB7060aIYu5wAGLuakj18GIUx1JPgXZb0Re/octFx4=
In-Reply-To: <vkcrc9$19c05$1@solani.org>
Bytes: 5815
Lines: 160

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